text:
module Main

import Graphics.Rendering.Gl.Types
import Graphics.Rendering.Gl.Buffers
import Graphics.Rendering.Gl.Gl41
import Graphics.Rendering.Gl
import Graphics.Util.Glfw
import Graphics.Rendering.Config

%include C "GL/glew.h"
%flag C "-Wno-pointer-sign"

flatten : List (Double, Double, Double, Double) -> List Double
flatten [] = []
flatten ((a,b,c,d) :: xs) = [a,b,c,d] ++ (flatten xs)

showError : String -> IO ()
showError msg = do err <- glGetError
                   if err == 0
                   then putStrLn $ msg ++ " -  OK "
                   else putStrLn $ msg ++ (show err)

record Shaders where
  constructor MkShaders
  vertexShader : Int
  fragmentShader : Int
  program : Int

createShaders : IO (Either FileError Shaders)
createShaders = do
  glGetError
  vertexShader <- glCreateShader GL_VERTEX_SHADER

  showError "create vertex shader "
  Right vtx <- readFile "shader.vtx" | Left err => pure (Left err)
  glShaderSource vertexShader 1 [vtx] [(cast $ length vtx)]
  glCompileShader vertexShader

  fragmentShader <- glCreateShader GL_FRAGMENT_SHADER
  showError "create fragment shader "

  Right frg <- readFile "shader.frg" | Left err => pure (Left err)
  glShaderSource fragmentShader 1 [frg] [(cast $ length frg)]
  glCompileShader fragmentShader

  program <- glCreateProgram
  glAttachShader program vertexShader
  glAttachShader program fragmentShader
  showError "attach shaders "

  glLinkProgram program
  showError "link "
  glUseProgram program
  showError "use "

  printShaderLog vertexShader
  printShaderLog fragmentShader

  pure $ Right (MkShaders vertexShader fragmentShader program)

destroyShaders : Shaders -> IO ()
destroyShaders (MkShaders shader1 shader2 program) = do
  glGetError
  glUseProgram 0
  glDetachShader program shader1
  glDetachShader program shader2
  glDeleteShader shader1
  glDeleteShader shader2
  glDeleteProgram program
  pure ()

vertices : List (Double, Double, Double, Double)
vertices = [
    ( -0.8, -0.8, 0.0, 1.0),
    (  0.0,  0.8, 0.0, 1.0),
    (  0.8, -0.8, 0.0, 1.0)
  ]

colors : List (Double, Double, Double, Double)
colors = [
    (1.0, 0.0, 0.0, 1.0),
    (0.0, 1.0, 0.0, 1.0),
    (0.0, 0.0, 1.0, 1.0)
  ]

record Vao where
  constructor MkVao
  id : Int
  buffer1 : Int
  buffer2 : Int

createBuffers : IO Vao
createBuffers = do
  ds <- sizeofDouble
  glGetError

  (vao :: _) <- glGenVertexArrays 1

  glBindVertexArray vao
  (buffer :: colorBuffer :: _) <- glGenBuffers 2
  glBindBuffer GL_ARRAY_BUFFER buffer

  let data1 = (flatten vertices)
  ptr <- doublesToBuffer data1
  glBufferData GL_ARRAY_BUFFER (ds * (cast $ length data1)) ptr GL_STATIC_DRAW
  free ptr

  showError "vertex buffer data "
  glEnableVertexAttribArray 0
  glVertexAttribPointer 0 4 GL_DOUBLE GL_FALSE 0 prim__null

  glBindBuffer GL_ARRAY_BUFFER colorBuffer

  let data2 = (flatten colors)
  ptr2 <- doublesToBuffer data2
  glBufferData GL_ARRAY_BUFFER (ds * (cast $ length data2)) ptr2 GL_STATIC_DRAW
  free ptr2

  glEnableVertexAttribArray 1
  glVertexAttribPointer 1 4 GL_DOUBLE GL_FALSE 0 prim__null
  showError "color buffer "

  pure $ MkVao vao buffer colorBuffer

destroyBuffers : Vao -> IO ()
destroyBuffers (MkVao vao buffer colorBuffer) = do
  glDisableVertexAttribArray 1
  glDisableVertexAttribArray 0

  glBindBuffer GL_ARRAY_BUFFER 0

  glDeleteBuffers 2 [buffer, colorBuffer]

  glBindVertexArray 0

  glDeleteVertexArrays 1 [vao]

  showError "destroy buffers "

data State = MkState GlfwWindow Vao Shaders

draw : State -> IO ()
draw (MkState win vao (MkShaders _ _ prog)) = do
                   glClearColor 0 0 0 1
                   glClear GL_COLOR_BUFFER_BIT
                   glClear GL_DEPTH_BUFFER_BIT
                   glBindVertexArray (id vao)
                   glUseProgram prog

                   glDrawArrays GL_TRIANGLES 0 3
                   glfwSwapBuffers win

initDisplay : String -> Int -> Int -> IO GlfwWindow
initDisplay title width height = do
  glfw <- glfwInit
  glfwWindowHint GLFW_CONTEXT_VERSION_MAJOR  4
  glfwWindowHint GLFW_CONTEXT_VERSION_MINOR  1
  glfwWindowHint GLFW_OPENGL_FORWARD_COMPAT  1
  glfwWindowHint GLFW_OPENGL_PROFILE         (toInt GLFW_OPENGL_CORE_PROFILE)
  win <- glfwCreateWindow title width height defaultMonitor
  -- now we pretend every thing is going to be ok
  glfwMakeContextCurrent win
  glewInit
  info <- glGetInfo
  putStrLn info
  glEnable GL_DEPTH_TEST
  glDepthFunc GL_LESS
  pure win

main : IO ()
main = do win <- initDisplay "Hello Idris" 640 480
          glfwSetInputMode win GLFW_STICKY_KEYS 1
          glfwSwapInterval 0
          Right shaders <- createShaders | Left err => do
            putStrLn $ show err
            pure()
          vao <- createBuffers
          eventLoop $ MkState win vao shaders
          destroyBuffers vao
          destroyShaders shaders
          glfwDestroyWindow win
          glfwTerminate
          pure ()
       where
         eventLoop : State -> IO ()
         eventLoop state@(MkState win vao prog) = do
                      draw state
                      glfwPollEvents
                      key <- glfwGetFunctionKey win GLFW_KEY_ESCAPE
                      shouldClose <- glfwWindowShouldClose win
                      if shouldClose || key == GLFW_PRESS
                      then pure ()
                      else do
                        eventLoop state

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module Dep

interface Monad m => FooBar m where
  Foo : {0 a : Type} -> a -> m a -> Type
  Bar : {0 A : Type} -> m A -> Type
  foo : {0 A : Type} -> (x : A) -> (ma : m A) -> Foo x ma -> Bar ma

ext: idr


text:
||| The Error monad (also called the Exception monad).
module Control.Monad.Error.Interface

import Control.Monad.Error.Either
import Control.Monad.Maybe
import Control.Monad.RWS.CPS
import Control.Monad.Reader.Reader
import Control.Monad.State.State
import Control.Monad.Trans
import Control.Monad.Writer.CPS

%default total

||| The strategy of combining computations that can throw exceptions
||| by bypassing bound functions
||| from the point an exception is thrown to the point that it is handled.
||| Is parameterized over the type of error information and
||| the monad type constructor.
||| It is common to use `Either String` as the monad type constructor
||| for an error monad in which error descriptions take the form of strings.
||| In that case and many other common cases the resulting monad is already defined
||| as an instance of the 'MonadError' class.
public export
interface Monad m => MonadError e m | m where
  ||| Is used within a monadic computation to begin exception processing.
  throwError : e -> m a

  ||| A handler function to handle previous errors and return to normal execution.
  ||| A common idiom is:
  |||
  ||| ```idris example
  ||| do { action1; action2; action3 } `catchError` handler
  ||| ```
  catchError : m a -> (e -> m a) -> m a

||| Lifts an `Either e` into any `MonadError e`.
public export
liftEither : MonadError e m => Either e a -> m a
liftEither = either throwError pure

||| Makes a success or failure of an action visible in
||| the return type.
public export
tryError : MonadError e m => m a -> m (Either e a)
tryError action = (map Right action) `catchError` (pure . Left)

||| `MonadError` analogue to the `withEitherT` function.
||| Modify the value (but not the type) of an error.
||| If you need to change the type of `e` use `mapError`.
public export
withError : MonadError e m => (e -> e) -> m a -> m a
withError f action = tryError action >>= either (throwError . f) pure

||| Flipped version of `catchError`.
public export
handleError : MonadError e m => (e -> m a) -> m a -> m a
handleError = flip catchError

||| `MonadError` analogue of the `mapEitherT` function.  The
||| computation is unwrapped, a function is applied to the `Either`, and
||| the result is lifted into the second `MonadError` instance.
public export
mapError : (MonadError e m, MonadError e' n)
         => (m (Either e a) -> n (Either e' b)) -> m a -> n b
mapError f action = f (tryError action) >>= liftEither

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

public export
MonadError () Maybe where
  throwError ()        = Nothing
  catchError Nothing f = f ()
  catchError x       _ = x

public export
MonadError e (Either e) where
  throwError             = Left
  Left  l `catchError` h = h l
  Right r `catchError` _ = Right r

public export
Monad m => MonadError e (EitherT e m) where
  throwError = throwE
  catchError = catchE

public export
MonadError e m => MonadError e (MaybeT m) where
  throwError = lift . throwError
  catchError (MkMaybeT m) f = MkMaybeT (catchError m (runMaybeT . f))

public export
MonadError e m => MonadError e (ReaderT r m) where
  throwError = lift . throwError
  catchError (MkReaderT m) f =
    MkReaderT $ \e => catchError (m e) (runReaderT e . f)

public export
MonadError e m => MonadError e (StateT r m) where
  throwError = lift . throwError
  catchError (ST m) f =
    ST $ \s => catchError (m s) (runStateT s . f)

public export
MonadError e m => MonadError e (RWST r w s m) where
  throwError = lift . throwError
  catchError (MkRWST m) f =
    MkRWST $ \r,w,s => catchError (m r w s) (\e => unRWST (f e) r w s)

public export
MonadError e m => MonadError e (WriterT w m) where
  throwError = lift . throwError
  catchError (MkWriterT m) f =
    MkWriterT $ \w => catchError (m w) (\e => unWriterT (f e) w)


text:
module Data.List.Fixes

%default total
%access export

public export
data PrefixOfBy : (holdsFor : type -> type -> Type)
               -> (pref  : List type)
               -> (input : List type)
               -> Type where
   Empty  : PrefixOfBy p Nil xs
   Extend : (prf : p x y)
         -> PrefixOfBy p xs ys
         -> PrefixOfBy p (x::xs) (y::ys)

rightIsEmpty : PrefixOfBy p (x :: xs) [] -> Void
rightIsEmpty Empty impossible
rightIsEmpty (Extend _ _) impossible

notPrefix : (contra : p x y -> Void)
         -> PrefixOfBy p (x :: xs) (y :: ys)
         -> Void
notPrefix contra (Extend prf x) = contra prf

restNotPrefix : (contra : PrefixOfBy p xs ys -> Void)
             -> PrefixOfBy p (x :: xs) (y :: ys)
             -> Void
restNotPrefix contra (Extend x y) = contra y

isPrefixOfBy : (test : (x,y : type) -> Dec (p x y))
            -> (pref, input : List type)
            -> (Dec $ PrefixOfBy p pref input)
isPrefixOfBy test [] input = Yes Empty
isPrefixOfBy test (x :: xs) [] = No rightIsEmpty
isPrefixOfBy test (x :: xs) (y :: ys) with (test x y)
  isPrefixOfBy test (x :: xs) (y :: ys) | (Yes prf) with (isPrefixOfBy test xs ys)
    isPrefixOfBy test (x :: xs) (y :: ys) | (Yes prf) | (Yes z) = Yes (Extend prf z)
    isPrefixOfBy test (x :: xs) (y :: ys) | (Yes prf) | (No contra) =
      No (restNotPrefix contra)

  isPrefixOfBy test (x :: xs) (y :: ys) | (No contra) =
      No (notPrefix contra)

isPrefixOf : DecEq type
          => (pref, input : List type)
          -> Dec $ PrefixOfBy (=) pref input
isPrefixOf = isPrefixOfBy decEq

public export
SuffixOfBy : (holdsFor : type -> type -> Type)
          -> (pref  : List type)
          -> (input : List type)
          -> Type
SuffixOfBy holdsFor pref input =
  PrefixOfBy holdsFor (reverse pref) (reverse input)

isSuffixOfBy : (test : (x,y : type) -> Dec (p x y))
            -> (pref, input : List type)
            -> (Dec $ SuffixOfBy p pref input)
isSuffixOfBy test pref input =
  isPrefixOfBy test (reverse pref) (reverse input)

isSuffixOf : DecEq type
          => (suf, input : List type)
          -> (Dec $ SuffixOfBy (=) suf input)
isSuffixOf suf input =
  isSuffixOfBy decEq suf input


text:
import Data.Vect

-- Type synonym
Position : Type
Position = (Double, Double)

-- Type function with pattern matching
StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety-four"
getStringOrInt True = 94

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False x = trim x
valToString True x = cast x

valToString2 : (isInt : Bool) -> (case isInt of
  False => String
  True => Int) -> String
valToString2 False x = trim x
valToString2 True x = cast x

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

adder : (Num numType) => (numargs : Nat) -> (acc : numType) -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

data Format =
  Number Format | -- %d followed by tail
  Dbl Format |
  Str Format | -- %s followed by tail
  Chr Format |
  Lit String Format | -- Literal string followed by text
  End -- empty

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (s : String) -> PrintfType fmt
PrintfType (Chr fmt) = (c : Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (d : Double) -> PrintfType fmt
PrintfType (Lit text fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Dbl fmt) acc = \d => printfFmt fmt (acc ++ cast d)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ cast c)
printfFmt (Lit text fmt) acc = printfFmt fmt (acc ++ text)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: xs) = Number (toFormat xs)
toFormat ('%' :: 's' :: xs) = Str (toFormat xs)
toFormat ('%' :: 'c' :: xs) = Chr (toFormat xs)
toFormat ('%' :: 'f' :: xs) = Dbl (toFormat xs)
toFormat ('%' :: xs) = Lit "%" (toFormat xs)
toFormat (x :: xs) = case toFormat xs of
  Lit lit chars => Lit (strCons x lit) chars
  fmt => Lit (strCons x "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

-- Exercise 1 - define a Matrix as a nested vector of Double
Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]

-- Exercise 2 is Chr and Dbl above in printf

-- Exercise 3 - implement a vector as nested pairs, with the nesting calculated
-- from the length, e.g.,
-- TupleVect 0 ty = ()
-- TupleVect 1 ty = (ty, ())
-- TupleVect 2 ty = (ty, (ty, ()))
TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) x = (x, TupleVect k x)

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
import System

import System.Concurrency.Pipe

{-- TODO: REWRITE EVERYTHING!
testMakeQueue : IO ()
testMakeQueue = do putStrLn "--- Begin testMakeQueue ---"
                   qRef <- makeQueue
                   q <- readIORef qRef
                   f <- readIORef $ front q
                   putStrLn "Front empty?"
                   if length f /= 0
                      then putStrLn "ERROR: Front not initially empty"
                      else do putStrLn "\tYes"
                              r <- readIORef $ rear q
                              putStrLn "Rear empty?"
                              if length r /= 0
                                 then putStrLn "ERROR: Rear not initially empty"
                                 else do putStrLn "\tYes"
                                         putStrLn "Can acquire mutex?"
                                         mutexAcquire $ lock q
                                         putStrLn "\tYes"
                                         putStrLn "Can release mutex?"
                                         mutexRelease $ lock q
                                         putStrLn "\tYes"
                                         putStrLn "Success."
                   putStrLn "---  End testMakeQueue  ---\n"

testEnqueue : IO ()
testEnqueue = do putStrLn "--- Begin testEnqueue ---"
                 qRef <- makeQueue
                 q <- readIORef qRef
                 r <- readIORef $ rear q
                 if length r /= 0
                    then putStrLn "ERROR: Rear not initially empty"
                    else do enqueue qRef (prepare "testEnqueue")
                            q' <- readIORef qRef
                            r' <- readIORef $ rear q'
                            if length r' /= 1
                               then putStrLn "ERROR: Did not enqueue 1 item"
                               else putStrLn "Success."
                 putStrLn "---  End testEnqueue  ---\n"

testDequeue : IO ()
testDequeue = do putStrLn "--- Begin testDequeue ---"
                 qRef <- makeQueue
                 q <- readIORef qRef
                 f <- readIORef $ front q
                 r <- readIORef $ rear q
                 if length f /= 0 || length r /= 0
                    then putStrLn "ERROR: Queue not initially empty"
                    else do enqueue qRef (prepare "testDequeue")
                            dq <- dequeue qRef
                            case dq of
                                 Nothing => putStrLn "ERROR: Nothing dequeued"
                                 Just m => case unsafeOpen m String of
                                                "testDequeue" =>
                                                  do q' <- readIORef qRef
                                                     f' <- readIORef $ front q'
                                                     r' <- readIORef $ rear q'
                                                     if length f' /= 0 || length r' /= 0
                                                        then putStrLn "ERROR: Queue not empty afterwards"
                                                        else putStrLn "Success."

                                                _ =>
                                                  putStrLn "ERROR: Did not get same thing back"
                 putStrLn "---  End testDequeue  ---\n"

testPeek : IO ()
testPeek = do putStrLn "--- Begin testPeek ---"
              qRef <- makeQueue
              q <- readIORef qRef
              f <- readIORef $ front q
              r <- readIORef $ rear q
              if length f /= 0 || length r /= 0
                 then putStrLn "ERROR: Queue not initially empty"
                 else do enqueue qRef (prepare "testPeek")
                         pk <- peek qRef
                         case pk of
                              Nothing => putStrLn "ERROR: Peek got Nothing"
                              Just m => case unsafeOpen m String of
                                             "testPeek" =>
                                               do q' <- readIORef qRef
                                                  f' <- readIORef $ front q'
                                                  r' <- readIORef $ rear q'
                                                  if length f' /= 1 && length r' /= 0
                                                     then putStrLn "ERROR: Queue in unexpected state after peek"
                                                     else putStrLn "Success."

                                             _ =>
                                               putStrLn "ERROR: Did not get same thing back"
              putStrLn "---  End testPeek  ---\n"

runAll : IO ()
runAll = do testMakeQueue
            testEnqueue
            testDequeue
            testPeek

main : IO ()
main = runAll
--}


text:
module ZiriaCont

data FreerCont : (f : Type -> Type) -> Type -> Type where
  Cont : ({r : Type} -> (a -> r) -> ({x : Type} -> f x -> (x -> r) -> r) -> r) -> FreerCont f a

return : a -> FreerCont f a
return x = Cont (\k, _ => k x)

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

data Zir : (i : Type) -> (o : Type) -> (v : Type) -> Type where
  Yield : o -> Zir i o ()
  NeedInput : Zir i o i

emit : o -> FreerCont (Zir i o) ()
emit o = Cont (\k, imp => imp (Yield o) k)

take : FreerCont (Zir i o) i
take = Cont (\k, imp => imp NeedInput k)

data Rec : (x : Type) -> (r : Type) -> Type where
  K : ((x -> Rec x r -> r) -> r) -> Rec x r

gImp :  ({y : Type} -> Zir i o y -> (y -> r) -> r) -> Zir m o x -> (x -> Rec m r -> r) -> Rec m r -> r
gImp imp (Yield ot) k rec = imp (Yield ot) (\() => k () rec)
gImp imp NeedInput k (K k') = k' k

fImp :  ({y : Type} -> Zir i o y -> (y -> r) -> r) -> Zir i m x -> (x -> (m -> Rec m r -> r) -> r) -> (m -> Rec m r -> r) -> r
fImp imp (Yield ot) k k' = k' ot (K (k ()))
fImp imp NeedInput k k' = imp NeedInput (\i => k i k')

infixl 9 >>>
(>>>) : FreerCont (Zir i m) v -> FreerCont (Zir m o) v -> FreerCont (Zir i o) v
(>>>) (Cont f) (Cont g) = Cont (\k, imp => let g' = g (\x, _ => k x) (gImp imp) in
                                           let f' = f (\x, _ => k x) (fImp imp) in
                                           g' (K f'))

imp : Zir i o x -> (x -> Stream i -> (v, List o)) -> Stream i -> (v, List o)
imp (Yield x) k xs = let (v, xs') = k () xs in (v, x :: xs')
imp NeedInput k (x :: xs) = k x xs

run : FreerCont (Zir i o) v -> Stream i -> (v, List o)
run (Cont f) = f k imp
 where
   k : v -> Stream i -> (v, List o)
   k x _ = (x, [])

example : FreerCont (Zir Int Int) Int
example = do x <- take
             emit (x + 1)
             y <- take
             emit (y + 2)
             return (x + y)

test : (Int, List Int)
test = run example [1..]

stream1 : FreerCont (Zir Int Int) Int
stream1 = do emit 1
             emit 2
             return 41

stream2 : FreerCont (Zir Int Int) Int
stream2 = do x <- take
             y <- take
             emit (x + y)
             return 42

test' : (Int, List Int)
test' = run (stream1 >>> stream2) [1..]

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Main

import Oyster.Core

%default total

{-
  EBNF grammar:

  expr ::= term ( + expr | - expr | epsilon )
  term ::= factor ( * expr | / expr | epsilon )
  factor ::= ( expr ) | integer
  integer ::= ... -2 | -1 | 0 | 1 | 2 | ...
-}

mutual
  partial
  expr : Parser Int
  expr = do t <- term
            do symbol "+"
               e <- expr
               pure (t + e)
             <|> do symbol "-"
                    e <- expr
                    pure (t - e)
             <|> pure t

  partial
  term : Parser Int
  term = do f <- factor
            do symbol "*"
               t <- term
               pure (f * t)
             <|> do symbol "/"
                    t <- term
                    pure (f `div` t)
             <|> pure f

  partial
  factor : Parser Int
  factor = do symbol "("
              e <- expr
              symbol ")"
              pure e
            <|> integer

eval : String -> Maybe Int
eval inp = case parse expr inp of
                [(n, "")] => Just n
                _ => Nothing

main : IO ()
main = do expr <- getLine
          pure ()

max_stars_repo_name: timmyjose-compilers/oyster

max_issues_repo_name: timmyjose-compilers/oyster

max_forks_repo_name: timmyjose-compilers/oyster


text:
> module Rel.Operations

> %default total
> %access public export

> |||
> pair : (a -> b -> Type, a -> c -> Type) -> a -> (b, c) -> Type
> pair (R, S) a (b, c) = (R a b, S a c)

> |||
> cross : (a -> c -> Type) -> (b -> d -> Type) -> (a, b) -> (c, d) -> Type
> cross R S (a, b) (c, d) = (R a c, S b d)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
mySum : (Num a) => List a -> a
mySum [] = 0
mySum (x::xs) = x + sum xs

main : IO ()
main = print (mySum [0..10000]) >>= \x => putStrLn ""


text:
||| Functions for the processing of received request and notifications.
|||
||| (C) The Idris Community, 2021
module Server.ProcessMessage

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Idris.ModTree
import Idris.Package
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Server.Capabilities
import Server.Configuration
import Server.Log
import Server.Response
import Server.Utils
import System

||| Guard for messages that requires a successful initialization before being allowed.
whenInitialized : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenInitialized k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => sendUnknownResponseMessage serverNotInitialized

||| Guard for messages that cannot be sent after the shutdown protocol.
whenNotShutdown : Ref LSPConf LSPConfiguration => Core () -> Core ()
whenNotShutdown k =
  if !(gets LSPConf isShutdown)
     then sendUnknownResponseMessage (invalidRequest "Server has been shutdown")
     else k

||| Process a parsed LSP message received from a client.
export
processMessage : Ref LSPConf LSPConfiguration
              => Ref Ctxt Defs
              => Ref UST UState
              => Ref Syn SyntaxInfo
              => Ref MD Metadata
              => Ref ROpts REPLOpts
              => {type : MethodType}
              -> (method : Method Client type)
              -> Message type method
              -> Core ()
processMessage Initialize msg@(MkRequestMessage id Initialize params) = do
  -- TODO: Here we should analyze the client capabilities.
  let response = Success (getResponseId msg) (MkInitializeResult serverCapabilities (Just serverInfo))
  -- The compiler does not work with the same root directory model that LSP operates with,
  -- may be a point of friction in particular with the location of generated binary files.
  setSourceDir (path <$> toMaybe params.rootUri)
  sendResponseMessage Initialize response
  update LSPConf (record {initialized = Just params})
processMessage Shutdown msg@(MkRequestMessage _ Shutdown _) = do
  -- In a future multithreaded model, we must guarantee that all pending request are still executed.
  let response = Success (getResponseId msg) (the (Maybe Null) Nothing)
  sendResponseMessage Shutdown response
  update LSPConf (record {isShutdown = True})
processMessage Exit (MkNotificationMessage Exit _) = do
  let status = if !(gets LSPConf isShutdown) then ExitSuccess else ExitFailure 1
  coreLift $ exitWith status
processMessage TextDocumentDidOpen msg@(MkNotificationMessage TextDocumentDidOpen params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Just (params.textDocument.uri, params.textDocument.version)})
    -- TODO: the compiler works directly with the file, we should upstream some changes to allow it to work with the
    --       source passed by the client.
    resetContext
    setSourceDir (path <$> toMaybe conf.rootUri)
    errs <- buildDeps params.textDocument.uri.path -- FIXME: the compiler always dumps the errors on stdout, requires
                                                   --        a compiler change.
    setSource params.textDocument.text
    resetProofState
    sendDiagnostics params.textDocument.uri (Just params.textDocument.version) errs
processMessage TextDocumentDidChange msg@(MkNotificationMessage TextDocumentDidChange params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Just (params.textDocument.uri, params.textDocument.version)})
    -- TODO: same issue of TextDocumentDidOpen
    resetContext
    setSourceDir (path <$> toMaybe conf.rootUri)
    let (Left source :: _) = params.contentChanges
      | _  => do logString Error $ "Error in textDocument/didChange expected format"
                 sendUnknownResponseMessage (invalidParams "Expected one full TextDocumentContentChangeEvent")
    errs <- buildDeps params.textDocument.uri.path -- FIXME: add string version to the compiler (requires upstream change, probably)
                                                   -- FIXME: stop emitting errors on stdout (requires upstream change)
    setSource source.text
    resetProofState
    sendDiagnostics params.textDocument.uri (Just params.textDocument.version) errs
processMessage TextDocumentDidClose msg@(MkNotificationMessage TextDocumentDidClose params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    update LSPConf (record {openFile = Nothing})
    logString Info $ "File " ++ params.textDocument.uri.path ++ " closed"
processMessage TextDocumentHover msg@(MkRequestMessage id TextDocumentHover params) =
  whenNotShutdown $ whenInitialized $ \conf => do
    -- Temporary measure for examples
    let fpath = params.textDocument.uri.path
    fname <- fromMaybe fpath <$> findIpkg (Just fpath)
    res <- loadMainFile fname
    -- TODO: do something with the errors

    -- FIXME: Checks local definitions only because we currently do not store the FC of global name calls :(
    Just (n, num, tm) <- findTypeAt (\p, n => within (params.position.line - 1, params.position.character - 1) p)
      | Nothing => do let response = Success (getResponseId msg) (Left $ MkHover (Right $ Right $ MkMarkupContent PlainText "") Nothing)
                      sendResponseMessage TextDocumentHover response
    defs <- get Ctxt
    term <- resugar [] !(normaliseHoles defs [] tm)
    let typeline = renderString $ unAnnotateS $ layoutUnbounded $ pretty (nameRoot n) <++> colon <++> prettyTerm term
    let markup = MkMarkupContent PlainText typeline
    let response = Success (getResponseId msg) (Left $ MkHover (Right $ Right markup) Nothing)
    sendResponseMessage TextDocumentHover response
processMessage {type = Request} method msg =
  whenNotShutdown $ whenInitialized $ \conf => do
    logString Warning $ "received a not supported" ++ show (toJSON method) ++ " request"
    sendResponseMessage method (methodNotFound msg)
processMessage {type = Notification} method msg =
  whenNotShutdown $ whenInitialized $ \conf =>
    logString Warning "unhandled notification"


text:
module Gen.TypeChecker

import Control.Monad.Identity
import Control.Monad.State

public export
interface TypeCheckerState s sig defs ctx | s where
	typeCheckerSig : s -> sig
	putTypeCheckerSig : s -> sig -> s
	typeCheckerDefs : s -> defs
	putTypeCheckerDefs : s -> defs -> s
	addTypeCheckerDefs : s -> defs -> s
	typeCheckerCtx : s -> ctx
	putTypeCheckerCtx : s -> ctx -> s
	addTypeCheckerCtx : s -> ctx -> s
	typeCheckerNextName : s -> Int
	putTypeCheckerNextName : s -> Int -> s

public export
interface (TypeCheckerState s sig defs ctx, Monad m, MonadState s m) => TCMonad (m : Type -> Type) s sig defs ctx | m
where {}

public export
signature : TCMonad m s sig defs ctx => m (sig)
signature {s} = map (typeCheckerSig {s}) get

public export
putSignature : TCMonad m s sig defs ctx => sig -> m ()
putSignature {s} sig = do
	ss <- get
	put (putTypeCheckerSig {s} ss sig)

public export
definitions : TCMonad m s sig defs ctx => m (defs)
definitions {s} = map (typeCheckerDefs {s}) get

public export
putDefinitions : TCMonad m s sig defs ctx => defs -> m ()
putDefinitions {s} defs = do
	ts <- get
	put (putTypeCheckerDefs {s} ts defs)

public export
extendDefinitions : TCMonad m s sig defs ctx => defs -> m a -> m a
extendDefinitions {s} edefs tc = do
	ts <- get
	put (addTypeCheckerDefs {s} ts edefs)
	x <- tc
	putDefinitions {s} (typeCheckerDefs ts)
	pure x

public export
context : TCMonad m s sig defs ctx => m (ctx)
context {s} = map (typeCheckerCtx {s}) get

public export
putContext : TCMonad m s sig defs ctx => ctx -> m ()
putContext {s} ctx = do
	ts <- get
	put (putTypeCheckerCtx {s} ts ctx)

public export
extendContext : TCMonad m s sig defs ctx => ctx -> m a -> m a
extendContext {s} ectx tc = do
	ts <- get
	put (addTypeCheckerCtx {s} ts ectx)
	x <- tc
	putContext {s} (typeCheckerCtx ts)
	pure x

public export
newName : TCMonad m s sig defs ctx => m Int
newName {s} = do
	ts <- get
	let n = typeCheckerNextName {s} ts
	put (putTypeCheckerNextName ts (n+1))
	pure $ n

public export
interface TypeCheckerMetas s subs | s where
	typeCheckerNextMeta : s -> Int
	putTypeCheckerNextMeta : s -> Int -> s
	typeCheckerSubs : s -> subs
	putTypeCheckerSubs : s -> subs -> s

public export
interface (TCMonad m s sig defs ctx, TypeCheckerMetas s subs) => TCPolyMonad (m : Type -> Type) s sig defs ctx subs | m
where {}

public export
newMetaVar : TCPolyMonad m s sig defs ctx subs => m Int
newMetaVar {s} = do
	ts <- get
	let n = typeCheckerNextMeta {s} ts
	put (putTypeCheckerNextMeta ts (n+1))
	pure n

public export
substitution : TCPolyMonad m s sig defs ctx subs => m subs
substitution {s} = map (typeCheckerSubs {s}) get

public export
putSubstitution : TCPolyMonad m s sig defs ctx subs => subs -> m ()
putSubstitution {s} subs = do
	ts <- get
	put (putTypeCheckerSubs {s} ts subs)

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Linear

import ZZ
import Rationals
import Data.Vect

%access public export

data SolExists : Type where
  YesExists : SolExists
  DNExist : SolExists

isFactor : Nat -> Nat -> Type
isFactor m n = (k : Nat ** (m * k = n)) -- will be useful in solving Diophantine equations:
                                        -- if the denominator is a factor of the numerator, there is an integer solution

is_a_zero: (a: ZZ) -> Bool
is_a_zero (Pos Z) = True
is_a_zero (Pos (S k)) = False
is_a_zero (NegS k) = False

ApZZ : (f: ZZ -> ZZ)-> n = m -> f n = f m -- like apNat, but for ZZ
ApZZ f Refl = Refl

-- Helper functions for the case ax = 0 --

ZeroSum: (a: ZZ) -> (b: ZZ) -> (a = 0) -> (b = 0) -> (a + b = 0) --sum of two zeroes is zero
ZeroSum (fromInt(0)) (fromInt(0)) Refl Refl = Refl

triviality1: (a: ZZ) -> (b: ZZ) -> (b = 0) -> (a*b=0) -- premultiplying 0 by anything returns 0
triviality1 a b prf = trans (apZZ (\x => a*x) b 0 prf) (multZeroRightZeroZ(a))

triviality2: (a: ZZ) -> (0*a=0) -- 0 times anything is zero
triviality2 a = multZeroLeftZeroZ(a)

triviality3: (a: ZZ) -> (a*0=0) -- 0 times anything is zero
triviality3 a = multZeroRightZeroZ(a)

ZeroProof: (a: ZZ) -> (b: ZZ) -> (b = 0) -> (0*a + 1*b = 0) -- shows that the rational number (0,1) satisfies ax = 0
ZeroProof a b prf = trans (trans (ApZZ (\x=> x + 1*b) (triviality2 a)) (ApZZ (\x => 0 + x) (triviality1 1 b prf))) (ZeroSum 0 0 Refl Refl)

-- Helper functions for the case ax + b = 0

triviality4: (a: ZZ) -> (b: ZZ) -> (a*b = b*a)
triviality4 a b = multCommutativeZ a (b)

triviality5: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a = a*(-b) + a*b )
triviality5 a b = ApZZ (\x=> a*(-b) + x) (triviality4 b a)

triviality6: (a: ZZ) -> (b: ZZ) -> ( (a*(-b)) + (a*b) = a*( (-b)+b ) )
triviality6 a b = sym ( multDistributesOverPlusRightZ a (-b) b )

triviality7: (a: ZZ) -> (b: ZZ) -> ( a*((-b) + b) = 0)
triviality7 a b = trans (ApZZ (\x => a*x) (plusNegateInverseRZ(b))) (triviality3(a))

SolutionProof: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a=0)
SolutionProof a b = trans (trans (triviality5 a b) (triviality6 a b)) (triviality7 a b)

--Solving a linear equation ax + b = 0 in the case when b = 0 (Basically, this shows that ax=0 is uniquely solved by (0,1))

trivialeqSolver : (a: ZZ) -> (b : ZZ) -> (b = 0) -> Either (x : ZZPair ** (SolExists, (fst x)*a + (snd x)*b = 0)) (SolExists)
trivialeqSolver a b prf = Left ((0,1) ** (YesExists, (ZeroProof a b prf)))

-- Solving the linear equation ax+b = 0 in general

eqSolver : (a: ZZ) -> (b : ZZ) -> (ZZNotZero b) -> Either (x : ZZPair ** (SolExists, a*(fst x) + b*(snd x) = 0)) (SolExists)
eqSolver a b prf = case (is_a_zero(a)) of
  (True) => Right (DNExist)
  (False) => Left ((-b, a) ** (YesExists, (SolutionProof a b))) -- The solution is (-b/a), a rational number, with proof.

-- Helper functions for ax + b = c

helper1: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a*(c+(-b))= a*c + a*(-b))
helper1 a b c = multDistributesOverPlusRightZ (a) (c) (-b)

helper2: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> ( a*(c-b) + b*a = a*c+ a*(-b)+ b*a )
helper2 a b c = ApZZ (\x => x+ b*a) (helper1 (a) (b) (c))

helper3: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a= 0)
helper3 a b = trans (trans (triviality5 a b) (triviality6 a b)) (triviality7 a b)

helper4: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a*c + a*(-b) + b*a = a*c)
helper4 a b c = rewrite sym (plusAssociativeZ (a*c) (a*(-b)) (b*a)) in
                rewrite helper3 a b in
                rewrite plusZeroRightNeutralZ (multZ a c) in Refl

GeneralProof: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> ( a*(c-b) + b*a = a*c )
GeneralProof a b c = trans (helper2 a b c) (helper4 a b c)

-- Solving the linear equation ax + b = c (2x +3 = 7, for example) over the rationals

GeneralEqSolver: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a0: ZZNotZero a) -> (b0: ZZNotZero b) -> (c0: ZZNotZero c) ->
(x : ZZPair ** (SolExists, a*(fst x) + b*(snd x) = (snd x)*c))
GeneralEqSolver a b c a0 b0 c0 = ( ( (c-b) , a ) ** (YesExists, (GeneralProof a b c) )) -- Solves the equation with proof

-- Now, we can use the rational solution of the linear equation ax + b = c to check whether this equation has an integer
-- solution; if it did, the denominator of the rational solution would divide the numerator. If it didn't, the equation
-- would have no solutions in the integers.


text:
= The Second Tale

> module WhoStoleTheTarts.TheSecondTale
>
> %access export
> %default total

This time, someone stole the flour!
<blockquote>
Find the miscreant, and take his head off!
</blockquote>

== Suspects

We know it was one of the March Hare, the Mad Hatter and the Dormouse.

> data MarchHare
>
> data MadHatter
>
> data Dormouse
>
> SomeoneStoleTheFlour : Type
> SomeoneStoleTheFlour = Either (    MarchHare, Not MadHatter, Not Dormouse)
>                      $ Either (Not MarchHare,     MadHatter, Not Dormouse)
>                               (Not MarchHare, Not MadHatter,     Dormouse)

== Statements

The March Hare claims the Hatter stole it.

> MarchHareStatement : (truth : Bool) -> Type
> MarchHareStatement False = Not MadHatter
> MarchHareStatement True = (Not MarchHare, MadHatter, Not Dormouse)

The thief told the truth...

> MadHatterStatement : (truth : Bool) -> Type
> MadHatterStatement False = Not MadHatter
> MadHatterStatement True = (Not MarchHare, MadHatter, Not Dormouse)

> DormouseStatement : (truth : Bool) -> Type
> DormouseStatement False = Not Dormouse
> DormouseStatement True = (Not MarchHare, Not MadHatter, Dormouse)

== Revelation

... and is the only one who did.

> Revelation : Type
> Revelation = Either ( (MarchHareStatement True, MarchHare)
>                     , MadHatterStatement False
>                     , DormouseStatement  False )
>                     ( Either ( MarchHareStatement False
>                              , MadHatterStatement True
>                              , DormouseStatement  False )
>                              ( MarchHareStatement False
>                              , MadHatterStatement False
>                              , DormouseStatement  True ) )

== Conclusion

> lemma1 : SomeoneStoleTheFlour
>       -> (Not MarchHare, Not MadHatter)
>       -> Dormouse
> lemma1 (Left (marchHare, _)) (toBlame, _)
>   = absurd (toBlame marchHare)
> lemma1 (Right (Left (_, madHatter, _))) (_, toBlame)
>   = absurd (toBlame madHatter)
> lemma1 (Right (Right (it, was, dormouse))) obviously
>   = dormouse

Given the [statements](#statements) above and the [revelation](#revelation),

> Thief : SomeoneStoleTheFlour -> Revelation

... we can conclude the Dormouse stole the flour.

>      -> (Not MarchHare, Not MadHatter, Dormouse)

Let's assume the March Hare did it. If so, then they told the truth, which would
mean that the Hatter stole the flour. They couldn't both have done it, so the
March Hare must have lied, which means they and the Mad Hatter are innocent.

> Thief (Left marchHare) (Left (((_, madHatter, _), _), toBlame, _))
>   = absurd (toBlame madHatter)
> Thief (Right (Left (toBlame, _))) (Left ((_, marchHare), _))
>   = absurd (toBlame marchHare)

If it was neither the March Hare nor the Mad Hatter,
then it must've been the Dormouse.

> Thief someone (Right (Left (notHatter, (notMarchHare, _), _)))
>   = let dormouse = lemma1 someone (notMarchHare, notHatter) in
>     (notMarchHare, notHatter, dormouse)
> Thief (Right (Right dormouse)) _ = dormouse

If the Dormouse told the truth,
then they stole the flour.

> Thief _ (Right (Right (_, _, dormouse))) = dormouse

∎

max_stars_repo_name: yurrriq/alice-in-puzzleland

max_issues_repo_name: yurrriq/alice-in-puzzleland

max_forks_repo_name: yurrriq/alice-in-puzzleland


text:
module Subtyping

import Expr
import Maps

%access public export

%default total

data Ty : Type where
  TyTop : Ty
  TyBool : Ty
  TyBase : Id -> Ty
  TyArrow : Ty -> Ty -> Ty
  TyUnit : Ty

namespace Types
  A : Ty
  A = TyBase A

  B : Ty
  B = TyBase B

  C : Ty
  C = TyBase C

  D : Ty
  D = TyBase D

  E : Ty
  E = TyBase E

  F : Ty
  F = TyBase F

data Tm : Type where
  Var : Id -> Tm
  App : Tm -> Tm -> Tm
  Abs : Id -> Ty -> Tm -> Tm
  Tru : Tm
  Fls : Tm
  Test : Tm -> Tm -> Tm -> Tm
  Unit : Tm

subst : (x : Id) -> (s, t : Tm) -> Tm
subst x s (Var y) with (decEq x y)
  subst x s (Var y) | Yes _ = s
  subst x s (Var y) | No _ = Var y
subst x s (App t1 t2) = App (subst x s t1) (subst x s t2)
subst x s (Abs y ty t) with (decEq x y)
  subst x s (Abs y ty t) | Yes _ = Abs y ty t
  subst x s (Abs y ty t) | No _ = Abs y ty (subst x s t)
subst x s Tru = Tru
subst x s Fls = Fls
subst x s (Test t1 t2 t3) = Test (subst x s t1) (subst x s t2) (subst x s t3)
subst x s Unit = Unit

data Value : Tm -> Type where
  V_Abs : Value (Abs x ty t)
  V_Tru : Value Tru
  V_Fls : Value Fls
  V_Unit : Value Unit

data Step : Tm -> Tm -> Type where
  ST_AppAbs : Value t2 -> Step (App (Abs x ty t1) t2) (subst x t2 t1)
  ST_App1 : Step t1 t1' -> Step (App t1 t2) (App t1' t2)
  ST_App2 : Value t1 -> Step t2 t2' -> Step (App t1 t2) (App t1 t2')
  ST_Test : Step t1 t1' -> Step (Test t1 t2 t3) (Test t1' t2 t3)
  ST_TestTru : Step (Test Tru t2 t3) t2
  ST_TestFls : Step (Test Fls t2 t3) t3

infix 4 -+>

(-+>) : Tm -> Tm -> Type
(-+>) = Step

data Subtype : Ty -> Ty -> Type where
  S_Refl : Subtype ty ty
  S_Trans : Subtype ty1 ty2 -> Subtype ty2 ty3 -> Subtype ty1 ty3
  S_Top : Subtype ty TyTop
  S_Arrow : Subtype ty3 ty1 -> Subtype ty2 ty4 ->
            Subtype (TyArrow ty1 ty2) (TyArrow ty3 ty4)

infix 4 <:

(<:) : Ty -> Ty -> Type
(<:) = Subtype

subtyping_example_0 : TyArrow C TyBool <: TyArrow C TyTop
subtyping_example_0 = S_Arrow S_Refl S_Top


text:
module Physics.Vector2D

public export
Vector2D : Type
Vector2D = (Double, Double)

export
Num Vector2D where
  (a1, b1) + (a2, b2) = (a1+a2, b1+b2)
  (a1, b1) * (a2, b2) = (a1*a2, b1*b2)
  fromInteger a = (cast a, cast a)

export
Neg Vector2D where
  negate (x, y) = (-x, -y)
  (x2, y2) - (x1, y1) = (x2-x1, y2-y1)

export
Abs Vector2D where
  abs (x, y) = (abs x, abs y)

export
norm : Vector2D -> Double
norm (x, y) = sqrt $ x*x + y*y

export
scale : Double -> Vector2D -> Vector2D
scale a (x, y) = (a*x, a*y)

infix 7 `scale`

public export
Cast (Integer, Integer) Vector2D where
  cast (x, y) = (the Double (cast x), the Double (cast y))

public export
Cast Vector2D (Int, Int) where
  cast (x, y) = (cast x, cast y)

export
nullVector : Vector2D
nullVector = (0, 0)

export
magnitude : Vector2D -> Double
magnitude (a, b) = sqrt(a*a + b*b)

export
normed : Vector2D -> Vector2D
normed x = let magnitude' = 1.0/(magnitude x) in magnitude' `scale` x

export
angle : Vector2D -> Double
angle (x, y) = atan2 y x


text:
||| Fresh lists, a variant of Catarina Coquand's contexts in "A
||| Formalised Proof of the Soundness and Completeness of a Simply
||| Typed Lambda-Calculus with Explicit Substitutions"
|||
||| Based directly on Agda's fresh lists:
||| http://agda.github.io/agda-stdlib/Data.List.Fresh.html
module FreshList

import public Data.So

%default total

-- Boolean "relation"
public export
BRel : Type -> Type
BRel a = a -> a -> Bool

infix 4 #, ##, #?

public export
data FreshVect : Nat -> (a : Type) -> (neq : BRel a) -> Type

-- The boolean version
public export
(##) : {neq : BRel a} -> (x : a) -> (xs : FreshVect l a neq) -> Bool
-- The type version
public export
(#) : {neq : BRel a} -> (x : a) -> (xs : FreshVect l a neq) -> Type

public export
data FreshVect : Nat -> (a : Type) -> (neq : BRel a) -> Type where
  Nil  : FreshVect Z a neq
  (::) : (x : a) -> (xs : FreshVect l a neq) ->
         {auto 0 fresh : x # xs} ->
         FreshVect (S l) a neq

%name FreshVect xs, ys, zs

x ##    []     = True
x ## (y :: xs) = (x `neq` y) && (x ## xs)

x # xs = So (x ## xs)

export
toList : FreshVect l a p -> List a
toList [] = []
toList (x :: xs) = x :: toList xs

export
Show a => Show (FreshVect l a p) where
  show = show . toList

parameters
  {0 A : Type} {0 Aneq : BRel A}
  {0 B : Type} {0 Bneq : BRel B}
  (F : A -> B)
  (Injectivity : (x,y : A) -> So (x `Aneq` y) -> So (F x `Bneq` F y))

  public export
  map : FreshVect l A Aneq -> FreshVect l B Bneq

  public export
  0 mapFreshness : {x : A} -> (ys : FreshVect l A Aneq) ->
                   x # ys -> F x # map ys

  map     []              = []
  map ((x :: xs) {fresh}) = (F x :: map xs) {fresh = mapFreshness xs fresh}

  mapFreshness    []              _
    = Oh
  mapFreshness (y :: ys) p
    = let (x_fresh_y, x_fresh_ys) = soAnd p in
      andSo (Injectivity _ _ x_fresh_y, mapFreshness ys x_fresh_ys)

namespace View
  public export
  data Empty : FreshVect Z a neq -> Type where
    Nil : Empty Nil

  public export
  data NonEmpty : FreshVect (S l) a neq -> Type where
    IsNonEmpty : NonEmpty ((x :: xs) {fresh})

public export
length : FreshVect l a neq -> Nat
length [] = 0
length (x :: xs) = 1 + length xs

public export
fromMaybe : Maybe a -> (l ** FreshVect l a neq)
fromMaybe Nothing  = (Z ** [])
fromMaybe (Just x) = (1 ** [x])

-- I don't include replicate since freshness ought not to be
-- reflexive, but feel free to add it if you need it

public export
uncons : FreshVect (S l) a neq -> (a , FreshVect l a neq)
uncons (x :: xs) = (x, xs)

public export
head : (xs : FreshVect (S l) a neq) -> a
head (x :: xs) = x

public export
tail : (xs : FreshVect (S l) a neq) -> FreshVect l a neq
tail (x :: xs) = xs

public export
0 (.freshness) : (xs : FreshVect (S l) a neq) ->
                 head xs # tail xs
(((x :: xs) {fresh}).freshness) = fresh

-- Freshness lemmata
parameters (0 x : a) (ys : FreshVect (S l) a neq)
  public export
  0 headFreshness : x # ys -> So (x `neq` head ys)

  public export
  0 tailFreshness : x # ys -> x # (tail ys)

headFreshness x (y :: ys) freshness
  = fst (soAnd freshness)
tailFreshness x (y :: ys) freshness
  = snd (soAnd freshness)

public export
take : (n : Nat) -> FreshVect (n + m) a neq -> FreshVect n a neq
public export
0 takeFreshness : (n : Nat) -> (xs : FreshVect (n + m) a neq) -> y # xs -> y # take n {m} xs

take 0     xs                  = []
take (S n) ((x :: xs) {fresh}) = (x :: take n xs) {fresh = takeFreshness {m} n xs fresh}

takeFreshness  0          xs  fresh = Oh
takeFreshness (S n) (x :: xs) fresh =
  let (y_neq_x, y_fresh_xs) = soAnd fresh in
  andSo (y_neq_x, takeFreshness n xs y_fresh_xs)

public export
drop : (n : Nat) -> FreshVect (n + m) a neq -> FreshVect m a neq
drop 0           xs  = xs
drop (S n) (x :: xs) = drop n xs

-- The Agda lib has more general takeWhile, dropWhile, filter
-- involving decidable predicts, but we follow the Idris stdlib and
-- use the special case for Bool

-- public export
-- takeWhile : (pred : a -> Bool) -> FreshVect l a neq -> (m ** FreshVect m a neq)
-- public export
-- 0 takeWhileFreshness : (pred : a -> Bool) -> (xs : FreshVect l a neq) ->
--   y # xs -> y # (takeWhile pred xs).snd
--
-- takeWhile pred     []              = (Z ** [])
-- takeWhile pred ((x :: xs) {fresh}) = case pred x of
--   True  => let (n ** rec) = takeWhile pred xs
--              ; res = (x :: rec) {fresh = takeWhileFreshness pred xs fresh} in
--              (S n ** res)
--   False => (Z ** [])

-- takeWhileFreshness  pred []           fresh
--   = Oh
-- takeWhileFreshness  pred (x :: xs) fresh with (pred x)
--  takeWhileFreshness pred (x :: xs) fresh | True
--   = let (y_fresh_x, y_fresh_xs) = soAnd fresh in
--     andSo (y_fresh_x, takeWhileFreshness pred xs y_fresh_xs)
--  takeWhileFreshness pred (x :: xs) fresh | False
--   = Oh
--
-- public export
-- dropWhile : (pred : a -> Bool) -> FreshVect a neq -> FreshVect a neq
--
-- public export
-- 0 dropWhileFreshness : (pred : a -> Bool) -> (xs : FreshVect a neq) ->
--   y # xs -> y # dropWhile pred xs
--
--
-- dropWhile pred     []              = []
-- dropWhile pred ((x :: xs) {fresh}) = case pred x of
--   True  => (x :: dropWhile pred xs) {fresh = dropWhileFreshness pred xs fresh}
--   False => []
--
-- dropWhileFreshness  pred    []     fresh = Oh
-- dropWhileFreshness  pred (x :: xs) fresh with (pred x)
--  dropWhileFreshness pred (x :: xs) fresh | False
--    = Oh
--  dropWhileFreshness pred (x :: xs) fresh | True
--    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
--      andSo (y_neq_x, dropWhileFreshness pred xs y_fresh_xs)
--
-- public export
-- filter : (pred : a -> Bool) -> FreshVect a neq -> FreshVect a neq
-- public export
-- 0 filterFreshness : (pred : a -> Bool) -> (xs : FreshVect a neq) ->
--   y # xs -> y # filter pred xs
--
-- filter pred     []              = []
-- filter pred ((x :: xs) {fresh}) = case pred x of
--   False => filter pred xs
--   True  => (x :: filter pred xs) {fresh = filterFreshness pred xs fresh}
--
-- filterFreshness  pred    []     fresh = Oh
-- filterFreshness  pred (x :: xs) fresh with (pred x)
--  filterFreshness pred (x :: xs) fresh | False
--    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
--      filterFreshness pred xs y_fresh_xs
--  filterFreshness pred (x :: xs) fresh | True
--    = let (y_neq_x, y_fresh_xs) = soAnd fresh in
--      andSo (y_neq_x, filterFreshness pred xs y_fresh_xs)

-- Todo: move `decSo : (b : Bool) -> Dec (So b)` to base
public export
decideFreshness : {neq : BRel a} ->
                  (x : a) -> (ys : FreshVect l a neq) ->
                  Dec (x # ys)
decideFreshness x ys with (x ## ys)
  decideFreshness x ys | True  = Yes Oh
  decideFreshness x ys | False = No absurd

public export
foldl : (f : b -> a -> b) -> b -> FreshVect l a neq -> b
foldl f x [] = x
foldl f x (y :: ys) = foldl f (x `f` y) ys

public export
foldr : (f : a -> b -> b) -> b -> FreshVect l a neq -> b
foldr f x [] = x
foldr f x (val :: vals) = (val `f` foldr f x vals)

namespace String
  public export
  (##) : BRel String
  s ## t = (s /= t)

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module Postfix

record Diag (a : Type) where
  fstt   : a
  sndd   : a
  equal : fstt === sndd

val : Diag a -> a
val diag = diag .fstt

prf : (d : Diag a) -> val d === d.sndd
prf = ?a

(.val') : Diag a -> a
diag .val' = diag .sndd

sym : (d : Diag a) -> d .fstt === d .val'
sym = ?b


text:
> module Functions
> %access public export

In this module we present types for basic proofs about functions between sets, such as

- injectivity, surjectivity, bijectivity
- quotienting by totality ("squashing")

> ||| The type of proofs that a given function is injective.
> ||| A function `f: t -> u` is injective if, given a proof that `f x = f y`,
> ||| we can prove `x=y`. An implementation of `Injective f` is a function that
> ||| returns an `(x = y)` proof given an `(f x = f y)` proof.
> Injective : {t,u:Type} -> (t -> u) -> Type
> Injective f {t} = (x,y:t) -> (f x = f y) -> (x = y)

> ||| The type of proofs that a given function is surjective.
> ||| A function `f: t -> u` is injective if, given any `y: u`, we can find
> ||| `x: t` with a proof `f x = y`. An implementation of `Surjective f` is a
> ||| function that returns a dependent pair `(x ** f x = y)`  given an
> ||| `(f x = f y)` proof. Note that there is no proof of uniqueness.
> Surjective : {t,u:Type} -> (t -> u) -> Type
> Surjective f {t} {u} = (y:u) -> (x:t ** f x = y)

> ||| The type of proofs that a given function is bijective.
> ||| Since this is equivalent to being both injective and surjective, that is
> ||| the definition we are using.
> Bijective : {t,u : Type} -> (t -> u) -> Type
> Bijective f {t} {u} = (Injective f, Surjective f)

> ||| The type of proofs that two types `t` and `u`, considered as simple sets
> ||| built by their constructible members, have the same cardinality. For our
> ||| purposes, this is equivalent to existential quantification on the type of
> ||| bijections between `t` and `u`.
> SameCardinality : Type -> Type -> Type
> SameCardinality t u = (f:(t->u) ** Bijective f)

Note that, for finite sets, the notion of `SameCardinality` collapses in the
obvious way; the problem of finding a bijection is equivalent to putting the
elements of the sets into two lists with the same length. We will formally prove
this later.

> ||| Proof that a type is a "mere proposition" (i.e. it only has one inhabitant
> ||| up to decidable equality.)
> Prop : (t:Type) -> Type
> Prop t = (p1:t) -> (p2:t) -> (p1=p2)

If P is a decidable proposition, we can quotient P by the totality equivalence
relation and get a "squashed" type. By "totality equivalence relation" we mean
a partition of the elements of $P : Type -> Type$ into two sets, one containing
constructible instances $P x$, the other containing unconstructible instances
$P y$. In NuPRL this is called "squash" so that is the name we will use here.

> squash : {p:Type} -> Dec p -> Type
> squash (Yes _) = Unit
> squash (No _) = Void

 Note that any two squashed values are trivially equal:

> ||| Any two squashed values of a given decidable proposition are equal.
> propSquash : {p: Type} -> (d : Dec p) -> Prop (squash d)
> propSquash (Yes prf) () () = Refl
> propSquash (No contra) v1 _ = absurd v1

> ||| Given a squashed proposition, obtain the original proposition.
> fromSquash : {p:Type} -> (d : Dec p) -> squash d -> p
> fromSquash (Yes prf) () = prf

Note that fromSquash can only ever accept a unit value since that is the only
value that is constructible.

> ||| Simple helper for projecting the first part of a dependent pair.
> proj1DP : (DPair a b) -> a
> proj1DP (x ** y) = x

> ||| Simple helper for projecting the second part of a dependent pair.
> proj2DP : (x : (DPair a b)) -> b (proj1DP x)
> proj2DP (x ** y) = y

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
module AOC.Solution

%default total

public export
record AOCSolution inputType where
  constructor MkAOCSolution
  day : Nat
  parser : String -> Maybe inputType
  part1 : inputType -> String
  part2 : inputType -> String

export
solutionToDP : {a : Type} -> (x : AOCSolution a) -> (inputType ** AOCSolution inputType)
solutionToDP {a} x = (a ** x)


text:
module Text.Markup.Edda.Process

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

import Text.Markup.Edda.Process.Inline
import Text.Markup.Edda.Process.Block

%default total
%access export

export
processDoc : EddaRaw DOC -> Edda DOC
processDoc (Doc title attrs body) = Doc (process title) attrs (process body)

export
processSnippet : EddaRaw SNIPPET -> Edda SNIPPET
processSnippet (Snippet content prf) with (prf)
  processSnippet (Snippet content prf) | IsInLine = Snippet (process content) prf
  processSnippet (Snippet content prf) | IsBlock = Snippet (process content) prf

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
import Data.Vect
import Data.Vect.Elem

oneInVector : Elem 1 [1,2,3]
oneInVector = Here

maryInVector : Elem "Mary" ["Peter", "Paul", "Mary"]
maryInVector = There (There Here)

fourNotInVector : Elem 4 [1,2,3] -> Void
fourNotInVector (There (There (There Here))) impossible
fourNotInVector (There (There (There (There _)))) impossible

peteNotInVector : Elem "Pete" ["John", "Paul", "George", "Ringo"] -> Void
peteNotInVector (There (There (There (There Here)))) impossible
peteNotInVector (There (There (There (There (There _))))) impossible


text:
module System

import public Data.So
import Data.String

import public System.Escape
import System.File

%default total

||| Shorthand for referring to the C support library
|||
||| @ fn the function name to refer to in the C support library
support : (fn : String) -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_support.h"

||| Shorthand for referring to libc 6
|||
||| @ fn the function name to refer to in libc 6
libc : (fn : String) -> String
libc fn = "C:" ++ fn ++ ", libc 6"

-- `sleep` and `usleep` need to be tied to `blodwen-[u]sleep` for threading
-- reasons (see support/racket/support.rkt)

%foreign "scheme,racket:blodwen-sleep"
         support "idris2_sleep"
prim__sleep : Int -> PrimIO ()

%foreign "scheme,racket:blodwen-usleep"
         support "idris2_usleep"
prim__usleep : Int -> PrimIO ()

||| Sleep for the specified number of seconds or, if signals are supported,
||| until an un-ignored signal arrives.
||| The exact wall-clock time slept might slighly differ depending on how busy
||| the system is and the resolution of the system's clock.
|||
||| @ sec the number of seconds to sleep for
export
sleep : HasIO io => (sec : Int) -> io ()
sleep sec = primIO (prim__sleep sec)

||| Sleep for the specified number of microseconds or, if signals are supported,
||| until an un-ignored signal arrives.
||| The exact wall-clock time slept might slighly differ depending on how busy
||| the system is and the resolution of the system's clock.
|||
||| @ usec the number of microseconds to sleep for
export
usleep : HasIO io => (usec : Int) -> So (usec >= 0) => io ()
usleep usec = primIO (prim__usleep usec)

-- Get the number of arguments
%foreign "scheme:blodwen-arg-count"
         support "idris2_getArgCount"
         "node:lambda:() => process.argv.length"
prim__getArgCount : PrimIO Int

-- Get argument number `n`
%foreign "scheme:blodwen-arg"
         support "idris2_getArg"
         "node:lambda:n => process.argv[n]"
prim__getArg : Int -> PrimIO String

||| Retrieve the arguments to the program call, if there were any.
export
getArgs : HasIO io => io (List String)
getArgs = do
            n <- primIO prim__getArgCount
            if n > 0
              then for [0..n-1] $ primIO . prim__getArg
              else pure []

%foreign libc "getenv"
         "node:lambda: n => process.env[n]"
prim__getEnv : String -> PrimIO (Ptr String)

%foreign support "idris2_getEnvPair"
prim__getEnvPair : Int -> PrimIO (Ptr String)
%foreign support "idris2_setenv"
prim__setEnv : String -> String -> Int -> PrimIO Int
%foreign support "idris2_unsetenv"
prim__unsetEnv : String -> PrimIO Int

||| Retrieve the specified environment variable's value string, or `Nothing` if
||| there is no such environment variable.
|||
||| @ var the name of the environment variable to look up
export
getEnv : HasIO io => (var : String) -> io (Maybe String)
getEnv var
   = do env <- primIO $ prim__getEnv var
        if prim__nullPtr env /= 0
           then pure Nothing
           else pure (Just (prim__getString env))

||| Retrieve all the key-value pairs of the environment variables, and return a
||| list containing them.
export
covering
getEnvironment : HasIO io => io (List (String, String))
getEnvironment = getAllPairs 0 []
  where
    splitEq : String -> (String, String)
    splitEq str
        = let (k, v)  = break (== '=') str
              (_, v') = break (/= '=') v in
              (k, v')

    getAllPairs : Int -> List String -> io (List (String, String))
    getAllPairs n acc = do
      envPair <- primIO $ prim__getEnvPair n
      if prim__nullPtr envPair /= 0
         then pure $ reverse $ map splitEq acc
         else getAllPairs (n + 1) (prim__getString envPair :: acc)

||| Add the specified variable with the given value string to the environment,
||| optionally overwriting any existing environment variable with the same name.
|||
||| @ var       the name of the environment variable to set
||| @ val       the value string to set the environment variable to
||| @ overwrite whether to overwrite the existing value if an environment
|||             variable with the specified name already exists
export
setEnv : HasIO io => (var : String) -> (val : String) -> (overwrite : Bool) ->
                     io Bool
setEnv var val overwrite
   = do ok <- primIO $ prim__setEnv var val (if overwrite then 1 else 0)
        pure $ ok == 0

||| Delete the specified environment variable. Returns `True` either if the
||| value was deleted or if the value was not defined/didn't exist. Returns
||| `False` if a system error occurred.
export
unsetEnv : HasIO io => (var : String) -> io Bool
unsetEnv var
   = do ok <- primIO $ prim__unsetEnv var
        pure $ ok == 0

%foreign "C:idris2_system, libidris2_support, idris_system.h"
prim__system : String -> PrimIO Int

||| Execute a shell command, returning its termination status or -1 if an error
||| occurred.
export
system : HasIO io => String -> io Int
system cmd = primIO (prim__system cmd)

namespace Escaped
  export
  system : HasIO io => List String -> io Int
  system = system . escapeCmd

||| Run a shell command, returning its stdout, and exit code.
export
covering
run : HasIO io => (cmd : String) -> io (String, Int)
run cmd = do
    Right f <- popen cmd Read
        | Left err => pure ("", 1)
    Right resp <- fRead f
        | Left err => pure ("", 1)
    exitCode <- pclose f
    pure (resp, exitCode)

namespace Escaped
  export
  covering
  run : HasIO io => (cmd : List String) -> io (String, Int)
  run = run . escapeCmd

%foreign support "idris2_time"
         "javascript:lambda:() => Math.floor(new Date().getTime() / 1000)"
prim__time : PrimIO Int

||| Return the number of seconds since epoch.
export
time : HasIO io => io Integer
time = pure $ cast !(primIO prim__time)

%foreign support "idris2_getPID"
prim__getPID : PrimIO Int

||| Get the ID of the currently running process.
export
getPID : HasIO io => io Int
getPID = primIO prim__getPID

%foreign libc "exit"
         "node:lambda:c => process.exit(c)"
prim__exit : Int -> PrimIO ()

||| Programs can either terminate successfully, or end in a caught
||| failure.
public export
data ExitCode : Type where
  ||| Terminate successfully.
  ExitSuccess : ExitCode
  ||| Program terminated for some prescribed reason.
  |||
  ||| @errNo A non-zero numerical value indicating failure.
  ||| @prf   Proof that the int value is non-zero.
  ExitFailure : (errNo    : Int) -> (So (not $ errNo == 0)) => ExitCode

||| Exit the program normally, with the specified status.
export
exitWith : HasIO io => ExitCode -> io a
exitWith ExitSuccess = primIO $ believe_me $ prim__exit 0
exitWith (ExitFailure code) = primIO $ believe_me $ prim__exit code

||| Exit the program with status value 1, indicating failure.
||| If you want to specify a custom status value, see `exitWith`.
export
exitFailure : HasIO io => io a
exitFailure = exitWith (ExitFailure 1)

||| Exit the program after a successful run.
export
exitSuccess : HasIO io => io a
exitSuccess = exitWith ExitSuccess


text:
module Main

import Dart.Core
import Dart.FFI

%inline
export
Point : Type
Point = Struct "Point,
// All foreign names must be fully qualified and
// the following import can always be assumed to exist:
// import 'dart:core' as $;
class Point {
  final $.int x;
  final $.int y;
  Point({this.x, this.y});
  Point.of(this.x, this.y);
}" [
  ("x", Int),
  ("y", Int)
]

Show Point where
  show pt = show (the Int (getField pt "x"), the Int (getField pt "y"))

namespace Point

  namespace New

    data Tag : Type where

    %inline
    public export
    x : Parameter Tag
    x = MkParameter "x" Int Tag

    %inline
    public export
    y : Parameter Tag
    y = MkParameter "y" Int Tag

  %inline
  public export
  new : Parameters [New.x, New.y] -> IO Point
  new ps = primIO $ prim__dart_new Point [] ps

%inline
export
Callbacks : Type
Callbacks = Struct "Callbacks,
class Callbacks {
  $.Object Function($.Object) x;
  $.Object Function($.Object) y;
  $.bool enabled;
  Callbacks({this.x, this.y, this.enabled});
  $.Object callX($.Object arg) => x(arg);
  $.Object callY($.Object arg) => y(arg);
}" [
  ("enabled", DartBool)
]

namespace Callbacks

  namespace New

    data Tag : Type where

    %inline
    public export
    x : Parameter Tag
    x = MkParameter "x" (Int -> Int) Tag

    %inline
    public export
    y : Parameter Tag
    y = MkParameter "y" (Int -> IO Int) Tag

    %inline
    public export
    enabled : Parameter Tag
    enabled = MkParameter "enabled" DartBool Tag

  %inline
  public export
  new : Parameters [Callbacks.New.x, Callbacks.New.y, Callbacks.New.enabled] -> IO Callbacks
  new ps = primIO $ prim__dart_new Callbacks [] ps

  export
  %foreign "Dart:.callX"
  callX : Callbacks -> Int -> Int

  export
  %foreign "Dart:.callY"
  callY : Callbacks -> Int -> PrimIO Int

||| A pure foreign function with a bool argument.
%foreign "Dart:ifBool,
$.Object ifBool($.bool condition, $.Object then, $.Object else_) {
  return condition ? then : else_;
}"
ifBool : DartBool -> Int -> Int -> Int

main : IO ()
main = do
  pt <- Point.new [
    x @= 42,
    y @= 37
  ]
  printLn pt

  cb <- Callbacks.new [
    x @= (\i => i * 2),
    y @= (\i => printLn i *> pure (i * 2)),
    enabled @= true
  ]
  printLn (callX cb 21)
  printLn !(primIO (callY cb 21))

  -- Dart bool
  printLn (the DartBool (cb `getField` "enabled"))
  printLn (ifBool true 1 2)
  printLn (ifBool false 1 2)
  pure ()


text:
||| Implementation of ordering relations for `Nat`ural numbers
module Data.Nat.Order

import Data.Nat
import Data.Fun
import Data.Rel
import Decidable.Decidable
import Decidable.Equality
import Decidable.Order

public export
total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->
                           LTE m n -> LTE n o ->
                           LTE m o
LTEIsTransitive Z n o                 LTEZero                  nlteo   = LTEZero
LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten)    (LTESucc nlteo)   = LTESucc (LTEIsTransitive m n o mlten nlteo)

public export
total LTEIsReflexive : (n : Nat) -> LTE n n
LTEIsReflexive Z      = LTEZero
LTEIsReflexive (S n)  = LTESucc (LTEIsReflexive n)

public export
implementation Preorder Nat LTE where
  transitive = LTEIsTransitive
  reflexive  = LTEIsReflexive

public export
total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->
                              LTE m n -> LTE n m -> m = n
LTEIsAntisymmetric Z Z         LTEZero LTEZero = Refl
LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)
   LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm)    | Refl = Refl

public export
implementation Poset Nat LTE where
  antisymmetric = LTEIsAntisymmetric

public export
total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void
zeroNeverGreater {n} LTEZero     impossible
zeroNeverGreater {n} (LTESucc _) impossible

public export
total zeroAlwaysSmaller : {n : Nat} -> LTE Z n
zeroAlwaysSmaller = LTEZero

public export
total ltesuccinjective : {0 n : Nat} -> {0 m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void
ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)
ltesuccinjective {n} {m} disprf LTEZero         impossible

public export
total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decideLTE    Z      y  = Yes LTEZero
decideLTE (S x)     Z  = No  zeroNeverGreater
decideLTE (S x)   (S y) with (decEq (S x) (S y))
  decideLTE (S x)   (S y) | Yes eq      = rewrite eq in Yes (reflexive (S y))
  decideLTE (S x)   (S y) | No _ with (decideLTE x y)
  decideLTE (S x)   (S y) | No _   | Yes nLTEm = Yes (LTESucc nLTEm)
  decideLTE (S x)   (S y) | No _   | No  nGTm  = No (ltesuccinjective nGTm)

public export
implementation Decidable [Nat,Nat] LTE where
  decide = decideLTE

public export
total
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

public export
total
shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
shift m n mLTEn = LTESucc mLTEn

public export
implementation Ordered Nat LTE where
  order Z      n = Left LTEZero
  order m      Z = Right LTEZero
  order (S k) (S j) with (order {to=LTE} k j)
    order (S k) (S j) | Left  prf = Left  (shift k j prf)
    order (S k) (S j) | Right prf = Right (shift j k prf)


text:
module Main

import System
import Control.Monad.State
import Data.SortedMap
import Data.SortedSet

import Data.Tree
import Deps.Data
import Deps.Lexer
import Deps.Parser

%default total

-- HELPER FUNCTIONS

filterMap : (a -> Maybe b) -> List a -> List b
filterMap pred xs =
  foldl
    (\acc, current => case pred current of
      Just result => result :: acc
      Nothing => acc)
    []
    xs

-- DIR/FILES

parseModule : String -> Namespace -> IO (Maybe IdrisHead)
parseModule rootDir ns = do
  let path = joinString "/" (rootDir :: ns) ++ ".idr"
  Right contents <- readFile path
    | pure Nothing
  pure (runParser contents program)

data ModuleCache
  = AlreadyParsed (Tree (IdrisHead, Bool))
  | Skipped

isAlreadyParsed : ModuleCache -> Bool
isAlreadyParsed (AlreadyParsed _) = True
isAlreadyParsed Skipped = False

data ParsedModule
  = Local IdrisHead
  | External

isLocalModule : ParsedModule -> Bool
isLocalModule (Local _) = True
isLocalModule External = False

partial
parseModulesHelper : String -> Namespace -> StateT (SortedMap Namespace ParsedModule) IO ()
parseModulesHelper rootDir ns' = do
  parsedModules <- get
  let Nothing = SortedMap.lookup ns' parsedModules
    | pure () -- Skip already parsed modules
  Just parsedModule <- lift (parseModule rootDir ns')
    | modify (insert ns' External)
  let localModule = Local (record { moduleNs = ns' } parsedModule)
  modify (insert ns' localModule)
  traverse (parseModulesHelper rootDir) (map ns (imports parsedModule))
  pure ()

partial
parseModules : String -> Namespace -> IO (SortedMap Namespace ParsedModule)
parseModules rootDir ns' = do
  (_, state) <- runStateT (parseModulesHelper rootDir ns') empty
  pure state

partial
buildTree : SortedMap Namespace ParsedModule -> Namespace -> State (SortedMap Namespace ModuleCache) (Tree (IdrisHead, Bool))
buildTree parsedModules ns' = do
  let externalNode = Node (MkIdrisHead ns' [], False) []
  trees <- get
  let Nothing = SortedMap.lookup ns' trees
    | Just (AlreadyParsed localNode) => pure localNode
    | Just Skipped => pure externalNode
  let Just (Local parsedIdrisHead) = SortedMap.lookup ns' parsedModules
    | do
      modify (insert ns' Skipped)
      pure externalNode
  subModules <- traverse (buildTree parsedModules) (map ns (imports parsedIdrisHead))
  let node = Node (record { moduleNs = ns' } parsedIdrisHead, True) subModules
  modify (insert ns' (AlreadyParsed node))
  pure node

partial
traverseModules : String -> Namespace -> IO (Tree (IdrisHead, Bool))
traverseModules rootDir ns' = do
  parsedModules <- parseModules rootDir ns'
  let (tree, _) = runState (buildTree parsedModules ns') empty
  pure tree

partial
getDependees : Namespace -> List IdrisHead -> List Namespace
getDependees usesNs idrisHeads =
  filterMap
    (\idrisHead => if usesNs `elem` map ns (imports idrisHead)
      then Just (moduleNs idrisHead)
      else Nothing)
    idrisHeads

partial
skipPreviousModules : Tree (IdrisHead, Bool) -> State (SortedSet Namespace) (Tree (IdrisHead, Bool))
skipPreviousModules (Node (idrisHead, isLocal) subForest) = do
  let currentNs = moduleNs idrisHead
  parsedModules <- get
  let False = SortedSet.contains currentNs parsedModules
    | pure (Node (record { imports = [] } idrisHead, isLocal) [])
  modify (SortedSet.insert currentNs)
  updatedSubForest <- traverse skipPreviousModules subForest
  pure (Node (idrisHead, isLocal) updatedSubForest)

-- UTILS

showLocal : Bool -> String
showLocal True = ""
showLocal False = " (Lib)"

moduleCacheToIsLocal : (Namespace, ModuleCache) -> (Namespace, Bool)
moduleCacheToIsLocal (ns', moduleCache) =
  (ns', isAlreadyParsed moduleCache)

parsedModuleToIsLocal : (Namespace, ParsedModule) -> (Namespace, Bool)
parsedModuleToIsLocal (ns', moduleCache) =
  (ns', isLocalModule moduleCache)

showModule : (Namespace, Bool) -> String
showModule (ns', isLocal) =
  showNamespace ns' ++ showLocal isLocal

parseNamespace : String -> Maybe Namespace
parseNamespace str =
  runParser str namespace_

-- CLI

data ListOption
  = ListAll
  | ListLocal
  | ListExternal

partial
listModules : String -> Namespace -> ListOption -> IO ()
listModules rootDir mainNs listOption = do
  modules <- parseModules rootDir mainNs
  let allNs = SortedMap.toList modules
  let (local, external) = partition (isLocalModule . snd) allNs
  let nsOutput =
    case listOption of
      ListAll => map (showModule . parsedModuleToIsLocal) allNs
      ListLocal => map (showNamespace . fst) local
      ListExternal => map (showNamespace . fst) external
  putStr (unlines nsOutput)

partial
depTree : String -> Namespace -> IO ()
depTree rootDir mainNs = do
    tree <- traverseModules rootDir mainNs
    let (treeSkippingModules, _) = runState (skipPreviousModules tree) empty
    let moduleNames = map showModuleFromIdrisHead treeSkippingModules
    putStr $ drawTree moduleNames
  where
      showModuleFromIdrisHead : (IdrisHead, Bool) -> String
      showModuleFromIdrisHead (idrisHead, isLocal) =
        showModule (moduleNs idrisHead, isLocal)

partial
usesDep : String -> Namespace -> Namespace -> IO ()
usesDep rootDir mainNs usesNs = do
  parsedModules <- parseModules rootDir mainNs
  let usedInNs = getDependees usesNs (localModules parsedModules)
  putStr $ unlines $ map showNamespace usedInNs
where
  localModules : SortedMap Namespace ParsedModule -> List IdrisHead
  localModules parsedModules =
    filterMap
      (\parsedModule => case parsedModule of
        Local idrisHead => Just idrisHead
        External => Nothing)
      (values parsedModules)

printUsage : IO ()
printUsage =
  putStrLn "Usage: deps <rootDir> <mainModule> [--list-all | --list-local | --list-external | --tree | --uses <module>]"

printInvalidNamespace : IO ()
printInvalidNamespace =
  putStrLn "Invalid namespace"

partial
main : IO ()
main = do
  (_ :: rootDir :: mainModule :: restArgs) <- getArgs
    | printUsage
  let Just mainNs = parseNamespace mainModule
    | printInvalidNamespace
  case restArgs of
    ["--list-all"] =>
      listModules rootDir mainNs ListAll

    ["--list-local"] =>
      listModules rootDir mainNs ListLocal

    ["--list-external"] =>
      listModules rootDir mainNs ListExternal

    ["--tree"] =>
      depTree rootDir mainNs

    ["--uses", usesModule] =>
      let Just usesNs = parseNamespace usesModule
        | printInvalidNamespace
      in usesDep rootDir mainNs usesNs

    _ =>
      printUsage

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Dummy

something : String
something = "Something something"

data Proxy : Type -> Type where
  MkProxy : Proxy a


text:
dupLinear : (1 x : a) -> (a, a)
dupLinear x = dup (let var = 22 in x)


text:
module Test.Inigo.Archive.ArchiveTest

import IdrTest.Test
import IdrTest.Expectation

import Inigo.Archive.Archive

export
suite : Test
suite =
  describe "Encode" [
    test "Simple Encode" (\_ => assertEq
      (encode [(["a","b"], "bbb"), (["a","c"], "ccc")])
      "a.b=\"bbb\"\na.c=\"ccc\""
    ),
    test "Simple Decode" (\_ => assertEq
      (decode "a.b=\"bbb\"\na.c=\"ccc\"")
      (Just [(["a","b"], "bbb"), (["a","c"], "ccc")])
    )
  ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module SimpleData
{-
import public Data.HVect
import public Data.Vect
import public Js.ASync
import public Js.Json

public export
data Label : String -> Type -> Type where
  MkLabel : (s : String) -> a -> Label s a

infixr 2 |=

export
(|=) : (s : String) -> a -> Label s a
(|=) x y = MkLabel x y

public export
data Alt : Vect n Type -> Type where
  MkAlt : (Elem t ts) -> t -> Alt ts

public export
AltExpand: Alt xs -> Alt (x::xs)
AltExpand (MkAlt p x) = MkAlt (There p) x

public export
data SDataTy : Type where
  SString : SDataTy
  SUnit : SDataTy
  SList : SDataTy -> SDataTy
  STuple : SDataTy -> SDataTy -> SDataTy
  SObj : Vect k (String, SDataTy) -> SDataTy
  SAlt : Vect k (String, SDataTy) -> SDataTy
  SEither : SDataTy -> SDataTy -> SDataTy
  SMaybe : SDataTy -> SDataTy
  SJson : SDataTy

export
ToJson SDataTy where
  toJson SString = JsonArray [JsonString "SString"]
  toJson SUnit = JsonArray [JsonString "SUnit"]
  toJson (SList x) = JsonArray [JsonString "SList", toJson x]
  toJson (STuple x y) = JsonArray [JsonString "STuple", toJson x, toJson y]
  toJson (SObj x) = JsonArray [JsonString "SObj", toJson x]
  toJson (SAlt x) = JsonArray [JsonString "SAlt", toJson x]
  toJson (SEither x y) = JsonArray [JsonString "SEither", toJson x, toJson y]
  toJson (SMaybe x) = JsonArray [JsonString "SMaybe", toJson x]
  toJson SJson = JsonArray [JsonString "SJson"]

export
FromJson SDataTy where
  fromJson (JsonArray [JsonString "SString"]) = Right SString
  fromJson (JsonArray [JsonString "SUnit"]) = Right SUnit
  fromJson (JsonArray [JsonString "SList", x]) = SList <$> fromJson x
  fromJson (JsonArray [JsonString "STuple", x, y]) = STuple <$> fromJson x <*> fromJson y
  fromJson (JsonArray [JsonString "SObj", JsonArray x]) =
    SObj <$> the (Either String (Vect (length x) (String, SDataTy))) (fromJson $ JsonArray x)
  fromJson (JsonArray [JsonString "SAlt", JsonArray x]) =
    SAlt <$> the (Either String (Vect (length x) (String, SDataTy))) (fromJson $ JsonArray x)
  fromJson (JsonArray [JsonString "SEither", x, y]) = SEither <$> fromJson x <*> fromJson y
  fromJson (JsonArray [JsonString "SMaybe", x]) = SMaybe <$> fromJson x
  fromJson (JsonArray [JsonString "SJson"]) = Right SJson

public export
SDataObj : {n:Nat} -> Type
SDataObj {n} = Vect n (String, SDataTy)

mutual
  public export total
  SObjTy : Vect k (String, SDataTy) -> Vect k Type
  SObjTy [] = []
  SObjTy ((s, x)::xs) = assert_total $ Label s (ISDataTy x) :: SObjTy xs

  public export  total
  SAltTy : Vect k (String, SDataTy) -> Vect k Type
  SAltTy [] = []
  SAltTy ((s, x)::xs) = assert_total $ Label s (ISDataTy x) :: SAltTy xs

  public export total
  ISDataTy : SDataTy -> Type
  ISDataTy SString = String
  ISDataTy SUnit = ()
  ISDataTy (SList x) = List (ISDataTy x)
  ISDataTy (STuple x y) = (ISDataTy x, ISDataTy y)
  ISDataTy (SObj x) = HVect (SObjTy x)
  ISDataTy (SAlt x) = Alt (SAltTy x)
  ISDataTy (SEither x y) = Either (ISDataTy x) (ISDataTy y)
  ISDataTy (SMaybe x) = Maybe (ISDataTy x)
  ISDataTy SJson = JsonValue

public export total
ISDataObj : SDataObj -> Type
ISDataObj x = ISDataTy $ SObj x

mutual
  export
  jsonValueToJS : JsonValue -> JS_IO Ptr
  jsonValueToJS (JsonString s) = pure $ believe_me s
  jsonValueToJS (JsonNumber d) = pure $ believe_me d
  jsonValueToJS (JsonBool True) = jscall "true" (() -> JS_IO Ptr) ()
  jsonValueToJS (JsonBool False) = jscall "false" (() -> JS_IO Ptr) ()
  jsonValueToJS JsonNull = jscall "null" (() -> JS_IO Ptr) ()
  jsonValueToJS (JsonArray []) =
    jscall "[]" (() -> JS_IO Ptr) ()
  jsonValueToJS (JsonArray (x::xs)) =
    do
      ys <- jsonValueToJS $ JsonArray xs
      y <- jsonValueToJS x
      jscall "%1.unshift(%0)" (Ptr -> Ptr -> JS_IO Ptr) y ys
      pure ys
  jsonValueToJS (JsonObject x) = jsonObjToJS $ toList x

  jsonObjToJS : List (String, JsonValue) -> JS_IO Ptr
  jsonObjToJS [] =
    jscall "{}" (() -> JS_IO Ptr) ()
  jsonObjToJS ((s,x)::xs) =
    do
      ys <- jsonObjToJS xs
      y <- jsonValueToJS x
      jscall "%2[%0]=%1" (String -> Ptr -> Ptr -> JS_IO Ptr) s y ys
      pure ys

export
encodeJS : (a:SDataTy) -> ISDataTy a -> JS_IO Ptr
encodeJS SString s = pure $ believe_me s
encodeJS SUnit () = jscall "null" (() -> JS_IO Ptr) ()
--encodeJS (SList _) [] = jscall "[]" (() -> JS_IO Ptr) ()
encodeJS (SList x) xs =
  do
    lstPtr <- sequence $ map (encodeJS x) xs
    makeJSList lstPtr
    --z <- encodeJS x t
    --w <- encodeJS (SList x) r
    --jscall "%1.unshift(%0)" (Ptr -> Ptr -> JS_IO ()) z w
    --pure w
encodeJS (STuple x y) (z, w) =
  jscall "[%0,%1]" (Ptr -> Ptr -> JS_IO Ptr) !(encodeJS x z) !(encodeJS y w)
encodeJS (SObj []) [] =
  jscall "{}" (() -> JS_IO Ptr) ()
encodeJS (SObj ((s,x) :: xs)) (MkLabel s v :: r) =
  do
   o <- encodeJS (SObj xs) r
   vv <- encodeJS x v
   jscall "%2[%0]=%1" (String -> Ptr -> Ptr -> JS_IO ()) s vv o
   pure o
--encodeJS (SAlt)
--encodeJS (SEither)
--encodeJS (SMaybe)
encodeJS SJson v = jsonValueToJS v

typeof : Ptr -> JS_IO String
typeof x = jscall "typeof %0" (Ptr -> JS_IO String) x

export
decodeJS : (a:SDataTy) -> Ptr -> JS_IO (Either String (ISDataTy a))
decodeJS SString p =
  do
    t <- typeof p
    if t == "string" then
      pure $ Right $ believe_me p
      else pure $ Left "decodeJS: Not a String"
decodeJS SUnit p =
  do
    isnull <- jscall "(%0 == null)+0" (Ptr -> JS_IO Int) p
    if isnull == 1 then pure $ Right ()
      else pure $ Left "decodeJS: Not null"
decodeJS (SList x) p =
  do
    isArray <- jscall "(Array.isArray(%0))+0" (Ptr -> JS_IO Int) p
    if isArray == 1 then
      do
        len <- jscall "%0.length" (Ptr -> JS_IO Int) p
        if len >0 then
          do
            pfirst <- jscall "%0[0]" (Ptr -> JS_IO Ptr) p
            prest <- jscall "%0.slice(1)" (Ptr -> JS_IO Ptr) p
            first <- decodeJS x pfirst
            rest <- decodeJS (SList x) prest
            pure $ (::) <$> first <*> rest
          else pure $ Right []
      else pure $ Left "decodeJS: Not an Array"
decodeJS (STuple x y) p =
  do
    isArray2 <- jscall "(Array.isArray(%0) && %0.length == 2)+0" (Ptr -> JS_IO Int) p
    if isArray2 == 1 then
      do
        px <- jscall "%0[0]" (Ptr -> JS_IO Ptr) p
        py <- jscall "%0[1]" (Ptr -> JS_IO Ptr) p
        xv <- decodeJS x px
        yv <- decodeJS y py
        pure $ MkPair <$> xv <*> yv
      else pure $ Left "decodeJS: Not a tuple"
decodeJS (SObj []) p = pure $ Right []
decodeJS (SObj ((s,v)::r)) p =
  do
    hasKey <- jscall "(%0 in %1)+0" (String -> Ptr -> JS_IO Int) s p
    if hasKey == 1 then
      do
        pv <- jscall "%0[%1]" (Ptr -> String -> JS_IO Ptr) p s
        vv <- decodeJS v pv
        rv <- decodeJS (SObj r) p
        pure $ (::) <$> (MkLabel s <$> vv) <*> rv
      else pure $ Left $ "decodeJS: missing key" ++ s

mutual

  encodeObjJson : (v: Vect n (String, SDataTy)) -> HVect (SObjTy v) -> SortedMap String JsonValue
  encodeObjJson [] [] = empty
  encodeObjJson ((s,x) :: xs) (MkLabel s v :: r) = insert s (encodeJson x v) $ encodeObjJson xs r

  export
  encodeJson : (a:SDataTy) -> ISDataTy a -> JsonValue
  encodeJson SString s = JsonString s
  encodeJson SUnit () = JsonNull
  encodeJson (SList x) l = JsonArray $ map (encodeJson x) l
  encodeJson (STuple x y) (z, w) = JsonArray [encodeJson x z, encodeJson y w]
  encodeJson (SObj x) y = JsonObject $ encodeObjJson x y
  encodeJson SJson x = x
-}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Main
-- Run a single test
-- > make test only=test013
import Cairo

example : Felt -> Cairo Felt
example n = dict 0 (\d =>
  let d1 = dwrite d 1 2
      d2 = dwrite d1 2 n
      d3 = dwrite d2 3 4
  in dread d3 2)

{-
Error: While processing right hand side of non_example. Trying to use linear name inner in non-linear context.

non_example : Felt -> Felt
non_example n =
  dict 0 (\outer =>
    let inner' = dict 1 (\inner => (outer, inner))
     in (inner', n)
  )
-}

pureDictComp : (1 d : LinDict) -> (LinDict, Felt)
pureDictComp d =
  let d1 = dwrite d 1 2
      d2 = dwrite d1 2 3
      d3 = dwrite d2 3 4
  in dread d3 5

%noinline
main : Cairo ()
main = do
    result1 <- example 42
    output result1
    result2 <- dict 8 pureDictComp
    output result2 -- returns default 8
    -- output $ non_example 42

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Deriving.Utils

import Language.Reflection.Utils

%access export

showFQN : TTName -> String
showFQN (UN n) = n
showFQN (MN i s) = "{" ++ s ++ "_" ++ (show i) ++ "}"
showFQN (NS tn ns) = (concat $ intersperse "." ns) ++ "." ++ (showFQN tn)
-- showFQN (SN _) = "unsuported"

namespace CtorArg
  getFunArg : CtorArg -> FunArg
  getFunArg (CtorParameter funArg) = funArg
  getFunArg (CtorField funArg)     = funArg

namespace TyConArg
  getFunArg : TyConArg -> FunArg
  getFunArg (TyConParameter x) = x
  getFunArg (TyConIndex x) = x

makeTypeParametersFrom : TTName -> List FunArg -> Elab (List FunArg)
makeTypeParametersFrom ifc tyconArgs = do
  let typeParameter = map (record {plicity = Implicit}) tyconArgs
  instanceParameter <- sequence $ map makeInstanceParameter (reverse tyconArgs)
  pure $ typeParameter ++ instanceParameter
where
  makeInstanceParameter : FunArg -> Elab FunArg
  makeInstanceParameter arg = do
    inst <- gensym "inst"
    pure $ MkFunArg inst (RApp (Var ifc) (Var (name arg))) Constraint NotErased

makeTypeParameters : TTName -> Datatype -> Elab (List FunArg)
makeTypeParameters ifc dt = do
  let tyconArgs = map getFunArg $ tyConArgs dt
  makeTypeParametersFrom ifc (reverse tyconArgs)

wrapWithParameters : Raw -> (List FunArg) -> Raw
wrapWithParameters  body args =
  foldl (\acc,arg => RApp acc (Var (name arg))) body args

wrapWithPatBind : Raw -> (List FunArg) -> Raw
wrapWithPatBind body args =
  foldr (\arg,acc => RBind (name arg) (PVar $ type arg) acc) body args

||| query the instance of the interface to idris
lookupInstanceFor : TTName -> TTName -> Raw -> Elab Raw
lookupInstanceFor fname ifc ty = do
    (inst, _) <- runElab (RApp (Var ifc) ty) $ do
      resolveTC fname
    -- TT -> Raw
    let Just inst = forget inst
    pure inst

||| find an instance of the interface in listed arguments
findInstanceFor : Maybe Nat -> List FunArg -> Datatype-> Maybe TTName
findInstanceFor Nothing  _        dt = Nothing
findInstanceFor (Just i) tyParams dt =
  let pad = length $ tyConArgs dt in
  map name $ index' (minus (2 * pad)  (1 + i)) tyParams

lookupCtorExact : TTName -> Elab TTName
lookupCtorExact ifc = do
  ifcData <- lookupDatatypeExact ifc
  let [(ctor, _, _)] = constructors ifcData
  pure ctor

resultType : Datatype -> Raw
resultType (MkDatatype name tyConArgs tyConRes constructors) = wrapWithParameters (Var name) (map getFunArg tyConArgs)

argsOfTyConArgs : List FunArg -> Datatype -> List FunArg
argsOfTyConArgs args dt =
  let pad = length $ tyConArgs dt in
  take pad args

argsExceptTyConArgs : List FunArg -> Datatype -> List FunArg
argsExceptTyConArgs args dt =
  let pad = length $ tyConArgs dt in
  drop pad args

rename : FunArg -> Elab FunArg
rename arg = do
  x <- gensym "arg"
  pure $ record {name = x} arg

-- TOOD: care about depedent products
renameAll : List FunArg -> Elab (List FunArg)
renameAll args = sequence $ map rename args

max_stars_repo_name: KeenS/idris-deriving

max_issues_repo_name: KeenS/idris-deriving

max_forks_repo_name: KeenS/idris-deriving


text:
module Tests.Deriving

import Test.Unit
import Test.Unit.Assertions
import Deriving
import System

%language ElabReflection

data Janken = Gu | Choki | Pa

%runElab derive [Show, Eq] `{{Janken}}

data StringMaybe = Some String | None

data Result a b = Ok a | Err b

%runElab do
  derive [Show, Eq] `{{StringMaybe}}
  derive [Show, Eq] `{{Result}}

exitIfFail : IO (List Bool) -> IO ()
exitIfFail action = do
  results <- action
  if not (all id results)
  then do
    putStrLn "Some tests failed"
    exit 1
  else pure ()

testShowJanken : IO ()
testShowJanken = exitIfFail $ runTests
  [assertEquals (show Gu) "Gu"
  , assertEquals (show Choki) "Choki"
  , assertEquals (show Pa) "Pa"
  ]

testEqJanken : IO ()
testEqJanken = exitIfFail $ runTests
  [ assertTrue  $ Gu    == Gu
  , assertTrue  $ Choki == Choki
  , assertTrue  $ Pa    == Pa
  , assertFalse $ Gu    == Choki
  , assertFalse $ Choki == Gu
  , assertFalse $ Choki == Pa
  , assertFalse $ Pa    == Choki
  , assertFalse $ Pa    == Gu
  , assertFalse $ Gu    == Pa
  , assertFalse $ Gu    /= Gu
  , assertFalse $ Choki /= Choki
  , assertFalse $ Pa    /= Pa
  , assertTrue  $ Gu    /= Choki
  , assertTrue  $ Choki /= Gu
  , assertTrue  $ Choki /= Pa
  , assertTrue  $ Pa    /= Choki
  , assertTrue  $ Pa    /= Gu
  , assertTrue  $ Gu    /= Pa
  ]

testShowStringMaybe : IO ()
testShowStringMaybe = exitIfFail $ runTests
  [ assertEquals (show $ Some "foo") "Some \"foo\""
  , assertEquals (show None) "None"
  ]

testEqStringMaybe : IO ()
testEqStringMaybe = exitIfFail $ runTests
  [ assertTrue  $ (Some "foo") == (Some "foo")
  , assertFalse $ (Some "foo") == (Some "bar")
  , assertTrue  $ None         == None
  , assertFalse $ (Some "foo") == None
  , assertFalse $ None         == (Some "foo")
  , assertFalse $ (Some "foo") /= (Some "foo")
  , assertTrue  $ (Some "foo") /= (Some "bar")
  , assertFalse $ None         /= None
  , assertTrue  $ (Some "foo") /= None
  , assertTrue  $ None         /= (Some "foo")
  ]

testShowResult : IO ()
testShowResult =
  let t = the (Result String Int) in
  exitIfFail $ runTests
  [ assertEquals (show $ t (Ok "foo")) "Ok \"foo\""
  , assertEquals (show $ t (Err 1))  "Err 1"
  ]

testEqResult : IO ()
testEqResult =
  let t = the (Result String Int) in
  exitIfFail $ runTests
  [ assertTrue  $ t (Ok "foo") == (Ok "foo")
  , assertFalse $ t (Ok "foo") == (Ok "bar")
  , assertTrue  $ t (Err 0)    == (Err 0)
  , assertFalse $ t (Err 0)    == (Err 1)
  , assertFalse $ t (Ok "foo") == (Err 0)
  , assertFalse $ t (Err 0)    == (Ok "foo")
  , assertFalse $ t (Ok "foo") /= (Ok "foo")
  , assertTrue  $ t (Ok "foo") /= (Ok "bar")
  , assertFalse $ t (Err 0)    /= (Err 0)
  , assertTrue  $ t (Err 0)    /= (Err 1)
  , assertTrue  $ t (Ok "foo") /= (Err 1)
  , assertTrue  $ t (Err 0)    /= (Ok "foo")
  ]

export
test : IO ()
test = do
  testShowJanken
  testShowStringMaybe
  testShowResult
  testEqJanken
  testEqStringMaybe
  testEqResult


text:
-- | Tainted Monad Transformer
module Control.Monad.Trans.Tainted

import Data.Tainted

-- | 'TaintedT' is a monad transformer of 'Tainted'
data TaintedT : (Type -> Type) -> Type where
  mkTaintedT : {m : Monad} -> m (Tainted a) -> TaintedT m a

-- | Lift a 'Tainted' into an 'TaintedT'
--hoistTainted : Monad m => Tainted a -> TaintedT m a
--hoistTainted = mkTaintedT . return

max_stars_repo_name: RossMeikleham/Idris-Tainted

max_issues_repo_name: RossMeikleham/Idris-Tainted

max_forks_repo_name: RossMeikleham/Idris-Tainted


text:
module Data.String.Utils

import Data.List

indentSize : Nat
indentSize = 4

export
parens : String -> String
parens b = "(" ++ b ++ ")"

export
bracket : String -> String
bracket b = "[" ++ b ++ "]"

export
indent : Nat -> String -> String
indent n b = fastConcat (replicate (n * indentSize) " ") ++ b

export
function : Show fun => Show arg => fun -> List arg -> String
function f args = show f ++ fastConcat ((\arg => " " ++ show arg) <$> args)

export
nlSep : Show a => List a -> String
nlSep xs = fastConcat $ (\x => show x ++ "\n\n") <$> xs


text:
badmap : List Int -> List Int
badmap = map (\0 x => 2)


text:
module Ref

import Toolkit.Data.Location

public export
record Ref where
  constructor MkRef
  span : FileContext
  get  : String

export
setSource : String -> Ref -> Ref
setSource new ref = record {span $= setSource new} ref

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits