text:
import Data.List

interface Foo a where
  covering
  foo : a -> ()

Foo (Maybe String) where
  foo Nothing = ()
  foo (Just x) = ()

Foo (Maybe Int) where
  foo Nothing = ()


text:
not : (arg1 : Bool) -> {default arg2 True : Bool}
not = ?a

ext: idr


text:
module Incrementer

import public Numeric

%default total

||| Increment integer
public export
incrementer : Integer -> Integer
incrementer = (+1)

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module With

import Data.Vect

filter' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter' f [] = (_ ** [])
filter' f (x :: xs) =
  let (_ ** xs') = filter' f xs
  in if f x
    then (_ ** x :: xs')
    else (_ ** xs')

filter'' : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter'' f [] = (_ ** [])
filter'' f (x :: xs) with (filter'' f xs)
  | (_ ** xs') = if f x then (_ ** x :: xs') else (_ ** xs')

-- similar to view pattern in haskell?
-- https://ghc.haskell.org/trac/ghc/wiki/ViewPatterns#Basicviewpatterns

data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd  : Parity (S (n + n))

parity : (n : Nat) -> Parity n
parity Z = Even {n = Z}
parity (S Z) = Odd {n = Z}
parity (S (S k)) = ?incomplete
-- parity (S (S k)) with (parity k)
--   parity (S (S (j + j)))     | Even = Even { n = S j }
--   parity (S (S (S (j + j)))) | Odd  = Odd  { n = S j }
  -- don't know how to go futher, the error message shows it cannot prove:
  --  (S j) + (S j) ~ S (S (j + j))

-- `with' syntax can be used to further decompose (pattern matchin) on the
-- parameter with respect to the result of an expression

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
  natToBin (j + j)    | Even = False :: natToBin j
  natToBin (S (j + j))| Odd  = True  :: natToBin j

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps


text:
module Main

import Test.Golden

%default covering

allTests : TestPool
allTests = MkTestPool "Name of the pool" [] Nothing
  [ "test001"
  , "test002"
  ]

main : IO ()
main = runner
  [ testPaths "inigo" allTests
  ] where
    testPaths : String -> TestPool -> TestPool
    testPaths dir = record { testCases $= map ((dir ++ "/") ++) }

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module IdrisJvm.Files

import Java.Nio
import IdrisJvm.IO

%access public export

JDirectory : Type
JDirectory = JVM_Native (Class "io/github/mmhelloworld/idrisjvm/io/Directory")

namespace Files
  FilesClass : JVM_NativeTy
  FilesClass = Class "io/github/mmhelloworld/idrisjvm/io/Files"

  Files : Type
  Files = JVM_Native FilesClass

  readFile : String -> JVM_IO (Either Throwable String)
  readFile = invokeStatic FilesClass "readFile" (String -> JVM_IO (Either Throwable String))

  writeFile : String -> String -> JVM_IO (Either Throwable ())
  writeFile = invokeStatic FilesClass "writeFile" (String -> String -> JVM_IO (Either Throwable ()))

  createDirectory : String -> JVM_IO (Either Throwable ())
  createDirectory = invokeStatic FilesClass "createDirectory" (String -> JVM_IO (Either Throwable ()))

  createDirectories : Path -> JVM_IO (Either Throwable ())
  createDirectories = invokeStatic FilesClass "createDirectories" (Path -> JVM_IO (Either Throwable ()))

  changeDir : String -> JVM_IO Bool
  changeDir = invokeStatic FilesClass "changeDir" (String -> JVM_IO Bool)

  getTemporaryFileName : JVM_IO String
  getTemporaryFileName = invokeStatic FilesClass "getTemporaryFileName" (JVM_IO String)

  chmod : String -> Int -> JVM_IO ()
  chmod = invokeStatic FilesClass "chmod" (String -> Int -> JVM_IO ())

  getWorkingDir : JVM_IO String
  getWorkingDir = invokeStatic FilesClass "getWorkingDir" (JVM_IO String)

  createPath : String -> JVM_IO Path
  createPath = invokeStatic FilesClass "createPath" (String -> JVM_IO Path)

  deleteIfExists : Path -> JVM_IO Bool
  deleteIfExists = invokeStatic FilesClass "deleteIfExists" (Path -> JVM_IO Bool)

  openDirectory : String -> JVM_IO (Either Throwable JDirectory)
  openDirectory = invokeStatic FilesClass "openDirectory" (String -> JVM_IO (Either Throwable JDirectory))

  closeDirectory : JDirectory -> JVM_IO ()
  closeDirectory = invokeStatic FilesClass "closeDirectory" (JDirectory -> JVM_IO ())

  nextDirectoryEntry : JDirectory -> JVM_IO (Either Throwable String)
  nextDirectoryEntry = invokeStatic FilesClass "getNextDirectoryEntry" (JDirectory -> JVM_IO (Either Throwable String))


text:
module SkepticLang.IOUtils

%access public export

||| Loads lines from a text file.
|||
||| @path   the path to the file
loadLines : (path : String) -> IO (Maybe (List String))
loadLines path = do
  txt <- readFile path
  case txt of
    Right txt' => pure (Just (lines txt'))
    _ => pure Nothing

||| Joins a list of strings with the specified delimiter.
|||
||| @delim  the delimiter
||| @strs   the list of strings
unsplit : (delim : String) -> (strs : List String) -> String
unsplit _ [] = ""
unsplit delim (str :: strs') = str ++ delim ++ unsplit delim strs'

||| Gets the directory portion of a given file path.
|||
||| @path the file path
dirName : (path : String) -> String
dirName path =
  case split (== '/') path of -- Split path.
    (x :: xs) => unsplit "/" (init (x :: xs))
    _ => ""

||| Checks if a path is terminated with a slash.
|||
||| @path the path to check
isSlashTerminated : (path : String) -> Bool
isSlashTerminated path = last' (unpack path) == Just '/'

||| Joins two paths together.
|||
||| @x the base path
||| @y the path to append
joinPaths : (x : String) -> (y : String) -> String
joinPaths x y = x ++ (if isSlashTerminated x then "" else "/") ++ y

||| Returns true if the given path is absolute.
|||
||| @path the path to check
isAbsPath : (path : String) -> Bool
isAbsPath path = head' (unpack path) == Just '/'

||| Converts a relative path to an absolute path.
|||
||| @base the base directory
||| @rel  the relative path to convert
toAbsPath : (base : String) -> (rel : String) -> String
toAbsPath base rel =
  if isAbsPath rel then
    rel
  else
    joinPaths base rel

||| Resolves an absolute path from a relative path.
|||
||| @rel  the relative path to convert
resolveAbsPath : (rel : String) -> IO String
resolveAbsPath rel = do
  base <- currentDir
  pure (toAbsPath base rel)

max_stars_repo_name: sr-lab/skeptic-lang

max_issues_repo_name: sr-lab/skeptic-lang

max_forks_repo_name: sr-lab/skeptic-lang


text:
module Replica.Help

import Data.List
import Data.List1
import Data.String
import Replica.Other.String

%default total

public export
record Help where
  constructor MkHelp
  name : String
  usage : Maybe String
  description : String
  chapter : List (String, List1 Help)
  lastWords : Maybe String

padRightTo : Nat -> String -> String
padRightTo k x = x ++ pack (replicate (minus k (length x)) ' ')

entrySynopsis : Nat -> Help -> List String
entrySynopsis k x =
  let (y:::ys) = lines x.description
  in "\{padRightTo k x.name}  \{y}" :: map (pack (replicate (2 + k) ' ') ++) ys

chapterSynopsis : Nat -> String -> List1 Help -> String
chapterSynopsis k x xs = unlines $
  "\{x}:" :: map (withOffset 2) (forget xs >>= entrySynopsis k)

export
display : Help -> String
display h = unlines $ "" :: intersperse "" (
  maybe id (\u => ("Usage: \{u}" ::)) h.usage $
  h.description ::
  map (uncurry $ chapterSynopsis maxLengthName) h.chapter
  ++ (maybe [] (\l => [l]) h.lastWords))
  where
    maxLengthName : Nat
    maxLengthName = foldl (\x, h => max x (length h.name)) 0 (h.chapter >>= forget . snd)

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Control.Algebra

infixl 6 <->
infixl 7 <.>

||| Sets equipped with a single binary operation that is associative, along with
||| a neutral element for that binary operation and inverses for all elements.
||| Must satisfy the following laws:
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
class Monoid a => Group a where
  inverse : a -> a

(<->) : Group a => a -> a -> a
(<->) left right = left <+> (inverse right)

||| Sets equipped with a single binary operation that is associative and
||| commutative, along with a neutral element for that binary operation and
||| inverses for all elements. Must satisfy the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
class Group a => AbelianGroup a where { }

||| Sets equipped with two binary operations, one associative and commutative
||| supplied with a neutral element, and the other associative, with
||| distributivity laws relating the two operations.  Must satisfy the following
||| laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class AbelianGroup a => Ring a where
  (<.>) : a -> a -> a

||| Sets equipped with two binary operations, one associative and commutative
||| supplied with a neutral element, and the other associative supplied with a
||| neutral element, with distributivity laws relating the two operations.  Must
||| satisfy the following laws:
|||
||| +  Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Neutral for `<.>`:
|||     forall a,     a <.> unity     == a
|||     forall a,     unity <.> a     == a
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class Ring a => RingWithUnity a where
  unity : a

||| Sets equipped with two binary operations – both associative, commutative and
||| possessing a neutral element – and distributivity laws relating the two
||| operations. All elements except the additive identity must have a
||| multiplicative inverse. Must satisfy the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Commutativity of `<+>`:
|||     forall a b,   a <+> b         == b <+> a
||| + Neutral for `<+>`:
|||     forall a,     a <+> neutral   == a
|||     forall a,     neutral <+> a   == a
||| + Inverse for `<+>`:
|||     forall a,     a <+> inverse a == neutral
|||     forall a,     inverse a <+> a == neutral
||| + Associativity of `<.>`:
|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
||| + Unity for `<.>`:
|||     forall a,     a <.> unity     == a
|||     forall a,     unity <.> a     == a
||| + InverseM of `<.>`, except for neutral
|||     forall a /= neutral,  a <.> inverseM a == unity
|||     forall a /= neutral,  inverseM a <.> a == unity
||| + Distributivity of `<.>` and `<+>`:
|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
class RingWithUnity a => Field a where
  inverseM : (x : a) -> Not (x = Algebra.neutral) -> a

sum' : (Foldable t, Monoid a) => t a -> a
sum' = concat

product' : (Foldable t, RingWithUnity a) => t a -> a
product' = foldr (<.>) unity

pow' : RingWithUnity a => a -> Nat -> a
pow' _ Z     = unity
pow' x (S n) = x <.> pow' x n

-- XXX todo:
--   Structures where "abs" make sense.
--   Euclidean domains, etc.
--   Where to put fromInteger and fromRational?

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module ExpressionParser
{- As an illustration to show interpreters are not hard to write, we make
an interpreter for a tiny language with:
  * a single data type: `Nat`
  * arithmetic expressions can have `+`, `*` and parenthesis.
  * assignment statements of the form `let variable = expression`, with variable names being a single character.
-}

import Parsers

-- Statements in our language, these are either expressions or definitions.
data Statement : Type where
  Expression: (n: Nat) -> Statement
  Definition: (var: Char) -> (value: Nat) -> Statement

-- A block (also called context) which is a list of statements but with the last statement the head of the list.
Block : Type
Block = List Statement

-- Getting a variable from a block; if it is defined more than once the last definition is used.
getVar : Block -> Char -> Maybe Nat
getVar [] c = Nothing
getVar ((Expression n) :: xs) c = getVar xs c
getVar ((Definition var value) :: xs) c =
  if var == c then Just value else getVar xs c

-- Parser for a variable name in a context
var : Block -> Parser Nat
var bl s = mapMaybe(letter)(getVar bl)(s)

-- Parsing a block of statements recursively
mutual
  -- A simple term in context: a literal natural number, a variable defined in the context or an expression in parenthesis
  simpleTerm : Block -> Parser Nat
  simpleTerm bl = nat || ((SS "(") <+ (expression bl) +> (SS ")")) || (var bl)

  -- A product of simple terms in context, possibly with just one simple term
  term : Block -> Parser Nat
  term bl = map(repSepTrim (simpleTerm bl) '*')(foldl(*)(1))

  -- A sum of terms in context, possibly with just one term
  expression: Block -> Parser Nat
  expression bl = map(repSepTrim (term bl) '+')(foldl(+)(0))

  -- An arithmetic expression as a statement parsed in context
  expr : Block -> Parser Statement
  expr bl = map(expression bl)(Expression)

  -- Parser for LHS and RHS of a definition in context
  defSides: Block -> Parser (Char, Nat)
  defSides bl = ((SS "let ") <+ letter +> (SS "=")) ++ (expression bl)

  -- Parser for a definition in a context
  defn : Block -> Parser Statement
  defn bl = map(defSides bl)(\p => (case p of
                                         (name, value) => Definition name value))

  -- Parser for a statement in context
  stat : Block -> Parser Statement
  stat bl = ((defn bl) || (expr bl)) +> ((SS ";") || map(eof)(\u => ";"))

  -- Parser for an empty block in context, returns the given context
  emptyBlock : Block -> Parser Block
  emptyBlock bl = map(rep(SS " ") <+ eof)(\u => bl)

  -- Recursively parsing a block given a context
  blockRec : Block -> Parser Block
  blockRec bl =
    (emptyBlock bl) ||
    flatMapWithNext(stat bl)(
      \s => blockRec (s :: bl))

-- Parser for a block, starting with the empty context
block: Parser Block
block = blockRec []

-- The value of a block: the value/rhs of the last statment, defaulting to 0
blockValue: Block -> Nat
blockValue [] = Z
blockValue ((Expression n) :: xs) = n
blockValue ((Definition var value) :: xs) = value

-- Interpret a string and getting the value of the result
interpret : String -> ParseResult Nat
interpret s = parse(map(block)(blockValue)) s

-- An example
eg: ParseResult Nat
eg = interpret "let a = (1 + 2 * (3 + 1)); let b = a + 3 ; a * (b + 1)"


text:
||| This is almost exact copy from the book with some naming adjusted
||| see
||| https://github.com/edwinb/TypeDD-Samples/blob/master/Chapter15/ProcessLib.idr
module Part3.Sec15a_ProcessLib

import System.Concurrency.Channels

%default total

||| `iface : reqType -> Type` defines type level service interface (service commands)
||| `reqType` would typically be some ADT defining commands and LHS `Type` is the
||| result type,  Idris makes these easier to define than Haskell but this approach
||| maps to the pattern of lifting ADT
||| with DataKinds and using GADT/Sing to map these back to `Type`
export
data MessagePID : (iface : reqType -> Type) -> Type where
     MkMessage : PID -> MessagePID iface

public export
NoRecv : Void -> Type
NoRecv = const Void

public export
data ProcState = Ready | Sent | Looping

{-
                     Respond
                       ->
            Respond   |  |      Loop
    Ready   ------->  Sent   --------> Looping
                             <--------
                              Respond
-}

||| payload type is the second type variable (after interface)
public export
data Process : (iface : reqType -> Type) ->
               Type -> ProcState -> ProcState -> Type where
     ||| Given service process and request message
     ||| returns paload as defined by service_iface, does not change state
     Request : MessagePID service_iface ->
               (msg : service_reqType) ->
               Process iface (service_iface msg) st st
     ||| CPS handler returns Process in in Ready state, iface is not specified but
     ||| iface (iface msg) is contrained, intersting this can be used with Pure
     ||| Note:  `Ready Ready` in CPS input works with Pure and Action
     Respond : ((msg : reqType) -> Process iface (iface msg) Ready Ready) ->
               Process iface (Maybe reqType) st Sent
     ||| see below (`Service iface a = Process iface a Ready Looping`)
     ||| given a service returns (maybe) process handle to it
     Spawn : Process service_iface () Ready Looping ->
             Process iface (Maybe (MessagePID service_iface)) st st

     ||| used by service to loop (note moves from Ready to Sent to provide
     ||| extra type safety while still allows to chain after any Respond
     ||| keeping Ready as starting state, see (>>=))
     ||| This basically allows server to be coded as `server = Respond (...) >> Loop server`
     Loop : Inf (Process iface a Ready Looping) ->
            Process iface a Sent Looping
     ||| Encodes IO as process
     Action : IO a -> Process iface a st st
     Pure : a -> Process iface a st st
     (>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) ->
             Process iface b st1 st3

public export
data Fuel = Dry | More (Lazy Fuel)

export partial
forever : Fuel
forever = More forever

export total
run : Fuel -> Process iface t in_state out_state -> IO (Maybe t)
run fuel (Request {service_iface} (MkMessage process) msg)
          = do Just chan <- connect process
                    | _ => pure Nothing
               ok <- unsafeSend chan msg
               if ok then do Just x <- unsafeRecv (service_iface msg) chan
                                  | Nothing => pure Nothing
                             pure (Just x)
                     else pure Nothing
run fuel (Respond {reqType} calc)
          = do Just sender <- listen 1
                    | Nothing => pure (Just Nothing)
               Just msg <- unsafeRecv reqType sender
                    | Nothing => pure (Just Nothing)
               Just res <- run fuel (calc msg)
                    | Nothing => pure Nothing
               unsafeSend sender res
               pure (Just (Just msg))
run (More fuel) (Loop proc) = run fuel proc
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                                | Nothing => pure (Just Nothing)
                           pure (Just (Just (MkMessage pid)))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                                  | Nothing => pure Nothing
                             run fuel (next x)
run Dry _ = pure Nothing

public export
Service : (iface : reqType -> Type) -> Type -> Type
Service iface a = Process iface a Ready Looping

public export
Client : Type -> Type
Client a = Process NoRecv a Ready Ready

partial export
runProc : Process iface () in_state out_state -> IO ()
runProc proc = do run forever proc
                  pure ()

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Salo.Language.TT

public export
data TT : Type -> Nat -> Type where
  P : TT m n

public export
record Binding (n : Nat) where
  constructor B
  name : String
  type : TT Bool n

public export
implementation Show (Binding n) where
  show x = show x.name

public export
data Name = UN String

public export
implementation Show Name where
  show (UN s) = show s

max_stars_repo_name: semissioncontrol/semcos

max_issues_repo_name: semissioncontrol/semcos

max_forks_repo_name: semissioncontrol/semcos


text:
-- test that things arrive in the order sent

import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          let val1 = 1
          let val2 = 2
          (MkDPair bc send) <- becomeSender bcRef
          (MkDPair bc' recv) <- becomeReceiver Blocking bcRef
          send Signal bc val1
          send Signal bc val2
          val1' <- recv bc'
          val2' <- recv bc'
          if val1 /= val1'
             then putStrLn "ERROR: First value changed in transit."
             else if val2 /= val2'
                     then putStrLn "ERROR: Second value changed in transit."
                     else putStrLn "Success!"


text:
import Data.Vect

Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

TupleVect : (n : Nat) -> (ty : Type) -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

test : TupleVect 4 Nat
test = (1, 2, 3, 4, ())

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


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

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

module Main

import StarterWareFree.Utils

main : IO ()
main = do
    ConsoleUtilsInit
    ConsoleUtilsSetType 0
    ConsoleUtilsPrintf "Hello, bare-metal Idris"

max_stars_repo_name: mokshasoft/bare-metal-idris

max_issues_repo_name: mokshasoft/bare-metal-idris

max_forks_repo_name: mokshasoft/bare-metal-idris


text:
module Test.Chapter6

import Test
import Exercises.Chapter6

%access public export

-- FIXME: This is a little weird...
testTupleVect : IO ()
testTupleVect = assertEq (1,2,3,4,()) (the (TupleVect 4 Nat) (1,2,3,4,()))

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module Streaming.Internal

import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.State

import public Data.Functor.Of
import public Data.Functor.Compose

import Control.Monad.Managed

-- Do I need builder-style stream fusion? If everything I do is a 'step' then
-- what is there to fuse? Sure it should help for operations on the result type,
-- but does it help for the stream state?

||| A neat bonus to the Build constructor is that we don't have to 'case' as
||| often when writing our functions because we can just farm out to Build which
||| streamFold will eventually case for us.
||| The Linearities are to satisfy HasIO, they might not stay.
public export
data Stream : (f : Type -> Type) -> (m : Type -> Type) -> Type -> Type where
  Return : (1 _ : r) -> Stream f m r
  ||| This is probably too strict right now, Step is strict in haskell but Effect is not
  Effect : (1 _ : m (Stream f m r)) -> Stream f m r
  Step : (1 _ : f (Stream f m r)) -> Stream f m r
  ||| Fusion constructor
  ||| We don't have a serious rewrite system in idris2 yet so this does the job
  ||| of fusing as long as we're careful about using streamFold and Build
  ||| whenever we can.
  Build : (1 _ : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b)) -> Stream f m r

%name Streaming.Internal.Stream str,str2,str3

export
streamBuild : (forall b. (r -> b) -> (m b -> b) -> (f b -> b) -> b)
           -> Stream f m r
streamBuild = \phi => phi Return Effect Step

export
streamFold : (Functor f, Monad m)
          => (r -> b) -> (m b -> b) -> (f b -> b) -> Stream f m r -> b
streamFold done effect construct (Return x) = done x
streamFold done effect construct (Effect x)
  = effect (streamFold done effect construct <$> x)
streamFold done effect construct (Step x)
  = construct (streamFold done effect construct <$> x)
streamFold done effect construct (Build g) = g done effect construct

-- %transform "dsfsdf" streamFold return_ effect_ step_ (streamBuild psi) = psi return_ effect_ step_

export
destroy : (Functor f, Monad m)
       => Stream f m r -> (f b -> b) -> (m b -> b) -> (r -> b) -> b
destroy stream construct effect done = streamFold done effect construct stream

mutual
  public export
  implementation
  (Functor f, Monad m) => Functor (Stream f m) where
    map f x = Build (\r,eff,step => streamFold (r . f) eff step x)

  public export
  implementation
  (Functor f, Monad m) => Applicative (Stream f m) where
    pure = Return
    x <*> y = do f <- x
                 v <- y
                 pure (f v)
  public export
  implementation
  (Functor f, Monad m) => Monad (Stream f m) where
    x >>= k = Build (\r,eff,step => streamFold (streamFold r eff step . k) eff step x)

-- Alternative (Stream f m) where

public export -- public, we're exporting Stream currently anyway
%inline
wrap : (Functor f, Monad m) => f (Stream f m a) -> Stream f m a
-- wrap x = Build (\r,eff,step => step $ map (streamFold r eff step) x)
wrap = Step

public export -- public, we're exporting Stream currently anyway
%inline
effect : (Functor f, Monad m) => m (Stream f m r) -> Stream f m r
effect = Effect

export
inspect : (Functor f, Monad m)
       => Stream f m r -> m (Either r (f (Stream f m r)))
inspect str
  = streamFold
      (pure . Left)
      join
      -- We compress the guts and then reconstruct around it.
      (pure . (Right . map (Effect {f} {m} . map (either Return Step))))
      str

export
unfold : (Functor f, Monad m)
      => (s -> m (Either r (f s))) -> s -> Stream f m r
unfold step s = Effect $ do
    Right fs <- step s
      | Left r => pure (Return r)
    pure (Step (unfold step <$> fs))

-- unfold inspect = id
baf : (Functor f, Monad m) => Stream f m r -> Stream f m r
baf = unfold inspect

infixr 2 |> -- flip .
export
||| reversed . for forward combination of stream operations
(|>) : (a -> b) -> (b -> c) -> a -> c
f |> g = \x => g (f x)

infixl 1 &$ -- flip $
export
||| reversed $ for forward combination of stream operations
(&$) : a -> (a -> b) -> b
x &$ f = f x

-------------------------------------------------
-- Maps
-- Mind that these don't share the same naming scheme as Haskell's 'streaming'
-------------------------------------------------

export
||| map(f): Target the (f)unctor of `Stream f m r`.
mapf : (Functor f, Monad m)
    => (forall x. f x -> g x) -> Stream f m r -> Stream g m r
mapf f s = Build (\r,eff,step => streamFold r eff (step . f) s)

export
||| map(s): Target (s)tream _values_ of `Stream (Of s) m r`.
maps : Monad m
    => (a -> b) -> Stream (Of a) m r -> Stream (Of b) m r
maps f s = mapf (mapFst f) s

export
||| map(f)M: Effectfully target the (f)unctor of `Stream f M r`.
mapfM : (Monad m, Functor f)
     => (forall x. f x -> m (g x)) -> Stream f m r -> Stream g m r
mapfM f s = Build (\r,eff,step => streamFold r eff (eff . map step . f) s)

export
||| map(s)M: Effectfully target (s)tream _values_ of `Stream (Of s) M r`.
mapsM : Monad m
    => (a -> m b) -> Stream (Of a) m r -> Stream (Of b) m r
mapsM f s = mapfM (\(c :> g) => (:> g) <$> f c) s

export
||| hoist: Target the (m)onad of a `Stream (Of s) m r`
hoist : (Functor f, Monad m)
    => (forall x. m x -> n x) -> Stream f m r -> Stream f n r
hoist f str = Build (\r,eff,step => streamFold r (eff . f) step str)

export
decompose : (Functor f, Monad m)
         => Stream (Compose m f) m r -> Stream f m r
decompose g
  = Build (\r,eff,step => streamFold r eff (eff . map step . getCompose) g)

export
run : Monad m => Stream m m r -> m r
run (Return x) = pure x
run (Effect x) = x >>= run
run (Step x) = x >>= run
run (Build g) = run (streamBuild g) -- probably reasonable, we're running after all

export
mapsM_ : (Monad m, Functor f) => (forall x . f x -> m x) -> Stream f m r -> m r
mapsM_ f = run . mapf f

||| This specializes to e.g.
||| intercalates :: (Monad m, Functor f) => Stream f m ()
||| -> Stream (Stream f m) m r -> Stream f m r
export
intercalates : (Monad m, Monad (t m), MonadTrans t)
            => t m x -> Stream (t m) m r -> t m r
intercalates sep (Return y) = pure y
intercalates sep (Effect y) = lift y >>= intercalates sep
intercalates sep (Step y) = do
    f' <- y
    steps sep f'
  where
    steps : t m x -> Stream (t m) m r -> t m r
    steps sep (Return y) = pure y
    steps sep (Effect y) = lift y >>= steps sep
    steps sep (Step y) = do
      sep
      f' <- y
      steps sep f'
    steps sep (Build g) = intercalates sep (streamBuild g)
intercalates sep (Build g) = intercalates sep (streamBuild g)

public export
(Functor f, HasIO m) => HasIO (Stream f m) where
  liftIO act = Effect (liftIO $ io_bind act (pure . Return))

public export
Functor f => MonadTrans (Stream f) where
  lift = Effect . map Return

public export
(Functor f, MonadManaged m) => MonadManaged (Stream f m) where
  use res = lift (use res)

public export
(Functor f, MonadReader r m) => MonadReader r (Stream f m) where
  ask = lift ask
  local f = hoist (local f)

public export
(Functor f, MonadState s m) => MonadState s (Stream f m) where
  get = lift get
  put s = lift (put s)

||| Run stream1 then stream2, <+> the results of each.
public export
(Semigroup r, Functor f, Monad m) => Semigroup (Stream f m r) where
  str <+> str2 = Build (\r,eff,step => streamFold (\v => streamFold (r . (v <+>))
                         eff step str2) eff step str)

public export
(Monoid r, Functor f, Monad m) => Monoid (Stream f m r) where
  neutral = pure neutral


text:
module Data.Bifunctor

%access public export

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

interface Bifunctor (f : Type -> Type -> Type) where
  bimap : (a -> b) -> (c -> d) -> f a c -> f b d

interface Bifunctor f => VerifiedBifunctor (f : Type -> Type -> Type) where
  bifunctorIdentity : {a, b : Type} -> (x : f a b) -> bimap Basics.id Basics.id x = Basics.id x
  bifunctorComposition : {a, b, c, d, e, g : Type} -> (x : f a b) ->
                         (f1 : a -> c) -> (f2 : c -> d) ->
                         (g1 : b -> e) -> (g2 : e -> g) ->
                         bimap (f2 . f1) (g2 . g1) x = (bimap f2 g2 . bimap f1 g1) x

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

Bifunctor Either where
  bimap f _ (Left l) = Left (f l)
  bimap _ g (Right r) = Right (g r)

VerifiedBifunctor Either where
  bifunctorIdentity (Left l) = Refl
  bifunctorIdentity (Right r) = Refl
  bifunctorComposition (Left l) f1 f2 g1 g2 = Refl
  bifunctorComposition (Right r) f1 f2 g1 g2 = Refl

Bifunctor Pair where
  bimap f g (a, b) = (f a, g b)

VerifiedBifunctor Pair where
  bifunctorIdentity (a, b) = Refl
  bifunctorComposition (a, b) f1 f2 g1 g2 = Refl

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

-- | Map a function over the first type argument of a `Bifunctor`.
lmap : Bifunctor f => (a -> b) -> f a c -> f b c
lmap f = bimap f id

-- | Map a function over the second type arguments of a `Bifunctor`.
rmap : Bifunctor f => (b -> c) -> f a b -> f a c
rmap = bimap id

max_stars_repo_name: Risto-Stevcev/idris-functors

max_issues_repo_name: Risto-Stevcev/idris-functors

max_forks_repo_name: Risto-Stevcev/idris-functors


text:
module Minecraft.Core.Entity.Pickup.GenericData

%default total

public export
record GenericItemEntityData (i : Type) where
  constructor MkItemEntity
  item : i

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Regex

-- Based on https://homepage.divms.uiowa.edu/~astump/papers/stump-icfp20.pdf

data ListF : Type -> Type -> Type where
  Nil : ListF a f
  Cons : a -> f -> ListF a f

data StdRegF : (r : Type) -> Type where
   NoMatch : StdRegF r
   MatchChar : Char -> StdRegF r
   Or : r -> r -> StdRegF r
   Plus : r -> StdRegF r
   Concat : r -> r -> StdRegF r

data Mu : (f : Type -> Type) -> Type where
  In : (f (Mu f)) -> Mu f

List' : Type -> Type
List' a = Mu (ListF a)

nil : List' a
nil = In Nil

isNil : List' a -> Bool
isNil (In []) = False
isNil (In (Cons x xs)) = True

(::) : a -> List' a -> List' a
(::) x xs = In (Cons x xs)

str : String -> List' Char
str xs = str' $ unpack xs
  where str' : List Char -> List' Char
        str' [] = In $ Nil
        str' (x :: xs) = In $ Cons x (str' xs)

StdReg : Type
StdReg = Mu StdRegF

char : Char -> StdReg
char c = In $ MatchChar c

concat : StdReg -> StdReg -> StdReg
concat r1 r2 = In $ Concat r1 r2

or : StdReg -> StdReg -> StdReg
or r1 r2 = In $ Or r1 r2

plus : StdReg -> StdReg
plus r = In $ Plus r

McatapnAlg : (f : Type -> Type) -> (x : Type -> Type) -> Type
McatapnAlg f x = {r : Type} -> (r -> x r) -> (r -> Mu f) -> f r -> x r

mcatapn : McatapnAlg f x -> Mu f -> x (Mu f)
mcatapn alg (In d) = alg (mcatapn alg) id d

K : Type -> Type
K t = t -> Bool

MatchT : Type -> Type
MatchT t = K t -> Bool

matchi : {t : Type} -> (t -> StdReg -> MatchT t) -> StdReg -> Char -> t -> MatchT t
matchi {t} match reg = mcatapn {x = MatchiX t} alg reg
  where MatchiX : (t : Type) -> (r : Type) -> Type
        MatchiX t _ = Char -> t -> MatchT t
        alg : McatapnAlg StdRegF (MatchiX t)
        alg eval _ NoMatch c cs k = False
        alg eval _ (MatchChar c') c cs k = if c == c' then k cs else False
        alg eval _ (Or r1 r2) c cs k = eval r1 c cs k || eval r2 c cs k
        alg eval reveal (Plus r) c cs k = eval r c cs (\cs => k cs || match cs (In (Plus $ reveal r)) k)
        alg eval reveal (Concat r1 r2) c cs k = eval r1 c cs (\cs => match cs (reveal r2) k)

match : List' Char -> StdReg -> Bool
match xs reg = mcatapn alg xs reg (\_ => True)
  where MatchX : Type -> Type
        MatchX r = StdReg -> MatchT r
        alg : McatapnAlg (ListF Char) MatchX
        alg eval _ Nil r k = False
        alg eval _ (Cons c cs) r k = matchi eval r c cs k

example : StdReg
example = concat (concat (char 'c') (plus $ or (char 'a') (char 'd'))) (char 'r')

test0 : Bool
test0 = match (str "car") example

test1 : Bool
test1 = match (str "cdr") example

test2 : Bool
test2 = match (str "cr") example

test3 : Bool
test3 = match (str "cddar") example

test4 : Bool
test4 = match (str "cdda") example

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
total
tailRecId : (a -> Either a b) -> a -> b
tailRecId f a with (f a)
  tailRecId f a | Left a2 = tailRecId f a2
  tailRecId f a | Right x = x

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Idris.IDEMode.SyntaxHighlight

import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Metadata

import Idris.REPL
import Idris.Syntax
import Idris.Pretty
import Idris.Doc.String
import Idris.IDEMode.Commands

import Data.List

import Libraries.Data.PosMap

%default total

||| Output some data using current dialog index
export
printOutput : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              SourceHighlight -> Core ()
printOutput highlight
  =  do opts <- get ROpts
        case idemode opts of
          REPL _ => pure ()
          IDEMode i _ f =>
            send f (Intermediate (HighlightSource [highlight]) i)

outputHighlight : {auto c : Ref Ctxt Defs} ->
                  {auto opts : Ref ROpts REPLOpts} ->
                  Highlight -> Core ()
outputHighlight hl =
  printOutput $ Full hl

lwOutputHighlight :
  {auto c : Ref Ctxt Defs} ->
  {auto opts : Ref ROpts REPLOpts} ->
  (FileName, NonEmptyFC, Decoration) -> Core ()
lwOutputHighlight (fname, nfc, decor) =
  printOutput $ Lw $ MkLwHighlight {location = cast (fname, nfc), decor}

outputNameSyntax : {auto c : Ref Ctxt Defs} ->
                   {auto s : Ref Syn SyntaxInfo} ->
                   {auto opts : Ref ROpts REPLOpts} ->
                   (FileName, NonEmptyFC, Decoration, Name) -> Core ()
outputNameSyntax (fname, nfc, decor, nm) = do
      defs <- get Ctxt
      log "ide-mode.highlight" 20 $ "highlighting at " ++ show nfc
                                 ++ ": " ++ show nm
                                 ++ "\nAs: " ++ show decor
      let fc = justFC nfc
      let (mns, name) = displayName nm
      outputHighlight $ MkHighlight
         { location = cast (fname, nfc)
         , name
         , isImplicit = False
         , key = ""
         , decor
         , docOverview = "" --!(getDocsForName fc nm)
         , typ = "" -- TODO: extract type maybe "" show !(lookupTyExact nm (gamma defs))
         , ns = maybe "" show mns
         }

export
outputSyntaxHighlighting : {auto c : Ref Ctxt Defs} ->
                           {auto m : Ref MD Metadata} ->
                           {auto s : Ref Syn SyntaxInfo} ->
                           {auto opts : Ref ROpts REPLOpts} ->
                           String ->
                           REPLResult ->
                           Core REPLResult
outputSyntaxHighlighting fname loadResult = do
  opts <- get ROpts
  when (opts.synHighlightOn) $ do
    meta <- get MD
    modIdent <- ctxtPathToNS fname

    let allNames = filter ((PhysicalIdrSrc modIdent ==) . fst . fst)
                     $ toList meta.nameLocMap
    --decls <- filter (inFile fname) . tydecls <$> get MD
    --_ <- traverse outputNameSyntax allNames -- ++ decls)

    let semHigh = meta.semanticHighlighting
    log "ide-mode.highlight" 19 $
      "Semantic metadata is: " ++ show semHigh

    let aliases
          : List ASemanticDecoration
          = flip foldMap meta.semanticAliases $ \ (from, to) =>
              let decors = uncurry exactRange (snd to) semHigh in
              map (\ ((fnm, loc), rest) => ((fnm, snd from), rest)) decors
    log "ide-mode.highlight.alias" 19 $
      "Semantic metadata from aliases is: " ++ show aliases

    let defaults
         : List ASemanticDecoration
         = flip foldMap meta.semanticDefaults $ \ decor@((_, range), _) =>
             case uncurry exactRange range semHigh of
               [] => [decor]
               _ => []

    traverse_ {b = Unit}
         (\(nfc, decor, mn) =>
           case mn of
             Nothing => lwOutputHighlight (fname, nfc, decor)
             Just n  => outputNameSyntax  (fname, nfc, decor, n))
         (defaults ++ aliases ++ toList semHigh)

  pure loadResult


text:
data Direction = North | East | South | West

data Nat = Z | S Nat

turnClockwise : Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North


text:
module Text.WebIDL.Codegen.Types

import public Data.SortedMap
import public Data.Validated
import Text.WebIDL.Types

import Generics.Derive

%language ElabReflection

--------------------------------------------------------------------------------
--          Kinds
--------------------------------------------------------------------------------

||| The kind of a WebIDL identifier.
|||
||| This is needed when converting external types to Idris2 types
||| in the code generator: Aliases need to be resolved, Enums
||| converted to their `String` representation, Callback arguments
||| are Idris2 functions that need to be converted to an external
||| type.
public export
data Kind : Type where
  KAlias      : Identifier -> Kind
  KCallback   : Identifier -> Kind
  KDictionary : Identifier -> Kind
  KEnum       : Identifier -> Kind
  KInterface  : (isParent : Bool) -> Identifier -> Kind
  KMixin      : Identifier -> Kind
  KOther      : Identifier -> Kind

%runElab derive "Kind" [Generic,Meta,Eq,Show]

public export
isParent : Kind -> Bool
isParent (KDictionary _)  = True
isParent (KInterface b _) = b
isParent (KMixin _)       = True
isParent _                = False

public export
ident : Kind -> Identifier
ident (KAlias x)        = x
ident (KCallback x)     = x
ident (KDictionary x)   = x
ident (KEnum x)         = x
ident (KInterface _ x)  = x
ident (KMixin x)        = x
ident (KOther x)        = x

public export
kindToString : Kind -> String
kindToString = value . ident

public export
data Wrapper = Direct | Opt | May | OptMay

public export
opt : Wrapper -> Wrapper
opt Direct = Opt
opt May    = OptMay
opt i      = i

public export
may : Wrapper -> Wrapper
may Direct = May
may i      = i

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

mutual
  public export
  data SimpleType : Type where
    ||| The undefined type (or () if it is a return type)
    Undef        : SimpleType

    ||| `Boolean` at the FFI, `Bool` in the API.
    Boolean      : SimpleType

    ||| A Web IDL interface. This has an instance of `SafeCast`,
    ||| and is being abstracted over when used in an argument
    ||| list in the API, but only, when the `isParent` flag is set to true.
    ||| If this flag is `False`, meaning that there are no subtypes of
    ||| this type, we do not abstract over the type to improve
    ||| type inference.
    Interface   : (isParent : Bool) -> Identifier  -> SimpleType

    ||| A dictionary, specifying a Javascript object with a
    ||| set of mandatory and optional attributes.
    ||| This is always abstracted over, since theoretically
    ||| every value with the same set of attributes is
    ||| a dictionary of the given type.
    |||
    ||| The type of a dictionary cannot be verified at
    ||| runtime, therefore they have no instance of `SafeCast`.
    Dictionary  : Identifier  -> SimpleType

    ||| A Web IDL `Mixin` is a set of attributes and operations (functions)
    ||| shared by several types. A type includes a given mixin, if
    ||| a corresponding `includes` statement is provided in the spec.
    |||
    ||| Mixins do not define new types, and whether a value implements
    ||| a given mixin can typcally not be verified at runtime, therefore
    ||| mixins come without an instance of `SafeCast`.
    ||| runtime, therefore they have no instance of `SafeCast`.
    Mixin  : Identifier  -> SimpleType

    ||| Primitive type or a wrapper of a primitive.
    ||| This is the same at the FFI and API and
    ||| has an instance of `SafeCast`.
    Primitive : String      -> SimpleType

    ||| Types that do not change between FFI and API
    Unchangeable : String      -> SimpleType

    ||| Enum type at the API, Strings at the FFI
    Enum         : Identifier  -> SimpleType

    ||| Some kind of Array
    Array        : CGType      -> SimpleType

    ||| Some kind of Record
    Record       : String      -> CGType -> SimpleType

  public export
  data CGType : Type where
    Any     : CGType
    Promise : CGType                      -> CGType
    Simple  : Nullable SimpleType         -> CGType
    Union   : Nullable (List1 SimpleType) -> CGType

||| True, if the type can be used as an index in a
||| WebIDL `Getter` or `Setter`, that is, it corresponds
||| to either an `unsigned long` or a `DOMString`.
export
isIndex : CGType -> Bool
isIndex (Simple $ NotNull $ Primitive "String") = True
isIndex (Simple $ NotNull $ Primitive "Bits32") = True
isIndex _                                          = False

namespace SimpleType
  ||| True, if the FFI representation of the given type
  ||| has a `SafeCast` implementation
  export
  safeCast : SimpleType -> Bool
  safeCast Undef            = True
  safeCast Boolean          = True
  safeCast (Interface _ x)  = True
  safeCast (Dictionary _)   = False
  safeCast (Mixin _)        = False
  safeCast (Primitive x)    = True
  safeCast (Unchangeable x) = False
  safeCast (Enum x)         = True
  safeCast (Array x)        = False
  safeCast (Record x y)     = False

  ||| True, if the type uses the same representation in
  ||| the FFI and the API as a function argument
  export
  sameArgType : SimpleType -> Bool
  sameArgType Undef            = True
  sameArgType Boolean          = False
  sameArgType (Interface b _)  = not b
  sameArgType (Dictionary _)   = False
  sameArgType (Mixin _)        = False
  sameArgType (Primitive t)    = True
  sameArgType (Unchangeable _) = True
  sameArgType (Enum _)         = False
  sameArgType (Array _)        = True
  sameArgType (Record _ _)     = True

  ||| True, if the type uses the same representation in
  ||| the FFI and the API as a return value.
  export
  sameRetType : SimpleType -> Bool
  sameRetType Undef            = True
  sameRetType Boolean          = False
  sameRetType (Interface _ _)  = True
  sameRetType (Dictionary _)   = True
  sameRetType (Mixin _)        = True
  sameRetType (Primitive _)    = True
  sameRetType (Unchangeable _) = True
  sameRetType (Enum _)         = False
  sameRetType (Array _)        = True
  sameRetType (Record _ _)     = True

  export
  inheritance : SimpleType -> Maybe (Identifier,Wrapper)
  inheritance (Interface True x)  = Just (x,Direct)
  inheritance (Dictionary x)      = Just (x,Direct)
  inheritance (Mixin x)           = Just (x,Direct)
  inheritance _                   = Nothing

namespace CGType

  public export
  simple : SimpleType -> CGType
  simple = Simple . NotNull

  public export
  unchangeable : String -> CGType
  unchangeable = simple . Unchangeable

  public export
  iface : Bool -> Identifier -> CGType
  iface b = simple . Interface b

  public export
  mixin : Identifier -> CGType
  mixin = simple . Mixin

  public export
  dict : Identifier -> CGType
  dict = simple . Dictionary

  ||| Wrapps the given kind in return type.
  export
  fromKind : Kind -> CGType
  fromKind (KAlias x)        = unchangeable x.value
  fromKind (KCallback x)     = unchangeable x.value
  fromKind (KDictionary x)   = dict x
  fromKind (KEnum x)         = Simple . NotNull $ Enum x
  fromKind (KInterface b x)  = iface b x
  fromKind (KMixin x)        = mixin x
  fromKind (KOther x)        = unchangeable x.value

  ||| True, if the FFI representation of the given type
  ||| has a `SafeCast` implementation
  export
  safeCast : CGType -> Bool
  safeCast Any         = True
  safeCast (Promise x) = False
  safeCast (Simple x)  = safeCast $ nullVal x
  safeCast (Union _)   = False

  ||| True, if the given type is the same in the API and
  ||| the FFI when used as an argument
  export
  sameArgType : CGType -> Bool
  sameArgType Any                    = False
  sameArgType (Promise x)            = True
  sameArgType (Simple $ MaybeNull _) = False
  sameArgType (Simple $ NotNull x)   = sameArgType x
  sameArgType (Union  _)             = False

  ||| True, if the given type is the same in the API and
  ||| the FFI when used as a return value
  export
  sameRetType : CGType -> Bool
  sameRetType Any                    = False
  sameRetType (Promise x)            = True
  sameRetType (Simple $ MaybeNull _) = False
  sameRetType (Simple $ NotNull x)   = sameRetType x
  sameRetType (Union  $ MaybeNull _) = False
  sameRetType (Union  $ NotNull xs)  = not $ all safeCast xs

  export
  inheritance : CGType -> Maybe (Identifier,Wrapper)
  inheritance (Simple $ MaybeNull x) = map may <$> inheritance x
  inheritance (Simple $ NotNull x)   = inheritance x
  inheritance _                      = Nothing

--------------------------------------------------------------------------------
--          ReturnType
--------------------------------------------------------------------------------

||| A function's return type.
public export
data ReturnType : Type where
  ||| This will be mapped to `()` in the codegen.
  Undefined : ReturnType

  ||| The attribute in question might not be defined
  ||| The return type will be wrapped in `UndefOr` in
  ||| the code generator.
  UndefOr  : CGType -> Maybe Default -> ReturnType

  ||| Nothing special about the wrapped return type.
  Def      : CGType -> ReturnType

||| Checks if the return type is `Undefined`.
public export
isUndefined : ReturnType -> Bool
isUndefined Undefined = True
isUndefined _         = False

namespace ReturnType

  public export
  simple : SimpleType -> ReturnType
  simple = Def . simple

  public export
  unchangeable : String -> ReturnType
  unchangeable = Def . unchangeable

  ||| Wrapps the given kind in return type.
  export
  fromKind : Kind -> ReturnType
  fromKind = Def . CGType.fromKind

  ||| True, if the given FFI type has a `SafeCast` instance
  export
  safeCast : ReturnType -> Bool
  safeCast Undefined     = True
  safeCast (UndefOr x _) = safeCast x
  safeCast (Def x)       = safeCast x

  ||| True, if the given return type is the same in the API and
  ||| the FFI.
  export
  sameType : ReturnType -> Bool
  sameType Undefined     = True
  sameType (UndefOr _ _) = False
  sameType (Def x)       = sameRetType x

--------------------------------------------------------------------------------
--          Constants
--------------------------------------------------------------------------------

public export
record CGConstType where
  constructor MkConstType
  primitive : String

public export
record CGConst where
  constructor MkConst
  type  : CGConstType
  name  : Identifier
  value : ConstValue

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

||| A function argument in the code generator.
public export
data CGArg : Type where
  ||| A mandatory function argument
  Mandatory : ArgumentName -> CGType -> CGArg

  ||| An optional function argument together with its
  ||| default value if the argument is `undefined`.
  Optional  : ArgumentName -> CGType -> Default -> CGArg

  ||| A variadic function argument
  VarArg    : ArgumentName -> CGType -> CGArg

export
argName : CGArg -> ArgumentName
argName (Mandatory x _)  = x
argName (Optional x _ _) = x
argName (VarArg x _)     = x

export
argType : CGArg -> CGType
argType (Mandatory _ y)  = y
argType (Optional _ y _) = y
argType (VarArg _ y)     = y

export
isOptional : CGArg -> Bool
isOptional (Optional _ _ _) = True
isOptional _                = False

namespace CGArg

  ||| True, if the given FFI type has a `SafeCast` instance
  export
  safeCast : CGArg -> Bool
  safeCast (Mandatory _ t)  = safeCast t
  safeCast (Optional _ t _) = safeCast t
  safeCast (VarArg _ _)     = False

  ||| True, if the given argument type is the same in the API and
  ||| the FFI.
  export
  sameType : CGArg -> Bool
  sameType (Mandatory _ t)  = sameArgType t
  sameType (Optional _ _ _) = False
  sameType (VarArg _ _)     = False

  export
  inheritance : CGArg -> Maybe (Identifier,Wrapper)
  inheritance (Mandatory _ t)  = inheritance t
  inheritance (Optional _ t _) = map opt <$> inheritance t
  inheritance (VarArg _ _)     = Nothing

public export
Args : Type
Args = List CGArg

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

||| A function, for which we will generate some code.
public export
data CGFunction : Type where
  ||| A read-write attribute
  Attribute :  (name : AttributeName)
            -> (obj  : Kind)
            -> (tpe  : CGArg)
            -> (ret  : ReturnType)
            -> CGFunction

  ||| An attribute getter.
  AttributeGet :  (name : AttributeName)
               -> (obj  : Kind)
               -> (tpe  : ReturnType)
               -> CGFunction

  ||| A static attribute setter.
  StaticAttributeSet :  (name : AttributeName)
                     -> (obj  : Kind)
                     -> (tpe  : CGArg)
                     -> CGFunction

  ||| A static attribute getter.
  StaticAttributeGet :  (name : AttributeName)
                     -> (obj  : Kind)
                     -> (tpe  : ReturnType)
                     -> CGFunction

  ||| An indexed getter.
  Getter : (obj : Kind) -> (index : CGArg) -> (tpe : ReturnType) -> CGFunction

  ||| An indexed setter.
  Setter : (obj : Kind) -> (index : CGArg) -> (value : CGArg) -> CGFunction

  ||| An interface constructor with (possibly) optional arguments.
  Constructor  :  (obj : Kind) -> (args : Args) -> CGFunction

  ||| An interface constructor with (possibly) optional arguments.
  DictConstructor : (obj : Kind) -> (args : Args) -> CGFunction

  ||| A regular function with (possibly) optional arguments.
  Regular      :  OperationName
               -> (obj : Kind)
               -> Args
               -> ReturnType
               -> CGFunction

  ||| A static function with (possibly) optional arguments.
  Static       :  OperationName
               -> (obj : Kind)
               -> Args
               -> ReturnType
               -> CGFunction

||| This is used for sorting lists of functions to
||| the determine the order in which they appear
||| in the generated code.
|||
||| Attributes will come first, sorted by name,
||| setters, getters, and unsetter grouped together in
||| that order.
|||
||| All other functions come later and will be sorted by name.
export
priority : CGFunction -> (Nat,String,Nat)
priority (DictConstructor n _)       = (0,value (ident n),0)
priority (Constructor n _)           = (0,value (ident n),0)
priority (StaticAttributeSet n _ _)  = (1,show n,1)
priority (StaticAttributeGet n _ _)  = (1,show n,0)
priority (Static n o _ _)            = (2,n.value ++ value (ident o),0)
priority (Getter _ _ _)              = (3,"",0)
priority (Setter _ _ _)              = (3,"",1)
priority (Attribute n _ _ _)         = (4,show n,0)
priority (AttributeGet n _ _)        = (4,show n,1)
priority (Regular n o _ _)           = (5,n.value ++ value (ident o),0)

--------------------------------------------------------------------------------
--          Inheritance
--------------------------------------------------------------------------------

||| An external, un-parameterized Javascript type, represented
||| by an identifier. Such a type comes with a parent
||| type (given as an `inheritance` value in the spec)
||| and a number of mixed in types.
|||
||| The actual name of the type is not included, as the set
||| of types is given in `Env` as a `SortedMap`.
public export
record JSType where
  constructor MkJSType
  parent : Maybe Identifier
  mixins : List Identifier

||| The parent types and mixins of a type. This is
||| used by the code generator to implement the
||| `JS.Inheritance.JSType` instances.
public export
record Supertypes where
  constructor MkSupertypes
  parents : List Identifier
  mixins  : List Identifier

--------------------------------------------------------------------------------
--          Domain
--------------------------------------------------------------------------------

public export
record CGDict where
  constructor MkDict
  name      : Identifier
  super     : Supertypes
  functions : List CGFunction

public export
record CGIface where
  constructor MkIface
  name      : Identifier
  super     : Supertypes
  constants : List CGConst
  functions : List CGFunction

public export
record CGMixin where
  constructor MkMixin
  name      : Identifier
  constants : List CGConst
  functions : List CGFunction

public export
record CGCallback where
  constructor MkCallback
  name      : Identifier
  constants : List CGConst
  type      : ReturnType
  args      : Args

public export
record CGDomain where
  constructor MkDomain
  name      : String
  callbacks : List CGCallback
  dicts     : List CGDict
  enums     : List Enum
  ifaces    : List CGIface
  mixins    : List CGMixin

export
domainFunctions : CGDomain -> List CGFunction
domainFunctions d =  (d.dicts  >>= functions)
                  ++ (d.ifaces >>= functions)
                  ++ (d.mixins >>= functions)

--------------------------------------------------------------------------------
--          Environment
--------------------------------------------------------------------------------

||| Codegen environment.
|||
||| This includes a mapping from identifiers to the kinds
||| they represent, a mapping from identifiers to their
||| inheritance relations (`jsTypes`) and a mapping of
||| type aliases.
|||
||| The `maxInheritance` constant is used when calculating a
||| type's supertypes to avoid a potentially infinite loop.
public export
record Env where
  constructor MkEnv
  maxInheritance : Nat
  kinds          : SortedMap Identifier Kind
  jsTypes        : SortedMap Identifier JSType
  aliases        : SortedMap Identifier (IdlTypeF ExtAttributeList Kind)

--------------------------------------------------------------------------------
--          Codegen Errors
--------------------------------------------------------------------------------

public export
data CodegenErr : Type where
  AnyInUnion             : Domain -> CodegenErr
  CBInterfaceInvalidOps  : Domain -> Identifier -> Nat -> CodegenErr
  InvalidConstType       : Domain -> CodegenErr
  InvalidGetter          : Domain -> Identifier -> CodegenErr
  InvalidSetter          : Domain -> Identifier -> CodegenErr
  NullableAny            : Domain -> CodegenErr
  NullablePromise        : Domain -> CodegenErr
  PromiseInUnion         : Domain -> CodegenErr
  RegularOpWithoutName   : Domain -> Identifier -> CodegenErr
  UnresolvedAlias        : Domain -> Identifier -> CodegenErr

public export
Codegen : Type -> Type
Codegen = Either (List CodegenErr)

public export
CodegenV : Type -> Type
CodegenV = Validated (List CodegenErr)


text:
module Main

import CLaSH.Prelude

dotp : Num a => Vect n a -> Vect n a -> a
dotp as bs = foldr (+) 0 (zipWith (*) as bs)

fir : (Num a, Default a) => Vect (S (S n)) (Signal a) -> Signal a -> Signal a
fir {a} coeffs x_t = y_t
  where
    xs : Default a => Vect (S (S n)) (Signal a)
    xs  = window x_t
    y_t = dotp coeffs xs

topEntity : Signal Integer -> Signal Integer
topEntity = fir [2,3,-2,8]

testInput : List Integer
testInput = [2,3,-2,8]

expectedOutput : List Integer
expectedOutput = [4,12,1,20]

main : IO ()
main = putStrLn (show $ simulate topEntity testInput == expectedOutput)

max_stars_repo_name: christiaanb/clash-prelude-idris

max_issues_repo_name: christiaanb/clash-prelude-idris

max_forks_repo_name: christiaanb/clash-prelude-idris


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#data-segments
module WebAssembly.Structure.Modules.DataSegments

import WebAssembly.Structure.Values
import WebAssembly.Structure.Instructions
import WebAssembly.Structure.Modules.Indices

import Decidable.Equality

-- Definition

public export
record Data where
  constructor MkData
  wdata  : MemIdx
  offset : Expr
  init   : List Byte

-- Equality

total public export
lemma_data__data_injective : ((d1 = d2) -> Void) -> (MkData d1 o1 i1 = MkData d2 o2 i2) -> Void
lemma_data__data_injective d1_not_d2 Refl = d1_not_d2 Refl

total public export
lemma_data__offset_injective : ((o1 = o2) -> Void) -> (MkData d1 o1 i1 = MkData d2 o2 i2) -> Void
lemma_data__offset_injective o1_not_o2 Refl = o1_not_o2 Refl

total public export
lemma_data__init_injective : ((i1 = i2) -> Void) -> (MkData d1 o1 i1 = MkData d2 o2 i2) -> Void
lemma_data__init_injective i1_not_i2 Refl = i1_not_i2 Refl

-- Dedidable Equality

public export
implementation DecEq Data where
  decEq (MkData d1 o1 i1) (MkData d2 o2 i2) = case decEq d1 d2 of
    No d1_not_d2 => No $ lemma_data__data_injective d1_not_d2
    Yes Refl     => case decEq o1 o2 of
      No o1_not_o2 => No $ lemma_data__offset_injective o1_not_o2
      Yes Refl     => case decEq i1 i2 of
        No i1_not_i2 => No $ lemma_data__init_injective i1_not_i2
        Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Ch05.Exercise_5_2_7

import Ch05.LambdaCalculus
import Ch05.Exercise_5_2_5

%default total

||| `le m n` tests whether `m` is less than or equal to `n`
le : Term
le = let m = Var 0
         n = Var 1 in
         Abs 0 (Abs 1 (iszro . (sub . m . n)))

||| Test whether two Church numerals are equal
equal : Term
equal = let m = Var 0
            n = Var 1
            m_le_n = le . m . n
            n_le_m = le . n . m in
            Abs 0 (Abs 1 (and . m_le_n . n_le_m))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Commons.Config.JSON

import Data.PList

import Text.Token
import Text.Lexer
import Text.Parser

import Language.JSON.Lexer

import public Commons.Config.JSON.Model

import Commons.Config.JSON.Parser

%default total
%access public export

fromString : String -> Maybe (JSONDoc DOC)
fromString src with (lexJSON src)
  fromString src | Nothing = Nothing
  fromString src | (Just x) with (parseJSON x)
    fromString src | (Just x) | Nothing = Nothing
    fromString src | (Just x) | (Just y) = Just y

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module LambdaSKI

-- Based on http://okmij.org/ftp/tagless-final/ski.pdf

data HasType : List a -> a -> Type where
  VZ : HasType (t :: env) t
  VS : HasType env t -> HasType (_ :: env) t

data Expr : List Type -> Type -> Type where
  Var : HasType env t -> Expr env t
  Lam : Expr (a :: env) b -> Expr env (a -> b)
  App : Expr env (a -> b) -> Expr env a -> Expr env b

data SKI : Type -> Type where
  KI : SKI (a -> a)
  KK : SKI (a -> b -> a)
  KS : SKI ((a -> b -> c) -> (a -> b) -> a -> c)
  KB : SKI ((a -> b) -> (c -> a) -> c -> b)
  KC : SKI ((a -> b -> c) -> b -> a -> c)
  KApp : SKI (a -> b) -> SKI a -> SKI b

data Repr : List Type -> Type -> Type where
  C : SKI a -> Repr env a
  N : Repr env (a -> b) -> Repr (a :: env) b
  W : Repr env a -> Repr (_ :: env) a

app : Repr env (a -> b) -> Repr env a -> Repr env b
app (C x) (C y) = C $ KApp x y
app (C x) (N y) = N $ app (C (KApp KB x)) y
app (C x) (W y) = W $ app (C x) y
app (N x) (C y) = N $ app (C  (KApp (KApp KC KC) y)) x
app (N x) (N y) = N $ app (app (C KS) x) y
app (N x) (W y) = N $ app (app (C KC) x) y
app (W x) (C y) = W $ app x (C y)
app (W x) (N y) = N $ app (app (C KB) x) y
app (W x) (W y) = W $ app x y

conv : Expr env a -> Repr env a
conv (Var VZ) = N $ C KI
conv (Var (VS x)) = W $ conv (Var x)
conv (Lam x) with (conv x)
  conv (Lam x) | (C y) = C $ KApp KK y
  conv (Lam x) | (N y) = y
  conv (Lam x) | (W y) = app (C KK) y
conv (App f x) = app (conv f) (conv x)

comp : Expr [] a -> SKI a
comp expr with (conv expr)
  comp expr | (C x) = x

example : Expr [] ((() -> ()) -> () -> ())
example = Lam (Lam (App (Var (VS VZ)) (Var VZ)))

test : SKI ((() -> ()) -> () -> ())
test = comp example


text:
%logging "declare.def.lhs" 10

data Tup : (a,b : Type) -> Type where
  MkTup : (1 f : a) -> (1 s : b) -> Tup a b

f : Tup a b -> a
f (MkTup f s) = f


text:
module Data.Cotree

import Data.Colist
import Data.Maybe
import Data.Tree

%default total

--------------------------------------------------------------------------------
--          Cotrees: Potentially infinte trees
--------------------------------------------------------------------------------

mutual
  ||| A potentially infinite rose tree
  public export
  record Cotree (a : Type) where
    constructor MkCotree
    value  : a
    forest : Inf (Coforest a)

  ||| A potentially finit stream of trees
  public export
  Coforest : Type -> Type
  Coforest = Colist . Cotree

public export
singleton : a -> Cotree a
singleton a = MkCotree a Nil

public export
unfold : (f : b -> (a,Colist b)) -> b -> Cotree a
unfold f vb = let (va,bs) = f vb
                   in MkCotree va $ unfoldF bs

  where unfoldF : Colist b -> Coforest a
        unfoldF []       = []
        unfoldF (h :: t) = unfold f h :: unfoldF t

public export
iterate : (f : a -> Colist a) -> a -> Cotree a
iterate f a = unfold (\v => (v, f v)) a

public export
expand : (a -> Colist a) -> Cotree a -> Cotree a
expand f (MkCotree v vs) = let MkCotree v2 vs2 = iterate f v
                            in MkCotree v2 (run vs vs2)
  where run : Coforest a -> Coforest a -> Coforest a
        run []        ys = ys
        run (x :: xs) ys = expand f x :: run xs ys

--------------------------------------------------------------------------------
--          To and from Tree
--------------------------------------------------------------------------------

public export
fromTree : Tree a -> Cotree a
fromTree (MkTree v fo) = MkCotree v (fromForest fo)
  where fromForest : Forest a -> Coforest a
        fromForest []        = []
        fromForest (x :: xs) = fromTree x :: fromForest xs

||| Converts a Cotree to a tree of the given maximum depth and width.
||| The maximum numbers of elements in the tree will be
||| maxWidth ^ maxDepth.
public export
toTree : (maxDepth : Nat) -> (maxWidth : Nat) -> Cotree a -> Tree a
toTree 0     _  (MkCotree v fo) = MkTree v []
toTree (S k) mw (MkCotree v fo) = MkTree v (toForest mw fo)
  where toForest : Nat -> Coforest a -> Forest a
        toForest 0     _         = []
        toForest (S n) []        = []
        toForest (S n) (t :: ts) = toTree k mw t :: toForest n ts

--------------------------------------------------------------------------------
--          Functor and Applicative
--------------------------------------------------------------------------------

public export
mapCotree : (a -> b) -> Cotree a -> Cotree b
mapCotree f (MkCotree v vs) = MkCotree (f v) (mapForest vs)
  where mapForest : Coforest a -> Coforest b
        mapForest []       = []
        mapForest (h :: t) = mapCotree f h :: mapForest t

public export
interleave : Cotree (a -> b) -> Cotree a -> Cotree b
interleave tf@(MkCotree vf fs) ta@(MkCotree va as) =
  MkCotree (vf va) (interleaveFs fs)

  where interleaveAs : Coforest a -> Coforest b
        interleaveAs []       = []
        interleaveAs (h :: t) = interleave tf h :: interleaveAs t

        interleaveFs : Coforest (a -> b) -> Coforest b
        interleaveFs []       = interleaveAs as
        interleaveFs (h :: t) = interleave h ta :: interleaveFs t

public export
bind : Cotree a -> (a -> Cotree b) -> Cotree b
bind (MkCotree v vs) f = let MkCotree w ws = f v
                       in MkCotree w (run vs ws)
  where run : Coforest a -> Coforest b -> Coforest b
        run []        ys = ys
        run (x :: xs) ys = bind x f :: run xs ys

public export
bindMaybe : Cotree (Maybe a) -> (a -> Cotree (Maybe b)) -> Cotree (Maybe b)
bindMaybe (MkCotree mv tas) f =
  case map f mv of
       Nothing => MkCotree Nothing (run tas Nil)
       Just (MkCotree mb tbs) => MkCotree mb (run tas tbs)

  where run : Coforest (Maybe a) -> Coforest (Maybe b) -> Coforest (Maybe b)
        run [] ys        = ys
        run (x :: xs) ys = bindMaybe x f :: run xs ys

--------------------------------------------------------------------------------
--          Shrinking
--------------------------------------------------------------------------------

public export
shrink : (maxSteps : Nat) -> Cotree (Maybe a) -> List a
shrink maxSteps x = run maxSteps [x]
  where run : Nat -> Coforest (Maybe a) -> List a
        run _ Nil          = Nil
        run 0 _            = Nil
        run (S k) (h :: t) = case h.value of
                               Just a  => a :: run k h.forest
                               Nothing => run k t

public export
mapShrink : (maxSteps : Nat) -> (a -> Maybe b) -> Cotree a -> List b
mapShrink ms f = shrink ms . mapCotree f

public export
shrinkIf : (maxSteps : Nat) -> (a -> Bool) -> Cotree a -> List a
shrinkIf ms p = mapShrink ms (\a => if p a then Just a else Nothing)

||| Prunes a cotree up to the given depth and width.
public export
pruneTo : (width : Nat) -> (depth : Nat) -> Cotree a -> Cotree a
pruneTo _ 0     (MkCotree v _ ) = MkCotree v Nil
pruneTo w (S d) (MkCotree v vs) = MkCotree v $ (map (pruneTo w d) $ keep w vs)
  where keep : Nat -> Colist t -> Colist t
        keep _ [] = []
        keep 0 _  = []
        keep (S k) (x :: xs) = x :: keep k xs

||| Removes all children from a cotree
public export
prune : Cotree a -> Cotree a
prune = pruneTo 0 0

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

public export
Functor Cotree where
  map = mapCotree

public export
Applicative Cotree where
  pure  = singleton
  (<*>) = interleave

--------------------------------------------------------------------------------
--          Filtering
--------------------------------------------------------------------------------

public export
takeUntil : (a -> Bool) -> Cotree a -> Cotree a
takeUntil f (MkCotree v vs) = if f v then MkCotree v []
                                     else MkCotree v (takeUntilF vs)
  where takeUntilF : Coforest a -> Coforest a
        takeUntilF []        = vs
        takeUntilF (MkCotree x xs :: ts) =
          if f x
             then [MkCotree x []]
             else MkCotree x (takeUntilF xs) :: takeUntilF ts

public export
takeBeforeNothing : Cotree (Maybe a) -> Maybe (Cotree a)
takeBeforeNothing (MkCotree Nothing _) = Nothing
takeBeforeNothing (MkCotree (Just v) vs) = Just (MkCotree v (run vs))
  where run : Coforest (Maybe a) -> Coforest a
        run []                             = []
        run ((MkCotree Nothing _) :: _)    = []
        run ((MkCotree (Just v) vs) :: ts) = MkCotree v (run vs) :: run ts

public export
takeBefore : (a -> Bool) -> Cotree a -> Maybe (Cotree a)
takeBefore f = takeBeforeNothing . map (\a => toMaybe (f a) a)

public export %inline
takeWhile : (a -> Bool) -> Cotree a -> Maybe (Cotree a)
takeWhile f = takeBefore (not . f)

public export %inline
mapMaybe : (a -> Maybe b) -> Cotree a -> Maybe (Cotree b)
mapMaybe f = takeBeforeNothing . map f


text:
import Partition
import Data.String

main : IO ()
main = do
  argv <- getArgs

  n <- pure $ index' 1 argv >>= parsePositive
  ls <- pure $ naiveAllParN <$> n

  printLn ls
  printLn $ length <$> ls


text:
module Toolkit.Data.List.Occurs

import Decidable.Equality

import Toolkit.Decidable.Informative

import Toolkit.Data.Nat
import Toolkit.Data.DList
import Toolkit.Data.List.Size
import Toolkit.Data.List.Interleaving

%default total

public export
data Occurs : (type : Type)
           -> (p    : type -> Type)
           -> (xs   : List type)
           -> (cy   : Nat)
           -> (cn   : Nat)
                   -> Type
   where
     O : (thrown     : List type)
      -> (sizeThrown : Size thrown t)

      -> (kept       : List type)
      -> (sizeKept   : Size kept   k)

      -> (prfOrigin  : Interleaving kept thrown input)

      -> (prfKept    : DList  type        holdsFor  kept)
      -> (prfThrown  : DList  type (Not . holdsFor) throw)

                    -> Occurs type holdsFor input k t

namespace Result

  public export
  data Occurs : (type : Type)
             -> (p    : type -> Type)
             -> (xs   : List type)
                     -> Type
    where
      O : {type  : Type}
       -> {p     : type -> Type}
       -> (xs    : List type)
       -> (cy,cn : Nat)
       -> (prf   : Occurs type p xs cy cn)
                -> Occurs type p xs

export
occurs : {type : Type}
      -> {p    : type -> Type}
      -> (f    : (this : type) -> Dec (p this))
      -> (xs   : List type)
              -> Occurs type p xs
occurs f []
  = O [] 0 0 (O [] Zero [] Zero Empty [] [])

occurs f (x :: xs) with (f x)
  occurs f (x :: xs) | (Yes prf) with (occurs f xs)

    occurs f (x :: xs) | (Yes prf) | (O xs cy cn (O thrown sizeThrown kept sizeKept prfOrigin prfKept prfThrown))
      = O (x::xs) (S cy) cn (O thrown sizeThrown (x :: kept) (PlusOne sizeKept) (Left x prfOrigin) (prf :: prfKept) prfThrown)

  occurs f (x :: xs) | (No not) with (occurs f xs)
    occurs f (x :: xs) | (No not) | (O xs cy cn (O thrown sizeThrown kept sizeKept prfOrigin prfKept prfThrown))
      = O (x::xs) cy (S cn) (O (x :: thrown) (PlusOne sizeThrown) kept sizeKept (Right x prfOrigin) prfKept (not :: prfThrown))

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
import Data.Primitives.Views

-- Exercise 1

every_other : Stream a -> Stream a
every_other (x :: y :: xs) = y :: every_other xs

-- Exercise 2

data InfList : Type -> Type where
     (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

Functor InfList where
    map func (value :: xs) = func value :: map func xs

Exercise 3

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'

data Face = Heads | Tails

total
getFace : Int -> Face
getFace x with (divides x 2)
  getFace ((2 * div) + rem) | (DivBy prf)
       = case rem of
              0 => Heads
              _ => Tails

coinFlips : Nat -> Stream Int -> List Face
coinFlips k rnds = map getFace (take k rnds)

-- Exercise 4

square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx
    = let next = (approx + (number / approx)) / 2 in
          approx :: square_root_approx number next

-- Exercise 5

square_root_bound : (max : Nat) -> (number : Double) -> (bound : Double) ->
                    (approxs : Stream Double) -> Double
square_root_bound Z number bound (x :: xs) = x
square_root_bound (S k) number bound (x :: xs) =
       if (abs (x * x - number) < bound)
          then x
          else square_root_bound k number bound xs

square_root : (number : Double) -> Double
square_root number = square_root_bound 100 number 0.00000000001
                                       (square_root_approx number number)


text:
module Circuits.NetList.Linear.Usage.TermType.Use.Channel

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra
import Toolkit.Data.DVect

import Circuits.Common

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage.DataType
import Circuits.NetList.Linear.Usage.DataType.Use.Full
import Circuits.NetList.Linear.Usage.DataType.Use.Partial

import Circuits.NetList.Linear.Usage.TermType

%default total

public export
data CanProject : (how  : Project dir)
               -> (type : Ty)
               -> (u    : Usage type)
                       -> Type
  where
    ProjectWrite : (prf : IsFree                   type          ein)
                       -> CanProject WRITE (TyChan type) (TyChan ein eout)

    ProjectRead : (prf : IsFree                  type              eout)
                      -> CanProject READ (TyChan type) (TyChan ein eout)

Uninhabited (CanProject how TyGate u) where
  uninhabited (ProjectWrite prf) impossible
  uninhabited (ProjectRead prf) impossible

Uninhabited (CanProject how TyUnit u) where
  uninhabited (ProjectWrite prf) impossible
  uninhabited (ProjectRead prf) impossible

Uninhabited (CanProject how (TyPort (f,dtype)) u) where
  uninhabited (ProjectWrite prf) impossible
  uninhabited (ProjectRead prf) impossible

cannotWriteTo : (IsFree type ein -> Void) -> CanProject WRITE (TyChan type) (TyChan ein eout) -> Void
cannotWriteTo f (ProjectWrite prf) = f prf

cannotReadFrom : (IsFree type eout -> Void) -> CanProject READ (TyChan type) (TyChan ein eout) -> Void
cannotReadFrom f (ProjectRead prf) = f prf

export
canProject : {type : Ty}
          -> (how : Project dir)
          -> (u   : Usage type)
                 -> Dec (CanProject how type u)
canProject how (TyPort u) = No absurd

canProject WRITE (TyChan ein eout) with (isFree ein)
  canProject WRITE (TyChan ein eout) | (Yes prf)
    = Yes (ProjectWrite prf)

  canProject WRITE (TyChan ein eout) | (No contra)
    = No (cannotWriteTo contra)

canProject READ (TyChan ein eout) with (isFree eout)
  canProject READ (TyChan ein eout) | (Yes prf)
    = Yes (ProjectRead prf)

  canProject READ (TyChan ein eout) | (No contra)
    = No (cannotReadFrom contra)

canProject how TyGate = No absurd
canProject how TyUnit = No absurd

public export
data Use : (how  : Project dir)
        -> (type : Ty)
        -> (old  : Usage type)
        -> (prf  : CanProject how type old)
        -> (new  : Usage type)
                -> Type

  where
    IsWrite : Use               type          ein                     free          newU       prf
           -> Use WRITE (TyChan type) (TyChan ein eout) (ProjectWrite free) (TyChan newU eout)

    IsRead : Use              type             eout               free              newU  prf
          -> Use READ (TyChan type)(TyChan ein eout) (ProjectRead free) (TyChan ein newU)

public export
data Result : (how  : Project dir)
           -> (type : Ty)
           -> (old  : Usage type)
           -> (prf  : CanProject how type old)
                   -> Type
  where
    R : (new : Usage  (TyChan type))
     -> (prf : Use    how (TyChan type) old proj new)
            -> Result how (TyChan type) old proj

export
use : {type : Ty}
   -> {how  : Project dir}
   -> {old  : Usage type}
   -> (prf  : CanProject how type old)
           -> Result     how type old prf
use (ProjectWrite prf) with (use prf)
  use (ProjectWrite prf) | (R u used result)
    = R (TyChan u _) (IsWrite result)
use (ProjectRead prf) with (use prf)
  use (ProjectRead prf) | (R u used result)
    = R (TyChan _ u) (IsRead result)

-- [ EOF ]


text:
> module Literate

This is a literate program in Idris. The file extension is `.lidr`, and the actual code is in lines starting with a `>`. A blank line is also expected between a line of
comment and a line of code.

Here is a simple "Hello, world" program:

> main : HasIO io => io ()
> main = putStrLn "Hello, world!"

And that is the end of the demo!

ext: lidr

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

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

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


text:
doPlus : Nat -> Nat -> Nat
doPlus x y = x `plus` y

doMult : Nat -> Nat -> Nat
doMult x y = x `mult` y

doMinus : Nat -> Nat -> Nat
doMinus x y = x `minus` y

doEqual : (m, n : Nat) -> Bool
doEqual m n = m `equalNat` n

doCompare : (m, n : Nat) -> Ordering
doCompare m n = m `compareNat` n


text:
module Syntax.Parser

import public Syntax.Term
import Syntax.Reader
import Error.Data
import Data.String
import Control.Monad.Maybe
import Data.List1
import Data.List
import Loc

Result : Type -> Type
Result = Either (Range, ParserError)

-- Name checkers

checkFirstLetter : {m : String} -> (Char -> Bool) -> (m : AsList m)  -> Bool
checkFirstLetter fn Nil = False
checkFirstLetter fn (char :: tl) = fn char

isLowered : String -> Bool
isLowered m = checkFirstLetter isLower (asList m)

isCapitalized : String -> Bool
isCapitalized m = checkFirstLetter isUpper (asList m)

-- Helper functions

incrementRange : Range -> Int -> Range
incrementRange (MkRange range _) len = (MkRange range (MkLoc ((Loc.column range) + len) (Loc.line range)))

-- Functions that actually parse IDS and paths.

parsePathRaw : (String -> Either ParserError String)
            -> (String -> Either ParserError String)
            -> Range -> String -> Result Path

parsePathRaw checkMiddle checkLast range str =
  parsePathWithPos 0 (forget $ split (== '.') str)
  where
    parsePathWithPos : Int -> (List String) -> Result Path
    parsePathWithPos curPos list =
      case list of
        (start :: []) =>
          let finalRange = incrementRange range (cast $ length start) in
          case checkLast start of
            Right res => pure $ PName finalRange res
            Left err  => Left $ (finalRange, err)
        (start :: tl) =>
          let finalRange = incrementRange range (cast $ length start) in
          case checkMiddle start of
            Right res => do
              resp <- parsePathWithPos ((cast $ length start) + 1) tl
              pure $ PDot range (MkName finalRange res) resp
            Left err => Left $ (finalRange, err)
        _ => Left $ (range, ImpossibleParsingError)

parseCapitalType : CapitalizedNameErr -> Range -> String -> Result Path
parseCapitalType err =
  parsePathRaw
    (isCapitalStr CapitalModule)
    (isCapitalStr err)
  where
    isCapitalStr : CapitalizedNameErr -> String -> Either ParserError String
    isCapitalStr err str =
      if isCapitalized str
        then Right str
        else Left (NeedCapitalizedName err)

parseTypePath : Range -> String -> Result Path
parseTypePath = parseCapitalType CapitalType

parseDCPath : Range -> String -> Result Path
parseDCPath = parseCapitalType CapitalDataConstructor

parsePath : Range -> String -> Result Path
parsePath = parsePathRaw (Right) (Right)

parseUnique : (String -> Bool) -> ParserError -> Range -> String -> Result Name
parseUnique checkLast err range str =
  let (hd ::: tl) = split (== '.') str in
  if (length tl) == 0
    then if (checkLast hd) then pure $ (MkName range hd) else Left (range, err)
    else Left $ (range, ExpectedIdButGotPath)

parseUniqueId : Range -> String -> Result Name
parseUniqueId = parseUnique isLowered NeedMinusculeName

parseUniqueType : Range -> String -> Result Name
parseUniqueType = parseUnique isCapitalized (NeedCapitalizedName CapitalType)

parseCapitalized : Range -> String -> Result Name
parseCapitalized = parseUnique isCapitalized (NeedCapitalizedName CapitalADTName)

unwrapId : TermExpr -> Result (Range, String)
unwrapId (TId range name) = Right (range, name)
unwrapId expr = Left (getRange expr, ExpectedIdentifier)

-- Parse everything

parseTypes : TermExpr -> Result Types
parseTypes (TList r (TId r_ "->" :: hd :: tl)) = do
  head <- parseTypes hd
  res <- traverse (\t => parseTypes t >>= \res => pure (getRange t, res)) tl
  let ((_, hdI) ::: tlI) = reverse $ (getRange hd, head) ::: res
  if length res /= 0
    then pure $ foldl (\acc, cur => TArrow (fst cur) (snd cur) acc) hdI tlI
    else Left $ (r, ArrowWithOneArg)

parseTypes (TList r [TId range name, type]) = do
  name <- parseTypePath range name
  type <- parseTypes type
  pure $ TPoly r name type

parseTypes (TId r str) =
  if isCapitalized str
    then pure $ TSimple r str
    else pure $ TVar r str

parseTypes expr = Left (getRange expr, NotAValidType)

parseLiteral : TermExpr -> Result Literal
parseLiteral (TStr r val) = pure (LStr r val)
parseLiteral (TInt r val) = pure (LInt r val)
parseLiteral expr  = Left (getRange expr, ExpectedLiteral)

parseTypeDef : TermExpr -> Result (Name, Maybe Types)
parseTypeDef expr@(TId range name) = do
  name <- parseUniqueType range name
  pure (name, Nothing)

parseTypeDef (TList range [name@(TId nrange str), types]) = do
  (name, _) <- parseTypeDef name
  type <- parseTypes types
  pure (name, Just type)

parseTypeDef (TList range (name :: types)) = Left (getRange name, ExpectedIdentifier)
parseTypeDef expr = Left (getRange expr, ExpectedTypeDef)

parsePat : TermExpr -> Result Pat
parsePat expr@(TStr r n) = PaLit r <$> parseLiteral expr
parsePat expr@(TInt r n) = PaLit r <$> parseLiteral expr
parsePat expr@(TId r name) = PaId <$> parseUniqueId r name

parsePat expr@(TList r ([TId r_ ":", a, b])) = do
  a <- parsePat a
  b <- parsePat b
  pure $ PaHdTl r a b

parsePat expr@(TList r [TId r_ "list"]) = pure $ PaList r []
parsePat expr@(TList r [other]) = parsePat other

parsePat expr@(TList r (name :: tl)) =
  case name of
    (TId nameRange "list") => PaList r <$> (traverse parsePat tl)
    (TId range str) => do
      path <- parseDCPath range str
      ls <- traverse parsePat tl
      pure $ PaData range path ls
    _ => Left (r, NotAValidPattern)

parsePat expr = Left (getRange expr, NotAValidPattern)

mutual
  pairUp : List TermExpr -> Result (List (Pat, Expr))
  pairUp (a::b::tl) = do
    pA <- parsePat a
    pB <- parseExpr  b
    paired <- pairUp tl
    pure ((pA, pB) :: paired)

  pairUp [one] = Left (getRange one, NotAllCasesHaveCond)
  pairUp [] = Right []

  parseExprWithRange : TermExpr -> Result (Range, Expr)
  parseExprWithRange term = do
    res <- parseExpr term
    pure (getRange term, res)

  parseExpr : TermExpr -> Result Expr

  parseExpr (TList range ((TId r_ "do") :: tl)) =
    pure $ EDo range !(traverse parseExpr tl)

  parseExpr (TList range ((TId r_ "case") :: cond :: cases)) = do
    cond <- parseExpr cond
    pairs <- pairUp cases
    pure $ ECase range cond pairs

  parseExpr (TList range (TId r_ "fn" :: hd :: tl)) = do
    arg  <- unwrapId hd >>= uncurry parseUniqueId
    body <- traverse parseExpr tl
    pure $ ELambda range arg (EDo range body)

  parseExpr (TList range [TId r_ "let", TId nameRange name, value, expr]) = do
    name <- parseUniqueId nameRange name
    val <- parseExpr value
    expr <- parseExpr expr
    pure $ ELet range name val expr

  parseExpr (TList range (fst :: params)) = do
    fstP  <- parseExpr fst
    body <- traverse (parseExprWithRange) params
    let result = foldl (\acc => \(range, expr) => ECall range acc expr) fstP body
    pure $ result

  parseExpr (TId range name) = EId <$> parsePath range name
  parseExpr expr@(TInt range n) = (ELit range) <$> (parseLiteral expr)
  parseExpr expr@(TStr range n) = (ELit range) <$> (parseLiteral expr)

  parseExpr expr = Left $ (getRange expr, InvalidExpr)

-- Data def

parseDataField : TermExpr -> Result (Name, List Types)
parseDataField (TList range (TId ranged name :: typed)) = do
    named <- parseCapitalized ranged name
    typed <- traverse parseTypes typed
    pure $ (named, typed)

parseDataField (TId range name) = (\t => (t, [])) <$> parseCapitalized range name
parseDataField expr = Left (getRange expr, ExpectedDataField)

parseDataDef : Range -> List TermExpr -> Result DataDef
parseDataDef range (typeDef :: fields) = do
  (name, types) <- parseTypeDef typeDef
  fields <- traverse parseDataField fields
  pure $ DefData name types fields

parseDataDef range expr = Left $ (range, InvalidTopLevel "data")

-- Def

parseDef : Range -> List TermExpr -> Result Def
parseDef range [TId nameRange name, type, body] = do
  named <- parseUniqueId nameRange name
  kind <- parseTypes type
  value <- parseExpr body
  pure $ (Define named (Just kind) value)

parseDef range [TId nameRange name, body] = do
  named <- parseUniqueId nameRange name
  value <- parseExpr body
  pure $ (Define named Nothing value)

parseDef range n = Left (range, InvalidTopLevel "def")

-- Defn

parseDefFn : Range -> List TermExpr -> Result Def

parseDefFn range [TId nameRange name, body] = do
  named <- parseUniqueId nameRange name
  value <- parseExpr body
  pure $ (Define named Nothing value)

-- TODO: Improve to not duplicate this shit
parseDefFn range ((TId nameRange name) :: type :: (TList argRange (TId r "list" :: args)) :: body) = do
  named <- parseUniqueId nameRange name
  kind <- parseTypes type
  bodyRes <- (EDo range) <$> traverse parseExpr body
  unwrapIds <- traverse (unwrapId) args
  args <- traverse (uncurry parseUniqueId) unwrapIds
  let lambda = foldl (\acc, cur => ELambda range cur acc) (bodyRes) (reverse args)
  pure $ (Define named (Just kind) lambda)

parseDefFn range ((TId nameRange name) :: (TList argRange (TId r "list" :: args)) :: body) = do
  named <- parseUniqueId nameRange name
  bodyRes <- (EDo range) <$> traverse parseExpr body
  unwrapIds <- traverse (unwrapId) args
  args <- traverse (uncurry parseUniqueId) unwrapIds
  let lambda = foldl (\acc, cur => ELambda range cur acc) (bodyRes) (reverse args)
  pure $ (Define named Nothing lambda)

parseDefFn range n = Left (range, InvalidTopLevel "defn")

parseRecordField : TermExpr -> Result (Name, Types)
parseRecordField (TList range [TId ranged name, typed]) = do
    named <- parseUniqueId ranged name
    typed <- parseTypes typed
    pure $ (named, typed)

parseRecordField expr = Left (getRange expr, NotAValidRecordField)

parseRecord : Range -> List TermExpr -> Result RecordDef
parseRecord range (typeDef :: fields) = do
  (name, types) <- parseTypeDef typeDef
  fields <- traverse parseRecordField fields
  pure $ DefRecord name types fields

parseRecord range expr = Left (range, InvalidTopLevel "record")

parseTopLevel : TermExpr -> Program -> Result Program
parseTopLevel expr program =
  case expr of
      TList range (TId dataName name :: tl) =>
        case name of
          "data" => do
            res <- parseDataDef range tl
            pure $ (record { dataDefs $= ((::) res) } program)
          "defn" => do
            res <- parseDefFn range tl
            pure $ (record { defs $= ((::) res) } program)
          "def" => do
            res <- parseDef range tl
            pure $ (record { defs $= ((::) res) } program)
          "record" => do
            res <- parseRecord range tl
            pure $ (record { recordDef $= ((::) res) } program)
          name => Left $ (dataName, InvalidTopLevel name)
      other => Left $ (getRange expr, Unreachable)

public export
parseProgram : String -> List TermExpr -> Either ErrorType Program
parseProgram name exprs =
  let program = MkProgram name [] [] [] in
  let res = foldl (\program, cur => program >>= (parseTopLevel cur)) (Right program) exprs in
  case res of
    Left (range, err) => Left $ ParsingError range err
    Right res => Right res

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module ErrorHandlingInterpreter

%default total

data Expr = Var String
          | Val Int
          | Add Expr Expr

data Eval : Type -> Type where
  MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch s = MkEval (\e => fetchVal e) where
  fetchVal : List (String, a) -> Maybe a
  fetchVal [] = Nothing
  fetchVal ((v, val) :: xs) = if v == s
                                 then (Just val)
                                 else (fetchVal xs)

Functor Eval where
  -- map : (a -> b) -> Eval a -> Eval b
  map f (MkEval g) = MkEval (\x => map f (g x))

Applicative Eval where
  -- pure : Eval a
  pure x = MkEval (\e => Just x)

  -- (<*>) : Eval (a -> b) -> Eval a -> Eval b
  (MkEval f) <*> (MkEval g) = MkEval (\x => app (f x) (g x)) where
    app : Maybe (a -> b) -> Maybe a -> Maybe b
    app (Just fx) (Just gx) = Just (fx gx)
    app _ _ = Nothing

{-
eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val n) = pure n
eval (Add x y) = pure (+) <*> eval x <*> eval y
-}

eval : Expr -> Eval Int
eval (Var x) = fetch x
eval (Val n) = [| n |]
eval (Add x y) = [| eval x + eval y |]

runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
                     MkEval envFn => envFn env


text:
module SmallStepStackMachine

import Expr
import Logic
import Maps
import SmallStepExpr

%access public export

%default total

data SInstr : Type where
  SPush : (n : Nat) -> SInstr
  SLoad : (x : Id) -> SInstr
  SPlus : SInstr
  SMinus : SInstr
  SMult : SInstr

Stack : Type
Stack = List Nat

Prog : Type
Prog = List SInstr

data StackStep : State -> (Prog, Stack) -> (Prog, Stack) -> Type where
  SS_Push : StackStep st (SPush n :: p', stk) (p', n :: stk)
  SS_Load : StackStep st (SLoad x :: p', stk) (p', st x :: stk)
  SS_Plus : StackStep st (SPlus :: p', n :: m :: stk) (p', m + n :: stk)
  SS_Minus : StackStep st (SMinus :: p', n :: m :: stk) (p', minus m n :: stk)
  SS_Mult : StackStep st (SMult :: p', n :: m :: stk) (p', m * n :: stk)

stack_deterministic : Deterministic (StackStep st)
stack_deterministic SS_Push SS_Push = Refl
stack_deterministic SS_Load SS_Load = Refl
stack_deterministic SS_Plus SS_Plus = Refl
stack_deterministic SS_Minus SS_Minus = Refl
stack_deterministic SS_Mult SS_Mult = Refl

StackMultiStep : (st : State) -> Relation (Prog, Stack)
StackMultiStep st = Multi (StackStep st)

s_compile : (e : AExp) -> Prog
s_compile (ANum k) = [SPush k]
s_compile (AId x) = [SLoad x]
s_compile (APlus x y) = s_compile x ++ s_compile y ++ [SPlus]
s_compile (AMinus x y) = s_compile x ++ s_compile y ++ [SMinus]
s_compile (AMult x y) = s_compile x ++ s_compile y ++ [SMult]

compiler_is_correct : AStep st e (ANum n) ->
                      Multi (StackStep st) (s_compile e, stk) ([], n :: stk)
compiler_is_correct AS_Id = MultiStep SS_Load MultiRefl
compiler_is_correct AS_Plus =
  MultiStep SS_Push $
  MultiStep SS_Push $
  MultiStep SS_Plus $
  MultiRefl
compiler_is_correct AS_Minus =
  MultiStep SS_Push $
  MultiStep SS_Push $
  MultiStep SS_Minus $
  MultiRefl
compiler_is_correct AS_Mult =
  MultiStep SS_Push $
  MultiStep SS_Push $
  MultiStep SS_Mult $
  MultiRefl


text:
import System.Concurrency

-- Simple producing thread.
producer : Channel Nat -> IO ()
producer c = ignore $ for [1..100] $ \n => channelPut c n

-- Test that using the same channel with multiple producers is okay.
main : IO ()
main =
  do c <- makeChannel
     tids <- for [1..10] $ \_ => fork (producer c)
     vals <- for [1..1000] $ \_ => channelGet c
     ignore $ traverse (\t => threadWait t) tids
     let s = sum vals
     if s == 50500
        then putStrLn "Success!"
        else putStrLn "How did we get here?"


text:
module Ch05.Exercise_5_2_3

import Ch05.LambdaCalculus

%default total

||| Alternative (more concise) way to define multiplication of Church numerals
times' : Term
times' = Abs 0 (Abs 1 ((Var 0) . (Var 1)))


text:
module Algebra.Solver.Ring

import public Algebra.Ring
import public Algebra.Solver.Ring.Expr
import public Algebra.Solver.Ring.Prod
import public Algebra.Solver.Ring.SolvableRing
import public Algebra.Solver.Ring.Sum

%default total


text:
module Prob

import Marginalization
import Semiring
import HetVect

%default total
%access public export

-- TODO: convert to haskell, parallel, prove

mutual
  ||| Probability monad which keeps a list of the variables it contains
  ||| Prob s xs a = probability of `a`, given `xs`. `s` is the unit
  data Prob : Type -> Type -> Type where
    ||| change to (forall s. Semiring s => (a -> s) -> s) in order to avoid enum,
    ||| bounded constraints (maybe).
    Dst : (a -> s) -> Prob s a
    Bnd
      : {xs : List Type}
      -> {auto finite : AllFinite xs}
      -> MultiProb s xs
      -> (Vect xs -> Prob s b)
      -> Prob s b

  data MultiProb : Type -> List Type -> Type where
    Nil  : MultiProb s []
    (::) : {x : Type} -> Prob s x -> MultiProb s xs -> MultiProb s (x :: xs)

getProb : Semiring s => Prob s a -> a -> s
getProb (Dst f) = f
getProb (Bnd {xs} ps f) = \y => margVec (\ws => allMessages ws * getProb (f ws) y) where

  funcs : Semiring s => {ys : List Type} -> MultiProb s ys -> s -> Vect ys -> s
  funcs [] = \n, _ => n
  funcs (p::ps) =
    let m  = getProb p
        ms = funcs ps
    in \n, (v::vs) => ms (n * m v) vs -- change to not tail-recursive to make parallel

  allMessages : Vect xs -> s
  allMessages = funcs ps one

getProbPar : Semiring s => Prob s a -> a -> s
getProbPar (Dst f) = f
getProbPar (Bnd {xs} ps f) = \y => margVec (\ws => allMessages ws * getProb (f ws) y) where

  funcs : Semiring s => {ys : List Type} -> MultiProb s ys -> Vect ys -> s
  funcs [] = \_ => one
  funcs (p::ps) = \(v::vs) =>
    let m  = getProbPar p v -- Evaluate these in parallel (only currently possible in Haskell)
        ms = funcs ps vs
    in ms * m

  allMessages : Vect xs -> s
  allMessages = funcs ps

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module Control.Algebra.Implementations

import Control.Algebra

-- This file is for algebra implementations with nowhere else to go.

%default total

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

Semigroup (ty -> ty) where
  (<+>) = (.)

SemigroupV (ty -> ty) where
  semigroupOpIsAssociative _ _ _ = Refl

Monoid (ty -> ty) where
  neutral = id

MonoidV (ty -> ty) where
  monoidNeutralIsNeutralL _ = Refl
  monoidNeutralIsNeutralR _ = Refl


text:
import Control.ST
import Data.Bits

record DecoderState where
    constructor MkDecoderState
    byteIndex : Int
    buffer : String

indexB64 : String -> Int -> Bits 64
indexB64 s i = intToBits $ fromInteger $ cast $ ord $ strIndex s i

startDecode : String -> STrans m Var res (\lbl => (lbl ::: State DecoderState) :: res)
startDecode buf = new $ MkDecoderState 0 buf

decDropNone : Var -> Resources -> Maybe (Bits 64) -> Resources
decDropNone _dec res Nothing = res
decDropNone dec res (Just _) = (dec ::: State DecoderState) :: res

getByte : (dec : Var) -> STrans m (Maybe (Bits 64))
    ((dec ::: State DecoderState) :: res)
    (decDropNone dec res)
getByte dec = do
    state <- read dec
    if length (buffer state) <= toNat (byteIndex state)
        then do
            delete dec
            pure Nothing
        else do
            write dec (record { byteIndex $= (+1) } state)
            let byte = buffer state `indexB64` byteIndex state
            pure (Just byte)

getVInt' : Nat -> (dec : Var) -> STrans m (Maybe (Bits 64))
    ((dec ::: State DecoderState) :: res)
    (decDropNone dec res)
getVInt' Z _ = pure (Just (intToBits 0))
getVInt' (S k) dec = case !(getByte dec) of
    Nothing => pure Nothing
    Just byte =>
        if byte < intToBits 128
           then pure (Just byte)
           else do case !(getVInt' k dec) of
                          Nothing => pure Nothing
                          Just rest => pure $ Just $
                               (byte `and` intToBits 127) `or` (rest `shiftLeft` intToBits 7)

getVInt : (dec : Var) -> STrans m (Maybe (Bits 64))
    ((dec ::: State DecoderState) :: res)
    (decDropNone dec res)
getVInt = getVInt' 8

max_stars_repo_name: zenhack/idris-protobufs

max_issues_repo_name: zenhack/idris-protobufs

max_forks_repo_name: zenhack/idris-protobufs