text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Tests

import Tester
import Tester.Runner

import Parser
import Lexer
import Files
import Process

tests : List Test
tests = Lexer.tests
     ++ Parser.tests
     ++ Files.tests
     ++ Process.tests

main : IO ()
main = do
    success <- runTests Tests.tests
    if success
        then putStrLn "All tests passed."
        else putStrLn "Not all tests passed."

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
||| JSON parser/ADT
||| Reference: https://www.json.org/json-en.html
module Extra.Json

import Extra.Parser
import Extra.Alternative
import Extra.Scientific
import Extra.Applicative
import Debug.Trace
import Data.Fin
import Data.List

||| A JSON value
public export
data Value : Type where
  MkString : String -> Value
  MkObject : List (String, Value) -> Value
  MkArray : List Value -> Value
  MkNumber : Scientific -> Value
  MkBoolean : Bool -> Value
  MkNull : Value

export
Show Value where
  show (MkString str) = show str
  show (MkNumber scientific) = show scientific
  show (MkArray array) = "[" <+> (concat $ intersperse "," $ map show array) <+> "]"
  show (MkObject obj) = "{" <+> (concat $ intersperse "," $ map (\(a, b) => show a <+> ":" <+> show b) obj) <+> "}"
  show (MkBoolean False) = "false"
  show (MkBoolean True) = "true"
  show MkNull = "null"

export
oneNineP : Stream i Char => Parser i Integer
oneNineP = (token '1' $> 1) <|> (token '2' $> 2) <|> (token '3' $> 3)
       <|> (token '4' $> 4) <|> (token '5' $> 5) <|> (token '6' $> 6)
       <|> (token '7' $> 7) <|> (token '8' $> 8) <|> (token '9' $> 9)

export
digitP : Stream i Char => Parser i Integer
digitP = (token '0' $> 0) <|> oneNineP

export
digitsP : Stream i Char => Parser i Integer
digitsP = map snd helper
  where
  helper : Parser i (Integer, Integer)
  helper = do
    d <- digitP
    maybe_ds <- optional helper
    case maybe_ds of
      Nothing => pure (1, d)
      Just (n, ds) => let n' = n * 10 in pure (n', d * n' + ds)

export
integerP : Stream i Char => Parser i Integer
integerP = do
  b <- option 1 (token '-' $> (-1))
  n <- (token '0' $> 0) <|> digitsP
  pure $ b * n

export
signP : Stream i Char => Parser i Integer
signP = (token '+' $> 1) <|> (token '-' $> -1)

export
numberP : Stream i Char => Parser i Scientific
numberP = do
  pre <- integerP
  dec <- option 0 $ token '.' *> digitsP
  exp <- option 0 $ (token 'e' <|> token 'E') *> ((*) <$> (signP <|> pure 1) <*> digitsP)
  let a = MkScientific pre exp
  let b = asDecimal dec
  pure $ a + if pre < 0 then -b else b

export
whitespaceP : Stream i Char => Parser i ()
whitespaceP = many space $> ()

export
boolP : Stream i Char => Parser i Bool
boolP = (string "true" $> True) <|> (string "false" $> False)

export
escapeP : Stream i Char => Parser i Char
escapeP = (token '\\')
  <|> (token '/')
  <|> (token 'b' $> '\b')
  <|> (token 'f' $> '\f')
  <|> (token 'n' $> '\n')
  <|> (token 'r' $> '\r')
  <|> (token 't' $> '\t')

export
characterP : Stream i Char => Parser i Char
characterP = notFollowedBy (token '"') *> ((token '\\' *> escapeP) <|> utf16 <|> (notFollowedBy (token '\\') *> anyToken))
  where
  hex : Parser i Int
  hex = (cast . finToInteger) <$> hexDigit
  code : Parser i Int
  code = do
    skip (token '\\' *> token 'u')
    b1 <- hex; b2 <- hex; b3 <- hex; b4 <- hex
    pure $ b1 * 0x1000 + b2 * 0x100 + b3 * 0x10 + b4
  utf16 : Parser i Char
  utf16 = do
    code >>= \high => case (0xD800 <= high && high <= 0xDBFF) of
      False => pure $ chr high
      True => code >>= \low => case 0xDC00 <= low && low <= 0xDFFF of
        False => fail "utf16 no low surrogate"
        True => pure $ chr $ 0x10000 + (high - 0xD800) * 0x400 + (low - 0xDC00)

export
charactersP : Stream i Char => Parser i String
charactersP = (strCons <$> characterP <*>| charactersP) <|> pure neutral

export
stringP : Stream i Char => Parser i String
stringP = token '"' *> charactersP <* token '"'

export
nullP : Stream i Char => Parser i Value
nullP = string "null" $> MkNull

mutual
  export
  elementP : Stream i Char => Parser i Value
  elementP = whitespaceP *> valueP <* whitespaceP

  export
  elementsP : Stream i Char => Parser i (List Value)
  elementsP =
    ((::) <$> elementP <*>| (token ',' *> elementsP))
    <|> (pure <$> elementP)

  export
  memberP : Stream i Char => Parser i (String, Value)
  memberP = (,) <$> (whitespaceP *> stringP <* whitespaceP) <*> (token ':' *> elementP)

  export
  membersP : Stream i Char => Parser i (List (String, Value))
  membersP = ((::) <$> memberP <*>| (token ',' *> membersP)) <|> (pure <$> memberP)

  export
  arrayP : Stream i Char => Parser i (List Value)
  arrayP = (token '[' *> (whitespaceP $> []) <* token ']')
       <|> (token '[' *> elementsP <* token ']')

  export
  objectP : Stream i Char => Parser i (List (String, Value))
  objectP = (token '{' *> (whitespaceP $> []) <* token '}')
        <|> (token '{' *> membersP <* token '}')

  export
  valueP : Stream i Char => Parser i Value
  valueP = whitespaceP *> ((MkString <$> stringP)
                       <|> (MkNumber <$> numberP)
                       <|> (MkArray <$> arrayP))
                       <|> (MkBoolean <$> boolP)
                       <|> (MkObject <$> objectP)
                       <|> nullP

ext: idr


text:
module Main

import Data.Strings

lorem : String
lorem = "Lorem ipsum dolor sit amet, consectetur adipiscing elit, sed do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum."

partial
main : IO ()
main = do
  printLn (prim__strIndex lorem 10)
  printLn (prim__strIndex lorem 50)
  printLn (prim__strIndex lorem 100)
  printLn (prim__strIndex lorem 200)


text:
module Ipkg.Rule

import Ipkg.Lexer

import Text.Parser

public export
Rule : Type -> Type
Rule a = Grammar () PkgToken True a

public export
EmptyRule : Type -> Type
EmptyRule a = Grammar () PkgToken False a

export
comment : Rule String
comment = terminal "Expected comment" $
  \case Comment i => Just i
        _ => Nothing

export
exact : String -> Rule String
exact s = terminal "Expected exactly \{s}" $
  \case Identifier s' => if s == s' then Just s else Nothing
        _ => Nothing

export
identifier : Rule String
identifier = terminal "Expected an Identifier" $
  \case Identifier s => Just s
        _ => Nothing

export
op' : Rule String
op' = terminal "Expected an Operator" $
  \case Operator s => Just s
        _ => Nothing

export
op : String -> Rule ()
op s = terminal "Expected operator \{s}" $
  \case Operator s' => if s == s' then Just () else Nothing
        _ => Nothing

sep' : Rule ()
sep' = terminal "Expected ','" $
  \case Separator => Just ()
        _ => Nothing

export
sep : Rule t -> Rule (List t)
sep r = forget <$> sepBy1 sep' r

export
space : Rule ()
space = terminal "Expected ','" $
  \case Space => Just ()
        _ => Nothing

export
dot : Rule ()
dot = terminal "Expected '.'" $
  \case Dot => Just ()
        _ => Nothing

export
equals : Rule ()
equals = terminal "Expected '='" $
  \case Equals => Just ()
        _ => Nothing

export
stringLit : Rule String
stringLit = terminal "Expected string" $
  \case StringLit s => Just s
        _ => Nothing

export
nat : Rule Nat
nat = terminal "Expected integer" $
  \case NatLit i => Just i
        _ => Nothing

export
property : String -> Rule ()
property s = ignore (exact s) >> equals

max_stars_repo_name: claymager/ipkg-to-json

max_issues_repo_name: claymager/ipkg-to-json

max_forks_repo_name: claymager/ipkg-to-json


text:
module LeftistHeap

import Heap

%default total
%access private

export
data LeftistHeap a = E | T Int a (LeftistHeap a) (LeftistHeap a)

rank : LeftistHeap a -> Int
rank E           = 0
rank (T r _ _ _) = r

makeT : a -> LeftistHeap a -> LeftistHeap a -> LeftistHeap a
makeT x a b = if rank a >= rank b then T (rank b + 1) x a b
              else T (rank a + 1) x b a

export
Heap LeftistHeap where
  empty = E
  isEmpty E = True
  isEmpty _ = False

  insert x h = merge (T 1 x E E) h

  merge h  E  = h
  merge E  h  = h
  merge h1@(T _ x a1 b1) h2@(T _ y a2 b2) =
    if x <= y then makeT x a1 (merge b1 h2)
    else makeT y a2 (merge h1 b2)

  findMin E = idris_crash "empty heap"
  findMin (T _ x a b) = x

  deleteMin E = idris_crash "empty heap"
  deleteMin (T _ x a b) = merge a b


text:
module Cordial.Model.Common.WireTy

import Data.Ranged

import Cordial.Model.Common.Essential

%default total
%access public export

||| Type of wire.
data WireTy : Type where
   ||| Does the wire carry memory mapable data or addresses
   Data : Bool -> WireTy

   ||| Clock for the interface
   Clock : (edge  : Maybe ClockEdge)
        -> (delay : Maybe Delay)
        -> (phase : Maybe (RangedNat 0 100))
        -> WireTy

   Reset : WireTy

   Information : WireTy
   Interrupt : WireTy
   Control   : WireTy
   General   : WireTy

DataWire : WireTy
DataWire = Data False

AddressWire : WireTy
AddressWire = Data True

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module G3MiddleFunctionsWinter

import G4LowerFormalPSpring

%access public export
%default total

-- 【後から気づいた】形式的体系P の関数を使って実装する必要は無い、原始再帰的であれば良い
-- 本での「述語」は「特性関数（Bool値を返す）」にする
-- 10.8.2 整数論
-- 1
canDivide : GNat -> GNat -> Bool
canDivide x d = canDivide' x d x where
  canDivide' x d Z     = False
  canDivide' x d (S n) = if x == d * (S n) then True else canDivide' x d n
-- 2
isPrime : GNat -> Bool
isPrime Z         = False
isPrime (S Z)     = False
isPrime (S (S x)) = isPrime' (S (S x)) (S (S x)) where
  isPrime' x Z     = True
  isPrime' x (S d) = if not ((S d) == 1) && not ((S d) == x) && canDivide x (S d) then False else isPrime' x d
-- 3
prime : GNat -> GNat -> GNat
prime Z     _ = 0
prime (S n) x = prime' n x Z x where
  prime' _ _ _ Z           = 0
  prime' n x p (S stopper) = if p == x + 1 then 0 else if prime n x < p && canDivide x p && isPrime p then p else prime' n x (S p) stopper
-- 4
factorial : GNat -> GNat
factorial Z     = 1
factorial (S n) = (S n) * factorial n
-- 5
pri : GNat -> GNat
pri Z     = 0
pri (S n) = pri' n Z ((factorial $ pri n) + 1 + 1) where
  pri' _ _  Z           = 0
  pri' n pp (S stopper) = if pri n < pp && isPrime pp then pp else pri' n (S pp) stopper
-- 10.8.3 列
-- 6
elem : GNat -> GNat -> GNat
elem x n = elem' x n Z (x + 1) where
  elem' _ _ _ Z           = 0
  elem' x n k (S stopper) = if canDivideByPower x n k && canDivideByPower x n (S k) then k else elem' x n (S k) stopper where
    canDivideByPower x n k  = canDivide x $ power (prime n x) k
-- 7
len : GNat -> GNat
len x = len' x Z (x + 1) where
  len' _ _ Z           = 0
  len' x k (S stopper) = if 0 < prime k x && 0 == prime (k + 1) x then k else len' x (S k) stopper
-- 8
comb : GNat -> GNat -> GNat
comb x y = comb' x y Z (m8 x y + 1) where
  m8 : GNat -> GNat -> GNat
  m8 x y = power (pri (len x + len y)) (plus x y)
  comb' : GNat -> GNat -> GNat -> GNat -> GNat
  comb' _ _ _ Z           = 0
  comb' x y z (S stopper) =
    if combSub1 Z (len x + 1) /= 0 then
      if combSub2 Z (len y + 1) /= 0 then z else comb' x y (S z) stopper
    else comb' x y (S z) stopper where
      combSub1 _ Z           = 0
      combSub1 m (S stopper) = if m < len x + 1 && 0 < m && elem z m == elem x m then 1 else combSub1 (S m) stopper
      combSub2 _ Z           = 0
      combSub2 n (S stopper) = if n < len y + 1 && 0 < n && elem z (len x + n) == elem y n then 1 else combSub2 (S n) stopper
-- 9
seq : GNat -> GNat
seq = power 2
-- 10
paren : GNat -> GNat
paren x = seq 左かっこ * x * seq 右かっこ
-- 10.8.4 変数・記号・論理式


text:
module Test.Data.JSError

import Data.JSError

%lib Node "fs"

readFile : String -> JS_IO ()
readFile path = foreign FFI_JS "fs.readFileSync(%0)" (String -> JS_IO ()) path

err : JSError
err = mkError "Foobar"

namespace Main
  export
  main : JS_IO ()
  main = do
    putStrLn' (message err)
    putStrLn' (show $ isJust $ stack err)
    catch (putStrLn' . show) $ readFile "non-existent-file"
    catch (putStrLn' . message) $ throw err

max_stars_repo_name: Risto-Stevcev/idris-jserror

max_issues_repo_name: Risto-Stevcev/idris-jserror

max_forks_repo_name: Risto-Stevcev/idris-jserror


text:
module A

-- Check that this doesn't go into a loop when resolving Show. because
-- f itself is a candidate when elaborating the top level f function!
public export
interface F (p : Type -> Type) where
  f : Show a => p a -> a


text:
module AssRecRule

import Data.Fin
import Data.Vect

%default total
%access public export

recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base fn [] = base
recList a x base fn (y :: xs) = fn y xs (recList a x base fn xs)

mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f lst = recList a (List b) []
      (\q => \lsta => \lstb => (f q) :: lstb) lst

foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op xs = recList a a init (\q => \lst => op q) xs

inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S k) FZ = base k
inducFin xs base step (S k) (FS x) = step k x (inducFin xs base step k x)

fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j vect = inducFin (\n => \q => Vect n a -> a)
                       (\m => \(x :: xs) => x)
                       (\p => \k => \prev => \(x :: xs) => prev xs)
                       q j vect


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 14

-- check that all functions are total
%default total

--
-- section 14.1
-- see DoorJam.idr
--

--
-- section 14.2
-- see ATM.idr
--

-- section 14.3
-- see Hangman.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Graphics.Util.ObjLoader

import Control.Monad.Identity

import Data.SortedMap as M

import Lightyear
import Lightyear.Combinators
import Lightyear.Strings
import Lightyear.Char

import Graphics.Util.Mesh

%access private

vtx : Double -> Double -> Double -> Vec3
vtx x y z = [x, y, z]

uv : Double -> Double -> Vec2
uv u v = [u, v]

Index : Type
Index = (Int, Int, Int)

export
data ObjLine
  = Position Vec3
  | TextureCoord Vec2
  | Normal Vec3
  | Face Index Index Index
  | Comment String
  | Ignored String

implementation Show ObjLine where
  show (Position v)       = "Position " ++ (show v)
  show (TextureCoord uv)  = "TextureCoord " ++ (show uv)
  show (Normal v)         = "Normal " ++ (show v)
  show (Face v1 v2 v3)    = "Face " ++ (show v1) ++ " " ++ (show v2) ++ " " ++ (show v3)
  show (Comment s)        = "Comment " ++ s
  show (Ignored s)        = "Ignored " ++ s

-- ------------------------------------------------------------------ [ Tokens ]

notEol : Monad m => ParserT String m Char
notEol = satisfy (\s => not (isNL s))

eol : Monad m => ParserT String m Char
eol = satisfy (\s => not (isNL s))

-- ---------------------------------------------------------- [ Double Parser ]
-- borrowed wholesale from https://github.com/ziman/lightyear/blob/master/examples/Json.idr
--
record Scientific where
  constructor MkScientific
  coefficient : Integer
  exponent : Integer

scientificToFloat : Scientific -> Double
scientificToFloat (MkScientific c e) = fromInteger c * exp
  where exp = if e < 0 then 1 / pow 10 (fromIntegerNat (- e))
                       else pow 10 (fromIntegerNat e)

parseScientific : Parser Scientific
parseScientific = do sign <- maybe 1 (const (-1)) `map` opt (char '-')
                     digits <- some digit
                     hasComma <- isJust `map` opt (char '.')
                     decimals <- if hasComma then some digit else pure Prelude.List.Nil
                     hasExponent <- isJust `map` opt (char 'e')
                     exponent <- if hasExponent then integer else pure 0
                     pure $ MkScientific (sign * fromDigits (digits ++ decimals))
                                         (exponent - cast (length decimals))
  where fromDigits : List (Fin 10) -> Integer
        fromDigits = foldl (\a, b => 10 * a + cast b) 0

double : Parser Double
double = map scientificToFloat parseScientific

-- ---------------------------------------------------------- [ OBJ Format ]

position : Parser ObjLine
position = do token "v"
              x <- lexeme double
              y <- lexeme double
              z <- lexeme double
              pure $ Position $ vtx x y z

normal : Parser ObjLine
normal = do token "vn"
            x <- lexeme double
            y <- lexeme double
            z <- lexeme double
            pure $ Normal $ vtx x y z

textureCoord : Parser ObjLine
textureCoord= do token "vt"
                 u <- lexeme double
                 v <- lexeme double
                 pure $ TextureCoord $ uv u v

faceVertex : Parser (Int, Int, Int)
faceVertex = do vertexIdx <- integer
                char '/'
                textureIdx <- integer
                char '/'
                normalIdx <- integer
                pure $ (vertexIdx, textureIdx, normalIdx)

face : Parser ObjLine
face = do token "f"
          (v3 :: v2 :: v1 :: []) <- ntimes 3 (lexeme faceVertex)
          pure $ Face v1 v2 v3

ignored : Parser ObjLine
ignored = do cont <- (many notEol) <?> "ignored"
             pure $ Ignored (cast cont)

comment : Parser ObjLine
comment = do string "#"
             cont <- many notEol
             pure $ Comment $ cast cont

line : Parser ObjLine
line = position <|> normal <|> textureCoord <|> face <|> comment <|> ignored

parseLine : String -> List ObjLine
parseLine input = case parse line input of
  Left  e => [] -- ignore Errors for now
  Right x => [x]

processLines : List ObjLine -> (List Vec3, List Vec3, List Vec2, List Index)
processLines lines = processLines' lines [] [] [] []
                   where processLines' : List ObjLine
                                       -> List Vec3 -- positions
                                       -> List Vec3 -- normals
                                       -> List Vec2     -- UVs / TextureCoordinates
                                       -> List Index -- indices
                                       -> (List Vec3, List Vec3, List Vec2, List Index)
                         processLines' []         pos norm uvs ind = (reverse pos, reverse norm, reverse uvs, reverse ind)
                         processLines' (l :: ls)  pos norm uvs ind = case l of
                           Position v      => processLines' ls (v :: pos)       norm        uvs                     ind
                           Normal v        => processLines' ls       pos  (v :: norm)       uvs                     ind
                           TextureCoord uv => processLines' ls       pos        norm (uv :: uvs)                    ind
                           Face i1 i2 i3   => processLines' ls       pos        norm        uvs  (i1 :: i2 :: i3 :: ind)
                           _               => processLines' ls       pos        norm        uvs                     ind

mapByIndex : List a -> M.SortedMap Int a
mapByIndex [] = M.empty
mapByIndex (x :: xs) = mapByIndex' (cast $ (length xs)) empty (reverse (x :: xs))
                where mapByIndex' : Int -> SortedMap Int a -> List a -> SortedMap Int a
                      mapByIndex' _ s        [] = s
                      mapByIndex' i s (x :: xs) = mapByIndex' (i-1) (insert i x s) xs

record VertexData where
  constructor MkData
  position : Vec3
  uv       : Vec2
  normal   : Vec3

getData : Index
          -> M.SortedMap Int Vec3
          -> M.SortedMap Int Vec3
          -> M.SortedMap Int Vec2
          -> Maybe VertexData
getData (p,t,n) positions normals uvs = do
  position <- lookup (p-1) positions
  normal   <- lookup (n-1) normals
  uv       <- lookup (t-1) uvs
  pure $ MkData position uv normal

toVects : List VertexData -> (Vect n Vec3, Vect n Vec2, Vect n Vec3)
toVects {n = Z}   []        = ([], [], [])
toVects {n = S m} (x :: xs) with (toVects {n=m} xs )
  | (ps, uvs, norms) = ((position x) :: ps, (uv x) :: uvs, (normal x) :: norms )

-- input is: a list of indices (triples of indices) and the Map with the vertexData for the indices
-- output will be: a list of Results for the vertex data and a list of indices for the vertex data
processFace : List Index
              -> M.SortedMap Int Vec3
              -> M.SortedMap Int Vec3
              -> M.SortedMap Int Vec2
              -> Int
              -> M.SortedMap Index Int        -- maps the given index v/t/n to the actual result index
              -> M.SortedMap Int VertexData   -- maps the given result index to the actual vertex data
              -> List Int                     -- the index buffer
              -> (List Int, List VertexData)
processFace []         _ _ _  _   indices vData buffer = (reverse buffer, (map snd $ toList vData))
processFace (f::faces)  p n t cnt indices vData buffer = case (lookup f indices) of
  Just i  => processFace faces p n t cnt indices vData (i :: buffer)
  Nothing => case (getData f p n t ) of
    Just vd => processFace faces p n t (cnt+1) (insert f cnt indices) (insert cnt vd vData) (cnt :: buffer)
    Nothing => processFace faces p n t cnt indices vData buffer -- ignore face: should not be possible

computeModel : List ObjLine -> Mesh
computeModel objLines =
  let
    (positions, normals, uvs, indices) = processLines objLines
    mappedPositions  = mapByIndex positions  -- Map Int Vertex
    mappedNormals    = mapByIndex normals    -- Map Int Vertex
    mappedUvs        = mapByIndex uvs        -- Map Int UV
    positionIndices = reverse $ map fst indices
    (posn, vData) = processFace indices mappedPositions mappedNormals mappedUvs 0 M.empty M.empty []

    (positions, uvs, norms) = toVects {n=length vData} vData

  in UvMesh positions norms uvs posn

export
loadObj : (filename: String) -> IO (Either FileError Mesh)
loadObj fname = do Right handle <- openFile fname Read | Left err => pure (Left err)
                   objLines <- parseFile' handle []
                   closeFile handle
                   pure $ Right (computeModel objLines)
                where
                   partial
                   parseFile' : File -> List ObjLine -> IO (List ObjLine)
                   parseFile' h acc =
                     do x <- fEOF h
                        if not x then do Right l <- fGetLine h | Left err => pure acc
                                         parseFile' h ((parseLine l) ++ acc)
                        else pure $ reverse acc

max_stars_repo_name: xiphiness/gl-idris

max_issues_repo_name: xiphiness/gl-idris

max_forks_repo_name: xiphiness/gl-idris


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#globals
module WebAssembly.Structure.Modules.Globals

import WebAssembly.Structure.Types
import WebAssembly.Structure.Instructions

import Decidable.Equality

-- Definition

public export
record Global where
  constructor MkGlobal
  type : GlobalType
  init : Expr

-- Equality

total public export
lemma_global__type_injective : ((t1 = t2) -> Void) -> (MkGlobal t1 i1 = MkGlobal t2 i2) -> Void
lemma_global__type_injective t1_not_t2 Refl = t1_not_t2 Refl

total public export
lemma_global__init_injective : ((i1 = i2) -> Void) -> (MkGlobal t1 i1 = MkGlobal t2 i2) -> Void
lemma_global__init_injective i1_not_i2 Refl = i1_not_i2 Refl

-- Decidable Equality

public export
implementation DecEq Global where
  decEq (MkGlobal t1 i1) (MkGlobal t2 i2) = case decEq t1 t2 of
    No t1_not_t2 => No $ lemma_global__type_injective t1_not_t2
    Yes Refl     => case decEq i1 i2 of
      No i1_not_i2 => No $ lemma_global__init_injective i1_not_i2
      Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Data.Optics.Optional

||| Optional
data Optional s a =
  MkOptional (s -> Maybe a) (s -> a -> s)

%name Optional optional, optional1, optional2

get : (Optional s a) -> (s -> Maybe a)
get (MkOptional get set) = get

getOrModify: (Optional s a) -> s -> Either s a
getOrModify optional s' = case (get optional s') of
                          Just a' => Right a'
                          Nothing => Left s'

set : Optional s a -> s -> a -> s
set (MkOptional get set)  = set

--
-- Compositions
--

infixr 9 ?:+
||| compose two optionals
(?:+): Optional a b -> Optional s a -> Optional s b
(MkOptional get1 set1) ?:+ (MkOptional get2 set2) = MkOptional newGet newSet
  where
    newGet: s -> Maybe b
    newGet s = do a <- get2 s
                  b <- get1 a
                  return b

    newSet: s -> b -> s
    newSet s b = let a' = get2 s
                     newA = do a'' <- a'
                               return (set1 a'' b)
                     newS = case newA of
                              Just v => set2 s v
                              Nothing => s
                     in newS

infixr 9 +:?
(+:?) : Optional s a -> Optional a b -> Optional s b
(+:?) = flip (?:+)

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


text:
allZeroesFromTo : Int -> Int -> String -> Bool
allZeroesFromTo n m str
  = if n < m
    then if strIndex str n == '0'
         then allZeroesFromTo (n+1) m str
         else False
    else True

isNthPowerOfTen : Int -> String -> Bool
isNthPowerOfTen n str
  = let m = cast (length str) in
    if m == n+1
    then strHead str == '1' && allZeroesFromTo 1 m str
    else False

main : IO ()
main = do
  let x = power 10 12468
  let sx = show x
  printLn (isNthPowerOfTen 12468 sx)
  let y = power 10 12470
  let sy = show y
  printLn (isNthPowerOfTen 12470 sy)

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:
data Input = Answer Int
           | QuitCmd

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String
  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (Pure val) = pure val
runCommand (Bind c f) = do res <- runCommand c
                           runCommand (f res)

namespace CommandDo
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

readInput : (prompt : String) -> Command Input
readInput prompt = do PutStr prompt
                      answer <- GetLine
                      if toLower answer == "quit"
                         then Pure QuitCmd
                         else Pure (Answer (cast answer))

mutual
  correct : Stream Int -> (score : Nat) -> (questions : Nat) -> ConsoleIO Nat
  correct nums score questions
    = do PutStr "Correct!\n"
         quiz nums (score + 1) (questions + 1)

  wrong : Stream Int -> Int -> (score : Nat) -> (questions : Nat)
    -> ConsoleIO Nat
  wrong nums ans score questions
    = do PutStr ("Wrong the answer is " ++ show ans ++ "\n")
         quiz nums score (questions + 1)

  quiz : Stream Int -> (score : Nat) -> (questions : Nat) -> ConsoleIO Nat
  quiz (num1 :: num2 :: nums) score questions
    = do PutStr ("Score so far: " ++ show score ++ "\n")
         input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
         case input of
              Answer answer => if answer == num1 * num2
                                  then correct nums score questions
                                  else wrong nums (num1 * num2) score questions
              QuitCmd => Quit score


text:
total sameCons: {xs: List a} -> {ys: List a} -> xs = ys -> x :: xs = x :: ys
sameCons Refl = Refl

total sameLists: {xs: List a} -> {ys: List a} -> x = y -> xs = ys -> x :: xs = y :: ys
sameLists Refl Refl = Refl

data ThreeEq: Nat -> Nat -> Nat -> Type where
  Same: (x:Nat) -> ThreeEq x x x

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

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Erlang.Data.IORef

import Erlang

%default total

export
data IORef : Type -> Type where
  MkIORef : ErlTerm -> IORef a

export
newIORef : HasIO io => a -> io (IORef a)
newIORef val = do
  ref <- pure $ erlUnsafeCall ErlTerm "erlang" "make_ref" []
  pure $ erlUnsafeCall ErlTerm "erlang" "put" [ref, MkRaw val]
  pure (MkIORef ref)

export
readIORef : HasIO io => IORef a -> io a
readIORef (MkIORef ref) = do
  MkRaw val <- pure $ erlUnsafeCall (Raw a) "erlang" "get" [ref]
  pure val

export
writeIORef : HasIO io => IORef a -> (val : a) -> io ()
writeIORef (MkIORef ref) val = do
  pure $ erlUnsafeCall ErlTerm "erlang" "put" [ref, MkRaw val]
  pure ()

export
modifyIORef : HasIO io => IORef a -> (a -> a) -> io ()
modifyIORef ref f = do
  val <- readIORef ref
  writeIORef ref (f val)


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

module ProcessLib

import System.Concurrency.Channels

-- check that all functions are total
%default total

export
data MessagePID : (iface : reqType -> Type) -> Type where
  MkMessage : PID -> MessagePID iface

public export
data ProcState = NoRequest | Sent | Complete

public export
data Process : (iface : reqType -> Type) ->
               Type ->
               (in_state : ProcState) ->
               (out_state : ProcState) ->
               Type where
  Action : IO a -> Process iface a st st
  Pure : a -> Process iface a st st
  (>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) ->
          Process iface b st1 st3
  Spawn : Process service_iface () NoRequest Complete ->
          Process iface (Maybe (MessagePID service_iface)) st st
  Request : MessagePID service_iface ->
            (msg : service_reqType) ->
            Process iface (service_iface msg) st st
  Respond : ((msg : reqType) ->
                Process iface (iface msg) NoRequest NoRequest) ->
            Process iface (Maybe reqType) st Sent
  Loop : Inf (Process iface a NoRequest Complete) ->
         Process iface a Sent Complete

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

export partial
forever : Fuel
forever = More forever

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

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

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

public export
Service : (iface : reqType -> Type) -> Type -> Type
Service iface a = Process iface a NoRequest Complete

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


text:
module Main

import Data.Vect
import Data.Fin

test : DecEq a => a -> a -> Bool
test i1 i2 with (decEq i1 i2)
  test i1 i1 | Yes Refl = True
  test i1 i2 | No p = False

main : IO ()
main = do
-- Primitives
  putStrLn . show $ test (the Int 3) (the Int 3)
  putStrLn . show $ test (the Integer 3) (the Integer 4)
  putStrLn . show $ test "hello" "hello"
  putStrLn . show $ test "hello" "world"
  putStrLn . show $ test (the Char '\0') (the Char '\0')
  putStrLn . show $ test (the Char '\1') (the Char '\2')
  putStrLn . show $ test """""" ""
  putStrLn . show $ test """"hello"""" "\"hello\""
  putStrLn . show $ test """""hello""""" "\"\"hello\"\""
  putStrLn . show $ test """""""""" "\"\"\"\""
-- Non-primitives
  -- Vect
  putStrLn . show $
    test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,3])
  putStrLn . show $
    test (the (Vect _ Int) [1,2,3]) (the (Vect _ Int) [1,2,4])
  -- List
  putStrLn . show $
    test (the (List Int) [1,2,3]) (the (List Int) [1,2,3])
  putStrLn . show $
    test (the (List Int) [1,2,3]) (the (List Int) [1,2])
  putStrLn . show $
    test (the (List Int) [1,2,3]) (the (List Int) [1,2,4])
  -- Tuple
  putStrLn . show $
    test (the (Int, Int) (1, 1)) (the (Int, Int) (1, 1))
  putStrLn . show $
    test (the (Int, Int) (1, 2)) (the (Int, Int) (1, 1))
  -- Unit
  putStrLn . show $ test () ()
  -- Booleans
  putStrLn . show $ test True True
  putStrLn . show $ test True False
  -- Maybe
  putStrLn . show $ test (Just "hello") (Just "hello")
  putStrLn . show $ test (Just "hello") (Just "world")
  putStrLn . show $ test (Just "hello") Nothing
  -- Either
  putStrLn . show $ test (the (Either String Bool) (Left "hello"))
                         (the (Either String Bool) (Left "hello"))
  putStrLn . show $ test (the (Either String Bool) (Left "hello"))
                         (the (Either String Bool) (Left "world"))
  putStrLn . show $ test (Left "hello") (Right "world")
  putStrLn . show $ test (Left "hello") (Right False)
  -- Fin
  putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
                         (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
  putStrLn . show $ test (the (Fin (S (S (S (Z))))) (FS (FS (FZ))))
                         (the (Fin (S (S (S (Z))))) (FS (FZ)))
  -- Nat
  putStrLn . show $ test (S (S (S Z))) (S (S (S Z)))
  putStrLn . show $ test (S (S (S Z))) (S (S Z))


text:
-- ---------------------------------------------------------- [ WellFormed.idr ]
-- Module    : WellFormed.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module XML.Test.WellFormed

import Test.Unit

import Commons.Data.Location
import Commons.Text.Parser.Test

import XML.Lexer
import XML.Parser
import XML.DOM
import XML.Serialise

showParseError : Run.ParseError Token -> String
showParseError (FError e) = show e
showParseError (PError e) = unlines [maybe "" show (location e), error e]
showParseError (LError (MkLexFail l i)) = unlines [show l, show i]

export
runTests : IO ()
runTests = do
  putStrLn $ "=> Well Formed"

  NonReporting.runTests [
         runParseTest showParseError $ parseTest "Well Formed 1" (parseXMLSnippet) "<root xmlns:h=\"http://www.w3.org/TR/html4/\" xmlns:f=\"http://www.w3schools.com/furniture\"/>\n"
       , runParseTest showParseError $ parseTest "Well Formed 2" (parseXMLSnippet) "<library xmlns=\"http://eric.van-der-vlist.com/ns/library\" xmlns:hr=\"http://eric.van-der-vlist.com/ns/person\"/>"
       , runParseTest showParseError $ parseTest "Well Formed 3" (parseXMLSnippet) "<root><child>asas asas</child></root>"
       , runParseTest showParseError $ parseTest "Well Formed 4" (parseXMLSnippet) "<empty/>"
       , runParseTest showParseError $ parseTest "Well Formed 5" (parseXMLSnippet) "<empty/><empty as=\"asas\" bs=\"de\"/>"

       , runParseTest showParseError $ parseTest "Well Formed 6" (parseString XMLLexer comment) "<!-- I am comment -->"
       , runParseTest showParseError $ parseTest "Well Formed 7" (parseXMLSnippet) "<hr:born>1950-10-04</hr:born>"

       , runParseTest showParseError $ parseFail "Well Formed 8" (parseXMLSnippet) "<root><child></root></child>"

       , runParseTest showParseError $ parseTest "Well Formed 9" (parseString XMLLexer instruction) "<? target value=\"as\" ?>"
       , runParseTest showParseError $ parseTest"Well Formed 10" (parseXMLSnippet) "<root><abc/><person name=\"bob\"><age>13</age></person></root>"

       , runParseTest showParseError $ parseTest "Well Formed 11" (parseString XMLLexer xmlinfo) "<?xml version=\"1.0\" encoding=\"utf-16\" standalone=\"true\" ?>"
       , runParseTest showParseError $ parseTest "Well Formed 12" (parseString XMLLexer xmlinfo) "<?xml version=\"1.0\" encoding=\"utf-16\"?>"
       , runParseTest showParseError $ parseTest  "Well Formed 13" (parseString XMLLexer doctype) "<!DOCTYPE hello PUBLIC \"//PUBLIC/hello\" \"hello.dtd\">"
       , runParseTest showParseError $ parseTest "Well Formed 14" (parseXMLSnippet) "<hello>\n<world xmlns=\"worldnamespace\" first=\"1\" second=\"a\">\n<!--Just a - comment-->\n<![CDATA[Some <CDATA&>]]>\n<empty/>\n<empty foo=\"bar\"/>\n<characters>A</characters>\n</world>\n</hello>"

       , runParseTest showParseError $ parseTest "Well Formed 15" (parseXMLDoc) "<?xml version=\"1.0\" encoding=\"utf-16\"?><!DOCTYPE hello PUBLIC \"//PUBLIC/hello\" \"hello.dtd\"><hello><world xmlns=\"worldnamespace\" first=\"1\" second=\"a\"><!--Just a - comment--><![CDATA[Some <CDATA&>]]><empty/><empty foo=\"bar\"/><characters>A</characters></world></hello>"

       , runParseTest showParseError $ parseTest "Well Formed 16" (parseXMLSnippet) "<xs:schema xmlns:xs=\"http://www.w3.org/2001/XMLSchema\">asas</xs:schema>"
       ]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
record R where
  constructor MkR
  field : Nat

myRec1 : R
myRec1 = MkR 3

mkRec2 : R
myRec2 = MkR 3


text:
module Dart.FFI.Elab.Types

import Data.List
import Data.List.Equalities

public export
DartName : Type
DartName = String

public export
data DartType : Type where
  NType : String -> DartType
  FType : List DartType -> DartType -> DartType
  GType : DartType -> (args : List DartType) -> {auto prf : NonEmpty args} -> DartType

public export
FromString DartType where
  fromString = NType

public export
Show DartType where
  show ty = case ty of
    NType n => n
    FType ps ret => concat $ intersperse " -> " $ show <$> (ps ++ [ret])
    GType t args => show t ++ show args

infixr 8 :->
public export
(:->) : DartType -> DartType -> DartType
(:->) ty (FType ps ret) = FType (ty :: ps) ret
(:->) p ret = FType [p] ret

infixl 9 :<>
public export
(:<>) : DartType -> DartType -> DartType
(:<>) (GType t args) arg = GType t (snoc args arg) @{SnocNonEmpty args arg}
(:<>) t arg = GType t [arg]

public export
data DartParameter
  = Positional DartName DartType
  | Named DartName DartType

infix 7 :?

namespace DartParameter
  public export
  (::) : DartName -> DartType -> DartParameter
  (::) = Positional

  public export
  (:?) : DartName -> DartType -> DartParameter
  (:?) = Named

public export
data DartDecl
  = Function DartType DartName (List DartParameter)
  | Val DartType DartName
  | Var DartType DartName
  | Effectful DartDecl
  | Static DartDecl
  | Class DartName (List DartDecl)
  | Enum DartName (List DartName)
  | Constructor DartName (List DartParameter)
  | Extends DartType
  | Generic (List DartName) DartDecl
  | Partial DartDecl
  | Const DartDecl
  | Primitive DartDecl

public export
Show DartDecl where
  show (Function _ n _) = "fun " ++ n
  show (Constructor n _) = "new " ++ show n
  show (Const d) = "const " ++ show d
  show (Val _ n) = "final " ++ n
  show (Var _ n) = "var " ++ n
  show (Effectful d) = "io $ " ++ show d
  show (Static d) = "static $ " ++ show d
  show (Class n _) = "class " ++ show n
  show (Enum n _) = "enum " ++ show n
  show (Extends t) = "extends " ++ show t
  show (Generic _ d) = "generic " ++ show d
  show (Partial d) = "partial " ++ show d
  show (Primitive d) = "primitive " ++ show d

public export
record DartPackage where
  constructor MkDartPackage
  name : String
  declarations : List DartDecl


text:
module Integration.Riemann

%access private

||| Computes the left Riemann sum of a function.
|||
||| @f  the function
||| @d  the delta x value
||| @a  the left limit of the interval
||| @n  the number of subintervals
export
lrs : (f : Double -> Double) -> (d : Double) -> (a : Double) -> (n : Nat) -> Double
lrs f d s Z = 0
lrs f d a (S n') = d * (lrs' n') where
  lrs' : (i : Nat) -> Double
  lrs' Z = f a
  lrs' i@(S i') = (f (a + ((cast i) * d))) + (lrs' i')

||| Computes the right Riemann sum of a function.
|||
||| @f  the function
||| @d  the delta x value
||| @a  the left limit of the interval
||| @n  the number of subintervals
export
rrs : (f : Double -> Double) -> (d : Double) -> (a : Double) -> (n : Nat) -> Double
rrs f d a Z = 0
rrs f d a n@(S n') = d * (rrs' n) where
  rrs' : (i : Nat) -> Double
  rrs' Z = 0
  rrs' i@(S i') = (f (a + ((cast i) * d))) + (rrs' i')

||| Approximates the integral of a function using the trapezoidal rule.
|||
||| @f  the function
||| @d  the delta x value
||| @a  the left limit of the interval
||| @n  the number of subintervals
export
trapz : (f : Double -> Double) -> (d : Double) -> (a : Double) -> (n : Nat) -> Double
trapz f d a n = ((lrs f d a n) + (rrs f d a n)) / 2

max_stars_repo_name: lambdacasserole/idris-integration

max_issues_repo_name: lambdacasserole/idris-integration

max_forks_repo_name: lambdacasserole/idris-integration


text:
module Injection

import Data.Vect
import Data.Nat

%default total

|||Is a Nat different from all the Nats in a vector?
public export
isDifferent : Nat -> Vect n Nat -> Bool
isDifferent n [] = True
isDifferent n (x :: xs) = (n /= x) && isDifferent n xs

|||Are all the elements of a Nat vector different?
public export
allDifferent : Vect n Nat -> Bool
allDifferent [] = True
allDifferent (x :: xs) = isDifferent x xs && allDifferent xs

|||Are all the elements in a vector smaller than a given Nat?
public export
allSmaller : Vect n Nat -> Nat -> Bool
allSmaller [] m = True
allSmaller (x :: xs) m = (x < m) && allSmaller xs m

public export
isInjective : Nat -> Vect n Nat -> Bool
isInjective m v = allSmaller v m && allDifferent v

|||Returns the element at index k in a vector
public export
index : (k : Nat) -> Vect n Nat -> {auto prf : (k < n) = True} -> Nat
index Z     (x::_)  = x
index (S k) (_::xs) = index k xs

|||Returns the vector [1,2,...,n]
public export
rangeVect : (startIndex : Nat) -> (length : Nat) -> Vect length Nat
rangeVect k Z = []
rangeVect k (S i) = k :: rangeVect (S k) i

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Go

public export
data GoInterface : String -> Type where
  MkInterface : (iface : String) -> GoInterface iface

public export
data Go_FFI_Call = Function String
  | Method (GoInterface iface) String

public export
data GoPtr : (a : Type) -> Type where  -- XXX limit to Go_Types?
  MkGoPtr : (x : a) -> GoPtr a

||| A byte
public export
data Byte : Type where
  MkByte : (ch : Char) -> Byte

%used MkByte ch

mutual

  ||| Go foreign types
  public export
  data Go_Types : Type -> Type where
    Go_Byte      : Go_Types Byte
    Go_Int       : Go_Types Int
    Go_Str       : Go_Types String
    Go_Unit      : Go_Types ()
    Go_Interface : Go_Types (GoInterface a)
    Go_Nilable   : Go_Types a -> Go_Types (Maybe a)
    Go_Ptr       : Go_Types a -> Go_Types (GoPtr a)
    Go_Any       : Go_Types (FFI_C.Raw a)
    -- Note that this is actually only valid as return value
    Go_MultiVal  : (Go_Types a, Go_Types b) -> Go_Types (a, b)

  public export
  FFI_Go : FFI
  FFI_Go = MkFFI Go_Types Go_FFI_Call String

  public export
  GIO : Type -> Type
  GIO = IO' FFI_Go

public export
%inline
gocall : (f : Go_FFI_Call) -> (ty : Type) -> {auto fty : FTy FFI_Go [] ty} -> ty
gocall f ty = foreign FFI_Go f ty

max_stars_repo_name: Trundle/idris-go

max_issues_repo_name: Trundle/idris-go

max_forks_repo_name: Trundle/idris-go


text:
{- Example (modified) by Chris Done,
 - from: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c115292

 - This files gives an example of a dependently typed printf function. printf
 - takes a format string as its first argument, for example:
      "This is a format string with an int %d and a string %s."
 - Our printf has the following type:
      printf : (s : String) -> interpFormat ( formatString s )
 - Here, the type of the expression `printf s` for a format string `s` is calculated
 - from the value of the format string. `interpFormat ( formatString s)` is a function
 - whose number of arguments and their types are determined by the format string's
 - value. Thus, a compiler error is thrown if the wrong arguments are passed
 - for a given format string. -}

%default total -- turns on totality checking for all functions

{- Idris can try and check that functions are total, i.e. that they terminate.
 - This is too hard a problem in general, but Idris can check totality for the
 - specific class of recursive functions which shrink toward a base case on
 - every call. -}

-- Formatting AST.
data Format
  = FInt Format
  | FString Format
  | FOther Char Format
  | FEnd

-- Parse the format string (list of characters) into an AST.
-- Example: "%d,%s"  →   (FInt (FOther ',' (FString FEnd)))
format : List Char -> Format
format ('%' :: 'd' :: cs ) = FInt ( format cs )
format ('%' :: 's' :: cs ) = FString ( format cs )
format ( c :: cs )         = FOther c ( format cs )
format []                  = FEnd

-- Convenience function to unpack a string into a list of chars, then
-- run format on it. Note that in Idris strings are not lists of characters.
formatString : String -> Format
formatString s = format ( unpack s )

-- Convert a format AST into a type.
-- Example: FInt (FOther ',' (FString FEnd))   →   Int -> String -> String
interpFormat : Format -> Type
interpFormat (FInt f)     = Int -> interpFormat f
interpFormat (FString f)  = String -> interpFormat f
interpFormat (FOther _ f) = interpFormat f
interpFormat FEnd         = String

-- Dependently-typed part: turn a formatting AST into a well-typed
-- function accepting n arguments.
-- Example:
--      toFunction (FInt (FString FEnd))
--    →
--      \a i s => a ++ (show i) ++ s
{-
-}
toFunction : (fmt : Format) -> String -> interpFormat fmt
toFunction ( FInt f ) a     = \i => toFunction f ( a ++ show i )
toFunction ( FString f ) a  = \s => toFunction f ( a ++ s )
toFunction ( FOther c f ) a = toFunction f ( a ++ pack [c])
toFunction FEnd a           = a

-- Dependently-typed part: turn a formatting string into a well-typed
-- function accepting n arguments.
-- Example: printf "%d%s" → \i s => (show i) ++ s
printf : (s : String) -> interpFormat ( formatString s )
printf s = toFunction ( formatString s ) ""

{- Now we can see printf in action. The following typechecks: -}

output : String
output = printf "My name is %s, and I am %d years old" "Isaac" 22

{- The following does not: -}

outputBad : String
outputBad = printf "My name is %s, and I am %d years old" 22 "Isaac"

{- Indeed, the compiler error is:

 Mismatch between: String and Int

 -}


text:
||| Red black trees, adapted from Purely functional data structures by Chris Okasaki.
|||
||| You are guaranteed to get the correct value for a key.
|||
||| TODO: Implement deletion.
|||
||| The code has a lot of duplication that can not be unduplicated in trivially
||| , due to the need to prove different things in different cases.

module TypedContainers.RBTree

import Data.Nat
import Data.DPair
import Data.List
import TypedContainers.In
import TypedContainers.LawfulOrd
import TypedContainers.RBTree.Base
import TypedContainers.RBTree.Index
import TypedContainers.RBTree.Insert

%default total

export
data RBTree : (kt : Type) -> (kord : LawfulOrd kt) => (kt -> Type) -> Type where
  MkRBTree : GoodTree {height, color, kt, kord, vt, keys} -> RBTree kt vt {kord}

export
empty : LawfulOrd kt => RBTree kt vt
empty = MkRBTree (Empty Refl)

export
insert : LawfulOrd kt => (k : kt) -> vt k -> RBTree kt vt -> RBTree kt vt
insert k v (MkRBTree tree) =
  let Evidence _ (Evidence _ tree') = insertG k v tree in
  MkRBTree tree'

export
index : LawfulOrd kt => kt -> RBTree kt vt -> Maybe (DPair kt vt)
index k (MkRBTree tree) =
  case indexGMaybe k tree {foldRight = \_, _ => (), foldLeft = id} of
    Left _ => Nothing
    Right (MkDPair k' $ Evidence _ v) => Just $ MkDPair k' v

export
index' : LawfullerOrd kt => (k : kt) -> RBTree kt vt -> Maybe (vt k)
index' k (MkRBTree tree) =
  case indexGMaybe k tree {foldRight = \k', (p, _) => p, foldLeft = id} of
    Left _ => Nothing
    Right (MkDPair k' $ Evidence p v) =>
      let 0 p = realEquality k' k p in
      Just $ rewrite sym p in v

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module Cam.FileSystem
import Cam.FFI
import Cam.Data.FCollections
import Cam.Data.Compat
import Data.Vect
import Data.HVect

%access export
public export
%inline

pipe : () -> FHVect [Int, Int]
pipe () = believe_me . unsafePerformIO $ fcall1 "filesystem_pipe" $ believe_me ()

public export
%inline
getcwd : () ->  Boxed String
getcwd () = believe_me . unsafePerformIO $ fcall1 "filesystem_getcwd" $ believe_me ()

data FileHandlerSpec;

public export
FileHandler : Type
FileHandler = Boxed FileHandlerSpec

public export
%inline
openFile : (filename: String) -> (mode: String) ->  IO FileHandler
openFile filename mode =
          let filename = believe_me . the (Boxed String) $ toForeign filename in
          let mode = believe_me . the (Boxed String) $ toForeign mode in
          believe_me $ fcall2 "filesystem_open_file" filename mode

public export
%inline
closeFile : FileHandler ->  IO ()
closeFile f =
        let f = believe_me f in
        believe_me $ fcall1 "filesystem_close_file" f

public export
%inline
readAllText : FileHandler -> IO (Boxed String)
readAllText f =
          let f = believe_me f in
          believe_me $ fcall1 "filesystem_read_all_text" f

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
import BSTree
import DataStore
import Direction
import Generic
import Picture
import Shape
import SumInputs
import Tree
import TryIndex
import Vect
import Vehicle


text:
module Example.Main

import Control.Monad.Either
import Data.SOP
import Data.List.Elem
import PQ.CRUD
import PQ.FFI
import PQ.Schema
import PQ.Types

--------------------------------------------------------------------------------
--          Tables
--------------------------------------------------------------------------------

SchemaName : Column
SchemaName = notNull String "schemaname" Text Just id ""

TableName : Column
TableName = notNull String "tablename" Text Just id ""

TableOwner : Column
TableOwner = notNull String "tableowner" Text Just id ""

TableSpace : Column
TableSpace = nullable String "tablespace" Text Just id ""

HasIndexes : Column
HasIndexes = notNull Bool "hasindexes" Boolean Just id ""

HasRules : Column
HasRules = notNull Bool "hasrules" Boolean Just id ""

HasTriggers : Column
HasTriggers = notNull Bool "hastriggers" Boolean Just id ""

RowSecurity : Column
RowSecurity = notNull Bool "rowsecurity" Boolean Just id ""

Tables : Table
Tables = MkTable "pg_tables"
           [ SchemaName
           , TableName
           , TableOwner
           , TableSpace
           , HasIndexes
           , HasRules
           , HasTriggers
           , RowSecurity
           ]

tableExists :  HasIO io
            => MonadError SQLError io
            => Connection
            -> Table
            -> io Bool
tableExists c t =
  (1 ==) <$> countCmd c Tables (TableName == t.name)

--------------------------------------------------------------------------------
--          User
--------------------------------------------------------------------------------

Id : Column
Id = primarySerial64 Bits32 "user_id" (Just . cast) ""

Name : Column
Name = notNull String "user_name" Text Just id ""

Password : Column
Password = notNull String "user_password" Text Just id ""

Salary : Column
Salary = notNull Bits32 "user_salary" BigInt (Just . cast) cast ""

Age : Column
Age = notNull Bits8 "user_age" SmallInt (Just . cast) cast ""

Supervisor : Column
Supervisor = nullable Bits32 "user_supervisor" BigInt (Just . cast) cast ""

User : Table
User = MkTable "show_user"
         [Id, Name, Password, Salary, Age, Supervisor]

0 UserInsertRow : Type
UserInsertRow = PutRow (columns User)

users : List UserInsertRow
users = [ [(), "CEO",   "top secret", 15000,  58, Nothing]
        , [(), "Gundi", "123456",      4500,  45, Just 1]
        , [(), "Lars",  "Lars",        3500,  23, Just 2]
        , [(), "Eleni", "I love cats", 9000,  35, Just 1]
        ] ++ map johnDoe [2000 .. 400000]
  where johnDoe : Bits32 -> UserInsertRow
        johnDoe n = [(), "John Doe", "John Doe", n, 33, Just 3]

createAndFill :  HasIO io
              => MonadError SQLError io
              => Connection
              -> io ()
createAndFill c = do
  False <- tableExists c User
    | True => pure ()
  createTable c User
  insert c User users

--------------------------------------------------------------------------------
--          Main function
--------------------------------------------------------------------------------

main_ : HasIO io => MonadError SQLError io => io ()
main_ = do
  c    <- connect "postgresql://gundi@localhost:5432/testdb"
  createAndFill c
  rows <- get c User [Id,Name,Supervisor] (Name /= "Eleni" && Age >= 33)
  finish c
  traverse_ printLn rows

main : IO ()
main = do Left err <- runEitherT (main_ {io = EitherT SQLError IO})
            | Right () => pure ()
          printLn err


text:
module Calc.Sub

%default total

export
subtract : Int -> Int -> Int
subtract x y = x - y

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

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

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


text:
-- ----------------------------------------------------------------- [ Org.idr ]
-- Module    : Org.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Reader.Org

import Effects
import Effect.File

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

import Data.AVL.Dict

import Lightyear
import Lightyear.Char
import Lightyear.Strings

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

import Text.Markup.Edda.Process.Utils
import Text.Markup.Edda.Reader.Common
import Text.Markup.Edda.Reader.Utils

%default partial
%access private

-- --------------------------------------------------------------------- [ Org ]

code : Parser (EddaRaw INLINE)
code = map (Raw CodeTy) (quoted '~') <?> "Code"

verb : Parser (EddaRaw INLINE)
verb = map (Raw VerbTy) (quoted '=') <?> "Verb"

math : Parser (EddaRaw INLINE)
math = map (Raw MathTy) (quoted '$') <?> "Math"

markup : MarkupTy -> Char -> Parser (EddaRaw INLINE)
markup mTy c = do
    txt <- between (char c) (char c) (some mText)
    pure $ Mark mTy txt
  <?> "Markup"

bold : Parser (EddaRaw INLINE)
bold = markup BoldTy '*' <?> "Bold"

emph : Parser (EddaRaw INLINE)
emph = markup EmphTy '/'  <?> "Emph"

strike : Parser (EddaRaw INLINE)
strike = markup StrikeTy '+' <?> "Strike"

uline : Parser (EddaRaw INLINE)
uline = markup UlineTy '_' <?> "Uline"

expLink : Parser (EddaRaw INLINE)
expLink = do
    txt <- brackets $ brackets url
    pure $ Link ExposedTy txt Nil
  <?> "Exposed Link"

hyper : Parser (EddaRaw INLINE)
hyper = do
    (uri, desc) <- brackets internal
    pure $ Link HyperTy uri desc
  where
    internal : Parser (String, List (EddaRaw INLINE))
    internal = do
      u <- brackets url
      d <- brackets $ some (text <* spaces)
      pure (u, intersperse (Punc ' ' ) d)

link : Parser (EddaRaw INLINE)
link = hyper <|> expLink <?> "Link"

fnote : Parser (EddaRaw INLINE)
fnote = do
   (l,d) <- brackets doFnote
   pure $ Link FnoteTy (fromMaybe "" l) d
 where
   doFnote : Parser (Maybe String, (List (EddaRaw INLINE)))
   doFnote = do
     string "fn"
     colon
     lab <- opt word
     colon
     desc <- opt $ some text
     pure (lab, fromMaybe Nil desc)

export
inline : Parser (EddaRaw INLINE)
inline = text
     <|> fnote <|> link
     <|> bold <|> emph <|> strike <|> uline
     <|> code <|> verb <|> math <|> punc
     <?> "Raw Inline"

-- -------------------------------------------------------------- [ Properties ]

export
attribute : String -> Parser (String, String)
attribute key = do
    string "#+" *> string key
    colon
    ps <- manyTill anyChar endOfLine
    pure (key, pack ps)
  <?> "Raw Attribute"

property : Parser (String, String)
property = attribute "PROPERTY" <?> "Property"

inlineKeyWord : String -> Parser (String, List (EddaRaw INLINE))
inlineKeyWord key = do
    string "#+" *> string key
    colon
    spaces
    ps <- manyTill inline endOfLine
    pure (key, ps)
  <?> "Attribute."

caption : Parser (List (EddaRaw INLINE))
caption = do
    (k,v) <- inlineKeyWord "CAPTION"
    pure v
  <?> "Caption"

label : Parser String
label = do
    (k,v) <- attribute "NAME"
    pure v
  <?> "Label"

target : Parser String
target = angles $ angles url
  <?> "Target"

title : Parser (List (EddaRaw INLINE))
title = do
    (k,v) <- inlineKeyWord "TITLE"
    pure v
  <?> "Label"

-- ----------------------------------------------------------------- [ Drawers ]

propEntry : Parser (String, String)
propEntry = do
    colon
    key <- word
    colon
    spaces
    value <- manyTill anyChar endOfLine
    pure (key, pack value)
  <?> "Property Entry"

drawer : Parser $ List (String, String)
drawer = do
    string ":PROPERTIES:"
    endOfLine
    ps <- some propEntry
    token ":END:"
    pure ps
  <?> "Property Drawer"
-- ------------------------------------------------------------------ [ Blocks ]

getOrgBlockType : String -> Either VerbBlockTy TextBlockTy
getOrgBlockType str = case str of
    "COMMENT"     => Left CommentTy
    "SRC"         => Left ListingTy
    "EXAMPLE"     => Left LiteralTy
    "EQUATION"    => Left EquationTy
    "QUOTE"       => Right QuotationTy
    "VERSE"       => Right QuotationTy
    "THEOREM"     => Right TheoremTy
    "COROLLARY"   => Right CorollaryTy
    "LEMMA"       => Right LemmaTy
    "PROPOSITION" => Right PropositionTy
    "PROOF"       => Right ProofTy
    "DEFINITION"  => Right DefinitionTy
    "EXERCISE"    => Right ExerciseTy
    "NOTE"        => Right NoteTy
    "PROBLEM"     => Right ProblemTy
    "QUESTION"    => Right QuestionTy
    "REMARK"      => Right RemarkTy
    "SOLUTION"    => Right SolutionTy
    otherwise     => Left LiteralTy

export
block : Parser (EddaRaw BLOCK)
block = do
    cap  <- opt caption
    lab  <- opt label
    attr <- opt $ attribute "ATTR"
    string "#+BEGIN_"
    ty <- word
    case getOrgBlockType ty of
      Left x => do
        srcopts <- opt $ space  *> manyTill anyChar endOfLine
        let as = dealWithSrcAttrs (convertOpts srcopts) (convertAttrs attr)

        txt <- manyTill anyChar (string "#+END_" *> token ty)
        pure $ VerbBlock x lab (fromMaybe Nil cap) as (pack txt)
      Right y => do
        txt <- manyTill inline (string "#+END_" *> token ty)
        pure $ TextBlock y lab (fromMaybe Nil cap) (convertAttrs attr) txt

   <?> "Blocks"

figure : Parser (EddaRaw BLOCK)
figure = do
    cap <- caption
    lab <- label
    as  <- opt $ some (attribute "ATTR")
    img <- expLink
    spaces
    let attrs = maybe empty (fromList) as
    pure (Figure (Just lab) cap attrs img)
  <?> "Figure"

export
para : Parser (EddaRaw BLOCK)
para = do
    txt <- manyTill inline (endOfLine *> endOfLine)
    spaces
    pure $ TextBlock ParaTy Nothing Nil empty txt
  <?> "Paragraphs"

paraLast : Parser (EddaRaw BLOCK)
paraLast = do
    txt <- manyTill inline (endOfLine *> spaces)
    pure $ TextBlock ParaTy Nothing Nil empty txt
  <?> "Filthy hack for last para"

hrule : Parser (EddaRaw BLOCK)
hrule = do
    token "-----"
    pure HRule

ulMarker : Parser ()
ulMarker = char' '+' <|> char' '-' <?> "UList Marker"

olMarker : Parser ()
olMarker = marker '.' <|> marker ')'
  where
    marker : Char -> Parser ()
    marker c = do
      some $ digit
      char c
      spaces
      pure ()

-- @TODO Add coninuations
listItem : Parser () -> Parser (List (EddaRaw INLINE))
listItem mark = do
    mark
    line <- manyTill inline endOfLine
    pure $ line

olist : Parser (EddaRaw BLOCK)
olist = do
    is <- some (listItem olMarker)
    endOfLine
    pure $ ListBlock NumberTy is

blist : Parser (EddaRaw BLOCK)
blist = do
    is <- some (listItem ulMarker)
    endOfLine
    pure $ ListBlock BulletTy is
  <?> "Bulleted lists"

dlist : Parser (EddaRaw BLOCK)
dlist = do
    is <- some defItem <* endOfLine
    pure $ DList is
  <?> "Description Lists"
  where
    marker : Parser (List (EddaRaw INLINE))
    marker = ulMarker *> space *> manyTill inline (spaces *> colon *> colon)
        <?> "Desc Marker"

    defItem : Parser (List (EddaRaw INLINE), List (EddaRaw INLINE))
    defItem = do
        key <- marker
        spaces
        values <- manyTill inline endOfLine
        pure (key, values)
      <?> "Desc Lists"

list : Parser (EddaRaw BLOCK)
list = dlist <|> blist <|> olist <?> "Lists"

export
header : Parser (EddaRaw BLOCK)
header = char '*' >! do
    depth <- opt (many $ char '*')
    let d = length (fromMaybe [] depth) + 1
    spaces
    title <- manyTill (inline) (endOfLine)
    l <- opt target
    spaces
    as <- opt drawer
    let attrs = maybe empty (fromList) as
    pure $ Heading d l title attrs

export
orgBlock : Parser (EddaRaw BLOCK)
orgBlock = header <|> block <|> list <|> figure <|> hrule <|> para <?> "Org Blocks"

parseOrg : Parser (EddaRaw DOC)
parseOrg = do
  title'  <- title
  author <- attribute "AUTHOR"
  date   <- attribute "DATE" <* space
  txt    <- many orgBlock
  lpara  <- many paraLast -- Dirty Hack
  let ps = fromList [author, date]
  let txt' = intersperse Empty txt
  pure $ Doc title' ps (txt' ++ [Empty] ++ lpara)
 <?> "Raw Org Mode"

-- -------------------------------------------------------------------- [ Read ]

namespace Doc
  export
  fromOrgE : String -> Eff (Either String (Edda DOC)) [FILE ()]
  fromOrgE = assert_total $ readEddaFileE parseOrg

  export
  fromOrg : String -> IO (Either String (Edda DOC))
  fromOrg = assert_total $ readEddaFile parseOrg

namespace Snippet
  namespace Inline
    export
    fromOrg : String -> Either String (Edda SNIPPET)
    fromOrg = assert_total $ readEddaSentance inline

  namespace Para
    export
    fromOrg : String -> Either String (Edda SNIPPET)
    fromOrg s = assert_total $ readEddaBody orgBlock (s ++ "\n\n")

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
import Data.Vect

read_vect_len : (len : Nat) -> IO (Vect len String)
read_vect_len Z = pure []
read_vect_len (S k) = do x <- getLine
                         xs <- read_vect_len k
                         pure (x :: xs)

data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

read_vect : IO (len ** Vect len String)
read_vect = do x <- getLine
               if (x == "")
                  then pure (_ ** [])
                  else do (_ ** xs) <- read_vect
                          pure (_ ** x :: xs)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module MemoryIO

import Effects
import Effect.State
import Data.Bits
import Data.Buffer
import Data.Vect

import Chip8
import Cpu
import Ram
import Utilities
import Screen

%default total

export
getOpcode : { [Chip8 ::: STATE Chip8, RAM] } Effects.DepEff.Eff (Bits16)
getOpcode =
  let chip = !(Chip8 :- get) in
  let memory = Memory chip in
  let cpu = Computer chip in
  let pc : Int = cast $ getPC cpu in
  let b1 = !(readByte memory pc) in
  let b2 = !(readByte memory (pc + 1)) in
  pure $ (cast b1) * 0x100 + (cast b2)

export
dumpBlock : (address : Int) -> (Vect len Bits8) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
dumpBlock address values =
  let chip = !(Chip8 :- get) in
  let memory = Memory chip in
  -- not aware of a faster way, this seems inefficient
  let _ = foldl (writeByteAt memory) (pure address) values in
    pure ()
  where
    writeByteAt : (buffer : Buffer) -> (addr : { [RAM] } Eff Int) -> (value : Bits8) -> { [RAM] } Eff Int
    writeByteAt buffer addr value =
      do
        offset <- addr
        writeByte buffer offset value
        pure $ offset + 1

-- quite inefficient as well.
build : {n : Nat} -> (f : Fin n -> { [t] } Eff a) -> { [t] } Eff (Vect n a)
build {n = Z} f = pure []
build {n = S _} f =
  do
    first <- f 0
    rest <- build (f . FS)
    pure $ first :: rest

export
loadBlock : (address : Int) -> (n : Fin len) -> { [Chip8 ::: STATE Chip8, RAM] } Eff (Vect (finToNat n) Bits8)
loadBlock address n =
  let chip = !(Chip8 :- get) in
  let memory = Memory chip in
  build {n = finToNat n} (readByteAt memory address)
  where
    readByteAt : (buffer : Buffer) -> (address : Int) -> (count : Fin index) -> { [RAM] } Eff Bits8
    readByteAt buffer address count =
      let offset = cast $ finToNat count in
      let location = address + offset in
      readByte buffer location

export
loadDefaultSpriteDataAt : (address : Int) -> { [Chip8 ::: STATE Chip8, RAM] } Eff ()
loadDefaultSpriteDataAt address =
  dumpBlock address $ fromList defaultSpriteData


text:
module Main

import Data.So

total
lem1 : So x -> So (not x) -> Void
lem1 Oh Oh impossible

foo : Nat -> Int
foo z = 94
  where
    lem2 : So x -> So (not x) -> Void
    lem2 Oh Oh impossible


text:
module AssRecRule

import Data.Fin
import Data.Vect

% access public export

recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x base step [] = base
recList a x base step (y :: xs) = step y xs previous where
  previous = recList a x base step xs

mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f = recList a (List b) base step where
  base = []
  step head tail prev = (f head) :: prev

foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op = recList a a base step where
  base = init
  step head tail prev = op head prev

recFin : (x: Type) ->
  (Nat -> x) ->
  ((n: Nat) -> Fin n -> x -> x) ->
  ((n: Nat) -> Fin n -> x)
recFin x base _ (S k) FZ = base k
recFin x base step (S k) (FS y) = step k y previous where
  previous = recFin x base step k y

inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S l) FZ = base l
inducFin xs base step (S l) (FS x) =
  step l x prev where
    prev = inducFin xs base step l x

fetchFamily: (a: Type) -> (n: Nat) -> Fin n -> Type
fetchFamily a n x = ((Vect n a) -> a)

fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a  = inducFin (fetchFamily a) base step where
  base m (x :: xs) =  x
  step p k prev (x :: xs) =
    fetchElem a p k xs


text:
module Main

import Interp
import Ast
import Examples
import Data.List

%default partial

program2 : Program
program2 = unDSL
  [ (s z)
  , (s (s z))
  ]

-- Some tests
main : IO ()
main = do
  putStrLn "\n--------------"
  print $ (nub $ dfs $ makeReportTree (unDSL [(n z)]) [n X])
  putStrLn "\n---------------"
  print $ (nub $ bfs $ makeReportTree (unDSL [(n z)]) [n X])
  putStrLn "\n---------------"
  -- Why does this one get [True, True]? It matches twice?
  print $ (nub $ bfs $ makeReportTree program2 [s X])
  putStrLn "\n---------------"
  print result
  putStrLn "\n---------------"
  print $ f_val z
  putStrLn "\n---------------"
  print $ f_val (s z)
  putStrLn "\n---------------"
  print $ f_val (s (s z))
  putStrLn "\n---------------"
  print $ nat z
  putStrLn "\n---------------"
  print $ nat (s z)
  putStrLn "\n---------------"
  print $ nat p
  putStrLn "\n---------------"


text:
import Data.Vect

total insert : Ord element => (x : element) -> (xsSorted : Vect k element) -> Vect (S k) element
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

total insSort : Ord element => Vect n element -> Vect n element
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                        insert x xsSorted

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
module lib.Library5

import lib.sub.Sub

export
salute5 : String
salute5 = "Hello, this is Library5" ++ subslaute


text:
module nat.split

||| The type of evidence I'll accept for m < n:
||| some k and evidence for m+(k+1)=n
data LTProof : Nat -> Nat -> Type where
     MkLTProof : (m:Nat) -> (n:Nat) -> (k:Nat) -> (m+(k+1)=n) -> LTProof m n

||| The type of evidence I'll accept for m < n:
||| some k and evidence for m+(k+1)=n
data GTEProof : Nat -> Nat -> Type where
    MkGTEProof : (m:Nat) -> (n:Nat) -> (k:Nat) -> (m=n+k) -> GTEProof m n

data SplitNatProof : Nat -> Type where
  Below : LTProof m n -> SplitNatProof n
  Above : GTEProof m n -> SplitNatProof n

||| Take (m,n) and return either proof that m <n or proof that m>=n
split : (m:Nat) -> (n:Nat) -> SplitNatProof n
split Z n = Below (MkLTProof n n n ?hole_3)
split (S k) n = ?hole_2
--split m Z = Above MkGTEProof m Z m refl
--split Z S k = Below MkLTProof Z S k k refl

--SplitNat : (n:Nat) -> DPair Nat (SplitNatProof n)

max_stars_repo_name: algeboy/FormalAlgebra

max_issues_repo_name: algeboy/FormalAlgebra

max_forks_repo_name: algeboy/FormalAlgebra


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 10

import Shape

-- check that all functions are total
%default total

area : Shape -> Double
area x with (shapeView x)
  area (triangle base height) | STriangle = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = pi * radius * radius

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Hedgehog.Internal.Terminal

import Control.ANSI.CSI
import Data.IORef
import Data.List1
import Data.String
import System.File

public export
record Terminal where
  constructor MkTerminal
  tmp      : IORef (List String)
  out      : String -> IO ()
  err      : String -> IO ()

putStrErr : HasIO io => String -> io ()
putStrErr s = fPutStr stderr s $> ()

export
console : HasIO io => io Terminal
console = do ref <- newIORef []
             pure $ MkTerminal ref putStr putStrErr

clearTmp : Terminal -> IO ()
clearTmp t = do ls <- readIORef t.tmp
                t.err $ concatMap (\_ => cursorUp1 <+> eraseLine End) ls
                writeIORef t.tmp []

export
putTmp : HasIO io => Terminal -> String -> io ()
putTmp t str =
  let ls = lines str
   in liftIO $ do clearTmp t
                  writeIORef t.tmp ls
                  t.err (str <+> "\n")

export
putOut : HasIO io => Terminal -> String -> io ()
putOut t str = liftIO $ do clearTmp t
                           t.out (str <+> "\n")


text:
module Syntax.Lexer

import Loc
import Error.Data
import Text.Lexer
import Text.Lexer.Core
import Syntax.Tokens
import Data.String
import Data.String.Extra

-- The entry point of lexing

comment : Lexer
comment = (is ';') <+> some (pred (/= '\n'))

string : Lexer
string = (is '"') <+> some (pred (\s => s /= '"' && s /= '\n')) <+> (is '"')

id : Lexer
id = some (non (oneOf "\"; \n\r()[]{}"))

trimStartEnd : Int -> Int -> String -> String
trimStartEnd start end text = strSubstr start ((cast $ length text) - (end + start)) text

tokenMap : TokenMap (Int, Tkn)
tokenMap =
   map (\(rule, fun) => (rule, (\s => (cast $ length s, fun s))))
      [(oneOf "\n\r", const TknLB),
      (digits, TknNum . cast),
      (id    , TknId),
      (is '(', const TknLPar),
      (is ')', const TknRPar),
      (is '[', const TknLSquare),
      (is ']', const TknRSquare),
      (is '{', const TknLCurly),
      (is '}', const TknRCurly),
      (space, const TknWhitespace),
      (comment, TknComment . (trimStartEnd 1 0)),
      (string, TknStr . (trimStartEnd 1 1))]

-- It transforms a parser of Tkn to (Int, Tkn). The tkn parameter indicates the
-- Length of the string that it's getting.

mapApply : (Lexer, String -> Tkn) -> (Lexer, String -> (Int, Tkn))
mapApply (rule, func) = (rule, \s => (cast $ length s, func s))

-- The token data for comments are broken. So think twice before using the range for
-- comments.

tokenDataToLoc : TokenData (Int, Tkn) -> (Range, Tkn)
tokenDataToLoc (MkToken line col (len, tkn)) =
  (MkRange (MkLoc {column = col, line = line}) (MkLoc {column = col + len, line }), tkn)

-- The main function that lexes the string to a list of (range,tkn)

public export
lex : String -> Either ErrorType (List (Range, Tkn))
lex str
  = case lex tokenMap str of
    (tokens, _, _,   "") => Right $ map tokenDataToLoc tokens
    (_, line, column, res) => Left $ LexicalError
      (MkRange (MkLoc { column, line }) (MkLoc { column = column + 1, line }))
      (if (take 1 res) == "\"" then UnterminatedString else UnexpectedChar)

public export
isUseless : Tkn -> Bool
isUseless tkn = case tkn of
                  TknComment x => True
                  TknWhitespace => True
                  TknLB => True
                  _ => False

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei