text:
-- source: https://github.com/edwinb/Idris2/blob/master/src/Core/Core.idr

module Core.Core

import Core.Env
import Core.TT
import Data.Vect
import Parser.Support

import public Control.Catchable
import public Data.IORef
import System

%default covering

public export
data TTCErrorMsg
    = Format String Int Int
    | EndOfBuffer String
    | Corrupt String

public export
data CaseError = DifferingArgNumbers
               | DifferingTypes
               | MatchErased (vars ** (Env Term vars, Term vars))
               | NotFullyApplied Name
               | UnknownType

public export
data DotReason = NonLinearVar
               | VarApplied
               | NotConstructor
               | ErasedArg
               | UserDotted
               | UnknownDot

export
Show DotReason where
  show NonLinearVar = "Non linear pattern variable"
  show VarApplied = "Variable applied to arguments"
  show NotConstructor = "Not a constructor application or primitive"
  show ErasedArg = "Erased argument"
  show UserDotted = "User dotted"
  show UnknownDot = "Unknown reason"

-- All possible errors, carrying a location
public export
data Error
    = Fatal Error -- flag as unrecoverable (so don't postpone awaiting further info)
    | CantConvert FC (Env Term vars) (Term vars) (Term vars)
    | CantSolveEq FC (Env Term vars) (Term vars) (Term vars)
    | PatternVariableUnifies FC (Env Term vars) Name (Term vars)
    | CyclicMeta FC Name
    | WhenUnifying FC (Env Term vars) (Term vars) (Term vars) Error
    | ValidCase FC (Env Term vars) (Either (Term vars) Error)
    | UndefinedName FC Name
    | InvisibleName FC Name (Maybe (List String))
    | BadTypeConType FC Name
    | BadDataConType FC Name Name
    | NotCovering FC Name Covering
    | NotTotal FC Name PartialReason
    | LinearUsed FC Nat Name
    | LinearMisuse FC Name RigCount RigCount
    | BorrowPartial FC (Env Term vars) (Term vars) (Term vars)
    | BorrowPartialType FC (Env Term vars) (Term vars)
    | AmbiguousName FC (List Name)
    | AmbiguousElab FC (Env Term vars) (List (Term vars))
    | AmbiguousSearch FC (Env Term vars) (List (Term vars))
    | AmbiguityTooDeep FC Name (List Name)
    | AllFailed (List (Maybe Name, Error))
    | RecordTypeNeeded FC (Env Term vars)
    | NotRecordField FC String (Maybe Name)
    | NotRecordType FC Name
    | IncompatibleFieldUpdate FC (List String)
    | InvalidImplicits FC (Env Term vars) (List (Maybe Name)) (Term vars)
    | TryWithImplicits FC (Env Term vars) (List (Name, Term vars))
    | BadUnboundImplicit FC (Env Term vars) Name (Term vars)
    | CantSolveGoal FC (Env Term vars) (Term vars)
    | DeterminingArg FC Name Int (Env Term vars) (Term vars)
    | UnsolvedHoles (List (FC, Name))
    | CantInferArgType FC (Env Term vars) Name Name (Term vars)
    | SolvedNamedHole FC (Env Term vars) Name (Term vars)
    | VisibilityError FC Visibility Name Visibility Name
    | NonLinearPattern FC Name
    | BadPattern FC Name
    | NoDeclaration FC Name
    | AlreadyDefined FC Name
    | NotFunctionType FC (Env Term vars) (Term vars)
    | RewriteNoChange FC (Env Term vars) (Term vars) (Term vars)
    | NotRewriteRule FC (Env Term vars) (Term vars)
    | CaseCompile FC Name CaseError
    | MatchTooSpecific FC (Env Term vars) (Term vars)
    | BadDotPattern FC (Env Term vars) DotReason (Term vars) (Term vars)
    | BadImplicit FC String
    | BadRunElab FC (Env Term vars) (Term vars)
    | GenericMsg FC String
    | TTCError TTCErrorMsg
    | FileErr String FileError
    | ParseFail FC ParseError
    | ModuleNotFound FC (List String)
    | CyclicImports (List (List String))
    | ForceNeeded
    | InternalError String

    | InType FC Name Error
    | InCon FC Name Error
    | InLHS FC Name Error
    | InRHS FC Name Error

export
Show TTCErrorMsg where
  show (Format file ver exp) =
    let age = if ver < exp then "older" else "newer" in
        "TTC data is in an " ++ age ++ " format, file: " ++ file ++ ", expected version: " ++ show exp ++ ", actual version: " ++ show ver
  show (EndOfBuffer when) = "End of buffer when reading " ++ when
  show (Corrupt ty) = "Corrupt TTC data for " ++ ty

-- Simplest possible display - higher level languages should unelaborate names
-- and display annotations appropriately
export
Show Error where
  show (Fatal err) = show err
  show (CantConvert fc env x y)
      = show fc ++ ":Type mismatch: " ++ show x ++ " and " ++ show y
  show (CantSolveEq fc env x y)
      = show fc ++ ":" ++ show x ++ " and " ++ show y ++ " are not equal"
  show (PatternVariableUnifies fc env n x)
      = show fc ++ ":Pattern variable " ++ show n ++ " unifies with " ++ show x
  show (CyclicMeta fc n)
      = show fc ++ ":Cycle detected in metavariable solution " ++ show n
  show (WhenUnifying fc _ x y err)
      = show fc ++ ":When unifying: " ++ show x ++ " and " ++ show y ++ "\n\t" ++ show err
  show (ValidCase fc _ prob)
      = show fc ++ ":" ++
           case prob of
             Left tm => assert_total (show tm) ++ " is not a valid impossible pattern because it typechecks"
             Right err => "Not a valid impossible pattern:\n\t" ++ assert_total (show err)
  show (UndefinedName fc x) = show fc ++ ":Undefined name " ++ show x
  show (InvisibleName fc x (Just ns))
       = show fc ++ ":Name " ++ show x ++ " is inaccessible since " ++
         showSep "." (reverse ns) ++ " is not explicitly imported"
  show (InvisibleName fc x _) = show fc ++ ":Name " ++ show x ++ " is private"
  show (BadTypeConType fc n)
       = show fc ++ ":Return type of " ++ show n ++ " must be Type"
  show (BadDataConType fc n fam)
       = show fc ++ ":Return type of " ++ show n ++ " must be in " ++ show fam
  show (NotCovering fc n cov)
       = show fc ++ ":" ++ show n ++ " is not covering:\n\t" ++
            case cov of
                 IsCovering => "Oh yes it is (Internal error!)"
                 MissingCases cs => "Missing cases:\n\t" ++
                                           showSep "\n\t" (map show cs)
                 NonCoveringCall ns => "Calls non covering function"
                                           ++ (case ns of
                                                   [fn] => " " ++ show fn
                                                   _ => "s: " ++ showSep ", " (map show ns))

  show (NotTotal fc n r)
       = show fc ++ ":" ++ show n ++ " is not total"
  show (LinearUsed fc count n)
      = show fc ++ ":There are " ++ show count ++ " uses of linear name " ++ show n
  show (LinearMisuse fc n exp ctx)
      = show fc ++ ":Trying to use " ++ showRig exp ++ " name " ++ show n ++
                   " in " ++ showRel ctx ++ " context"
     where
       showRig : RigCount -> String
       showRig Rig0 = "irrelevant"
       showRig Rig1 = "linear"
       showRig RigW = "unrestricted"

       showRel : RigCount -> String
       showRel Rig0 = "irrelevant"
       showRel Rig1 = "relevant"
       showRel RigW = "non-linear"
  show (BorrowPartial fc env t arg)
      = show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++
                   " so must be fully applied"
  show (BorrowPartialType fc env t)
      = show fc ++ ":" ++ show t ++ " borrows, so must return a concrete type"

  show (AmbiguousName fc ns) = show fc ++ ":Ambiguous name " ++ show ns
  show (AmbiguousElab fc env ts) = show fc ++ ":Ambiguous elaboration " ++ show ts
  show (AmbiguousSearch fc env ts) = show fc ++ ":Ambiguous search " ++ show ts
  show (AmbiguityTooDeep fc n ns)
      = show fc ++ ":Ambiguity too deep in " ++ show n ++ " " ++ show ns
  show (AllFailed ts) = "No successful elaboration: " ++ assert_total (show ts)
  show (RecordTypeNeeded fc env)
      = show fc ++ ":Can't infer type of record to update"
  show (NotRecordField fc fld Nothing)
      = show fc ++ ":" ++ fld ++ " is not part of a record type"
  show (NotRecordField fc fld (Just ty))
      = show fc ++ ":Record type " ++ show ty ++ " has no field " ++ fld
  show (NotRecordType fc ty)
      = show fc ++ ":" ++ show ty ++ " is not a record type"
  show (IncompatibleFieldUpdate fc flds)
      = show fc ++ ":Field update " ++ showSep "->" flds ++ " not compatible with other updates"
  show (InvalidImplicits fc env ns tm)
     = show fc ++ ":" ++ show ns ++ " are not valid implicit arguments in " ++ show tm
  show (TryWithImplicits fc env imps)
     = show fc ++ ":Need to bind implicits "
          ++ showSep "," (map (\x => show (fst x) ++ " : " ++ show (snd x)) imps)
          ++ "\n(The front end should probably have done this for you. Please report!)"
  show (BadUnboundImplicit fc env n ty)
      = show fc ++ ":Can't bind name " ++ nameRoot n ++
                   " with type " ++ show ty
  show (CantSolveGoal fc env g)
      = show fc ++ ":Can't solve goal " ++ assert_total (show g)
  show (DeterminingArg fc n i env g)
      = show fc ++ ":Can't solve goal " ++ assert_total (show g) ++
                " since argument " ++ show n ++ " can't be inferred"
  show (UnsolvedHoles hs) = "Unsolved holes " ++ show hs
  show (CantInferArgType fc env n h ty)
      = show fc ++ ":Can't infer type for " ++ show n ++
                   " (got " ++ show ty ++ " with hole " ++ show h ++ ")"
  show (SolvedNamedHole fc _ h _) = show fc ++ ":Named hole " ++ show h ++ " is solved by unification"
  show (VisibilityError fc vx x vy y)
      = show fc ++ ":" ++ show vx ++ " " ++ show x ++ " cannot refer to "
                       ++ show vy ++ " " ++ show y
  show (NonLinearPattern fc n) = show fc ++ ":Non linear pattern variable " ++ show n
  show (BadPattern fc n) = show fc ++ ":Pattern not allowed here: " ++ show n
  show (NoDeclaration fc x) = show fc ++ ":No type declaration for " ++ show x
  show (AlreadyDefined fc x) = show fc ++ ":" ++ show x ++ " is already defined"
  show (NotFunctionType fc env tm) = show fc ++ ":Not a function type: " ++ show tm
  show (RewriteNoChange fc env rule ty)
      = show fc ++ ":Rewriting by " ++ show rule ++ " did not change type " ++ show ty
  show (NotRewriteRule fc env rule)
      = show fc ++ ":" ++ show rule ++ " is not a rewrite rule type"
  show (CaseCompile fc n DifferingArgNumbers)
      = show fc ++ ":Patterns for " ++ show n ++ " have different numbers of arguments"
  show (CaseCompile fc n DifferingTypes)
      = show fc ++ ":Patterns for " ++ show n ++ " require matching on different types"
  show (CaseCompile fc n UnknownType)
      = show fc ++ ":Can't infer type to match in " ++ show n
  show (CaseCompile fc n (MatchErased (_ ** (env, tm))))
      = show fc ++ ":Attempt to match on erased argument " ++ show tm ++
                   " in " ++ show n
  show (CaseCompile fc n (NotFullyApplied c))
      = show fc ++ ":Constructor " ++ show c ++ " is not fully applied"
  show (MatchTooSpecific fc env tm)
      = show fc ++ ":Can't match on " ++ show tm ++ " as it is has a polymorphic type"
  show (BadDotPattern fc env reason x y)
      = show fc ++ ":Can't match on " ++ show x ++
           " (" ++ show reason ++ ")" ++
           " - it elaborates to " ++ show y
  show (BadImplicit fc str) = show fc ++ ":" ++ str ++ " can't be bound here"
  show (BadRunElab fc env script) = show fc ++ ":Bad elaborator script " ++ show script
  show (GenericMsg fc str) = show fc ++ ":" ++ str
  show (TTCError msg) = "Error in TTC file: " ++ show msg
  show (FileErr fname err) = "File error (" ++ fname ++ "): " ++ show err
  show (ParseFail fc err) = "Parse error (" ++ show err ++ ")"
  show (ModuleNotFound fc ns)
      = show fc ++ ":" ++ showSep "." (reverse ns) ++ " not found"
  show (CyclicImports ns)
      = "Module imports form a cycle: " ++ showSep " -> " (map showMod ns)
    where
      showMod : List String -> String
      showMod ns = showSep "." (reverse ns)
  show ForceNeeded = "Internal error when resolving implicit laziness"
  show (InternalError str) = "INTERNAL ERROR: " ++ str

  show (InType fc n err)
       = show fc ++ ":When elaborating type of " ++ show n ++ ":\n" ++
         show err
  show (InCon fc n err)
       = show fc ++ ":When elaborating type of constructor " ++ show n ++ ":\n" ++
         show err
  show (InLHS fc n err)
       = show fc ++ ":When elaborating left hand side of " ++ show n ++ ":\n" ++
         show err
  show (InRHS fc n err)
       = show fc ++ ":When elaborating right hand side of " ++ show n ++ ":\n" ++
         show err

export
getErrorLoc : Error -> Maybe FC
getErrorLoc (Fatal err) = getErrorLoc err
getErrorLoc (CantConvert loc _ _ _) = Just loc
getErrorLoc (CantSolveEq loc _ _ _) = Just loc
getErrorLoc (PatternVariableUnifies loc _ _ _) = Just loc
getErrorLoc (CyclicMeta loc _) = Just loc
getErrorLoc (WhenUnifying loc _ _ _ _) = Just loc
getErrorLoc (ValidCase loc _ _) = Just loc
getErrorLoc (UndefinedName loc _) = Just loc
getErrorLoc (InvisibleName loc _ _) = Just loc
getErrorLoc (BadTypeConType loc _) = Just loc
getErrorLoc (BadDataConType loc _ _) = Just loc
getErrorLoc (NotCovering loc _ _) = Just loc
getErrorLoc (NotTotal loc _ _) = Just loc
getErrorLoc (LinearUsed loc _ _) = Just loc
getErrorLoc (LinearMisuse loc _ _ _) = Just loc
getErrorLoc (BorrowPartial loc _ _ _) = Just loc
getErrorLoc (BorrowPartialType loc _ _) = Just loc
getErrorLoc (AmbiguousName loc _) = Just loc
getErrorLoc (AmbiguousElab loc _ _) = Just loc
getErrorLoc (AmbiguousSearch loc _ _) = Just loc
getErrorLoc (AmbiguityTooDeep loc _ _) = Just loc
getErrorLoc (AllFailed ((_, x) :: _)) = getErrorLoc x
getErrorLoc (AllFailed []) = Nothing
getErrorLoc (RecordTypeNeeded loc _) = Just loc
getErrorLoc (NotRecordField loc _ _) = Just loc
getErrorLoc (NotRecordType loc _) = Just loc
getErrorLoc (IncompatibleFieldUpdate loc _) = Just loc
getErrorLoc (InvalidImplicits loc _ _ _) = Just loc
getErrorLoc (TryWithImplicits loc _ _) = Just loc
getErrorLoc (BadUnboundImplicit loc _ _ _) = Just loc
getErrorLoc (CantSolveGoal loc _ _) = Just loc
getErrorLoc (DeterminingArg loc _ _ _ _) = Just loc
getErrorLoc (UnsolvedHoles ((loc, _) :: _)) = Just loc
getErrorLoc (UnsolvedHoles []) = Nothing
getErrorLoc (CantInferArgType loc _ _ _ _) = Just loc
getErrorLoc (SolvedNamedHole loc _ _ _) = Just loc
getErrorLoc (VisibilityError loc _ _ _ _) = Just loc
getErrorLoc (NonLinearPattern loc _) = Just loc
getErrorLoc (BadPattern loc _) = Just loc
getErrorLoc (NoDeclaration loc _) = Just loc
getErrorLoc (AlreadyDefined loc _) = Just loc
getErrorLoc (NotFunctionType loc _ _) = Just loc
getErrorLoc (RewriteNoChange loc _ _ _) = Just loc
getErrorLoc (NotRewriteRule loc _ _) = Just loc
getErrorLoc (CaseCompile loc _ _) = Just loc
getErrorLoc (MatchTooSpecific loc _ _) = Just loc
getErrorLoc (BadDotPattern loc _ _ _ _) = Just loc
getErrorLoc (BadImplicit loc _) = Just loc
getErrorLoc (BadRunElab loc _ _) = Just loc
getErrorLoc (GenericMsg loc _) = Just loc
getErrorLoc (TTCError _) = Nothing
getErrorLoc (FileErr _ _) = Nothing
getErrorLoc (ParseFail loc _) = Just loc
getErrorLoc (ModuleNotFound loc _) = Just loc
getErrorLoc (CyclicImports _) = Nothing
getErrorLoc ForceNeeded = Nothing
getErrorLoc (InternalError _) = Nothing
getErrorLoc (InType _ _ err) = getErrorLoc err
getErrorLoc (InCon _ _ err) = getErrorLoc err
getErrorLoc (InLHS _ _ err) = getErrorLoc err
getErrorLoc (InRHS _ _ err) = getErrorLoc err

-- Core is a wrapper around IO that is specialised for efficiency.
export
record Core t where
  constructor MkCore
  runCore : IO (Either Error t)

export
coreRun : Core a ->
          (Error -> IO b) -> (a -> IO b) -> IO b
coreRun (MkCore act) err ok
    = either err ok !act

export
coreFail : Error -> Core a
coreFail e = MkCore (pure (Left e))

export
wrapError : (Error -> Error) -> Core a -> Core a
wrapError fe (MkCore prog)
    = MkCore (prog >>=
                 (\x => case x of
                             Left err => pure (Left (fe err))
                             Right val => pure (Right val)))

-- This would be better if we restrict it to a limited set of IO operations
export
%inline
coreLift : IO a -> Core a
coreLift op = MkCore (do op' <- op
                         pure (Right op'))

{- Monad, Applicative, Traversable are specialised by hand for Core.
In theory, this shouldn't be necessary, but it turns out that Idris 1 doesn't
specialise interfaces under 'case' expressions, and this has a significant
impact on both compile time and run time.

Of course it would be a good idea to fix this in Idris, but it's not an urgent
thing on the road to self hosting, and we can make sure this isn't a problem
in the next version (i.e., in this project...)! -}

-- Functor (specialised)
export %inline
map : (a -> b) -> Core a -> Core b
map f (MkCore a) = MkCore (map (map f) a)

export %inline
(<$>) : (a -> b) -> Core a -> Core b
(<$>) f (MkCore a) = MkCore (map (map f) a)

-- Monad (specialised)
export %inline
(>>=) : Core a -> (a -> Core b) -> Core b
(>>=) (MkCore act) f
    = MkCore (act >>=
                   (\x => case x of
                               Left err => pure (Left err)
                               Right val => runCore (f val)))

-- Applicative (specialised)
export %inline
pure : a -> Core a
pure x = MkCore (pure (pure x))

export
(<*>) : Core (a -> b) -> Core a -> Core b
(<*>) (MkCore f) (MkCore a) = MkCore [| f <*> a |]

export %inline
when : Bool -> Lazy (Core ()) -> Core ()
when True f = f
when False f = pure ()

export
Catchable Core Error where
  catch (MkCore prog) h
      = MkCore ( do p' <- prog
                    case p' of
                         Left e => let MkCore he = h e in he
                         Right val => pure (Right val))
  throw = coreFail

-- Traversable (specialised)
traverse' : (a -> Core b) -> List a -> List b -> Core (List b)
traverse' f [] acc = pure (reverse acc)
traverse' f (x :: xs) acc
    = traverse' f xs (!(f x) :: acc)

export
traverse : (a -> Core b) -> List a -> Core (List b)
traverse f xs = traverse' f xs []

export
traverseVect : (a -> Core b) -> Vect n a -> Core (Vect n b)
traverseVect f [] = pure []
traverseVect f (x :: xs) = [| f x :: traverseVect f xs |]

export
traverseOpt : (a -> Core b) -> Maybe a -> Core (Maybe b)
traverseOpt f Nothing = pure Nothing
traverseOpt f (Just x) = map Just (f x)

export
traverse_ : (a -> Core b) -> List a -> Core ()
traverse_ f [] = pure ()
traverse_ f (x :: xs)
    = do f x
         traverse_ f xs

namespace PiInfo
  export
  traverse : (a -> Core b) -> PiInfo a -> Core (PiInfo b)
  traverse f Explicit = pure Explicit
  traverse f Implicit = pure Implicit
  traverse f AutoImplicit = pure AutoImplicit
  traverse f (DefImplicit t) = pure (DefImplicit !(f t))

namespace Binder
  export
  traverse : (a -> Core b) -> Binder a -> Core (Binder b)
  traverse f (Lam c p ty) = pure $ Lam c !(traverse f p) !(f ty)
  traverse f (Let c val ty) = pure $ Let c !(f val) !(f ty)
  traverse f (Pi c p ty) = pure $ Pi c !(traverse f p) !(f ty)
  traverse f (PVar c p ty) = pure $ PVar c !(traverse f p) !(f ty)
  traverse f (PLet c val ty) = pure $ PLet c !(f val) !(f ty)
  traverse f (PVTy c ty) = pure $ PVTy c !(f ty)

export
anyM : (a -> Core Bool) -> List a -> Core Bool
anyM f [] = pure False
anyM f (x :: xs)
    = if !(f x)
         then pure True
         else anyM f xs

export
allM : (a -> Core Bool) -> List a -> Core Bool
allM f [] = pure True
allM f (x :: xs)
    = if !(f x)
         then allM f xs
         else pure False

export
filterM : (a -> Core Bool) -> List a -> Core (List a)
filterM p [] = pure []
filterM p (x :: xs)
    = if !(p x)
         then do xs' <- filterM p xs
                 pure (x :: xs')
         else filterM p xs

export
data Ref : label -> Type -> Type where
	   MkRef : IORef a -> Ref x a

export
newRef : (x : label) -> t -> Core (Ref x t)
newRef x val
    = do ref <- coreLift (newIORef val)
         pure (MkRef ref)

export %inline
get : (x : label) -> {auto ref : Ref x a} -> Core a
get x {ref = MkRef io} = coreLift (readIORef io)

export %inline
put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
put x {ref = MkRef io} val = coreLift (writeIORef io val)

export
cond : List (Lazy Bool, Lazy a) -> a -> a
cond [] def = def
cond ((x, y) :: xs) def = if x then y else cond xs def

export
condC : List (Core Bool, Core a) -> Core a -> Core a
condC [] def = def
condC ((x, y) :: xs) def
    = if !x then y else condC xs def

max_stars_repo_name: tolvanea/yarra-valley

max_issues_repo_name: tolvanea/yarra-valley

max_forks_repo_name: tolvanea/yarra-valley


text:
occurences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurences item [] = 0
occurences item (value :: values) = case value == item of
                                        False => occurences item values
                                        True => 1 + occurences item values

data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

Eq elem => Eq (Tree elem) where
    (==) Empty Empty = True
    (==) (Node left el right) (Node left' el' right') =
        left == left' && el == el' && right == right'
    (==) _ _ = False

Functor Tree where
    map func Empty = Empty
    map func (Node left el right) =
        Node (map func left) (func el) (map func right)

Foldable Tree where
    foldr func acc Empty = acc
    foldr func acc (Node left el right) =
        let leftFold = foldr func acc left
            rightFold = foldr func leftFold right in
            func el rightFold

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

Eq Shape where
    (==) (Triangle x z) (Triangle y w) = x == y && z == w
    (==) (Rectangle x z) (Rectangle y w) = x == y && z == w
    (==) (Circle x) (Circle y) = x == y
    (==) _ _ = False

area : Shape -> Double
area (Triangle x y) = x * y * 0.5
area (Rectangle x y) = x * y
area (Circle x) = x * x * pi

Ord Shape where
    compare x y = compare (area x) (area y)

testShapes : List Shape
testShapes = [
    Circle 3,
    Triangle 3 9,
    Rectangle 2 6,
    Circle 4,
    Rectangle 2 7
]

ext: idr


text:
module Testlib1

export
val1 : String
val1 = "Hello, Idris!"

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
module Main
import Effects
import Effect.StdIO

hello : Eff () [STDIO]
hello = putStrLn “Hello world!”

main : IO ()
main = run hello

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Dot

import Graph.Core
import Graph.API

-- %default total

data Kind = Undirected | Directed

data Attribute : Type where
  Color : String -> Attribute
  Label : String -> Attribute

data EdgeDef : (kind : Kind) -> Type where
  SimpleEdge : (target : String) -> (source : String) -> EdgeDef kind
  (::) : String -> EdgeDef kind -> EdgeDef kind

data Statement : (kind : Kind) -> Type where
  Node : String -> List Attribute -> Statement kind
  Edge : EdgeDef kind -> List Attribute -> Statement kind

record Dot (kind : Kind) where
  constructor MkDot
  strict : Bool
  id : Maybe String
  body : List (Statement kind)

Show Kind where
  show Undirected = "graph"
  show Directed = "digraph"

Show Attribute where
  show (Color col) = "color=" ++ col
  show (Label lab) = "label=" ++ lab

edgeConnector : Kind -> String
edgeConnector Undirected = "--"
edgeConnector Directed = "->"

Show (EdgeDef kind) where
  show (SimpleEdge target source) = unwords [source, edgeConnector kind, target]
  show (target :: def) = unwords [show def, edgeConnector kind, target]

appendAttrs : List Attribute -> String -> String
appendAttrs [] str = str
appendAttrs attrs str = str ++ (" [" ++ tags ++ "]") where
  tags = unwords (map show attrs)

Show (Statement kind) where
  show (Node node attrs) = appendAttrs attrs (node)
  show (Edge def attrs) = appendAttrs attrs (show def)

showDeclaration : Dot kind -> String
showDeclaration dot = unwords . putStrict . putKind . putId $ [] where
  putKind : List String -> List String
  putKind ws = (show kind) :: ws
  putId : List String -> List String
  putId ws = case id dot of
                  Nothing => ws
                  Just identifier => identifier :: ws
  putStrict : List String -> List String
  putStrict ws = if strict dot then "strict" :: ws else ws

showBody : Dot kind -> String
showBody dot = unlines (map show (body dot))

Show (Dot kind) where
  show dot = showDeclaration dot ++ " {\n" ++ showBody dot ++ "\n}"

test : Dot Directed
test = MkDot True (Just "yo") [
  Node "a" [],
  Node "b" [],
  Edge (SimpleEdge "a" "b") []
  ]

fromGraph : (Show a, Show b) => Graph a b -> Dot Directed
fromGraph graph = MkDot False Nothing (nodes ++ edges) where
  nodes : List (Statement Directed)
  nodes = map (\(id, l) => Node (show id) [Label (show l)]) (labNodes graph)
  edges : List (Statement Directed)
  edges = map f (labEdges graph) where
    f : Show b => (Int, Int, b) -> Statement Directed
    f (source, target, l)
      = Edge (SimpleEdge (show target) (show source)) [Label (show l)]

export
graphToDot : (Show a, Show b) => Graph a b -> String
graphToDot = show . fromGraph

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
module Specdris.Data.SpecResult

import Specdris.Data.ConsoleColor
import Specdris.Data.SpecState

%access export
%default total

||| Result of a single `Expectation`s or `Pending` if none
||| exists.
public export
data SpecResult : Type where
     Pending : (message : Maybe String) -> SpecResult

     Success : SpecResult

     UnaryFailure : Show a => (val : a) -> (reason : String) -> SpecResult
     BinaryFailure : (Show a, Show b) => (left : a) -> (right : b) -> (reason : String) -> SpecResult

Eq SpecResult where
  (==) (Pending aMsg) (Pending bMsg)                           = aMsg == bMsg
  (==) Success Success                                         = True
  (==) (UnaryFailure _ aReason) (UnaryFailure _ bReason)       = aReason == bReason
  (==) (BinaryFailure _ _ aReason) (BinaryFailure _ _ bReason) = aReason == bReason
  (==) _ _ = False

private
show : SpecResult -> (level : Nat) -> String
show (Pending message) _ = case message of
                             (Just msg) => " [] pending: " ++ msg
                             Nothing    => " [] pending"
show Success _ = ""
show (UnaryFailure actual reason) level           = " [x] " ++ reason ++
                                                    "\n     " ++ indent(level) ++ "actual: " ++ show actual
show (BinaryFailure actual expected reason) level = " [x] " ++ reason ++
                                                    "\n     " ++ indent(level) ++ "actual:   " ++ show actual ++
                                                    "\n     " ++ indent(level) ++ "expected: " ++ show expected

namespace SpecResultDo
  (>>=) : SpecResult -> (SpecResult -> SpecResult) -> SpecResult
  (>>=) (UnaryFailure actual reason) _           = (UnaryFailure actual reason)
  (>>=) (BinaryFailure actual expected reason) _ = (BinaryFailure actual expected reason)
  (>>=) result f                                 = f result

private
handleOutput : String -> SpecState -> (storeOutput : Bool) -> IO' ffi SpecState
handleOutput output state store = if store then
                                    pure $ addLine output state
                                  else do
                                    putStrLn' output
                                    pure state

{- Evaluates a given expectation result in updates the `SpecState` accordingly:
     - `Success` : increase spec count
     - `Failure` : increase spec and failure count
     - `Pending` : encrease spec and pending count
   Furthermore it prints the result to console if `storeOutput == False`.
 -}
evalResult : SpecResult -> SpecState -> (storeOutput : Bool) -> (level : Nat) -> IO' ffi SpecState
evalResult r@(Pending msg) state store level = let output = format (show r $ level + 1) Yellow (level + 1) in
                                                   pure $ addPending !(handleOutput output state store)

evalResult Success state _ _ = pure $ addSpec state
evalResult r@(UnaryFailure a reason) state store level    = let output = format (show r $ level + 1) Red (level + 1) in
                                                                pure $ addFailure !(handleOutput output state store)

evalResult r@(BinaryFailure a b reason) state store level = let output = format (show r $ level + 1) Red (level + 1) in
                                                                pure $ addFailure !(handleOutput output state store)

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Web.Raw.UIEvents

import JS
import Web.Internal.UIEventsPrim
import Web.Internal.Types

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

namespace CompositionEvent

  export
  data_ : (obj : CompositionEvent) -> JSIO String
  data_ a = primJS $ CompositionEvent.prim__data a

namespace FocusEvent

  export
  relatedTarget : (obj : FocusEvent) -> JSIO (Maybe EventTarget)
  relatedTarget a = tryJS "FocusEvent.relatedTarget"
                  $ FocusEvent.prim__relatedTarget a

namespace InputEvent

  export
  data_ : (obj : InputEvent) -> JSIO (Maybe String)
  data_ a = tryJS "InputEvent.data_" $ InputEvent.prim__data a

  export
  inputType : (obj : InputEvent) -> JSIO String
  inputType a = primJS $ InputEvent.prim__inputType a

  export
  isComposing : (obj : InputEvent) -> JSIO Bool
  isComposing a = tryJS "InputEvent.isComposing"
                $ InputEvent.prim__isComposing a

namespace KeyboardEvent

  public export
  DOM_KEY_LOCATION_LEFT : Bits32
  DOM_KEY_LOCATION_LEFT = 0x1

  public export
  DOM_KEY_LOCATION_NUMPAD : Bits32
  DOM_KEY_LOCATION_NUMPAD = 0x3

  public export
  DOM_KEY_LOCATION_RIGHT : Bits32
  DOM_KEY_LOCATION_RIGHT = 0x2

  public export
  DOM_KEY_LOCATION_STANDARD : Bits32
  DOM_KEY_LOCATION_STANDARD = 0x0

  export
  altKey : (obj : KeyboardEvent) -> JSIO Bool
  altKey a = tryJS "KeyboardEvent.altKey" $ KeyboardEvent.prim__altKey a

  export
  charCode : (obj : KeyboardEvent) -> JSIO Bits32
  charCode a = primJS $ KeyboardEvent.prim__charCode a

  export
  code : (obj : KeyboardEvent) -> JSIO String
  code a = primJS $ KeyboardEvent.prim__code a

  export
  ctrlKey : (obj : KeyboardEvent) -> JSIO Bool
  ctrlKey a = tryJS "KeyboardEvent.ctrlKey" $ KeyboardEvent.prim__ctrlKey a

  export
  isComposing : (obj : KeyboardEvent) -> JSIO Bool
  isComposing a = tryJS "KeyboardEvent.isComposing"
                $ KeyboardEvent.prim__isComposing a

  export
  key : (obj : KeyboardEvent) -> JSIO String
  key a = primJS $ KeyboardEvent.prim__key a

  export
  keyCode : (obj : KeyboardEvent) -> JSIO Bits32
  keyCode a = primJS $ KeyboardEvent.prim__keyCode a

  export
  location : (obj : KeyboardEvent) -> JSIO Bits32
  location a = primJS $ KeyboardEvent.prim__location a

  export
  metaKey : (obj : KeyboardEvent) -> JSIO Bool
  metaKey a = tryJS "KeyboardEvent.metaKey" $ KeyboardEvent.prim__metaKey a

  export
  repeat : (obj : KeyboardEvent) -> JSIO Bool
  repeat a = tryJS "KeyboardEvent.repeat" $ KeyboardEvent.prim__repeat a

  export
  shiftKey : (obj : KeyboardEvent) -> JSIO Bool
  shiftKey a = tryJS "KeyboardEvent.shiftKey" $ KeyboardEvent.prim__shiftKey a

  export
  getModifierState : (obj : KeyboardEvent) -> (keyArg : String) -> JSIO Bool
  getModifierState a b = tryJS "KeyboardEvent.getModifierState"
                       $ KeyboardEvent.prim__getModifierState a b

namespace MouseEvent

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

  export
  button :  (0 _ : JSType t1)
         => {auto 0 _ : Elem MouseEvent (Types t1)}
         -> (obj : t1)
         -> JSIO Int16
  button a = primJS $ MouseEvent.prim__button (up a)

  export
  buttons :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MouseEvent (Types t1)}
          -> (obj : t1)
          -> JSIO Bits16
  buttons a = primJS $ MouseEvent.prim__buttons (up a)

  export
  clientX :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MouseEvent (Types t1)}
          -> (obj : t1)
          -> JSIO Int32
  clientX a = primJS $ MouseEvent.prim__clientX (up a)

  export
  clientY :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MouseEvent (Types t1)}
          -> (obj : t1)
          -> JSIO Int32
  clientY a = primJS $ MouseEvent.prim__clientY (up a)

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

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

  export
  relatedTarget :  (0 _ : JSType t1)
                => {auto 0 _ : Elem MouseEvent (Types t1)}
                -> (obj : t1)
                -> JSIO (Maybe EventTarget)
  relatedTarget a = tryJS "MouseEvent.relatedTarget"
                  $ MouseEvent.prim__relatedTarget (up a)

  export
  screenX :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MouseEvent (Types t1)}
          -> (obj : t1)
          -> JSIO Int32
  screenX a = primJS $ MouseEvent.prim__screenX (up a)

  export
  screenY :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MouseEvent (Types t1)}
          -> (obj : t1)
          -> JSIO Int32
  screenY a = primJS $ MouseEvent.prim__screenY (up a)

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

  export
  getModifierState :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem MouseEvent (Types t1)}
                   -> (obj : t1)
                   -> (keyArg : String)
                   -> JSIO Bool
  getModifierState a b = tryJS "MouseEvent.getModifierState"
                       $ MouseEvent.prim__getModifierState (up a) b

namespace UIEvent

  export
  detail :  (0 _ : JSType t1)
         => {auto 0 _ : Elem UIEvent (Types t1)}
         -> (obj : t1)
         -> JSIO Int32
  detail a = primJS $ UIEvent.prim__detail (up a)

  export
  view :  (0 _ : JSType t1)
       => {auto 0 _ : Elem UIEvent (Types t1)}
       -> (obj : t1)
       -> JSIO (Maybe Window)
  view a = tryJS "UIEvent.view" $ UIEvent.prim__view (up a)

  export
  which :  (0 _ : JSType t1)
        => {auto 0 _ : Elem UIEvent (Types t1)}
        -> (obj : t1)
        -> JSIO Bits32
  which a = primJS $ UIEvent.prim__which (up a)

namespace WheelEvent

  public export
  DOM_DELTA_LINE : Bits32
  DOM_DELTA_LINE = 0x1

  public export
  DOM_DELTA_PAGE : Bits32
  DOM_DELTA_PAGE = 0x2

  public export
  DOM_DELTA_PIXEL : Bits32
  DOM_DELTA_PIXEL = 0x0

  export
  deltaMode : (obj : WheelEvent) -> JSIO Bits32
  deltaMode a = primJS $ WheelEvent.prim__deltaMode a

  export
  deltaX : (obj : WheelEvent) -> JSIO Double
  deltaX a = primJS $ WheelEvent.prim__deltaX a

  export
  deltaY : (obj : WheelEvent) -> JSIO Double
  deltaY a = primJS $ WheelEvent.prim__deltaY a

  export
  deltaZ : (obj : WheelEvent) -> JSIO Double
  deltaZ a = primJS $ WheelEvent.prim__deltaZ a

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

namespace CompositionEventInit

  export
  new : (data_ : Optional String) -> JSIO CompositionEventInit
  new a = primJS $ CompositionEventInit.prim__new (toFFI a)

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

  export
  data_ :  (0 _ : JSType t)
        => {auto 0 _ : Elem CompositionEventInit (Types t)}
        -> t
        -> Attribute True Optional String
  data_ v = fromUndefOrPrim "CompositionEventInit.getdata"
                            prim__data
                            prim__setData
                            ""
                            (v :> CompositionEventInit)

namespace EventModifierInit

  export
  new :  (ctrlKey : Optional Bool)
      -> (shiftKey : Optional Bool)
      -> (altKey : Optional Bool)
      -> (metaKey : Optional Bool)
      -> (modifierAltGraph : Optional Bool)
      -> (modifierCapsLock : Optional Bool)
      -> (modifierFn : Optional Bool)
      -> (modifierFnLock : Optional Bool)
      -> (modifierHyper : Optional Bool)
      -> (modifierNumLock : Optional Bool)
      -> (modifierScrollLock : Optional Bool)
      -> (modifierSuper : Optional Bool)
      -> (modifierSymbol : Optional Bool)
      -> (modifierSymbolLock : Optional Bool)
      -> JSIO EventModifierInit
  new a b c d e f g h i j k l m n = primJS
                                  $ EventModifierInit.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)
                                                                (toFFI n)

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

  export
  altKey :  (0 _ : JSType t)
         => {auto 0 _ : Elem EventModifierInit (Types t)}
         -> t
         -> Attribute True Optional Bool
  altKey v = fromUndefOrPrim "EventModifierInit.getaltKey"
                             prim__altKey
                             prim__setAltKey
                             False
                             (v :> EventModifierInit)

  export
  ctrlKey :  (0 _ : JSType t)
          => {auto 0 _ : Elem EventModifierInit (Types t)}
          -> t
          -> Attribute True Optional Bool
  ctrlKey v = fromUndefOrPrim "EventModifierInit.getctrlKey"
                              prim__ctrlKey
                              prim__setCtrlKey
                              False
                              (v :> EventModifierInit)

  export
  metaKey :  (0 _ : JSType t)
          => {auto 0 _ : Elem EventModifierInit (Types t)}
          -> t
          -> Attribute True Optional Bool
  metaKey v = fromUndefOrPrim "EventModifierInit.getmetaKey"
                              prim__metaKey
                              prim__setMetaKey
                              False
                              (v :> EventModifierInit)

  export
  modifierAltGraph :  (0 _ : JSType t)
                   => {auto 0 _ : Elem EventModifierInit (Types t)}
                   -> t
                   -> Attribute True Optional Bool
  modifierAltGraph v = fromUndefOrPrim "EventModifierInit.getmodifierAltGraph"
                                       prim__modifierAltGraph
                                       prim__setModifierAltGraph
                                       False
                                       (v :> EventModifierInit)

  export
  modifierCapsLock :  (0 _ : JSType t)
                   => {auto 0 _ : Elem EventModifierInit (Types t)}
                   -> t
                   -> Attribute True Optional Bool
  modifierCapsLock v = fromUndefOrPrim "EventModifierInit.getmodifierCapsLock"
                                       prim__modifierCapsLock
                                       prim__setModifierCapsLock
                                       False
                                       (v :> EventModifierInit)

  export
  modifierFn :  (0 _ : JSType t)
             => {auto 0 _ : Elem EventModifierInit (Types t)}
             -> t
             -> Attribute True Optional Bool
  modifierFn v = fromUndefOrPrim "EventModifierInit.getmodifierFn"
                                 prim__modifierFn
                                 prim__setModifierFn
                                 False
                                 (v :> EventModifierInit)

  export
  modifierFnLock :  (0 _ : JSType t)
                 => {auto 0 _ : Elem EventModifierInit (Types t)}
                 -> t
                 -> Attribute True Optional Bool
  modifierFnLock v = fromUndefOrPrim "EventModifierInit.getmodifierFnLock"
                                     prim__modifierFnLock
                                     prim__setModifierFnLock
                                     False
                                     (v :> EventModifierInit)

  export
  modifierHyper :  (0 _ : JSType t)
                => {auto 0 _ : Elem EventModifierInit (Types t)}
                -> t
                -> Attribute True Optional Bool
  modifierHyper v = fromUndefOrPrim "EventModifierInit.getmodifierHyper"
                                    prim__modifierHyper
                                    prim__setModifierHyper
                                    False
                                    (v :> EventModifierInit)

  export
  modifierNumLock :  (0 _ : JSType t)
                  => {auto 0 _ : Elem EventModifierInit (Types t)}
                  -> t
                  -> Attribute True Optional Bool
  modifierNumLock v = fromUndefOrPrim "EventModifierInit.getmodifierNumLock"
                                      prim__modifierNumLock
                                      prim__setModifierNumLock
                                      False
                                      (v :> EventModifierInit)

  export
  modifierScrollLock :  (0 _ : JSType t)
                     => {auto 0 _ : Elem EventModifierInit (Types t)}
                     -> t
                     -> Attribute True Optional Bool
  modifierScrollLock v = fromUndefOrPrim "EventModifierInit.getmodifierScrollLock"
                                         prim__modifierScrollLock
                                         prim__setModifierScrollLock
                                         False
                                         (v :> EventModifierInit)

  export
  modifierSuper :  (0 _ : JSType t)
                => {auto 0 _ : Elem EventModifierInit (Types t)}
                -> t
                -> Attribute True Optional Bool
  modifierSuper v = fromUndefOrPrim "EventModifierInit.getmodifierSuper"
                                    prim__modifierSuper
                                    prim__setModifierSuper
                                    False
                                    (v :> EventModifierInit)

  export
  modifierSymbol :  (0 _ : JSType t)
                 => {auto 0 _ : Elem EventModifierInit (Types t)}
                 -> t
                 -> Attribute True Optional Bool
  modifierSymbol v = fromUndefOrPrim "EventModifierInit.getmodifierSymbol"
                                     prim__modifierSymbol
                                     prim__setModifierSymbol
                                     False
                                     (v :> EventModifierInit)

  export
  modifierSymbolLock :  (0 _ : JSType t)
                     => {auto 0 _ : Elem EventModifierInit (Types t)}
                     -> t
                     -> Attribute True Optional Bool
  modifierSymbolLock v = fromUndefOrPrim "EventModifierInit.getmodifierSymbolLock"
                                         prim__modifierSymbolLock
                                         prim__setModifierSymbolLock
                                         False
                                         (v :> EventModifierInit)

  export
  shiftKey :  (0 _ : JSType t)
           => {auto 0 _ : Elem EventModifierInit (Types t)}
           -> t
           -> Attribute True Optional Bool
  shiftKey v = fromUndefOrPrim "EventModifierInit.getshiftKey"
                               prim__shiftKey
                               prim__setShiftKey
                               False
                               (v :> EventModifierInit)

namespace FocusEventInit

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem EventTarget (Types t1)}
      -> (relatedTarget : Optional (Maybe t1))
      -> JSIO FocusEventInit
  new a = primJS $ FocusEventInit.prim__new (omyUp a)

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

  export
  relatedTarget :  (0 _ : JSType t)
                => {auto 0 _ : Elem FocusEventInit (Types t)}
                -> t
                -> Attribute True Optional (Maybe EventTarget)
  relatedTarget v = fromUndefOrPrim "FocusEventInit.getrelatedTarget"
                                    prim__relatedTarget
                                    prim__setRelatedTarget
                                    Nothing
                                    (v :> FocusEventInit)

namespace InputEventInit

  export
  new :  (data_ : Optional (Maybe String))
      -> (isComposing : Optional Bool)
      -> (inputType : Optional String)
      -> JSIO InputEventInit
  new a b c = primJS $ InputEventInit.prim__new (toFFI a) (toFFI b) (toFFI c)

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

  export
  data_ :  (0 _ : JSType t)
        => {auto 0 _ : Elem InputEventInit (Types t)}
        -> t
        -> Attribute True Optional (Maybe String)
  data_ v = fromUndefOrPrim "InputEventInit.getdata"
                            prim__data
                            prim__setData
                            (Just "")
                            (v :> InputEventInit)

  export
  inputType :  (0 _ : JSType t)
            => {auto 0 _ : Elem InputEventInit (Types t)}
            -> t
            -> Attribute True Optional String
  inputType v = fromUndefOrPrim "InputEventInit.getinputType"
                                prim__inputType
                                prim__setInputType
                                ""
                                (v :> InputEventInit)

  export
  isComposing :  (0 _ : JSType t)
              => {auto 0 _ : Elem InputEventInit (Types t)}
              -> t
              -> Attribute True Optional Bool
  isComposing v = fromUndefOrPrim "InputEventInit.getisComposing"
                                  prim__isComposing
                                  prim__setIsComposing
                                  False
                                  (v :> InputEventInit)

namespace KeyboardEventInit

  export
  new :  (key : Optional String)
      -> (code : Optional String)
      -> (location : Optional Bits32)
      -> (repeat : Optional Bool)
      -> (isComposing : Optional Bool)
      -> JSIO KeyboardEventInit
  new a b c d e = primJS
                $ KeyboardEventInit.prim__new (toFFI a)
                                              (toFFI b)
                                              (toFFI c)
                                              (toFFI d)
                                              (toFFI e)

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

  export
  code :  (0 _ : JSType t)
       => {auto 0 _ : Elem KeyboardEventInit (Types t)}
       -> t
       -> Attribute True Optional String
  code v = fromUndefOrPrim "KeyboardEventInit.getcode"
                           prim__code
                           prim__setCode
                           ""
                           (v :> KeyboardEventInit)

  export
  isComposing :  (0 _ : JSType t)
              => {auto 0 _ : Elem KeyboardEventInit (Types t)}
              -> t
              -> Attribute True Optional Bool
  isComposing v = fromUndefOrPrim "KeyboardEventInit.getisComposing"
                                  prim__isComposing
                                  prim__setIsComposing
                                  False
                                  (v :> KeyboardEventInit)

  export
  key :  (0 _ : JSType t)
      => {auto 0 _ : Elem KeyboardEventInit (Types t)}
      -> t
      -> Attribute True Optional String
  key v = fromUndefOrPrim "KeyboardEventInit.getkey"
                          prim__key
                          prim__setKey
                          ""
                          (v :> KeyboardEventInit)

  export
  location :  (0 _ : JSType t)
           => {auto 0 _ : Elem KeyboardEventInit (Types t)}
           -> t
           -> Attribute True Optional Bits32
  location v = fromUndefOrPrim "KeyboardEventInit.getlocation"
                               prim__location
                               prim__setLocation
                               0
                               (v :> KeyboardEventInit)

  export
  repeat :  (0 _ : JSType t)
         => {auto 0 _ : Elem KeyboardEventInit (Types t)}
         -> t
         -> Attribute True Optional Bool
  repeat v = fromUndefOrPrim "KeyboardEventInit.getrepeat"
                             prim__repeat
                             prim__setRepeat
                             False
                             (v :> KeyboardEventInit)

namespace MouseEventInit

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem EventTarget (Types t1)}
      -> (screenX : Optional Int32)
      -> (screenY : Optional Int32)
      -> (clientX : Optional Int32)
      -> (clientY : Optional Int32)
      -> (button : Optional Int16)
      -> (buttons : Optional Bits16)
      -> (relatedTarget : Optional (Maybe t1))
      -> JSIO MouseEventInit
  new a b c d e f g = primJS
                    $ MouseEventInit.prim__new (toFFI a)
                                               (toFFI b)
                                               (toFFI c)
                                               (toFFI d)
                                               (toFFI e)
                                               (toFFI f)
                                               (omyUp g)

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

  export
  button :  (0 _ : JSType t)
         => {auto 0 _ : Elem MouseEventInit (Types t)}
         -> t
         -> Attribute True Optional Int16
  button v = fromUndefOrPrim "MouseEventInit.getbutton"
                             prim__button
                             prim__setButton
                             0
                             (v :> MouseEventInit)

  export
  buttons :  (0 _ : JSType t)
          => {auto 0 _ : Elem MouseEventInit (Types t)}
          -> t
          -> Attribute True Optional Bits16
  buttons v = fromUndefOrPrim "MouseEventInit.getbuttons"
                              prim__buttons
                              prim__setButtons
                              0
                              (v :> MouseEventInit)

  export
  clientX :  (0 _ : JSType t)
          => {auto 0 _ : Elem MouseEventInit (Types t)}
          -> t
          -> Attribute True Optional Int32
  clientX v = fromUndefOrPrim "MouseEventInit.getclientX"
                              prim__clientX
                              prim__setClientX
                              0
                              (v :> MouseEventInit)

  export
  clientY :  (0 _ : JSType t)
          => {auto 0 _ : Elem MouseEventInit (Types t)}
          -> t
          -> Attribute True Optional Int32
  clientY v = fromUndefOrPrim "MouseEventInit.getclientY"
                              prim__clientY
                              prim__setClientY
                              0
                              (v :> MouseEventInit)

  export
  relatedTarget :  (0 _ : JSType t)
                => {auto 0 _ : Elem MouseEventInit (Types t)}
                -> t
                -> Attribute True Optional (Maybe EventTarget)
  relatedTarget v = fromUndefOrPrim "MouseEventInit.getrelatedTarget"
                                    prim__relatedTarget
                                    prim__setRelatedTarget
                                    Nothing
                                    (v :> MouseEventInit)

  export
  screenX :  (0 _ : JSType t)
          => {auto 0 _ : Elem MouseEventInit (Types t)}
          -> t
          -> Attribute True Optional Int32
  screenX v = fromUndefOrPrim "MouseEventInit.getscreenX"
                              prim__screenX
                              prim__setScreenX
                              0
                              (v :> MouseEventInit)

  export
  screenY :  (0 _ : JSType t)
          => {auto 0 _ : Elem MouseEventInit (Types t)}
          -> t
          -> Attribute True Optional Int32
  screenY v = fromUndefOrPrim "MouseEventInit.getscreenY"
                              prim__screenY
                              prim__setScreenY
                              0
                              (v :> MouseEventInit)

namespace UIEventInit

  export
  new :  (view : Optional (Maybe Window))
      -> (detail : Optional Int32)
      -> JSIO UIEventInit
  new a b = primJS $ UIEventInit.prim__new (toFFI a) (toFFI b)

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

  export
  detail :  (0 _ : JSType t)
         => {auto 0 _ : Elem UIEventInit (Types t)}
         -> t
         -> Attribute True Optional Int32
  detail v = fromUndefOrPrim "UIEventInit.getdetail"
                             prim__detail
                             prim__setDetail
                             0
                             (v :> UIEventInit)

  export
  view :  (0 _ : JSType t)
       => {auto 0 _ : Elem UIEventInit (Types t)}
       -> t
       -> Attribute True Optional (Maybe Window)
  view v = fromUndefOrPrim "UIEventInit.getview"
                           prim__view
                           prim__setView
                           Nothing
                           (v :> UIEventInit)

namespace WheelEventInit

  export
  new :  (deltaX : Optional Double)
      -> (deltaY : Optional Double)
      -> (deltaZ : Optional Double)
      -> (deltaMode : Optional Bits32)
      -> JSIO WheelEventInit
  new a b c d = primJS
              $ WheelEventInit.prim__new (toFFI a) (toFFI b) (toFFI c) (toFFI d)

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

  export
  deltaMode :  (0 _ : JSType t)
            => {auto 0 _ : Elem WheelEventInit (Types t)}
            -> t
            -> Attribute True Optional Bits32
  deltaMode v = fromUndefOrPrim "WheelEventInit.getdeltaMode"
                                prim__deltaMode
                                prim__setDeltaMode
                                0
                                (v :> WheelEventInit)

  export
  deltaX :  (0 _ : JSType t)
         => {auto 0 _ : Elem WheelEventInit (Types t)}
         -> t
         -> Attribute True Optional Double
  deltaX v = fromUndefOrPrim "WheelEventInit.getdeltaX"
                             prim__deltaX
                             prim__setDeltaX
                             0.0
                             (v :> WheelEventInit)

  export
  deltaY :  (0 _ : JSType t)
         => {auto 0 _ : Elem WheelEventInit (Types t)}
         -> t
         -> Attribute True Optional Double
  deltaY v = fromUndefOrPrim "WheelEventInit.getdeltaY"
                             prim__deltaY
                             prim__setDeltaY
                             0.0
                             (v :> WheelEventInit)

  export
  deltaZ :  (0 _ : JSType t)
         => {auto 0 _ : Elem WheelEventInit (Types t)}
         -> t
         -> Attribute True Optional Double
  deltaZ v = fromUndefOrPrim "WheelEventInit.getdeltaZ"
                             prim__deltaZ
                             prim__setDeltaZ
                             0.0
                             (v :> WheelEventInit)


text:
module Synchronous

import Data.Vect

%access export
%default total

counterFrom : Num ty => ty -> Stream ty
counterFrom = iterate (+1)

simulate : (Stream a -> Stream b) -> Stream a -> Stream b
simulate f xs = f xs

public export
delay : a -> Stream a -> Stream a
delay a s = a :: s

mux : Stream Bool -> Stream a -> Stream a -> Stream a
mux = liftA3 (\e,a,b=>if e then a else b)

regEn : a -> Stream Bool -> Stream a -> Stream a
regEn a (False :: xs) (y :: ys) = a :: regEn a xs ys
regEn a (True  :: xs) (y :: ys) = a :: regEn y xs ys

regMaybe : a -> Stream (Maybe a) -> Stream a
regMaybe a (Nothing  :: xs) = a :: regMaybe a xs
regMaybe a ((Just x) :: xs) = a :: regMaybe x xs

public export
window : (n : Nat) -> a -> Stream a -> Stream (Vect n a)
window Z a xs     = pure []
window (S k) a xs = let dl = scanl (flip delay) xs (replicate (k) a)
                    in  sequence dl


text:
module Data.Buffer

import System.Directory
import System.File

import Data.List

-- Reading and writing binary buffers. Note that this primitives are unsafe,
-- in that they don't check that buffer locations are within bounds.
-- We really need a safe wrapper!
-- They are used in the Idris compiler itself for reading/writing checked
-- files.

-- This is known to the compiler, so maybe ought to be moved to Builtin
export
data Buffer : Type where [external]

%foreign "scheme:blodwen-buffer-size"
         "node:lambda:b => BigInt(b.length)"
prim__bufferSize : Buffer -> Int

export
rawSize : HasIO io => Buffer -> io Int
rawSize buf = pure (prim__bufferSize buf)

%foreign "scheme:blodwen-new-buffer"
         "node:lambda:s=>Buffer.alloc(Number(s))"
prim__newBuffer : Int -> PrimIO Buffer

export
newBuffer : HasIO io => Int -> io (Maybe Buffer)
newBuffer size
    = do buf <- primIO (prim__newBuffer size)
         pure $ Just buf
--          if prim__nullAnyPtr buf /= 0
--             then pure Nothing
--             else pure $ Just $ MkBuffer buf size 0

-- might be needed if we do this in C...
export
freeBuffer : HasIO io => Buffer -> io ()
freeBuffer buf = pure ()

%foreign "scheme:blodwen-buffer-setbyte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
prim__setByte : Buffer -> Int -> Int -> PrimIO ()

%foreign "scheme:blodwen-buffer-setbyte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(Number(value), Number(offset))"
prim__setBits8 : Buffer -> Int -> Bits8 -> PrimIO ()

-- Assumes val is in the range 0-255
export
setByte : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setByte buf loc val
    = primIO (prim__setByte buf loc val)

export
setBits8 : HasIO io => Buffer -> (loc : Int) -> (val : Bits8) -> io ()
setBits8 buf loc val
    = primIO (prim__setBits8 buf loc val)

%foreign "scheme:blodwen-buffer-getbyte"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
prim__getByte : Buffer -> Int -> PrimIO Int

%foreign "scheme:blodwen-buffer-getbyte"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt8(Number(offset)))"
prim__getBits8 : Buffer -> Int -> PrimIO Bits8

export
getByte : HasIO io => Buffer -> (loc : Int) -> io Int
getByte buf loc
    = primIO (prim__getByte buf loc)

export
getBits8 : HasIO io => Buffer -> (loc : Int) -> io Bits8
getBits8 buf loc
    = primIO (prim__getBits8 buf loc)

%foreign "scheme:blodwen-buffer-setbits16"
         "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(Number(value), Number(offset))"
prim__setBits16 : Buffer -> Int -> Bits16 -> PrimIO ()

export
setBits16 : HasIO io => Buffer -> (loc : Int) -> (val : Bits16) -> io ()
setBits16 buf loc val
    = primIO (prim__setBits16 buf loc val)

%foreign "scheme:blodwen-buffer-getbits16"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt16LE(Number(offset)))"
prim__getBits16 : Buffer -> Int -> PrimIO Bits16

export
getBits16 : HasIO io => Buffer -> (loc : Int) -> io Bits16
getBits16 buf loc
    = primIO (prim__getBits16 buf loc)

%foreign "scheme:blodwen-buffer-setbits32"
         "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(Number(value), Number(offset))"
prim__setBits32 : Buffer -> Int -> Bits32 -> PrimIO ()

export
setBits32 : HasIO io => Buffer -> (loc : Int) -> (val : Bits32) -> io ()
setBits32 buf loc val
    = primIO (prim__setBits32 buf loc val)

%foreign "scheme:blodwen-buffer-getbits32"
         "node:lambda:(buf,offset)=>BigInt(buf.readUInt32LE(Number(offset)))"
prim__getBits32 : Buffer -> Int -> PrimIO Bits32

export
getBits32 : HasIO io => Buffer -> (loc : Int) -> io Bits32
getBits32 buf loc
    = primIO (prim__getBits32 buf loc)

%foreign "scheme:blodwen-buffer-setbits64"
prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()

export
setBits64 : HasIO io => Buffer -> (loc : Int) -> (val : Bits64) -> io ()
setBits64 buf loc val
    = primIO (prim__setBits64 buf loc val)

%foreign "scheme:blodwen-buffer-getbits64"
prim__getBits64 : Buffer -> Int -> PrimIO Bits64

export
getBits64 : HasIO io => Buffer -> (loc : Int) -> io Bits64
getBits64 buf loc
    = primIO (prim__getBits64 buf loc)

%foreign "scheme:blodwen-buffer-setint32"
         "node:lambda:(buf,offset,value)=>buf.writeInt32LE(Number(value), Number(offset))"
prim__setInt32 : Buffer -> Int -> Int -> PrimIO ()

export
setInt32 : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt32 buf loc val
    = primIO (prim__setInt32 buf loc val)

%foreign "scheme:blodwen-buffer-getint32"
         "node:lambda:(buf,offset)=>BigInt(buf.readInt32LE(Number(offset)))"
prim__getInt32 : Buffer -> Int -> PrimIO Int

export
getInt32 : HasIO io => Buffer -> (loc : Int) -> io Int
getInt32 buf loc
    = primIO (prim__getInt32 buf loc)

%foreign "scheme:blodwen-buffer-setint"
         "node:lambda:(buf,offset,value)=>buf.writeInt64(Number(value), Number(offset))"
prim__setInt : Buffer -> Int -> Int -> PrimIO ()

export
setInt : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt buf loc val
    = primIO (prim__setInt buf loc val)

%foreign "scheme:blodwen-buffer-getint"
         "node:lambda:(buf,offset)=>BigInt(buf.readInt64(Number(offset)))"
prim__getInt : Buffer -> Int -> PrimIO Int

export
getInt : HasIO io => Buffer -> (loc : Int) -> io Int
getInt buf loc
    = primIO (prim__getInt buf loc)

%foreign "scheme:blodwen-buffer-setdouble"
         "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, Number(offset))"
prim__setDouble : Buffer -> Int -> Double -> PrimIO ()

export
setDouble : HasIO io => Buffer -> (loc : Int) -> (val : Double) -> io ()
setDouble buf loc val
    = primIO (prim__setDouble buf loc val)

%foreign "scheme:blodwen-buffer-getdouble"
         "node:lambda:(buf,offset)=>buf.readDoubleLE(Number(offset))"
prim__getDouble : Buffer -> Int -> PrimIO Double

export
getDouble : HasIO io => Buffer -> (loc : Int) -> io Double
getDouble buf loc
    = primIO (prim__getDouble buf loc)

-- Get the length of a string in bytes, rather than characters
export
%foreign "C:strlen,libc 6"
stringByteLength : String -> Int

%foreign "scheme:blodwen-buffer-setstring"
         "node:lambda:(buf,offset,value)=>buf.write(value, Number(offset),buf.length - Number(offset), 'utf-8')"
prim__setString : Buffer -> Int -> String -> PrimIO ()

export
setString : HasIO io => Buffer -> (loc : Int) -> (val : String) -> io ()
setString buf loc val
    = primIO (prim__setString buf loc val)

%foreign "scheme:blodwen-buffer-getstring"
         "node:lambda:(buf,offset,len)=>buf.slice(Number(offset), Number(offset+len)).toString('utf-8')"
prim__getString : Buffer -> Int -> Int -> PrimIO String

export
getString : HasIO io => Buffer -> (loc : Int) -> (len : Int) -> io String
getString buf loc len
    = primIO (prim__getString buf loc len)

export
bufferData : HasIO io => Buffer -> io (List Int)
bufferData buf
    = do len <- rawSize buf
         unpackTo [] len
  where
    unpackTo : List Int -> Int -> io (List Int)
    unpackTo acc 0 = pure acc
    unpackTo acc loc
        = do val <- getByte buf (loc - 1)
             unpackTo (val :: acc) (loc - 1)

%foreign "scheme:blodwen-buffer-copydata"
         "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,Number(o2), Number(o1), Number(o1+length))"
prim__copyData : Buffer -> Int -> Int -> Buffer -> Int -> PrimIO ()

export
copyData : HasIO io => (src : Buffer) -> (start, len : Int) ->
           (dest : Buffer) -> (loc : Int) -> io ()
copyData src start len dest loc
    = primIO (prim__copyData src start len dest loc)

%foreign "C:idris2_readBufferData,libidris2_support"
         "node:lambdaRequire:fs:(f,b,l,m) => BigInt(__require_fs.readSync(f.fd,b,Number(l), Number(m)))"
prim__readBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int

%foreign "C:idris2_writeBufferData,libidris2_support"
         "node:lambdaRequire:fs:(f,b,l,m) => BigInt(__require_fs.writeSync(f.fd,b,Number(l), Number(m)))"
prim__writeBufferData : FilePtr -> Buffer -> Int -> Int -> PrimIO Int

export
readBufferData : HasIO io => File -> Buffer ->
                 (loc : Int) -> -- position in buffer to start adding
                 (maxbytes : Int) -> -- maximums size to read, which must not
                                     -- exceed buffer length
                 io (Either FileError ())
readBufferData (FHandle h) buf loc max
    = do read <- primIO (prim__readBufferData h buf loc max)
         if read >= 0
            then pure (Right ())
            else pure (Left FileReadError)

export
writeBufferData : HasIO io => File -> Buffer ->
                  (loc : Int) -> -- position in buffer to write from
                  (maxbytes : Int) -> -- maximums size to write, which must not
                                      -- exceed buffer length
                  io (Either FileError ())
writeBufferData (FHandle h) buf loc max
    = do written <- primIO (prim__writeBufferData h buf loc max)
         if written >= 0
            then pure (Right ())
            else pure (Left FileWriteError)

export
writeBufferToFile : HasIO io => String -> Buffer -> Int -> io (Either FileError ())
writeBufferToFile fn buf max
    = do Right f <- openFile fn WriteTruncate
             | Left err => pure (Left err)
         Right ok <- writeBufferData f buf 0 max
             | Left err => pure (Left err)
         closeFile f
         pure (Right ok)

export
createBufferFromFile : HasIO io => String -> io (Either FileError Buffer)
createBufferFromFile fn
    = do Right f <- openFile fn Read
             | Left err => pure (Left err)
         Right size <- fileSize f
             | Left err => pure (Left err)
         Just buf <- newBuffer size
             | Nothing => pure (Left FileReadError)
         Right ok <- readBufferData f buf 0 size
             | Left err => pure (Left err)
         closeFile f
         pure (Right buf)

export
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
resizeBuffer old newsize
    = do Just buf <- newBuffer newsize
              | Nothing => pure Nothing
         -- If the new buffer is smaller than the old one, just copy what
         -- fits
         oldsize <- rawSize old
         let len = if newsize < oldsize then newsize else oldsize
         copyData old 0 len buf 0
         freeBuffer old
         pure (Just buf)

||| Create a buffer containing the concatenated content from a
||| list of buffers.
export
concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
concatBuffers xs
    = do let sizes = map prim__bufferSize xs
         let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
         let cumulative = reverse revCumulative
         Just buf <- newBuffer totalSize
              | Nothing => pure Nothing
         traverse (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
         pure (Just buf)
    where
        scanSize : (Int, List Int) -> Int -> (Int, List Int)
        scanSize (s, cs) x  = (s+x, s::cs)

||| Split a buffer into two at a position.
export
splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
splitBuffer buf pos = do size <- rawSize buf
                         if pos > 0 && pos < size
                             then do Just first <- newBuffer pos
                                        | Nothing => pure Nothing
                                     Just second <- newBuffer (size - pos)
                                        | Nothing => pure Nothing
                                     copyData buf 0 pos first 0
                                     copyData buf pos (size-pos) second 0
                                     pure $ Just (first, second)
                             else pure Nothing


text:
module Language.LSP.Message.CodeLens

import Language.JSON
import Language.LSP.Message.Command
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
public export
record CodeLensClientCapabilities where
  constructor MkCodeLensClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{CodeLensClientCapabilities}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
public export
record CodeLensOptions where
  constructor MkCodeLensOptions
  workDoneProgress : Maybe Bool
  resolveProvider  : Maybe Bool
%runElab deriveJSON defaultOpts `{CodeLensOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
public export
record CodeLensRegistrationOptions where
  constructor MkCodeLensRegistrationOptions
  workDoneProgress : Maybe Bool
  resolveProvider  : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{CodeLensRegistrationOptions}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
public export
record CodeLensParams where
  constructor MkCodeLensParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{CodeLensParams}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_codeLens
public export
record CodeLens where
  constructor MkCodeLens
  range   : Range
  command : Maybe Command
  data_   : Maybe JSON
%runElab deriveJSON ({renames := [("data_", "data")]} defaultOpts) `{CodeLens}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#codeLens_refresh
public export
record CodeLensWorkspaceClientCapabilities where
  constructor MkCodeLensWorkspaceClientCapabilities
  refreshSupport : Maybe Bool
%runElab deriveJSON defaultOpts `{CodeLensWorkspaceClientCapabilities}


text:
main : IO ()
main = putStrLn "Running Chez program located in folder with spaces"

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module lib.test.MoreTests

export
test : IO Bool
test = do putStrLn "Yeah"
          pure True


text:
module Equal

-- Equality type

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

-- Simple examples

bool : Equal Bool Bool
bool = ?bool

true : Equal True True
true = ?true

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

-- Helpers

transitive : Equal a b -> Equal b c -> Equal a c
transitive ab bc = ?transitive

symmetric : Equal a b -> Equal b a
symmetric ab = ?symmetric

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

-- Stepping it up

plusZero : (n : Nat) -> Equal (plus n Z) n
plusZero n = ?plusZero

-- Built-in equality

plusZero' : (n : Nat) -> plus n Z = n
plusZero' n = ?plusZero'