text:
module Ex4_1

import Data.Strings
import Data.Vect
import System.REPL

data DataStore : Type where
  MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : (store : DataStore) -> Nat
size (MkData size' _) = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData _ items') = items'

addToStore : (store : DataStore) -> (item : String) -> DataStore
addToStore (MkData size items) newItem = MkData _ (addToData items)
  where
    addToData : (items : Vect old String) -> Vect (S old) String
    addToData [] = [newItem]
    addToData (item :: items) = item :: addToData items

searchStore : (store : DataStore) -> (word : String) -> String
searchStore (MkData _ items) word = searchHelper items 0 word ""
  where
    searchHelper : Vect n String -> (idx : Nat) -> (word : String) -> (results : String) -> String
    searchHelper [] idx word results = results
    searchHelper (item :: items) idx word results =
      case isInfixOf word item of
           True => searchHelper items (idx + 1) word (results ++ show (idx + 1) ++ " " ++ item ++ "\n")
           False => searchHelper items (idx + 1)  word results

empty : DataStore
empty = MkData 0 []

data Command = Add String
             | Get Integer
             | Size
             | Search String
             | Quit

processCommand : (store : DataStore) -> (cmd : Command) -> Maybe (String, DataStore)
processCommand store (Add str) = Just ("ID" ++ show (size store) ++ "\n", addToStore store str)
processCommand store (Get idx) = case integerToFin idx (size store) of
                                Nothing => Just ("Invalid index: " ++ show idx ++ "\n", store)
                                Just pos => Just (index pos (items store) ++ "\n", store)
processCommand store (Search str) = Just (searchStore store str ++ "\n", store)
processCommand store Size = Just ("Number of items: " ++ show (size store) ++ "\n", store)
processCommand store Quit = Nothing

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" idxStr = case all isDigit (unpack idxStr) of
                              False => Nothing
                              True => Just (Get (cast idxStr))
parseCommand "search" str = Just (Search str)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _  = Nothing

parse : String -> Maybe Command
parse inp = let (cmd, args) = span (/= ' ') inp in
                parseCommand cmd (ltrim args)

processInput : (store : DataStore) -> String -> Maybe (String, DataStore)
processInput store inp =
  case parse inp of
       Nothing => Just ("Invalid command\n", store)
       Just cmd => processCommand store cmd

main : IO ()
main = replWith empty "Command: " processInput

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
import Data.Vect

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

my_reverse : Vect n elem -> Vect n elem
my_reverse [] = []
my_reverse (x :: xs) = reverseProof (my_reverse xs ++ [x])
  where
    reverseProof : Vect (plus k 1) elem -> Vect (S k) elem
    reverseProof {k} result = rewrite my_plusCommutes 1 k in result

my_reverse' : Vect n elem -> Vect n elem
my_reverse' xs = reverse' [] xs
  where
    reverseProof_nil : Vect n1 a -> Vect (plus n1 0) a
    reverseProof_nil {n1} acc = rewrite plusZeroRightNeutral n1 in acc

    reverseProof_xs : Vect ((S n) + k) a -> Vect (plus n (S k)) a
    reverseProof_xs {n} {k} xs = rewrite sym (plusSuccRightSucc n k) in xs

    reverse' : Vect n a -> Vect m a -> Vect (n + m) a
    reverse' acc [] = reverseProof_nil acc
    reverse' acc (x::xs) = reverseProof_xs (reverse' (x::acc) xs)

ext: idr

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:
module RnaTranscription

import Data.Vect

%access export
%default total

namespace DnaStrand
  public export
  data DnaStrand = A | C | T | G

implementation Eq DnaStrand where
  (==) A A = True
  (==) C C = True
  (==) T T = True
  (==) G G = True
  (==) _ _ = False

namespace RnaStrand
  public export
  data RnaStrand = A | C | G | U

implementation Eq RnaStrand where
  (==) A A = True
  (==) C C = True
  (==) G G = True
  (==) U U = True
  (==) _ _ = False

toRna : Vect n DnaStrand -> Vect n RnaStrand
toRna [] = []
toRna (A :: xs) = U :: toRna xs
toRna (C :: xs) = G :: toRna xs
toRna (T :: xs) = A :: toRna xs
toRna (G :: xs) = C :: toRna xs


text:
module Utils.Octal

import Data.Primitives.Views

%default total

octDigit : Int -> Char
octDigit 0 = '0'
octDigit 1 = '1'
octDigit 2 = '2'
octDigit 3 = '3'
octDigit 4 = '4'
octDigit 5 = '5'
octDigit 6 = '6'
octDigit 7 = '7'
octDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below

||| Convert a positive integer into a list of octal characters
export
asOct : Int -> String
asOct n = pack $ asOct' n []
  where
    asOct' : Int -> List Char -> List Char
    asOct' 0 oct = oct
    asOct' n oct with (n `divides` 8)
      asOct' (8 * div + rem) oct | DivBy div rem _ =
        assert_total $ asOct' div (octDigit rem :: oct)

export
fromOctDigit : Char -> Maybe Int
fromOctDigit '0' = Just 0
fromOctDigit '1' = Just 1
fromOctDigit '2' = Just 2
fromOctDigit '3' = Just 3
fromOctDigit '4' = Just 4
fromOctDigit '5' = Just 5
fromOctDigit '6' = Just 6
fromOctDigit '7' = Just 7
fromOctDigit _ = Nothing

export
fromOctChars : List Char -> Maybe Int
fromOctChars = fromOctChars' 1
  where
    fromOctChars' : Int -> List Char -> Maybe Int
    fromOctChars' _ [] = Just 0
    fromOctChars' m (d :: ds) = pure $ !(fromOctDigit (toLower d)) * m + !(fromOctChars' (m*8) ds)

export
fromOct : String -> Maybe Int
fromOct = fromOctChars . unpack


text:
module Js.DOM.Element

import Js.Object

%default total
%access export

public export
data Element = MkElement Ptr

Class Element where
    ptr (MkElement p) = p

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module Data.Functor.Compose

%access public export

-- | `Compose f g` is the composition of the two functors `f` and `g`.
data Compose : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  MkCompose : f (g a) -> Compose f g a

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

bihoistCompose : (Functor f, Functor g, Functor h, Functor i) =>
                 ({a : Type} -> f a -> h a) ->
                 ({a : Type} -> g a -> i a) ->
                 ({a : Type} -> Compose f g a -> Compose h i a)
bihoistCompose natF natG (MkCompose fga) = MkCompose (natF (map natG fga))

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

Eq (f (g a)) => Eq (Compose f g a) where
  (MkCompose x) == (MkCompose y) = x == y

Ord (f (g a)) => Ord (Compose f g a) where
  compare (MkCompose x) (MkCompose y) = compare x y

Show (f (g a)) => Show (Compose f g a) where
  show (MkCompose x) = "Compose (" <+> show x <+> ")"

(Functor f, Functor g) => Functor (Compose f g) where
  map f (MkCompose fga) = MkCompose $ map f <$> fga

(Applicative f, Applicative g) => Applicative (Compose f g) where
  pure = MkCompose . pure . pure
  (MkCompose x) <*> (MkCompose y) = MkCompose $ map (<*>) x <*> y

(Foldable f, Foldable g) => Foldable (Compose f g) where
  foldr f init (MkCompose fga) = foldr (flip (foldr f)) init fga
  foldl f init (MkCompose fga) = foldl (foldl f) init fga

(Traversable f, Traversable g) => Traversable (Compose f g) where
  traverse f (MkCompose fga) = map MkCompose $ traverse (traverse f) fga

(Alternative f, Applicative g) => Alternative (Compose f g) where
  empty = MkCompose empty
  (MkCompose x) <|> (MkCompose y) = MkCompose (x <|> y)

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 Equal

-- Equality type

data Equal : x -> y -> Type where
  Reflexive : Equal a a

-- Simple examples

bool : Equal Bool Bool
bool = Reflexive

true : Equal True True
true = Reflexive

two : Equal 2 (1 + 1)
two = Reflexive

-- Helpers

transitive : Equal a b -> Equal b c -> Equal a c
transitive Reflexive Reflexive = Reflexive

symmetric : Equal a b -> Equal b a
symmetric Reflexive = Reflexive

congruent : (f : t -> x) -> Equal a b -> Equal (f a) (f b)
congruent f Reflexive = Reflexive

-- Stepping it up

plusZero : (n : Nat) -> Equal (plus n Z) n
plusZero Z = the (Equal Z Z) Reflexive
plusZero (S k) =
  let induction = plusZero k
  in congruent S induction

-- Built-in equality

plusZero' : (n : Nat) -> plus n Z = n
plusZero' Z = Refl
plusZero' (S k) =
  let induction = plusZero' k
  in ?plusZero'_2

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

Equal.plusZero'_2 = proof
  intros
  rewrite induction
  trivial


text:
module Main

import IdrisScript
import IdrisScript.RegExps
import IdrisScript.Arrays

main : JS_IO ()
main = do
  args  <- with Arrays empty
  args `push` (toJS {to=JSString} "Pinkie Pie")
  args `push` (toJS {to=JSString} "g")

  regex <- new !RegExp args

  let text = "Pinkie Pie is best pony!"

  case regex of
       ("RegExp" ** r) => putStrLn !(replace text r "Rainbow Dash")
       _               => putStrLn "Whoops"

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Erlang.Debug

import Erlang

%default total

||| Print the underlying value using `io:format/2`.
export
erlPrintLn : HasIO io => a -> io ()
erlPrintLn x = do
  pure $ erlUnsafeCall ErlTerm "io" "format" ["~p~n", the (ErlList _) [MkRaw x]]
  pure ()

||| Print the underlying value using `io:format/2`, and return the given value.
|||
||| This function is unsafe as it breaks referential transparency.
export
erlInspect : a -> a
erlInspect x = unsafePerformIO $ do
  erlPrintLn x
  pure x


text:
average : String -> Double
average str =
  let num_words = word_count str
      total_length = sum (word_lengths (words str))
  in cast total_length / cast num_words

  where
    word_count : String -> Nat
    word_count str = length (words str)

    word_lengths : List String -> List Nat
    word_lengths strs = map length strs

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

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


text:
module Unit

import Basic

%default total

public export
data Unit : Type where
  MkUnit : Unit

public export
UnitInduction : (p : Unit -> Type) -> p () -> (x : Unit) -> p x
UnitInduction _ prop () = prop

public export
UnitRecursion : (p : Type) -> p -> Unit -> p
UnitRecursion _ p () = p

public export
UnitTerminal : (p : Type) -> p -> Unit
UnitTerminal _ = const ()


text:
%inline %noinline
foo : Int -> Int
foo x = x


text:
module Control.Indexed

import public Control.Functor.Indexed
import public Control.Applicative.Indexed
import public Control.Monad.Indexed
import public Control.Monad.Indexed.Do

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
foo : String
foo = "λx→x"

bar : String
bar = "λx→x"

baz : Char
baz = 'λ'

quux : String
quux = "\x0a\x80\xC9\xFF\n3\n4"

appMany : Nat -> String
appMany Z = foo
appMany (S k) = bar ++ appMany k

main : IO ()
main = do putStrLn foo
          putStrLn (foo ++ bar)
          putStrLn (reverse (foo ++ bar))
          printLn (length foo)
          printLn baz
          printLn (strCons '\x141' "")
          printLn (singleton (chr 0x141))
          let x = 4
          let newstr = appMany (toNat x)
          putStrLn newstr
          printLn (strHead newstr)
          printLn (length newstr)
          printLn (strIndex newstr 4)
          putStrLn (strCons (strIndex newstr 4) "")
          putStrLn ("Tail: " ++ strTail newstr)
          putStrLn ("Tail Tail: " ++ strTail (strTail newstr))
          putStrLn ("Cons: " ++ strCons 'λ' newstr)
          putStrLn ("Reverse: " ++ reverse newstr)
          printLn [1..5]
          printLn [5..1]
          printLn [(-9), (-7)..(-1)]
          printLn [17,15..1]
          printLn [19,15..2]
          printLn [-2,0..4]
          printLn [1,0..-2]
          printLn [3,5..3]
          printLn [2,1..2]
          printLn [4,1..3]
          printLn [1,4..2]
          printLn [3,5..1]
          printLn [4,1..5]
          printLn [1,1..2]
          printLn [2,2..1]
          printLn $ the (List Nat) [1..5]
          printLn $ the (List Nat) [5..1]
          printLn $ the (List Nat) [5,4..1]
          printLn $ the (List Nat) [1,3..5]
          printLn $ the (List Nat) [5,3..1]
          printLn $ the (List Nat) [3,5..3]
          printLn $ the (List Nat) [2,1..2]
          printLn $ the (List Nat) [4,1..3]
          printLn $ the (List Nat) [1,4..2]
          printLn $ the (List Nat) [3,5..1]
          printLn $ the (List Nat) [4,1..5]
          printLn $ the (List Nat) [1,1..2]
          printLn $ the (List Nat) [2,2..1]
          printLn $ the (List Int) [(-1)..(-5)]
          printLn $ the (List Int) [-2,0..4]
          printLn $ the (List Int) [1,0..-2]
          printLn $ the (List Int) [3,5..3]
          printLn $ the (List Int) [2,1..2]
          printLn $ the (List Int) [4,1..3]
          printLn $ the (List Int) [1,4..2]
          printLn $ the (List Int) [3,5..1]
          printLn $ the (List Int) [4,1..5]
          printLn $ the (List Int) [1,1..2]
          printLn $ the (List Int) [2,2..1]
          printLn ['z'..'x']
          printLn ['g','e'..'a']
          printLn ['x'..'z']
          printLn ['a','c'..'g']

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

import Effects
import Effect.File
import Effect.StdIO

data Test : Type where

readFile : { [Test ::: FILE_IO (OpenFile Read), STDIO] } EffM IO ()
readFile = if !(Test :- eof) then return ()
              else do putStrLn !(Test :- readLine)
                      readFile

read : String -> { [Test ::: FILE_IO (), STDIO] } EffM IO ()
read f = do case !(Test :- open f Read) of
                 False => return ()
                 True => do readFile
                            Test :- close

main : IO ()
main = run [Test := (), ()] (read "test")

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Maybe
import Control.Monad.Trans

%default total
%access public export

record MaybeT (m : Type -> Type) (a : Type) where
  constructor MT
  runMaybeT :  m (Maybe a)

Functor f => Functor (MaybeT f) where
    map f (MT g) = MT (map (map f) g)

Monad f => Applicative (MaybeT f) where
    pure x = MT (pure (Just x))

    (MT f) <*> (MT a) = MT (do g <- f
                               case g of
                                 Just h  => map (map h) a
                                 Nothing => pure Nothing)

Monad f => Alternative (MaybeT f) where
    empty = MT (pure Nothing)
    (MT a) <|> (MT b) = MT (do a' <- a
                               case a' of
                                 Just a'' => pure (Just a'')
                                 _        => b)

MonadTrans MaybeT where
    lift x = MT (map Just x)

Monad f => Monad (MaybeT f) where
    (MT f) >>= k = MT (do g <- f
                          case g of
                            Just a  => runMaybeT (k a)
                            Nothing => (pure Nothing))

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


text:
module Main

main : IO ()
main = do
     putStr "Enter thy name: "
     x <- getLine
     putStrLn ("Howdy " ++ x)

printLen : IO ()
printLen = getLine >>= putStr . show . length

printLonger : IO ()
printLonger = do
            putStr "First string: "
            a <- getLine
            putStr "2nd string: "
            b <- getLine
            print $ if length a > length b then length a else length b

pL : IO ()
pL = putStr "1st: " >>= \_ => getLine >>= \a => putStr "2nd: " >>= \_ => getLine >>= \b => print $ if length a > length b then length a else length b


text:
module Effect.Glfw

import Effects
import public Graphics.Util.Glfw

%access public export

data GlfwMode : Type where
  On : GlfwMode

data Glfw : Effect where
  ||| initialises Glfw
  Initialise : sig Glfw Bool () (\res => if res then GlfwMode else ())
  WithGlfw : (GlfwMode -> IO a)
               -> sig Glfw a GlfwMode (\w => GlfwMode)
  Terminate : sig Glfw () GlfwMode ()

implementation Handler Glfw IO where
  handle () Initialise    k = do ret <- glfwInit
                                 if ret then k True On
                                        else k False ()
  handle On (WithGlfw f)  k = do r <- f On; k r On
  handle On Terminate     k = do glfwTerminate; k () ()

GLFW : Type -> EFFECT
GLFW res = MkEff res Glfw

GLFW_ON : EFFECT
GLFW_ON = GLFW GlfwMode

initialise : { [GLFW ()] ==> {res} [GLFW (if res then GlfwMode else ())] } Eff Bool
initialise = call Initialise

terminate : { [GLFW_ON] ==> [GLFW ()] } Eff ()
terminate = call Terminate

swapInterval : Nat -> { [GLFW_ON] } Eff ()
swapInterval n = call $ WithGlfw (\_ => glfwSwapInterval (toIntNat n))

windowHint : GlfwFlags -> Int -> { [GLFW_ON] } Eff ()
windowHint flag i = call $ WithGlfw (\_ => glfwWindowHint flag i)

data GlfwWindowEff : Effect where
  ||| creates a Glfw window
  CreateWindow : (title: String)
                 -> (width: Int)
                 -> (height: Int)
                 -> sig GlfwWindowEff Bool () (\res => if res then GlfwWindow else ())
  Poll : sig GlfwWindowEff () GlfwWindow GlfwWindow
  WithWindow : (GlfwWindow -> IO a)
               -> sig GlfwWindowEff a GlfwWindow (\w => GlfwWindow)
  DestroyWindow : sig GlfwWindowEff () GlfwWindow ()

GLFW_WINDOW : Type -> EFFECT
GLFW_WINDOW res = MkEff res GlfwWindowEff

GLFW_WINDOW_ON : EFFECT
GLFW_WINDOW_ON = GLFW_WINDOW GlfwWindow

implementation Handler GlfwWindowEff IO where
  handle () (CreateWindow title width height) k =
    do win <- glfwCreateWindow title width height defaultMonitor
       isNull <- isWindow win
       if isNull then k False ()
                 else k True win
  handle win Poll            k = do glfwPollEvents; k () win
  handle win (WithWindow f)  k = do r <- f win; k r win
  handle win DestroyWindow   k = do glfwDestroyWindow win; k () ()

createWindow : String -> Int -> Int -> { [GLFW_WINDOW ()] ==> {res} [GLFW_WINDOW (if res then GlfwWindow else ())]} Eff Bool
createWindow title width height = call $ CreateWindow title width height

pollEvents :  { [GLFW_WINDOW_ON] } Eff ()
pollEvents = call Poll

makeContextCurrent : { [GLFW_WINDOW_ON] } Eff ()
makeContextCurrent = call $ WithWindow (\win => glfwMakeContextCurrent win)

swapBuffers : { [GLFW_WINDOW_ON] } Eff ()
swapBuffers = call $ WithWindow (\win => glfwSwapBuffers win)

getFunctionKey : FunctionKey -> { [GLFW_WINDOW_ON] } Eff KeyEventTy
getFunctionKey key = call $ WithWindow (\win => glfwGetFunctionKey win key)

getKey : Char -> { [GLFW_WINDOW_ON] } Eff KeyEventTy
getKey key = call $ WithWindow (\win => glfwGetKey win key)

setInputMode : GlfwFlags -> Int -> { [GLFW_WINDOW_ON] } Eff ()
setInputMode flag val = call $ WithWindow (\win => glfwSetInputMode win flag val)

shouldClose : { [GLFW_WINDOW_ON] } Eff Bool
shouldClose = call $ WithWindow (\win => glfwWindowShouldClose win)

destroyWindow : { [GLFW_WINDOW_ON] ==> [GLFW_WINDOW ()] } Eff ()
destroyWindow = call DestroyWindow

max_stars_repo_name: eckart/glfw-idris

max_issues_repo_name: eckart/glfw-idris

max_forks_repo_name: eckart/glfw-idris


text:
{- Copied straight from the book -}
module Part2.Sec6_2_2_printf

{- This one is like recursive enumeration -}
data Format = Number Format
             | Str Format
             | Lit String Format
             | End

{-  Nice recursive definition that ends up resolving to a long function returning String.
   This ends up being implementable with TypeFamilies and DataKinds (for Format) in Haskell. -}
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

{- CPS implemenation that still maps nicely to Haskell -}
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

{- No dependent typing here -}
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

{- Hah, so simple! Currently no such luck in Haskell -}
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module LightClick.Error

import Control.WellFounded
import Data.Vect
import Data.Fin
import Data.String
import Data.List
import Data.List.Views

import Toolkit.Data.Location
import Toolkit.Data.DVect

import LightClick.Types
import LightClick.Connection
import LightClick.Types.Compatibility

import LightClick.IR.Channel.Normalise.Error

%default total

export
interface PrettyError (type : Type) where
  toString : type -> String

export
PrettyError Direction.Valid.Error where
  toString InputCannotSend = "Input cannot send"
  toString DirIsSame = "Directions are the same"
  toString OutputCannotReceive = "Output ports cannot receive"

export
PrettyError Direction.Safe.Error where
  toString (VCError x) = toString x
  toString PossibleFeedbackFromReceiver = "Possible Feedback from Receiver."
  toString PossibleFeedbackFromSender = "Possible Feedback from Sender."

export
Show Wire where
   show Data      = "data"
   show Address   = "address"
   show Clock     = "clock"
   show Reset     = "reset"
   show Info      = "info"
   show Interrupt = "interrupt"
   show Control   = "control"
   show General   = "general"

export
PrettyError Compatibility.Wire.Error where
  toString (TypesDiffer a b)
    = unlines [ "Incompatible intentions:"
              , "\tExpected:"
              , "\t\t" <+> show a
              , "\tGiven:"
              , "\t\t" <+> show b
              ]

export
Show Sensitivity where
 show High        = "high"
 show Low         = "low"
 show Rising      = "rising"
 show Falling     = "falling"
 show Insensitive = "insensitive"

export
PrettyError (Sensitivity.Error) where
  toString NoChangeFromHigh
    = "Cannot go from High to a different level."
  toString NoChangeFromLow
    = "Cannot go from Low to a different level."
  toString NoChangeFromRising
    = "Cannot go from Rising to a different level."
  toString NoChangeFromFalling
    = "Cannot go from Falling to a different level."

namespace Compatibility

  namespace Data

    toString : (Data.Error) -> String
    toString Mismatch = "The data types are wildly different."
    toString MismatchArrayLength
      = "The arrays presented have different lengths."
    toString (MismatchArrayType x)
      = "The arrays presented have different types:\n" <+> toString x
    toString MismatchStructureLength
      = "The union/struct must have the same number of fields."
    toString (MismatchStructureFieldType pos err)
      = "The union/struct differs at position " <+> show pos <+> ". With Error:\n" <+> toString err
    toString (MismatchStructureFieldLabel pos x y)
      = "The labels differ at position " <+> show pos <+> ". With Error:\n" <+> show x <+> " & " <+> show y <+> "."

    export
    PrettyError (Data.Error ) where
      toString = Data.toString

  namespace Port

    export
    PrettyError Port.Error where

      toString (InCompatSensitivity err) = toString err
      toString (InCompatDirection   err) = toString err
      toString (InCompatWTypes      err) = toString err
      toString (InCompatDTypes      err) = toString err

namespace Types

  Show TyRig where
    show None = show 0
    show One  = show 1
    show Tonne = "*"

  mutual
    kvsToString : Vect n (Pair String (Ty DATA)) -> String
    kvsToString [] = ""
    kvsToString ((l, ty) :: xs)
      = unwords [l, ":", toString ty]

    ksToListString : DVect String (Ty . PORT) n ps -> String
    ksToListString [] = ""
    ksToListString (ex :: []) = Types.toString ex
    ksToListString (ex :: (x :: rest))
      = Types.toString ex <+> "," <+> ksToListString (x::rest)

    export
    toString : forall a . Ty a -> String
    toString TyLogic
     = "logic"
    toString (TyArray type length)
     = toString type <+> "[" <+> show length <+> "]"

    toString (TyStruct kvs)
      = "struct {" <+> kvsToString kvs <+> "}"

    toString (TyUnion kvs)
      = "union {" <+> kvsToString kvs <+> "}"

    toString TyUnit
      = "()"
    toString TyConn
      = "conn"

    toString TyGate
      = "gate"

    toString (TyPort label dir sense wty type usage)
      = unwords [ label
                , ":"
                , "port ("
                , show dir
                , show sense
                , show wty
                , toString type
                , show usage
                , ")"]

    toString (TyModule xs)
      = "module ( " <+> (ksToListString xs) <+> ")"

namespace LightClick

  public export
  data FanTy = FANIN | FANOUT

  public export
  data Error = Err FileContext String
             | NotSupposedToHappen (Maybe String)
             | MetaTypeMismatch FileContext MTy MTy
             | IdentifierNotFound FileContext String
             | IdentifierAlreadyExists FileContext String
             | LabelAlreadyExists FileContext String (List String)
             | InvalidModuleIndex FileContext String (Vect (S n) String)
             | MetaTypeConstructionError FileContext MTy MTy
             | PortInUse FileContext String
             | ConstantsNotAllowed FileContext
             | UnSafeDirectConnection FileContext Port.Error
             | UnSafeFan FileContext FanTy Nat Port.Error
             | UnSafeMuxCtrl FileContext Port.Error
             | NormalisationError Normalise.Error
             | UnusedPorts (List (String, List String))
             | Mismatch FileContext (Ty a) (Ty b)
             | Nest LightClick.Error LightClick.Error

  export
  PrettyError LightClick.Error where

    toString (Err loc msg) = unlines [show loc,msg]
    toString (NotSupposedToHappen Nothing)  = "Not Supposed to Happen."
    toString (NotSupposedToHappen (Just s)) = "Not Supposed to Happen. " <+> s
    toString (MetaTypeMismatch loc e g) =
        unlines [ show loc
                , "Type Mismatch:"
                , "\tExpected: " <+> show e
                , "\tGiven: " <+> show g]
    toString (IdentifierNotFound loc label) =
        unlines [ show loc
                , "Identifier " <+> show label <+> " not found."]
    toString (IdentifierAlreadyExists loc label) =
        unlines [ show loc
                , "Identifier " <+> show label <+> " already exists."]
    toString (LabelAlreadyExists loc label store) =
        unlines [ show loc
                , "The label " <+> show label <+> " already exists"
                , "It should *not* be one of: "
                , "\t" <+> show store]

    toString (InvalidModuleIndex loc label names) =
        unlines [ show loc
                , "The label " <+> show label <+> " is not a valid identifier."
                , "It should be one of: "
                , "\t" <+> show names]
    toString (MetaTypeConstructionError loc exp g) =
        unlines [ show loc
                , "Type Mismatch:"
                , "\tExpected: " <+> show' exp
                , "\tGiven: " <+> show g]
    toString (PortInUse loc s) =
        unlines [ show loc
                , "The port " <+> show s <+> " is already in use."]
    toString (ConstantsNotAllowed loc) =
        unlines [ show loc
                , "Constants are not allowed."
                ]

    toString (UnSafeDirectConnection loc msg) =
        unlines [ show loc
                , "Unsafe connection with " <+> toString msg
                ]

    toString (UnSafeFan loc ty idx msg) =
         unlines [ show loc
                 , "Unsafe " <+> case ty of {FANIN => "Fan-IN."; FANOUT => "Fan-OUT."}
                 , "Wire #" <+> show idx <+> " is unsafe:"
                 , "\t" <+> toString msg
                 ]

    toString (UnSafeMuxCtrl loc msg) =
        unlines [ show loc
                , "Mux control wire is unsafe :"
                , "\t" <+> toString msg
                ]
    toString (NormalisationError err) =
        unlines ["Normalisation Error:"
                , show err
                ]

    toString (UnusedPorts Nil) = "Not supposed to happen: Unused port error is empty."
    toString (UnusedPorts ((n,ps)::Nil)) =
        unlines ["Unused port:"
                , "\t - " <+> (unwords [n, show ps])
                ]
    toString (UnusedPorts (p'::ps)) =
        unlines $ "Unused ports:" :: (map (\(n,ns) => "\t - " <+> (unwords [n, show ns])) (p'::ps))

    toString (Mismatch loc e g) =
        unlines [ show loc
                , "Connection mismatch when trying to connect:"
                , "\tthis:\n\t\t" <+> toString e
                , "\tthat:\n\t\t" <+> toString g]

    toString (Nest x y)
      = unlines [toString x, "Specifically:", toString y]

  export
  Show LightClick.Error where
    show = (trim . toString)

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Idris.IDEMode.Commands

import Core.Core
import Core.Context
import Core.Context.Log
import Core.Name
import public Idris.REPL.Opts
import Libraries.Utils.Hex

import System.File

%default total

public export
data SExp = SExpList (List SExp)
          | StringAtom String
          | BoolAtom Bool
          | IntegerAtom Integer
          | SymbolAtom String

public export
data DocMode = Overview | Full

public export
data IDECommand
     = Interpret String
     | LoadFile String (Maybe Integer)
     | TypeOf String (Maybe (Integer, Integer))
     | NameAt String (Maybe (Integer, Integer))
     | CaseSplit Integer Integer String
     | AddClause Integer String
     -- deprecated: | AddProofClause
     | AddMissing Integer String
     | ExprSearch Integer String (List String) Bool
     | ExprSearchNext
     | GenerateDef Integer String
     | GenerateDefNext
     | MakeLemma Integer String
     | MakeCase Integer String
     | MakeWith Integer String
     | DocsFor String (Maybe DocMode)
     | Directive String
     | Apropos String
     | Metavariables Integer
     | WhoCalls String
     | CallsWho String
     | BrowseNamespace String
     | NormaliseTerm     String -- TODO: implement a Binary lib
     | ShowTermImplicits String -- and implement Binary (Term)
     | HideTermImplicits String -- for these four defintions,
     | ElaborateTerm     String -- then change String to Term, as in idris1
     | PrintDefinition String
     | ReplCompletions String
     | EnableSyntax Bool
     | Version
     | GetOptions

readHints : List SExp -> Maybe (List String)
readHints [] = Just []
readHints (StringAtom s :: rest)
    = do rest' <- readHints rest
         pure (s :: rest')
readHints _ = Nothing

export
getIDECommand : SExp -> Maybe IDECommand
getIDECommand (SExpList [SymbolAtom "interpret", StringAtom cmd])
    = Just $ Interpret cmd
getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname])
    = Just $ LoadFile fname Nothing
getIDECommand (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom l])
    = Just $ LoadFile fname (Just l)
getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n])
    = Just $ TypeOf n Nothing
getIDECommand (SExpList [SymbolAtom "type-of", StringAtom n,
                         IntegerAtom l, IntegerAtom c])
    = Just $ TypeOf n (Just (l, c))
getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n])
    = Just $ NameAt n Nothing
getIDECommand (SExpList [SymbolAtom "name-at", StringAtom n,
                         IntegerAtom l, IntegerAtom c])
    = Just $ NameAt n (Just (l, c))
getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, IntegerAtom c,
                         StringAtom n])
    = Just $ CaseSplit l c n
getIDECommand (SExpList [SymbolAtom "case-split", IntegerAtom l, StringAtom n])
    = Just $ CaseSplit l 0 n
getIDECommand (SExpList [SymbolAtom "add-clause", IntegerAtom l, StringAtom n])
    = Just $ AddClause l n
getIDECommand (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
    = Just $ AddMissing line n
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n])
    = Just $ ExprSearch l n [] False
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, SExpList hs])
    = (\hs' => ExprSearch l n hs' False) <$> readHints hs
getIDECommand (SExpList [SymbolAtom "proof-search", IntegerAtom l, StringAtom n, SExpList hs, SymbolAtom mode])
    = (\hs' => ExprSearch l n hs' (getMode mode)) <$> readHints hs
  where
    getMode : String -> Bool
    getMode m = m == "all"
getIDECommand (SymbolAtom "proof-search-next") = Just ExprSearchNext
getIDECommand (SExpList [SymbolAtom "generate-def", IntegerAtom l, StringAtom n])
    = Just $ GenerateDef l n
getIDECommand (SymbolAtom "generate-def-next") = Just GenerateDefNext
getIDECommand (SExpList [SymbolAtom "make-lemma", IntegerAtom l, StringAtom n])
    = Just $ MakeLemma l n
getIDECommand (SExpList [SymbolAtom "make-case", IntegerAtom l, StringAtom n])
    = Just $ MakeCase l n
getIDECommand (SExpList [SymbolAtom "make-with", IntegerAtom l, StringAtom n])
    = Just $ MakeWith l n
getIDECommand (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
    = do -- Maybe monad
         modeOpt <- case modeTail of
                      []                      => Just Nothing
                      [SymbolAtom "overview"] => Just $ Just Overview
                      [SymbolAtom "full"    ] => Just $ Just Full
                      _ => Nothing
         Just $ DocsFor n modeOpt
getIDECommand (SExpList [SymbolAtom "apropos", StringAtom n])
    = Just $ Apropos n
getIDECommand (SExpList [SymbolAtom "directive", StringAtom n])
    = Just $ Directive n
getIDECommand (SExpList [SymbolAtom "metavariables", IntegerAtom n])
    = Just $ Metavariables n
getIDECommand (SExpList [SymbolAtom "who-calls", StringAtom n])
    = Just $ WhoCalls n
getIDECommand (SExpList [SymbolAtom "calls-who", StringAtom n])
    = Just $ CallsWho n
getIDECommand (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
    = Just $ BrowseNamespace ns
getIDECommand (SExpList [SymbolAtom "normalise-term", StringAtom tm])
    = Just $ NormaliseTerm     tm
getIDECommand (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
    = Just $ ShowTermImplicits tm
getIDECommand (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
    = Just $ HideTermImplicits tm
getIDECommand (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
    = Just $ ElaborateTerm     tm
getIDECommand (SExpList [SymbolAtom "print-definition", StringAtom n])
    = Just $ PrintDefinition n
getIDECommand (SExpList [SymbolAtom "repl-completions", StringAtom n])
    = Just $ ReplCompletions n
getIDECommand (SExpList [SymbolAtom "enable-syntax", BoolAtom b])
    = Just $ EnableSyntax b
getIDECommand (SymbolAtom "version") = Just Version
getIDECommand (SExpList [SymbolAtom "get-options"]) = Just GetOptions
getIDECommand _ = Nothing

export
putIDECommand : IDECommand -> SExp
putIDECommand (Interpret cmd)                 = (SExpList [SymbolAtom "interpret", StringAtom cmd])
putIDECommand (LoadFile fname Nothing)        = (SExpList [SymbolAtom "load-file", StringAtom fname])
putIDECommand (LoadFile fname (Just line))    = (SExpList [SymbolAtom "load-file", StringAtom fname, IntegerAtom line])
putIDECommand (TypeOf cmd Nothing)            = (SExpList [SymbolAtom "type-of", StringAtom cmd])
putIDECommand (TypeOf cmd (Just (line, col))) = (SExpList [SymbolAtom "type-of", StringAtom cmd, IntegerAtom line, IntegerAtom col])
putIDECommand (NameAt cmd Nothing)            = (SExpList [SymbolAtom "name-at", StringAtom cmd])
putIDECommand (NameAt cmd (Just (line, col))) = (SExpList [SymbolAtom "name-at", StringAtom cmd, IntegerAtom line, IntegerAtom col])
putIDECommand (CaseSplit line col n)          = (SExpList [SymbolAtom "case-split", IntegerAtom line, IntegerAtom col, StringAtom n])
putIDECommand (AddClause line n)              = (SExpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom n])
putIDECommand (AddMissing line n)             = (SExpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom n])
putIDECommand (ExprSearch line n exprs mode)  = (SExpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom n, SExpList $ map StringAtom exprs, getMode mode])
  where
  getMode : Bool -> SExp
  getMode True  = SymbolAtom "all"
  getMode False = SymbolAtom "other"
putIDECommand ExprSearchNext                  = SymbolAtom "proof-search-next"
putIDECommand (GenerateDef line n)            = (SExpList [SymbolAtom "generate-def", IntegerAtom line, StringAtom n])
putIDECommand GenerateDefNext                 = SymbolAtom "generate-def-next"
putIDECommand (MakeLemma line n)              = (SExpList [SymbolAtom "make-lemma", IntegerAtom line, StringAtom n])
putIDECommand (MakeCase line n)               = (SExpList [SymbolAtom "make-case", IntegerAtom line, StringAtom n])
putIDECommand (MakeWith line n)               = (SExpList [SymbolAtom "make-with", IntegerAtom line, StringAtom n])
putIDECommand (DocsFor n modeOpt)             = let modeTail = case modeOpt of
                                                                 Nothing       => []
                                                                 Just Overview => [SymbolAtom "overview"]
                                                                 Just Full     => [SymbolAtom "full"] in
                                                (SExpList (SymbolAtom "docs-for" ::  StringAtom n :: modeTail))
putIDECommand (Apropos n)                     = (SExpList [SymbolAtom "apropos", StringAtom n])
putIDECommand (Metavariables n)               = (SExpList [SymbolAtom "metavariables", IntegerAtom n])
putIDECommand (WhoCalls n)                    = (SExpList [SymbolAtom "who-calls", StringAtom n])
putIDECommand (CallsWho n)                    = (SExpList [SymbolAtom "calls-who", StringAtom n])
putIDECommand (BrowseNamespace ns)            = (SExpList [SymbolAtom "browse-namespace", StringAtom ns])
putIDECommand (NormaliseTerm     tm)          = (SExpList [SymbolAtom "normalise-term", StringAtom tm])
putIDECommand (ShowTermImplicits tm)          = (SExpList [SymbolAtom "show-term-implicits", StringAtom tm])
putIDECommand (HideTermImplicits tm)          = (SExpList [SymbolAtom "hide-term-implicits", StringAtom tm])
putIDECommand (ElaborateTerm     tm)          = (SExpList [SymbolAtom "elaborate-term", StringAtom tm])
putIDECommand (PrintDefinition n)             = (SExpList [SymbolAtom "print-definition", StringAtom n])
putIDECommand (ReplCompletions n)             = (SExpList [SymbolAtom "repl-completions", StringAtom n])
putIDECommand (Directive n)             = (SExpList [SymbolAtom "directive", StringAtom n])
putIDECommand (EnableSyntax b)                = (SExpList [SymbolAtom "enable-syntax", BoolAtom b])
putIDECommand GetOptions                      = (SExpList [SymbolAtom "get-options"])
putIDECommand Version                         = SymbolAtom "version"

export
getMsg : SExp -> Maybe (IDECommand, Integer)
getMsg (SExpList [cmdexp, IntegerAtom num])
   = do cmd <- getIDECommand cmdexp
        pure (cmd, num)
getMsg _ = Nothing

escape : String -> String
escape = pack . concatMap escapeChar . unpack
  where
    escapeChar : Char -> List Char
    escapeChar '\\' = ['\\', '\\']
    escapeChar '"'  = ['\\', '\"']
    escapeChar c    = [c]

export
Show SExp where
  show (SExpList xs) = assert_total $ "(" ++ showSep " " (map show xs) ++ ")"
  show (StringAtom str) = "\"" ++ escape str ++ "\""
  show (BoolAtom b) = ":" ++ show b
  show (IntegerAtom i) = show i
  show (SymbolAtom s) = ":" ++ s

public export
interface SExpable a where
  toSExp : a -> SExp

export
SExpable IDECommand where
  toSExp = putIDECommand

export
SExpable SExp where
  toSExp = id

export
SExpable Bool where
  toSExp = BoolAtom

export
SExpable String where
  toSExp = StringAtom

export
SExpable Integer where
  toSExp = IntegerAtom

export
SExpable Int where
  toSExp = IntegerAtom . cast

export
SExpable Nat where
  toSExp = IntegerAtom . cast

export
SExpable Name where
  toSExp = SymbolAtom . show

export
(SExpable a, SExpable b) => SExpable (a, b) where
  toSExp (x, y)
      = case toSExp y of
             SExpList xs => SExpList (toSExp x :: xs)
             y' => SExpList [toSExp x, y']

export
SExpable a => SExpable (List a) where
  toSExp xs
      = SExpList (map toSExp xs)

export
SExpable a => SExpable (Maybe a) where
  toSExp Nothing = SExpList []
  toSExp (Just x) = toSExp x

export
version : Int -> Int -> SExp
version maj min = toSExp (SymbolAtom "protocol-version", maj, min)

sendStr : File -> String -> IO ()
sendStr f st =
  map (const ()) (fPutStr f st)

export
send : {auto c : Ref Ctxt Defs} -> SExpable a => File -> a -> Core ()
send f resp
    = do let r = show (toSExp resp) ++ "\n"
         log "ide-mode.send" 20 r
         coreLift $ sendStr f $ leftPad '0' 6 (asHex (cast (length r)))
         coreLift $ sendStr f r
         coreLift $ fflush f


text:
module Data.Bytes.Strict.IO

-- functions for reading/writing Bytes to and from files

-- Data.Bytes.Strict.IO should be safe and stable to depend on, though the
-- module might move over time. Conversely Data.Bytes.Lazy.IO is not a good
-- idea to depend on despite being the more useful API. It is being provided
-- for the purposes of developing this library and for people to prototype with
-- but it is lazy IO, and one of the lessons of Haskell is that while lazyness
-- is good, lazy io isn't. There's just no way to deal with IO errors in pure
-- code, and doing IO lazily will give you exactly that. Say we've read some
-- file into a lazy bytes and pass it along to our pure code. If the file is
-- closed before we start consuming the LBytes, we'll get a file error in a
-- place it can't be addressed/handled. We don't have an exception mechanism in
-- idris2 currently so this is slightly less of a problem than it is in haskell
-- but at the same time it'd be a real hassle to make every LBytes method end
-- with `Either Error a`. The ideal way to go is a streaming IO library that
-- provides our LBytes rather than lazy io because you can structure your
-- program around the streaming lib and have confidence about when issues will
-- crop up and where to handle them.


text:
module lib.Library3

export
salute3 : String
salute3 = "Hello, this is Library3"


text:
module Circuits.NetList.Types

import Decidable.Equality

import Data.List.Elem

import public Circuits.Common

%default total

namespace Direction

  public export
  data Direction = INPUT | OUTPUT | INOUT

  Uninhabited (INPUT = OUTPUT) where
    uninhabited Refl impossible

  Uninhabited (OUTPUT = INOUT) where
    uninhabited Refl impossible

  Uninhabited (INPUT = INOUT) where
    uninhabited Refl impossible

  export
  DecEq Direction where
    decEq INPUT INPUT   = Yes Refl
    decEq INPUT OUTPUT  = No absurd
    decEq INPUT INOUT   = No absurd

    decEq OUTPUT INPUT  = No (negEqSym absurd)
    decEq OUTPUT OUTPUT = Yes Refl
    decEq OUTPUT INOUT  = No absurd

    decEq INOUT INPUT   = No (negEqSym absurd)
    decEq INOUT OUTPUT  = No (negEqSym absurd)
    decEq INOUT INOUT   = Yes Refl

namespace Proj

  public export
  data Project : Direction -> Type where
    WRITE : Project OUTPUT
    READ  : Project INPUT

namespace Cast

  public export
  data Cast : (from,to : Direction) -> Type where
    BI : Cast INOUT INPUT
    BO : Cast INOUT OUTPUT

  Uninhabited (Cast OUTPUT flow) where
    uninhabited BI impossible
    uninhabited BO impossible

  Uninhabited (Cast INPUT flow) where
    uninhabited BI impossible
    uninhabited BO impossible

  Uninhabited (Cast INOUT INOUT) where
    uninhabited BI impossible
    uninhabited BO impossible

  export
  cast : (f,t : Direction) -> Dec (Cast f t)
  cast INPUT _  = No absurd
  cast OUTPUT _ = No absurd
  cast INOUT INPUT = Yes BI
  cast INOUT OUTPUT = Yes BO
  cast INOUT INOUT = No absurd

namespace Index

  public export
  data Up : (flow : Direction) -> Type where
    UO : Up OUTPUT
    UB : Up INOUT

  public export
  data Down : (flow : Direction) -> Type where
    DI : Down INPUT
    DB : Down INOUT

  public export
  data Index : (flow : Direction) -> Type where
    UP   : Up f -> Index f
    DOWN : Down f -> Index f

  export
  dirFromCast : Cast INOUT flow -> Index INOUT
  dirFromCast BI = DOWN DB
  dirFromCast BO = UP UB

namespace Gate

  namespace Binary
    public export
    data Kind = AND  | IOR  | XOR
              | ANDN | IORN | XORN

  namespace Unary
    public export
    data Kind = NOT

    export
    Show Unary.Kind where
      show NOT = "not"

namespace Types

  public export
  data Ty  : Type where
    TyUnit : Ty
    TyPort : (Direction, DType) -> Ty
    TyChan : DType -> Ty
    TyGate : Ty

  Uninhabited (TyUnit = TyPort x) where
    uninhabited Refl impossible

  Uninhabited (TyUnit = TyChan x) where
   uninhabited Refl impossible

  Uninhabited (TyUnit = TyGate) where
    uninhabited Refl impossible

  Uninhabited (TyPort x = TyGate) where
    uninhabited Refl impossible

  Uninhabited (TyPort x = TyChan y) where
    uninhabited Refl impossible

  Uninhabited (TyGate = TyChan y) where
    uninhabited Refl impossible

  export
  DecEq Ty where
    decEq TyUnit TyUnit = Yes Refl
    decEq TyUnit (TyPort x) = No absurd
    decEq TyUnit TyGate = No absurd
    decEq TyUnit (TyChan x) = No absurd

    decEq (TyPort x) TyUnit = No (negEqSym absurd)
    decEq (TyPort x) (TyPort y) with (decEq x y)
      decEq (TyPort x) (TyPort x) | (Yes Refl)
        = Yes Refl
      decEq (TyPort x) (TyPort y) | (No contra)
        = No (\Refl => contra Refl)
    decEq (TyPort x) TyGate = No (absurd)
    decEq (TyPort x) (TyChan c) = No (absurd)

    decEq TyGate TyUnit = No (negEqSym absurd)
    decEq TyGate (TyPort x) = No (negEqSym absurd)
    decEq TyGate TyGate = Yes Refl
    decEq TyGate (TyChan x) = No absurd

    decEq (TyChan ty) TyUnit = No (negEqSym absurd)
    decEq (TyChan ty) (TyPort x) = No (negEqSym absurd)
    decEq (TyChan ty) TyGate = No (negEqSym absurd)
    decEq (TyChan x) (TyChan y) with (decEq x y)
      decEq (TyChan x) (TyChan x) | (Yes Refl) = Yes Refl
      decEq (TyChan x) (TyChan y) | (No contra) = No (\Refl => contra Refl)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML

import Data.List
import Data.List1
import Data.SortedMap

import Text.Bounded
import Text.Token
import Language.TOML.Lexer
import Language.TOML.Parser
import public Language.TOML.Value
import Language.TOML.ConcreteSyntax as C

private
data SectionIdent = SGlobal
                  | STable CKey
                  | STableArray CKey

toPair : Item -> Maybe (CKey,CValue)
toPair (IKeyValue key val) = Just (key,val)
toPair (ITableHeader _)    = Nothing
toPair (ITableArray _)     = Nothing

takeWhileJust : (a -> Maybe b) -> List a -> (List b, List a)
takeWhileJust f [] = ([],[])
takeWhileJust f (x :: xs) = case f x of
  Nothing => ([],x :: xs)
  Just vb => let (bs,as) = takeWhileJust f xs in (vb :: bs, as)

private
sections : List C.Item -> List (SectionIdent, List (CKey, CValue))
sections xs = loop SGlobal xs
    where
        loop : SectionIdent -> List C.Item -> List (SectionIdent, List (CKey, CValue))
        loop sec [] = []
        loop sec ((ITableHeader header) :: xs) = loop (STable header) xs
        loop sec ((ITableArray header) :: xs) = loop (STableArray header) xs
        loop sec xs =
            let (kvs, rest) = takeWhileJust toPair xs
             in (sec, kvs) :: loop sec rest

public export
data Error = ErrDottedIsNotATable Key Value
           | LexerError
           | ParseError (List String)
           | Unimplemented

public export
Show Error where
    show (ErrDottedIsNotATable x y) = "Dotted key part `" ++ show x ++ "`is not a table"
    show LexerError = "Lexer error"
    show (ParseError x) = "Parse error: " ++ show x
    show Unimplemented = "Unimplemented feature"

private
keyAtomStr : CKeyAtom -> Key
keyAtomStr (CKBare x) = x
keyAtomStr (CKQuoted x) = x

private
keyParts : CKey -> List1 Key
keyParts (CKAtom x) = keyAtomStr x ::: []
keyParts (CKDotted x) = map keyAtomStr x

public export
Eq CKeyAtom where
    x == y = keyAtomStr x == keyAtomStr y

public export
Eq CKey where
    x == y = keyParts x == keyParts y

private
tableSetWithParts : (t : Table) -> (path : List1 Key) -> (val : Value) -> Either Error Table
tableSetWithParts t (head ::: []) val = pure $ insert head val t
tableSetWithParts t (head ::: (x :: xs)) val = do
    inner <- case lookup head t of
                    Nothing => pure empty
                    Just (VTable t) => pure t
                    Just v => Left $ ErrDottedIsNotATable head v

    inner' <- tableSetWithParts inner (x ::: xs) val
    pure $ insert head (VTable inner') t

mutual

    private
    cvalToVal : CValue -> Either Error Value
    cvalToVal (CVString x) = pure $ VString x
    cvalToVal (CVInteger x) = pure $ VInteger x
    cvalToVal (CVFloat x) = pure $ VFloat x
    cvalToVal (CVBoolean x) = pure $ VBoolean x
    cvalToVal (CVArray xs) = map VArray $ for xs cvalToVal
    cvalToVal (CVInlineTable xs) = map VTable $ tableFromKVs xs

    private
    tableFromKVs : List (CKey, CValue) -> Either Error Table
    tableFromKVs xs = loop empty xs
        where
            loop : Table -> List (CKey, CValue) -> Either Error Table
            loop t [] = Right t
            loop t ((k, v) :: xs) = do
                v' <- cvalToVal v
                let parts = keyParts k
                t' <- tableSetWithParts t parts v'
                loop t' xs

private
extendFile : (file : Table) -> (sects : List (SectionIdent, List (CKey, CValue))) -> Either Error Table
extendFile file [] = pure file
extendFile file ((SGlobal, kvs) :: rest) = do
    tab <- tableFromKVs kvs
    extendFile (mergeLeft tab file) rest
extendFile file (((STable key), kvs) :: rest) = do
    tab <- tableFromKVs kvs
    let kParts = keyParts key
    file' <- tableSetWithParts file kParts (VTable tab)
    extendFile file' rest

extendFile file rest@(((STableArray key), kvs) :: _) = do
    let (array, rest') = partition
            (\(sect, _) => case sect of
                (STableArray key') => key == key'
                _ => False)
            rest
    array' <- traverse (map VTable . tableFromKVs) (map snd array)
    file' <- tableSetWithParts file (keyParts key) (VArray array')
    extendFile file' rest'

export
parseTOML : (src : String) -> Either Error Table
parseTOML src = do
    let Just toks = lexTOML src
        | Nothing => Left LexerError

    items <- bimap ParseError id (parseItems toks)

    let sects = sections items

    extendFile empty sects

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module Dart.FFI.Elab.Implementation

import public Dart.FFI
import public Dart.FFI.Elab.Types
import public Data.Either
import public Data.List1
import public Data.Maybe
import public Data.String
import public Language.Reflection

titleCase : String -> String
titleCase s = toUpper (substr 0 1 s) ++ substr 1 (length s) s

mkTy : Name -> TTImp -> ITy
mkTy = MkTy EmptyFC EmptyFC

primVal : Constant -> TTImp
primVal = IPrimVal EmptyFC

publicExport : List FnOpt -> ITy -> Decl
publicExport = IClaim EmptyFC MW Public

export
publicExportHint : ITy -> Decl
publicExportHint = publicExport [Hint False]

publicExportInline : ITy -> Decl
publicExportInline = publicExport [Inline]

patClause : TTImp -> TTImp -> Clause
patClause = PatClause EmptyFC

var : Name -> TTImp
var = IVar EmptyFC

app : TTImp -> TTImp -> TTImp
app = IApp EmptyFC

namedApp : TTImp -> Name -> TTImp -> TTImp
namedApp = INamedApp EmptyFC

pi : Name -> TTImp -> TTImp -> TTImp
pi n v = IPi EmptyFC MW ExplicitArg (Just n) v

implicitPi : Name -> TTImp -> TTImp -> TTImp
implicitPi n v = IPi EmptyFC MW ImplicitArg (Just n) v

bindVar : String -> TTImp
bindVar = IBindVar EmptyFC

inNamespace : Namespace -> List Decl -> Decl
inNamespace ns = INamespace EmptyFC ns

def : Name -> List Clause -> Decl
def = IDef EmptyFC

bindParameter : TTImp -> String -> TTImp
bindParameter ps p = `(~ps ~(bindVar p))

parameterized : TTImp -> List String -> TTImp
parameterized n ps = foldl bindParameter n ps

simpleDef : Name -> List String -> TTImp -> Decl
simpleDef n ps val =
  def n [
    patClause (parameterized (var n) ps) val
  ]

defExport : Name -> List String -> TTImp -> TTImp -> List Decl
defExport n ps ty val = [
  publicExportInline (mkTy n ty),
  simpleDef n ps val
]

dartInvoke : String -> TTImp -> TTImp -> TTImp -> TTImp
dartInvoke foreignName typeArgs positional named =
  `(prim__dart_invoke ~(primVal (Str foreignName)) ~typeArgs ~positional ~named)

dartInvokePure : String -> TTImp -> TTImp -> TTImp -> TTImp
dartInvokePure foreignName typeArgs positional named =
  `(prim__dart_invoke_pure ~(primVal (Str foreignName)) ~typeArgs ~positional ~named)

dartNew : TTImp -> String -> TTImp -> TTImp -> TTImp
dartNew ty ctorName positional named =
  `(prim__dart_new ~ty ~(primVal (Str ctorName)) ~positional ~named)

dartNewConst : TTImp -> String -> TTImp -> TTImp -> TTImp
dartNewConst ty ctorName positional named =
  `(prim__dart_new_const ~ty ~(primVal (Str ctorName)) ~positional ~named)

listWithVars : List String ->  TTImp
listWithVars vars = foldr (\v, acc => `(~(var (UN v)) :: ~acc)) `(Nil) vars

positionalOrNamed : DartParameter -> Either (DartName, DartType) (DartName, DartType)
positionalOrNamed (Positional n ty) = Left (n, ty)
positionalOrNamed (Named n ty) = Right (n, ty)

consArrow : TTImp -> TTImp -> TTImp
consArrow ty acc = `(~ty -> ~acc)

varOf : DartName -> TTImp
varOf n = var $
  case reverse (toList (split (=='.') n)) of
    (n :: ns@(_ :: _)) => NS (MkNS ns) (UN n)
    _ => UN n

TypeParameters : Type
TypeParameters = List (String, TTImp)

parsePrimitiveType : DartName -> Maybe TTImp
parsePrimitiveType = \case
  "int" => Just `(Int)
  "Int" => Just `(Int)
  "String" => Just `(String)
  "bool" => Just `(DartBool)
  "Bool" => Just `(DartBool)
  "double" => Just `(Double)
  "Double" => Just `(Double)
  "void" => Just `(())
  "()" => Just `(())
  _ => Nothing

elabType' : TypeParameters -> DartType -> TTImp
elabType' ts = \case
  FType ps ret => foldr (\p, acc => `(~p -> ~acc)) (elabType' ts ret) (elabType' ts <$> ps)
  GType t args => foldl app (elabType' ts t) (elabType' ts <$> args)
  NType n => case parsePrimitiveType n of
    Just ty => ty
    _ => case lookup n ts of
      Nothing => varOf n
      Just _ => bindVar n

elabType : DartType -> TTImp
elabType = elabType' []

packageQualifiedName : {auto p : DartPackage} -> String -> String
packageQualifiedName n =
  if length p.name == 0
    then n
    else n ++ "," ++ p.name

withMemberName : String -> String -> String
withMemberName qname member =
  case split (== ',') qname of
    q ::: p :: _ => q ++ "." ++ member ++ "," ++ p
    _ => qname ++ "." ++ member

none : TTImp
none = `(Parameters.none)

record Invocation where
  constructor MkInvocation
  hasIO : Bool
  invoke : (positional : TTImp) -> (named : TTImp) -> TTImp

functionType : TTImp -> TypeParameters -> TTImp
functionType ty ps = foldr (\(pn, pty), acc => pi (UN pn) pty acc) ty ps

functionType' : TTImp -> TypeParameters -> TypeParameters -> TTImp
functionType' ty implicitPs ps =
  let signature = functionType ty ps
  in foldr (\(pn, pty), acc => implicitPi (UN pn) pty acc) signature implicitPs

defParameter : TypeParameters -> Namespace -> (DartName, DartType) -> List Decl
defParameter tps tagNS (name, ty) =
  let
    tag = var (NS tagNS (UN "Tag"))
    tag' = foldl app tag (var . UN . fst <$> tps)
  in
    defExport (UN name) []
      (functionType' `(Parameter ~(tag')) tps [])
      `(mkParameter ~(primVal (Str name)) ~(elabType ty))

tagDataType : TypeParameters -> List Decl
tagDataType tps = `[
  public export data Tag : ~(functionType' `(Type) [] tps) where
]

qualifiedNamedApp : TypeParameters -> Namespace -> String -> TTImp
qualifiedNamedApp tps ns n =
  let qname = var (NS ns (UN n))
  in foldl (\acc, t => let n = UN t in namedApp acc n (var n)) qname (fst <$> tps)

consParameter : TypeParameters -> Namespace -> TTImp -> String -> TTImp
consParameter tps ns acc n =
  let name = qualifiedNamedApp tps ns n
  in `(~name :: ~acc)

parameterDeclarationsFor : TypeParameters -> Namespace -> Namespace -> List (DartName, DartType) -> List Decl
parameterDeclarationsFor tps ns tagNS named =
  let
    namedNames = fst <$> named
    namedParameters = foldl (consParameter tps tagNS) `(Nil) namedNames
  in [
    inNamespace ns $
      tagDataType tps
      ++ concatMap (defParameter tps tagNS) named
      ++ `[
        %inline
        public export
        NamedParameters : ~(functionType' `(Type) tps [])
        NamedParameters = Parameters ~(namedParameters)
      ]
  ]

elabFunctionWithNamedParameters
  : List String
 -> Invocation
 -> TypeParameters
 -> (thisTy : Maybe TTImp)
 -> TTImp
 -> String
 -> List DartParameter
 -> List (DartName, DartType)
 -> List (DartName, DartType)
 -> List Decl
elabFunctionWithNamedParameters parentNS invocation typeParams thisTy ty idrisName ps positional named =
  let
    topNS = titleCase idrisName
    ns = MkNS [topNS]
    tagNS = MkNS (topNS :: parentNS)
    namedParametersTy = qualifiedNamedApp typeParams tagNS "NamedParameters"
    fn = UN idrisName
    returnType = if invocation.hasIO then `(~(bindVar "io") ~(ty)) else ty
    thisParam = ("this",) <$> thisTy
    params = (map (elabType' typeParams) <$> positional) ++ [("ps", namedParametersTy)] ++ toList thisParam
    paramNames = fst <$> params
    posArgs = listWithVars (toList (fst <$> thisParam) ++ (fst <$> positional))
    sig = functionType' returnType typeParams params
  in parameterDeclarationsFor typeParams ns tagNS named ++
    if invocation.hasIO
      then defExport fn paramNames `(HasIO ~(bindVar "io") => ~sig) `(primIO $ ~(invocation.invoke posArgs `(ps)))
      else defExport fn paramNames sig (invocation.invoke posArgs `(ps))

elabFunctionWithPositionalParameters : Invocation
  -> TypeParameters
  -> Maybe TTImp
  -> TTImp
  -> (idrisName : String)
  -> List DartParameter
  -> List (DartName, DartType)
  -> List Decl
elabFunctionWithPositionalParameters invocation typeParams thisTy ty idrisName ps positional =
  let
    fn = UN idrisName
    returnType = if invocation.hasIO then `(~(bindVar "io") ~(ty)) else ty
    thisParam = ("this",) <$> thisTy
    params = (map (elabType' typeParams) <$> positional) ++ toList thisParam
    paramNames = fst <$> params
    posArgs = listWithVars (toList (fst <$> thisParam) ++ (fst <$> positional))
    sig = functionType' returnType typeParams params
  in if invocation.hasIO
    then defExport fn paramNames `(HasIO ~(bindVar "io") => ~sig) `(primIO ~(invocation.invoke posArgs none))
    else defExport fn paramNames sig (invocation.invoke posArgs none)

elabFunction'
  : List String
 -> Invocation
 -> TypeParameters
 -> (thisTy : Maybe TTImp)
 -> TTImp
 -> (idrisName : String)
 -> List DartParameter
 -> List Decl
elabFunction' ns invocation typeParams thisTy ty n ps =
  let (positional, named) = partitionEithers (positionalOrNamed <$> ps)
  in if null named
    then elabFunctionWithPositionalParameters invocation typeParams thisTy ty n ps positional
    else elabFunctionWithNamedParameters ns invocation typeParams thisTy ty n ps positional named

ioInvocationOf : String -> List String -> Invocation
ioInvocationOf fn typeArgs = MkInvocation {
  hasIO = True,
  invoke = dartInvoke fn (listWithVars typeArgs)
}

pureInvocationOf : String -> List String -> Invocation
pureInvocationOf fn typeArgs = MkInvocation {
  hasIO = False,
  invoke = dartInvokePure fn (listWithVars typeArgs)
}

elabFunction
  : {auto p : DartPackage}
 -> (hasIO : Bool)
 -> DartType
 -> DartName
 -> List DartParameter
 -> List Decl
elabFunction hasIO ty n ps =
  let
    fn = packageQualifiedName n
    invocation = if hasIO then ioInvocationOf fn [] else pureInvocationOf fn []
  in elabFunction' [] invocation [] Nothing (elabType ty) n ps

elabConstructorOf : List String -> TTImp -> TypeParameters -> String -> List DartParameter -> Invocation -> List Decl
elabConstructorOf ns ty typeParams n ps invocation =
  elabFunction'
    ns
    invocation
    typeParams
    Nothing
    ty
    (if length n == 0 then "new" else n)
    ps

elabGetter : (hasIO : Bool)
  -> TypeParameters
  -> Maybe TTImp
  -> DartType
  -> DartName
  -> String
  -> List Decl
elabGetter False typeParams (Just thisTy) ty n fn =
  defExport (UN n) ["this"] (functionType' (elabType ty) typeParams [("thisTy", thisTy)])
    `(prim__dart_get_pure ~(primVal (Str fn)) ~(var (UN "this")))
elabGetter False typeParams Nothing ty n fn =
  defExport (UN n) [] (elabType ty)
    `(prim__dart_get_pure ~(primVal (Str fn)) Void)
elabGetter True typeParams (Just thisTy) ty n fn =
  let io = bindVar "io"
  in defExport (UN n) ["this"]
    `(HasIO ~io => ~(functionType' `(~io ~(elabType ty)) typeParams [("this", thisTy)]))
    `(primIO $ prim__dart_get ~(primVal (Str fn)) ~(var (UN "this")))
elabGetter True typeParams Nothing ty n fn =
  let io = bindVar "io"
  in defExport (UN n) []
    `(HasIO ~io => ~io ~(elabType ty))
    `(primIO $ prim__dart_get ~(primVal (Str fn)) Void)

elabVal : DartType -> DartName -> String -> List Decl
elabVal = elabGetter False [] Nothing

elabVar : TypeParameters -> Maybe TTImp ->  DartType -> DartName -> String -> List Decl
elabVar typeParams thisTy ty n fn =
  let
    io = bindVar "io"
    ty' = elabType ty
    get = UN n
    set = UN ("set" ++ titleCase n)
    getTy = `(~io ~ty')
    setTy = `(~io ())
  in case thisTy of
    Just thisTy =>
      defExport get ["this"]
        `(HasIO ~io => ~(functionType' getTy typeParams [("this", thisTy)]))
        `(primIO $ prim__dart_get ~(primVal (Str fn)) ~(var (UN "this")))
      ++ defExport set ["value", "this"]
        `(HasIO ~io => ~(functionType' setTy typeParams [("value", ty'), ("this", thisTy)]))
        `(ignore $ primIO $ prim__dart_set ~(primVal (Str fn)) ~(var (UN "value")) ~(var (UN "this")))
    Nothing =>
      defExport get []
        `(HasIO ~io => ~getTy)
        `(primIO $ prim__dart_get ~(primVal (Str fn)) Void)
      ++ defExport set ["value"]
        `(HasIO ~io => (value : ~ty') -> ~setTy)
        `(ignore $ primIO $ prim__dart_set ~(primVal (Str fn)) ~(var (UN "value")) Void)

simpleNameOf : DartType -> Maybe String
simpleNameOf = \case
  NType n => Just n
  GType t _ => simpleNameOf t
  FType _ _ => Nothing

elabTypeParams : List String -> List (String, TTImp)
elabTypeParams tps = (,`(Type)) <$> tps

elabClassMember : List String -> String -> List (String, TTImp) -> TTImp -> DartDecl -> List (Decl)
elabClassMember ns qName typeParams thisTy d = case d of
  Static (Effectful (Function ty n ps)) =>
    elabFunction' ns (ioInvocationOf (withMemberName qName n) []) typeParams Nothing (elabType ty) n ps
  Generic funTypeParams (Static (Effectful (Function ty n ps))) =>
    elabFunction' ns (ioInvocationOf (withMemberName qName n) funTypeParams) (elabTypeParams funTypeParams) Nothing (elabType ty) n ps
  Effectful (Function ty n ps) =>
    elabFunction' ns (ioInvocationOf ("." ++ n) []) typeParams (Just thisTy) (elabType ty) n ps
  Generic funTypeParams (Effectful (Function ty n ps)) =>
    elabFunction' ns (ioInvocationOf ("." ++ n) funTypeParams) (typeParams ++ elabTypeParams funTypeParams) (Just thisTy) (elabType ty) n ps
  Function ty n ps =>
    elabFunction' ns (pureInvocationOf ("." ++ n) []) typeParams (Just thisTy) (elabType ty) n ps
  Generic funTypeParams (Function ty n ps) =>
    elabFunction' ns (pureInvocationOf ("." ++ n) funTypeParams) (typeParams ++ elabTypeParams funTypeParams) (Just thisTy) (elabType ty) n ps
  Static (Function ty n ps) =>
    elabFunction' ns (pureInvocationOf (withMemberName qName n) []) typeParams Nothing (elabType ty) n ps
  Generic funTypeParams $ Static (Function ty n ps) =>
    elabFunction' ns (pureInvocationOf (withMemberName qName n) funTypeParams) (elabTypeParams funTypeParams) Nothing (elabType ty) n ps
  Static (Val ty n) =>
    elabVal ty n (withMemberName qName n)
  Val ty n =>
    elabGetter False typeParams (Just thisTy) ty n ("." ++ n)
  Static (Effectful (Val ty n)) =>
    elabGetter True [] Nothing ty n (withMemberName qName n)
  Effectful (Val ty n) =>
    elabGetter True typeParams (Just thisTy) ty n ("." ++ n)
  Static (Var ty n) =>
    elabVar [] Nothing ty n (withMemberName qName n)
  Var ty n =>
    elabVar typeParams (Just thisTy) ty n ("." ++ n)
  Constructor n ps =>
    elabConstructorOf ns thisTy typeParams n ps (MkInvocation {hasIO = True, invoke = dartNew thisTy n})
  Const $ Constructor n ps =>
    elabConstructorOf ns thisTy typeParams n ps (MkInvocation {hasIO = False, invoke = dartNewConst thisTy n})
  _ => []

elabEnumMember : {auto p : DartPackage} -> TTImp -> String -> String -> List (Decl)
elabEnumMember enumTy dartType n =
  defExport (UN n) [] enumTy
    `(prim__dart_get_pure ~(primVal (Str (packageQualifiedName (dartType ++ "." ++ n)))) Void)

elabPrimitive : {auto p : DartPackage} -> DartName -> List DartDecl -> Elab ()
elabPrimitive n members =
  case parsePrimitiveType n of
    Just thisTy => do
      let qName = packageQualifiedName n
      when (not (null members)) $
        declare [
          inNamespace (MkNS [n]) $
            concatMap (elabClassMember [n] qName [] thisTy) members
        ]
    Nothing => fail $ "Unsupported primitive type " ++ n

elabClass : {auto p : DartPackage} -> DartName -> List String -> List DartDecl -> Elab ()
elabClass n ps members = do
  let qName = packageQualifiedName n
  when (not (null members)) $
    declare [
      inNamespace (MkNS [n])
        let
          typeParams = elabTypeParams ps
          thisTy = foldl (\ps, p => `(~ps ~(var (UN p)))) (var (UN n)) ps
        in concatMap (elabClassMember [n] qName typeParams thisTy) members
    ]

elabPackageDecl : {auto p : DartPackage} -> DartDecl -> Elab ()
elabPackageDecl = \case
  Generic funTypeParams (Effectful (Function ty n ps)) =>
    declare $ elabFunction' [] (ioInvocationOf (packageQualifiedName n) funTypeParams) (elabTypeParams funTypeParams) Nothing (elabType ty) n ps
  Effectful (Function ty fn ps) =>
    declare $ elabFunction True ty fn ps
  Function ty fn ps =>
    declare $ elabFunction False ty fn ps
  Val ty n =>
    declare $ elabVal ty n (packageQualifiedName n)
  Var ty n =>
    declare $ elabVar [] Nothing ty n (packageQualifiedName n)
  Generic ps $ Class n members =>
    elabClass n ps members
  Class n members =>
    elabClass n [] members
  Primitive $ Class n members =>
    elabPrimitive n members
  Enum n members =>
    when (not (null members)) $
      declare [
        inNamespace (MkNS [n])
          (concatMap (elabEnumMember (var (UN n)) n) members)
      ]
  Partial d =>
    elabPackageDecl d
  d => fail $ "Unsupported Dart definition: " ++ show d

lookupIsAssignableFromConstructor : Elab Name
lookupIsAssignableFromConstructor = do
  [(n, _)] <- getType `{{IsAssignableFrom}}
    | _ => fail "IsAssignableFrom is not in scope."
  [c] <- getCons n
    | _ => fail "IsAssignableFrom should have a single constructor!"
  pure c

record ExtendsInfo where
  constructor MkExtendsInfo
  className : DartName
  superType : DartType

extendsInfo : DartName -> DartDecl -> Maybe ExtendsInfo
extendsInfo className (Extends t) = Just (MkExtendsInfo className t)
extendsInfo _ _ = Nothing

defStruct : {auto p : DartPackage} -> String -> List Decl
defStruct n =
  defExport (UN n) [] `(Type)
    `(Struct ~(primVal (Str (packageQualifiedName n))) [])

defGeneric : {auto p : DartPackage} -> String -> List String -> List Decl
defGeneric n ps =
  let ty = `(Type)
  in defExport (UN n) ps (functionType ty ((,ty) <$> ps))
    `(GenericType ~(primVal (Str (packageQualifiedName n))) ~(listWithVars ps))

elabTypeDecl : {auto p : DartPackage} -> DartDecl -> List Decl
elabTypeDecl = \case
  Class n members => defStruct n
  Enum n members => defStruct n
  Generic ps (Class n _) => defGeneric n ps
  _ => []

elabTypeDeclExtends : {auto p : DartPackage} -> DartDecl -> List ExtendsInfo
elabTypeDeclExtends = \case
  Class n members => mapMaybe (extendsInfo n) members -- TODO: Enum => IsEnum
  Partial d => elabTypeDeclExtends d
  _ => []

elabExtends : Name -> ExtendsInfo -> List Decl
elabExtends isAssignableFromCtor e =
  let n = UN (e.className ++ "Extends" ++ fromMaybe "" (simpleNameOf e.superType))
  in [
    publicExportHint (mkTy n `(IsAssignableFrom ~(elabType e.superType) ~(var (UN e.className)))),
    simpleDef n [] (var isAssignableFromCtor)
  ]

elabPackage : DartPackage -> Elab ()
elabPackage p = do
  -- Declare all `IsAssignableFrom` / `IsEnum` constraints
  let extensions = concatMap elabTypeDeclExtends p.declarations
  when (not (null extensions)) $ do
    isAssignableFromCtor <- lookupIsAssignableFromConstructor
    for_ extensions (declare . elabExtends isAssignableFromCtor)

  -- Only then, the actual functions
  for_ p.declarations elabPackageDecl

export
importDart : List DartPackage -> Elab ()
importDart packages = do
  -- Declare all foreign types first
  for_ packages \p =>
    for_ p.declarations (declare . elabTypeDecl)
  for_ packages elabPackage


text:
%flag C "-I/usr/include/libdrm -I/usr/include/libpng16 "
%flag C "-lGLEW -lGLU -lGL -lpng16 -lz "
%flag C "-lGL"

max_stars_repo_name: corazza/gl-idris

max_issues_repo_name: corazza/gl-idris

max_forks_repo_name: corazza/gl-idris


text:
module Koans.HigherOrderFunctions

-- Complete these functions

-- Maps are used to map a function to elements in a list.
myFirstMap : Bool
myFirstMap = ?fillme1 == map (2*) [1..4]

mySecondMap : Bool
mySecondMap = [1, 4, 9, 16, 25] == map ?fillme2 [1..5]

myThirdMap : Bool
myThirdMap = [25, 16, 9, 4, 1] == map ?fillme3 [1..5]

-- Folds are used to combine elements in a list from start to finish using a function.
myFirstFold : Bool
myFirstFold = foldl (+) 0 [1..4] == ?fillme4

mySecondFold : Bool
mySecondFold = 5 == foldl ?fillme5 5 [1..4]

-- Scans are like fold but you see the intermediate results, and then the result.
myFirstScan : Bool
myFirstScan = scanl (max) 5 [1,2,3,4] == ?fillme6

mySecondScan : Bool
mySecondScan = scanl ?fillme7 5 [1,2,10,1] == [5,5,5,10,10]

myThirdScan : Bool
myThirdScan = scanl (/) 64 [4,2,4] == ?fillme8

-- TODO Add examples for scanr and foldr

-- You can filter things as well.

xs : List Int
xs = [1,2,3,4,5,6,7,8,9,10]

myFirstFilter : Bool
myFirstFilter = filter (>5) xs == ?fillme15

mySecondFilter : Bool
mySecondFilter = filter ?fillme16 [10,20,30,40,50,60,70,80,90,100] == xs

-- You can combine functions as well

myFirstCombi : Bool
myFirstCombi =  ["bang", "boom", "bang", "boom", "bang"] == map ?fillme17 (filter ?fillme18 xs)

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
module TypeChecking

import Logic
import Maps
import Stlc

%access public export

%default total

beq_ty : Ty -> Ty -> Bool
beq_ty TyBool TyBool = True
beq_ty TyBool (TyArrow _ _) = False
beq_ty (TyArrow _ _) TyBool = False
beq_ty (TyArrow t11 t12) (TyArrow t21 t22) = beq_ty t11 t21 && beq_ty t12 t22

beq_ty_refl : TypeChecking.beq_ty ty ty = True
beq_ty_refl {ty = TyBool} = Refl
beq_ty_refl {ty = (TyArrow ty1 ty2)} = rewrite beq_ty_refl {ty=ty1}
                                       in rewrite beq_ty_refl {ty=ty2}
                                       in Refl

beq_ty__eq : TypeChecking.beq_ty ty1 ty2 = True -> ty1 = ty2
beq_ty__eq {ty1 = TyBool} {ty2 = TyBool} _ = Refl
beq_ty__eq {ty1 = TyBool} {ty2 = TyArrow ty21 ty22} prf = absurd prf
beq_ty__eq {ty1 = TyArrow ty11 ty12} {ty2 = TyBool} prf = absurd prf
beq_ty__eq {ty1 = TyArrow ty11 ty12} {ty2 = TyArrow ty21 ty22} prf =
  let (prf1, prf2) = band prf
  in rewrite beq_ty__eq {ty1=ty11} {ty2=ty21} prf1
  in rewrite beq_ty__eq {ty1=ty12} {ty2=ty22} prf2
  in Refl

type_check : (gamma : Context) -> (t : Tm) -> Maybe Ty
type_check gamma (Var x) = gamma x
type_check gamma (Abs x ty t) = do
  ty' <- type_check (update x ty gamma) t
  pure (TyArrow ty ty')
type_check gamma (App t1 t2) = do
  ty1 <- type_check gamma t1
  ty2 <- type_check gamma t2
  case ty1 of
    TyArrow ty11 ty12 => case beq_ty ty11 ty2 of
      False => Nothing
      True => pure ty12
    _ => Nothing
type_check _ Tru = Just TyBool
type_check _ Fls = Just TyBool
type_check gamma (Test cond tt tf) = do
  ty_cond <- type_check gamma cond
  ty_t <- type_check gamma tt
  ty_f <- type_check gamma tf
  case ty_cond of
    TyBool => case beq_ty ty_t ty_f of
      False => Nothing
      True => pure ty_t
    _ => Nothing

type_checking_sound : TypeChecking.type_check gamma t = Just ty ->
                      HasType gamma t ty
type_checking_sound {t = Var _} prf = T_Var prf
type_checking_sound {gamma} {t = App t1 t2} prf
  with (type_check gamma t1) proof t1_prf
    type_checking_sound {gamma} {t = App t1 t2} prf | Nothing = absurd prf
    type_checking_sound {gamma} {t = App t1 t2} prf
    | Just ty1 with (type_check gamma t2) proof t2_prf
      type_checking_sound {gamma} {t = App t1 t2} prf | Just ty1 | Nothing =
        absurd prf
      type_checking_sound {gamma} {t = App t1 t2} prf
      | Just ty1 | Just ty2 with (ty1)
        type_checking_sound {gamma} {t = App t1 t2} prf
        | Just ty1 | Just ty2 | TyArrow ty11 ty12 with (beq_ty ty11 ty2) proof ty_prf
          type_checking_sound {gamma} {t = App t1 t2} prf
          | Just ty1 | Just ty2 | TyArrow ty11 ty12 | False = absurd prf
          type_checking_sound {gamma} {t = App t1 t2} prf
          | Just ty1 | Just ty2 | TyArrow ty11 ty12 | True =
            T_App (rewrite sym (justInjective prf)
                   in type_checking_sound (sym t1_prf))
                  (rewrite beq_ty__eq {ty1=ty11} {ty2=ty2} (sym ty_prf)
                   in type_checking_sound (sym t2_prf))
        type_checking_sound {gamma} {t = App t1 t2} prf
        | Just ty1 | Just ty2 | TyBool = absurd prf
type_checking_sound {gamma} {t = Abs x ty t} prf with (_)
  type_checking_sound {gamma} {t = Abs x ty t} prf | with_pat = ?type_checking_sound_rhs_3_rhs

type_checking_sound {t = Tru} prf = rewrite sym (justInjective prf) in T_Tru
type_checking_sound {t = Fls} prf = rewrite sym (justInjective prf) in T_Fls
type_checking_sound {gamma} {t = Test cond tt tf} prf
  with (type_check gamma cond) proof cond_prf
    type_checking_sound {gamma} {t = Test cond tt tf} prf | Nothing =
      absurd prf
    type_checking_sound {gamma} {t = Test cond tt tf} prf
    | Just ty_cond with (type_check gamma tt) proof tt_prf
      type_checking_sound {gamma} {t = Test cond tt tf} prf
      | Just ty_cond | Nothing = absurd prf
      type_checking_sound {gamma} {t = Test cond tt tf} prf
      | Just ty_cond | Just ty_t with (type_check gamma tf) proof tf_prf
        type_checking_sound {gamma} {t = Test cond tt tf} prf
        | Just ty_cond | Just ty_t | Nothing = absurd prf
        type_checking_sound {gamma} {t = Test cond tt tf} prf
        | Just ty_cond | Just ty_t | Just ty_f with (ty_cond)
          type_checking_sound {gamma} {t = Test cond tt tf} prf
          | Just ty_cond | Just ty_t | Just ty_f | TyBool
            with (beq_ty ty_t ty_f) proof ty_prf
              type_checking_sound {gamma} {t = Test cond tt tf} prf
              | Just ty_cond | Just ty_t | Just ty_f | TyBool | False =
                absurd prf
              type_checking_sound {gamma} {t = Test cond tt tf} prf
              | Just ty_cond | Just ty_t | Just ty_f | TyBool | True =
                rewrite sym (justInjective prf)
                in T_Test (type_checking_sound (sym cond_prf))
                          (type_checking_sound (sym tt_prf))
                          (rewrite beq_ty__eq {ty1=ty_t} {ty2=ty_f}
                                              (sym ty_prf)
                           in type_checking_sound (sym tf_prf))
          type_checking_sound {gamma} {t = Test cond tt tf} prf
          | Just ty_cond | Just ty_t | Just ty_f | TyArrow _ _ = absurd prf


text:
module Web.Internal.WebglTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace WebGLPowerPreference

  public export
  data WebGLPowerPreference = Default | LowPower | HighPerformance

  public export
  Show WebGLPowerPreference where
    show Default = "default"
    show LowPower = "low-power"
    show HighPerformance = "high-performance"

  public export
  Eq WebGLPowerPreference where
    (==) = (==) `on` show

  public export
  Ord WebGLPowerPreference where
    compare = compare `on` show

  public export
  read : String -> Maybe WebGLPowerPreference
  read "default" = Just Default
  read "low-power" = Just LowPower
  read "high-performance" = Just HighPerformance
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (WebGLPowerPreference.read s)}
             -> WebGLPowerPreference
  fromString s = fromJust $ read s

  export
  ToFFI WebGLPowerPreference String where
    toFFI = show

  export
  FromFFI WebGLPowerPreference String where
    fromFFI = read

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

export data WebGL2RenderingContext : Type where [external]

export
ToFFI WebGL2RenderingContext WebGL2RenderingContext where toFFI = id

export
FromFFI WebGL2RenderingContext WebGL2RenderingContext where fromFFI = Just

export
SafeCast WebGL2RenderingContext where
  safeCast = unsafeCastOnPrototypeName "WebGL2RenderingContext"

export data WebGLActiveInfo : Type where [external]

export
ToFFI WebGLActiveInfo WebGLActiveInfo where toFFI = id

export
FromFFI WebGLActiveInfo WebGLActiveInfo where fromFFI = Just

export
SafeCast WebGLActiveInfo where
  safeCast = unsafeCastOnPrototypeName "WebGLActiveInfo"

export data WebGLBuffer : Type where [external]

export
ToFFI WebGLBuffer WebGLBuffer where toFFI = id

export
FromFFI WebGLBuffer WebGLBuffer where fromFFI = Just

export
SafeCast WebGLBuffer where
  safeCast = unsafeCastOnPrototypeName "WebGLBuffer"

export data WebGLFramebuffer : Type where [external]

export
ToFFI WebGLFramebuffer WebGLFramebuffer where toFFI = id

export
FromFFI WebGLFramebuffer WebGLFramebuffer where fromFFI = Just

export
SafeCast WebGLFramebuffer where
  safeCast = unsafeCastOnPrototypeName "WebGLFramebuffer"

export data WebGLObject : Type where [external]

export
ToFFI WebGLObject WebGLObject where toFFI = id

export
FromFFI WebGLObject WebGLObject where fromFFI = Just

export
SafeCast WebGLObject where
  safeCast = unsafeCastOnPrototypeName "WebGLObject"

export data WebGLProgram : Type where [external]

export
ToFFI WebGLProgram WebGLProgram where toFFI = id

export
FromFFI WebGLProgram WebGLProgram where fromFFI = Just

export
SafeCast WebGLProgram where
  safeCast = unsafeCastOnPrototypeName "WebGLProgram"

export data WebGLQuery : Type where [external]

export
ToFFI WebGLQuery WebGLQuery where toFFI = id

export
FromFFI WebGLQuery WebGLQuery where fromFFI = Just

export
SafeCast WebGLQuery where
  safeCast = unsafeCastOnPrototypeName "WebGLQuery"

export data WebGLRenderbuffer : Type where [external]

export
ToFFI WebGLRenderbuffer WebGLRenderbuffer where toFFI = id

export
FromFFI WebGLRenderbuffer WebGLRenderbuffer where fromFFI = Just

export
SafeCast WebGLRenderbuffer where
  safeCast = unsafeCastOnPrototypeName "WebGLRenderbuffer"

export data WebGLRenderingContext : Type where [external]

export
ToFFI WebGLRenderingContext WebGLRenderingContext where toFFI = id

export
FromFFI WebGLRenderingContext WebGLRenderingContext where fromFFI = Just

export
SafeCast WebGLRenderingContext where
  safeCast = unsafeCastOnPrototypeName "WebGLRenderingContext"

export data WebGLSampler : Type where [external]

export
ToFFI WebGLSampler WebGLSampler where toFFI = id

export
FromFFI WebGLSampler WebGLSampler where fromFFI = Just

export
SafeCast WebGLSampler where
  safeCast = unsafeCastOnPrototypeName "WebGLSampler"

export data WebGLShader : Type where [external]

export
ToFFI WebGLShader WebGLShader where toFFI = id

export
FromFFI WebGLShader WebGLShader where fromFFI = Just

export
SafeCast WebGLShader where
  safeCast = unsafeCastOnPrototypeName "WebGLShader"

export data WebGLShaderPrecisionFormat : Type where [external]

export
ToFFI WebGLShaderPrecisionFormat WebGLShaderPrecisionFormat where toFFI = id

export
FromFFI WebGLShaderPrecisionFormat WebGLShaderPrecisionFormat where fromFFI = Just

export
SafeCast WebGLShaderPrecisionFormat where
  safeCast = unsafeCastOnPrototypeName "WebGLShaderPrecisionFormat"

export data WebGLSync : Type where [external]

export
ToFFI WebGLSync WebGLSync where toFFI = id

export
FromFFI WebGLSync WebGLSync where fromFFI = Just

export
SafeCast WebGLSync where
  safeCast = unsafeCastOnPrototypeName "WebGLSync"

export data WebGLTexture : Type where [external]

export
ToFFI WebGLTexture WebGLTexture where toFFI = id

export
FromFFI WebGLTexture WebGLTexture where fromFFI = Just

export
SafeCast WebGLTexture where
  safeCast = unsafeCastOnPrototypeName "WebGLTexture"

export data WebGLTransformFeedback : Type where [external]

export
ToFFI WebGLTransformFeedback WebGLTransformFeedback where toFFI = id

export
FromFFI WebGLTransformFeedback WebGLTransformFeedback where fromFFI = Just

export
SafeCast WebGLTransformFeedback where
  safeCast = unsafeCastOnPrototypeName "WebGLTransformFeedback"

export data WebGLUniformLocation : Type where [external]

export
ToFFI WebGLUniformLocation WebGLUniformLocation where toFFI = id

export
FromFFI WebGLUniformLocation WebGLUniformLocation where fromFFI = Just

export
SafeCast WebGLUniformLocation where
  safeCast = unsafeCastOnPrototypeName "WebGLUniformLocation"

export data WebGLVertexArrayObject : Type where [external]

export
ToFFI WebGLVertexArrayObject WebGLVertexArrayObject where toFFI = id

export
FromFFI WebGLVertexArrayObject WebGLVertexArrayObject where fromFFI = Just

export
SafeCast WebGLVertexArrayObject where
  safeCast = unsafeCastOnPrototypeName "WebGLVertexArrayObject"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data WebGLContextAttributes : Type where [external]

export
ToFFI WebGLContextAttributes WebGLContextAttributes where toFFI = id

export
FromFFI WebGLContextAttributes WebGLContextAttributes where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data WebGL2RenderingContextBase : Type where [external]

export
ToFFI WebGL2RenderingContextBase WebGL2RenderingContextBase where toFFI = id

export
FromFFI WebGL2RenderingContextBase WebGL2RenderingContextBase where fromFFI = Just

export data WebGL2RenderingContextOverloads : Type where [external]

export
ToFFI WebGL2RenderingContextOverloads WebGL2RenderingContextOverloads where toFFI = id

export
FromFFI WebGL2RenderingContextOverloads WebGL2RenderingContextOverloads where fromFFI = Just

export data WebGLRenderingContextBase : Type where [external]

export
ToFFI WebGLRenderingContextBase WebGLRenderingContextBase where toFFI = id

export
FromFFI WebGLRenderingContextBase WebGLRenderingContextBase where fromFFI = Just

export data WebGLRenderingContextOverloads : Type where [external]

export
ToFFI WebGLRenderingContextOverloads WebGLRenderingContextOverloads where toFFI = id

export
FromFFI WebGLRenderingContextOverloads WebGLRenderingContextOverloads where fromFFI = Just


text:
module Parser.Package

import public Parser.Lexer.Package
import public Parser.Rule.Package
import public Libraries.Text.Lexer
import public Libraries.Text.Parser
import public Parser.Support

import Core.Core
import Core.FC
import Core.Name.Namespace
import System.File

%default total

export
runParser : (fname : String) -> (str : String) -> Rule ty -> Either Error ty
runParser fname str p
    = do toks   <- mapFst (\err => fromLexError
                     (PhysicalPkgSrc fname) (NoRuleApply, err)) $ lex str
         (_, val, _) <- mapFst (fromParsingErrors (PhysicalPkgSrc fname)) $ parse p toks
         Right val

export
covering
parseFile : (fname : String) -> Rule ty -> IO (Either Error ty)
parseFile fname p
    = do Right str <- readFile fname
             | Left err => pure (Left (FileErr fname err))
         pure (runParser fname str p)


text:
data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

noFinZ : Fin Z -> Void
noFinZ FZ impossible
noFinZ (FS k) impossible

noFinZ' : Fin Z -> Void
noFinZ' x impossible

noEmpty : Void -> Fin Z
noEmpty t impossible


text:
module Data.Time.LocalTime.Internal.LocalTime

import Data.Time.Calendar.Days
import Data.Time.Calendar.Gregorian
import Data.Time.Clock.DiffTime
import Data.Time.Clock.Internal.UTCTime
import Data.Time.LocalTime.TimeZone
import Data.Time.LocalTime.TimeOfDay

import Generics.Derive

%default total
%language ElabReflection

-- --------------------------------------------------------------------------

||| A simple day and time aggregate, where the day is of the specified parameter,
||| and the time is a TimeOfDay.
||| Conversion of this (as local civil time) to UTC depends on the time zone.
||| Conversion of this (as local mean time) to UT1 depends on the longitude.
public export
record LocalTime where
  constructor MkLocalTime
  localDay : Day
  localTimeOfDay : TimeOfDay
%runElab derive "LocalTime" [Generic, Eq, Ord, DecEq]

public export
Show LocalTime where
  show x = show x.localDay ++ " " ++ show x.localTimeOfDay

-- --------------------------------------------------------------------------

||| Get the local time of a UTC time in a time zone.
export utcToLocalTime : TimeZone -> UTCTime -> LocalTime
utcToLocalTime tz (MkUTCTime day dt) = let
  (i, tod) = utcToLocalTimeOfDay tz (timeToTimeOfDay dt)
  in MkLocalTime (addDays i day) tod

||| Get the UTC time of a local time in a time zone.
export localTimeToUTC : TimeZone -> LocalTime -> UTCTime
localTimeToUTC tz (MkLocalTime day tod) = let
  (i, todUTC) = localToUTCTimeOfDay tz tod
  in MkUTCTime (addDays i day) (timeOfDayToTime todUTC)

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Main

import Effects
import Effect.State

data BTree a = Leaf
             | Node (BTree a) a (BTree a)

Show a => Show (BTree a) where
    show Leaf = "[]"
    show (Node l x r) = "[" ++ show l ++ " "
                            ++ show x ++ " "
                            ++ show r ++ "]"

testTree : BTree String
testTree = Node (Node Leaf "Jim" Leaf)
                "Fred"
                (Node (Node Leaf "Alice" Leaf)
                      "Sheila"
                      (Node Leaf "Bob" Leaf))

-- treeTag : (i : Int) -> BTree a -> BTree (Int, a)

-- treeTagAux : (i : Int) -> BTree a -> (Int, BTree (Int, a))
-- treeTagAux i Leaf = (i, Leaf)
-- treeTagAux i (Node l x r)
--        = let (i', l') = treeTagAux i l in
--          let x' = (i', x) in
--          let (i'', r') = treeTagAux (i' + 1) r in
--              (i'', Node l' x' r')

treeTagAux : BTree a -> Eff (BTree (Int, a)) [STATE Int]
treeTagAux Leaf = pure Leaf
treeTagAux (Node l x r)
    = do l' <- treeTagAux l
         i <- get
         put (i + 1)
         r' <- treeTagAux r
         pure (Node l' (i, x) r')

-- treeTag : (i : Int) -> BTree a -> BTree (Int, a)
-- treeTag i x = snd (treeTagAux i x)

treeTag : (i : Int) -> BTree a -> BTree (Int, a)
treeTag i x = runPure (do put i
                          treeTagAux x)

main : IO ()
main = print (treeTag 1 testTree)

max_stars_repo_name: asmodehn/idris-playground

max_issues_repo_name: asmodehn/idris-playground

max_forks_repo_name: asmodehn/idris-playground


text:
module Main

import Effect.Select

no_attack : (Int, Int) -> (Int, Int) -> Bool
no_attack (x, y) (x', y')
   = x /= x' && y /= y' && abs (x - x') /= abs (y - y')

rowsIn : Int -> List (Int, Int) -> List Int
rowsIn col qs = [ x | x <- [1..8], all (no_attack (x, col)) qs ]

addQueens : Int -> List (Int, Int) -> { [SELECT] } Eff m (List (Int, Int))
addQueens 0   qs = return qs
addQueens col qs = do row <- select (rowsIn col qs)
                      addQueens (col - 1) ((row, col) :: qs)

getQueens : Maybe (List (Int, Int))
getQueens = run (addQueens 8 [])

main : IO ()
main = do let qs = getQueens
          putStrLn ("Solution:\n" ++ show qs)

--           let num = the Integer (cast (length qs))
--           putStrLn (show num ++ " solutions:\n" ++ showAll qs)
--     where showAll [] = ""
--           showAll (x :: xs) = show x ++ "\n" ++ showAll xs

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module lib.Library3

import lib.Library2

export
salute : String
salute = "Hello, I'm library 3, and I can also talk with library 2:\n" ++ salute2


text:
module Fib

%access export
%default total

namespace Preloaded

  %access public export
  %default total

  fibAux : Nat -> Nat -> Nat -> Nat
  fibAux a b Z = a
  fibAux a b (S n) = fibAux b (a + b) n

  fib2 : Nat -> Nat
  fib2 = fibAux 0 1

fibEq : (n : Nat) -> fib2 n = fib n
fibEq = auxInter Z where
  auxInter : (l, k : Nat) -> fibAux 0 1 (l + k) = fibAux (fib k) (fib (S k)) l
  auxInter l Z     = rewrite plusZeroRightNeutral l in Refl
  auxInter l (S k) = rewrite sym $ plusSuccRightSucc l k in
                     rewrite plusCommutative (fib (S k)) (fib k) in
                     auxInter (S l) k

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import System.Concurrency.Channels

-- check that all functions are total
%default total

data Message = Add Nat Nat

data MessagePID = MkMessage PID

data Process : Type -> Type where
  Action : IO a -> Process a
  Pure : a -> Process a
  (>>=) : Process a -> (a -> Process b) -> Process b
  Spawn : Process () -> Process (Maybe MessagePID)
  Request : MessagePID -> Message -> Process (Maybe Nat)
  Respond : ((msg : Message) -> Process Nat) -> Process (Maybe Message)
  Loop : Inf (Process a) -> Process a

partial
run : Process t -> IO t
run (Action act) = act
run (Pure val) = pure val
run (act >>= next) = do x <- run act
                        run (next x)
run (Spawn proc) = do Just pid <- spawn (run proc)
                      | Nothing => pure Nothing
                      pure (Just (MkMessage pid))
run (Request (MkMessage pid) msg)
  = do Just chan <- connect pid
       | _ => pure Nothing
       ok <- unsafeSend chan msg
       if ok then do Just x <- unsafeRecv Nat chan
                     | Nothing => pure Nothing
                     pure (Just x)
              else pure Nothing
run (Respond calc)
  = do Just sender <- listen 1
       | Nothing => pure Nothing
       Just msg <- unsafeRecv Message sender
       | Nothing => pure Nothing
       res <- run (calc msg)
       unsafeSend sender res
       pure (Just msg)
run (Loop act) = run act

procAdder : Process ()
procAdder = do Respond (\msg => case msg of
                                  Add x y => Pure (x + y))
               Loop procAdder

procMain : Process ()
procMain = do Just adder_id <- Spawn procAdder
              | Nothing => Action (putStrLn "Spawn failed")
              Just answer <- Request adder_id (Add 2 3)
              | Nothing => Action (putStrLn "Request failed")
              Action (printLn answer)

-- run with:
-- :exec run procMain

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
> module SequentialDecisionProblems.TabBackwardsInductionOptDefaults1

> import Data.Vect

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.TabBackwardsInduction1
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.CoreTheoryOptDefaults

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Opt.Operations
> import Rel.TotalPreorder
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Vect.Operations
> import Vect.Properties
> import Decidable.Predicates

> %default total
> %access public export
> %auto_implicits off

> SequentialDecisionProblems.TabBackwardsInduction1.tabCvalargmax {n} x r v ps =
>   Opt.Operations.argmax totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (tabCval x r v ps)

> |||
> goodCtrl : {t, m : Nat} ->
>            (x : State t) -> .(r : Reachable x) -> .(v : Viable (S m) x) ->
>            PolicyTable t (S m) -> GoodCtrl t x m
> goodCtrl {t} {m} x r v pt =
>   let xs   : Vect (cardState t) (State t)
>            = vectState t in
>   let prf  : Elem x xs
>            = toVectComplete (finiteState t) x in
>   let rvxs : Vect (cardReachableAndViableState t (S m)) (State t)
>            = map outl (vectReachableAndViableState t (S m)) in
>   let dRV  : ((x : State t) -> Dec (ReachableAndViable (S m) x))
>            = decidableReachableAndViable (S m) in
>   let prf' : Elem x rvxs
>            = filterTagSigmaLemma {P = ReachableAndViable (S m)} dRV x xs prf (r,v) in
>   let k    : Fin (cardReachableAndViableState t (S m))
>            = lookup x rvxs prf' in
>   let x'   : State t
>            = outl (index k pt) in
>   let gy'  : GoodCtrl t x' m
>            = snd (outr (index k pt)) in
>   let gy   : GoodCtrl t x m
>            = replace {P = \ X => GoodCtrl t X m} (believe_me gy') gy' in
>   gy

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Bautzen.SExp

import Data.List
import Data.Nat
import Data.Vect
import Control.WellFounded

public export
data SExp : Type where
  SList : List SExp -> SExp
  SSym : String -> SExp
  SStr : String -> SExp
  SInt : Int -> SExp

||| Conversion utility from a type to a `SExp`
public export
interface ToSExp a where
  toSExp : a -> SExp

export
ToSExp SExp where
  toSExp = id

export
ToSExp Unit where
  toSExp () = SList []

export
ToSExp String where
  toSExp = SStr

export
ToSExp Int where
  toSExp = SInt

export
ToSExp Bool where
  toSExp True = SSym "t"
  toSExp False = SSym "nil"

export
ToSExp Integer where
  toSExp = SInt . fromInteger

export
ToSExp Nat where
  toSExp = SInt . cast

export
ToSExp (Fin n) where
  toSExp = SInt . fromInteger . cast

export
(ToSExp a, ToSExp b) => ToSExp (a, b) where
  toSExp (a, b) = SList [ toSExp a, toSExp b ]

export
ToSExp a => ToSExp (Maybe a) where
  toSExp Nothing = SSym "nil"
  toSExp (Just a) = toSExp a

export
ToSExp a => ToSExp (List a) where
  toSExp = SList . map toSExp

export
ToSExp a => ToSExp (Vect n a) where
  toSExp = toSExp . toList

export
(ToSExp a, ToSExp b) => ToSExp (Either a b) where
  toSExp (Left l) = SList [ SSym ":error", toSExp l ]
  toSExp (Right r) = SList [ SSym ":ok", toSExp r ]

export
Show SExp where
  show (SList xs) = "(" ++ showList xs ++ ")"
    where
      showList : List SExp -> String
      showList [] = ""
      showList [x] = show x
      showList (x :: xs) = show x ++ " " ++ showList xs
  show (SStr x)   = show x
  show (SSym x)   = ":" ++ x
  show (SInt x)   = show x

export
Eq SExp where
  (SList []) == (SList []) = True
  (SList (x :: xs)) == (SList (x' :: xs')) = x == x' && equal xs xs'
    where
      equal : List SExp -> List SExp -> Bool
      equal [] [] = True
      equal (x :: xs) (y :: ys) = x == y && equal xs ys
      equal _ _ = False

  (SStr x) == (SStr x') = x == x'
  (SSym x) == (SSym x') = x == x'
  (SInt x) == (SInt x') = x == x'
  _ == _ = True

mutual
  private
  step : (x1 : List SExp) -> ((y : List SExp) -> Smaller y x1 -> Either String (List String)) -> Either String (List String)
  step []        f = Right []
  step (x :: xs) f with (isLTE (length xs) (length xs))
    step (x :: xs) f | Yes prf = do s <- toStrings x
                                    ss <- f xs $ LTESucc prf
                                    pure $ s ++ ss
    step (x :: xs) f | No contra = absurd (contra lteRefl)

  ||| Convert a s-expression into a list of strings
  |||
  ||| This function actually _flattens_ the given s-expression, traversing it depth-first and
  ||| expecting to find only _strings_.
  |||
  ||| * A single string is converted as a singleton
  ||| * A list of strings is converted as a list
  ||| * Any other type raises an error
  export
  toStrings : SExp -> Either String (List String)
  toStrings (SStr x) = pure [ x ]
  toStrings (SSym x) = Left $ "Unexpected symbol "++ x ++ ", wanted a string"
  toStrings (SInt x) = Left $ "Unexpected int "++ show x ++ ", wanted a string"
  toStrings (SList x) = sizeRec step x

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames