text:
module Main

import Conway.Conway
import Conway.Graphics
import Conway.RLE

import Effect.File

import Data.Vect

showCW : Conway m n -> String
showCW (MkConway v) = concat $ map (\row => showRow row ++ "\n") v
  where showRow : Vect n CellState -> String
        showRow v = concat $ map (\cs => case cs of
                            Alive => ". "
                            Dead  => "  "
                        ) v

loop : Conway m n -> IO ()
loop cw = do
       putStrLn $ showCW cw
       getLine
       loop $ iterateGame cw

maxLength : List (List a) -> Nat
maxLength xs = maxLength' 0 xs
  where maxLength' : Nat -> List (List a) -> Nat
        maxLength' n [] = n
        maxLength' n (x::xs) = maxLength' (max n (length x)) xs

repeatN : (n : Nat) -> a -> Vect n a
repeatN Z _ = []
repeatN (S n) a = (a::(repeatN n a))

lToV : (n : Nat) -> List (List CellState) -> List (Vect n CellState)
lToV n [] = []
lToV n ys = map (\x => f n x) ys
  where f : (n : Nat) -> List CellState -> Vect n CellState
        f Z _ = []
        f (S n) [] = (Dead::(f n []))
        f (S n) (y::ys) = (y::(f n ys))

main : IO ()
main = do
  args <- getArgs
  let fNameM = index' 1 args
  case fNameM of
    Nothing => print "Usage ./Conway 'filename'"
    Just fName => do
        cwM <- readCFile fName
        case cwM of
          Nothing => print "Error in converting file contents\n"
          Just cw => do
            let lVec = lToV (maxLength cw) cw
            let vec = fromList lVec
            let conway = MkConway vec
            conwayLoop conway

 {-
  conwayLoop cw
  where
      row1 : Vect 4 CellState
      row1 = fromList [Dead, Alive, Dead, Dead]

      row2 : Vect 4 CellState
      row2 = fromList [Dead, Alive, Dead, Dead]

      row3 : Vect 4 CellState
      row3 = fromList [Dead, Alive, Dead, Dead]

      row4 : Vect 4 CellState
      row4 = fromList [Dead, Dead, Dead, Dead]

      v : Vect 4 (Vect 4 CellState)
      v = fromList [row1, row2, row3, row4]

      cw : Conway 4 4
      cw = MkConway v
  -}

max_stars_repo_name: RossMeikleham/Idris-Conway

max_issues_repo_name: RossMeikleham/Idris-Conway

max_forks_repo_name: RossMeikleham/Idris-Conway


text:
module Effect.File

import Effects
import Control.IOExcept

data OpenFile : Mode -> Type where
     FH : File -> OpenFile m

openOK : Mode -> Bool -> Type
openOK m True = OpenFile m
openOK m False = ()

data FileIO : Effect where
     Open  : String -> (m : Mode) ->
             {() ==> if result then OpenFile m else ()} FileIO Bool
     Close : {OpenFile m ==> ()}               FileIO ()

     ReadLine  :           {OpenFile Read}  FileIO String
     WriteLine : String -> {OpenFile Write} FileIO ()
     EOF       :           {OpenFile Read}  FileIO Bool

instance Handler FileIO IO where
    handle () (Open fname m) k = do h <- openFile fname m
                                    valid <- validFile h
                                    if valid then k True (FH h)
                                             else k False ()
    handle (FH h) Close      k = do closeFile h
                                    k () ()
    handle (FH h) ReadLine        k = do str <- fread h
                                         k str (FH h)
    handle (FH h) (WriteLine str) k = do fwrite h str
                                         k () (FH h)
    handle (FH h) EOF             k = do e <- feof h
                                         k e (FH h)

FILE_IO : Type -> EFFECT
FILE_IO t = MkEff t FileIO

open : Handler FileIO e =>
       String -> (m : Mode) ->
       { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool
open f m = Open f m

close : Handler FileIO e =>
        { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()
close = Close

readLine : Handler FileIO e =>
           { [FILE_IO (OpenFile Read)] } Eff e String
readLine = ReadLine

writeLine : Handler FileIO e =>
            String -> { [FILE_IO (OpenFile Write)] } Eff e ()
writeLine str = WriteLine str

eof : Handler FileIO e =>
      { [FILE_IO (OpenFile Read)] } Eff e Bool
eof = EOF

ext: idr

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
||| Tail-call optimization.
|||
||| Here is a lengthy explanation how this works at the
||| moment. Assume the following call graph of functions f1,f2,f3,f4 all
||| calling each other in tail call position:
|||
||| ```
|||       ------------ f2 ---- f4 (result)
|||      /          /     \
||| f1 ---- f1     /       -- f1
|||      \        /
|||       -- f3 --
||| ```
|||
||| First, a directed graph of all toplevel function calls
||| (incoming and outgoing) in tail-call position is created:
|||
||| ```idris
||| MkCallGraph $ fromList [(f1,[f1,f2,f3]),(f2,[f1,f4]),(f3,[f2])]
|||             $ fromList [(f1,[f1,f2]),(f2,[f1,f3]),(f3,[f1]),(f4,[f2])]
||| ```
|||
||| Mutually tail-recursive functions form a strongly connected
||| component in such a call graph: There is a (directed) path from every function
||| to every other function. Tarjan's algorithm is used to identify
||| these strongly connected components and grouping them in
||| a `List` of `List1`s.
|||
||| A tail-recursive group of functions is now converted to an imperative
||| loop as follows: Let `obj={h:_, a1:_, a2:_, ...}`
||| be a Javascript object consisting
||| of a tag `h` and arguments `a1`,`a2`,... . `h` indicates, whether `obj.a1`
||| contains the result of the computation (`h = 0`) or describes
||| a continuation indicating the next function to be invoked, in which
||| case fields `a1`,`a2`,... are the function's arguments.
||| together with the necessary arguments. The group of mutually
||| recursive functions is now converted to a single switch statement
||| where each branch corresponds to one of the function.
||| Each function will be changed in such a way that instead of
||| (recursively) calling another function in its group it will return
||| a new object `{h:_, a1:_, ...}` with `h` indicating the next
||| function to call (the next branch to choose in the `switch`
||| statement and `a1`,`a2`,... being the next function's set of
||| arguments. The function and initial argument object will then
||| be passed to toplevel function `__tailRec`, which loops
||| until the object signals that we have arrived at a result.
|||
||| Here is an example of two mutually tail-recursive functions
||| together with the generated tail-call optimized code.
|||
||| Original version:
|||
||| ```javascript
||| function isEven(arg){
|||   switch (arg) {
|||     case 0  : return 1;
|||     default : return isOdd(arg - 1);
|||   }
||| }
|||
||| function isOdd(arg){
|||   switch (arg) {
|||     case 0  : return 0;
|||     default : return isEven(arg - 1);
|||   }
||| }
||| ```
|||
||| The above gets converted to code similar to
||| the following.
|||
||| ```javascript
||| function tcOpt(arg) {
|||   switch(arg.h) {
|||   // former function isEven
|||   case 1: {
|||     switch (arg.a1) {
|||       case 0  : return {h: 0, a1: 1};
|||       default : return {h: 2, a1: arg.a1 - 1};
|||     }
|||   }
|||   // former function isOdd
|||   case 2: {
|||     switch (a1) {
|||       case 0  : return {h: 0, a1: 0};
|||       default : return {h: 1, a1: arg.a1 - 1};
|||     }
|||   }
||| }
|||
||| function isEven(arg){
|||   return __tailRec(tcOpt,{h: 1, a1: arg})
||| }
|||
||| function isOdd(arg){
|||   return __tailRec(tcOpt,{h: 2, a1: arg})
||| }
||| ```
|||
||| Finally, `__tailRec` is implemented as follows:
|||
||| ```javascript
|||   function __tailRec(f,ini) {
|||     let obj = ini;
|||     while(true){
|||       switch(obj.h){
|||         case 0: return obj.a1;
|||         default: obj = f(obj);
|||       }
|||     }
|||   }
||| ```
|||
||| While the above example is in Javascript, this module operates
||| on `NamedCExp` exclusively, so it might be used with any backend
||| where the things described above can be expressed.
module Compiler.ES.TailRec

import Data.Maybe
import Data.List
import Data.List1
import Data.String
import Libraries.Data.Graph
import Libraries.Data.SortedSet
import Libraries.Data.List.Extra as L
import Libraries.Data.SortedMap as M
import Core.Name
import Core.CompileExpr
import Core.Context

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

-- indices of a list starting at 1
indices : List a -> List Int
indices as = [1 .. cast (length as)]

zipWithIndices : List a -> List (Int,a)
zipWithIndices as = zip (indices as) as

--------------------------------------------------------------------------------
--          Tailcall Graph
--------------------------------------------------------------------------------

||| A (toplevel) function in a group of mutually tail recursive functions.
public export
record TcFunction where
  constructor MkTcFunction
  ||| Function's name
  name  : Name

  ||| Function's index in its tail call group
  ||| This is used to decide on which branch to choose in
  ||| the next iteration
  index : Int

  ||| Argument list
  args  : List Name

  ||| Function's definition
  exp   : NamedCExp

||| A group of mutually tail recursive toplevel functions.
public export
record TcGroup where
  constructor MkTcGroup
  ||| Index of the group. This is used to generate a uniquely
  ||| named tail call optimized toplevel function.
  index     : Int

  ||| Set of mutually recursive functions.
  functions : SortedMap Name TcFunction

-- tail calls made from an expression
tailCalls : NamedCExp -> SortedSet Name
tailCalls (NmLet _ _ _ z) = tailCalls z
tailCalls (NmApp _ (NmRef _ x) _) = singleton x
tailCalls (NmConCase fc sc xs x) =
  concatMap (\(MkNConAlt _ _ _ _ x) => tailCalls x) xs <+>
  concatMap tailCalls x
tailCalls (NmConstCase fc sc xs x) =
  concatMap (\(MkNConstAlt _ x) => tailCalls x) xs <+>
  concatMap tailCalls x
tailCalls _ = empty

-- Checks if a `List1` of functions actually has any tail recursive
-- function calls and needs to be optimized.
-- In case of a larger group (more than one element)
-- the group contains tailcalls by construction. In case
-- of a single function, we need to check that at least one
-- outgoing tailcall goes back to the function itself.
-- We use the given mapping from `Name` to set of names
-- called in tail position to verify this.
hasTailCalls : SortedMap Name (SortedSet Name) -> List1 Name -> Bool
hasTailCalls g (x ::: Nil) = maybe False (contains x) $ lookup x g
hasTailCalls _ _           = True

-- Given a strongly connected group of functions, plus
-- a unique index, convert them to a list of
-- consisting of the function names plus the `TcGroup`,
-- to which they belong.
toGroup :  SortedMap Name (Name,List Name,NamedCExp)
        -> (Int,List1 Name)
        -> List (Name,TcGroup)
toGroup funMap (groupIndex,functions) =
  let ns    = zipWithIndices $ forget functions
      group = MkTcGroup groupIndex . fromList $ mapMaybe fun ns
   in (,group) <$> forget functions
  where fun : (Int,Name) -> Maybe (Name,TcFunction)
        fun (fx, n) = do
          (_,args,exp) <- lookup n funMap
          pure (n,MkTcFunction n fx args exp)

-- Returns the connected components of the tail call graph
-- of a set of toplevel function definitions.
-- Every function name that is part of a tail-call group
-- (a set of mutually tail-recursive functions)
-- points to its corresponding group.
tailCallGroups :  List (Name,List Name,NamedCExp)
               -> SortedMap Name TcGroup
tailCallGroups funs =
  let funMap = M.fromList $ map (\t => (fst t,t)) funs
      graph  = map (\(_,_,x) => tailCalls x) funMap
      groups = filter (hasTailCalls graph) $ tarjan graph
   in fromList $ concatMap (toGroup funMap) (zipWithIndices groups)

--------------------------------------------------------------------------------
--          Converting tail call groups to expressions
--------------------------------------------------------------------------------

public export
record Function where
  constructor MkFunction
  name : Name
  args : List Name
  body : NamedCExp

tcFunction : Int -> Name
tcFunction = MN "$tcOpt"

tcArgName : Name
tcArgName = MN "$a" 0

tcContinueName : (groupIndex : Int) -> (functionIndex : Int) -> Name
tcContinueName gi fi = MN ("TcContinue" ++ show gi) fi

tcDoneName : (groupIndex : Int) -> Name
tcDoneName gi = MN "TcDone" gi

-- Converts a single function in a mutually tail-recursive
-- group of functions to a single branch in a pattern match.
-- Recursive function calls will be replaced with an
-- applied data constructor whose tag indicates the
-- branch in the pattern match to use next, and whose values
-- will be used as the arguments for the next function.
conAlt : TcGroup -> TcFunction -> NamedConAlt
conAlt (MkTcGroup tcIx funs) (MkTcFunction n ix args exp) =
  let name = tcContinueName tcIx ix
   in MkNConAlt name DATACON (Just ix) args (toTc exp)

   where mutual
     -- this is returned in case we arrived at a result
     -- (an expression not corresponding to a recursive
     -- call in tail position).
     tcDone : NamedCExp -> NamedCExp
     tcDone x = NmCon EmptyFC (tcDoneName tcIx) DATACON (Just 0) [x]

     -- this is returned in case we arrived at a resursive call
     -- in tail position. The index indicates the next "function"
     -- to call, the list of expressions are the function's
     -- arguments.
     tcContinue : (index : Int) -> List NamedCExp -> NamedCExp
     tcContinue ix = NmCon EmptyFC (tcContinueName tcIx ix) DATACON (Just ix)

     -- recursively converts an expression. Only the `NmApp` case is
     -- interesting, the rest is pretty much boiler plate.
     toTc : NamedCExp -> NamedCExp
     toTc (NmLet fc x y z) = NmLet fc x y $ toTc z
     toTc x@(NmApp _ (NmRef _ n) xs) =
       case lookup n funs of
         Just v  => tcContinue v.index xs
         Nothing => tcDone x
     toTc (NmConCase fc sc a d) = NmConCase fc sc (map con a) (map toTc d)
     toTc (NmConstCase fc sc a d) = NmConstCase fc sc (map const a) (map toTc d)
     toTc x@(NmCrash _ _) = x
     toTc x = tcDone x

     con : NamedConAlt -> NamedConAlt
     con (MkNConAlt x y tag xs z) = MkNConAlt x y tag xs (toTc z)

     const : NamedConstAlt -> NamedConstAlt
     const (MkNConstAlt x y) = MkNConstAlt x (toTc y)

-- Converts a group of mutually tail recursive functions
-- to a list of toplevel function declarations. `tailRecLoopName`
-- is the name of the toplevel function that does the
-- infinite looping (function `__tailRec` in the example at
-- the top of this module).
convertTcGroup : (tailRecLoopName : Name) -> TcGroup -> List Function
convertTcGroup loop g@(MkTcGroup gindex fs) =
  let functions = sortBy (comparing index) $ values fs
      branches  = map (conAlt g) functions
      switch    = NmConCase EmptyFC (local tcArgName) branches Nothing
   in MkFunction tcFun [tcArgName] switch :: map toFun functions

  where tcFun : Name
        tcFun = tcFunction gindex

        local : Name -> NamedCExp
        local = NmLocal EmptyFC

        toFun : TcFunction -> Function
        toFun (MkTcFunction n ix args x) =
          let exps  = map local args
              tcArg = NmCon EmptyFC (tcContinueName gindex ix)
                        DATACON (Just ix) exps
              tcFun = NmRef EmptyFC tcFun
              body  = NmApp EmptyFC (NmRef EmptyFC loop) [tcFun,tcArg]
           in MkFunction n args body

-- Tail recursion optimizations: Converts all groups of
-- mutually tail recursive functions to an imperative loop.
tailRecOptim :  SortedMap Name TcGroup
             -> (tcLoopName : Name)
             -> List (Name,List Name,NamedCExp)
             -> List Function
tailRecOptim groups loop ts =
  let regular = mapMaybe toFun ts
      tailOpt = concatMap (convertTcGroup loop) $ values groups
   in tailOpt ++ regular

  where toFun : (Name,List Name,NamedCExp) -> Maybe Function
        toFun (n,args,exp) = case lookup n groups of
          Just _  => Nothing
          Nothing => Just $ MkFunction n args exp

||| Converts a list of toplevel definitions (potentially
||| several groups of mutually tail-recursive functions)
||| to a new set of tail-call optimized function definitions.
||| `MkNmFun`s are converted. Other constructors of `NamedDef`
||| are ignored and silently dropped.
export
functions :  (tcLoopName : Name)
          -> List (Name,FC,NamedDef)
          -> List Function
functions loop dfs =
  let ts = mapMaybe def dfs
   in tailRecOptim (tailCallGroups ts) loop ts
   where def : (Name,FC,NamedDef) -> Maybe (Name,List Name,NamedCExp)
         def (n,_,MkNmFun args x) = Just (n,args,x)
         def _                    = Nothing


text:
-- a mini prelude

module Stuff

public export
data Bool = True | False

public export
not : Bool -> Bool
not True = False
not False = True

public export
data Maybe : Type -> Type where
     Nothing : Maybe a
     Just : (1 x : a) -> Maybe a

public export
data Either : Type -> Type -> Type where
     Left : (1 x : a) -> Either a b
     Right : (1 y : b) -> Either a b

public export
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True

public export
ifThenElse : Bool -> Lazy a -> Lazy a -> a
ifThenElse True t e = t
ifThenElse False t e = e

public export
data Nat : Type where
     Z : Nat
     S : (1 _ : Nat) -> Nat

public export
fromInteger : Integer -> Nat
fromInteger x = ifThenElse (intToBool (prim__eq_Integer x 0))
                      Z (S (fromInteger (prim__sub_Integer x 1)))

public export
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

infixr 5 ::

public export
data List : Type -> Type where
     Nil : List a
     (::) : (1 _ : a) -> (1 _ : List a) -> List a

public export
data Eq : a -> b -> Type where
     Refl : (x : a) -> Eq x x

public export
data Unit = MkUnit

public export
data Pair : Type -> Type -> Type where
     MkPair : {a, b : Type} -> a -> b -> Pair a b

public export
the : (a : Type) -> a -> a
the _ x = x


text:
module GRIN.Opts.UnusedVarElim

import Data.SortedSet as Set
import Data.SortedMap

import GRIN.AST
import GRIN.GrinM

collectUsedSVal : SVal -> SortedSet Var
collectUsedSVal (SVar x) = singleton x
collectUsedSVal (SLit x) = empty

collectUsedVal : Val name -> SortedSet Var
collectUsedVal (SimpleVal x) = collectUsedSVal x
collectUsedVal (ConstTagNode x xs) = foldMap collectUsedSVal xs
collectUsedVal (ConstTag x) = empty
collectUsedVal (VarTagNode x xs) = insert x $ foldMap collectUsedSVal xs
collectUsedVal VUnit = empty

mutual
    collectUsedSExp : SExp name -> SortedSet Var
    collectUsedSExp (Do x) = collectUsedExp x
    collectUsedSExp (App x xs) = fromList xs
    collectUsedSExp (Pure x) = collectUsedVal x
    collectUsedSExp (Store x) = collectUsedVal x
    collectUsedSExp (Fetch x y) = singleton y
    collectUsedSExp (FetchI x k y) = singleton y
    collectUsedSExp (Update x y) = empty

    collectUsedExp : Exp name -> SortedSet Var
    collectUsedExp (SimpleExp x) = collectUsedSExp x
    collectUsedExp (Bind x y z) = collectUsedSExp y <+> collectUsedExp z
    collectUsedExp (Case x xs) = collectUsedVal x <+> foldMap collectUsedAlt xs

    collectUsedAlt : Alt name -> SortedSet Var
    collectUsedAlt (MkAlt _ exp) = collectUsedExp exp

mutual
    pureSExp : SExp name -> Bool
    pureSExp (Do x) = pureExp x
    pureSExp (App x xs) = False -- TODO: effect tracking
    pureSExp (Update x y) = False
    pureSExp _ = True

    pureExp : Exp name -> Bool
    pureExp (SimpleExp x) = pureSExp x
    pureExp (Bind x y z) = pureSExp y && pureExp z
    pureExp (Case x xs) = all pureAlt xs

    pureAlt : Alt name -> Bool
    pureAlt (MkAlt _ exp) = pureExp exp

parameters (used : SortedSet Var)
  mutual
    removeUnusedSExp : SExp name -> SExp name
    removeUnusedSExp (Do x) = mkDo $ removeUnusedExp x
    removeUnusedSExp exp = exp

    removeUnusedExp : Exp name -> Exp name
    removeUnusedExp (SimpleExp x) = mkSimpleExp $ removeUnusedSExp x
    removeUnusedExp (Bind v@(SimpleVal $ SVar x) y z) = if contains x used || not (pureSExp y)
        then Bind v (removeUnusedSExp y) (removeUnusedExp z)
        else removeUnusedExp z
    removeUnusedExp (Bind v y z) = Bind v (removeUnusedSExp y) (removeUnusedExp z)
    removeUnusedExp (Case x xs) = Case x $ removeUnusedAlt <$> xs

    removeUnusedAlt : Alt name -> Alt name
    removeUnusedAlt (MkAlt pat exp) = MkAlt pat $ removeUnusedExp exp

removeUnusedDef : Def name -> Def name
removeUnusedDef def =
    let used = collectUsedExp def.body
     in record { body $= removeUnusedExp used } def

export
unusedVarElim : Monad m => Ord name => GrinT name m ()
unusedVarElim = do
    p@(MkProg exts defs _) <- gets prog
    putProg $ record { defs = map removeUnusedDef defs } p
    -- invalidate CallGraph


text:
module Compiler.LLVM.Rapid.Object

import Data.Vect

import Control.Codegen
import Compiler.LLVM.IR
import Compiler.LLVM.Instruction
import Data.Utils
import Rapid.Common

export
OBJECT_TYPE_ID_CON_NO_ARGS : Int
OBJECT_TYPE_ID_CON_NO_ARGS = 0xff

export
OBJECT_TYPE_ID_INT : Int
OBJECT_TYPE_ID_INT = 1

-- for now treat all numbers the same
export
OBJECT_TYPE_ID_DOUBLE : Int
OBJECT_TYPE_ID_DOUBLE = 1

export
OBJECT_TYPE_ID_BITS64 : Int
OBJECT_TYPE_ID_BITS64 = 1

export
OBJECT_TYPE_ID_STR : Int
OBJECT_TYPE_ID_STR = 2

export
OBJECT_TYPE_ID_CLOSURE : Int
OBJECT_TYPE_ID_CLOSURE = 3

export
OBJECT_TYPE_ID_CHAR : Int
OBJECT_TYPE_ID_CHAR = 4

export
OBJECT_TYPE_ID_IOREF : Int
OBJECT_TYPE_ID_IOREF = 5

export
OBJECT_TYPE_ID_BUFFER : Int
OBJECT_TYPE_ID_BUFFER = 6

export
OBJECT_TYPE_ID_OPAQUE : Int
OBJECT_TYPE_ID_OPAQUE = 0x07

export
OBJECT_TYPE_ID_POINTER : Int
OBJECT_TYPE_ID_POINTER = 0x08

export
OBJECT_TYPE_ID_IOARRAY : Int
OBJECT_TYPE_ID_IOARRAY = 0x09

export
OBJECT_TYPE_ID_BIGINT : Int
OBJECT_TYPE_ID_BIGINT = 0x0a

export
OBJECT_TYPE_ID_CLOCK : Int
OBJECT_TYPE_ID_CLOCK = 0x0b

export
getObjectSlotAddrVar : {t : IRType} -> IRValue IRObjPtr -> IRValue I64 -> Codegen (IRValue (Pointer 1 t))
getObjectSlotAddrVar obj pos = do
  slotPtr <- SSA (Pointer 1 $ Pointer 0 I8) <$> assignSSA ("getelementptr inbounds %Object, " ++ toIR obj ++ ", i32 0, i32 1, " ++ toIR pos)
  bitcastA slotPtr

export
getObjectPayloadAddr : {t : IRType} -> IRValue IRObjPtr -> Codegen (IRValue (Pointer 1 t))
getObjectPayloadAddr obj = getObjectSlotAddrVar obj (Const I64 0)

export
getObjectSlot : {t : IRType} -> IRValue IRObjPtr -> Int -> Codegen (IRValue t)
getObjectSlot obj n = load !(getObjectSlotAddrVar obj (Const I64 $ cast n))

export
putObjectSlot : {t : IRType} -> IRValue IRObjPtr -> IRValue I64 -> IRValue t -> Codegen ()
putObjectSlot {t} obj pos val = store val !(getObjectSlotAddrVar obj pos)

export
getObjectHeader : IRValue IRObjPtr -> Codegen (IRValue I64)
getObjectHeader obj = do
  headerPtr <- SSA (Pointer 1 I64) <$> assignSSA ("getelementptr inbounds %Object, " ++ (toIR obj) ++ ", i32 0, i32 0")
  load headerPtr

export
getObjectSize : IRValue IRObjPtr -> Codegen (IRValue I32)
getObjectSize obj = do
  hdr <- getObjectHeader obj
  mkTrunc {to=I32} hdr

export
putObjectHeader : IRValue IRObjPtr -> IRValue I64 -> Codegen ()
putObjectHeader obj hdr = do
  headerPtr <- SSA (Pointer 1 I64) <$> assignSSA ("getelementptr inbounds %Object, " ++ (toIR obj) ++ ", i32 0, i32 0")
  store hdr headerPtr

export
mkHeader : Int -> IRValue I32 -> Codegen (IRValue I64)
mkHeader objType sizeOrTag =
  mkOr (Const I64 $ (cast objType) `prim__shl_Integer` 32) !(mkZext sizeOrTag)

export
constHeader : Int -> Bits32 -> IRValue I64
constHeader objType sizeOrTag =
  Const I64 $ cast (((cast objType) `prim__shl_Bits64` 32) `prim__or_Bits64` (cast sizeOrTag))

HEADER_SIZE : IRValue I64
HEADER_SIZE = (Const I64 8)

export
dynamicAllocateInto : GCFlavour -> String -> IRValue I64 -> Codegen ()
dynamicAllocateInto Statepoint destVarName payloadSize = do
  totalSize <- mkAddNoWrap payloadSize HEADER_SIZE

  hp <- ((++) "%RuntimePtr ") <$> assignSSA "load %RuntimePtr, %RuntimePtr* %HpVar"
  hpLim <- ((++) "%RuntimePtr ") <$> assignSSA "load %RuntimePtr, %RuntimePtr* %HpLimVar"
  let base = "%TSOPtr %BaseArg"

  allocated <- assignSSA $ "call fastcc %Return1 @rapid_allocate_fast(" ++ showSep ", " [hp, base, hpLim] ++ ", "++(toIR totalSize)++") alwaysinline optsize nounwind"
  newHp <- assignSSA $ "extractvalue %Return1 " ++ allocated ++ ", 0"
  appendCode $ "store %RuntimePtr " ++ newHp ++ ", %RuntimePtr* %HpVar"
  newHpLim <- assignSSA $ "extractvalue %Return1 " ++ allocated ++ ", 1"
  appendCode $ "store %RuntimePtr " ++ newHpLim ++ ", %RuntimePtr* %HpLimVar"
  appendCode $ destVarName ++ " = extractvalue %Return1 " ++ allocated ++ ", 2"
dynamicAllocateInto Zero destVarName payloadSize = do
  payloadSizePlus7 <- mkAddNoWrap payloadSize (Const I64 7)
  payloadSizeAligned <- mkAnd payloadSizePlus7 (Const I64 (-8))
  totalSize <- mkAddNoWrap payloadSizeAligned HEADER_SIZE
  appendCode $ destVarName ++ " = call ccc %ObjPtr @malloc(" ++ toIR totalSize ++ ")"
dynamicAllocateInto BDW destVarName payloadSize = do
  payloadSizePlus7 <- mkAddNoWrap payloadSize (Const I64 7)
  payloadSizeAligned <- mkAnd payloadSizePlus7 (Const I64 (-8))
  totalSize <- mkAddNoWrap payloadSizeAligned HEADER_SIZE
  appendCode $ destVarName ++ " = call ccc %ObjPtr @GC_malloc(" ++ toIR totalSize ++ ")"

export
dynamicAllocate : IRValue I64 -> Codegen (IRValue IRObjPtr)
dynamicAllocate payloadSize = do
  varName <- mkVarName "%a"
  gc <- gcFlavour <$> getOpts
  dynamicAllocateInto gc varName payloadSize
  pure $ SSA IRObjPtr varName

TRACE : Bool
TRACE = False

export
assertObjectTypeAny : IRValue IRObjPtr -> Integer -> Codegen ()
assertObjectTypeAny o msg = when TRACE $ do
  let tVal = (Const I64 (0x10000 + msg))
  typeOk <- genLabel "typecheck_ok"
  typeError <- genLabel "typecheck_error"
  typeEnd <- genLabel "typecheck_end"

  hdr <- getObjectHeader o
  hdrTypFull <- mkShiftR hdr (Const I64 32)
  hdrTyp <- mkAnd (Const I64 0xff) hdrTypFull
  hdrTypOk <- icmp "ne" (Const I64 0) hdrTyp
  branch hdrTypOk typeOk typeError
  beginLabel typeError
  appendCode $ "call ccc void @idris_rts_crash_typecheck(" ++ showSep ", " [toIR o, toIR tVal] ++ ") noreturn"
  appendCode $ "unreachable"
  beginLabel typeOk

export
assertObjectType' : IRValue IRObjPtr -> Int -> Codegen ()
assertObjectType' o t = when TRACE $ do
  let tVal = (Const I64 $ cast t)
  typeOk <- genLabel "typecheck_ok"
  typeError <- genLabel "typecheck_error"
  typeEnd <- genLabel "typecheck_end"

  hdr <- getObjectHeader o
  hdrTypFull <- mkShiftR hdr (Const I64 32)
  hdrTyp <- mkAnd (Const I64 0xff) hdrTypFull
  hdrTypOk <- icmp "eq" tVal hdrTyp
  branch hdrTypOk typeOk typeError
  beginLabel typeError
  appendCode $ "call ccc void @idris_rts_crash_typecheck(" ++ showSep ", " [toIR o, toIR tVal] ++ ") noreturn"
  appendCode $ "unreachable"
  beginLabel typeOk

export
cgMkChar : IRValue I32 -> Codegen (IRValue IRObjPtr)
cgMkChar val = do
  newObj <- dynamicAllocate (ConstI64 0)
  header <- mkHeader OBJECT_TYPE_ID_CHAR val
  putObjectHeader newObj header
  pure newObj

export
unboxChar' : IRValue IRObjPtr -> Codegen (IRValue I32)
unboxChar' src = do
  charHdr <- getObjectHeader src
  pure !(mkTrunc charHdr)

export
mkCon : Int -> List (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mkCon tag args = do
  newObj <- dynamicAllocate (ConstI64 $ cast (8 * (length args)))
  -- TODO: add object type to header for GC
  hdr <- mkHeader OBJECT_TYPE_ID_CON_NO_ARGS (pConst tag)
  hdrWithArgCount <- mkOr hdr (Const I64 ((cast $ length args) `prim__shl_Integer` 40))
  putObjectHeader newObj hdrWithArgCount
  let enumArgs = enumerate args
  for_ enumArgs (\x => let (i, arg) = x in do
                            assertObjectTypeAny arg (cast i+1)
                            putObjectSlot newObj (ConstI64 $ cast i) arg
                          )
  pure newObj

export
mkConstCon : Int -> List (String) -> Codegen (IRValue IRObjPtr)
mkConstCon tag args = do
  let newHeader = constHeader (OBJECT_TYPE_ID_CON_NO_ARGS + (256 * (cast $ length args))) (cast tag)
  let typeSignature = "{i64" ++ repeatStr ", %ObjPtr" (length args) ++ "}"
  cName <- addConstant $ "private unnamed_addr addrspace(1) constant " ++ typeSignature ++ " {" ++ toIR newHeader ++ (concat $ map ((++) ", ") args) ++ "}, align 8"
  pure $ SSA IRObjPtr $ "bitcast (" ++ typeSignature ++ " addrspace(1)* " ++ cName ++ " to %ObjPtr)"

export
cgMkDouble : IRValue F64 -> Codegen (IRValue IRObjPtr)
cgMkDouble val = do
  newObj <- dynamicAllocate (ConstI64 8)
  putObjectHeader newObj (constHeader OBJECT_TYPE_ID_DOUBLE 0)
  putObjectSlot newObj (ConstI64 0) val
  pure newObj

export
cgMkConstDouble : Double -> Codegen (IRValue IRObjPtr)
cgMkConstDouble d = do
  let newHeader = constHeader OBJECT_TYPE_ID_DOUBLE 0
  let typeSignature = "{i64, double}"
  cName <- addConstant $ "private unnamed_addr addrspace(1) constant " ++ typeSignature ++ " {" ++ toIR newHeader ++ ", double 0x" ++ (assert_total $ doubleToHex d) ++ "}, align 8"
  pure $ SSA IRObjPtr $ "bitcast (" ++ typeSignature ++ " addrspace(1)* " ++ cName ++ " to %ObjPtr)"

export
cgMkDoubleFromBits : IRValue I64 -> Codegen (IRValue IRObjPtr)
cgMkDoubleFromBits val = do
  newObj <- dynamicAllocate (ConstI64 8)
  putObjectHeader newObj (constHeader OBJECT_TYPE_ID_DOUBLE 0)
  putObjectSlot newObj (Const I64 0) val
  pure newObj

export
unboxFloat64 : IRValue (Pointer 0 IRObjPtr) -> Codegen (IRValue F64)
unboxFloat64 src = getObjectSlot {t=F64} !(load src) 0

export
unboxFloat64' : IRValue IRObjPtr -> Codegen (IRValue F64)
unboxFloat64' src = getObjectSlot {t=F64} src 0

export
cgMkInt : IRValue I64 -> Codegen (IRValue IRObjPtr)
cgMkInt val = do
  boxed <- assignSSA $ "tail call fastcc noalias %ObjPtr @llvm.rapid.boxint(" ++ toIR val ++ ") \"gc-leaf-function\""
  pure (SSA IRObjPtr boxed)

export
unboxInt' : IRValue IRObjPtr -> Codegen (IRValue I64)
unboxInt' src = SSA I64 <$> assignSSA ("tail call fastcc i64 @llvm.rapid.unboxint(" ++ toIR src ++ ") \"gc-leaf-function\"")

export
cgMkBits64 : IRValue I64 -> Codegen (IRValue IRObjPtr)
cgMkBits64 val = do
  newObj <- dynamicAllocate (ConstI64 8)
  putObjectHeader newObj (constHeader OBJECT_TYPE_ID_BITS64 0)
  putObjectSlot newObj (ConstI64 0) val
  pure newObj

-- TODO: change to List Bits8
utf8EncodeChar : Char -> List Int
utf8EncodeChar c = let codepoint = cast {to=Int} c
                       bor = prim__or_Int
                       band = prim__and_Int
                       shr = prim__shr_Int in
                       map id $
                       if codepoint <= 0x7f then [codepoint]
                       else if codepoint <= 0x7ff then [
                         bor 0xc0 (codepoint `shr` 6),
                         bor 0x80 (codepoint `band` 0x3f)
                         ]
                       else if codepoint <= 0xffff then [
                         bor 0xe0 (codepoint `shr` 12),
                         bor 0x80 ((codepoint `shr` 6) `band` 0x3f),
                         bor 0x80 ((codepoint `shr` 0) `band` 0x3f)
                         ]
                       else [
                         bor 0xf0 (codepoint `shr` 18),
                         bor 0x80 ((codepoint `shr` 12) `band` 0x3f),
                         bor 0x80 ((codepoint `shr` 6) `band` 0x3f),
                         bor 0x80 ((codepoint `shr` 0) `band` 0x3f)
                         ]

utf8EncodeString : String -> List Int
utf8EncodeString s = concatMap utf8EncodeChar $ unpack s

getStringIR : List Int -> String
getStringIR utf8bytes = concatMap okchar utf8bytes
  where
    okchar : Int -> String
    -- c >= ' ' && c <= '~' && c /= '\\' && c /= '"'
    okchar c = if c >= 32 && c <= 126 && c /= 92 && c /= 34
                  then cast $ cast {to=Char} c
                  else "\\" ++ asHex2 c

export
mkStr : String -> Codegen (IRValue IRObjPtr)
mkStr s = do
  let utf8bytes = utf8EncodeString s
  let len = length utf8bytes
  let newHeader = constHeader OBJECT_TYPE_ID_STR (cast len)
  let typeSignature = "{i64, [" ++ show len ++ " x i8]}"
  cName <- addConstant $ "private unnamed_addr addrspace(1) constant " ++ typeSignature ++ " {" ++ toIR newHeader ++ ", [" ++ show len ++ " x i8] c\"" ++ (getStringIR utf8bytes) ++ "\"}, align 8"
  pure $ SSA IRObjPtr $ "bitcast (" ++ typeSignature ++ " addrspace(1)* " ++ cName ++ " to %ObjPtr)"

export
getStringByteLength : IRValue IRObjPtr -> Codegen (IRValue I32)
getStringByteLength = getObjectSize

export
mkUnit : Codegen (IRValue IRObjPtr)
mkUnit = mkCon 0 []

{- Runtime-related stuff, might fit into own module -}
export
mkRuntimeCrash : String -> Codegen ()
mkRuntimeCrash s = do
  msg <- mkStr s
  appendCode $ "  call ccc void @idris_rts_crash_msg(" ++ toIR msg ++ ") noreturn"
  appendCode $ "unreachable"

export
globalHpVar : IRValue (Pointer 0 RuntimePtr)
globalHpVar = SSA (Pointer 0 RuntimePtr) "%HpVar"

export
globalHpLimVar : IRValue (Pointer 0 RuntimePtr)
globalHpLimVar = SSA (Pointer 0 RuntimePtr) "%HpLimVar"

export
globalRValVar : IRValue (Pointer 0 IRObjPtr)
globalRValVar = SSA (Pointer 0 IRObjPtr) "%rvalVar"

export
funcEntry : Codegen ()
funcEntry = do
  appendCode "%HpVar = alloca %RuntimePtr\n"
  appendCode "%HpLimVar = alloca %RuntimePtr\n"
  appendCode "%rvalVar = alloca %ObjPtr\n"
  store (SSA RuntimePtr "%HpArg") globalHpVar
  store (SSA RuntimePtr "%HpLimArg") globalHpLimVar
  store nullPtr globalRValVar

export
funcReturn : Codegen ()
funcReturn = do
  finHp <- load globalHpVar
  finHpLim <- load globalHpLimVar
  finRVal <- load globalRValVar

  ret1 <- assignSSA $ "insertvalue %Return1 undef, " ++ toIR finHp ++ ", 0"
  ret2 <- assignSSA $ "insertvalue %Return1 " ++ ret1 ++ ", " ++ toIR finHpLim ++ ", 1"
  ret3 <- assignSSA $ "insertvalue %Return1 " ++ ret2 ++ ", " ++ toIR finRVal ++ ", 2"
  appendCode $ "ret %Return1 " ++ ret3


text:
data Sentence : String -> Type where
  Phrase : (s:String) -> Sentence s

say : Sentence "Hello World!" -> IO ()
say _ = printLn "Hello World!"

main : IO ()
main = say $ Phrase "Hello World!"

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Neg num, Integral num, Abs num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x =  0 - x
  (-) = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs

Show ty => Show (Expr ty) where
  show (Val x) = show x
  show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
  show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
  show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
  show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
  show (Abs x) = " |" ++ show x ++ "| "

(Eq ty, Abs ty, Integral ty, Neg ty)=> Eq (Expr ty) where
  (==) x y = eval x == eval y

Cast ty ty where
  cast orig = orig

(Eq tx, Abs tx, Integral tx, Neg tx, Cast tx ty) => Cast (Expr tx) ty where
  cast orig = cast (eval orig)

Functor Expr where
  map func (Val x) = Val (func x)
  map func (Add x y) = Add (map func x) (map func y)
  map func (Sub x y) = Sub (map func x) (map func y)
  map func (Mul x y) = Mul (map func x) (map func y)
  map func (Div x y) = Div (map func x) (map func y)
  map func (Abs x) = Abs (map func x)


text:
||| The Core Computation Context.
|||
||| Module    : Core.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
||| `TheRug` is defined in the toolkit. Here we establish the synonyms
||| required for `Idealised`.
|||
module Circuits.Idealised.Core

import        System

import        Data.String

import public Toolkit.TheRug
import        Toolkit.System

import public Circuits.Idealised.Error
import        Circuits.Idealised.Pretty

%default total

public export
%inline
Idealised : Type -> Type
Idealised = TheRug Idealised.Error

namespace Idealised

  %inline
  whenErr : (msg : Idealised.Error)
                -> IO ()
  whenErr err
    = do putStrLn (show err)
         exitWith (ExitFailure 1)

  %inline
  whenOK : a -> IO ()
  whenOK _ = pure ()

  export
  run : (prog : Idealised a)
             -> IO ()
  run = run whenErr whenOK

-- [ 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:
{-data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

data Elem : a -> Vect k a -> Type where
  Here : Elem x (x :: xs)
  There : (later : Elem x xs) -> Elem x (y :: xs)

import Data.Vect

removeElem : DecEq a => (value : a) -> (xs : Vect (S n) a) -> Vect n a
removeElem value (x :: xs) = case decEq value x of
                                  (Yes prf) => xs
                                  (No contra) => ?removeElem_rhs_3

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

import Data.Vect

removeElem: (value : a) ->
            (xs : Vect (S n) a) ->
            (prf : Elem value xs) ->
            Vect n a
removeElem value (value :: ys) Here = ys
removeElem value {n = Z} (y :: []) (There later) = absurd later
removeElem value {n = (S k)} (y :: ys) (There later)
                                              = y :: removeElem value ys later
Uninhabited (2 + 2 = 5) where
  uninhabited Refl impossible

removeElem_auto : (value : a) -> (xs : Vect (S n) a) ->
                  {auto prf : Elem value xs} -> Vect n a
removeElem_auto value xs {prf} = removeElem value xs prf

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


text:
module Main

pattern : Eff () [STDIO]
pattern = do putStrLn "Pattern:"
        for x in [1..4]:
			for y in [1..x]:
				putStr ("*")
			putStrLn ("")

main : IO ()
main = run pattern

--Run:
--$ idris pattern.idr -o pattern
--$ ./pattern

max_stars_repo_name: coyote-dev/Hello-World

max_issues_repo_name: coyote-dev/Hello-World

max_forks_repo_name: coyote-dev/Hello-World


text:
module AwesomeProgram

import AwesomeLib

mutual
  awesomeNat : Nat -> Awesome Nat
  awesomeNat n = MkAwesome n

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module Main

interleave : Ord a => List a -> List a -> List a
interleave (e1 :: r1) (e2 :: r2) with (compare e1 e2)
  | LT = e1 :: merge r1 (e2 :: r2)
  | EQ = e1 :: merge r1 r2
  | GT = e2 :: merge (e1 :: r1) r2

euler : Nat -> List Nat
euler = (interleave (take))

main : IO ()
main = putStrLn ?greeting

max_stars_repo_name: ericvm/euler-project

max_issues_repo_name: ericvm/euler-project

max_forks_repo_name: ericvm/euler-project


text:
module Palindrome

export
palindrome : Nat -> String -> Bool
palindrome minLen str = longEnough && lowered == (Strings.reverse lowered)
  where
    longEnough = length str > minLen
    lowered = toLower str

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:
foo : Semigroup a => a -> ()
foo x = ()

main : IO ()
main = pure (foo ())


text:
module Main

import System.Concurrency

child : Condition -> Mutex -> IO ()
child cond mtx = do
    mutexAcquire mtx
    str <- getThreadData String
    putStrLn $ "child data: " ++ (show str)

    setThreadData 17
    i <- getThreadData Int
    putStrLn $ "child data now: " ++ (show i)

    conditionSignal cond
    conditionWait cond mtx

    putStrLn $ "child exiting"

    conditionSignal cond
    mutexRelease mtx

main : IO ()
main = do
    setThreadData 13
    i <- getThreadData Int
    putStrLn $ "parent data initialized to: " ++ (show i)

    setThreadData "hello"
    str <- getThreadData String
    putStrLn $ "parent data now: " ++ (show str)

    mtx <- makeMutex
    cond <- makeCondition

    mutexAcquire mtx
    _ <- fork (child cond mtx)
    conditionWait cond mtx

    str2 <- getThreadData String
    putStrLn $ "parent data still: " ++ (show str2)

    conditionSignal cond
    conditionWait cond mtx

    putStrLn $ "parent exiting"
    mutexRelease mtx


text:
import Data.Vect

add_row : Num num => (xs : Vect cols num) -> (ys : Vect cols num) -> Vect cols num
add_row [] [] = []
add_row (x :: xs) (y :: ys) = (x + y) :: add_row xs ys

add : Num num =>
      Vect rows (Vect cols num) -> Vect rows (Vect cols num) ->
      Vect rows (Vect cols num)
add [] [] = []
add (x :: xs) (y :: ys) = let rest = add xs ys
                          in add_row x y :: rest

create_empties : Vect n (Vect 0 el)
create_empties {n} = replicate n []

transpose_mat : Vect n (Vect m el) -> Vect m (Vect n el)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = zipWith (::) x (transpose_mat xs)

calc_row : Num num => (xs : Vect m num) -> (rgt : Vect p (Vect m num)) -> Vect p num
calc_row xs ys = map (\x => sum (zipWith (*) xs x)) ys

mult : Num num =>
       Vect n (Vect m num) -> Vect m (Vect p num) ->
       Vect n (Vect p num)
mult lft rgt = let rgt' = transpose_mat rgt in
               map (\r => calc_row r rgt') lft


text:
module Flexidisc.Record.Type

import        Flexidisc.RecordContent
import public Flexidisc.THList

import public Flexidisc.Dec.IsYes
import public Flexidisc.Header
import public Flexidisc.TaggedValue

%default total
%access export

-- CREATE

||| A `RecordM` is a set of rows
||| @ m      A Type constructor used to decorate all values of the record
||| @ k      The type of the labels
||| @ header The list of rows into the record, with their types
public export
data RecordM : (m : Type -> Type) -> (k : Type) -> (header : Header k) -> Type where
  Rec : (o : Ord k) =>
        (values : RecordContentM m k o header) -> (nubProof : Nub header) ->
        RecordM m k (H header)

public export
Record : (k : Type) -> (header : Header k) -> Type
Record = RecordM id

infix 6 :::

||| Convenient helper for row type readability
public export
(:::) : (k : l) -> (v : Type) -> Pair l Type
(:::) = MkPair

%name Record xs, ys, zs

||| The empty record
public export
Nil : Ord k => RecordM m k []
Nil = Rec empty []

||| Insert a new row in a record (with explicit proof)
public export
cons' : (DecEq k, Ord k) => TaggedValue k' (m ty) -> RecordM m k header ->
        (fresh : Fresh k' header) ->
        RecordM m k ((k', ty) :: header)
cons' x (Rec xs isnub) (F fresh) =
  Rec (insert x xs) (freshInsert fresh isnub)

||| Insert a new row in a record
public export
cons : (DecEq k, Ord k) => TaggedValue k' (m ty) -> RecordM m k header ->
       {default SoTrue fresh : IsFresh k' header} ->
       RecordM m k ((k', ty) :: header)
cons x xs {fresh} = cons' x xs (getProof fresh)

||| Insert a new row in a record
public export
(::) : (DecEq k, Ord k) => TaggedValue k' (m ty) -> RecordM m k header ->
       {default SoTrue fresh : IsFresh k' header} ->
       RecordM m k ((k', ty) :: header)
(::) = cons

||| Decide whether a record can be extended with the proposed key/value pair or not
public export
decCons : (DecEq k, Ord k) =>
          TaggedValue k' (m ty) -> RecordM m k header ->
          Dec (RecordM m k ((k', ty) :: header))
decCons x (Rec xs _) {k'} {ty} {header = H hs} with (decNub (insert (k', ty) hs))
  | (Yes prf) = Yes (Rec (insert x xs) prf)
  | (No contra) = No (cantBuildARecordWithNonNubHeader contra)
  where
    cantBuildARecordWithNonNubHeader : (DecEq k, o : Ord k) =>
                                       {hs : OrdHeader k o} ->
                                       (contra : Nub hs -> Void) -> Not (RecordM m k (H hs))
    cantBuildARecordWithNonNubHeader contra (Rec xs prf) = contra prf

||| It's just monomorphic `id` with a fancy name, to help type inference
recM : (m : Type -> Type) -> RecordM m k header -> RecordM m k header
recM _ = id

||| It's just monomorphic `id` with a fancy name, to help type inference
rec : Record k header -> Record k header
rec = id

namespace test
  %access private

  test_rec1 : Record String ["Firstname" ::: String]
  test_rec1 = ["Firstname" := "John"]

  test_rec2 : Record String ["Lastname" ::: String, "Firstname" ::: String]
  test_rec2 = ["Firstname" := "John", "Lastname" := "Doe"]

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Math

%include C "eps.h"
%link C "eps.o"

machineEps : Double -> Double
machineEps x = unsafePerformIO $ foreign FFI_C "machine_eps" (Double -> IO Double) x

max_stars_repo_name: sebeaumont/hilbert

max_issues_repo_name: sebeaumont/hilbert

max_forks_repo_name: sebeaumont/hilbert


text:
module Control.ST.Curses

import Control.ST
import public UI.Curses

%access export

||| This is used to specify whether colors can be used or not
public export
data HasColor = Color | NoColor

||| This is the resource for the `CURSES` effect before it has done anything
public export
data Pre = MkPre

||| When the `CURSES` effect has this resource, the curses functions can be
||| called. Note that a `CURSES` effect should only be `run` if the type
||| signature does not contain the `Active` resource.
public export
data Active : (hasColor : HasColor) -> Type where
  MkActive : Active hasColor

||| This is the resource the `CURSES` effect has after curses has been
||| terminated
public export
data Post = MkPost

Default Pre where
  default = MkPre

public export
data Curses : Effect where

  Start : GetChMode ->  sig Curses () Pre (Active NoColor)
  End   :               sig Curses () (Active c) Post

  StartColor :  Curses HasColor (Active NoColor) (\result => Active result)

  MovePrevCh    :                   { Active c } Curses Bool
  MoveNextCh    :                   { Active c } Curses Bool
  Move          : Int -> Int ->     { Active c } Curses Bool
  SetGetChMode  : GetChMode ->      { Active c } Curses ()
  ScrSize       :                   { Active c } Curses (Int, Int)
  Refresh       :                   { Active c } Curses ()
  Keypad        : Bool ->           { Active c } Curses ()
  GetYX         :                   { Active c } Curses (Int, Int)
  GetMaxYX      :                   { Active c } Curses (Int, Int)
  GetStr        : Bool -> Bool ->   { Active c } Curses String
  GetCh         :                   { Active c } Curses (Maybe Char)
  ForceCh       :                   { Active c } Curses Char
  Echo          : Bool ->           { Active c } Curses ()
  CursSet       : CursorState ->    { Active c } Curses (Maybe CursorState)
  ClrToEol      :                   { Active c } Curses ()
  Clear         :                   { Active c } Curses ()
  AddStr        : String ->         { Active c } Curses ()
  AddNStr       : String -> Nat ->  { Active c } Curses ()
  AddCh         : Char ->           { Active c } Curses ()

  SetAttr         : List Attr -> { Active NoColor } Curses ()
  SetAttrAndColor : List Attr -> Maybe ColorPair ->
                      { Active Color } Curses ()

Handler Curses IO where
  handle _ (Start gcm) k = startCurses gcm  *> k () MkActive
  handle _ End         k = endWin           *> k () MkPost

  handle _ StartColor k = do success <- hasColors
                             startColor
                             k (if success then Color else NoColor) MkActive

  handle m MovePrevCh k = movePrevCh >>= \success => k success m
  handle m MoveNextCh k = moveNextCh >>= \success => k success m
  handle m (Move y x) k = move y x   >>= \success => k success m

  handle m (SetGetChMode gcm)  k = setGetChMode gcm *>              k ()      m
  handle m ScrSize             k = scrSize          >>= \dims   =>  k dims    m
  handle m Refresh             k = refresh          *>              k ()      m
  handle m (Keypad bf)         k = keypad   bf      *>              k ()      m
  handle m GetYX               k = getYX            >>= \coords =>  k coords  m
  handle m GetMaxYX            k = getMaxYX         >>= \maxYX  =>  k maxYX   m
  handle m (GetStr ue se)      k = getStr   ue  se  >>= \str    =>  k str     m
  handle m GetCh               k = getCh            >>= \mc     =>  k mc      m
  handle m ForceCh             k = forceCh          >>= \c      =>  k c       m
  handle m (Echo bf)           k = echo bf          *>              k ()      m
  handle m (CursSet cs)        k = cursSet  cs      >>= \mcs    =>  k mcs     m
  handle m ClrToEol            k = clrToEol         *>              k ()      m
  handle m Clear               k = clear            *>              k ()      m
  handle m (AddStr str)        k = addStr   str     *>              k ()      m
  handle m (AddNStr str n)     k = addNStr  str n   *>              k ()      m
  handle m (AddCh c)           k = addCh    c       *>              k ()      m

  handle m (SetAttr attrs)             k =
    setAttrAndColor attrs Nothing *> k () m
  handle m (SetAttrAndColor attrs col) k =
    setAttrAndColor attrs col     *> k () m

||| The curses effect.
CURSES : Type -> EFFECT
CURSES res = MkEff res Curses

||| Use this function to start curses. Note that `end` should *always* be called
||| before the program terminates.
||| @getChMode the mode that getCh will use
start : (getChMode : GetChMode) ->
        { [CURSES Pre] ==> [CURSES $ Active NoColor] } Eff ()
start gcm = call $ Start gcm

||| Terminates curses. This should *always* be called before the program
||| terminates.
end : { [CURSES $ Active c] ==> [CURSES Post] } Eff ()
end = call Effect.Curses.End

||| Tries to initialize colors. The return value specifies if this was
||| successful. You can only use colors if you have called this function
||| and it returned `Color`.
startColor : { [CURSES $ Active NoColor] ==>
               {result} [CURSES $ Active result] } Eff HasColor
startColor = call StartColor

||| Moves the cursor to the previous position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
movePrevCh : { [CURSES $ Active c] } Eff Bool
movePrevCh = call MovePrevCh

||| Advances the cursor to the next position, if possible. Returns `True` if
||| cursor was moved, `False` otherwise.
moveNextCh : { [CURSES $ Active c] } Eff Bool
moveNextCh = call MoveNextCh

||| Moves the cursor to the specified coordinates.
||| Returns `True` if the cursor was moved, `False` otherwise.
||| @y the line to which the cursor will move (counting starts at 0)
||| @x the column to which the cursor will move (counting starts at 0)
move : (y : Int) -> (x : Int) -> { [CURSES $ Active c] } Eff Bool
move y x = call $ Move y x

||| Sets the mode `getCh` will operate in.
setGetChMode : GetChMode -> { [CURSES $ Active c] } Eff ()
setGetChMode gcm = call $ SetGetChMode gcm

||| Returns the size of the standard window.
|||
||| The format is `(lines, columns)`
scrSize : { [CURSES $ Active c] } Eff (Int, Int)
scrSize = call ScrSize

||| Refreshes the standard window. It is unlikely that a program needs to
||| manually call this function.
refresh : { [CURSES $ Active c] } Eff ()
refresh = call Refresh

||| Enables or disables the reading of function keys, arrow keys, and so on.
||| This is turned on by default.
||| @bf if `True`, enables reading, otherwise, disables it.
keypad : (bf : Bool) -> { [CURSES $ Active c] } Eff ()
keypad bf = call $ Keypad bf

||| Returns the current cursor position.
|||
||| The format is `(line, column)`.
getYX : { [CURSES $ Active c] } Eff (Int, Int)
getYX = call GetYX

||| Returns the highest line and column the cursor can be at.
|||
||| The format is `(line, column)`.
getMaxYX : { [CURSES $ Active c] } Eff (Int, Int)
getMaxYX = call GetMaxYX

||| Returns a `String` the user enters. This function is affected by whether or
||| not the `GetChMode` is a "raw" or a "linebuf" mode.
||| @useEcho  if `True`, the user will see the `String` they enter
||| @setEcho  if `True`, echo will be on after the `String` has been returned,
|||             otherwise, echo will be off
getStr : (useEcho : Bool) -> (setEcho : Bool) ->
         { [CURSES $ Active c] } Eff String
getStr ue se = call $ GetStr ue se

||| Returns `Just` a character, or `Nothing` if the `GetChMode` is `Wait k` and
||| the time runs out. See `GetChMode` for more information.
getCh : { [CURSES $ Active c] } Eff $ Maybe Char
getCh = call GetCh

||| Returns a character once the user presses a key. This function is affected
||| by whether or not the `GetChMode` is a "raw" or a "linebuf" mode.
forceCh : { [CURSES $ Active c] } Eff Char
forceCh = call ForceCh

||| `echo` determines whether a character will be printed when the user presses
||| a key
||| @bf whether or not the echo will be on
echo : (bf : Bool) -> { [CURSES $ Active c] } Eff ()
echo bf = call $ Echo bf

||| Sets the cursor state. Returns `Nothing`, if the specified cursor state
||| cannot be set, and `Just` the previous cursor state otherwise.
||| @cs the cursor state that will be set
cursSet : (cs : CursorState) -> { [CURSES $ Active c] } Eff $ Maybe CursorState
cursSet cs = call $ CursSet cs

||| Clears the screen to the end of the line
clrToEol : { [CURSES $ Active c] } Eff ()
clrToEol = call ClrToEol

||| Clears the screen
clear : { [CURSES $ Active c] } Eff ()
clear = call Clear

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s the string that will be printed
addStr : (s : String) -> { [CURSES $ Active c] } Eff ()
addStr str = call $ AddStr str

||| Prints a `String` to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @s        the string that will be printed
||| @maxChars specifies the maximum number of characters that will be printed
addNStr : (s : String) -> (maxChars : Nat) -> { [CURSES $ Active c] } Eff ()
addNStr str k = call $ AddNStr str k

||| Prints a character to the standard screen at current cursor position.
||| The cursor will be advanced after printing.
||| @c the character that will be printed
addCh : (c : Char) -> { [CURSES $ Active col] } Eff ()
addCh c = call $ AddCh c

||| Sets all given attributes.
||| @attrs  the attributes that will be set
setAttr : (attrs : List Attr) -> { [CURSES $ Active NoColor] } Eff ()
setAttr attrs = call $ SetAttr attrs

||| Sets all given attributes and the specified colors.
||| @attrs  the attributes that will be set
||| @colors if this is `Nothing`, the default colors will be used, which are
|||           usually white on black; if this is not `Nothing`, the specified
|||           Pair will be initialized and used - note that if characters on the
|||           screen use the pair with index *i*, and the pair with index *i* is
|||           then reinitialized with different colors, the characters that are
|||           already on the screen will change their color
setAttrAndColor : (attrs : List Attr) -> (colors : Maybe ColorPair) ->
                    { [CURSES $ Active Color] } Eff ()
setAttrAndColor attrs col = call $ SetAttrAndColor attrs col

max_stars_repo_name: zenntenn/curses-idris

max_issues_repo_name: zenntenn/curses-idris

max_forks_repo_name: zenntenn/curses-idris


text:
record Four a b c d where
  constructor MkFour
  x : a
  y : b
  z : c
  w : d

firstTwo : Four a b c d -> (a, b)
firstTwo $ MkFour {x, y, _} = (x, y)

record X where
  constructor MkX
  x : Int
  y : Nat
  z : Integer

SomeX : Monad m => m X
SomeX = pure $ MkX {x=5} {y=3} {z=10}

analyzeX : Monad m => m Integer
analyzeX = do
  MkX {y, z, _} <- SomeX
  pure $ z + natToInteger y

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Graphics.DOT.Parser

import Text.Parser
import Data.String
import Data.Vect

import Graphics.DOT.Lexer
import Graphics.DOT.AST

%default total

-- Terminals --

lBrace : Grammar _ DOTToken True ()
lBrace = terminal "Expected '{'"
            (\case LBrace => Just ()
                   _ => Nothing)

rBrace : Grammar _ DOTToken True ()
rBrace = terminal "Expected '}' (might not be properly closed?)"
            (\case RBrace => Just ()
                   _ => Nothing)

lBracket : Grammar _ DOTToken True ()
lBracket = terminal "Expected '['"
              (\case LBracket => Just ()
                     _ => Nothing)

rBracket : Grammar _ DOTToken True ()
rBracket = terminal "Expected ']' (might not be properly closed?)"
              (\case RBracket => Just ()
                     _ => Nothing)

colon : Grammar _ DOTToken True ()
colon = terminal "Expected ':'"
          (\case Colon => Just ()
                 _ => Nothing)

semicolon : Grammar _ DOTToken True ()
semicolon = terminal "Expected ';' (shouldn't get this message)"
              (\case Semicolon => Just ()
                     _ => Nothing)

comma : Grammar _ DOTToken True ()
comma = terminal "Expected ','"
          (\case Comma => Just ()
                 _ => Nothing)

equals : Grammar _ DOTToken True ()
equals = terminal "Expected '='"
          (\case Equal => Just ()
                 _ => Nothing)

nameID : Grammar _ DOTToken True DOT
nameID = terminal "Not a name"
          (\case (NameID str) => Just (NameID str)
                 _ => Nothing)

numeralID : Grammar _ DOTToken True DOT
numeralID = terminal "Not a numeral"
              (\case (NumeralID num) => Just (NumeralID num)
                     _ => Nothing)

stringID : Grammar _ DOTToken True DOT
stringID = terminal "Not a string"
            (\case (StringID str) => Just (StringID str)
                   _ => Nothing)

htmlID : Grammar _ DOTToken True DOT
htmlID = terminal "Not an HTML string"
          (\case (HTML_ID html) => Just (HTML_ID html)
                 _ => Nothing)

nodeKW : Grammar _ DOTToken True DOT
nodeKW = terminal "Expected 'node' keyword"
          (\case Keyword "node" => Just Node
                 _ => Nothing)

edgeKW : Grammar _ DOTToken True DOT
edgeKW = terminal "Expecetd 'edge' keyword"
          (\case Keyword "edge" => Just Edge
                 _ => Nothing)

graphKW : Grammar _ DOTToken True DOT
graphKW = terminal "Expected 'graph' keyword"
           (\case Keyword "graph" => Just GraphKW
                  _ => Nothing)

digraphKW : Grammar _ DOTToken True DOT
digraphKW = terminal "Expected 'digraph' keyword"
              (\case Keyword "digraph" => Just DiGraph
                     _ => Nothing)

subgraphKW : Grammar _ DOTToken True DOT
subgraphKW = terminal "Expected 'subgraph' keyword"
              (\case Keyword "subgraph" => Just SubGraph
                     _ => Nothing)

strictKW : Grammar _ DOTToken True DOT
strictKW = terminal "Expected 'strict' keyword"
            (\case Keyword "strict" => Just Strict
                   _ => Nothing)

||| Compass points (n, ne, e, se, s, sw, w, nw, c, _).
compassPt : Grammar _ DOTToken True DOT
compassPt = terminal "Unknown compass-point"
              (\case CompassPt pt =>
                        case pt of
                             "n"  => Just North
                             "ne" => Just NorthEast
                             "e"  => Just East
                             "se" => Just SouthEast
                             "s"  => Just South
                             "sw" => Just SouthWest
                             "w"  => Just West
                             "nw" => Just NorthWest
                             "c"  => Just CenterCPt
                             "_"  => Just UnderCPt
                             _    => Nothing
                     _ => Nothing)

||| --
grEdgeOp : Grammar _ DOTToken True DOT
grEdgeOp = terminal "Expected '--'"
            (\case GrEdgeOp => Just GrEdgeOp
                   _ => Nothing)

||| ->
diGrEdgeOp : Grammar _ DOTToken True DOT
diGrEdgeOp = terminal "Exepected '->'"
              (\case DiGrEdgeOp => Just DiGrEdgeOp
                     _ => Nothing)

-- Non-terminals --

||| Keywords ('node', 'edge', 'graph', 'digraph', 'subgraph', 'strict').
keyword : Grammar _ DOTToken True DOT
keyword =  nodeKW
       <|> edgeKW
       <|> graphKW
       <|> digraphKW
       <|> subgraphKW
       <|> strictKW

||| An identifier is either:
||| - a name
||| - a numeral
||| - a quoted string
||| - an HTML string
identifier : Grammar _ DOTToken True DOT
identifier =  nameID
          <|> numeralID
          <|> stringID
          <|> htmlID

||| Assignment, i.e.
||| ID '=' ID
assign_ : Grammar _ DOTToken True DOT
assign_ = do idLHS <- identifier
             equals
             idRHS <- identifier
             pure (Assign [idLHS, idRHS])    -- returns assign node in AST

||| Separators are semicolons and commas, but they are purely aesthetic.
sepChoice : Grammar _ DOTToken False ()
sepChoice = ignore $ optional (choose semicolon comma)

-- helper for `a_list`
a_list' : Grammar _ DOTToken True (List DOT)
a_list' = do head <- assign_
             sepChoice
             rest <- (a_list' <|> pure [])
             pure (head :: rest)

||| An 'a_list' is an assignment, optionally followed by a separator, optionally
||| followed by more of an 'a_list' (see helper `a_list'`).
a_list : Grammar _ DOTToken True DOT
a_list = do l <- a_list'
            pure (AList l)

-- OLD IMPLEMENTATION:
--a_list = (do head <- assign_
--             sepChoice
--             pure (AList [head]))
--      <|> (do head <- assign_
--              sepChoice
--              rest <- a_list
--              pure (AList (head :: [rest])))

-- helper for `attr_list`
attr_list' : Grammar _ DOTToken True (List DOT)
attr_list' = do lBracket
                mAList <- optional a_list
                rBracket
                rest <- (attr_list' <|> pure [])
                the (Grammar _ _ False _) $   -- case can confuse the type-checker
                  case mAList of
                       Nothing      => pure rest
                       (Just aList) => pure (aList :: rest)

||| An 'attr_list' is a '[', optionally followed by an 'a_list', followed by a
||| ']', optionally followed by another 'attr_list' (see helper `attr_list'`).
attr_list : Grammar _ DOTToken True DOT
attr_list = do l <- attr_list'
               pure (AttrList l)

-- OLD IMPLEMENTATION:
--attr_list =  (do lBracket
--                 mAList <- optional a_list
--                 rBracket
--                 pure (AttrList (maybeToList mAList)))
--         <|> (do lBracket
--                 mAList <- optional a_list
--                 rBracket
--                 rest <- attr_list
--                 pure (AttrList ((maybeToList mAList) ++ [rest])))
--          where
--            maybeToList : Maybe DOT -> List DOT
--            maybeToList Nothing    = []
--            maybeToList (Just dot) = [dot]

||| An attr_stmt is one of the keywords 'graph', 'node', or 'edge', followed by
||| an attr_list.
attr_stmt : Grammar _ DOTToken True DOT
attr_stmt =
  do kw <- gne    -- (graph|node|edge)
     attrList <- attr_list
     pure (AttrStmt kw attrList)
  where
    gne : Grammar _ DOTToken True DOT
    gne =  graphKW
       <|> nodeKW
       <|> edgeKW

||| A colon followed by an ID, optionally followed by more colon+compass_pt
||| pairs.
idPort : Grammar _ DOTToken True DOT
idPort = do colon
            id_ <- identifier
            maybeCPT <- optional compassPt
            pure (IDPort id_ maybeCPT)

||| A colon followed by a compass_pt.
cptPort : Grammar _ DOTToken True DOT
cptPort = do colon
             cpt <- compassPt
             pure (CPTPort cpt)

||| A port is either:
||| - A colon followed by an ID, optionally followed by more colon+compass_pt
|||   pairs.
||| - A colon followed by a compass_pt.
port : Grammar _ DOTToken True DOT
port =  idPort
    <|> cptPort

||| A 'node_id' is an identifier optionally followed by a port.
node_id : Grammar _ DOTToken True DOT
node_id = do id_ <- identifier
             mPort <- optional port
             pure (NodeID id_ mPort)

||| A 'node_stmt' is a 'node_id' optionally followed by an 'attr_list'.
node_stmt : Grammar _ DOTToken True DOT
node_stmt = do nID <- node_id
               attrList <- optional attr_list
               pure (NodeStmt nID attrList)

||| An edgeop is either '->' in directed graphs, or '--' in undirected graphs.
edgeop : Grammar _ DOTToken True DOT
edgeop =  diGrEdgeOp
      <|> grEdgeOp

||| A subgraph ID is the keyword 'subgraph' optionally followed by an
||| identifier.
subgraphID : Grammar _ DOTToken True DOT
subgraphID = do ignore $ subgraphKW   -- only one possible kw, so don't store it
                mID <- optional identifier
                pure (SubgraphID mID)

mutual
  ||| A subgraph is optionally a `subgraphID` (a helper function), followed by a
  ||| '{', followed by a 'stmt_list', followed by a '}'.
  subgraph : Grammar _ DOTToken True DOT
  subgraph = do sID <- optional subgraphID
                lBrace
                stmtList <- stmt_list
                rBrace
                pure (Subgraph sID stmtList)

  -- helper for `edgeRHS'` (which is itself a helper) and 'edge_stmt'
  nidORsubgr : Grammar _ DOTToken True DOT
  nidORsubgr =  subgraph
            <|> node_id

  -- helper for edgeRHS
  edgeRHS' : Grammar _ DOTToken True (List DOT)
  edgeRHS' = do edgeOp <- edgeop
                nORs <- nidORsubgr
                rest <- (edgeRHS' <|> pure [])
                pure (edgeOp :: nORs :: rest)

  ||| The RHS of an edge is an 'edgeop', followed by either a 'node_id' or a
  ||| 'subgraph', optionally followed by more 'edgeRHS'.
  edgeRHS : Grammar _ DOTToken True DOT
  edgeRHS = do l <- edgeRHS'
               pure (EdgeRHS l)

  ||| An 'edge_stmt' is either a 'node_id' or a 'subgraph', followed by an
  ||| 'edgeRHS', optionally followed by an 'attr_list'.
  edge_stmt : Grammar _ DOTToken True DOT
  edge_stmt = do nORs <- nidORsubgr
                 rhs <- edgeRHS
                 mAttrList <- optional attr_list
                 pure (EdgeStmt nORs rhs mAttrList)

  -- The possible things that can be in a statement. A helper for 'stmt'.
  stmtAlts : Grammar _ DOTToken True DOT
  stmtAlts =  subgraph
          <|> edge_stmt
          <|> attr_stmt
          <|> assign_
          <|> node_stmt

  ||| A 'stmt' is either a 'node_stmt', 'edge_stmt', 'attr_stmt', an assignment,
  ||| or a subgraph.
  stmt : Grammar _ DOTToken True DOT
  stmt = do theStmt <- stmtAlts
            pure (Stmt theStmt)

  -- helper for 'stmt_list'
  stmt_list' : Grammar _ DOTToken True (List DOT)
  stmt_list' = do aStmt <- stmt
                  ignore $ optional semicolon   -- we don't store the ';'
                  rest <- (stmt_list' <|> pure [])
                  pure (aStmt :: rest)

  ||| A 'stmt_list' is optionally: a 'stmt', followed by an optional semicolon,
  ||| followed by more of a 'stmt_list' (see the `stmt_list'` helper).
  stmt_list : Grammar _ DOTToken True DOT
  stmt_list = do theStmts <- stmt_list'
                 pure (StmtList theStmts)

  -- Is the graph strict? Helper for 'graph'.
  isStrict : Grammar _ DOTToken False Bool
  isStrict = do (Just _) <- optional strictKW
                  | Nothing => pure False
                pure True

  -- Directed or undirected graph? Helper for 'graph'.
  graphType : Grammar _ DOTToken True DOT
  graphType =  graphKW
           <|> digraphKW

  ||| A 'graph' is optionally the keyword "strict", followed by either the
  ||| keywords "graph" or "digraph", optionally followed by an identifier,
  ||| followed by a 'stmt_list' in braces.
  graph : Grammar _ DOTToken True DOT
  graph = do strict <- isStrict
             gType <- graphType
             mID <- optional identifier
             lBrace
             stmtList <- stmt_list
             rBrace
             pure (Graph strict gType mID stmtList)

export
parse :  (xs : List (WithBounds DOTToken))
      -> Either (List1 (ParsingError DOTToken)) (DOT, List (WithBounds DOTToken))
parse xs = parse graph xs


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

module Language.TOML.Tokens

import Text.Token

%default total

public export
strTrue : String
strTrue = "true"

public export
strFalse : String
strFalse = "false"

public export
data Bracket = Open | Close

public export
Eq Bracket where
    (==) Open Open = True
    (==) Close Close = True
    (==) _ _ = False

public export
data Punctuation
    = Comma
    | Dot
    | Equal
    | NewLine
    | Square Bracket
    | Curly Bracket

public export
Eq Punctuation where
    (==) Comma Comma = True
    (==) Dot Dot = True
    (==) Equal Equal = True
    (==) NewLine NewLine = True
    (==) (Square x) (Square y) = x == y
    (==) (Curly x) (Curly y) = x == y
    (==) _ _ = False

public export
data TOMLTokenKind
    = TTBoolean
    | TTInt
    | TTFloat
    | TTString
    | TTPunct Punctuation
    | TTBare
    | TTIgnored

public export
TOMLToken : Type
TOMLToken = Token TOMLTokenKind

public export
Eq TOMLTokenKind where
    (==) TTBoolean TTBoolean = True
    (==) TTInt TTInt = True
    (==) TTFloat TTFloat = True
    (==) TTString TTString = True
    (==) (TTPunct x) (TTPunct y) = x == y
    (==) TTBare TTBare = True
    (==) TTIgnored TTIgnored = True
    (==) _ _ = False

public export
TokenKind TOMLTokenKind where
    TokType TTBoolean = Bool
    TokType TTInt = Integer
    TokType TTFloat = Double
    TokType TTString = String
    TokType (TTPunct _) = ()
    TokType TTBare = String
    TokType TTIgnored = ()

    tokValue TTBoolean s = s == strTrue
    tokValue TTInt s = cast s
    tokValue TTFloat s = cast s
    tokValue TTString s = s -- TODO "unescape" the string
    tokValue (TTPunct _) _ = ()
    tokValue TTBare s = s
    tokValue TTIgnored _ = ()

export
ignored : TOMLToken -> Bool
ignored (Tok TTIgnored _) = True
ignored _ = False

max_stars_repo_name: tiatomee/toml-idr

max_issues_repo_name: tiatomee/toml-idr

max_forks_repo_name: tiatomee/toml-idr


text:
module Rhone.Canvas.Angle

%default total

--------------------------------------------------------------------------------
--          Angle
--------------------------------------------------------------------------------

public export
data Angle : Type where
  Radians : Double -> Angle
  Degree : Double -> Angle

export %inline
rad : Double -> Angle
rad = Radians

export %inline
deg : Double -> Angle
deg = Degree

export
toRadians : Angle -> Double
toRadians (Radians x) = x
toRadians (Degree x)  = (x / 180) * pi

export
toDegree : Angle -> Double
toDegree (Radians x) = (x / pi) * 180
toDegree (Degree x)  = x

export
Show Angle where
  show = show . toDegree