text:
module Main

import Control.Monad.Either
import Data.List.Elem
import Data.SOP
import Data.String
import Data.Validated
import System
import System.Console.GetOpt
import System.File
import Text.WebIDL.Codegen as Codegen
import Text.WebIDL.Encoder
import Text.WebIDL.Types
import Text.WebIDL.Parser
import Text.PrettyPrint.Prettyprinter

--------------------------------------------------------------------------------
--          Command line options
--------------------------------------------------------------------------------

record Config where
  constructor MkConfig
  outDir         : String
  maxInheritance : Nat
  files          : List String

init : List String -> Config
init = MkConfig "../dom/src" 100

setOutDir : String -> Config -> Either (List String) Config
setOutDir s = Right . record { outDir = s }

descs : List $ OptDescr (Config -> Either (List String) Config)
descs = [ MkOpt ['o'] ["outDir"] (ReqArg setOutDir "<dir>")
            "output directory"
        ]

applyArgs : List String -> Either (List String) Config
applyArgs args =
  case getOpt RequireOrder descs args of
       MkResult opts n  [] [] => foldl (>>=) (Right $ init n) opts
       MkResult _ _ u e       => Left $ map unknown u ++ e

  where unknown : String -> String
        unknown = ("Unknown option: " ++)

--------------------------------------------------------------------------------
--          Codegen
--------------------------------------------------------------------------------

0 Prog : Type -> Type
Prog = EitherT String IO

toProgWith : (a -> String) ->  IO (Either a b) -> Prog b
toProgWith f io = MkEitherT $ map (mapFst f) io

toProg : Show a => IO (Either a b) -> Prog b
toProg = toProgWith show

runProg : Prog () -> IO ()
runProg (MkEitherT p) = do Right _ <- p
                             | Left e => putStrLn ("Error: " ++ e)
                           pure ()

fromCodegen : CodegenV a -> Prog a
fromCodegen = toProgWith (fastUnlines . map err) . pure . toEither
  where err : CodegenErr -> String
        err (CBInterfaceInvalidOps x y k) =
          #"Invalid number of callback operations in \#{x.domain}: \#{y.value} (\#{show k} operations)"#
        err (RegularOpWithoutName x y) =
          #"Unnamed regular operation in \#{x.domain}: \#{y.value}"#
        err (InvalidGetter x y) =
          #"Invalid getter in \#{x.domain}: \#{y.value}"#
        err (InvalidSetter x y) =
          #"Invalid setter in \#{x.domain}: \#{y.value}"#
        err (UnresolvedAlias x y) =
          #"Unresolved alias in \#{x.domain}: \#{y.value}"#
        err (AnyInUnion x) = #"\"Any\" type in a union type in \#{x.domain}"#
        err (PromiseInUnion x) = #"\"Promise\" type in a union type in \#{x.domain}"#
        err (NullableAny x) = #"Nullable \"Any\" type in \#{x.domain}"#
        err (NullablePromise x) = #"Nullable \"Promise\" type in \#{x.domain}"#
        err (InvalidConstType x) = #"Invalid constant type in \#{x.domain}"#

writeDoc : String -> String -> Prog ()
writeDoc f doc = toProg $ writeFile f doc

loadDef : String -> Prog (String,PartsAndDefs)
loadDef f = let mn = moduleName
                   . head
                   . split ('.' ==)
                   . last
                   $ split ('/' ==) f

             in do s <- toProg (readFile f)
                   d <- toProg (pure $ parseIdl partsAndDefs s)
                   pure (mn,d)

typesGen : Config -> List CGDomain -> Prog ()
typesGen c ds =
  let typesFile = c.outDir ++ "/Web/Internal/Types.idr"
   in writeDoc typesFile (typedefs ds)

codegen : Config -> CGDomain -> Prog ()
codegen c d =
  let typesFile = c.outDir ++ "/Web/Internal/" ++ d.name ++ "Types.idr"
      primFile  = c.outDir ++ "/Web/Internal/" ++ d.name ++ "Prim.idr"
      apiFile   = c.outDir ++ "/Web/Raw/" ++ d.name ++ ".idr"

   in do writeDoc typesFile (types d)
         writeDoc primFile (primitives d)
         writeDoc apiFile  (definitions d)

logAttributes : HasAttributes a => a -> Prog ()
logAttributes = traverse_ (putStrLn . extAttribute) . attributes

--------------------------------------------------------------------------------
--          Main Function
--------------------------------------------------------------------------------

run : List String -> Prog ()
run args = do config <- toProg (pure $ applyArgs args)
              ds     <- toDomains <$> traverse loadDef config.files

              let e = env config.maxInheritance ds

              doms   <- fromCodegen (traverse (domain e) ds)

--              logAttributes ds
              traverse_ (codegen config) doms
              typesGen config doms

main : IO ()
main = do (pn :: args) <- getArgs
                       |  Nil => putStrLn "Missing executable name. Aborting..."

          runProg (run args)


text:
data Nat : Type where
     Z : Nat
     S : (1 k : Nat) -> Nat

data Bool : Type where
     False : Bool
     True : Bool

data Thing : Bool -> Type where
     TF : Thing False
     TT : Thing True

data Maybe : Type -> Type where
     Nothing : {a : Type} -> Maybe a
     Just : {a : Type} -> a -> Maybe a

ok : (0 b : Bool) -> Thing b -> Bool
ok False TF = True
ok True TT = False

id : {a : Type} -> (1 x : a) -> a
id x = x

test : (1 x : Nat) -> Nat
test x = id x

data Pair : Type -> Type -> Type where
     MkPair : (1 x : a) -> (0 y : b) -> Pair a b

fst : (1 p : Pair a b) -> a
fst (MkPair x y) = x

wibble : (1 p : Pair a b) -> a
wibble {a=a} (MkPair x y)
    = let test : (1 y : a) -> a
          test y = y in
      test x

plus : (1 x : Nat) -> (1 y : Nat) -> Nat
plus Z y = y
plus (S k) y = S (plus k y)

holetest1 : (1 x : Nat) -> (1 y : Nat) -> Nat
holetest1 x y = plus ?this y

holetest2 : (1 x : Nat) -> (1 y : Nat) -> Nat
holetest2 x y = plus x ?that

ext: idr


text:
module Web.Internal.CssTypes

import JS

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

export data CSSGroupingRule : Type where [external]

export
ToFFI CSSGroupingRule CSSGroupingRule where toFFI = id

export
FromFFI CSSGroupingRule CSSGroupingRule where fromFFI = Just

export
SafeCast CSSGroupingRule where
  safeCast = unsafeCastOnPrototypeName "CSSGroupingRule"

export data CSSImportRule : Type where [external]

export
ToFFI CSSImportRule CSSImportRule where toFFI = id

export
FromFFI CSSImportRule CSSImportRule where fromFFI = Just

export
SafeCast CSSImportRule where
  safeCast = unsafeCastOnPrototypeName "CSSImportRule"

export data CSSMarginRule : Type where [external]

export
ToFFI CSSMarginRule CSSMarginRule where toFFI = id

export
FromFFI CSSMarginRule CSSMarginRule where fromFFI = Just

export
SafeCast CSSMarginRule where
  safeCast = unsafeCastOnPrototypeName "CSSMarginRule"

export data CSSNamespaceRule : Type where [external]

export
ToFFI CSSNamespaceRule CSSNamespaceRule where toFFI = id

export
FromFFI CSSNamespaceRule CSSNamespaceRule where fromFFI = Just

export
SafeCast CSSNamespaceRule where
  safeCast = unsafeCastOnPrototypeName "CSSNamespaceRule"

export data CSSPageRule : Type where [external]

export
ToFFI CSSPageRule CSSPageRule where toFFI = id

export
FromFFI CSSPageRule CSSPageRule where fromFFI = Just

export
SafeCast CSSPageRule where
  safeCast = unsafeCastOnPrototypeName "CSSPageRule"

export data CSSPseudoElement : Type where [external]

export
ToFFI CSSPseudoElement CSSPseudoElement where toFFI = id

export
FromFFI CSSPseudoElement CSSPseudoElement where fromFFI = Just

export
SafeCast CSSPseudoElement where
  safeCast = unsafeCastOnPrototypeName "CSSPseudoElement"

export data CSSRule : Type where [external]

export
ToFFI CSSRule CSSRule where toFFI = id

export
FromFFI CSSRule CSSRule where fromFFI = Just

export
SafeCast CSSRule where
  safeCast = unsafeCastOnPrototypeName "CSSRule"

export data CSSRuleList : Type where [external]

export
ToFFI CSSRuleList CSSRuleList where toFFI = id

export
FromFFI CSSRuleList CSSRuleList where fromFFI = Just

export
SafeCast CSSRuleList where
  safeCast = unsafeCastOnPrototypeName "CSSRuleList"

export data CSSStyleDeclaration : Type where [external]

export
ToFFI CSSStyleDeclaration CSSStyleDeclaration where toFFI = id

export
FromFFI CSSStyleDeclaration CSSStyleDeclaration where fromFFI = Just

export
SafeCast CSSStyleDeclaration where
  safeCast = unsafeCastOnPrototypeName "CSSStyleDeclaration"

export data CSSStyleRule : Type where [external]

export
ToFFI CSSStyleRule CSSStyleRule where toFFI = id

export
FromFFI CSSStyleRule CSSStyleRule where fromFFI = Just

export
SafeCast CSSStyleRule where
  safeCast = unsafeCastOnPrototypeName "CSSStyleRule"

export data CSSStyleSheet : Type where [external]

export
ToFFI CSSStyleSheet CSSStyleSheet where toFFI = id

export
FromFFI CSSStyleSheet CSSStyleSheet where fromFFI = Just

export
SafeCast CSSStyleSheet where
  safeCast = unsafeCastOnPrototypeName "CSSStyleSheet"

export data MediaList : Type where [external]

export
ToFFI MediaList MediaList where toFFI = id

export
FromFFI MediaList MediaList where fromFFI = Just

export
SafeCast MediaList where
  safeCast = unsafeCastOnPrototypeName "MediaList"

export data StyleSheet : Type where [external]

export
ToFFI StyleSheet StyleSheet where toFFI = id

export
FromFFI StyleSheet StyleSheet where fromFFI = Just

export
SafeCast StyleSheet where
  safeCast = unsafeCastOnPrototypeName "StyleSheet"

export data StyleSheetList : Type where [external]

export
ToFFI StyleSheetList StyleSheetList where toFFI = id

export
FromFFI StyleSheetList StyleSheetList where fromFFI = Just

export
SafeCast StyleSheetList where
  safeCast = unsafeCastOnPrototypeName "StyleSheetList"

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

export data ElementCSSInlineStyle : Type where [external]

export
ToFFI ElementCSSInlineStyle ElementCSSInlineStyle where toFFI = id

export
FromFFI ElementCSSInlineStyle ElementCSSInlineStyle where fromFFI = Just

export data LinkStyle : Type where [external]

export
ToFFI LinkStyle LinkStyle where toFFI = id

export
FromFFI LinkStyle LinkStyle where fromFFI = Just


text:
module India

import System
import System.File

export
parseFileWith :
  (parse : String -> Either String a) ->
  (filename: String) ->
  IO $ Either String a
parseFileWith parse filename = do
  Right text <- readFile filename
    | Left err => pure $ Left $ show err
  pure $ parse text

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
import Data.List

data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

length : Vect n a -> Nat
length [] = Z
length (x :: xs) = S (length xs)

wrong : Nat -> Nat
wrong x = length x


text:
> module Num.Operations

> import Data.Vect

> import Matrix.Matrix

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

> ||| Scalar-vector "multiplication"
> multSV : (Num t) => t -> Vect m t -> Vect m t
> -- multSV _ Nil = Nil
> -- multSV x (y :: ys) = (x * y) :: (multSV x ys)
> multSV x = map (x *)

> ||| Vector-matrix "multiplication" (kind of)
> multVM : (Num t) => Vect m t -> Matrix m n t -> Matrix m n t
> -- multVM {m = Z}   {n} Nil Nil = Nil
> -- multVM {m = S l} {n} (x :: xs) (v :: vs) = (multSV x v) :: (multVM xs vs)
> multVM {m} {n} xs xss = map (uncurry multSV) (zip xs xss)

> |||
> multConcat : (Num t) => Vect m t -> Vect m (Vect n t) -> Vect (m * n) t
> multConcat {m = Z}   {n} Nil Nil = Nil
> multConcat {m = S l} {n} (x :: xs) (v :: vs) = (multSV x v) ++ multConcat xs vs

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- Contains Helper functions
module Minesweeper.Helper

export
readNat : String -> Maybe Nat
readNat s = go 0 (unpack s) where

  readDigit : Char -> Maybe Nat
  readDigit c = case c of
    '0' => Just 0
    '1' => Just 1
    '2' => Just 2
    '3' => Just 3
    '4' => Just 4
    '5' => Just 5
    '6' => Just 6
    '7' => Just 7
    '8' => Just 8
    '9' => Just 9
    _   => Nothing

  go : Nat -> List Char -> Maybe Nat
  go acc l = case l of
    [] => Just acc
    (c::cs) => do
                  d <- readDigit c
                  go ((acc * 10) + d) cs

max_stars_repo_name: RossMeikleham/Idris-Minesweeper

max_issues_repo_name: RossMeikleham/Idris-Minesweeper

max_forks_repo_name: RossMeikleham/Idris-Minesweeper


text:
module Compiler.Erlang.Cmd

import Data.Strings

%default total

escapeCmd : List String -> String
escapeCmd components = unwords (map escapeComponent components)
  where
    escapeChar : Char -> String
    escapeChar '\'' = "'\"'\"'"
    escapeChar c    = cast c
    escapeComponent : String -> String
    escapeComponent component = "'" ++ concat (map escapeChar (unpack component)) ++ "'"

evalErlangSourceCmd : (erl : String) -> (code : String) -> String
evalErlangSourceCmd erl code =
  escapeCmd [erl, "-noshell", "-boot", "no_dot_erlang", "-eval", code]

pmapErlFun : String
pmapErlFun = "Collect = fun
  Collect([]) -> [];
  Collect([{Pid, MRef} | Next]) ->
    receive
      {Pid, Res} ->
        erlang:demonitor(MRef, [flush]),
        [{ok, Res} | Collect(Next)];
      {'DOWN', MRef, process, Pid, Reason} ->
        [{error, Reason} | Collect(Next)]
    end
  end,
  Pmap = fun(F, Es) ->
  Parent = self(),
  Running = [
    spawn_monitor(fun() -> Parent ! {self(), F(E)} end)
      || E <- Es],
  Collect(Running)
end"

export
executeBeamCmd : (erl : String) -> (outputDir : String) -> (modName : String) -> String
executeBeamCmd erl outputDir modName =
  escapeCmd [erl, "-noshell", "-boot", "no_dot_erlang", "-pa", outputDir, "-run", modName]

export
compileErlToBeamCmd : (erlc : String) -> (srcFiles : List String) -> (outputDir : String) -> String
compileErlToBeamCmd erlc srcFiles outputDir =
  escapeCmd $ [erlc, "-W0", "-o", outputDir] ++ srcFiles

export
compileAbstrToBeamCmd : (erl : String) -> (srcFiles : List String) -> (outputDir : String) -> String
compileAbstrToBeamCmd erl srcFiles outputDir =
  let code =
        concat {t=List}
          [pmapErlFun, ",
CompileAbstr = fun(File, OutputDir) ->
  {ok, Forms} = file:consult(File),
  {ok, ModuleName, BinaryOrCode} = compile:noenv_forms(Forms, []),
  OutputFile = filename:join(OutputDir, atom_to_list(ModuleName) ++ \".beam\"),
  file:write_file(OutputFile, BinaryOrCode)
end,
Pmap(fun(File) -> CompileAbstr(File, ", show outputDir, ") end, ", show srcFiles, "),
halt(0)"]
  in evalErlangSourceCmd erl code

export
compileAbstrToErlCmd : (isMinified : Bool) -> (erl : String) -> (srcFiles : List String) -> (outputDir : String) -> String
compileAbstrToErlCmd isMinified erl srcFiles outputDir =
  let columnWidth : Int =
        if isMinified
          then 10000
          else 120
      prettyOpts =
        "[{paper, " ++ show columnWidth ++ "}, {ribbon, " ++ show columnWidth ++ "}]"
      code =
        concat {t=List}
          [pmapErlFun, ",
ModuleNameFromForms = fun(Forms) ->
  lists:foldl(
    fun
      ({attribute, _, module, ModuleName}, _Acc) -> {ok, ModuleName};
      (_, Acc) -> Acc
    end, not_found, Forms)
end,
GenerateErl = fun(File, OutputDir) ->
  {ok, Forms} = file:consult(File),
  {ok, ModuleName} = ModuleNameFromForms(Forms),
  OutputFile = filename:join(OutputDir, atom_to_list(ModuleName) ++ \".erl\"),
  ErlangSource = erl_prettypr:format(erl_syntax:form_list(Forms), ", prettyOpts, "),
  file:write_file(OutputFile, ErlangSource)
end,
Pmap(fun(File) -> GenerateErl(File, ", show outputDir, ") end, ", show srcFiles, "),
halt(0)"]
  in evalErlangSourceCmd erl code


text:
module Circuits.NetList.Terms

import Decidable.Equality

import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.Quantifiers

import Data.String

import Data.Nat

import Toolkit.Data.DList
import Toolkit.Data.Whole

import Circuits.Common

import Circuits.NetList.Types

%default total

public export
data Term : (context : List Ty)
         -> (type    : Ty)
                    -> Type
  where
    Var : {type : Ty}
       -> (prf  : Elem type ctxt)
               -> Term ctxt type

    Port : (flow  : Direction)
        -> (dtype : DType)
        -> (body : Term (TyPort (flow, dtype)::ctxt) TyUnit)
                -> Term                        ctxt  TyUnit

    Wire : (type : DType)
        -> (body : Term (TyChan type :: ctxt) TyUnit)
                -> Term                 ctxt  TyUnit

    GateDecl : (g    : Term ctxt TyGate)
            -> (body : Term (TyGate::ctxt) TyUnit)
                    -> Term ctxt TyUnit

    Stop : Term ctxt TyUnit

    Assign : {type : DType}
          -> (i : Term ctxt (TyPort (INPUT,type)))
          -> (o : Term ctxt (TyPort (OUTPUT,type)))
          -> (body : Term ctxt TyUnit)
                  -> Term ctxt TyUnit

    Index : (idir : Index flow)
         -> (what : Term ctxt (TyPort (flow, BVECT (W (S n) ItIsSucc) type)))
         -> (idx  : Fin (S n))
         -> Term ctxt (TyPort (flow, type))

    Mux : (o   : Term ctxt (TyPort (OUTPUT, LOGIC)))
       -> (c   : Term ctxt (TyPort (INPUT,  LOGIC)))
       -> (l,r : Term ctxt (TyPort (INPUT,  LOGIC)))
              -> Term ctxt TyGate

    GateB : Binary.Kind
         -> (o   : Term ctxt (TyPort (OUTPUT, LOGIC)))
         -> (l,r : Term ctxt (TyPort (INPUT,  LOGIC)))
                -> Term ctxt TyGate

    GateU : Unary.Kind
         -> (o : Term ctxt (TyPort (OUTPUT, LOGIC)))
         -> (i : Term ctxt (TyPort (INPUT,  LOGIC)))
              -> Term ctxt TyGate

    Collect : {type : DType}
           -> (o   : Term ctxt (TyPort (OUTPUT, BVECT (W (S (S Z)) ItIsSucc) type)))
           -> (l,r : Term ctxt (TyPort (INPUT,  type)))
                  -> Term ctxt TyGate

    Split : (l,r : Term ctxt (TyPort (OUTPUT, LOGIC)))
         -> (i   : Term ctxt (TyPort (INPUT,  LOGIC)))
                -> Term ctxt TyGate

    Project : {type : DType}
           -> (how  : Project dir)
           -> (what : Term ctxt (TyChan type))
                   -> Term ctxt (TyPort (dir, type))

    Cast : {type : DType}
        -> (dir  : Cast INOUT flow)
        -> (what : Term ctxt (TyPort (INOUT, type)))
                -> Term ctxt (TyPort (flow,  type))

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- | Exercises on Boolean Relations.
module Koans.Boolean

logicalAND : Bool
logicalAND = True && ?fillme1 == True

logicalOR : Bool
logicalOR = False || ?fillme2 == False

logicalNOT : Bool
logicalNOT = not ?fillme3 == False

logicalPredicate : Bool
logicalPredicate = not ( ?fillme4 && True) || (?fillme5 && False) == True

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

max_stars_repo_name: yurrriq/idris-koans

max_issues_repo_name: TheWizardTower/idris-koans

max_forks_repo_name: yurrriq/idris-koans


text:
module Circuits.NetList.Linear.Usage.DataType.Use.Full

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra

import Circuits.Common
import Circuits.NetList.Types
import Circuits.NetList.Linear.Usage.DataType

%default total

mutual
  public export
  data Use : (type : DType)
          -> (free : Usage  type)
          -> (this : IsFree type free)
          -> (used : Usage  type)
          -> (that : IsUsed type used)
                  -> Type
    where
      UFL : Use LOGIC (Logic FREE) FreeL
                      (Logic USED) UsedL

      UFA : (prf : Use type fs free us used)
                -> Use (BVECT (W (S n) ItIsSucc) type) (Array fs) (FreeA free)
                                                       (Array us) (UsedA used)

  public export
  data Result : (type : DType)
             -> (free : Usage type)
             -> (prf  : IsFree type free)
                     -> Type
    where
      R : (u      : Usage type)
       -> (used   : IsUsed type u)
       -> (result : Use    type f free u used)
                 -> Result type f free

  namespace Vect
    public export
    data Use : (type : DType)
            -> (this : Vect n (Usage type))
            -> (free : All (IsFree type) this)
            -> (that : Vect n (Usage type))
            -> (used : All (IsUsed type) that)
                    -> Type
      where
        End : Use type Nil Nil Nil Nil
        Ext : Use type  f       pf        u       pu
           -> Use type     fs       pfs      us       pus
           -> Use type (f::fs) (pf::pfs) (u::us) (pu::pus)

    public export
    data Result : (type : DType)
               -> (free : Vect n (Usage type))
               -> (prf  : All (IsFree type) free)
                       -> Type
      where
        R : {this    : Vect n (Usage type)}
         -> (free    : All (IsFree type) this)
         -> (us      : Vect n (Usage type))
         -> (useds   : All (IsUsed type) us)
         -> (results : Use    type this free us useds)
                    -> Result type this free

mutual

  export
  use : {type : DType}
     -> {free : Usage type}
     -> (prf  : IsFree type free)
             -> Result type free prf
  use FreeL
    = R (Logic USED) UsedL UFL

  use (FreeA prf) with (use prf)
    use (FreeA prf) | (R prf us useds results)
      = R (Array us) (UsedA useds) (UFA results)

  namespace Vect
    export
    use : {type : DType}
       -> {free : Vect n (Usage type)}
       -> (prf  : All (IsFree type) free)
               -> Result type free prf
    use []
      = R [] [] [] End

    use (x :: xs) with (use x)
      use (x :: xs) | (R u used result) with (use xs)
        use (x :: xs) | (R u used result) | (R xs us useds results)
          = R (x :: xs) (u :: us) (used :: useds) (Ext result results)

-- [ EOF ]


text:
||| Represents shapes.
data Shape = ||| A triangle, with its base length and height.
             Triangle Double Double
           | ||| A rectangle, with its length and height.
           Rectangle Double Double
           | ||| A circle, with its raduis
             Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
                      (Combine (Translate 35 5 circle)
                               (Translate 15 25 triangle))

%name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe (Just x) (Just y) = case x < y of
                                  False => Just x
                                  True => Just y

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive t@(Triangle x y)) = Just $ area t
biggestTriangle (Primitive _) = Nothing
biggestTriangle (Combine pic pic1) = maxMaybe (biggestTriangle pic) (biggestTriangle pic1)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Basic.Types.Gate

%default total
%access public export

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


text:
||| Central module use to import the Specdris test framework
module Specdris.Spec

import System

import public Specdris.Data.SpecState
import public Specdris.Data.SpecResult
import public Specdris.Data.SpecInfo

import public Specdris.Core
import public Specdris.Expectations

import Specdris.Data.ConsoleColor

%access export
%default total

||| Adds a context/description to the spec test. It can have
||| nested descriptions or spec cases.
describe: (description : String) -> SpecTree' ffi -> SpecTree' ffi
describe descr tree = Node (Leaf $ Left $ Describe descr)
                           (tree)

||| Adds a spec case to the spec test. Spec cases consist only
||| of expectations. Nested spec cases or descriptions are not
||| allowed.
it : (description : String) -> SpecResult -> SpecTree' ffi
it descr spec = Node (Leaf $ Left $ It $ descr)
                     (Leaf $ Right $ pure spec)

||| Executes a spec test.
specWithState : {default False storeOutput : Bool} -> SpecTree' ffi -> IO' ffi SpecState
specWithState {storeOutput} tree
  = evaluate (\spec => spec) storeOutput tree

||| Executes a spec test and prints the result.
spec' : SpecTree' ffi -> IO' ffi ()
spec' tree
  = do state <- specWithState tree
       putStrLn' $ "\n" ++ stateToStr state

||| Executes a spec test, prints the result to the command line, and exits
||| with an error code if any tests have failed.
spec : SpecTree -> IO ()
spec tree
  = do state <- specWithState tree

       putStrLn' $ "\n" ++ stateToStr state

       if (failed state) > 0 then
         exitFailure
       else
         pure ()

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module SC

-- import Data.Stream

{-
interface Comonad (w : Type -> Type) where
  extract   : w a -> a
  duplicate : w a -> w (w a)

Comonad Stream where
  extract   (x :: _)  = x
  duplicate (x :: xs) = (x :: xs) :: duplicate xs
-}

data Cofree : (Type -> Type) -> Type -> Type where
  (::) : a -> Inf (f (Cofree f a)) -> Cofree f a

Functor f => Functor (Cofree f) where
  map f (x :: xs) = f x :: map (map f) xs

duplicate : (Functor f) => Cofree f a -> Cofree f (Cofree f a)
duplicate (x :: xs) = (x :: xs) :: map duplicate xs

pure : Cofree f a -> a
pure (x :: _) = x

(>>=) : (Functor f) => Cofree f a -> (Cofree f a -> b) -> Cofree f b
w >>= g = map g (duplicate w)

extend : (Functor f) => (Cofree f a -> b) -> (Cofree f a) -> Cofree f b
extend g w = map g (duplicate w)

data Id a = MkId a

Functor Id where
  map f (MkId x) = MkId (f x)

Strm : Type -> Type
Strm = Cofree Id

iterate : (f : a -> a) -> (x : a) -> Strm a
iterate f x = x :: MkId (iterate f (f x))

zeros : Strm Int
zeros = 0 :: MkId zeros

test : Strm Int
test = do
  x <- zeros
  pure x

data Cofree : (Type -> Type) -> Type -> Type where
  (::) : a -> Inf (f (Cofree f a)) -> Cofree f a

data ZP a = MkZP a a
data MV = L | R

Functor ZP where
  map f (MkZP x y) = MkZP (f x) (f y)

browsing : (forall b . f b -> i -> b) -> Cofree f a -> List i -> a
browsing idx (a :: as) []        = a
browsing idx (a :: as) (k :: ks) = browsing idx (idx as k) ks

Zipper : Type -> Type
Zipper = Cofree ZP

move : ZP a -> MV -> a
move (MkZP l r) L = l
move (MkZP l r) R = r

moves : List MV -> Zipper a -> Zipper a
moves m = extend (\x => browsing move x m)

-- https://chrispenner.ca/posts/representable-cofree-zippers
-- moveLeft : Zipper a -> Zipper a

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Foo

public export
foo : Nat -> Nat
foo = S


text:
module Evens

% access public export

public export
data IsEven : Nat -> Type where
  ZEven : IsEven 0
  SSEven : (n: Nat) -> IsEven n -> IsEven (S (S n))

twoEven : IsEven 2
twoEven = SSEven 0 ZEven

fourEven : IsEven 4
fourEven = SSEven 2 twoEven

half : (n: Nat) -> IsEven n -> Nat
half Z ZEven = 0
half (S (S k)) (SSEven k x) = S (half k x)

double: Nat -> Nat
double Z = Z
double (S k) = S (S (double k))

doubleEven : (n: Nat) -> IsEven (double n)
doubleEven Z = ZEven
doubleEven (S k) = SSEven (double k) (doubleEven k)

halfDouble: Nat -> Nat
halfDouble n = half (double n) (doubleEven n)

oneOdd: IsEven 1 -> Void
oneOdd ZEven impossible
oneOdd (SSEven _ _) impossible

threeOdd : IsEven 3 -> Void
threeOdd (SSEven (S Z) ZEven) impossible
threeOdd (SSEven (S Z) (SSEven _ _)) impossible

nOrSnEven: (n: Nat) -> Either (IsEven n) (IsEven (S n))
nOrSnEven Z = Left ZEven
nOrSnEven (S k) = case (nOrSnEven k) of
                       (Left l) => Right (SSEven k l)
                       (Right r) => Left r

halfRoof: Nat -> Nat
halfRoof n = case (nOrSnEven n) of
                  (Left nEven) => half n nEven
                  (Right snEven) => half (S n) snEven

nSnNotBothEven: (n: Nat) -> (IsEven n) -> IsEven (S n) -> Void
nSnNotBothEven Z ZEven ZEven impossible
nSnNotBothEven Z ZEven (SSEven _ _) impossible
nSnNotBothEven (S (S k)) (SSEven k x) (SSEven (S k) y) = nSnNotBothEven k x y

notNandSnEven : (n: Nat) -> (IsEven n , IsEven (S n)) -> Void
notNandSnEven n (a, b) = nSnNotBothEven n a b

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

byTwo : (n: Nat) -> IsEven n -> (k: Nat ** double k = n)
byTwo Z ZEven = (0 ** Refl)
byTwo (S (S k)) (SSEven k x) = step where
  step = case (byTwo k x) of
            (m ** pf) => ((S m) ** apNat (\l => S (S l)) (double m) k pf)

oneOddFamily : Nat -> Type
oneOddFamily Z = ()
oneOddFamily (S Z) = Void
oneOddFamily (S (S k)) = ()

oneOddProof : (n : Nat) -> IsEven n -> oneOddFamily n
oneOddProof Z ZEven = ()
oneOddProof (S (S k)) (SSEven k x) = ()

-- Examples

halfRoof3 : Nat
halfRoof3 = halfRoof 3 -- 2 : Nat

-- Equality added

thmAdd : (a: Nat) -> (b: Nat) -> (a = 0) -> (b = 0) -> (a + b = 0)
thmAdd Z Z Refl Refl = Refl

symmEq : (x : Type) -> (a: x) -> (b: x) -> (a = b) -> (b = a)
symmEq x b b Refl = Refl


text:
module Graphics.Util.Glfw

import public Graphics.Util.GlfwConfig

%include C "GLFW/glfw3.h"

%access private

||| Glfw Window
public export
data GlfwWindow = Win Ptr

||| Glfw Monitor
public export
data GlfwMonitor = Monitor Ptr | DefaultMonitor

public export
defaultMonitor : GlfwMonitor
defaultMonitor = DefaultMonitor

public export
interface Flag a where
  toInt   : a -> Int

public export
interface Flag a => GlfwConstant a where
  fromInt : Int -> a

public export
data KeyEventTy
  = GLFW_PRESS
  | GLFW_RELEASE
  | GLFW_REPEAT

public export
implementation Flag KeyEventTy where
  toInt   GLFW_PRESS   = 1
  toInt   GLFW_RELEASE = 0
  toInt   GLFW_REPEAT  = 2

public export
implementation GlfwConstant KeyEventTy where
  fromInt 1            = GLFW_PRESS
  fromInt 0            = GLFW_RELEASE
  fromInt 2            = GLFW_REPEAT

public export
implementation Eq KeyEventTy where
  GLFW_PRESS   == GLFW_PRESS   = True
  GLFW_RELEASE == GLFW_RELEASE = True
  GLFW_REPEAT  == GLFW_REPEAT  = True
  _            == _            = False

public export
implementation Show KeyEventTy where
  show GLFW_PRESS   = "GLFW_PRESS"
  show GLFW_RELEASE = "GLFW_RELEASE"
  show GLFW_REPEAT  = "GLFW_REPEAT"

-- | Special key is a key not represented in the 32 - 127 printable ASCII range.
public export
data FunctionKey
  = UNKNOWN
  | GLFW_KEY_ESCAPE
  | GLFW_KEY_ENTER
  | GLFW_KEY_TAB
  | GLFW_KEY_BACKSPACE
  | GLFW_KEY_INSERT
  | GLFW_KEY_DELETE
  | GLFW_KEY_RIGHT
  | GLFW_KEY_LEFT
  | GLFW_KEY_DOWN
  | GLFW_KEY_UP
  | GLFW_KEY_PAGE_UP
  | GLFW_KEY_PAGE_DOWN
  | GLFW_KEY_HOME
  | GLFW_KEY_END
  | GLFW_KEY_CAPS_LOCK
  | GLFW_KEY_SCROLL_LOCK
  | GLFW_KEY_NUM_LOCK
  | GLFW_KEY_PRINT_SCREEN
  | GLFW_KEY_PAUSE
  | GLFW_KEY_F1
  | GLFW_KEY_F2
  | GLFW_KEY_F3
  | GLFW_KEY_F4
  | GLFW_KEY_F5
  | GLFW_KEY_F6
  | GLFW_KEY_F7
  | GLFW_KEY_F8
  | GLFW_KEY_F9
  | GLFW_KEY_F10
  | GLFW_KEY_F11
  | GLFW_KEY_F12
  | GLFW_KEY_F13
  | GLFW_KEY_F14
  | GLFW_KEY_F15
  | GLFW_KEY_F16
  | GLFW_KEY_F17
  | GLFW_KEY_F18
  | GLFW_KEY_F19
  | GLFW_KEY_F20
  | GLFW_KEY_F21
  | GLFW_KEY_F22
  | GLFW_KEY_F23
  | GLFW_KEY_F24
  | GLFW_KEY_F25
  | GLFW_KEY_KP_0
  | GLFW_KEY_KP_1
  | GLFW_KEY_KP_2
  | GLFW_KEY_KP_3
  | GLFW_KEY_KP_4
  | GLFW_KEY_KP_5
  | GLFW_KEY_KP_6
  | GLFW_KEY_KP_7
  | GLFW_KEY_KP_8
  | GLFW_KEY_KP_9
  | GLFW_KEY_KP_DECIMAL
  | GLFW_KEY_KP_DIVIDE
  | GLFW_KEY_KP_MULTIPLY
  | GLFW_KEY_KP_SUBTRACT
  | GLFW_KEY_KP_ADD
  | GLFW_KEY_KP_ENTER
  | GLFW_KEY_KP_EQUAL
  | GLFW_KEY_LEFT_SHIFT
  | GLFW_KEY_LEFT_CONTROL
  | GLFW_KEY_LEFT_ALT
  | GLFW_KEY_LEFT_SUPER
  | GLFW_KEY_RIGHT_SHIFT
  | GLFW_KEY_RIGHT_CONTROL
  | GLFW_KEY_RIGHT_ALT
  | GLFW_KEY_RIGHT_SUPER
  | GLFW_KEY_MENU
  | GLFW_KEY_LAST

public export
implementation Flag FunctionKey where
  toInt UNKNOWN                     = -1
  toInt GLFW_KEY_ESCAPE             = 256
  toInt GLFW_KEY_ENTER              = 257
  toInt GLFW_KEY_TAB                = 258
  toInt GLFW_KEY_BACKSPACE          = 259
  toInt GLFW_KEY_INSERT             = 260
  toInt GLFW_KEY_DELETE             = 261
  toInt GLFW_KEY_RIGHT              = 262
  toInt GLFW_KEY_LEFT               = 263
  toInt GLFW_KEY_DOWN               = 264
  toInt GLFW_KEY_UP                 = 265
  toInt GLFW_KEY_PAGE_UP            = 266
  toInt GLFW_KEY_PAGE_DOWN          = 267
  toInt GLFW_KEY_HOME               = 268
  toInt GLFW_KEY_END                = 269
  toInt GLFW_KEY_CAPS_LOCK          = 280
  toInt GLFW_KEY_SCROLL_LOCK        = 281
  toInt GLFW_KEY_NUM_LOCK           = 282
  toInt GLFW_KEY_PRINT_SCREEN       = 283
  toInt GLFW_KEY_PAUSE              = 284
  toInt GLFW_KEY_F1                 = 290
  toInt GLFW_KEY_F2                 = 291
  toInt GLFW_KEY_F3                 = 292
  toInt GLFW_KEY_F4                 = 293
  toInt GLFW_KEY_F5                 = 294
  toInt GLFW_KEY_F6                 = 295
  toInt GLFW_KEY_F7                 = 296
  toInt GLFW_KEY_F8                 = 297
  toInt GLFW_KEY_F9                 = 298
  toInt GLFW_KEY_F10                = 299
  toInt GLFW_KEY_F11                = 300
  toInt GLFW_KEY_F12                = 301
  toInt GLFW_KEY_F13                = 302
  toInt GLFW_KEY_F14                = 303
  toInt GLFW_KEY_F15                = 304
  toInt GLFW_KEY_F16                = 305
  toInt GLFW_KEY_F17                = 306
  toInt GLFW_KEY_F18                = 307
  toInt GLFW_KEY_F19                = 308
  toInt GLFW_KEY_F20                = 309
  toInt GLFW_KEY_F21                = 310
  toInt GLFW_KEY_F22                = 311
  toInt GLFW_KEY_F23                = 312
  toInt GLFW_KEY_F24                = 313
  toInt GLFW_KEY_F25                = 314
  toInt GLFW_KEY_KP_0               = 320
  toInt GLFW_KEY_KP_1               = 321
  toInt GLFW_KEY_KP_2               = 322
  toInt GLFW_KEY_KP_3               = 323
  toInt GLFW_KEY_KP_4               = 324
  toInt GLFW_KEY_KP_5               = 325
  toInt GLFW_KEY_KP_6               = 326
  toInt GLFW_KEY_KP_7               = 327
  toInt GLFW_KEY_KP_8               = 328
  toInt GLFW_KEY_KP_9               = 329
  toInt GLFW_KEY_KP_DECIMAL         = 330
  toInt GLFW_KEY_KP_DIVIDE          = 331
  toInt GLFW_KEY_KP_MULTIPLY        = 332
  toInt GLFW_KEY_KP_SUBTRACT        = 333
  toInt GLFW_KEY_KP_ADD             = 334
  toInt GLFW_KEY_KP_ENTER           = 335
  toInt GLFW_KEY_KP_EQUAL           = 336
  toInt GLFW_KEY_LEFT_SHIFT         = 340
  toInt GLFW_KEY_LEFT_CONTROL       = 341
  toInt GLFW_KEY_LEFT_ALT           = 342
  toInt GLFW_KEY_LEFT_SUPER         = 343
  toInt GLFW_KEY_RIGHT_SHIFT        = 344
  toInt GLFW_KEY_RIGHT_CONTROL      = 345
  toInt GLFW_KEY_RIGHT_ALT          = 346
  toInt GLFW_KEY_RIGHT_SUPER        = 347
  toInt GLFW_KEY_MENU               = 348
  toInt GLFW_KEY_LAST               = 348

public export
implementation Eq FunctionKey where
  (==) k l = (toInt k) == (toInt l)

public export
implementation Show FunctionKey where
  show k = "Key " ++ (show (toInt k))

public export
data GlfwFlags
  = GLFW_FOCUSED
  | GLFW_ICONIFIED
  | GLFW_RESIZABLE
  | GLFW_VISIBLE
  | GLFW_DECORATED
  | GLFW_AUTO_ICONIFY
  | GLFW_FLOATING
  | GLFW_RED_BITS
  | GLFW_GREEN_BITS
  | GLFW_BLUE_BITS
  | GLFW_ALPHA_BITS
  | GLFW_DEPTH_BITS
  | GLFW_STENCIL_BITS
  | GLFW_ACCUM_RED_BITS
  | GLFW_ACCUM_GREEN_BITS
  | GLFW_ACCUM_BLUE_BITS
  | GLFW_ACCUM_ALPHA_BITS
  | GLFW_AUX_BUFFERS
  | GLFW_STEREO
  | GLFW_SAMPLES
  | GLFW_SRGB_CAPABLE
  | GLFW_REFRESH_RATE
  | GLFW_DOUBLEBUFFER
  | GLFW_CLIENT_API
  | GLFW_CONTEXT_VERSION_MAJOR
  | GLFW_CONTEXT_VERSION_MINOR
  | GLFW_CONTEXT_REVISION
  | GLFW_CONTEXT_ROBUSTNESS
  | GLFW_OPENGL_FORWARD_COMPAT
  | GLFW_OPENGL_DEBUG_CONTEXT
  | GLFW_OPENGL_PROFILE
  | GLFW_CONTEXT_RELEASE_BEHAVIOR
  | GLFW_OPENGL_API
  | GLFW_OPENGL_ES_API
  | GLFW_NO_ROBUSTNESS
  | GLFW_NO_RESET_NOTIFICATION
  | GLFW_LOSE_CONTEXT_ON_RESET
  | GLFW_OPENGL_ANY_PROFILE
  | GLFW_OPENGL_CORE_PROFILE
  | GLFW_OPENGL_COMPAT_PROFILE
  | GLFW_CURSOR
  | GLFW_STICKY_KEYS
  | GLFW_STICKY_MOUSE_BUTTONS
  | GLFW_CURSOR_NORMAL
  | GLFW_CURSOR_HIDDEN
  | GLFW_CURSOR_DISABLED
  | GLFW_ANY_RELEASE_BEHAVIOR
  | GLFW_RELEASE_BEHAVIOR_FLUSH
  | GLFW_RELEASE_BEHAVIOR_NONE

public export
implementation Flag GlfwFlags where
  toInt GLFW_FOCUSED                = 0x00020001
  toInt GLFW_ICONIFIED              = 0x00020002
  toInt GLFW_RESIZABLE              = 0x00020003
  toInt GLFW_VISIBLE                = 0x00020004
  toInt GLFW_DECORATED              = 0x00020005
  toInt GLFW_AUTO_ICONIFY           = 0x00020006
  toInt GLFW_FLOATING               = 0x00020007
  toInt GLFW_RED_BITS               = 0x00021001
  toInt GLFW_GREEN_BITS             = 0x00021002
  toInt GLFW_BLUE_BITS              = 0x00021003
  toInt GLFW_ALPHA_BITS             = 0x00021004
  toInt GLFW_DEPTH_BITS             = 0x00021005
  toInt GLFW_STENCIL_BITS           = 0x00021006
  toInt GLFW_ACCUM_RED_BITS         = 0x00021007
  toInt GLFW_ACCUM_GREEN_BITS       = 0x00021008
  toInt GLFW_ACCUM_BLUE_BITS        = 0x00021009
  toInt GLFW_ACCUM_ALPHA_BITS       = 0x0002100A
  toInt GLFW_AUX_BUFFERS            = 0x0002100B
  toInt GLFW_STEREO                 = 0x0002100C
  toInt GLFW_SAMPLES                = 0x0002100D
  toInt GLFW_SRGB_CAPABLE           = 0x0002100E
  toInt GLFW_REFRESH_RATE           = 0x0002100F
  toInt GLFW_DOUBLEBUFFER           = 0x00021010
  toInt GLFW_CLIENT_API             = 0x00022001
  toInt GLFW_CONTEXT_VERSION_MAJOR  = 0x00022002
  toInt GLFW_CONTEXT_VERSION_MINOR  = 0x00022003
  toInt GLFW_CONTEXT_REVISION       = 0x00022004
  toInt GLFW_CONTEXT_ROBUSTNESS     = 0x00022005
  toInt GLFW_OPENGL_FORWARD_COMPAT  = 0x00022006
  toInt GLFW_OPENGL_DEBUG_CONTEXT   = 0x00022007
  toInt GLFW_OPENGL_PROFILE         = 0x00022008
  toInt GLFW_CONTEXT_RELEASE_BEHAVIOR = 0x00022009
  toInt GLFW_OPENGL_API             = 0x00030001
  toInt GLFW_OPENGL_ES_API          = 0x00030002
  toInt GLFW_NO_ROBUSTNESS          =          0
  toInt GLFW_NO_RESET_NOTIFICATION  = 0x00031001
  toInt GLFW_LOSE_CONTEXT_ON_RESET  = 0x00031002
  toInt GLFW_OPENGL_ANY_PROFILE     =          0
  toInt GLFW_OPENGL_CORE_PROFILE    = 0x00032001
  toInt GLFW_OPENGL_COMPAT_PROFILE  = 0x00032002
  toInt GLFW_CURSOR                 = 0x00033001
  toInt GLFW_STICKY_KEYS            = 0x00033002
  toInt GLFW_STICKY_MOUSE_BUTTONS   = 0x00033003
  toInt GLFW_CURSOR_NORMAL          = 0x00034001
  toInt GLFW_CURSOR_HIDDEN          = 0x00034002
  toInt GLFW_CURSOR_DISABLED        = 0x00034003
  toInt GLFW_ANY_RELEASE_BEHAVIOR   =          0
  toInt GLFW_RELEASE_BEHAVIOR_FLUSH = 0x00035001
  toInt GLFW_RELEASE_BEHAVIOR_NONE  = 0x00035002

public export
implementation Flag Bool where
  toInt   True  = 1
  toInt   False = 0

public export
implementation GlfwConstant Bool where
  fromInt 1     = True
  fromInt 0     = False

-- GLFW from here

export
glfwInit : IO Bool
glfwInit = do ret <- foreign FFI_C "glfwInit" (IO Int)
              pure $ if ret == 1 then True else False

export
glfwWindowHint : GlfwFlags -> Int -> IO ()
glfwWindowHint flag val = foreign FFI_C "glfwWindowHint" (Int -> Int -> IO ()) (toInt flag) val

export
glfwGetPrimaryMonitor : IO GlfwMonitor
glfwGetPrimaryMonitor = do p <- foreign FFI_C "glfwGetPrimaryMonitor" (IO Ptr)
                           pure $ Monitor p

export
glfwCreateWindow : (title: String) -> (width: Int) -> (height: Int) -> GlfwMonitor -> IO GlfwWindow
glfwCreateWindow title width height (Monitor ptr) =
  do p <- foreign FFI_C "glfwCreateWindow" (Int -> Int -> String -> Ptr -> Ptr -> IO Ptr) width height title ptr prim__null
     pure $ Win p
glfwCreateWindow title width height DefaultMonitor =
  do p <- foreign FFI_C "glfwCreateWindow" (Int -> Int -> String -> Ptr -> Ptr -> IO Ptr) width height title prim__null prim__null
     pure $ Win p

export
isWindow : GlfwWindow -> IO Bool
isWindow (Win ptr) = nullPtr ptr

export
glfwMakeContextCurrent : GlfwWindow -> IO ()
glfwMakeContextCurrent (Win ptr) = foreign FFI_C "glfwMakeContextCurrent" (Ptr -> IO()) ptr

export
glfwDestroyWindow : GlfwWindow -> IO ()
glfwDestroyWindow (Win ptr) = foreign FFI_C "glfwDestroyWindow" (Ptr -> IO()) ptr

export
glfwTerminate : IO ()
glfwTerminate  = foreign FFI_C "glfwTerminate" (IO ())

export
glfwSwapBuffers : GlfwWindow -> IO ()
glfwSwapBuffers (Win ptr) = foreign FFI_C "glfwSwapBuffers" (Ptr -> IO()) ptr

export
glfwWaitEvents : IO ()
glfwWaitEvents = foreign FFI_C "glfwWaitEvents" (IO ())

export
glfwPollEvents : IO ()
glfwPollEvents = foreign FFI_C "glfwPollEvents" (IO ())

export
glfwSetInputMode : GlfwWindow -> GlfwFlags -> Int -> IO ()
glfwSetInputMode (Win ptr) flag val = foreign FFI_C "glfwSetInputMode" (Ptr -> Int -> Int -> IO ()) ptr (toInt flag) val

export
glfwGetFunctionKey : GlfwWindow -> FunctionKey -> IO KeyEventTy
glfwGetFunctionKey (Win ptr) k = do e <- foreign FFI_C "glfwGetKey" (Ptr -> Int -> IO Int) ptr (toInt k)
                                    pure $ fromInt e
export
glfwGetKey : GlfwWindow -> Char -> IO KeyEventTy
glfwGetKey (Win ptr) k = do e <- foreign FFI_C "glfwGetKey" (Ptr -> Int -> IO Int) ptr (ord $ toUpper k)
                            pure $ fromInt e

export
glfwWindowShouldClose : GlfwWindow -> IO Bool
glfwWindowShouldClose (Win ptr) = do flag <- foreign FFI_C "glfwWindowShouldClose" (Ptr -> IO Int) ptr
                                     let bool = if flag == 0 then False else True
                                     pure bool

{--
GLFWAPI void glfwGetVersion(int* major, int* minor, int* rev);
GLFWAPI const char* glfwGetVersionString(void);
GLFWAPI GLFWerrorfun glfwSetErrorCallback(GLFWerrorfun cbfun);
GLFWAPI GLFWmonitor** glfwGetMonitors(int* count);

GLFWAPI void glfwGetMonitorPos(GLFWmonitor* monitor, int* xpos, int* ypos);
GLFWAPI void glfwGetMonitorPhysicalSize(GLFWmonitor* monitor, int* widthMM, int* heightMM);
GLFWAPI const char* glfwGetMonitorName(GLFWmonitor* monitor);
GLFWAPI GLFWmonitorfun glfwSetMonitorCallback(GLFWmonitorfun cbfun);
GLFWAPI const GLFWvidmode* glfwGetVideoModes(GLFWmonitor* monitor, int* count);
GLFWAPI const GLFWvidmode* glfwGetVideoMode(GLFWmonitor* monitor);
GLFWAPI void glfwSetGamma(GLFWmonitor* monitor, float gamma);
GLFWAPI const GLFWgammaramp* glfwGetGammaRamp(GLFWmonitor* monitor);
GLFWAPI void glfwSetGammaRamp(GLFWmonitor* monitor, const GLFWgammaramp* ramp);
GLFWAPI void glfwDefaultWindowHints(void);

GLFWAPI GLFWwindow* glfwCreateWindow(int width, int height, const char* title, GLFWmonitor* monitor, GLFWwindow* share);

GLFWAPI void glfwSetWindowShouldClose(GLFWwindow* window, int value);
GLFWAPI void glfwSetWindowTitle(GLFWwindow* window, const char* title);
GLFWAPI void glfwGetWindowPos(GLFWwindow* window, int* xpos, int* ypos);
GLFWAPI void glfwSetWindowPos(GLFWwindow* window, int xpos, int ypos);
GLFWAPI void glfwGetWindowSize(GLFWwindow* window, int* width, int* height);
GLFWAPI void glfwSetWindowSize(GLFWwindow* window, int width, int height);
GLFWAPI void glfwGetFramebufferSize(GLFWwindow* window, int* width, int* height);
GLFWAPI void glfwGetWindowFrameSize(GLFWwindow* window, int* left, int* top, int* right, int* bottom);
GLFWAPI void glfwIconifyWindow(GLFWwindow* window);
GLFWAPI void glfwRestoreWindow(GLFWwindow* window);
GLFWAPI void glfwShowWindow(GLFWwindow* window);
GLFWAPI void glfwHideWindow(GLFWwindow* window);
GLFWAPI GLFWmonitor* glfwGetWindowMonitor(GLFWwindow* window);
GLFWAPI int glfwGetWindowAttrib(GLFWwindow* window, int attrib);
GLFWAPI void glfwSetWindowUserPointer(GLFWwindow* window, void* pointer);
GLFWAPI void* glfwGetWindowUserPointer(GLFWwindow* window);
GLFWAPI GLFWwindowposfun glfwSetWindowPosCallback(GLFWwindow* window, GLFWwindowposfun cbfun);
GLFWAPI GLFWwindowsizefun glfwSetWindowSizeCallback(GLFWwindow* window, GLFWwindowsizefun cbfun);
GLFWAPI GLFWwindowclosefun glfwSetWindowCloseCallback(GLFWwindow* window, GLFWwindowclosefun cbfun);
GLFWAPI GLFWwindowrefreshfun glfwSetWindowRefreshCallback(GLFWwindow* window, GLFWwindowrefreshfun cbfun);
GLFWAPI GLFWwindowfocusfun glfwSetWindowFocusCallback(GLFWwindow* window, GLFWwindowfocusfun cbfun);
GLFWAPI GLFWwindowiconifyfun glfwSetWindowIconifyCallback(GLFWwindow* window, GLFWwindowiconifyfun cbfun);
GLFWAPI GLFWframebuffersizefun glfwSetFramebufferSizeCallback(GLFWwindow* window, GLFWframebuffersizefun cbfun);

GLFWAPI void glfwPostEmptyEvent(void);
GLFWAPI int glfwGetInputMode(GLFWwindow* window, int mode);
GLFWAPI void glfwSetInputMode(GLFWwindow* window, int mode, int value);

GLFWAPI int glfwGetMouseButton(GLFWwindow* window, int button);
GLFWAPI void glfwGetCursorPos(GLFWwindow* window, double* xpos, double* ypos);
GLFWAPI void glfwSetCursorPos(GLFWwindow* window, double xpos, double ypos);
GLFWAPI GLFWcursor* glfwCreateCursor(const GLFWimage* image, int xhot, int yhot);
GLFWAPI GLFWcursor* glfwCreateStandardCursor(int shape);
GLFWAPI void glfwDestroyCursor(GLFWcursor* cursor);
GLFWAPI void glfwSetCursor(GLFWwindow* window, GLFWcursor* cursor);
GLFWAPI GLFWkeyfun glfwSetKeyCallback(GLFWwindow* window, GLFWkeyfun cbfun);
GLFWAPI GLFWcharfun glfwSetCharCallback(GLFWwindow* window, GLFWcharfun cbfun);
GLFWAPI GLFWcharmodsfun glfwSetCharModsCallback(GLFWwindow* window, GLFWcharmodsfun cbfun);
GLFWAPI GLFWmousebuttonfun glfwSetMouseButtonCallback(GLFWwindow* window, GLFWmousebuttonfun cbfun);
GLFWAPI GLFWcursorposfun glfwSetCursorPosCallback(GLFWwindow* window, GLFWcursorposfun cbfun);
GLFWAPI GLFWcursorenterfun glfwSetCursorEnterCallback(GLFWwindow* window, GLFWcursorenterfun cbfun);
GLFWAPI GLFWscrollfun glfwSetScrollCallback(GLFWwindow* window, GLFWscrollfun cbfun);
GLFWAPI GLFWdropfun glfwSetDropCallback(GLFWwindow* window, GLFWdropfun cbfun);
GLFWAPI int glfwJoystickPresent(int joy);
GLFWAPI const float* glfwGetJoystickAxes(int joy, int* count);
GLFWAPI const unsigned char* glfwGetJoystickButtons(int joy, int* count);
GLFWAPI const char* glfwGetJoystickName(int joy);
GLFWAPI void glfwSetClipboardString(GLFWwindow* window, const char* string);
GLFWAPI const char* glfwGetClipboardString(GLFWwindow* window);
GLFWAPI double glfwGetTime(void);
GLFWAPI void glfwSetTime(double time);

GLFWAPI GLFWwindow* glfwGetCurrentContext(void);

GLFWAPI int glfwExtensionSupported(const char* extension);
GLFWAPI GLFWglproc glfwGetProcAddress(const char* procname);

--}

export
glfwSwapInterval : Int -> IO ()
glfwSwapInterval interval = foreign FFI_C "glfwSwapInterval" (Int -> IO ()) interval

max_stars_repo_name: eckart/glfw-idris

max_issues_repo_name: eckart/glfw-idris

max_forks_repo_name: eckart/glfw-idris


text:
module Ram

import Effects
import Data.Bits
import Data.Buffer

%default total

public
export
data Ram : Effect where
  ReadByte : Buffer -> Int -> Ram Bits8 a (\v => a)
  WriteByte : Buffer -> Int -> Bits8 -> Ram () a (\v => ())

public
export
Handler Ram IO where
  handle () (ReadByte buf addr) k =
    do
      val <- Buffer.getByte buf addr
      k val ()
  handle () (WriteByte buf addr val) k =
    do
      Buffer.setByte buf addr val
      k () ()

public
export
RAM : EFFECT
RAM = MkEff () Ram

public
export
readByte : Buffer -> Int -> Eff Bits8 [RAM]
readByte buf addr = call (ReadByte buf addr)

public
export
writeByte : Buffer -> Int -> Bits8 -> Eff () [RAM]
writeByte buf addr val = call (WriteByte buf addr val)


text:
||| CSS Rules for the Inc. Buttons Example
module Examples.CSS.Reset

import Data.Vect
import Examples.CSS.Colors
import public Examples.CSS.Core
import Rhone.JS
import Text.CSS

--------------------------------------------------------------------------------
--          IDs
--------------------------------------------------------------------------------

||| Where the accumulated count is printed to
public export
out : ElemRef Div
out = Id Div "reset_out"

||| ID of the increasing button
public export
btnInc : ElemRef Button
btnInc = Id Button "reset_inc"

||| ID of the decreasing button
public export
btnDec : ElemRef Button
btnDec = Id Button "reset_dec"

||| ID of the reset button
public export
btnReset : ElemRef Button
btnReset = Id Button "reset_reset"

--------------------------------------------------------------------------------
--          CSS
--------------------------------------------------------------------------------

export
resetLbl : String
resetLbl = "reset_resetlbl"

export
incLbl : String
incLbl = "reset_inclbl"

export
decLbl : String
decLbl = "reset_declbl"

export
countLbl : String
countLbl = "reset_countlbl"

export
resetContent : String
resetContent = "reset_content"

export
resetBtn : String
resetBtn = "reset_incbtn"

data Tag = LRes | BRes | LInc | BInc | LDec | BDec | LCnt | OCnt

AreaTag Tag where
  showTag LRes = "LRes"
  showTag BRes = "BRes"
  showTag LInc = "LInc"
  showTag BInc = "BInc"
  showTag LDec = "LDec"
  showTag BDec = "BDec"
  showTag LCnt = "LCnt"
  showTag OCnt = "OCnt"

export
css : List (Rule 1)
css =
  [ class resetContent !!
      [ Display             .= Area
          (replicate 4 MinContent)
          [MaxContent, MaxContent]
          [ [LRes, BRes]
          , [LInc, BInc]
          , [LDec, BDec]
          , [LCnt, OCnt]
          ]

      , ColumnGap           .= px 10
      , RowGap              .= px 10
      , Padding             .= VH (px 20) (px 10)
      ]

  , class resetLbl  !! [ GridArea .= LRes ]

  , idRef btnReset  !! [ GridArea .= BRes ]

  , class incLbl    !! [ GridArea .= LInc ]

  , idRef btnInc    !! [ GridArea .= BInc ]

  , class decLbl    !! [ GridArea .= LDec ]

  , idRef btnDec    !! [ GridArea .= BDec ]

  , class countLbl  !! [ GridArea .= LCnt ]

  , idRef out  !!
      [ FontSize        .= Large
      , GridArea        .= OCnt
      , TextAlign       .= End
      ]
  ]


text:
module IdrisScript.RegExps

import IdrisScript

%access public export

RegExp : JS_IO (JSValue JSFunction)
RegExp = do
  regex <- jscall "RegExp" (JS_IO Ptr)
  pure $ MkJSFunction regex

data RegExpFlags = Global
                 | IgnoreCase
                 | Multiline

implementation Eq RegExpFlags where
  Global     == Global     = True
  IgnoreCase == IgnoreCase = True
  Multiline  == Multiline  = True
  _          == _          = False

JSRegExp : JSType
JSRegExp = JSObject "RegExp"

||| Creates a new RegExp with a list of flags.
newRegExp : String -> List RegExpFlags -> JS_IO (JSValue JSRegExp)
newRegExp patt flags = do
  regex <- jscall "new RegExp(%0, %1)" (String -> String -> JS_IO Ptr)
                  patt (mkFlags . nub $ flags)
  pure $ MkJSObject regex
where
  mkFlags : List RegExpFlags -> String
  mkFlags (Global     :: fs) = "g" ++ mkFlags fs
  mkFlags (IgnoreCase :: fs) = "i" ++ mkFlags fs
  mkFlags (Multiline  :: fs) = "m" ++ mkFlags fs
  mkFlags []                 = ""

||| Uses a RegExp `regex` on the string `str`.
match : (str : String)
     -> (regex : JSValue JSRegExp)
     -> JS_IO (JSValue JSArray)
match str regex = do
  res <- jscall "%0.match(%1)" (String -> Ptr -> JS_IO Ptr)
                str (unpack regex)
  pure $ MkJSObject res

||| Replaces matches of `regex` with `rpl` in the string `str`. Modifies
||| the original value.
replace : (str : String)
       -> (regex : JSValue JSRegExp)
       -> (rpl : String)
       -> JS_IO String
replace str regex rpl =
      jscall "%0.replace(%1, %2)" (String -> Ptr -> String -> JS_IO String)
             str (unpack regex) rpl

||| Splits an array `str` at the occurences of `regex`.
split : (str : String)
     -> (regex : JSValue JSRegExp)
     -> JS_IO (JSValue JSArray)
split str regex = do
  res <- jscall "%0.split(%1)" (String -> Ptr -> JS_IO Ptr)
                str (unpack regex)
  pure $ MkJSObject res

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Main

import Erlang

%default total

readFile : String -> IO (Maybe String)
readFile filename = do
  Right result <- erlCall "file" "read_file" [filename]
    | Left _ => do
      putStrLn "Failed to read file"
      pure Nothing
  let Right (MkTuple2 ok content) = erlDecode
        (tuple2 (exact (MkAtom "ok")) string)
        result
    | Left _ => do
      putStrLn "Failed to decode"
      pure Nothing
  pure $ Just content

main : IO ()
main = do
  Just content <- readFile "secret.txt"
    | Nothing => putStrLn "Failed to read content"
  putStrLn content

examplePerson : ErlAnyMap
examplePerson = insert "loves_idris" (MkAtom "true") $ insert "age" 34 $ insert "name" "Christian" empty

record Person where
  constructor MkPerson
  name : String
  age : Integer
  lovesIdris : Bool

Show Person where
  show (MkPerson name age lovesIdris) = "MkPerson \{show name} \{show age} \{show lovesIdris}"

main2 : IO ()
main2 = do
  let Just [name, age, lovesIdris] = erlDecodeMay
        (mapEntries
          [ "name" .= string
          , "age" .= integer
          , "loves_idris" .= bool
          ])
        examplePerson
    | Nothing => putStrLn "Unable to decode person"
  printLn (MkPerson name age lovesIdris)


text:
{-data SnocList ty = Empty | Snoc (SnocList ty) ty

reverseSnoc : SnocList ty -> List ty
reverseSnoc Empty = []
reverseSnoc (Snoc xs x) = x :: reverseSnoc xs-}

data SnocList : List a -> Type where
  Empty : SnocList []
  Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])

snocListHelp : (snoc : SnocList input) -> (rest : List a) ->
               SnocList (input ++ rest)
snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp {input} snoc (x :: xs) = rewrite appendAssociative input [x] xs in
                                      snocListHelp (Snoc snoc {x}) xs

snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs

myReverseHelper : (input : List a) -> SnocList input -> List a
myReverseHelper [] Empty = []
myReverseHelper (xs ++ [x]) (Snoc rec) = x :: myReverseHelper xs rec

{-myReverse : List a -> List a
myReverse xs = myReverseHelper xs (snocList xs)-}

myReverse : List a -> List a
myReverse input with (snocList input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (Snoc rec) = x :: myReverse xs | rec

isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix [] input2 | Empty = True
  isSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    isSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
      = if x == y then isSuffix xs ys | xsrec | ysrec
                  else False

data SplitRec : List a -> Type where
  SplitRecNil : SplitRec []
  SplitRecOne : SplitRec [x]
  SplitRecPair : (lrec : Lazy (SplitRec lefts)) ->
                 (rrec : Lazy (SplitRec rights)) ->
                 SplitRec (lefts ++ rights)

total splitRec : (xs : List a) -> SplitRec xs


text:
> module FastSimpleProb.MonadicProperties

> import Data.List
> import Data.List.Quantifiers
> import Syntax.PreorderReasoning

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicPostulates
> import FastSimpleProb.Predicates
> import FastSimpleProb.Functor
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Postulates
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties

> import Double.Predicates
> import Num.Refinements
> import Num.Properties
> import Fun.Operations
> import List.Operations
> import List.Properties
> import Unique.Predicates
> import Finite.Predicates
> import Sigma.Sigma
> import Pairs.Operations
> import Functor.Predicates

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

* Monadic properties of |support|, |normalize|:

> |||
> supportRetLemma : {A : Type} ->
>                   (a : A) -> support (ret a) = ret a
> supportRetLemma a = ( support (ret a) )
>                   ={ Refl }=
>                     ( map fst (toList (ret a)) )
>                   ={ Refl }=
>                     ( map fst (toList (MkSimpleProb [(a, one)] positiveOne)) )
>                   ={ Refl }=
>                     ( map fst [(a, one)] )
>                   ={ Refl }=
>                     ( [a] )
>                   ={ Refl }=
>                     ( ret a )
>                   QED

> ||| |normalize| is a natural transformation
> normalizeNatural : Natural {F = SimpleProb} {G = SimpleProb} normalize
> normalizeNatural = fmapNormalizeLemma

* |SimpleProb| is a container monad:

> |||
> elemNonEmptySpec0 : {A : Type} ->
>                     (a : A) -> (sp : SimpleProb A) -> a `Elem` sp -> NonEmpty sp
> elemNonEmptySpec0 {A} a sp aesp = List.Properties.elemNonEmptySpec0 a (support sp) aesp

> |||
> elemNonEmptySpec1 : {A : Type} ->
>                     (sp : SimpleProb A) -> NonEmpty sp -> Sigma A (\ a => a `Elem` sp)
> elemNonEmptySpec1 {A} sp nesp = List.Properties.elemNonEmptySpec1 (support sp) nesp

> |||
> containerMonadSpec1 : {A : Type} -> {a : A} -> a `FastSimpleProb.MonadicOperations.Elem` (ret a)
> containerMonadSpec1 {A} {a} = s3 where
>   s1 : a `Data.List.Elem` (List.Operations.ret a)
>   s1 = List.Properties.containerMonadSpec1
>   s2 : a `Data.List.Elem` (support (FastSimpleProb.MonadicOperations.ret a))
>   s2 = replace {P = \ X => a `Data.List.Elem` X} (sym (supportRetLemma a)) s1
>   s3 : a `FastSimpleProb.MonadicOperations.Elem` (ret a)
>   s3 = s2

> |||
> containerMonadSpec3 : {A : Type} -> {P : A -> Type} ->
>                       (a : A) -> (sp : SimpleProb A) ->
>                       All P sp -> a `Elem` sp -> P a
> containerMonadSpec3 {A} {P} a sp allp elemp = List.Properties.containerMonadSpec3 a (support sp) allp elemp

* Specific container monad properties

> |||
> uniqueAllLemma : {A : Type} -> {P : A -> Type} ->
>                  Unique1 P -> (sp : SimpleProb A) -> Unique (All P sp)
> uniqueAllLemma u1P sp = List.Properties.uniqueAllLemma u1P (support sp)

> |||
> finiteAll : {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (sp : SimpleProb A) -> Finite (All P sp)
> finiteAll f1P sp = List.Properties.finiteAll f1P (support sp)

> ||| All is decidable
> decidableAll : {A : Type} -> {P : A -> Type} ->
>                (dec : (a : A) -> Dec (P a)) -> (sp : SimpleProb A) -> Dec (All P sp)
> decidableAll dec sp = List.Properties.decidableAll dec (support sp)

> ||| NotEmpty is finite
> finiteNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Finite (FastSimpleProb.MonadicOperations.NonEmpty sp)
> finiteNonEmpty sp = List.Properties.finiteNonEmpty (support sp)

> ||| NotEmpty is decidable
> decidableNonEmpty : {A : Type} -> (sp : SimpleProb A) -> Dec (FastSimpleProb.MonadicOperations.NonEmpty sp)
> decidableNonEmpty sp = List.Properties.decidableNonEmpty (support sp)

* |SimpleProb|s are never empty

> using implementation NumNonNegDouble
>   |||
>   nonEmptyLemma1 : {A : Type} -> (sp : SimpleProb A) -> List.Operations.NonEmpty (toList sp)
>   nonEmptyLemma1 {A} (MkSimpleProb Nil psum) = s4 where
>     s1 : sumMapSnd {A = A} {B = NonNegDouble} Nil = zero
>     s1 = sumMapSndNilLemma {A = A} {B = NonNegDouble}
>     s2 : Positive (toDouble (sumMapSnd {A = A} {B = NonNegDouble} Nil))
>     s2 = psum
>     s3 : Positive (toDouble zero)
>     s3 = replace {P = \ X => Positive (toDouble X)} s1 s2
>     s4 : List.Operations.NonEmpty {A = (A, NonNegDouble)} (toList (MkSimpleProb Nil psum))
>     s4 = notPositiveZero s3
>   nonEmptyLemma1 (MkSimpleProb (ap :: aps) psum) = ()

> |||
> nonEmptyLemma : {A : Type} -> (sp : SimpleProb A) -> NonEmpty sp
> nonEmptyLemma {A} sp = s4 where
>   s1 : List.Operations.NonEmpty (toList sp)
>   s1 = nonEmptyLemma1 sp
>   s2 : List.Operations.NonEmpty (map fst (toList sp))
>   s2 = mapPreservesNonEmpty fst (toList sp) s1
>   s3 : List.Operations.NonEmpty (support sp)
>   s3 = s2
>   s4 : NonEmpty sp
>   s4 = s3

* Properies of |fmap| and |toList|

> using implementation NumNonNegDouble
>   |||
>   toListFmapLemma : {A, B : Type} ->
>                     (f : A -> B) -> (sp : SimpleProb A) ->
>                     toList (fmap f sp) = fmap (cross f id) (toList sp)
>   toListFmapLemma f (MkSimpleProb aps psum) =
>       ( toList (fmap f (MkSimpleProb aps psum)) )
>     ={ Refl }=
>       ( toList (MkSimpleProb
>                 (fmap (cross f id) aps)
>                 (replace {P = \ X => Positive (toDouble X)} (cong {f = sum} (sym (mapSndMapCrossAnyIdLemma f aps))) psum)) )
>     ={ Refl }=
>       ( fmap (cross f id) aps )
>     ={ Refl }=
>       ( fmap (cross f id) (toList (MkSimpleProb aps psum)) )
>     QED

> {-

> ---}


text:
||| Algebra.Monoid: A representation of monoids.
|||
||| A monoid is an associative unital magma (i.e., a unital semigroup).
||| Mathematically, one has a pair \\(\mathscr{N} = (N, \*)\\) satisfying:
|||
||| * \\((x*y)*z = x*(y*z)\\)
||| * \\(\exists e \in N [ \forall x \in N [ x*e = e*x = x ]]\\)
|||
||| Monoids strike a nice balance between generality and richness of structure;
||| many naturally-occuring magmas are indeed monoids. For example, consider the
||| set of functions \\(X \to X\\). This set always forms a monoid under
||| function composition (i.e., \\(\* \coloneqq \circ\\))! Everything has the
||| required type (the composition of two functions in \\(X \to X\\) is another
||| such function), the identity, of course, is the identity function
||| \\(\mathrm{id}\\), and function composition is always associative (applying
||| f, then applying (g then h) is the same as applying (f then g), then
||| applying h). Thus, we have a monoid.
|||
||| Another simplr monoid is the set of strings over a given alphabet, with
||| string concatenation as the function (and the empty string
||| \\(\varepsilon\\)) as the identity. Again, this obviously must be monoidal,
||| since string concatenation is clearly associative.
|||
||| TODO: add a little more
module Algebra.Monoid

import Algebra.Magma
import Algebra.Semigroup

%default total

export
record Monoid where
  constructor MkMonoid'
  magma  : Magma
  ID     : Set {magma}
  {assoc : {s,t,u : Set {magma}} -> s |*| (t |*| u) = (s |*| t) |*| u}
  {idl   : {n : Set {magma}} -> (ID |*| n  = n)}
  {idr   : {n : Set {magma}} -> (n  |*| ID = n)}

MkMonoid : (set : Type) -> (op : set -> set -> set) -> (i : set)
             -> {auto assoc : {s,t,u : set} -> s `op` (t `op` u) = (s `op` t) `op` u}
             -> {auto idl   : {n : set} -> (i `op` n = n)}
             -> {auto idr   : {n : set} -> (n `op` i = n)}
             -> Monoid
MkMonoid set op i {assoc} {idl} {idr} = MkMonoid' (MkMagma set op) i {assoc} {idl} {idr}

FuncMonoid : {a : Type} -> Monoid
FuncMonoid {a} = MkMonoid (a -> a) (.) (id)

%hint
listIdr : {a : Type} -> {xs : List a} -> xs ++ [] = xs
listIdr {xs = []}      = Refl
listIdr {xs = (x::xr)} = cong listIdr

%hint
listAssoc : {a : Type} -> {xs,ys,zs : List a} -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
listAssoc {xs=[]}      {ys} {zs} = Refl
listAssoc {xs=(x::xr)} {ys} {zs} = cong listAssoc

ListMonoid : {a : Type} -> Monoid
ListMonoid {a} = MkMonoid (List a) (++) []

MonoidToSemigroup : Monoid -> Semigroup
MonoidToSemigroup monoid = MkSemigroup Set (|*|) {assoc = assoc monoid}
--
{-
export
interface Magma N op => Monoid (N : Type) (op : N -> N -> N) (e : N) where
  assoc : {n,p,q : N} -> ((n `op` p) `op` q = n `op` (p `op` q))
  idl : {n : N} -> (n `op` e = n)
  idr : {n : N} -> (e `op` n = n)

_e : Monoid n op e -> n
_e _ = e

export
e : (Monoid n op e) => n
e @{monoid} = _e monoid

-- idk why this isn't working. try the forums, i guess.
-- Algebra.Monoid.Monoid n op ide => Algebra.Semigroup.Semigroup n op where
--   assoc = assoc
-}

max_stars_repo_name: greatBigDot/algebra

max_issues_repo_name: greatBigDot/algebra

max_forks_repo_name: greatBigDot/algebra


text:
main : HasIO io => io ()
main = do printLn (0 * the Bits8 1)
          printLn (0 * the Bits16 1)
          printLn (0 * the Bits32 1)
          printLn (0 * the Bits64 1)


text:
module TTImp.Elab.Utils

import Core.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Normalise
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.TTImp

%default covering

detagSafe : {auto c : Ref Ctxt Defs} ->
            Defs -> NF [] -> Core Bool
detagSafe defs (NTCon _ n _ _ args)
    = do Just (TCon _ _ _ _ _ _ _ (Just detags)) <- lookupDefExact n (gamma defs)
              | _ => pure False
         args' <- traverse (evalClosure defs . snd) args
         pure $ notErased 0 detags args'
  where
    -- if any argument positions are in the detaggable set, and unerased, then
    -- detagging is safe
    notErased : Nat -> List Nat -> List (NF []) -> Bool
    notErased i [] _ = True -- Don't need an index available
    notErased i ns [] = False
    notErased i ns (NErased _ True :: rest)
        = notErased (i + 1) ns rest -- Can't detag here, look elsewhere
    notErased i ns (_ :: rest) -- Safe to detag via this argument
        = elem i ns || notErased (i + 1) ns rest
detagSafe defs _ = pure False

findErasedFrom : {auto c : Ref Ctxt Defs} ->
                 Defs -> Nat -> NF [] -> Core (List Nat, List Nat)
findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf)
    = do -- In the scope, use 'Erased fc True' to mean 'argument is erased'.
         -- It's handy here, because we can use it to tell if a detaggable
         -- argument position is available
         sc <- scf defs (toClosure defaultOpts [] (Erased fc (isErased c)))
         (erest, dtrest) <- findErasedFrom defs (1 + pos) sc
         let dt' = if !(detagSafe defs !(evalClosure defs aty))
                      then (pos :: dtrest) else dtrest
         pure $ if isErased c
                   then (pos :: erest, dt')
                   else (erest, dt')
findErasedFrom defs pos tm = pure ([], [])

-- Find the argument positions in the given type which are guaranteed to be
-- erasable
export
findErased : {auto c : Ref Ctxt Defs} ->
             ClosedTerm -> Core (List Nat, List Nat)
findErased tm
    = do defs <- get Ctxt
         tmnf <- nf defs [] tm
         findErasedFrom defs 0 tmnf

export
updateErasable : {auto c : Ref Ctxt Defs} ->
                 Name -> Core ()
updateErasable n
    = do defs <- get Ctxt
         Just gdef <- lookupCtxtExact n (gamma defs)
              | Nothing => pure ()
         (es, dtes) <- findErased (type gdef)
         ignore $ addDef n $ record
                    { eraseArgs = es,
                      safeErase = dtes } gdef

export
wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a
wrapErrorC opts err
    = if InCase `elem` opts
         then id
         else wrapError err

plicit : Binder (Term vars) -> PiInfo RawImp
plicit (Pi _ _ p _) = forgetDef p
plicit (PVar _ _ p _) = forgetDef p
plicit _ = Explicit

export
bindNotReq : {vs : _} ->
             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
             List (PiInfo RawImp, Name) ->
             Term vs -> (List (PiInfo RawImp, Name), Term pre)
bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
bindNotReq fc i (b :: env) SubRefl ns tm
   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
         (ns', refToLocal (MN "arg" i) _ btm)
bindNotReq fc i (b :: env) (KeepCons p) ns tm
   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
         (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
         (ns', refToLocal (MN "arg" i) _ btm)
bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
   = bindNotReq fc i env p ((plicit b, n) :: ns)
       (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b)) tm)

export
bindReq : {vs : _} ->
          FC -> Env Term vs -> (sub : SubVars pre vs) ->
          List (PiInfo RawImp, Name) ->
          Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)
bindReq {vs} fc env SubRefl ns tm
    = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
  where
    notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
    notLets acc [] _ = acc
    notLets acc (v :: vs) (b :: env) = if isLet b then notLets acc vs env
                                       else notLets (v :: acc) vs env
bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
    = do b' <- shrinkBinder b p
         bindReq fc env p ((plicit b, n) :: ns)
            (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b')) tm)
bindReq fc (b :: env) (DropCons p) ns tm
    = bindReq fc env p ns tm

-- This machinery is to calculate whether any top level argument is used
-- more than once in a case block, in which case inlining wouldn't be safe
-- since it might duplicate work.

data ArgUsed = Used1 -- been used
             | Used0 -- not used
             | LocalVar -- don't care if it's used

data Usage : List Name -> Type where
     Nil : Usage []
     (::) : ArgUsed -> Usage xs -> Usage (x :: xs)

initUsed : (xs : List Name) -> Usage xs
initUsed [] = []
initUsed (x :: xs) = Used0 :: initUsed xs

initUsedCase : (xs : List Name) -> Usage xs
initUsedCase [] = []
initUsedCase [x] = [Used0]
initUsedCase (x :: xs) = LocalVar :: initUsedCase xs

setUsedVar : {idx : _} ->
             (0 _ : IsVar n idx xs) -> Usage xs -> Usage xs
setUsedVar First (Used0 :: us) = Used1 :: us
setUsedVar (Later p) (x :: us) = x :: setUsedVar p us
setUsedVar First us = us

isUsed : {idx : _} ->
         (0 _ : IsVar n idx xs) -> Usage xs -> Bool
isUsed First (Used1 :: us) = True
isUsed First (_ :: us) = False
isUsed (Later p) (_ :: us) = isUsed p us

data Used : Type where

setUsed : {idx : _} ->
          {auto u : Ref Used (Usage vars)} ->
          (0 _ : IsVar n idx vars) -> Core ()
setUsed p
    = do used <- get Used
         put Used (setUsedVar p used)

extendUsed : ArgUsed -> (new : List Name) -> Usage vars -> Usage (new ++ vars)
extendUsed a [] x = x
extendUsed a (y :: xs) x = a :: extendUsed a xs x

dropUsed : (new : List Name) -> Usage (new ++ vars) -> Usage vars
dropUsed [] x = x
dropUsed (x :: xs) (u :: us) = dropUsed xs us

inExtended : ArgUsed -> (new : List Name) ->
             {auto u : Ref Used (Usage vars)} ->
             (Ref Used (Usage (new ++ vars)) -> Core a) ->
             Core a
inExtended a new sc
    = do used <- get Used
         u' <- newRef Used (extendUsed a new used)
         res <- sc u'
         put Used (dropUsed new !(get Used @{u'}))
         pure res

termInlineSafe : {vars : _} ->
                 {auto u : Ref Used (Usage vars)} ->
                 Term vars -> Core Bool
termInlineSafe (Local fc isLet idx p)
   = if isUsed p !(get Used)
        then pure False
         else do setUsed p
                 pure True
termInlineSafe (Meta fc x y xs)
    = allInlineSafe xs
  where
    allInlineSafe : List (Term vars) -> Core Bool
    allInlineSafe [] = pure True
    allInlineSafe (x :: xs)
        = do xok <- termInlineSafe x
             if xok
                then allInlineSafe xs
                else pure False
termInlineSafe (Bind fc x b scope)
   = do bok <- binderInlineSafe b
        if bok
           then inExtended LocalVar [x] (\u' => termInlineSafe scope)
           else pure False
  where
    binderInlineSafe : Binder (Term vars) -> Core Bool
    binderInlineSafe (Let _ _ val _) = termInlineSafe val
    binderInlineSafe _ = pure True
termInlineSafe (App fc fn arg)
    = do fok <- termInlineSafe fn
         if fok
            then termInlineSafe arg
            else pure False
termInlineSafe (As fc x as pat) = termInlineSafe pat
termInlineSafe (TDelayed fc x ty) = termInlineSafe ty
termInlineSafe (TDelay fc x ty arg) = termInlineSafe arg
termInlineSafe (TForce fc x val) = termInlineSafe val
termInlineSafe _ = pure True

mutual
  caseInlineSafe : {vars : _} ->
                   {auto u : Ref Used (Usage vars)} ->
                   CaseTree vars -> Core Bool
  caseInlineSafe (Case idx p scTy xs)
      = if isUsed p !(get Used)
           then pure False
           else do setUsed p
                   altsSafe xs
    where
      altsSafe : List (CaseAlt vars) -> Core Bool
      altsSafe [] = pure True
      altsSafe (a :: as)
          = do u <- get Used
               aok <- caseAltInlineSafe a
               if aok
                  then do -- We can reset the usage information, because we're
                          -- only going to use one alternative at a time
                          put Used u
                          altsSafe as
                  else pure False
  caseInlineSafe (STerm x tm) = termInlineSafe tm
  caseInlineSafe (Unmatched msg) = pure True
  caseInlineSafe Impossible = pure True

  caseAltInlineSafe : {vars : _} ->
                      {auto u : Ref Used (Usage vars)} ->
                      CaseAlt vars -> Core Bool
  caseAltInlineSafe (ConCase x tag args sc)
      = inExtended Used0 args (\u' => caseInlineSafe sc)
  caseAltInlineSafe (DelayCase ty arg sc)
      = inExtended Used0 [ty, arg] (\u' => caseInlineSafe sc)
  caseAltInlineSafe (ConstCase x sc) = caseInlineSafe sc
  caseAltInlineSafe (DefaultCase sc) = caseInlineSafe sc

-- An inlining is safe if no variable is used more than once in the tree,
-- which means that there's no risk of an input being evaluated more than
-- once after the definition is expanded.
export
inlineSafe : {vars : _} ->
             CaseTree vars -> Core Bool
inlineSafe t
    = do u <- newRef Used (initUsed vars)
         caseInlineSafe t

export
canInlineDef : {auto c : Ref Ctxt Defs} ->
               Name -> Core Bool
canInlineDef n
    = do defs <- get Ctxt
         Just (PMDef _ _ _ rtree _) <- lookupDefExact n (gamma defs)
             | _ => pure False
         inlineSafe rtree

-- This is a special case because the only argument we actually care about
-- is the last one, since the others are just variables passed through from
-- the environment, and duplicating a variable doesn't cost anything.
export
canInlineCaseBlock : {auto c : Ref Ctxt Defs} ->
                     Name -> Core Bool
canInlineCaseBlock n
    = do defs <- get Ctxt
         Just (PMDef _ vars _ rtree _) <- lookupDefExact n (gamma defs)
             | _ => pure False
         u <- newRef Used (initUsedCase vars)
         caseInlineSafe rtree


text:
import Data.Vect

parameters (len : Nat)
  record Foo where
    constructor Bar
    Gnat : Vect len Nat

foo : Foo 1
foo = Bar _ [0]