text:
module Circuits.Idealised.Parser

import Data.Nat
import Data.List1

import public Circuits.Common.Lexer
import public Circuits.Common.Parser

import        Circuits.Idealised.Core

import        Circuits.Idealised.Types
import public Circuits.Idealised.AST
import public Circuits.Idealised.Lexer

%hide logic
%hide array
%hide type

%default total

namespace Direction
  export
  direction : Rule Direction
  direction = gives "input" INPUT <|> gives "output" OUTPUT

namespace Types

  mutual
    logic : Rule DType
    logic = gives "logic" LOGIC

    array : Rule DType
    array
        = do ty <- logic
             ns <- indices
             pure (arraytype ty ns)
      where
        index : Rule Whole
        index
          = do symbol "["
               n <- whole
               symbol "]"
               pure n

        indices : Rule (List1 Whole)
        indices = some index

        arraytype : DType -> List1 Whole -> DType
        arraytype ty (x:::xs) = foldl (\ty, n => BVECT n ty) ty (x::xs)

    export
    type : Rule DType
    type = array <|> logic

namespace Kinds

  export
  gateKind : Rule GateKind
  gateKind =  gives "nand" ANDN
          <|> gives "and"  AND
          <|> gives "xor"  XOR
          <|> gives "xnor" XORN
          <|> gives "ior"  IOR
          <|> gives "nior" IORN
          <|> gives "join" JOIN

namespace Terms

  portDecl : Rule (Location, Ref, Direction, DType)
  portDecl
    = do s <- Toolkit.location
         d <- direction
         t <- type
         r <- ref
         pure (s,r,d,t)

  portList : Rule (List1 (Location,Ref, Direction, DType))
  portList
    = do symbol "("
         ps <- sepBy1 (symbol ",") portDecl
         symbol ")"
         symbol ";"
         pure ps

  data Body = WDecl  FileContext DType Ref Ref
            | GInst  FileContext GateKind Ref Ref Ref
            | DInst  FileContext Ref Ref Ref
            | NInst  FileContext Ref Ref
            | MInst  FileContext Ref Ref Ref Ref
            | ISInst FileContext Ref Ref
            | IEInst FileContext End Ref Ref Ref
            | IPInst FileContext Nat Ref Ref Ref Ref

            | ESInst FileContext Ref Ref
            | Merge  FileContext Ref Ref Ref

  gateNot : Rule Body
  gateNot
    = do s <- Toolkit.location
         keyword "not"
         symbol "("
         o <- ref
         symbol ","
         i <- ref
         fc <- sFooter s
         pure (NInst fc o i)

  gateBin : Rule Body
  gateBin
    = do s <- Toolkit.location
         k <- gateKind
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         e <- Toolkit.location
         pure (GInst fc k o a b)

  gateCopy : Rule Body
  gateCopy
    = do s <- Toolkit.location
         keyword "copy"
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (DInst fc o a b)

  gateMux : Rule Body
  gateMux
    = do s <- Toolkit.location
         keyword "mux"
         symbol "("
         o <- ref
         symbol ","
         c <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (MInst fc o c a b)

  gateMerge : Rule Body
  gateMerge
    = do s <- Toolkit.location
         keyword "merge"
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (Merge fc o a b)

  gateSplit : Rule Body
  gateSplit
      = singletonI <|> singletonE <|> edge <|> split
    where

      singletonE : Rule Body
      singletonE
        = do s <- Toolkit.location
             keyword "extract"
             symbol "("
             o <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (ISInst fc o i)

      singletonI : Rule Body
      singletonI
        = do s <- Toolkit.location
             keyword "insert"
             symbol "("
             o <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (ESInst fc o i)

      kind : Rule End
      kind = gives "first" F <|> gives "last" L

      edge : Rule Body
      edge
        = do s <- Toolkit.location
             k <- kind
             symbol "("
             a <- ref
             symbol ","
             b <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (IEInst fc k a b i)

      split : Rule Body
      split
        = do s <- Toolkit.location
             keyword "index"
             symbol "["
             n <- nat
             symbol "]"
             symbol "("
             a <- ref
             symbol ","
             b <- ref
             symbol ","
             x <- ref
             symbol ","
             y <- ref
             fc <- sFooter s
             pure (IPInst fc n a b x y)

  wireDecl : Rule Body
  wireDecl
      = do s <- Toolkit.location
           keyword "wire"
           t <- type
           keyword "as"
           symbol "("
           a <- ref
           symbol ","
           b <- ref
           symbol ")"
           symbol ";"
           e <- Toolkit.location
           pure (WDecl (newFC s e) t a b)

  expr : Rule Body
  expr =  wireDecl
      <|> gateNot
      <|> gateBin
      <|> gateCopy
      <|> gateSplit
      <|> gateMux
      <|> gateSplit
      <|> gateMerge

  foldBody : Location
          -> List Body
          -> AST
  foldBody l Nil
        = Stop (newFC l l)
  foldBody l (head :: tail)
        = foldr doFold (Stop (newFC l l)) (head :: tail)
    where
      doFold : Body -> AST -> AST
      doFold (WDecl x y z w) accum
        = Wire x y z w accum

      doFold (MInst v x y z w) accum
        = Seq (Mux v (Var x) (Var y) (Var z) (Var w))
              accum

      doFold (GInst x k y z w) accum
        = Seq (Gate x k (Var y) (Var z) (Var w))
              accum

      doFold (DInst x y z w) accum
        = Seq (Dup x (Var y) (Var z) (Var w))
              accum

      doFold (NInst x y z) accum
        = Seq (Not x (Var y) (Var z))
              accum

      doFold (ISInst x y z) accum
        = Seq (IndexS x (Var y) (Var z))
              accum

      doFold (IEInst v w x y z) accum
        = Seq (IndexE v w (Var x) (Var y) (Var z))
              accum

      doFold (IPInst u v w x y z) accum
        = Seq (IndexP u v (Var w) (Var x) (Var y) (Var z))
              accum

      doFold (ESInst fc o i) accum
        = Seq (MergeS fc (Var o) (Var i))
              accum

      doFold (Merge fc o a b) accum
        = Seq (MergeV fc (Var o) (Var a) (Var b))
              accum

  foldPorts : Location
           -> List1 (Location,Ref, Direction, DType)
           -> AST
           -> AST
  foldPorts e (x:::xs) y
    = foldr (\(s,r,d,t), body => Input (newFC s e) d t r body) y (x::xs)

  export
  design : Rule AST
  design
    = do keyword "module"
         n <- ref
         ps <- portList
         b <- many expr
         e <- Toolkit.location
         keyword "endmodule"
         symbol ";"
         pure (foldPorts e ps (foldBody e b))

namespace Idealised

  export
  fromFile : (fname : String)
                   -> Idealised AST
  fromFile fname
    = do ast <- parseFile (Parse fname)
                Idealised.Lexer
                design
                fname
         pure (setSource fname ast)

-- [ 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:
module X

export
f : Int -> Int

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Streaming.Streams

import Streaming.Internal as S
import Streaming.API as S

import Data.Functor.Of

import System.File

import Data.Strings

import Util

export
data DecodeError = CodepointOutOfRange
                 | InvalidStartByte Bits8
                 | CodepointEndedEarly

export
Show DecodeError where
  show CodepointOutOfRange = "CodepointOutOfRange"
  show (InvalidStartByte x) = "InvalidStartByte " ++ show x
  show CodepointEndedEarly = "CodepointEndedEarly"

export
data EncodeError = EncCodepointOutOfRange
-- data EncodeError = CodepointOutOfRange
--                  | InvalidStartByte Bits8
--                  | CodepointEndedEarly
--
-- export
export
Show EncodeError where
  show EncCodepointOutOfRange = "CodepointOutOfRange"
--   show (InvalidStartByte x) = "InvalidStartByte " ++ show x
--   show CodepointEndedEarly = "CodepointEndedEarly"

{-
The intent of this module is to provide common stream sources, it's not very
thought-through at the moment and is mostly used as a testbed for things that
move elsewhere.
-}

export
stdinLn : HasIO io => Stream (Of String) io ()
stdinLn = effect $ do
   False <- fEOF stdin
     | True => pure (Return ())
   x <- getLine
   pure $ wrap (x :> stdinLn)

-- readFile : HasIO io =>

-- stdinLn : HasIO io => Stream (Of String) io ()
-- stdinLn = ?sdff
  -- streamFold pure join (\(s :> act) => putStrLn s *> act) str
  -- fflush stdout

export
stdoutLn : HasIO io => Stream (Of String) io () -> io ()
stdoutLn str = do
  streamFold pure join (\(s :> act) => putStrLn s *> act) str
  fflush stdout

export
stdoutChr : HasIO io => Stream (Of Char) io () -> io ()
stdoutChr str = do
  streamFold pure join (\(s :> act) => putChar s *> act) str
  fflush stdout

export
stdoutChrLn : HasIO io => Stream (Of Char) io () -> io ()
stdoutChrLn str = do
  streamFold pure join (\(s :> act) => putChar s *> act) str
  putChar '\n'
  fflush stdout

export
stdoutChrLn' : HasIO io => Stream (Of Char) io r -> io r
stdoutChrLn' str = do
  r <- streamFold pure join (\(s :> act) => putChar s *> act) str
  putChar '\n'
  fflush stdout
  pure r

{-

>>> S.sum $ S.take 3 (S.readLn :: Stream (Of Int) IO ())
1<Enter>
2<Enter>
3<Enter>
6 :> ()

>>> S.stdoutLn $ S.map (map toUpper) $ S.take 2 S.stdinLn
hello<Enter>
HELLO
world!<Enter>
WORLD!

-}

ofHandle : File -> Stream (Of Char) IO ()
ofHandle handle = Build (\r,eff,step => bef handle r eff step)
  where
    bef : File -> (() -> b) -> (eff : IO b -> b) -> (step : Of Char b -> b) -> b
    bef file r eff step = eff $ do
      False <- fEOF file
        | True => r <$> pclose file
      Right c <- fGetChar file
        | Left err => do Prelude.putStrLn "file read error"
                         r <$> pclose file
      pure $ step (c :> bef file r eff step)

foobaloo1 : IO ()
foobaloo1 = do
  z <- the (IO (Of Int ())) (sum $ maps cast $ take 3 stdinLn)
  printLn z

foobaloo2 : IO ()
foobaloo2 = stdoutLn $ maps toUpper $ take 2 stdinLn

foobaloo3 : IO ()
foobaloo3 = stdoutLn $ maps toUpper $ stdinLn


text:
import InfIO

%default total

totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action = do
  putStr prompt
  cmd <- getLine
  putStr (action cmd)
  totalREPL prompt action

partial
main : IO ()
main = run forever (totalREPL "\n: " toUpper)

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 Data.Zippable

%default total

---------------------------
-- Zips and unzips --
---------------------------

||| The `Zippable` interface describes how you can combine and split the
||| elements in a parameterised type.
||| @ z the parameterised type
public export
interface Zippable z where
  ||| Combine two parameterised types by applying a function.
  ||| @ z the parameterised type
  ||| @ func the function to combine elements with
  zipWith : (func : a -> b -> c) -> z a -> z b -> z c

  ||| Combine two parameterised types into a parameterised type of pairs.
  ||| @ z the parameterised type
  zip : z a -> z b -> z (a, b)
  zip = zipWith (,)

  infixr 6 `zip`

  ||| Combine three parameterised types by applying a function.
  ||| @ z the parameterised type
  ||| @ func the function to combine elements with
  zipWith3 : (func : a -> b -> c -> d) -> z a -> z b -> z c -> z d

  ||| Combine three parameterised types into a parameterised type of triplets.
  ||| @ z the parameterised type
  zip3 : z a -> z b -> z c -> z (a, b, c)
  zip3 = zipWith3 (,,)

  ||| Split a parameterised type by applying a function into a pair of
  ||| parameterised types.
  ||| @ z the parameterised type
  ||| @ func the function to split elements with
  unzipWith : (func : a -> (b, c)) -> z a -> (z b, z c)

  ||| Split a parameterised type of pairs into a pair of parameterised types.
  ||| @ z the parameterised type
  unzip : z (a, b) -> (z a, z b)
  unzip = unzipWith id

  ||| Split a parameterised type by applying a function into a triplet of
  ||| parameterised types.
  ||| @ z the parameterised type
  ||| @ func the function to split elements with
  unzipWith3 : (func : a -> (b, c, d)) -> z a -> (z b, z c, z d)

  ||| Split a parameterised type of triplets into a triplet of parameterised
  ||| types.
  ||| @ z the parameterised type
  unzip3 : z (a, b, c) -> (z a, z b, z c)
  unzip3 = unzipWith3 id


text:
module Commons.Data.Rig

import public Data.Vect

%default total
%access public export

data TyRig = None | One | Tonne

noneNotOne : (None = One) -> Void
noneNotOne Refl impossible

noneNotTonne : (None = Tonne) -> Void
noneNotTonne Refl impossible

oneNotTonne : (One = Tonne) -> Void
oneNotTonne Refl impossible

DecEq TyRig where
  decEq None None = Yes Refl
  decEq None One = No noneNotOne
  decEq None Tonne = No noneNotTonne
  decEq One None = No (negEqSym noneNotOne)
  decEq One One = Yes Refl
  decEq One Tonne = No oneNotTonne
  decEq Tonne None = No (negEqSym noneNotTonne)
  decEq Tonne One = No (negEqSym oneNotTonne)
  decEq Tonne Tonne = Yes Refl

export
plus : TyRig -> TyRig -> TyRig
plus None None = None
plus None One = One
plus None Tonne = Tonne
plus One None = One
plus One One = Tonne
plus One Tonne = Tonne
plus Tonne None = Tonne
plus Tonne One = Tonne
plus Tonne Tonne = Tonne

export
multiply : TyRig -> TyRig -> TyRig
multiply None None = None
multiply None One = None
multiply None Tonne = None
multiply One None = None
multiply One One = One
multiply One Tonne = Tonne
multiply Tonne None = None
multiply Tonne One = Tonne
multiply Tonne Tonne = Tonne

export
product : Vect n TyRig -> Vect n TyRig -> Vect n TyRig
product [] [] = []
product (x :: xs) (y :: ys) = multiply x y :: product xs ys

export
sum : Vect n TyRig -> Vect n TyRig -> Vect n TyRig
sum [] [] = []
sum (x :: xs) (y :: ys) = plus x y :: sum xs ys

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module GRIN.GrinM

import Data.SortedMap
import Data.SortedSet

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

import GRIN.AST
import public GRIN.Error
import public GRIN.GrinState
import GRIN.Analysis.CallGraph

export
record GrinT name (m : Type -> Type) a where
    constructor MkGrinM
    unGrinM : StateT (GrinState name) m a

public export
GrinM : Type -> Type -> Type
GrinM name a = GrinT name Identity a

export
Functor m => Functor (GrinT name m) where
    map f = MkGrinM . map f . unGrinM

export
Monad m => Applicative (GrinT name m) where
    pure = MkGrinM . pure
    f <*> x = MkGrinM $ unGrinM f <*> unGrinM x

export
Monad m => Monad (GrinT name m) where
    x >>= f = MkGrinM $ unGrinM x >>= unGrinM . f

export
MonadTrans (GrinT name) where
    lift = MkGrinM . lift

export
Monad m => MonadState (GrinState name) (GrinT name m) where
    get = MkGrinM get
    put = MkGrinM . put
    state = MkGrinM . state

export
HasIO m => HasIO (GrinT name m) where
    liftIO = lift . liftIO

export
mapProg : Monad m => (Prog name -> Prog name) -> GrinT name m ()
mapProg f = modify $ record { prog $= f }

export
putProg : Monad m => Prog name -> GrinT name m ()
putProg p = modify $ record { prog = p }

export
invalidate : Monad m => AnalysisTag -> GrinT name m ()
invalidate t = modify $ case t of
    CallsGraph => record { calls = Nothing }
    CalledByGraph => record { calledBy = Nothing }
    CallGraphs => record { calls = Nothing, calledBy = Nothing }

export
getCalls : Monad m => Ord name => GrinT name m (CallGraph name)
getCalls = do
    Nothing <- gets calls
        | Just cg => pure cg
    p <- gets prog
    let cg = callsGraph p
    modify $ record { calls = Just cg }
    pure cg

export
getCalledBy : Monad m => Ord name => GrinT name m (CallGraph name)
getCalledBy = do
    Nothing <- gets calledBy
        | Just cg => pure cg
    calls <- getCalls
    let cg = calledByGraph calls
    modify $ record { calledBy = Just cg }
    pure cg

export
liftGrinM : (forall a. m1 a -> m2 a) -> GrinT name m1 a -> GrinT name m2 a
liftGrinM f (MkGrinM (ST m)) = MkGrinM $ ST \st => f $ m st

export
newError : Monad m => Error -> GrinT name m ()
newError err = modify $ record { errors $= (err ::) }

export
resetVarMap : Monad m => GrinT name m ()
resetVarMap = modify $ record { varMap = empty }

export
runGrinT' : GrinT name m a -> GrinState name -> m (GrinState name, a)
runGrinT' m a = runStateT a $ unGrinM m

export
execGrinT' : Functor m => GrinT name m a -> GrinState name -> m (GrinState name)
execGrinT' m st = fst <$> runGrinT' m st

export
runGrinT : Ord name => Functor m => GrinT name m a -> Prog name -> m (Prog name, a)
runGrinT m p = mapFst prog <$> runGrinT' m (newGrinState p)

export
runGrinM' : GrinM name a -> GrinState name -> (GrinState name, a)
runGrinM' m st = runIdentity $ runGrinT' m st

export
runGrinM : Ord name => GrinM name a -> Prog name -> (Prog name, a)
runGrinM m p = runIdentity $ runGrinT m p

export
execGrinM : Ord name => GrinM name a -> Prog name -> Prog name
execGrinM m p = fst $ runGrinM m p


text:
module TyTTP.Core.Routing

import Control.Monad.Maybe
import TyTTP.Core.Context

export
routes : Alternative m
  => List (
    Context me u h1 s h2 a b
    -> m $ Context me' p' h1' s' h2' a' b'
  )
  -> Context me u h1 s h2 a b
  -> m $ Context me' p' h1' s' h2' a' b'
routes handlers ctx = choiceMap ($ ctx) handlers

export
routes' : Monad m
  => (
    Context me u h1 s h2 a b
    -> m $ Context me' p' h1' s' h2' a' b'
  )
  -> List (
    Context me u h1 s h2 a b
    -> MaybeT m $ Context me' p' h1' s' h2' a' b'
  )
  -> Context me u h1 s h2 a b
  -> m $ Context me' p' h1' s' h2' a' b'
routes' def handlers ctx = do
  Just result <- runMaybeT $ routes handlers ctx
    | Nothing => def ctx
  pure result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
import Data.Vect

data WordState: (guesses_remaining: Nat) -> (letters: Nat) -> Type where
  MkWordState: (word: String) -> (missing: Vect letters Char) -> WordState guesses_remaining letters

data Finished: Type where
  Lost: (game: WordState 0 (S letters))   -> Finished
  Won:  (game: WordState (S remaining) 0) -> Finished

data ValidInput: List Char -> Type where
  Letter: (c: Char) -> ValidInput [c]

total emptyNotValidInput : ValidInput [] -> Void
emptyNotValidInput (Letter _) impossible

total tooManyChars : ValidInput (x :: (y :: xs)) -> Void
tooManyChars (Letter _) impossible

total isValidInput: (chars: List Char) -> Dec (ValidInput chars)
isValidInput [] = No emptyNotValidInput
isValidInput (x :: []) = Yes(Letter x)
isValidInput (x :: (y :: xs)) = No tooManyChars

isValidString: (s: String) -> Dec(ValidInput(unpack s))
isValidString s = isValidInput (unpack s)

readGuess: IO (x ** ValidInput x)
readGuess = do
  putStr "Guess: "
  userGuess <- getLine
  case isValidString (toUpper userGuess) of
    (Yes prf) => pure (_ ** prf)
    (No contra) => do
      putStrLn ("Invalid guess = [" ++ userGuess ++"]")
      readGuess

removeElem: (value: a) -> (xs: Vect (S n) a) -> {auto prf: Elem value xs} -> Vect n a
removeElem             value (value :: ys) {prf = Here}          = ys
removeElem {n = Z}     value (y     :: []) {prf = (There later)} = absurd later
removeElem {n = (S k)} value (y     :: ys) {prf = (There later)} = y :: removeElem value ys

processGuess: (letter: Char) ->
              WordState (S guesses) (S letters) ->
              Either (WordState guesses (S letters))
                     (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
  (Yes prf) => Right (MkWordState word (removeElem letter missing))
  (No contra) => Left (MkWordState word missing)

game: (state: WordState (S guesses) (S letters)) -> IO Finished
game {guesses} {letters} state = do
  ([input] ** Letter input) <- readGuess
  case processGuess input state of
    (Left l) => do
      putStrLn "Wrong!"
      case guesses of
        Z   => pure (Lost l)
        S k => game l
    (Right r) => do
      putStrLn "Right!"
      case letters of
        Z => pure (Won r)
        (S k) => game r

main: IO ()
main =
  let
    wordToGuess = MkWordState "Test" ['T', 'E', 'S']
  in
    do
      result <- game {guesses=2} wordToGuess
      case result of
        (Lost (MkWordState word missing)) => putStrLn ("You lost. The word was" ++ word)
        (Won game) => putStrLn "You win"

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Example.Validation

import Data.Fin
import Data.String

import Flexidisc
import Flexidisc.Validation

data AcceptedColour = Red | Blue

data Error = CantParseColour String
           | CantParseQuantity String

parseColour : String -> ValidationL Error AcceptedColour
parseColour "red" = Valid Red
parseColour "blue" = Valid Blue
parseColour str = Error $ pure (CantParseColour str)

parseQuantity : String -> ValidationL Error Nat
parseQuantity str = maybe (Error (pure $ CantParseQuantity str))
                          Valid
                          $ parsePositive str

Line : (m : Type -> Type) -> (name : Type) -> (qty : Type) -> Type
Line m name qty = RecordM m String ["colour" ::: name, "qty" ::: qty]

ImportedLine : Type
ImportedLine = Line id String String

ValidatedLine : Type
ValidatedLine = Line id AcceptedColour Nat

validateLine : ImportedLine -> ValidationL Error ValidatedLine
validateLine x = traverseRecord
                   [ "colour" := parseColour
                   , "qty" := parseQuantity
                   ] x

testOK : ValidationL Error ValidatedLine
testOK = validateLine ["colour" := "red", "qty" := "100"]
-- Valid ["name" := Red, "qty" := 100]

testKOColour : ValidationL Error ValidatedLine
testKOColour = validateLine ["colour" := "reed", "qty" := "100"]
-- Error [CantParseColour "reed"]

testKOQty : ValidationL Error ValidatedLine
testKOQty = validateLine ["colour" := "red", "qty" := "-10"]
-- Error [CantParseQuantity "-10"]

testKOBoth : ValidationL Error ValidatedLine
testKOBoth = validateLine ["colour" := "reed", "qty" := "-10"]
-- Error [CantParseColour "reed", CantParseQuantity "-10"]

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Language.LSP.DocumentHighlight

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Name
import Data.List
import Idris.Doc.String
import Language.LSP.Message
import Libraries.Data.NameMap
import Server.Configuration
import Server.Log
import Server.Utils

makeHighlight : NonEmptyFC -> DocumentHighlight
makeHighlight fc = MkDocumentHighlight
  { range = cast fc
  , kind = Nothing
  }

export
documentHighlights : Ref Ctxt Defs
                  => Ref MD Metadata
                  => Ref LSPConf LSPConfiguration
                  => DocumentHighlightParams -> Core (List DocumentHighlight)
documentHighlights params = do
  logI DocumentHighlight "Searching for \{show params.textDocument.uri}"
  Just (uri, _) <- gets LSPConf openFile
    | Nothing => logE DocumentHighlight "No open file" >> pure []
  let True = uri == params.textDocument.uri
    | False => do
        logD DocumentHighlight "Expected request for the currently opened file \{show uri}, instead received \{show params.textDocument.uri}"
        pure []

  let line = params.position.line
  let col  = params.position.character
  nameLocs <- gets MD nameLocMap
  let Just (_, name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => logD DocumentHighlight "No name found at \{show line}:\{show col}}" >> pure []
  logI DocumentHighlight "Found name \{show name}"

  matchingNames <- gets MD (nub . map fst . filter ((==) name . snd) . toList . nameLocMap)
  logI DocumentHighlight "Found \{show $ length matchingNames} matches"
  pure (makeHighlight <$> matchingNames)


text:
module Text.Show.Value

import Data.Vect
import Data.List1
import Generics.Derive
import Text.Lexer
import Text.Parser
import Text.PrettyPrint.Prettyprinter

%hide Language.Reflection.TT.Name

%language ElabReflection

%default total

||| A name.
public export
record Name where
  constructor MkName
  unName : String

%runElab derive "Text.Show.Value.Name" [Generic,Meta,Show,Eq,Ord,Semigroup]

public export
FromString Name where fromString = MkName

public export
Pretty Name where
  pretty = pretty . unName

||| Generic Idris values.
||| The `String` in the literals is the text for the literals "as is".
|||
||| A chain of infix constructors means that they appeared in the input string
||| without parentheses, i.e
|||
||| `1 :+: 2 :*: 3` is represented with `InfixCons 1 [(":+:",2),(":*:",3)]`, whereas
|||
||| `1 :+: (2 :*: 3)` is represented with `InfixCons 1 [(":+:",InfixCons 2 [(":*:",3)])]`.
public export
data Value = Con Name (List Value)
           | InfixCons Value (List (Name,Value))
           | Rec Name (List (Name,Value))
           | Tuple Value Value (List Value) -- At least two values
           | Lst (List Value)
           | Neg Value
           | Natural String
           | Dbl String
           | Chr String
           | Str String

%runElab derive "Value" [Generic,Meta]

export
Eq Value where (==) = assert_total genEq

export
Show Value where showPrec = assert_total genShowPrec

export
depth : Value -> Nat
depth v = case v of
               (Con x xs)       => S $ maxDepth xs
               (InfixCons x xs) => S $ maxDepthP xs
               (Rec x xs)       => S $ maxDepthP xs
               (Tuple x y xs)   => S . max (depth x) $ max (depth y) (maxDepth xs)
               (Lst xs)         => S $ maxDepth xs
               (Neg x)          => S $ depth x
               (Natural x)      => 0
               (Dbl x)          => 0
               (Chr x)          => 0
               (Str x)          => 0

  where maxDepth : List Value -> Nat
        maxDepth []       = 0
        maxDepth (h :: t) = max (depth h) (maxDepth t)

        maxDepthP : List (a,Value) -> Nat
        maxDepthP []           = 0
        maxDepthP ((_,h) :: t) = max (depth h) (maxDepthP t)

||| Displays an applied binary operator.
||| If the same operator appears several times in a row,
||| this is treated as a list of infix constructors.
public export
binOp : Name -> Value -> Value -> Value
binOp op pvx pvy =
   case pvy of
        InfixCons pv1 pairs@((op2, pv2) :: xs) =>
          if op2 == op then InfixCons pvx ((op,pvy) :: pairs)
                       else InfixCons pvx [(op,pvy)]
        _ => InfixCons pvx [(op,pvy)]

||| Hide constructors matching the given predicate.
||| If the hidden value is in a record, we also hide
||| the corresponding record field.
|||
||| If the boolean flag is true, then we also hide
||| constructors all of whose fields were hidden.
public export covering
hideCon : Bool -> (Name -> Bool) -> Value -> Value
hideCon collapse hidden = toVal . delMaybe
  where
  hiddenV : Value
  hiddenV = Con "_" []

  toVal : Maybe Value -> Value
  toVal = fromMaybe hiddenV

  mutual
    covering
    delMany : (Functor f, Foldable f) => f Value -> Maybe (f Value)
    delMany vals =
      let newVals = map delMaybe vals
       in if collapse && all isNothing newVals
            then Nothing
            else Just (map toVal newVals)

    covering
    delMaybe : Value -> Maybe Value
    delMaybe val =
      case val of
           Con x vs =>
             if hidden x
               then Nothing
               else if null vs
                 then Just val
                 else Con x <$> delMany vs

           InfixCons v ys =>
             let (cs,vs) = unzip ys
                 mbs     = delay $ map delMaybe vs
              in if any hidden cs
                   then Nothing
                   else do (v1 ::: vs1) <- delMany (v ::: vs)
                           pure (InfixCons v1 (zip cs vs1))

           Rec x fs =>
             let (ls,vs) = delay $ unzip fs
                 mbs     = delay $ map delMaybe vs
              in if hidden x
                   then Nothing
                   else if null fs
                     then Just val
                     else if collapse && all isNothing mbs
                       then Nothing
                       else let ps = mapMaybe (\(f,mv) => (f,) <$> mv)
                                              (zip ls mbs)
                             in Just (Rec x ps)

           Tuple v1 v2 vs  => let vs2 = delMany (v1 :: v2 :: Vect.fromList vs)
                               in map (\(a::b::xs) => Tuple a b (toList xs)) vs2

           Lst []          => Just val
           Lst vs          => Lst <$> delMany vs
           Neg v           => Neg <$> delMaybe v
           Natural _       => Just val
           Dbl _           => Just val
           Chr _           => Just val
           Str _           => Just val

--------------------------------------------------------------------------------
--          Tokenizer
--------------------------------------------------------------------------------

-- taken from the actual Idris2 tokenizer
data Flavour = Capitalised | Normal

isIdentStart : Flavour -> Char -> Bool
isIdentStart _           '_' = True
isIdentStart Capitalised  x  = isUpper x
isIdentStart _            x  = isAlpha x

isIdentTrailing : Char -> Bool
isIdentTrailing '\'' = True
isIdentTrailing '_'  = True
isIdentTrailing x    = isAlphaNum x || x > chr 160

ident : Flavour -> Lexer
ident flavour =   (pred $ isIdentStart flavour)
              <+> (many $ pred isIdentTrailing )

identNormal : Lexer
identNormal = ident Normal

namespaceIdent : Lexer
namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.'))

namespacedIdent : Lexer
namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal)

public export
data ShowToken = StringLit String
               | NatLit    String
               | DblLit    String
               | CharLit   String
               | Ident     String
               | Symbol    String
               | Op        String
               | Space     String

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

holeIdent : Lexer
holeIdent = is '?' <+> identNormal

dotIdent : Lexer
dotIdent = is '.' <+> identNormal

pragma : Lexer
pragma = is '%' <+> identNormal

isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")

op : Lexer
op = some (pred isOpChar)

isSymbol : Char -> Bool
isSymbol c = c `elem` (unpack "()[]{},")

parseOp : String -> ShowToken
parseOp "=" = Symbol "="
parseOp s   = Op s

anyIdent : Lexer
anyIdent =  choice {t = List} [ namespacedIdent
                              , identNormal
                              , dotIdent
                              , holeIdent
                              , pragma
                              ]

doubleLit : Lexer
doubleLit = digits <+> is '.' <+> digits <+> opt
             ((is 'e' <|> is 'E') <+> opt (is '-' <|> is '+') <+> digits)

tokens : TokenMap ShowToken
tokens = [ (doubleLit, DblLit)
         , (binLit <|> octLit <|> hexLit <|> digits, NatLit)
         , (stringLit, StringLit)
         , (charLit, CharLit)
         , (anyIdent, Ident)
         , (op, parseOp)
         , (pred isSymbol, Symbol)
         , (spaces, Space)
         ]

public export
data Err = LexErr Int Int String
         | ParseErr String
         | EOIErr (List $ WithBounds ShowToken)

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

export
lex : String -> Either Err (List $ WithBounds ShowToken)
lex str = case lex tokens str of
               (ts, (_, _, "")) => Right $ filter (notSpace . val) ts
               (_, (a,b,c))     => Left $ LexErr a b c
  where notSpace : ShowToken -> Bool
        notSpace (Space _) = False
        notSpace _         = True

export
lex_ : String -> Either Err (List ShowToken)
lex_ = (map . map) val . lex

--------------------------------------------------------------------------------
--          Parser
--------------------------------------------------------------------------------

Rule : Type -> Type
Rule = Grammar () ShowToken True

EmptyRule : Type -> Type
EmptyRule = Grammar () ShowToken False

constant : Rule Value
constant = terminal "Expected constant" $
                     \case CharLit c    => Just $ Chr c
                           DblLit d     => Just $ Dbl d
                           StringLit s  => Just $ Str s
                           NatLit s     => Just $ Natural s
                           _            => Nothing

identRule : Rule Name
identRule = terminal "Expected identifier" $
                     \case Ident s => Just $ MkName s
                           _       => Nothing

operator : Rule Name
operator = terminal "Expected operator" $
                    \case Op s => Just $ MkName s
                          _    => Nothing

minus : Rule ()
minus = terminal "Expected minus sign" $
                 \case Op "-" => Just ()
                       _      => Nothing

symbol : String -> Rule ()
symbol s = terminal ("Expected " ++ s) $
                    \case Symbol s2 => if s == s2 then Just ()
                                                  else Nothing
                          _         => Nothing

comma : Rule ()
comma = symbol ","

equals : Rule ()
equals = symbol "="

parens : {c : _} -> Inf (Grammar () ShowToken c a) -> Rule a
parens g = symbol "(" *> g <* symbol ")"

brackets : {c : _} -> Inf (Grammar () ShowToken c a) -> Rule a
brackets g = symbol "[" *> g <* symbol "]"

braces : {c : _} -> Inf (Grammar () ShowToken c a) -> Rule a
braces g = symbol "{" *> g <* symbol "}"

identOrOp : Rule Name
identOrOp = identRule <|>
            map (\(MkName n) => MkName ("(" ++ n ++ ")")) (parens operator)

unit : Rule Value
unit =  symbol "(" *> symbol ")" $> Con "()" []

mutual
  covering
  value : Rule Value
  value = choice {t = List} [ constant
                            , unit
                            , negated
                            , list
                            , tuple
                            , rec
                            , con
                            , infx
                            ]

  covering
  applied : Rule Value
  applied =   constant
          <|> unit
          <|> map (\n => Con n []) identOrOp
          <|> list
          <|> tuple
          <|> parens value

  covering
  negated : Rule Value
  negated = minus *> map Neg applied

  covering
  tuple : Rule Value
  tuple = parens $ do (v1::v2::vs) <- sepBy comma value
                        | vs => fail "Tuple needs at least two values"
                      pure (Tuple v1 v2 vs)

  covering
  list : Rule Value
  list = Lst <$> brackets (sepBy comma value)

  covering
  pair : Rule (Name,Value)
  pair = [| (,) identOrOp (equals *> value) |]

  covering
  rec : Rule Value
  rec = [| Rec identOrOp (braces $ sepBy comma pair) |]

  covering
  con : Rule Value
  con = [| Con identOrOp (many applied) |]

  covering
  infx : Rule Value
  infx = uncurry InfixCons <$> go
    where go : Rule (Value,List (Name,Value))
          go = do v    <- applied
                  op   <- operator
                  map (\(v2,ps) => (v,(op,v2) :: ps)) go <|>
                  map (\v2 => (v, [(op,v2)])) applied

export covering
parseValueE : String -> Either Err Value
parseValueE str = lex str >>= doParse
  where covering doParse : List (WithBounds ShowToken) -> Either Err Value
        doParse ts =
          case parse value ts of
               Left (Error str _ ::: _) => Left $ ParseErr str
               Right (v,[])             => Right v
               Right (_,ts)             => Left $ EOIErr ts

export covering
parseValue : String -> Maybe Value
parseValue = either (const Nothing) Just . parseValueE


text:
module Primitives

import Control.ST
import Control.ST.Exception
import DataTypes
import Util
import Ratio
import Lists
import Numbers
import Strings
import Bools
import Symbols
import Vector
import Procedures
import Data.Complex

%access public export

--------------
-- Primitives
--------------

isChar : PrimitiveLispFunc
isChar [LispCharacter _] = pure $ LispBool False
isChar _ = pure $ LispBool False

eqv : PrimitiveLispFunc
eqv [(LispBool arg1), (LispBool arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispInteger arg1), (LispInteger arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispFloat arg1), (LispFloat arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispRational arg1), (LispRational arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispComplex arg1), (LispComplex arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispString arg1), (LispString arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispCharacter arg1), (LispCharacter arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispAtom arg1), (LispAtom arg2)] = pure $ LispBool $ arg1 == arg2
eqv [(LispDottedList xs x), (LispDottedList ys y)] = eqv [LispList $ xs ++ [x], LispList $ ys ++ [y]]
eqv [(LispList arg1), (LispList arg2)] =
    if
        not (length arg1 == length arg2)
    then
        pure $ LispBool False
    else
        do
            allEq <- eqvPairs arg1 arg2
            pure $ LispBool $ (length arg1 == length arg2) && allEq
    where
    eqvPairs : List LispVal -> List LispVal -> ThrowsError Bool
    eqvPairs [] [] = pure True
    eqvPairs _ [] = pure False
    eqvPairs [] _ = pure False
    eqvPairs (x::xs) (y::ys) =
        do
            eq <- eqv [x, y]
            case eq of
                LispBool False => pure False
                LispBool True => eqvPairs xs ys
                _ => pure False
eqv [_, _] = pure $ LispBool False
eqv badArgList = Left $ NumArgs (MinMax 2 2) (cast $ length badArgList) badArgList

-- --------------
-- -- IO Primitives
-- --------------
-- makePort :: IOMode -> IOPrimitiveFunc
-- makePort mode [String filename] = fmap Port $ liftIO $ openFile filename mode
-- makePort _ _ = throw $ Default "makePort error"
--
-- closePort :: IOPrimitiveFunc
-- closePort [Port port] = liftIO $ hClose port *> (pure $ Bool True)
-- closePort _ = pure $ Bool False
--
-- writeProc :: IOPrimitiveFunc
-- writeProc [obj] = writeProc [obj, Port stdout]
-- writeProc [obj, Port port] = liftIO $ hPrint port obj *> (pure $ Bool True)
-- writeProc _ = throw $ Default "writeProc error"
--
-- readContents :: IOPrimitiveFunc
-- readContents [String filename] = fmap String $ liftIO $ readFile filename
-- readContents _ = throw $ Default "readContents error"
--

-- ioPrimitives :: [(String, IOPrimitiveFunc)]
-- ioPrimitives =
--   [ ("open-input-file", makePort ReadMode)
--   , ("open-output-file", makePort WriteMode)
--   , ("close-input-port", closePort)
--   , ("close-output-port", closePort)
--   , ("write", writeProc)
--   , ("read-contents", readContents)
--   ]

primitives : List (String, PrimitiveLispFunc)
primitives =
  vectorPrimitives ++
  listPrimitives ++
  numPrimitives ++
  strPrimitives ++
  boolPrimitives ++
  symbolPrimitives ++
  procedurePrimitives ++
  [ ("char?", isChar)
  , ("eq?", eqv)
  , ("eqv?", eqv)
  , ("equal?", eqv)
  , ("void", (\_ => pure LispVoid))
  ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module RewriteRules.EqChainInline

import Data.SortedMap
import Data.SortedSet
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Core.Context
import Data.List
import CommonDef
import Primitives.Primitives

%hide Prelude.toList

-- Note: ValueTracker is not able to handle Case transforms so we use a direct version here
--       We cover not all cases as we want to detect and transform patterns and not do general optimisations
--       We assume that a constant fold has run before (otherwise it will not work with felts)
--       Currently code duplication is not limited
--        Todo: Build a limit
--        Todo: If limit reached do not do the transform or extract into Method

-- Transforms Boolean expressions with multiple if cascades into a single if cascade where possible
--   Or formulated otherwise:
--    fun x = if x == C1 || x == C2 then E1 else E2
--   Into:
--    fun C1 = E1
--    fun C2 = E1
--    fun _ = E2
-- The transformation is:
--  From: (Example has 2 sequntial ops where first has nesting 1 and second nesting 2 | However works for any number of sequential ops with any number of nesting)
--   a1 = p == C1
--   a2 = if a1 then True else p == C2
--   a3 = if a2 then E1 else E2
--  To:
--   a3 = if p == C1 then E1 else if p == C2 then E1 else E2

data ExtractedData : Type where
    ConstData : CairoConst -> ExtractedData
    OrEqChain : CairoReg -> List CairoConst -> ExtractedData

checkAndFilterReg : CairoReg -> Maybe (CairoReg, List CairoConst) -> Maybe (CairoReg, List CairoConst)
checkAndFilterReg _ Nothing = Nothing
checkAndFilterReg r1 res@(Just (r2, _)) = if r1 == r2 then res else Nothing

constEqLookup : CairoReg -> SortedMap CairoReg ExtractedData -> Maybe ExtractedData
constEqLookup (Const c) _ = Just $ ConstData c
constEqLookup r detection = lookup r detection

mutual
    analyzeMatchingCase : SortedMap CairoReg ExtractedData -> CairoReg -> List (CairoConst, List CairoInst) -> Maybe (List CairoInst) -> Maybe (CairoReg, List CairoConst)
    analyzeMatchingCase detection branchReg [(I 1,[MKCONSTANT tr (I 1)]),(I 0, [bF])] Nothing = checkAndFilterReg tr (analyzeFalseCase detection branchReg bF)
    analyzeMatchingCase detection branchReg [(I 0, [bF]),(I 1,[MKCONSTANT tr (I 1)])] Nothing = checkAndFilterReg tr (analyzeFalseCase detection branchReg bF)
    analyzeMatchingCase detection branchReg [(I 1,[MKCONSTANT tr (I 1)])] (Just [bF]) = checkAndFilterReg tr (analyzeFalseCase detection branchReg bF)
    analyzeMatchingCase detection branchReg [(I 0, [bF])] (Just [MKCONSTANT tr (I 1)]) = checkAndFilterReg tr (analyzeFalseCase detection branchReg bF)
    analyzeMatchingCase _ _ _ _ = Nothing

    analyzeFalseCase : SortedMap CairoReg ExtractedData -> CairoReg -> CairoInst -> Maybe (CairoReg, List CairoConst)
    analyzeFalseCase detection _ (MKCONSTANT tr (I 0)) = Just (tr, [])
    analyzeFalseCase detection branchReg (OP tr _ (EQ _) [a, b]) = if a == branchReg
        then process (constEqLookup b detection)
        else if b == branchReg
            then process (constEqLookup a detection)
            else Nothing
                where process : Maybe ExtractedData -> Maybe (CairoReg, List CairoConst)
                      process (Just (ConstData c)) = Just (tr, [c])
                      process _ = Nothing

    analyzeFalseCase detection branchReg (CONSTCASE r alts def) = process (constEqLookup r detection)
        where appendResult : List CairoConst -> Maybe (CairoReg, List CairoConst) -> Maybe (CairoReg, List CairoConst)
              appendResult cs (Just (resReg, cs2)) = Just (resReg, cs2 ++ cs)
              appendResult _ Nothing = Nothing
              process : Maybe ExtractedData -> Maybe (CairoReg, List CairoConst)
              process (Just (OrEqChain brReg cs)) = if branchReg == brReg
                then appendResult cs (analyzeMatchingCase detection branchReg alts def)
                else Nothing
              process _ = Nothing
    analyzeFalseCase _ _ _ = Nothing

analyzeCase : SortedMap CairoReg ExtractedData -> CairoInst -> SortedMap CairoReg ExtractedData
analyzeCase detection (CONSTCASE r alts def) = process (constEqLookup r detection)
    where buildResult : CairoReg -> List CairoConst -> Maybe (CairoReg, List CairoConst) -> SortedMap CairoReg ExtractedData
          buildResult brReg cs (Just (resReg, cs2)) = insert resReg (OrEqChain brReg (cs2 ++ cs)) detection
          buildResult _ _ Nothing = detection
          process : Maybe ExtractedData -> SortedMap CairoReg ExtractedData
          process (Just (OrEqChain brReg cs)) = buildResult brReg cs (analyzeMatchingCase detection brReg alts def)
          process _ = detection
analyzeCase detection _ = detection

mutual
    inlineOrEqChain : CairoInst -> SortedMap CairoReg ExtractedData -> (CairoInst, SortedMap CairoReg ExtractedData)
    inlineOrEqChain inst@(ASSIGN r s) detection = (inst, propagate $ constEqLookup s detection)
        where propagate : Maybe ExtractedData -> SortedMap CairoReg ExtractedData
              propagate Nothing = detection
              propagate (Just oec) = insert r oec detection

    inlineOrEqChain inst@(MKCONSTANT r c) detection = (inst, insert r (ConstData c) detection)
    inlineOrEqChain inst@(OP r _ (EQ _) [a, b]) detection = (inst, process (constEqLookup a detection) (constEqLookup b detection))
        where process : Maybe ExtractedData -> Maybe ExtractedData -> SortedMap CairoReg ExtractedData
              process (Just (ConstData (I 1))) (Just chain@(OrEqChain _ _)) = insert r chain detection
              process (Just chain@(OrEqChain _ _)) (Just (ConstData (I 1))) = insert r chain detection
              process (Just (ConstData c)) _ = insert r (OrEqChain b [c]) detection
              process _ (Just (ConstData c)) = insert r (OrEqChain a [c]) detection
              process _ _ = detection

    inlineOrEqChain inst@(OP r _ (BOr IntType) [a, b]) detection = (inst, process (constEqLookup a detection) (constEqLookup b detection))
        where process : Maybe ExtractedData -> Maybe ExtractedData -> SortedMap CairoReg ExtractedData
              process (Just (OrEqChain r1 c1)) (Just (OrEqChain r2 c2)) = if r1 == r2
                then insert r (OrEqChain r1 (c1 ++ c2)) detection
                else detection
              process _ _ = detection
    inlineOrEqChain (CASE r alts def) detection = (CASE r (map (\(i,b) => (i, processInsts detection b)) alts) (map (processInsts detection) def), detection)
    -- for safety as im unsure how ANF behaves in that case
    inlineOrEqChain (CONSTCASE r [(i,b)] Nothing) detection = (CONSTCASE r [(i, processInsts detection b)] Nothing, detection)
    inlineOrEqChain (CONSTCASE r [] (Just b)) detection = (CONSTCASE r [] (Just (processInsts detection b)), detection)
    inlineOrEqChain inst@(CONSTCASE r alts def) detection = (process (constEqLookup r detection), analyzeCase detection inst)
      where processedAlts : List (CairoConst, List CairoInst)
            processedAlts = map (\(c,b) => (c, processInsts detection b)) alts
            processedDef : Maybe (List CairoInst)
            processedDef = map (processInsts detection) def
            trueCase : List CairoInst
            trueCase = fromMaybe (fromMaybe (assert_total $ idris_crash "if without true case not allowed") def) (lookup (I 1) (fromList processedAlts))
            falseCase : List CairoInst
            falseCase = fromMaybe (fromMaybe (assert_total $ idris_crash "if without false case not allowed") def) (lookup (I 0) (fromList processedAlts))
            process : Maybe ExtractedData -> CairoInst
            -- Todo: add size limit on true but for that we need complexity/size functions
            process (Just (OrEqChain r2 cs)) = CONSTCASE r2 (map (\c => (c, trueCase)) (toList $ SortedSet.fromList cs)) (Just falseCase)
            process _ = CONSTCASE r processedAlts processedDef

    inlineOrEqChain inst detection = (inst, detection)

    processInsts: SortedMap CairoReg ExtractedData -> List CairoInst -> List CairoInst
    processInsts state insts = snd $ foldl (\(s,acc),i => let (ni,ns) = inlineOrEqChain i s in (ns, acc ++ [ni])) (state, []) insts

eqChainInlineDef : (Name, CairoDef) -> (Name, CairoDef)
eqChainInlineDef (name, FunDef params implicits rets body) = (name, FunDef params implicits rets (processInsts empty body))
eqChainInlineDef def = def

export
eqChainInline : List (Name, CairoDef) -> List (Name, CairoDef)
eqChainInline defs = map eqChainInlineDef defs

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Eval

-- Evaluators for terms in the untyped
-- lambda calculus.

import BigStep
import Equivalence
import Determinism
import Progress
import Step
import Subst
import Term

%access export

------------------------------------------------------------
-- Begin: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS

eval : (e : Term 0) -> (e' : Term 0 ** (Value e', TransStep e e'))
eval e = case progress e of
  Left v           => (e ** (v, TStRefl e))
  Right (e' ** s') => let (e'' ** (v'', s'')) = eval e'
                      in (e'' ** (v'', TStTrans s' s''))

-- End: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS
----------------------------------------------------------

----------------------------------------------------------
-- Begin: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS

eval' : Term 0 -> Term 0
eval' (TVar i)       = absurd $ FinZAbsurd i
eval' (TAbs e)       = TAbs e
eval' (TApp e1 e2)   = let (TAbs e1v) = eval' e1
                           e2v        = eval' e2
                       in eval' $ subst e2v FZ e1v
eval' TZero          = TZero
eval' (TSucc e)      = TSucc (eval' e)
eval' (TPred e)      = case eval' e of
                            TZero     => TZero
                            TSucc ev' => ev'
eval' (TIfz e1 e2 e3) = case eval' e1 of
                             TZero   => eval' e2
                             TSucc _ => eval' e3

-- End: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS
--------------------------------------------------------

--------------------------------------------------------
-- Begin: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS

evalBigStep : (e : Term 0) -> (e' : Term 0 ** (Value e', BigStep e e'))
evalBigStep (TVar i)     = absurd $ FinZAbsurd i
evalBigStep (TAbs x)     = (TAbs x ** (VAbs, BStValue VAbs))
evalBigStep (TApp x y)   = let (TAbs ex ** (_, bStx)) = evalBigStep x
                               (ey ** (vy, bSty))     = evalBigStep y
                               (er ** (vr, bStr))     = evalBigStep (subst ey FZ ex)
                           in (er ** (vr, BStApp bStx bSty bStr))
evalBigStep TZero        = (TZero ** (VZero, BStValue VZero))
evalBigStep (TSucc x)    = let (ex ** (vx, bStx)) = evalBigStep x
                           in (TSucc ex ** (VSucc vx, BStSucc bStx))
evalBigStep (TPred x)    = case evalBigStep x of
   (TZero    ** (_, bStx))        => (TZero ** (VZero, BStPredZero bStx))
   (TSucc ex ** (VSucc vx, bStx)) => (ex    ** (vx,    BStPredSucc bStx))
evalBigStep (TIfz x y z) = case evalBigStep x of
   (TZero    ** (_, bStx)) => let (ey ** (vy, bSty)) = evalBigStep y
                              in (ey ** (vy, BStIfzZero bStx bSty))
   (TSucc ex ** (_, bStx)) => let (ez ** (vz, bStz)) = evalBigStep z
                              in (ez ** (vz, BStIfzSucc bStx bStz))

-- End: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS
------------------------------------------------------

-----------------------------------
-- Begin: EQUIVALENCE OF EVALUATORS

total equivEval : (eval e1) = (e2 ** (v2, tst2)) ->
                  (evalBigStep e1) = (e3 ** (v3, bSt3)) ->
                  e2 = e3
equivEval {v2 = v2} {tst2 = tst2} {bSt3 = bSt3} _ _ =
  let (tst3, v3) = bigStepToTransStep bSt3
  in transStepDeterministic v2 tst2 v3 tst3

-- End: EQUIVALENCE OF EVALUATORS
---------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Text.Markup.Edda.Org

import public Text.Markup.Edda.Model
import public Text.Markup.Edda.Walk
import public Text.Markup.Edda.Query

import public Text.Markup.Edda.Reader.Org
import public Text.Markup.Edda.Writer.Org

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Quantities.SIBaseQuantities

import Quantities.Core

%default total
%access public export

Length : Dimension
Length = MkDimension "Length"

Mass : Dimension
Mass = MkDimension "Mass"

Time : Dimension
Time = MkDimension "Time"

ElectricCurrent : Dimension
ElectricCurrent = MkDimension "ElectricCurrent"

-- Thermodynamic temperature
Temperature : Dimension
Temperature = MkDimension "Temperature"

AmountOfSubstance : Dimension
AmountOfSubstance = MkDimension "AmountOfSubstance"

LuminousIntensity : Dimension
LuminousIntensity = MkDimension "LuminousIntensity"

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module Toolkit.Text.Parser.Location

import Text.Lexer
import Text.Parser

import Toolkit.Data.Nat
import Toolkit.Data.Location
import Toolkit.Text.Parser.Support

%default total

namespace Toolkit
  export
  location : RuleEmpty state tok Location
  location = do
    (x,y) <- Text.Parser.location
    pure (MkLoc Nothing (toNat x) (toNat y))

  namespace WithFileName
    export
    location : String -> RuleEmpty state tok Location
    location fname = do
      l <- Toolkit.location
      pure (record { source = Just fname} l)

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Data.Either.Extras

%default total
%access export

toEither : (input : Bool) -> (left : Lazy l) -> (right : Lazy r) -> Either l r
toEither False left _ = Left left
toEither True _ right = Right right

|||Maps func over l if input is Left l.
mapLeft : (func : Lazy (l -> l')) -> (input : Either l r) -> Either l' r
mapLeft func (Left l) = Left $ func l
mapLeft _ (Right r) = Right r

|||Maps either funcl or funcr over input.
mapEither : (funcl : Lazy (l -> l')) -> (funcr : Lazy (r -> r')) -> (input : Either l r) -> Either l' r'
mapEither funcl _ (Left l) = Left $ funcl l
mapEither _ funcr (Right r) = Right $ funcr r

max_stars_repo_name: jheiling/idris-extras

max_issues_repo_name: jheiling/idris-extras

max_forks_repo_name: jheiling/idris-extras


text:
filterFizzBuzz' : List Int -> List Int -> List Int
filterFizzBuzz' aux xxs with (id xxs)
  filterFizzBuzz' aux@_     _ | [] = aux
  filterFizzBuzz' aux@_ xxs@_ | (x::xs) =
    if (x `mod` 3 == 0) || (x `mod` 5 == 0)
      then x :: (filterFizzBuzz' aux xxs | xs)
      else       filterFizzBuzz' aux xxs | xs

filterFizzBuzz : List Int -> List Int
filterFizzBuzz = filterFizzBuzz' []

main : IO ()
main = putStrLn . show $ filterFizzBuzz [1..20]

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
record Pack (a : Type) where
  constructor MkPack
  nested : a
  nat : Nat

proj : List (Pack Bool) -> List (Bool, Nat)
proj []        = []
proj (x :: xs) = MkPair x.nested (nat x) :: proj xs

ununpack : List (Pack (Pack a)) -> List a
ununpack = map (.nested.nested)

deepNats : List (Pack (Pack a)) -> List Nat
deepNats = map ((.nat) . (.nested))


text:
printLength : IO ()
printLength = do putStr "Input string: "
                 input <- getLine
                 let len = length input
                 putStrLn (show len)

printTwoThings : IO ()
printTwoThings = do putStrLn "Hello"
                    putStrLn "World"

printInput : IO ()
printInput = do x <- getLine
                putStrln x


text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#global-types
module WebAssembly.Validation.Types.GlobalTypes

import WebAssembly.Structure

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

public export
data ValidGlobalType : GlobalType -> Type where
  MkGlobalValidType : (globalType: GlobalType) -> ValidGlobalType globalType

-------------------------------------------------------------------------------
-- Decidablity of Validation
-------------------------------------------------------------------------------

total public export
isGlobalTypeValid : (globalType : GlobalType) -> Dec (ValidGlobalType globalType)
isGlobalTypeValid globalType = Yes (MkGlobalValidType globalType)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Web.Raw.Fetch

import JS
import Web.Internal.FetchPrim
import Web.Internal.Types

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

namespace Headers

  export
  new :  (init : Optional (NS I [ Array (Array ByteString)
                                , Record ByteString ByteString
                                ]))
      -> JSIO Headers
  new a = primJS $ Headers.prim__new (toFFI a)

  export
  new' : JSIO Headers
  new' = primJS $ Headers.prim__new undef

  export
  append :  (obj : Headers)
         -> (name : ByteString)
         -> (value : ByteString)
         -> JSIO ()
  append a b c = primJS $ Headers.prim__append a b c

  export
  delete : (obj : Headers) -> (name : ByteString) -> JSIO ()
  delete a b = primJS $ Headers.prim__delete a b

  export
  get : (obj : Headers) -> (name : ByteString) -> JSIO (Maybe ByteString)
  get a b = tryJS "Headers.get" $ Headers.prim__get a b

  export
  has : (obj : Headers) -> (name : ByteString) -> JSIO Bool
  has a b = tryJS "Headers.has" $ Headers.prim__has a b

  export
  set :  (obj : Headers)
      -> (name : ByteString)
      -> (value : ByteString)
      -> JSIO ()
  set a b c = primJS $ Headers.prim__set a b c

namespace Request

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem RequestInit (Types t1)}
      -> (input : NS I [ Request , String ])
      -> (init : Optional t1)
      -> JSIO Request
  new a b = primJS $ Request.prim__new (toFFI a) (optUp b)

  export
  new' : (input : NS I [ Request , String ]) -> JSIO Request
  new' a = primJS $ Request.prim__new (toFFI a) undef

  export
  cache : (obj : Request) -> JSIO RequestCache
  cache a = tryJS "Request.cache" $ Request.prim__cache a

  export
  credentials : (obj : Request) -> JSIO RequestCredentials
  credentials a = tryJS "Request.credentials" $ Request.prim__credentials a

  export
  destination : (obj : Request) -> JSIO RequestDestination
  destination a = tryJS "Request.destination" $ Request.prim__destination a

  export
  headers : (obj : Request) -> JSIO Headers
  headers a = primJS $ Request.prim__headers a

  export
  integrity : (obj : Request) -> JSIO String
  integrity a = primJS $ Request.prim__integrity a

  export
  isHistoryNavigation : (obj : Request) -> JSIO Bool
  isHistoryNavigation a = tryJS "Request.isHistoryNavigation"
                        $ Request.prim__isHistoryNavigation a

  export
  isReloadNavigation : (obj : Request) -> JSIO Bool
  isReloadNavigation a = tryJS "Request.isReloadNavigation"
                       $ Request.prim__isReloadNavigation a

  export
  keepalive : (obj : Request) -> JSIO Bool
  keepalive a = tryJS "Request.keepalive" $ Request.prim__keepalive a

  export
  method : (obj : Request) -> JSIO ByteString
  method a = primJS $ Request.prim__method a

  export
  mode : (obj : Request) -> JSIO RequestMode
  mode a = tryJS "Request.mode" $ Request.prim__mode a

  export
  redirect : (obj : Request) -> JSIO RequestRedirect
  redirect a = tryJS "Request.redirect" $ Request.prim__redirect a

  export
  referrer : (obj : Request) -> JSIO String
  referrer a = primJS $ Request.prim__referrer a

  export
  referrerPolicy : (obj : Request) -> JSIO ReferrerPolicy
  referrerPolicy a = tryJS "Request.referrerPolicy"
                   $ Request.prim__referrerPolicy a

  export
  signal : (obj : Request) -> JSIO AbortSignal
  signal a = primJS $ Request.prim__signal a

  export
  url : (obj : Request) -> JSIO String
  url a = primJS $ Request.prim__url a

  export
  clone : (obj : Request) -> JSIO Request
  clone a = primJS $ Request.prim__clone a

namespace Response

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem ResponseInit (Types t1)}
      -> (body : Optional (Maybe (NS I [ ReadableStream
                                       , Blob
                                       , Int8Array
                                       , Int16Array
                                       , Int32Array
                                       , UInt8Array
                                       , UInt8Array
                                       , UInt8Array
                                       , UInt8ClampedArray
                                       , Float32Array
                                       , Float64Array
                                       , DataView
                                       , ArrayBuffer
                                       , FormData
                                       , URLSearchParams
                                       , String
                                       ])))
      -> (init : Optional t1)
      -> JSIO Response
  new a b = primJS $ Response.prim__new (toFFI a) (optUp b)

  export
  new' : JSIO Response
  new' = primJS $ Response.prim__new undef undef

  export
  error : JSIO Response
  error = primJS $ Response.prim__error

  export
  redirect : (url : String) -> (status : Optional Bits16) -> JSIO Response
  redirect a b = primJS $ Response.prim__redirect a (toFFI b)

  export
  redirect' : (url : String) -> JSIO Response
  redirect' a = primJS $ Response.prim__redirect a undef

  export
  headers : (obj : Response) -> JSIO Headers
  headers a = primJS $ Response.prim__headers a

  export
  ok : (obj : Response) -> JSIO Bool
  ok a = tryJS "Response.ok" $ Response.prim__ok a

  export
  redirected : (obj : Response) -> JSIO Bool
  redirected a = tryJS "Response.redirected" $ Response.prim__redirected a

  export
  status : (obj : Response) -> JSIO Bits16
  status a = primJS $ Response.prim__status a

  export
  statusText : (obj : Response) -> JSIO ByteString
  statusText a = primJS $ Response.prim__statusText a

  export
  type : (obj : Response) -> JSIO ResponseType
  type a = tryJS "Response.type" $ Response.prim__type a

  export
  url : (obj : Response) -> JSIO String
  url a = primJS $ Response.prim__url a

  export
  clone : (obj : Response) -> JSIO Response
  clone a = primJS $ Response.prim__clone a

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

namespace Body

  export
  body :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Body (Types t1)}
       -> (obj : t1)
       -> JSIO (Maybe ReadableStream)
  body a = tryJS "Body.body" $ Body.prim__body (up a)

  export
  bodyUsed :  (0 _ : JSType t1)
           => {auto 0 _ : Elem Body (Types t1)}
           -> (obj : t1)
           -> JSIO Bool
  bodyUsed a = tryJS "Body.bodyUsed" $ Body.prim__bodyUsed (up a)

  export
  arrayBuffer :  (0 _ : JSType t1)
              => {auto 0 _ : Elem Body (Types t1)}
              -> (obj : t1)
              -> JSIO (Promise ArrayBuffer)
  arrayBuffer a = primJS $ Body.prim__arrayBuffer (up a)

  export
  blob :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Body (Types t1)}
       -> (obj : t1)
       -> JSIO (Promise Blob)
  blob a = primJS $ Body.prim__blob (up a)

  export
  formData :  (0 _ : JSType t1)
           => {auto 0 _ : Elem Body (Types t1)}
           -> (obj : t1)
           -> JSIO (Promise FormData)
  formData a = primJS $ Body.prim__formData (up a)

  export
  json :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Body (Types t1)}
       -> (obj : t1)
       -> JSIO (Promise AnyPtr)
  json a = primJS $ Body.prim__json (up a)

  export
  text :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Body (Types t1)}
       -> (obj : t1)
       -> JSIO (Promise String)
  text a = primJS $ Body.prim__text (up a)

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

namespace RequestInit

  export
  new :  (method : Optional ByteString)
      -> (headers : Optional (NS I [ Array (Array ByteString)
                                   , Record ByteString ByteString
                                   ]))
      -> (body : Optional (Maybe (NS I [ ReadableStream
                                       , Blob
                                       , Int8Array
                                       , Int16Array
                                       , Int32Array
                                       , UInt8Array
                                       , UInt8Array
                                       , UInt8Array
                                       , UInt8ClampedArray
                                       , Float32Array
                                       , Float64Array
                                       , DataView
                                       , ArrayBuffer
                                       , FormData
                                       , URLSearchParams
                                       , String
                                       ])))
      -> (referrer : Optional String)
      -> (referrerPolicy : Optional ReferrerPolicy)
      -> (mode : Optional RequestMode)
      -> (credentials : Optional RequestCredentials)
      -> (cache : Optional RequestCache)
      -> (redirect : Optional RequestRedirect)
      -> (integrity : Optional String)
      -> (keepalive : Optional Bool)
      -> (signal : Optional (Maybe AbortSignal))
      -> (window : Optional Any)
      -> JSIO RequestInit
  new a b c d e f g h i j k l m = primJS
                                $ RequestInit.prim__new (toFFI a)
                                                        (toFFI b)
                                                        (toFFI c)
                                                        (toFFI d)
                                                        (toFFI e)
                                                        (toFFI f)
                                                        (toFFI g)
                                                        (toFFI h)
                                                        (toFFI i)
                                                        (toFFI j)
                                                        (toFFI k)
                                                        (toFFI l)
                                                        (toFFI m)

  export
  new' : JSIO RequestInit
  new' = primJS
       $ RequestInit.prim__new undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef
                               undef

  export
  body :  (0 _ : JSType t)
       => {auto 0 _ : Elem RequestInit (Types t)}
       -> t
       -> Attribute False Optional (Maybe (Union16 ReadableStream
                                                   Blob
                                                   Int8Array
                                                   Int16Array
                                                   Int32Array
                                                   UInt8Array
                                                   UInt8Array
                                                   UInt8Array
                                                   UInt8ClampedArray
                                                   Float32Array
                                                   Float64Array
                                                   DataView
                                                   ArrayBuffer
                                                   FormData
                                                   URLSearchParams
                                                   String))
  body v = fromUndefOrPrimNoDefault "RequestInit.getbody"
                                    prim__body
                                    prim__setBody
                                    (v :> RequestInit)

  export
  cache :  (0 _ : JSType t)
        => {auto 0 _ : Elem RequestInit (Types t)}
        -> t
        -> Attribute False Optional RequestCache
  cache v = fromUndefOrPrimNoDefault "RequestInit.getcache"
                                     prim__cache
                                     prim__setCache
                                     (v :> RequestInit)

  export
  credentials :  (0 _ : JSType t)
              => {auto 0 _ : Elem RequestInit (Types t)}
              -> t
              -> Attribute False Optional RequestCredentials
  credentials v = fromUndefOrPrimNoDefault "RequestInit.getcredentials"
                                           prim__credentials
                                           prim__setCredentials
                                           (v :> RequestInit)

  export
  headers :  (0 _ : JSType t)
          => {auto 0 _ : Elem RequestInit (Types t)}
          -> t
          -> Attribute False Optional (Union2 (Array (Array ByteString))
                                              (Record ByteString ByteString))
  headers v = fromUndefOrPrimNoDefault "RequestInit.getheaders"
                                       prim__headers
                                       prim__setHeaders
                                       (v :> RequestInit)

  export
  integrity :  (0 _ : JSType t)
            => {auto 0 _ : Elem RequestInit (Types t)}
            -> t
            -> Attribute False Optional String
  integrity v = fromUndefOrPrimNoDefault "RequestInit.getintegrity"
                                         prim__integrity
                                         prim__setIntegrity
                                         (v :> RequestInit)

  export
  keepalive :  (0 _ : JSType t)
            => {auto 0 _ : Elem RequestInit (Types t)}
            -> t
            -> Attribute False Optional Bool
  keepalive v = fromUndefOrPrimNoDefault "RequestInit.getkeepalive"
                                         prim__keepalive
                                         prim__setKeepalive
                                         (v :> RequestInit)

  export
  method :  (0 _ : JSType t)
         => {auto 0 _ : Elem RequestInit (Types t)}
         -> t
         -> Attribute False Optional ByteString
  method v = fromUndefOrPrimNoDefault "RequestInit.getmethod"
                                      prim__method
                                      prim__setMethod
                                      (v :> RequestInit)

  export
  mode :  (0 _ : JSType t)
       => {auto 0 _ : Elem RequestInit (Types t)}
       -> t
       -> Attribute False Optional RequestMode
  mode v = fromUndefOrPrimNoDefault "RequestInit.getmode"
                                    prim__mode
                                    prim__setMode
                                    (v :> RequestInit)

  export
  redirect :  (0 _ : JSType t)
           => {auto 0 _ : Elem RequestInit (Types t)}
           -> t
           -> Attribute False Optional RequestRedirect
  redirect v = fromUndefOrPrimNoDefault "RequestInit.getredirect"
                                        prim__redirect
                                        prim__setRedirect
                                        (v :> RequestInit)

  export
  referrer :  (0 _ : JSType t)
           => {auto 0 _ : Elem RequestInit (Types t)}
           -> t
           -> Attribute False Optional String
  referrer v = fromUndefOrPrimNoDefault "RequestInit.getreferrer"
                                        prim__referrer
                                        prim__setReferrer
                                        (v :> RequestInit)

  export
  referrerPolicy :  (0 _ : JSType t)
                 => {auto 0 _ : Elem RequestInit (Types t)}
                 -> t
                 -> Attribute False Optional ReferrerPolicy
  referrerPolicy v = fromUndefOrPrimNoDefault "RequestInit.getreferrerPolicy"
                                              prim__referrerPolicy
                                              prim__setReferrerPolicy
                                              (v :> RequestInit)

  export
  signal :  (0 _ : JSType t)
         => {auto 0 _ : Elem RequestInit (Types t)}
         -> t
         -> Attribute False Optional (Maybe AbortSignal)
  signal v = fromUndefOrPrimNoDefault "RequestInit.getsignal"
                                      prim__signal
                                      prim__setSignal
                                      (v :> RequestInit)

  export
  window :  (0 _ : JSType t)
         => {auto 0 _ : Elem RequestInit (Types t)}
         -> t
         -> Attribute False Optional Any
  window v = fromUndefOrPrimNoDefault "RequestInit.getwindow"
                                      prim__window
                                      prim__setWindow
                                      (v :> RequestInit)

namespace ResponseInit

  export
  new :  (status : Optional Bits16)
      -> (statusText : Optional ByteString)
      -> (headers : Optional (NS I [ Array (Array ByteString)
                                   , Record ByteString ByteString
                                   ]))
      -> JSIO ResponseInit
  new a b c = primJS $ ResponseInit.prim__new (toFFI a) (toFFI b) (toFFI c)

  export
  new' : JSIO ResponseInit
  new' = primJS $ ResponseInit.prim__new undef undef undef

  export
  headers :  (0 _ : JSType t)
          => {auto 0 _ : Elem ResponseInit (Types t)}
          -> t
          -> Attribute False Optional (Union2 (Array (Array ByteString))
                                              (Record ByteString ByteString))
  headers v = fromUndefOrPrimNoDefault "ResponseInit.getheaders"
                                       prim__headers
                                       prim__setHeaders
                                       (v :> ResponseInit)

  export
  status :  (0 _ : JSType t)
         => {auto 0 _ : Elem ResponseInit (Types t)}
         -> t
         -> Attribute True Optional Bits16
  status v = fromUndefOrPrim "ResponseInit.getstatus"
                             prim__status
                             prim__setStatus
                             200
                             (v :> ResponseInit)

  export
  statusText :  (0 _ : JSType t)
             => {auto 0 _ : Elem ResponseInit (Types t)}
             -> t
             -> Attribute False Optional ByteString
  statusText v = fromUndefOrPrimNoDefault "ResponseInit.getstatusText"
                                          prim__statusText
                                          prim__setStatusText
                                          (v :> ResponseInit)


text:
module Main

import System

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Kaboom"
countdown secs@(S k) = do putStrLn $ show secs
                          usleep 1000000
                          countdown k


text:
module Main

import Data.List
import Data.Strings
import System
import System.File

import Sat
import Data.DIMACS

main : IO ()
main = do
  (_::fname::_) <- getArgs
  | _ => putStrLn $ "missing input filename"
  (Right cnfText) <- readFile fname
  | Left readErr => putStrLn $ "error reading input file: " ++ show readErr
  case parseDIMACS cnfText of
       Right problem => do
         --printLn problem
         case sat problem.numVars problem.clauses of
              Nothing => putStrLn "unsat"
              Just assignment => do putStrLn "sat"
                                    putStrLn $ unwords $ map showDIMACS assignment
       Left error => putStrLn $ "parsing error: " ++ error


text:
module Postgres.Query

import public Language.JSON
import public Data.Vect.Quantifiers
import public Postgres.Data.PostgresValue
import public Data.HVect

import Postgres.Utility
import Postgres.Data.Conn
import Postgres.Data.PostgresType
import Postgres.Exec
import Postgres.Result
import Decidable.Equality
import Data.Fin
import Data.Vect
import Data.Either

%default total

||| Get the first row first column from the given
||| result. Will return `Nothing` if there are no
||| results.
maybeFirstRowCol : {r,c : Nat} -> TupleResult r c -> Maybe String
maybeFirstRowCol res = do row <- natToFin 0 r
                          col <- natToFin 0 c
                          pure $ pgResultStringValue res row col

--
-- Headers
--

headerNames : {colCount : Nat} -> TupleResult _ colCount -> Vect colCount String
headerNames t = pgResultsetColNames t

headerTypes : {auto types : TypeDictionary}
           -> {colCount : Nat}
           -> TupleResult _ colCount
           -> Vect colCount PType
headerTypes t = pgResultsetColTypes t

headers : {auto types : TypeDictionary}
       -> {colCount : Nat}
       -> TupleResult _ colCount
       -> Vect colCount ColHeader
headers t = (uncurry MkHeader) <$> (zip (headerNames t) (headerTypes t))

--
-- Stringy (unityped) Results
--

rows : {rowCount, colCount : Nat} -> TupleResult rowCount colCount -> Vect rowCount (Vect colCount (Maybe String))
rows t = (map force) <$> pgNullableStringResultset t

export
pgStringResultsQuery : {auto types : TypeDictionary}
                    -> (header : Bool)
                    -> (query : String)
                    -> Conn
                    -> IO (Either String (StringResultset header))
pgStringResultsQuery header query conn = withExecResult conn query stringResults
  where
    stringResults : Result -> IO (Either String (StringResultset header))
    stringResults r = do Nothing <- pure $ pgResultErrorMessage r
                           | Just err => pure $ Left err
                         Just tuples <- pure $ tupleResult r
                           | Nothing  => pure $ Left "query did not result in expected response."
                         pure $ Right $ if header
                                        then (_ ** _ ** (headers tuples, rows tuples))
                                        else (_ ** _ ** rows tuples)

--
-- JSON Results
--

||| Get the result as JSON if it is 1 row and column that can
||| be successfully parsed as JSON.
export
pgJSONResultQuery : (query: String) -> Conn -> IO (Maybe JSON)
pgJSONResultQuery query conn = withExecResult conn query toJson where
 toJson : Result -> IO (Maybe JSON)
 toJson r = pure $ [ json | json <- parse !(maybeFirstRowCol !(tupleResult r)) ]

--
-- Expected Type Results
--

-- Here you pass the vect of types you expect and get back results if possible.

processValue : Castable expected
            -> Maybe String
            -> Either String expected
processValue hasDefault = (asDefaultType hasDefault)

processCols : {0 expected : Vect colCount Type}
           -> All Castable expected
           -> Vect colCount (Maybe String)
           -> Either String (HVect expected)
processCols [] [] = Right []
processCols (castable :: castables) (x :: xs) =
  [| (processValue castable x) :: (processCols castables xs) |]

processRows : {0 expected : Vect colCount Type}
           -> {auto castable : (All Castable expected)}
           -> Vect rowCount (Vect colCount (Maybe String))
           -> Either String (Vect rowCount (HVect expected))
processRows xs = traverse (processCols castable) xs

||| Get the result as a rows of the expected types of values if possible.
export
pgResultQuery : {auto types : TypeDictionary}
             -> {colCount : Nat}
             -> (expected : Vect colCount Type)
             -> (query : String)
             -> Conn
             -> {auto castable : (All Castable expected)}
             -> IO (Either String (rowCount ** Vect rowCount (HVect expected)))
pgResultQuery expected query conn =
  do Right (rowCount ** receivedCols ** strings) <- pgStringResultsQuery False query conn
       | Left err => pure $ Left err
     pure $
       case decEq colCount receivedCols of
            (No _) =>
              Left $ columnMismatchError receivedCols
            (Yes correctCols) =>
              (MkDPair rowCount) <$> processRows (rewrite correctCols in strings)
    where
      columnMismatchError : (received : Nat) -> String
      columnMismatchError received =
        "Wrong number of columns returned. Expected " ++ (show colCount) ++ " but got " ++ (show received)

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
import DoorJam
import ATM
import Hangman


text:
import Js.Utils

%lib Node "tst/st"

main : JS_IO ()
main = putStr' "ola"

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Idris.Codegen.ExtSTG.Erased

import Core.Core
import Core.Context
import Compiler.ANF
import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.STG

ERASED_TYPE_NAME : String
ERASED_TYPE_NAME = "Erased"

ERASED_CON_NAME : String
ERASED_CON_NAME = "Erased"

export
ERASED_TOPLEVEL_NAME : String
ERASED_TOPLEVEL_NAME = "idrisErasedValue"

export
defineErasedADT
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Core ()
defineErasedADT = do
  d <- createSTyCon
        (ERASED_TYPE_NAME, SsUnhelpfulSpan ERASED_TYPE_NAME)
        [ (ERASED_CON_NAME, AlgDataCon [], SsUnhelpfulSpan ERASED_CON_NAME)]
  defineDataType (MkUnitId MAIN_UNIT) (MkModuleName MAIN_MODULE) d

export
erasedTopBinding
  :  UniqueMapRef
  => Ref Counter Int
  => DataTypeMapRef
  => Core TopBinding
erasedTopBinding = do
  dtc <- mkDataConIdStr ERASED_CON_NAME
  rhs <- pure $ StgRhsCon dtc []
  erasedNameBinder <- mkSBinderStr emptyFC ERASED_TOPLEVEL_NAME
  binding <- pure $ StgNonRec erasedNameBinder rhs
  pure $ StgTopLifted binding

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen