text:
module Provider

import DB.SQLite.Effect
import DB.SQLite.SQLiteCodes
import Effects

import Database
import ParserHack
import Queries
import Schema
import SQLiteTypes

%access export

%language TypeProviders

mkDB : ResultSet -> Either String (List (String, Schema))
mkDB [] = Right []
mkDB ([DBText v]::rest) =
  case getSchema (toLower v) of
    Nothing => Left ( "Couldn't parse schema '" ++ v ++ "'\n")
    Just (t, tbl) =>
      with Applicative
        Right List.(::) <*> Right (t, tbl) <*> mkDB rest
mkDB _ = Left "Couldn't understand SQLite output - wrong type"

getSchemas : (filename : String) -> Eff (Provider (DB filename)) [SQLITE ()]
getSchemas file =
  do let ddlQuery = "SELECT `sql` FROM `sqlite_master` " ++
                    "WHERE NOT (sqlite_master.name LIKE \"sqlite%\");"
     resSet <- executeSelect file ddlQuery [] $
               do sql <- getColumnText 0
                  pure [DBText sql]
     case resSet of
       Left err => pure (Error $ "Error reading '" ++ file ++ "': " ++ (show err))
       Right res => case mkDB res of
                      Left err => pure (Error err)
                      Right db => pure (Provide (MkDB file db))

getRow : (s : Schema) -> SimpleEff.Eff (Row s) [SQLITE (SQLiteExecuting ValidRow)]
getRow s = go 0 s
  where go : Int -> (s : Schema) -> Eff (Row s) [SQLITE (SQLiteExecuting ValidRow)]
        go i []          = pure []
        go i ((_ ::: ty) :: s) = [| getCol ty :: go (i+1) s |]
          where getCol : (t : SQLiteType) -> Eff (interpSql t) [SQLITE (SQLiteExecuting ValidRow)]
                getCol TEXT = getColumnText i
                getCol INTEGER = do int <- getColumnInt i
                                    pure (cast int)
                getCol REAL = getColumnFloat i
                getCol (NULLABLE x) = do nullp <- isColumnNull i
                                         case nullp of
                                           True => pure Nothing
                                           False => do val <- getCol x
                                                       pure (Just val)

collectRows : (s : Schema) -> Eff (Table s) [SQLITE (SQLiteExecuting ValidRow)] [SQLITE (SQLiteExecuting InvalidRow)]
collectRows s = do row <- getRow s
                   case !nextRow of
                     Unstarted => pure $ row :: !(collectRows s)
                     StepFail => pure $ row :: !(collectRows s)
                     StepComplete => pure $ row :: !(collectRows s)
                     NoMoreRows => pure [row]

query : {file : String} -> {db : DB file} -> Query db s -> Eff (Either QueryError (Table s)) [SQLITE ()]
query {file=fn} q =
  case !(openDB fn) of
    Left err => pure $ Left err
    Right () =>  -- FIXME should really use binding
      case !(prepareStatement (compileQuery q)) of
        Left err => do cleanupPSFail
                       pure $ Left err
        Right () =>
          case !finishBind of
            Just err => do cleanupBindFail ; return $ Left err
            Nothing =>
              case !executeStatement of
                Unstarted => do rs <- collectRows _
                                finalise
                                closeDB
                                pure (Right rs)
                StepFail => do rs <- collectRows _
                               finalise
                               closeDB
                               pure (Right rs)
                StepComplete => do rs <- collectRows _
                                   finalise
                                   closeDB
                                   pure (Right rs)
                NoMoreRows => do finalise
                                 closeDB
                                 pure (Right [])

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
-- Minimal implicational logic, PHOAS approach, initial encoding

module Pi.ArrMp

%default total

-- Types

infixr 0 :=>
data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty

-- Context and truth judgement

Cx : Type
Cx = Ty -> Type

isTrue : Ty -> Cx -> Type
isTrue a tc = tc a

-- Terms

infixl 1 :$
data Tm : Cx -> Ty -> Type where
  var  : isTrue a tc                -> Tm tc a
  lam' : (isTrue a tc -> Tm tc b)   -> Tm tc (a :=> b)
  (:$) : Tm tc (a :=> b) -> Tm tc a -> Tm tc b

lam'' : (Tm tc a -> Tm tc b) -> Tm tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

syntax "lam" {a} ":=>" [b] = lam'' (\a => b)

Thm : Ty -> Type
Thm a = {tc : Cx} -> Tm tc a

-- Example theorems

aI : Thm (a :=> a)
aI =
  lam x :=> x

aK : Thm (a :=> b :=> a)
aK =
  lam x :=>
    lam y :=> x

aS : Thm ((a :=> b :=> c) :=> (a :=> b) :=> a :=> c)
aS =
  lam f :=>
    lam g :=>
      lam x :=> f :$ x :$ (g :$ x)

tSKK : Thm (a :=> a)
tSKK {a} =
  aS {b = a :=> a} :$ aK :$ aK

ext: idr

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Cycle1

import Cycle2


text:
module Tensor

-- Based on https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf

import Data.Vect
import Data.Matrix.Numeric

%access public export

data Tensor : Vect n Nat -> Type -> Type where
  Scalar : a -> Tensor [] a
  Prism : Tensor ns (Vect n a) -> Tensor (n :: ns) a

toVectT : Vect n Nat -> Type -> Type
toVectT [] a = a
toVectT (x :: xs) a = toVectT xs (Vect x a)

toTensor : toVectT xs a -> Tensor xs a
toTensor {xs = []} v = Scalar v
toTensor {xs = (x :: xs)} v = Prism (toTensor v)

toVect : Tensor xs a -> toVectT xs a
toVect {xs = []} (Scalar v) = v
toVect {xs = (x :: xs)} (Prism v) = toVect v

tabulate : (Fin n -> a) -> Vect n a
tabulate {n = Z} _ = []
tabulate {n = S k} f = f FZ :: tabulate (f . FS)

Functor (Tensor ns) where
  map f (Scalar x) = Scalar (f x)
  map f (Prism x) = Prism (map (map f) x)

Foldable (Tensor ns) where
  foldr {ns = []} f acc (Scalar x) = f x acc
  foldr {ns = (n :: ns)} f acc (Prism x) = foldr (\x, acc => foldr f acc x) acc x

Applicative (Tensor ns) where
  pure {ns = []} x = Scalar x
  pure {ns = (n :: ns)} x = Prism (pure (pure x))

  (<*>) {ns = []} (Scalar f) (Scalar x) = Scalar (f x)
  (<*>) {ns = (n :: ns)} (Prism f) (Prism x) = Prism ((<*>) <$> f <*> x)

Traversable (Tensor ns) where
  traverse {ns = []} f (Scalar x) = map Scalar (f x)
  traverse {ns = (n :: ns)} f (Prism x) = map Prism (traverse (traverse f) x)

Show a => Show (Tensor ns a) where
  show (Scalar x) = show x
  show (Prism x) = show x

Num a => Num (Tensor ns a) where
  (+) {ns = []} (Scalar x) (Scalar y) = Scalar (x + y)
  (+) {ns = (n :: ns)} (Prism x) (Prism y) = Prism (x + y)
  (*) {ns = []} (Scalar x) (Scalar y) = Scalar (x * y)
  (*) {ns = (n :: ns)} (Prism x) (Prism y) = Prism (x * y)
  fromInteger {ns = []} i = Scalar (fromInteger i)
  fromInteger {ns = (n :: ns)} i = Prism (fromInteger i)

example : Tensor [2, 2] Int
example = Prism (Prism (Scalar [[1, 2], [3, 4]]))

test : Tensor [2, 2] Int
test = map (\x => x * 2) example

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Setter
import Control.Lens.Types
import Control.Monad.Identity
import Data.Profunctor

%default total

public export
sets : ((a -> b) -> s -> t) -> Setter s t a b
sets l (Mor f) = Mor $ Id . l (runIdentity . f)

public export
over : Setter s t a b -> (a -> b) -> s -> t
over l f = runIdentity . applyMor (l (Mor (Id . f)))

public export
set : Setter s t a b -> b -> s -> t
set l b = over l (const b)

infixr 4 .~
public export
(.~) : Setter s t a b -> b -> s -> t
(.~) = set

infixr 4 &~
public export
(&~) : Setter s t a b -> (a -> b) -> s -> t
(&~) = over

-- & is a special character and can't be used
infixl 1 |>
public export
(|>) : a -> (a -> b) -> b
(|>) a f = f a

public export
mapped : Functor f => LensLike Identity (f a) (f b) a b
mapped = sets map

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


text:
-- ------------------------------------------------------------- [ Encrypt.idr ]
-- Module      : Encrypt
-- Description : Classes for Encryption operations.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Std.Encrypt

import Crypto.Common
import Crypto.Nonce
import Crypto.Message

import Crypto.Std.Key

||| Description of a Authenticated PKE Scheme.
|||
class AuthPKEncScheme s where
  ||| Generate Public Private Key Pair.
  apkeKeyGen  : (Key Public Asymm n, Key Private Asymm m)

  ||| Encrypt a message.
  |||
  ||| @ n The Nonce
  ||| @ recvenc The receiver's public key.
  ||| @ senddec The sender's private key.
  ||| @ msg The plainttext to be encrypted.
  apkeEncrypt : (n : Nonce Asymm Random a)
               -> (recvenc : Key Public Asymm b)
               -> (senddec : Key Private Asymm c)
               -> (msg : Message d)
               -> Maybe (Encrypted e)

  ||| Decrypted a ciphertext.
  |||
  ||| @ n The nonce.
  ||| @ sendenc The sender's public key.
  ||| @ recvdec The receiver's private key.
  ||| @ ctxt The ciphertext to be decrypted.
  apkeDecrypt : (n : Nonce Asymm Random a)
               -> (sendenc : Key Public Asymm c)
               -> (recvdec : Key Private Asymm b)
               -> (ctxt : Encrypted e)
               -> Maybe (Message d)

||| Description of an Symmetric Encryption Scheme.
|||
class SymmScheme s where
  ||| Generate a symmetric key.
  symmKeyGen  : (Key Private Symm n)

  ||| Encrypt a msg.
  |||
  ||| @ n The nonce.
  ||| @ k The secret key.
  ||| @ msg The plaintext to be encrypted.
  symmEncrypt : (n : Nonce Symm Random a)
                -> (k : Key Private Symm b)
                -> (msg : Message c)
                -> Maybe (Encrypted d)

  ||| Decrypt a ciphertext
  |||
  ||| @ n The nonce
  ||| @ k The secret key.
  ||| @ ctxt The ciphertext to be decrypted.
  symmDecrypt : (n : Nonce Symm Random a)
                -> (k : Key Private Symm b)
                -> (ctxt : Encrypted d)
                -> Maybe (Message c)

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

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Compiler.VMCode

import Compiler.ANF

import Core.CompileExpr
import Core.Context
import Core.Core
import Core.TT

import Libraries.Data.IntMap
import Data.List
import Data.Maybe
import Data.Vect

%default covering

public export
data Reg : Type where
     RVal : Reg
     Loc : Int -> Reg
     Discard : Reg

-- VM instructions - first Reg is where the result goes, unless stated
-- otherwise.

-- As long as you have a representation of closures, and an 'apply' function
-- which adds an argument and evaluates if it's fully applied, then you can
-- translate this directly to a target language program.
public export
data VMInst : Type where
     DECLARE : Reg -> VMInst
     START : VMInst -- start of the main body of the function
     ASSIGN : Reg -> Reg -> VMInst
     MKCON : Reg -> (tag : Either Int Name) -> (args : List Reg) -> VMInst
     MKCLOSURE : Reg -> Name -> (missing : Nat) -> (args : List Reg) -> VMInst
     MKCONSTANT : Reg -> Constant -> VMInst

     APPLY : Reg -> (f : Reg) -> (a : Reg) -> VMInst
     CALL : Reg -> (tailpos : Bool) -> Name -> (args : List Reg) -> VMInst
     OP : {0 arity : Nat} -> Reg -> PrimFn arity -> Vect arity Reg -> VMInst
       --  ^ we explicitly bind arity here to silence the warnings it is shadowing
       -- an existing global definition
     EXTPRIM : Reg -> Name -> List Reg -> VMInst

     CASE : Reg -> -- scrutinee
            (alts : List (Either Int Name, List VMInst)) -> -- based on constructor tag
            (def : Maybe (List VMInst)) ->
            VMInst
     CONSTCASE : Reg -> -- scrutinee
                 (alts : List (Constant, List VMInst)) ->
                 (def : Maybe (List VMInst)) ->
                 VMInst
     PROJECT : Reg -> (value : Reg) -> (pos : Int) -> VMInst
     NULL : Reg -> VMInst

     ERROR : String -> VMInst

public export
data VMDef : Type where
     MkVMFun : (args : List Int) -> List VMInst -> VMDef
     MkVMForeign : (ccs : List String) -> (fargs : List CFType) ->
                   CFType -> VMDef
     MkVMError : List VMInst -> VMDef

export
Show Reg where
  show RVal = "RVAL"
  show (Loc i) = "v" ++ show i
  show Discard = "DISCARD"

export
Show VMInst where
  show (DECLARE r) = "DECLARE " ++ show r
  show START = "START"
  show (ASSIGN r v) = show r ++ " := " ++ show v
  show (MKCON r t args)
      = show r ++ " := MKCON " ++ show t ++ " (" ++
                  showSep ", " (map show args) ++ ")"
  show (MKCLOSURE r n m args)
      = show r ++ " := MKCLOSURE " ++ show n ++ " " ++ show m ++ " (" ++
                  showSep ", " (map show args) ++ ")"
  show (MKCONSTANT r c) = show r ++ " := MKCONSTANT " ++ show c
  show (APPLY r f a) = show r ++ " := " ++ show f ++ " @ " ++ show a
  show (CALL r t n args)
      = show r ++ " := " ++ (if t then "TAILCALL " else "CALL ") ++
        show n ++ "(" ++ showSep ", " (map show args) ++ ")"
  show (OP r op args)
      = show r ++ " := " ++ "OP " ++
        show op ++ "(" ++ showSep ", " (map show (toList args)) ++ ")"
  show (EXTPRIM r n args)
      = show r ++ " := " ++ "EXTPRIM " ++
        show n ++ "(" ++ showSep ", " (map show args) ++ ")"

  show (CASE scr alts def)
      = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}"
  show (CONSTCASE scr alts def)
      = "CASE " ++ show scr ++ " " ++ show alts ++ " {default: " ++ show def ++ "}"

  show (PROJECT r val pos)
      = show r ++ " := PROJECT(" ++ show val ++ ", " ++ show pos ++ ")"
  show (NULL r) = show r ++ " := NULL"
  show (ERROR str) = "ERROR " ++ show str

export
Show VMDef where
  show (MkVMFun args body) = show args ++ ": " ++ show body
  show (MkVMForeign ccs args ret)
      = "Foreign call " ++ show ccs ++ " " ++
        show args ++ " " ++ show ret
  show (MkVMError err) = "Error: " ++ show err

toReg : AVar -> Reg
toReg (ALocal i) = Loc i
toReg ANull = Discard

projectArgs : Int -> Int -> (used : IntMap ()) -> (args : List Int) -> List VMInst
projectArgs scr i used [] = []
projectArgs scr i used (arg :: args)
    = case lookup arg used of
           Just _ => PROJECT (Loc arg) (Loc scr) i :: projectArgs scr (i + 1) used args
           Nothing => projectArgs scr (i + 1) used args

collectReg : Reg -> IntMap ()
collectReg (Loc i) = singleton i ()
collectReg _ = empty

collectUsed : VMInst -> IntMap ()
collectUsed (DECLARE reg) = collectReg reg
collectUsed START = empty
collectUsed (ASSIGN _ val) = collectReg val
collectUsed (MKCON _ _ args) = foldMap collectReg args
collectUsed (MKCLOSURE _ _ _ args) = foldMap collectReg args
collectUsed (MKCONSTANT _ _) = empty
collectUsed (APPLY _ fn arg) = collectReg fn <+> collectReg arg
collectUsed (CALL _ _ _ args) = foldMap collectReg args
collectUsed (OP _ _ args) = foldMap collectReg args
collectUsed (EXTPRIM _ _ args) = foldMap collectReg args
collectUsed (CASE sc is mdef)
    = collectReg sc
      <+> foldMap (foldMap collectUsed . snd) is
      <+> maybe empty (foldMap collectUsed) mdef
collectUsed (CONSTCASE sc is mdef)
    = collectReg sc
      <+> foldMap (foldMap collectUsed . snd) is
      <+> maybe empty (foldMap collectUsed) mdef
collectUsed (PROJECT _ val _) = collectReg val
collectUsed (NULL _) = empty
collectUsed (ERROR _) = empty

toVM : (tailpos : Bool) -> (target : Reg) -> ANF -> List VMInst
toVM t Discard _ = []
toVM t res (AV fc (ALocal i))
    = [ASSIGN res (Loc i)]
toVM t res (AAppName fc _ n args)
    = [CALL res t n (map toReg args)]
toVM t res (AUnderApp fc n m args)
    = [MKCLOSURE res n m (map toReg args)]
toVM t res (AApp fc _ f a)
    = [APPLY res (toReg f) (toReg a)]
toVM t res (ALet fc var val body)
    = toVM False (Loc var) val ++ toVM t res body
toVM t res (ACon fc n ci (Just tag) args)
    = [MKCON res (Left tag) (map toReg args)]
toVM t res (ACon fc n ci Nothing args)
    = [MKCON res (Right n) (map toReg args)]
toVM t res (AOp fc _ op args)
    = [OP res op (map toReg args)]
toVM t res (AExtPrim fc _ p args)
    = [EXTPRIM res p (map toReg args)]
toVM t res (AConCase fc (ALocal scr) [MkAConAlt n ci mt args code] Nothing) -- exactly one alternative, so skip matching
    = let body = toVM t res code
          used = foldMap collectUsed body
       in projectArgs scr 0 used args ++ body
toVM t res (AConCase fc (ALocal scr) alts def)
    = [CASE (Loc scr) (map toVMConAlt alts) (map (toVM t res) def)]
  where
    toVMConAlt : AConAlt -> (Either Int Name, List VMInst)
    toVMConAlt (MkAConAlt n ci tag args code)
       = let body = toVM t res code
             used = foldMap collectUsed body
          in (maybe (Right n) Left tag, projectArgs scr 0 used args ++ body)
toVM t res (AConstCase fc (ALocal scr) alts def)
    = [CONSTCASE (Loc scr) (map toVMConstAlt alts) (map (toVM t res) def)]
  where
    toVMConstAlt : AConstAlt -> (Constant, List VMInst)
    toVMConstAlt (MkAConstAlt c code)
        = (c, toVM t res code)
toVM t res (APrimVal fc c)
    = [MKCONSTANT res c]
toVM t res (AErased fc)
    = [NULL res]
toVM t res (ACrash fc err)
    = [ERROR err]
toVM t res _
    = [NULL res]

findVars : VMInst -> List Int
findVars (ASSIGN (Loc r) _) = [r]
findVars (MKCON (Loc r) _ _) = [r]
findVars (MKCLOSURE (Loc r) _ _ _) = [r]
findVars (MKCONSTANT (Loc r) _) = [r]
findVars (APPLY (Loc r) _ _) = [r]
findVars (CALL (Loc r) _ _ _) = [r]
findVars (OP (Loc r) _ _) = [r]
findVars (EXTPRIM (Loc r) _ _) = [r]
findVars (CASE _ alts d)
    = foldMap findVarAlt alts ++ fromMaybe [] (map (foldMap findVars) d)
  where
    findVarAlt : (Either Int Name, List VMInst) -> List Int
    findVarAlt (t, code) = foldMap findVars code
findVars (CONSTCASE _ alts d)
    = foldMap findConstVarAlt alts ++ fromMaybe [] (map (foldMap findVars) d)
  where
    findConstVarAlt : (Constant, List VMInst) -> List Int
    findConstVarAlt (t, code) = foldMap findVars code
findVars (PROJECT (Loc r) _ _) = [r]
findVars _ = []

declareVars : List Int -> List VMInst -> List VMInst
declareVars got code
    = let vs = foldMap findVars code in
          declareAll got vs
  where
    declareAll : List Int -> List Int -> List VMInst
    declareAll got [] = START :: code
    declareAll got (i :: is)
        = if i `elem` got
             then declareAll got is
             else DECLARE (Loc i) :: declareAll (i :: got) is

export
toVMDef : ANFDef -> Maybe VMDef
toVMDef (MkAFun args body)
    = Just $ MkVMFun args (declareVars args (toVM True RVal body))
toVMDef (MkAForeign ccs cargs ret)
    = Just $ MkVMForeign ccs cargs ret
toVMDef (MkAError body)
    = Just $ MkVMError (declareVars [] (toVM True RVal body))
toVMDef _ = Nothing

export
allDefs : List (Name, ANFDef) -> List (Name, VMDef)
allDefs = mapMaybe (\ (n, d) => do d' <- toVMDef d; pure (n, d'))


text:
module Data.Trifunctor

%default total
%access public export

||| Zifunctor is abstraction over description of computation t that:
||| takes r as input (reader, input)
||| produce result a (a result)
||| or produce error of type e
||| Progression of abstractions: Functor => Bifunctor, Profunctor => Zifunctor
||| Zifunctor combine capabilities of Functor, Bifunctor, Profunctor and add more
interface Zifunctor (t : Type -> Type -> Type -> Type) where
  zimap : (rr -> r) -> (e -> ee) -> (a -> aa) -> t r e a -> t rr ee aa

  bimap : (e -> ee) -> (a -> aa) -> t r e a -> t r ee aa
  bimap = zimap id

  dimap : (rr -> r) -> (a -> aa) -> t r e a -> t rr e aa
  dimap r = zimap r id

  dimapLeft : (rr -> r) -> (e -> ee) -> t r e a -> t rr ee a
  dimapLeft r e = zimap r e id

  map : (a -> aa) -> t r e a -> t r e aa
  map = zimap id id

  mapLeft : (e -> ee) -> t r e a -> t r ee a
  mapLeft e = zimap id e id

  contramap : (rr -> r) -> t r e a -> t rr e a
  contramap r = zimap r id id

-- TODO Zifunctor implementation for r -> Either e a
-- TODO Zifunctor implementation for r -> (e,a)
-- TODO Zifunctor implementation for Bifunctor b => r -> b e a

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module DepSec.Ref

import public DepSec.Labeled
import public DepSec.DIO
import Data.IORef

%access export

||| Secure reference
data SecRef : (l : labelType) -> (valueType : Type) -> Type where
  ||| TCB
  MkSecRef : (ref : IORef a) -> SecRef l a

||| Create a reference with a labeled intial value
||| @ flow evidence that l may flow to l'
||| @ flow' evidence that l' may flow to l''
||| @ value initial value
newRef : Poset labelType
      => {l, l', l'' : labelType}
      -> {auto flow : l `leq` l'}
      -> {auto flow' : l' `leq` l''}
      -> (value : Labeled l' a)
      -> DIO l (SecRef l'' a)
newRef (MkLabeled v)
  = lift $ newIORef v >>= pure . MkSecRef

||| Read a secure reference
||| @ flow evidence that l may flow to l'
||| @ ref reference to read
readRef : Poset labelType
       => {l, l' : labelType}
       -> {auto flow : l `leq` l'}
       -> (ref  : SecRef l' a)
       -> DIO l (Labeled l' a)
readRef (MkSecRef ioRef)
  = lift $ map MkLabeled $ readIORef ioRef

||| Write a labeled value to a secure reference
||| @ flow evidence that l may flow to l'
||| @ flow' evidence that l' may flow to l''
||| @ ref reference to write to
||| @ content value to write to reference
writeRef : Poset labelType
        => {l, l', l'' : labelType}
        -> {auto flow : l `leq` l'}
        -> {auto flow' : l' `leq` l''}
        -> (ref : SecRef l'' a)
        -> (content : Labeled l' a)
        -> DIO l ()
writeRef (MkSecRef ioRef) (MkLabeled content)
  = lift $ writeIORef ioRef content

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Extra.Monad

||| Function to sequence two functors
||| TODO: Can we do this with applicative instead of monad?
export
map2 : Monad m => (a -> b -> c) -> m a -> m b -> m c
map2 f x y =
  join $ map (\x' => map (\y' => f x' y') y) x

||| Function to sequence three functors
export
map3 : Monad m => (a -> b -> c -> d) -> m a -> m b -> m c -> m d
map3 f x y z =
  (map2 f x y) <*> z

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- Reads Runtime Length Encoded files
-- containing a Game of Life
module Conway.RLE

import Conway.Conway

-- map all uppercase to lowercase
lower : (List String) -> (List String)
lower = map toLower

-- Remove whitespace
removeWS : (List String) -> (List String)
removeWS = map (\s => pack $ filter (\c => not $ isSpace c) (unpack s))

-- Remove Comments from RLE
removeComments : (List String) -> (List String)
removeComments = filter (\s => not $ isEmptyOrComment $ unpack s)
  where isEmptyOrComment : List Char -> Bool
        isEmptyOrComment [] = True
        isEmptyOrComment (x::xs) = x == '#'

compress : (List String) -> (List String)
compress [] = []
compress (x::xs) = x::[concat xs]

-- Functions for Parsing a String into an Int
charToInt : Char -> Maybe Int
charToInt c = let i = cast {to=Int} c in
              let zero = cast {to=Int} '0' in
              let nine = cast {to=Int} '9' in
              if i < zero || i > nine
                then Nothing
                else Just (i - zero)

parseInt : String -> Maybe Int
parseInt s = parseInt' (unpack s)
  where
    parseInt' : List Char -> Maybe Int
    parseInt' [] = Nothing
    parseInt' s@(x::xs) = parseInt'' 0 s
      where parseInt'' : Int -> List Char -> Maybe Int
            parseInt'' i [] = Just i
            parseInt'' i (x::xs) = case charToInt x of
                          Just n => do
                            let i' = (i * 10) + n
                            parseInt'' i' xs
                          Nothing => Nothing

-- Obtain dimensions x * y of Conway board
getDimensions : (List String) -> Maybe (Int, Int)
getDimensions [] = Nothing
getDimensions (x::xs) = getDim x
  where getDim : String -> Maybe (Int, Int)
        getDim s = case (pack $ take 2 $ unpack s) of
              "x=" => do
                        x <- parseInt (pack $ takeWhile (/= ',') (drop 2 $ unpack s))
                        case (pack $ take 3 s2) of
                          ",y=" => do
                              y <- parseInt (pack $ drop 3 s2)
                              pure (x, y)
                          _ => Nothing
              _ => Nothing

        where
            s2 : List Char
            s2 = dropWhile (/= ',') $ unpack s

getInitial : Int -> (List String) -> Maybe (List (List CellState))
getInitial _ [] = Nothing
getInitial _ (x1::[]) = Nothing
getInitial y (x1::x2::xs) = getInitial' y (unpack x2)
  where
        next : (List Char) -> Maybe (List Char)
        next xs = case dropWhile (/= '$') xs of
                    [] => Nothing
                    (x::xs) => Just xs

        getN : (List Char) -> Maybe (Nat, List Char)
        getN xs = case (takeWhile isDigit) xs of
                    [] => Just (1, xs)
                    digits => do
                      n <- parseInt (pack digits)
                      pure (cast n, drop (length digits) xs)

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

        getLine : (List Char) -> Maybe (List (CellState))
        getLine ('$'::xs) = Just []
        getLine xs = do
          numNext <- getN xs
          case (snd numNext) of
            ('b'::xs) => liftA (\l => (repeatN (fst numNext) Dead) ++ l)  (getLine xs)
            ('o'::xs) => liftA (\l => (repeatN (fst numNext) Alive) ++ l) (getLine xs)
            _        => Nothing

        getInitial' : Int  -> (List Char) -> Maybe (List (List CellState))
        getInitial' 0 _ = Just []
        getInitial' y xs = do
            first <- getLine xs
            nextItems <- next xs
            rest <- getInitial' (y - 1) nextItems
            pure (first::rest)

getConway : List (String) -> Maybe (List (List CellState))
getConway lines = do
  dimensions <- getDimensions lines
  getInitial (snd dimensions) lines

export
readCFile : String -> IO (Maybe (List (List CellState)))
readCFile fName = do
  readFileRes <- readFile fName
  case readFileRes of
    Left err => pure Nothing
    Right str => do
      let strLines = lines str
      let noWSLines = compress $ removeWS $ removeComments $ strLines
      pure $ getConway noWSLines

max_stars_repo_name: RossMeikleham/Idris-Conway

max_issues_repo_name: RossMeikleham/Idris-Conway

max_forks_repo_name: RossMeikleham/Idris-Conway


text:
{-
Ni!
Ni!
Ni!
-}
module Main

knight : IO ()
knight = putStrLn "Ni!"

knights : Stream (IO ())
knights = repeat knight

main : IO ()
main = for_ (take 3 knights) id

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Solutions.Folds

import Data.Maybe
import Data.SnocList
import Data.Vect

%default total

--------------------------------------------------------------------------------
--          Recursion
--------------------------------------------------------------------------------

-- 1

anyList : (a -> Bool) -> List a -> Bool
anyList p []        = False
anyList p (x :: xs) = case p x of
  False => anyList p xs
  True  => True

allList : (a -> Bool) -> List a -> Bool
allList p []        = True
allList p (x :: xs) = case p x of
  True  => allList p xs
  False => False

-- 2

findList : (a -> Bool) -> List a -> Maybe a
findList f []        = Nothing
findList f (x :: xs) = if f x then Just x else findList f xs

-- 3

collectList : (a -> Maybe b) -> List a -> Maybe b
collectList f []        = Nothing
collectList f (x :: xs) = case f x of
  Just vb => Just vb
  Nothing => collectList f xs

-- Note utility function `Data.Maybe.toMaybe` in the implementation
lookupList : Eq a => a -> List (a,b) -> Maybe b
lookupList va = collectList (\(k,v) => toMaybe (k == va) v)

-- 4

mapTR : (a -> b) -> List a -> List b
mapTR f = go Lin
  where go : SnocList b -> List a -> List b
        go sx []        = sx <>> Nil
        go sx (x :: xs) = go (sx :< f x) xs

-- 5

filterTR : (a -> Bool) -> List a -> List a
filterTR f = go Lin
  where go : SnocList a -> List a -> List a
        go sx []        = sx <>> Nil
        go sx (x :: xs) = if f x then go (sx :< x) xs else go sx xs

-- 6

mapMaybeTR : (a -> Maybe b) -> List a -> List b
mapMaybeTR f = go Lin
  where go : SnocList b -> List a -> List b
        go sx []        = sx <>> Nil
        go sx (x :: xs) = case f x of
          Just vb => go (sx :< vb) xs
          Nothing => go sx xs

catMaybesTR : List (Maybe a) -> List a
catMaybesTR = mapMaybeTR id

-- 7

concatTR : List a -> List a -> List a
concatTR xs ys = (Lin <>< xs) <>> ys

-- 8

bindTR : List a -> (a -> List b) -> List b
bindTR xs f = go Lin xs
  where go : SnocList b -> List a -> List b
        go sx []        = sx <>> Nil
        go sx (x :: xs) = go (sx <>< f x) xs

joinTR : List (List a) -> List a
joinTR = go Lin
  where go : SnocList a -> List (List a) -> List a
        go sx []        = sx <>> Nil
        go sx (x :: xs) = go (sx <>< x) xs

--------------------------------------------------------------------------------
--          A few Notes on Totality Checking
--------------------------------------------------------------------------------

record Tree a where
  constructor Node
  value  : a
  forest : List (Tree a)

Forest : Type -> Type
Forest = List . Tree

example : Tree Bits8
example = Node 0 [Node 1 [], Node 2 [Node 3 [], Node 4 [Node 5 []]]]

mutual
  treeSize : Tree a -> Nat
  treeSize (Node _ forest) = S $ forestSize forest

  forestSize : Forest a -> Nat
  forestSize []        = 0
  forestSize (x :: xs) = treeSize x + forestSize xs

-- 1

mutual
  treeDepth : Tree a -> Nat
  treeDepth (Node _ forest) = S $ forestDepth forest

  forestDepth : Forest a -> Nat
  forestDepth []        = 0
  forestDepth (x :: xs) = max (treeDepth x) (forestDepth xs)

-- 2

-- It's often easier to write complex interface implementations
-- via a utility function.
--
-- Of course, we could also use a `mutual` block as with
-- `treeSize` and `forestSize` here.
treeEq : Eq a => Tree a -> Tree a -> Bool
treeEq (Node v1 f1) (Node v2 f2) = v1 == v2 && go f1 f2
  where go : Forest a -> Forest a -> Bool
        go []        []        = True
        go (x :: xs) (y :: ys) = treeEq x y && go xs ys
        go _         _         = False

Eq a => Eq (Tree a) where (==) = treeEq

-- 3

treeMap : (a -> b) -> Tree a -> Tree b
treeMap f (Node value forest) = Node (f value) (go forest)
  where go : Forest a -> Forest b
        go []        = []
        go (x :: xs) = treeMap f x :: go xs

Functor Tree where map = treeMap

-- 4

treeShow : Show a => Prec -> Tree a -> String
treeShow p (Node value forest) =
  showCon p "Node" $ showArg value ++ case forest of
    []      => " []"
    x :: xs => " [" ++ treeShow Open x ++ go xs ++ "]"

  where go : Forest a -> String
        go []        = ""
        go (y :: ys) = ", " ++ treeShow Open y ++ go ys

Show a => Show (Tree a) where showPrec = treeShow

-- 5

mutual
  treeToVect : (tr : Tree a) -> Vect (treeSize tr) a
  treeToVect (Node value forest) = value :: forestToVect forest

  forestToVect : (f : Forest a) -> Vect (forestSize f) a
  forestToVect []        = []
  forestToVect (x :: xs) = treeToVect x ++ forestToVect xs

--------------------------------------------------------------------------------
--          Interface Foldable
--------------------------------------------------------------------------------

-- 1

data Crud : (i : Type) -> (a : Type) -> Type where
  Create : (value : a) -> Crud i a
  Update : (id : i) -> (value : a) -> Crud i a
  Read   : (id : i) -> Crud i a
  Delete : (id : i) -> Crud i a

Foldable (Crud i) where
  foldr acc st (Create value)   = acc value st
  foldr acc st (Update _ value) = acc value st
  foldr _   st (Read _)         = st
  foldr _   st (Delete _)       = st

  foldl acc st (Create value)   = acc st value
  foldl acc st (Update _ value) = acc st value
  foldl _   st (Read _)         = st
  foldl _   st (Delete _)       = st

  null (Create _)   = False
  null (Update _ _) = False
  null (Read _)     = True
  null (Delete _)   = True

  foldMap f (Create value)   = f value
  foldMap f (Update _ value) = f value
  foldMap _ (Read _)         = neutral
  foldMap _ (Delete _)       = neutral

  foldlM acc st (Create value)   = acc st value
  foldlM acc st (Update _ value) = acc st value
  foldlM _   st (Read _)         = pure st
  foldlM _   st (Delete _)       = pure st

  toList (Create v)   = [v]
  toList (Update _ v) = [v]
  toList (Read _)     = []
  toList (Delete _)   = []

-- 2

data Response : (e, i, a : Type) -> Type where
  Created : (id : i) -> (value : a) -> Response e i a
  Updated : (id : i) -> (value : a) -> Response e i a
  Found   : (values : List a) -> Response e i a
  Deleted : (id : i) -> Response e i a
  Error   : (err : e) -> Response e i a

Foldable (Response e i) where
  foldr acc st (Created _ value) = acc value st
  foldr acc st (Updated _ value) = acc value st
  foldr acc st (Found values)    = foldr acc st values
  foldr _   st (Deleted _)       = st
  foldr _   st (Error _)         = st

  foldl acc st (Created _ value) = acc st value
  foldl acc st (Updated _ value) = acc st value
  foldl acc st (Found values)    = foldl acc st values
  foldl _   st (Deleted _)       = st
  foldl _   st (Error _)         = st

  null (Created _ _)     = False
  null (Updated _ _)     = False
  null (Found values)    = null values
  null (Deleted _)       = True
  null (Error _)         = True

  foldMap f (Created _ value) = f value
  foldMap f (Updated _ value) = f value
  foldMap f (Found values)    = foldMap f values
  foldMap f (Deleted _)       = neutral
  foldMap f (Error _)         = neutral

  toList (Created _ value) = [value]
  toList (Updated _ value) = [value]
  toList (Found values)    = values
  toList (Deleted _)       = []
  toList (Error _)         = []

  foldlM acc st (Created _ value) = acc st value
  foldlM acc st (Updated _ value) = acc st value
  foldlM acc st (Found values)    = foldlM acc st values
  foldlM _   st (Deleted _)       = pure st
  foldlM _   st (Error _)         = pure st

-- 3

data List01 : (nonEmpty : Bool) -> Type -> Type where
  Nil  : List01 False a
  (::) : a -> List01 False a -> List01 ne a

list01ToList : List01 ne a -> List a
list01ToList = go Lin
  where go : SnocList a -> List01 ne' a -> List a
        go sx []        = sx <>> Nil
        go sx (x :: xs) = go (sx :< x) xs

list01FoldMap : Monoid m => (a -> m) -> List01 ne a -> m
list01FoldMap f = go neutral
  where go : m -> List01 ne' a -> m
        go vm []        = vm
        go vm (x :: xs) = go (vm <+> f x) xs

Foldable (List01 ne) where
  foldr acc st []        = st
  foldr acc st (x :: xs) = acc x (foldr acc st xs)

  foldl acc st []        = st
  foldl acc st (x :: xs) = foldl acc (acc st x) xs

  null []       = True
  null (_ :: _) = False

  toList = list01ToList

  foldMap = list01FoldMap

  foldlM _ st []        = pure st
  foldlM f st (x :: xs) = f st x >>= \st' => foldlM f st' xs

-- 4

mutual
  foldrTree : (el -> st -> st) -> st -> Tree el -> st
  foldrTree f v (Node value forest) = f value (foldrForest f v forest)

  foldrForest : (el -> st -> st) -> st -> Forest el -> st
  foldrForest _ v []        = v
  foldrForest f v (x :: xs) = foldrTree f (foldrForest f v xs) x

mutual
  foldlTree : (st -> el -> st) -> st -> Tree el -> st
  foldlTree f v (Node value forest) = foldlForest f (f v value) forest

  foldlForest : (st -> el -> st) -> st -> Forest el -> st
  foldlForest _ v []        = v
  foldlForest f v (x :: xs) = foldlForest f (foldlTree f v x) xs

mutual
  foldMapTree : Monoid m => (el -> m) -> Tree el -> m
  foldMapTree f (Node value forest) = f value <+> foldMapForest f forest

  foldMapForest : Monoid m => (el -> m) -> Forest el -> m
  foldMapForest _ []        = neutral
  foldMapForest f (x :: xs) = foldMapTree f x <+> foldMapForest f xs

mutual
  toListTree : Tree el -> List el
  toListTree (Node value forest) = value :: toListForest forest

  toListForest : Forest el -> List el
  toListForest []        = []
  toListForest (x :: xs) = toListTree x ++ toListForest xs

mutual
  foldlMTree : Monad m => (st -> el -> m st) -> st -> Tree el -> m st
  foldlMTree f v (Node value forest) =
    f v value >>= \v' => foldlMForest f v' forest

  foldlMForest : Monad m => (st -> el -> m st) -> st -> Forest el -> m st
  foldlMForest _ v []        = pure v
  foldlMForest f v (x :: xs) =
    foldlMTree f v x >>= \v' => foldlMForest f v' xs

Foldable Tree where
  foldr   = foldrTree
  foldl   = foldlTree
  foldMap = foldMapTree
  foldlM  = foldlMTree
  null _  = False
  toList  = toListTree

-- 5

record Comp (f,g : Type -> Type) (a : Type) where
  constructor MkComp
  unComp  : f (g a)

Foldable f => Foldable g => Foldable (Comp f g) where
  foldr f st (MkComp v)  = foldr (flip $ foldr f) st v
  foldl f st (MkComp v)  = foldl (foldl f) st v
  foldMap f (MkComp v)   = foldMap (foldMap f) v
  foldlM f st (MkComp v) = foldlM (foldlM f) st v
  toList (MkComp v)      = foldMap toList v
  null (MkComp v)        = all null v

record Product (f,g : Type -> Type) (a : Type) where
  constructor MkProduct
  fst : f a
  snd : g a

Foldable f => Foldable g => Foldable (Product f g) where
  foldr f st (MkProduct v w)  = foldr f (foldr f st w) v
  foldl f st (MkProduct v w)  = foldl f (foldl f st v) w
  foldMap f (MkProduct v w)   = foldMap f v <+> foldMap f w
  toList  (MkProduct v w)     = toList v ++ toList w
  null (MkProduct v w)        = null v && null w
  foldlM f st (MkProduct v w) = foldlM f st v >>= \st' => foldlM f st' w

--------------------------------------------------------------------------------
--          Tests
--------------------------------------------------------------------------------

iterateTR : Nat -> (a -> a) -> a -> List a
iterateTR k f = go k Lin
  where go : Nat -> SnocList a -> a -> List a
        go 0     sx _ = sx <>> Nil
        go (S k) sx x = go k (sx :< x) (f x)

values : List Integer
values = iterateTR 100000 (+1) 0

main : IO ()
main = do
  printLn . length $ mapTR (*2)  values
  printLn . length $ filterTR (\n => n `mod` 2 == 0)  values
  printLn . length $ mapMaybeTR (\n => toMaybe (n `mod` 2 == 1) "foo")  values
  printLn . length $ concatTR values values
  printLn . length $ bindTR [1..500] (\n => iterateTR n (+1) n)


text:
> module Basic.Properties

> import Basic.Operations

> %default total

> %access public export

* Replace properties:

> |||
> replaceLemma : {a : _} -> {x : _} -> {y : _} -> {P : a -> Type} ->
>                (prf : x = y) -> (px : P x) -> replace prf px = px
> replaceLemma Refl px = Refl

> |||
> replaceLemma2 : {A : Type} -> {P : A -> Type} -> {Q : (a : A) -> P a -> Type} ->
>                 {a1 : A} -> {a2 : A} ->
>                 (f : (a : A) -> (pa : P a) -> Q a pa) ->
>                 (prf : a1 = a2) ->
>                 (pa2 : P a2) ->
>                 f a1 (replace (sym prf) pa2) = f a2 pa2
> replaceLemma2 f Refl pa2 = Refl

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Decidable.Equality

data DivisiblebyX : Nat -> Nat -> Type where
  Base: DivisiblebyX x x
  Multiple: DivisiblebyX x y -> DivisiblebyX x (x+y)

data FizzBuzzProof: Nat -> Type where
  Fizz: DivisiblebyX 3 x -> (DivisiblebyX 5 x -> Void) -> FizzBuzzProof x
  Buzz: DivisiblebyX 5 x -> (DivisiblebyX 3 x -> Void) -> FizzBuzzProof x
  FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProof x
  Normal: (x: Nat) -> (DivisiblebyX 3 x -> Void) ->(DivisiblebyX 5 x -> Void) -> FizzBuzzProof x

Show (FizzBuzzProof x) where
  show (Fizz _ _) = "fizz"
  show (Buzz _ _) = "buzz"
  show (FizzBuzz _ _) = "fizzbuzz"
  show (Normal x _ _) = show x

threeLessNotDivisible3 : (notdiv : DivisiblebyX 3 (S y) -> Void) -> DivisiblebyX 3 (3 + (S y)) -> Void
threeLessNotDivisible3 notdiv (Multiple x) = notdiv x

zeroNotDivisible3 : DivisiblebyX 3 0 -> Void
zeroNotDivisible3 Base impossible
zeroNotDivisible3 (Multiple _) impossible

oneNotDivisible3 : DivisiblebyX 3 1 -> Void
oneNotDivisible3 Base impossible
oneNotDivisible3 (Multiple _) impossible

twoNotDivisible3 : DivisiblebyX 3 2 -> Void
twoNotDivisible3 Base impossible
twoNotDivisible3 (Multiple _) impossible

divisibleby3: (y: Nat) -> Dec (DivisiblebyX 3 y)
divisibleby3 Z = No zeroNotDivisible3
divisibleby3 (S Z) = No oneNotDivisible3
divisibleby3 (S (S Z)) = No twoNotDivisible3
divisibleby3 (S (S (S Z))) = Yes Base
divisibleby3 (S (S (S (S y)))) = case divisibleby3 (S y) of
  Yes prf => Yes (Multiple prf)
  No notdiv => No (threeLessNotDivisible3 notdiv)

zeroNotDivisible5 : DivisiblebyX 5 0 -> Void
zeroNotDivisible5 Base impossible
zeroNotDivisible5 (Multiple _) impossible

oneNotDivisible5 : DivisiblebyX 5 1 -> Void
oneNotDivisible5 Base impossible
oneNotDivisible5 (Multiple _) impossible

twoNotDivisible5 : DivisiblebyX 5 2 -> Void
twoNotDivisible5 Base impossible
twoNotDivisible5 (Multiple _) impossible

threeNotDivisible5 : DivisiblebyX 5 3 -> Void
threeNotDivisible5 Base impossible
threeNotDivisible5 (Multiple _) impossible

fourNotDivisible5 : DivisiblebyX 5 4 -> Void
fourNotDivisible5 Base impossible
fourNotDivisible5 (Multiple _) impossible

fiveLessNotDivisible5 : (notdiv : DivisiblebyX (fromInteger 5) (S y) -> Void) -> DivisiblebyX 5 (S (S (S (S (S (S y)))))) -> Void
fiveLessNotDivisible5 notdiv (Multiple x) = notdiv x

divisibleby5: (y: Nat) -> Dec (DivisiblebyX 5 y)
divisibleby5 Z = No zeroNotDivisible5
divisibleby5 (S Z) = No oneNotDivisible5
divisibleby5 (S (S Z)) = No twoNotDivisible5
divisibleby5 (S (S (S Z))) = No threeNotDivisible5
divisibleby5 (S (S (S (S Z)))) = No fourNotDivisible5
divisibleby5 (S (S (S (S (S Z))))) = Yes Base
divisibleby5 (S (S (S (S (S (S y)))))) = case divisibleby5 (S y) of
  Yes prf => Yes (Multiple prf)
  No notdiv => No (fiveLessNotDivisible5 notdiv)

fizzbuzz: (x: Nat) -> FizzBuzzProof x
fizzbuzz x = case (divisibleby3 x, divisibleby5 x) of
  (No not_fizz, No not_buzz) => Normal x not_fizz not_buzz
  (Yes fizz_prf, Yes buzz_prf) => FizzBuzz fizz_prf buzz_prf
  (No not_fizz, Yes buzz_prf) => Buzz buzz_prf not_fizz
  (Yes fizz_prf, No not_buzz) => Fizz fizz_prf not_buzz

fizzbuzz_string: (x: Nat) -> String
fizzbuzz_string x = show $ fizzbuzz x

fizzbuzz_loop: (n: Nat) -> (end: Nat) -> IO ()
fizzbuzz_loop n end with (decEq n end)
  fizzbuzz_loop n end | Yes prf = pure ()
  fizzbuzz_loop n end | No contra =  do
    putStrLn $ show $ fizzbuzz n
    fizzbuzz_loop (S n) end

main: IO ()
main = fizzbuzz_loop 1 101


text:
cfn : Bool -> Nat
cfn = \case
  bar => ?cfn_rhs


text:
module Part2.Sez10_3_hiding

-- export type, not constructors (symilar to typical approach in Haskell)
export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

-- export these instead of constructors (symilar to typical approach in Haskell)
-- only in Idris we can pattern match on these!
export
triangle : Double -> Double -> Shape
triangle = Triangle

export
rectangle : Double -> Double -> Shape
rectangle = Rectangle

export
circle : Double -> Shape
circle = Circle

-- exports view (with contructors for client to pattern match on) instead of
-- Shape constructors
-- note exported functions used on the RHS of constructors
public export
data ShapeView : Shape -> Type where
     STriangle : ShapeView (triangle base height)
     SRectangle : ShapeView (rectangle width height)
     SCircle : ShapeView (circle radius)

export
shapeView : (s : Shape) -> ShapeView s
shapeView (Triangle x y) = STriangle
shapeView (Rectangle x y) = SRectangle
shapeView (Circle x) = SCircle

-- example client code
-- can use elaborate pattern match that reflects on the RHS of ShapeView
-- using exported functions
area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = pi * radius * radius

{-
*Part2/Sez10_3_hiding> area (circle 1)
3.141592653589793 : Double
-}

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
> module Nat.Positive

> import Syntax.PreorderReasoning

> import Unique.Predicates
> import Subset.Properties

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

> |||
> data Positive : Nat -> Type where
>   MkPositive  : {n : Nat} -> Positive (S n)

> |||
> PositiveUnique : {n : Nat} -> Unique (Positive n)
> PositiveUnique MkPositive MkPositive = Refl

> |||
> fromSucc : (m : Nat) -> (n : Nat) -> S m = n -> Positive n
> fromSucc m n prf = s2 where
>   s1 : Positive (S m)
>   s1 = MkPositive
>   s2 : Positive n
>   s2 = replace prf s1

> |||
> implementation Uninhabited (Positive Z) where
>   uninhabited (MkPositive {n}) impossible

> |||
> positiveNotZ : {n : Nat} -> Positive n -> Not (n = Z)
> positiveNotZ {n = Z}   p = absurd p
> positiveNotZ {n = S m} _ = SIsNotZ

> |||
> plusPreservesPositivity : Positive m -> Positive n -> Positive (m + n)
> plusPreservesPositivity {m = Z  } {n      } MkPositive _            impossible
> plusPreservesPositivity {m      } {n = Z  } _          MkPositive   impossible
> plusPreservesPositivity {m = S m} {n = S n} _          _          = MkPositive

> |||
> multPreservesPositivity : Positive m -> Positive n -> Positive (m * n)
> multPreservesPositivity {m = Z  } {n      } MkPositive _            impossible
> multPreservesPositivity {m      } {n = Z  } _          MkPositive   impossible
> multPreservesPositivity {m = S m} {n = S n} _          _          = MkPositive


text:
module GrinFFI

public export
int_print : Int -> IO ()
int_print i
   = foreign FFI_C "idris_int_print" (Int -> IO ()) i

public export
bool_print : Bool -> IO ()
bool_print b =
  foreign FFI_C "idris_int_print" (Int -> IO ()) $
  case b of
    False => 0
    True  => 1

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module IdrisWeb.Common.Date
import Builtins
%access public

{- Simple date and time records.
   Like, really simple. They'll do for now.

   Allows date serialisation and deserialisation as per
   RFC822, which is used when setting cookies.

   TODO: Timezones, timestamp, comparison

-}

data Day = Monday
         | Tuesday
         | Wednesday
         | Thursday
         | Friday
         | Saturday
         | Sunday

data Month = January
           | February
           | March
           | April
           | May
           | June
           | July
           | August
           | September
           | October
           | November
           | December

-- Not using the show typeclass for cookies, since there are so many
-- different ways of showing dates.
showCookieDay : Day -> String
showCookieDay Monday = "Mon"
showCookieDay Tuesday = "Tue"
showCookieDay Wednesday = "Wed"
showCookieDay Thursday = "Thu"
showCookieDay Friday = "Fri"
showCookieDay Saturday = "Sat"
showCookieDay Sunday = "Sun"

--private
{-
divides : Integer -> Integer -> Bool
divides x y = (x `mod` y) == 0

isLeapYear : (year : Integer) -> Bool
isLeapYear y = if divides y 400 then True
                   else if divides y 100 then False
                   else if divides y 4 then True
                   else False

--  where y : Nat
  --      y = cast year
  -}

isLeapYear : (year : Integer) -> Bool
isLeapYear year = if (y `mod` 400) == O then True
                   else if (y `mod` 100) == O then False
                   else if (y `mod` 4) == O then True
                   else False
  where y : Nat
        y = cast year

daysInMonth : Month -> (year : Integer) -> Int
daysInMonth September _ = 30
daysInMonth April _ = 30
daysInMonth June _ = 30
daysInMonth November _ = 30
daysInMonth February y = if isLeapYear y then 29
                                         else 28
daysInMonth _ _ = 31

dayOfWeek : (year : Integer) -> (month : Integer) -> (day : Integer) -> Int
dayOfWeek year month day = d + (2.6 * m)
  where y = if (month == 1 || month == 2) then year - 1 else year
        m = (month - 2) `mod` 12
        d = daysInMonth month

public
record Date : Type where
  MkDate : (day : Integer) ->
           (month : Integer) ->
           (year : Integer) -> Date

public
record DateTime : Type where
  MkDateTime : (day : Integer) ->
               (month : Integer) ->
               (year : Integer) ->
               (hour : Integer) ->
               (minute : Integer) ->
               (second : Integer) ->
               DateTime

-- Why everyone can't just use the ISO one, I'll never know...
-- Wed, 13 Jan 2021 22:23:01 GMT
--abstract
--showCookieTime : DateTime -> String
--showCookieTime dt

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Main

next : Nat -> Stream Nat
next n = (n :: Delay (next (S n)))

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

-- sugar me with do-notation
(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

-- First try, infinite IO with partial run

loopPrint : Nat -> InfIO
loopPrint x = do putStrLn (show x)
                 loopPrint (S x)

run : InfIO -> IO ()
run (Do x f) = do res <- x
                  run (f res)

-- Second try, finine infinite IO with total run

data Fuel : Type where
  Dry : Fuel
  More : Fuel -> Fuel

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

total runTank : Fuel -> InfIO -> IO ()
runTank Dry _ = putStrLn "Out of Fuel"
runTank (More fuel) (Do c f) = do res <- c
                                  runTank fuel (f res)

-- Third try, Lazy Fuel for infinite infinite IO with a total run

data Gas : Type where
  Empty : Gas
  Some : Lazy Gas -> Gas

data Run : Type where
  Stop : Run
  Step : Lazy Run -> Run

total runEngine : Gas -> InfIO -> IO ()
runEngine Empty y = putStrLn "Out of fuel"
runEngine (Some x) (Do y f) = y >>= \res => runEngine x (f res)

freeGas : Gas
freeGas = Some freeGas

main : IO ()
main = runEngine freeGas (loopPrint 0)

h : Nat -> () -> Nat
h x = \_ => (+) x 1

h' : Nat -> Lazy Nat
h' x = (+) x 1

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
-- ----------------------------------------------------------------- [ DSL.idr ]
-- Module    : DSL.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Build a Sif Model from the AST.
module Sif.DSL

-- ----------------------------------------------------------------- [ Imports ]
import Effects
import Effect.State
import Effect.Default
import Effect.Perf
import Effect.File
import Effect.Exception
import Effect.Logging.Default

import Lightyear
import Lightyear.Strings

import Sif.Types
import Sif.AbsSyntax
import Sif.Error

import Sif.Pattern

import Sif.DSL.State
import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution
import Sif.DSL.Parser

-- -------------------------------------------------------------- [ Directives ]
%access private
%default partial

-- @TODO de exception this...

-- ----------------------------------------------------------- [ Build Helpers ]

getBuildState : Eff BuildState ['bstate ::: STATE BuildState]
getBuildState = pure $ !('bstate :- get)

putBuildState : BuildState -> Eff () ['bstate ::: STATE BuildState]
putBuildState st = 'bstate :- put st

updateBuildState : (BuildState -> BuildState) -> Eff () ['bstate ::: STATE BuildState]
updateBuildState f = 'bstate :- update (\st => f st)

public export
DSLBuilder : Type -> Type
DSLBuilder rTy = Eff rTy [ FILE_IO ()
                         , LOG
                         , PERF
                         , 'sif    ::: EXCEPTION SifError
                         , 'bstate ::: STATE BuildState
                         ]

-- ----------------------------------------------------------- [ Build Problem ]

buildReqE : SifBuilder impl
         -> (d : SifDomain)
         -> SifAST TyREQ
         -> DSLBuilder $ REQUIREMENT impl d
buildReqE bob c q@(Req i ty t d) = do
  st <- getBuildState
  case lookup i (getRQs st) of
    Just x  => Sif.raise (DuplicateID i)
    Nothing => do
      let r = mkRequirement bob c ty t d
      putBuildState (record { getRQs = (i,q) :: (getRQs st)} st)
      pure r

buildProblemE : SifBuilder impl
             -> (d : SifDomain)
             -> SifAST TyPROBLEM
             -> DSLBuilder (PROBLEM impl d)
buildProblemE bob d (Problem i t d' _ rs) = do
    trace "Building problem specification"
    rs' <- mapE (\r => buildReqE bob d r) rs
    splitTimerMsg (getPFName !getBuildState) "Building Requirements"
    let p = mkProblem bob d t d' rs'
    updateBuildState (\st => record { getProbID     = Just i
                                    , pattTitle   = t} st)
    pure p

problemFromAST : SifBuilder impl
              -> (d : SifDomain)
              -> SifAST TyPROBLEM
              -> DSLBuilder (PROBLEM impl d)
problemFromAST bob d past = do
    mkTimer (getPFName !getBuildState)
    startTimer (getPFName !getBuildState)
    rval <- buildProblemE bob d past
    stopTimer (getPFName !getBuildState)
    pure $ rval

-- ---------------------------------------------------------- [ Build Solution ]

buildAffectE : SifBuilder impl
            -> (d : SifDomain)
            -> SifAST TyAFFECTS
            -> DSLBuilder (AFFECT impl d)
buildAffectE bob ctxt (Affect c i d) = do
  debug $ unwords ["Building Affect for", show i]
  st <- getBuildState
  case lookup i (getRQs st) of
    Nothing => Sif.raise (IDMissing i)
    Just (Req i' ty t d')  => do
      let r = mkRequirement bob ctxt ty t d'
      pure $ mkAffect bob ctxt c r d

buildTraitE : SifBuilder impl
           -> (d : SifDomain)
           -> SifAST TyTRAIT
           -> DSLBuilder (TRAIT impl d)
buildTraitE bob c (Trait ty t v d as) = do
  debug $ unwords ["Building Trait", show t]
  as' <- mapE (\x => buildAffectE bob c x) as
  splitTimerMsg (getSFName !getBuildState) "Building Affects"
  pure $ mkTrait bob c ty t d v as'

buildPropertyE : SifBuilder impl
              -> (d : SifDomain)
              -> SifAST TyPROPERTY
              -> DSLBuilder (PROPERTY impl d)
buildPropertyE bob c (Property t d ts) = do
  debug $ unwords ["Building Property", show t]
  ts' <- mapE (\x => buildTraitE bob c x) ts
  splitTimerMsg (getSFName !getBuildState) "Building Traits"
  pure $ mkProperty bob c t d ts'

buildSolutionE : SifBuilder impl
              -> (d : SifDomain)
              -> SifAST TySOLUTION
              -> DSLBuilder (SOLUTION impl d)
buildSolutionE bob d (Solution t (pID, pDesc) d' _ ps) = do
  trace "Building solution specification"
  st <- getBuildState
  trace "Comparing "
  case getProbID st of
    Nothing   => Sif.raise InternalErr
    Just pID' => do
      case (not (pID' == pID)) of
        True => Sif.raise (MismatchError pID pID')
        False => do
          ps' <- mapE (\p => buildPropertyE bob d p) ps
          splitTimerMsg (getSFName !getBuildState) "Building Properties"
          updateBuildState (\st => record
              { pattTitle = unwords [pattTitle st, "through",t]
              , pattDesc = pDesc
              } st)
          pure $ mkSolution bob d t d' ps'

solutionFromAST : SifBuilder impl
              -> (d : SifDomain)
              -> SifAST TySOLUTION
              -> DSLBuilder (SOLUTION impl d)
solutionFromAST bob d sast = do
    mkTimer (getSFName !getBuildState)
    startTimer (getSFName !getBuildState)
    sval <- buildSolutionE bob d sast
    stopTimer (getSFName !getBuildState)
    pure sval

-- ----------------------------------------------------------------- [ Pattern ]

buildPatternE : SifBuilder impl
             -> (d : SifDomain)
             -> PROBLEM impl d
             -> SOLUTION impl d
             -> DSLBuilder (PATTERN impl d)
buildPatternE bob c p s = do
    st <- getBuildState
    trace $ unwords ["Building Pattern", show $ pattTitle st]
    let res = mkPattern bob c (pattTitle st) (pattDesc st) p s
    splitTimerMsg (unwords [ "Building for "
                           , getPFName st
                           , "&"
                           , getSFName st]) "Finished Pattern"
    pure res

export
patternFromFile : SifBuilder impl
               -> String
               -> String
               -> DSLBuilder (d ** PATTERN impl d)
patternFromFile bob pfile sfile = do
  putBuildState (defBuildSt pfile sfile)

  trace "Parsing Specifications"
  splitTimerMsg (unwords ["Building for ", pfile, "&", sfile])
                "Starting Parsing"

  (Right past) <- readSifFile problem pfile  | Left err => Sif.raise err

  splitTimerMsg (unwords ["Building for ", pfile, "&", sfile])
                "Finished problem parsing"

  (Right sast) <- readSifFile solution sfile | Left err => Sif.raise err
  splitTimerMsg (unwords ["Building for ", pfile, "&", sfile])
                "Finished solution parsing"

  trace "Comparing Context of Solution and Problem"
  case compatible past sast of
    Nothing => Sif.raise ContextMismatch
    Just d  => do
      p' <- problemFromAST bob d past

      splitTimerMsg (unwords ["Building for ", pfile, "&", sfile])
                   "Finished Problem now Solution"

      s' <- solutionFromAST bob d sast

      splitTimerMsg (unwords ["Building for ", pfile, "&", sfile])
                   "Finished Solution now Pattern"

      res <- buildPatternE bob d p' s'
      pure (d ** res)

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
-- ---------------------------------------------------------------- [ YAML.idr ]
-- Description : Parse YAML files.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.YAML

import Effects
import Effect.File
import Effect.Exception

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

import public Config.Error

import Config.Parse.Common
import Config.Parse.Utils

%access private

-- ------------------------------------------------------------------- [ Model ]

||| YAML Documentation representation.
|||
||| There is no support for:
||| + Anchors
||| + Complex Maps
||| + Schema's
||| + User Defined tags
||| + Interesting Scalar Formats
public export
data YAMLNode : Type where
  -- Value Types
  YAMLNull   : YAMLNode
  YAMLString : String -> YAMLNode
  YAMLInt    : Int    -> YAMLNode
  YAMLFloat  : Double -> YAMLNode
  YAMLBool   : Bool   -> YAMLNode
  -- Node Types
  YAMLScalar : String -> YAMLNode
  YAMLSeq    : List YAMLNode -> YAMLNode
  YAMLMap    : List (YAMLNode, YAMLNode) -> YAMLNode
  -- Documents
  YAMLDoc    : List (String, String) -> YAMLNode -> YAMLNode

normaliseLiterals : String -> String
normaliseLiterals s = s

public export
Show YAMLNode where
  -- Value Types
  show YAMLNull       = "!!null \"null\""
  show (YAMLString x) = "!!str " ++ show x
  show (YAMLInt i)    = "!!int " ++ show i
  show (YAMLFloat f)  = "!!float " ++ show f
  show (YAMLBool b)   = "!!bool " ++ show b
  -- Node Types
  show (YAMLScalar s) = "!!str " ++ show (normaliseLiterals s)
  show (YAMLSeq ys)   = "!!seq " ++ show ys
  show (YAMLMap ys)   = "!!map " ++ "{" ++
      unwords (intersperse "," (map showKV ys))++ "}"
     where
       showKV : (YAMLNode, YAMLNode) -> String
       showKV (k,v) = show k ++ " : " ++ show v
  -- Documents
  show (YAMLDoc _ x) = "%YAML 1.2\n---\n" ++ show x ++ "\n...\n"

showUnTyped : YAMLNode -> String
showUnTyped YAMLNull       = "null"
showUnTyped (YAMLString x) = x
showUnTyped (YAMLInt i)    = show i
showUnTyped (YAMLFloat f)  = show f
showUnTyped (YAMLBool b)   = show b
-- Node Types
showUnTyped (YAMLScalar s) = show (normaliseLiterals s)
showUnTyped (YAMLSeq ys)   = unwords ["["
      , unwords $ intersperse "," (map showUnTyped ys)
      , "]"]
showUnTyped (YAMLMap ys)   = unwords ["{"
      , unwords (intersperse "," (map showUnTypedKV ys))
      ,"}"]
   where
     showUnTypedKV : (YAMLNode, YAMLNode) -> String
     showUnTypedKV (k,v) = with List concat [showUnTyped k, ": ", showUnTyped  v]
-- Documents
showUnTyped (YAMLDoc _ x) = unlines ["%YAML 1.2","---", showUnTyped x,"..."]

public export
implementation [yamlUnTyped] Show YAMLNode where
  show x = showUnTyped x

-- ------------------------------------------------------------------ [ Parser ]

-- [ Values ]
yamlString : Parser YAMLNode
yamlString = map YAMLString word <?> "YAML String"

yamlNull : Parser YAMLNode
yamlNull = token "null" >! pure YAMLNull <?> "YAML Null"

yamlBool : Parser YAMLNode
yamlBool = do token "false"; pure $ YAMLBool False
       <|> do token "true";  pure $ YAMLBool True
       <?> "YAML Boolean"

yamlFloat : Parser YAMLNode
yamlFloat = map YAMLFloat $ map scientificToFloat parseScientific <?> "YAML Floats"

yamlInt : Parser YAMLNode
yamlInt = do
    num <- map pack (some $ satisfy isDigit)
    pure $ YAMLInt (cast num)
  <?> "YAML Int"

yamlNum : Parser YAMLNode
yamlNum = yamlFloat <|> yamlInt <?> "YAML Num"

-- [ Scalars ]

yamlQuotedScalar : Parser YAMLNode
yamlQuotedScalar = yamlQuoteGen '\'' <|> yamlQuoteGen '\"' <?> "YAML Qoted Scalar"
  where
    yamlQuoteGen : Char -> Parser YAMLNode
    yamlQuoteGen c = do
        ws <- quoted c
        spaces
        pure $ YAMLScalar $ ws
      <?> "YAML Scalar General"

yamlFlowValue : Parser YAMLNode
yamlFlowValue = yamlNull
            <|> yamlBool
            <|> yamlNum
            <|> yamlQuotedScalar
            <|> yamlStrs
             <?> "YAML Primitives"
  where
    yamlStrs : Parser YAMLNode
    yamlStrs = do
      ws <- some $ lexeme asciiSeq
      pure $ YAMLString $ unwords ws

-- [ Nodes ]
yamlFlowSeq : Parser YAMLNode
yamlFlowSeq = do
    xs <- brackets (commaSep (lexeme yamlFlowValue))
    spaces
    pure $ YAMLSeq xs
   <?> "YAML Flow Sequence"

yamlKVPair : Parser (YAMLNode, YAMLNode)
yamlKVPair = do
   key <- yamlString
   colon
   value <- yamlFlowValue
   pure $ (key, value)
  <?> "YAML KV Pair Flow"

yamlFlowMap : Parser YAMLNode
yamlFlowMap = do
    xs <- braces (commaSep (lexeme yamlKVPair))
    spaces
    pure $ YAMLMap xs
  <?> "YAML Flow Map"

yamlSentance : Parser YAMLNode
yamlSentance = do
  ws <- manyTill (spaces *> word) endOfLine
  pure $ YAMLString $ unwords ws

-- ------------------------------------------------------------------ [ Blocks ]
yamlObject : Parser YAMLNode
yamlObject = yamlNull <|> yamlBool <|> yamlNum <|> yamlQuotedScalar
         <|> yamlSentance <|> yamlFlowSeq <|> yamlFlowMap
         <?> "YAMLValue"

yamlBlockSeq : Parser YAMLNode
yamlBlockSeq = do
    xs <- some (token "-" *!> yamlObject <* spaces)
    pure $ YAMLSeq xs
  <?> "YAML List Sequence"

yamlBlockKVPair : Parser (YAMLNode, YAMLNode)
yamlBlockKVPair = do
    key <- yamlString
    colon
    spaces
    value <- yamlObject
    pure $ (key, value)
  <?> "YAML Block KV Pair"

yamlBlockMap : Parser YAMLNode
yamlBlockMap = do
    xs <- some (yamlBlockKVPair <* spaces)
    pure $ YAMLMap xs
  <?> "Map Block"

yamlDirective : Parser (String, String)
yamlDirective = do
    string "%"
    k <- word
    spaces
    v <- manyTill anyChar endOfLine
    pure $ (k, pack v)
  <?> "YAML Directive"

||| This does not recognise:
|||  + keep or strip options
|||  + indent options
|||  + Inline Comments.
|||  + Scalar Blocks
|||  + Complext Block Map and Block Seq, these only take flow nodes.
export
parseYAMLDoc : Parser YAMLNode
parseYAMLDoc = do
    ds <- some yamlDirective
    token "---"
    b <- body
    opt $ token "..."
    pure $ YAMLDoc ds b
   <?> "YAML Document"
  where
    body : Parser YAMLNode
    body = yamlBlockMap <|> yamlBlockSeq

||| This does not recognise:
|||  + keep or strip options
|||  + indent options
|||  + Inline Comments.
|||  + Scalar Blocks
|||  + Complext Map and Seq Blocks
export
parseYAMLStream : Parser (List YAMLNode)
parseYAMLStream = some parseYAMLDoc

-- ------------------------------------------------------------------ [ String ]
export
toString : YAMLNode -> String
toString doc = show @{yamlUnTyped} doc

export
toStringTyped : YAMLNode -> String
toStringTyped doc = show doc

||| Requires that the file is untyped
|||
||| This does not recognise:
|||  + keep or strip options
|||  + indent options
|||  + Inline Comments.
|||  + Scalar Blocks
|||  + Complext Map and Seq Blocks
export
fromString : String -> Either ConfigError YAMLNode
fromString str =
    case parse parseYAMLDoc str of
      Left err  => Left (PureParseErr err)
      Right doc => Right doc

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

||| This does not recognise:
|||  + keep or strip options
|||  + indent options
|||  + Inline Comments.
|||  + Scalar Blocks
|||  + Complext Map and Seq Blocks
export
readYAMLConfig : String -> Eff (Either ConfigError YAMLNode) [FILE ()]
readYAMLConfig = readConfigFile parseYAMLDoc

||| This does not recognise:
|||  + keep or strip options
|||  + indent options
|||  + Inline Comments.
|||  + Scalar Blocks
|||  + Complext Map and Seq Blocks
export
readYAMLStream : String -> Eff (List YAMLNode) [FILE ()]
readYAMLStream inStr =
    case !(readConfigFile parseYAMLStream inStr) of
      Left _   => pure Nil
      Right ds => pure ds

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
> module NonNegDouble.open_issues.Main

> import Data.So

> %default total
> %access public export

> data NonNegative : Double -> Type where
>   MkNonNegative : {x : Double} -> So (0.0 <= x) -> NonNegative x

> NonNegDouble : Type
> NonNegDouble = Subset Double NonNegative

> plus : NonNegDouble -> NonNegDouble -> NonNegDouble
> mult : NonNegDouble -> NonNegDouble -> NonNegDouble
> fromNat : Nat -> NonNegDouble

> implementation Num NonNegDouble where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat


text:
module Main

record Point where
  constructor MkPoint
  x : Double
  y : Double

-- a record creates two projections:
--
-- .x : Point -> Double
-- .y : Point -> Double
--
-- because %prefix_record_projections are on by default, we also get:
--
-- x : Point -> Double
-- y : Point -> Double

-- to prevent cluttering the ordinary name space with short identifiers
%prefix_record_projections off

record Rect where
  constructor MkRect
  topLeft : Point
  bottomRight : Point

-- .topLeft : Rect -> Point
-- .bottomRight : Rect -> Point
--
-- For Rect, we don't get the prefix projections:
--
-- Main> :t topLeft
-- (interactive):1:4--1:11:Undefined name topLeft
-- Main> :t .topLeft
-- \{rec:0} => .topLeft rec : ?_ -> Point

pt : Point
pt = MkPoint 4.2 6.6

rect : Rect
rect =
  MkRect
    (MkPoint 1.1 2.5)
    (MkPoint 4.3 6.3)

-- New lexical structure:
--
-- Foo.bar.baz with uppercase F is one lexeme: NSIdent ["baz", "bar", "Foo"]
-- foo.bar.baz with lowercase f is three lexemes: foo, .bar, .baz
-- .foo.bar.baz is three lexemes: .foo, .bar, .baz
--
-- If you want Constructor.field, you have to write (Constructor).field.
--
-- New syntax of simpleExpr:
--
-- Expressions binding tighter than application (simpleExpr),
-- such as variables or parenthesised expressions,
-- have been renamed to simplerExpr,
-- and an extra layer of syntax has been inserted.
--
--   simpleExpr ::= (.field)+               -- parses as PPostfixAppPartial
--                | simplerExpr (.field)+   -- parses as PPostfixApp
--                | simplerExpr             -- (parses as whatever it used to)
--
-- (.foo) is a name, so you can use it to e.g. define a function called .foo (see .squared below)
-- (.foo.bar) is a parenthesised expression
--
-- New desugaring rules
--
-- (.field1 .field2 .field3) desugars to (\x => .field3 (.field2 (.field1 x)))
-- (simpleExpr .field1 .field2 .field3) desugars to ((.field .field2 .field3) simpleExpr).
--
-- There are more details such as namespacing; see below.

-- user-defined projections work, too (should they?)
(.squared) : Double -> Double
(.squared) x = x * x

-- #649: Forced patterns remain unaffected by postfix projections.
test649 : (x, y : Bool) -> x = y -> Bool
test649 .(x) x Refl = x

-- #441: Locals do not shadow record projections.
test441 : (Point -> Double) -> (Point -> Double) -> Point -> Double
test441 x y pt = pt.x + pt.y
  -- no ambiguity errors: the locals "x" and "y" are not considered in pt.x and pt.y


text:
module Client.Skeleton.BaseWithTest.Package

import Fmt

export
name : (String, String) -> List String
name (packageNS, packageName) = [packageName ++ ".idr"]

export
build : (String, String) -> String
build (packageNS, packageName) = fmt """
module %s

main : IO ()
main =
  putStrLn \"Hello from %s.%s\"
""" packageName packageNS packageName


text:
module Control.Optics.Lens

import public Control.Optics.Types

export
lens : (prj : s -> a) -> (inj : s -> b -> t) -> Lens s t a b
lens prj inj (Mor f) = Mor (\s => inj s <$> f (prj s))


text:
module Text.Bounded

%default total

public export
record Bounds where
  constructor MkBounds
  startLine : Int
  startCol : Int
  endLine : Int
  endCol : Int

export
Show Bounds where
  showPrec d (MkBounds sl sc el ec) =
    showCon d "MkBounds" (concat [showArg sl, showArg sc, showArg el, showArg ec])

export
startBounds : Bounds -> (Int, Int)
startBounds b = (b.startLine, b.startCol)

export
endBounds : Bounds -> (Int, Int)
endBounds b = (b.endLine, b.endCol)

export
Eq Bounds where
  (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =
      sl == sl'
   && sc == sc'
   && el == el'
   && ec == ec'

public export
record WithBounds ty where
  constructor MkBounded
  val : ty
  isIrrelevant : Bool
  bounds : Bounds

export
start : WithBounds ty -> (Int, Int)
start = startBounds . bounds

export
end : WithBounds ty -> (Int, Int)
end = endBounds . bounds

export
Eq ty => Eq (WithBounds ty) where
  (MkBounded val ir bd) == (MkBounded val' ir' bd') =
    val == val' && ir == ir' && bd == bd'

export
Show ty => Show (WithBounds ty) where
  showPrec d (MkBounded val ir bd) =
    showCon d "MkBounded" (concat [showArg ir, showArg val, showArg bd])

export
Functor WithBounds where
  map f (MkBounded val ir bd) = MkBounded (f val) ir bd

export
Foldable WithBounds where
  foldr c n b = c b.val n

export
Traversable WithBounds where
  traverse f (MkBounded v a bd) = (\ v => MkBounded v a bd) <$> f v

export
irrelevantBounds : ty -> WithBounds ty
irrelevantBounds x = MkBounded x True (MkBounds (-1) (-1) (-1) (-1))

export
removeIrrelevance : WithBounds ty -> WithBounds ty
removeIrrelevance (MkBounded val ir bd) = MkBounded val True bd

export
mergeBounds : WithBounds ty -> WithBounds ty' -> WithBounds ty'
mergeBounds (MkBounded _ True _) (MkBounded val True _) = irrelevantBounds val
mergeBounds (MkBounded _ True _) b2 = b2
mergeBounds b1 (MkBounded val True _) = const val <$> b1
mergeBounds b1 b2 =
  let (ur, uc) = min (start b1) (start b2)
      (lr, lc) = max (end b1) (end b2) in
      MkBounded b2.val False (MkBounds ur uc lr lc)

export
joinBounds : WithBounds (WithBounds ty) -> WithBounds ty
joinBounds b = mergeBounds b b.val


text:
module Network.Curl.Easy

import System.File
import Data.Buffer

import Network.Curl.Easy.FFI
import Network.Curl.Easy.Enum

%default total

||| libcurl curl_easy raw objects
export
data Curl = CPtr AnyPtr

||| Extracts the raw AnyPtr to a libcurl curl object
export
unsafeCurlPtr : Curl -> AnyPtr
unsafeCurlPtr (CPtr ptr) = ptr

||| Create a new curl easy object. Never share between threads.
export
curl_easy_init : IO Curl
curl_easy_init = CPtr <$> primIO prim__curl_easy_init

||| Destroy a curl easy object. Do not pass Curl to anything else.
-- TODO: Enforce that every curl_easy_init is destroyed and never reused after
export
curl_easy_cleanup : Curl -> IO ()
curl_easy_cleanup (CPtr ptr) = primIO $ prim__curl_easy_cleanup ptr

public export
data ObjectPtr
    = ObjectPtrAny AnyPtr
    | ObjectPtrBuffer Buffer
    | ObjectPtrFile FilePtr

||| Idris 2 type representation of libcurl option types
public export
curlOptPrimitiveType : CurlOptType -> Type
curlOptPrimitiveType CurlOptTypeObjectpoint = ObjectPtr
curlOptPrimitiveType CurlOptTypeStringpoint = String
curlOptPrimitiveType CurlOptTypeLong = Bits64
curlOptPrimitiveType CurlOptTypeFunctionpoint = AnyPtr
curlOptPrimitiveType CurlOptTypeSlistpoint = Void -- Not implemented
curlOptPrimitiveType CurlOptTypeBlob = Void -- Not implemented
curlOptPrimitiveType CurlOptTypeOffT = Void -- Not implemented

-- Helper function for curl_easy_setopt with explicit type argument
private
curl_easy_setopt_typed : Curl
                       -> (optType : CurlOptType)
                       -> Int
                       -> curlOptPrimitiveType optType
                       -> IO CurlCode
curl_easy_setopt_typed (CPtr ptr) optType optCode param =
    map fromCode $ case optType of
        CurlOptTypeStringpoint => primIO $ prim__curl_easy_setopt_str ptr optCode param
        CurlOptTypeLong => primIO $ prim__curl_easy_setopt_long ptr optCode param
        CurlOptTypeFunctionpoint => primIO $ prim__curl_easy_setopt_file ptr optCode param
        CurlOptTypeObjectpoint =>
            case param of
                ObjectPtrAny op => primIO $ prim__curl_easy_setopt_ptr ptr optCode op
                ObjectPtrBuffer op => primIO $ prim__curl_easy_setopt_buf ptr optCode op
                ObjectPtrFile op => primIO $ prim__curl_easy_setopt_file ptr optCode op
        _ => pure $ toCode CurlENotBuiltIn

public export
parameterType : CurlOpt -> Type
parameterType = curlOptPrimitiveType . curlOptType

||| Set a curl easy option for the given curl object. Check libcurl reference for details.
export
curl_easy_setopt : Curl
                 -> (curlOpt : CurlOpt)
                 -> parameterType curlOpt
                 -> IO CurlCode
curl_easy_setopt curl opt param =
    curl_easy_setopt_typed curl (curlOptType opt) (toCode opt) param

||| Destroy a curl easy object. Do not pass Curl to anything else.
-- TODO: Enforce that every curl_easy_init is destroyed and never reused after
export
curl_easy_perform : Curl -> IO CurlCode
curl_easy_perform (CPtr ptr) = map fromCode . primIO $ prim__curl_easy_perform ptr


text:
||| Vertical composition of morphisms
module VertComp

import Data.Vect
import VectHelp
import ProcessLib
import Util
import Proto

%default total

-- TODO: we aren't handling any errors here
||| Connect two process
makeConnection: (w: DTy) ->
                (loc: Elem w cut_b) ->
                ProcPID (MkNiche cut_a cut_b) ->
                ProcPID (MkNiche cut_b cut_c) ->
                Process (ProcIF (MkNiche cut_a cut_c)) () Ready Ready
makeConnection (Down a) loc pid_f pid_g = do r <- Request pid_f (Conn (BotOutWire loc) pid_g (TopInWire loc))
                                             Action $ putStrLn $ "CONN: Down: " ++ show r
makeConnection (Up a)   loc pid_f pid_g = do r <- Request pid_g (Conn (TopOutWire loc) pid_f (BotInWire loc))
                                             Action $ putStrLn $ "CONN: Up  : " ++ show r

||| Connect two process that have a common cut
makeConnections: (cut_b: Cut m1) ->
                 ProcPID (MkNiche cut_a cut_b) ->
                 ProcPID (MkNiche cut_b cut_c) ->
                 Process (ProcIF (MkNiche cut_a cut_c)) () Ready Ready
makeConnections cut_b pid_f pid_g = let locs = allElems cut_b
  in sequence (map (\(dt ** loc) => makeConnection dt loc pid_f pid_g) locs)

||| Handle incoming requests
||| Just reroutes the requests to the appropriate morphism
resp: ProcPID (MkNiche cut_a cut_b) ->
      ProcPID (MkNiche cut_b cut_c) ->
      (msg : Req (MkNiche cut_a cut_c)) ->
      Process (ProcIF (MkNiche cut_a cut_c))
              (ProcIF (MkNiche cut_a cut_c) msg)
              Ready
              Ready
resp pid_f pid_g con@(Conn (TopOutWire _) _ _) = Request pid_f con
resp pid_f pid_g con@(Conn (BotOutWire _) _ _) = Request pid_g con
resp pid_f pid_g val@(Val (TopInWire _) _)     = do r <- Request pid_f val
                                                    --Action $ putStrLn $ "vert: reroute top val: " ++ show r
                                                    Pure r
resp pid_f pid_g val@(Val (BotInWire _) _)     = do r <- Request pid_g val
                                                    --Action $ putStrLn $ "vert: reroute bot val: " ++ show r
                                                    Pure r

infixl 3 -*-

||| Vertical composition of morphisms in the category of processes
public export partial
(-*-): {l,m,n: Nat} -> {cut_a: Cut l} -> {cut_b: Cut m} -> {cut_c: Cut n} ->
       Hom cut_a cut_b -> Hom cut_b cut_c -> Hom cut_a cut_c
(-*-) {cut_b} f g = do Just pid_f <- Spawn f | _ => do Action $ putStrLn "ERROR: (-*-): failed spawn 1"
                                                       f -*- g
                       Just pid_g <- Spawn g | _ => do Action $ putStrLn "ERROR: (-*-): failed spawn 2"
                                                       f -*- g
                       makeConnections cut_b pid_f pid_g
                       looper pid_f pid_g
  where
    looper : ProcPID (MkNiche cut_a cut_b) ->
             ProcPID (MkNiche cut_b cut_c) ->
             Process (ProcIF (MkNiche cut_a cut_c)) () Ready Looping
    looper pid_f pid_g = do --Action $ putStrLn $ "(-*-): normal loop"
                            Respond (resp pid_f pid_g)
                            Loop (looper pid_f pid_g)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Ch05.LambdaCalculus

import Ch03.Relations

%access public export

||| The type of variables
Variable : Type
Variable = Nat

||| The type of terms in the untyped lambda calculus
data Term = Var Variable
          | Abs Variable Term
          | App Term Term

||| Convenient infix notation for construction of function application terms
(.) : Term -> Term -> Term
(.) = App

-- TODO: Can we get rid of the argument `n`?
||| Convenience function for constructing lambda terms
lambda : Nat -> (Term -> Term) -> Term
lambda n f = Abs n (f (Var n))

MultiAppArgType : (numArgs : Nat) -> Type
MultiAppArgType Z = Term
MultiAppArgType (S k) = Term -> MultiAppArgType k

-- K_0 = id : a -> a
-- K : a -> b -> a
-- K_2 : a -> b -> b -> a
-- K_n : a -> b ... -> b -> a
--
-- K f t
-- K_2 f t1 t2 := K (K f t1) t2
--
-- K_{n+1} : a -> b -> .. -> b -> (b -> a)
-- K_{n+1} f x1 ... x{n+1} = K (K_n f x1 ... x_n) x_{n+1}

||| Convenience version of the `App` constructor that allows for a variable number of arguments.
multi_app : {numArgs : Nat} -> (MultiAppArgType numArgs -> Term)
multi_app {numArgs = Z} = \f => f
multi_app {numArgs = (S k)} = ?hole--(\f : Term => App f t) . (multi_app {numArgs=k})

data DirectSubterm : Term -> Term -> Type where
  IsAbsBody : {x : Variable} ->
              {t : Term} ->
              DirectSubterm t (Abs x t)
  IsAppFun : {f, x : Term} ->
             DirectSubterm f (App f x)

  IsAppArg : {f, x : Term} ->
             DirectSubterm x (App f x)

Subterm : Term -> Term -> Type
Subterm = ReflSymmClos DirectSubterm

-- vars (x) = {x}
-- vars (lambda x . t) = {x} \cup vars (t)
-- vars (f t) = vars(f) \cup vars(t)
--
-- bound_vars (x) = {}
-- bound_vars (lambda x . t) = \{x\} \cup bound_vars(t)
-- bound_vars (f t) = bound_vars(f) \cup bound_vars(t)
--
-- free_vars (x) = {}
-- free_vars (lambda x . t) = free_vars(t) - \{x\}
-- free_vars (f t) = free_vars(f) \cup free_vars(t)
--

namespace Occurs
  ||| Propositional type describing that a variable occurs in a term.
  data Occurs : Variable -> Term -> Type where
    IsVar : (x : Variable) ->
            Occurs x (Var x)

namespace OccursFree
  ||| Propositional type describing that a variable occurs freely in a term.
  data OccursFree : Variable -> Term -> Type where
    IsVar : (x : Variable) ->
            OccursFree x (Var x)
    InBody : {x,y : Variable} ->
             {t : Term} ->
             Not (x = y) ->
             OccursFree x t ->
             OccursFree x (Abs y t)
    InAppFun : {x : Variable} ->
               {f, t : Term} ->
               OccursFree x f ->
               OccursFree x (App f t)
    InAppArg : {x : Variable} ->
               {f, t : Term} ->
               OccursFree x t ->
               OccursFree x (App f t)

Closed : Term -> Type
Closed t = (x : Variable) -> Not (OccursFree x t)

namespace OccursBound
  ||| Propositional type describing that a variable occurs bound in a term.
  data OccursBound : Variable -> Term -> Type where

||| The identity combinator.
id : Term
id = Abs 0 (Var 0)

||| Proof that the identity combinator is closed.
id_is_closed : Closed Ch05.LambdaCalculus.id
id_is_closed x pf_occurs_free = case pf_occurs_free of
                                     (InBody pf_ne pf_in_t) => case pf_in_t of
                                                                    (IsVar Z) => pf_ne Refl

--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------

||| The Church boolean true
tru : Term
tru = Abs 1 (Abs 0 (Var 1))

||| The Church boolean false
fls : Term
fls = Abs 1 (Abs 0 (Var 0))

||| Church encoding of the if-then-else operator
test : Term
test = Abs 2 (Abs 1 (Abs 0 (App (App (Var 2) (Var 1)) (Var 0))))

||| Logical AND operator for Church booleans.
and : Term
and = Abs 0 (Abs 1 (App (App (Var 0) (Var 1)) fls))

--------------------------------------------------------------------------------
-- Pairs
--------------------------------------------------------------------------------

||| Church pair constructor
pair : Term
pair = Abs 0 (Abs 1 (Abs 2 (App (App (Var 2) (Var 0)) (Var 1))))

||| Projection onto the first component of a pair
fst : Term
fst = Abs 0 (Abs 1 (Var 0))

||| Projection onto the second component of a pair
snd : Term
snd = Abs 0 (Abs 1 (Var 1))

--------------------------------------------------------------------------------
-- Numerals
--------------------------------------------------------------------------------

||| The Church numeral zero.
church_zero : Term
church_zero = Abs 1 (Abs 0 (Var 0))

||| The Church numeral one.
church_one : Term
church_one = Abs 1 (Abs 0 (App (Var 1) (Var 0)))

||| The Church numeral two.
church_two : Term
church_two = Abs 1 (Abs 0 (App (Var 1) (App (Var 1) (Var 0))))

||| The successors function for Church numerals
scc : Term
scc = Abs 0 (Abs 1 (Abs 2 (App (Var 1) (App (App (Var 0) (Var 1)) (Var 2)))))

||| Addition of Church numerals
plus : Term
plus = Abs 0 (Abs 1 (Abs 2 (Abs 3 ((Var 0) . (Var 2)) . (((Var 1) . (Var 2)) . (Var 3)))))

||| Multiplication of Church numerals
times : Term
times = Abs 0 (Abs 1 ((Var 0) . (plus . (Var 1))) . church_zero)

||| Tests whether a Church numeral is zero or not
iszro : Term
iszro = Abs 0 ((Var 0) . (Abs 0 fls)) . tru

||| The predecessor function on Church numerals
prd : Term
prd = let zz = pair . church_zero . church_zero
          ss = Abs 0 (pair . (snd . (Var 0)) . (scc . (snd . (Var 0)))) in
          Abs 0 (fst . ((Var 0) . ss) . zz)

--------------------------------------------------------------------------------
-- Lists
--------------------------------------------------------------------------------

-- See Ch05.Exercise_5_2_8

--------------------------------------------------------------------------------
-- Self-replicating terms
--------------------------------------------------------------------------------

||| The (?) simplest self-replicating term in the lambda calculus
omega : Term
omega = let x = Var 0
            f = Abs 0 (x . x) in
            f . f

||| The call-by-value version of the fix-point combinator (i.e. Y combinator)
fix : Term
fix = let f = Var 0
          x = Var 1
          y = Var 2
          t = Abs 1 f . (Abs 2 (x . x . y)) in
          Abs 0 (t . t)

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Main

import Data.List

data Token : Type where
     TokenString : Token
     TokenNumber : Token
     TerminalWord : String -> Token
     TerminalChar : Char -> Token

tokenize : (xs : List Char) -> List Token
tokenize [] = []
tokenize ('%' :: 'd' :: chars) = TokenNumber :: tokenize(chars)
tokenize ('%' :: 's' :: chars) = TokenString :: tokenize(chars)
tokenize (c :: chars) = (TerminalChar c) :: tokenize(chars)

stringToTokens : String -> List Token
stringToTokens s = tokenize . unpack $ s

Formatter : (List Token) -> Type
Formatter [] = String
Formatter (x :: xs) = case x of
                           TokenNumber => (i : Int) -> Formatter xs
                           TokenString => (s : String) -> Formatter xs
                           _ => Formatter xs

printFmt : (tokens : List Token) -> (acc : String) -> Formatter tokens
printFmt [] acc = acc
printFmt (x :: xs) acc = case x of
                                       TokenNumber => (\i => printFmt xs (acc ++ show i))
                                       TokenString => \s => printFmt xs (acc ++ s)
                                       (TerminalWord w) => printFmt xs (acc ++ w)
                                       (TerminalChar c) => printFmt xs (acc ++ (strCons c ""))

||| поддерживает следующие шаблоны:
|||
||| - %d - целое число
||| - %s - строка
||| - %v - структура поддерживающая интерфейс Show
|||
||| Пример использования:
|||
||| printf "Привет мир от %s" "Ивана"
|||
||| printf "Я получил %d монет от %s" 100 "Михаила"
|||
||| printf "Структура Nat: %v" (S (S (S N)))
|||
printf : (template : String) -> Formatter (stringToTokens template)
printf template = printFmt (stringToTokens template) ""

main : IO ()
main = do
     putStrLn (printf "Hello, %s !" "UserName")
     putStrLn (printf "I have %d%s" 100 "$")
     putStrLn (printf "%s %d %s %d" "a" 10 "b" 10)

     -- Ошибочные случаи, когда мы не пройдем Type Checker:

     -- Type mistmatch beetween String -> String and String
     -- putStrLn (printf "%s %s" "hello")

     -- Type mistmatch between String and Int (expected type)
     -- putStrLn (printf "%d %s" "arg" 1)


text:
module Text.Html.Attribute

import Data.List
import Data.Maybe
import Data.String
import Text.Html.Event

%default total

public export
data Dir = LTR | RTL

export
Show Dir where
  show LTR = "ltr"
  show RTL = "rtl"

public export
data LoadType = Lzy | Eager

export
Show LoadType where
  show Lzy   = "lazy"
  show Eager = "eager"

public export
data InputType =
    Button
  | CheckBox
  | Color
  | Date
  | DateTime
  | Email
  | File
  | Image
  | Month
  | Number
  | Password
  | Radio
  | Range
  | Tel
  | Text
  | Time
  | URL
  | Week

export
Show InputType where
  show Button   = "button"
  show CheckBox = "checkbox"
  show Color    = "color"
  show Date     = "date"
  show DateTime = "datetime-local"
  show Email    = "email"
  show File     = "file"
  show Image    = "image"
  show Month    = "month"
  show Number   = "number"
  show Password = "password"
  show Radio    = "radio"
  show Range    = "range"
  show Tel      = "tel"
  show Text     = "text"
  show Time     = "time"
  show URL      = "url"
  show Week     = "week"

public export
data Attribute : (event : Type) -> Type where
  Id    : (value : String) -> Attribute event
  Str   : (name : String) -> (value : String) -> Attribute event
  Bool  : (name : String) -> (value : Bool) -> Attribute event
  Event : DOMEvent event -> Attribute event

public export
Attributes : Type -> Type
Attributes = List . Attribute

export
displayAttribute : Attribute ev -> Maybe String
displayAttribute (Id va)        = Just #"id="\#{va}""#
displayAttribute (Str nm va)    = Just #"\#{nm}="\#{va}""#
displayAttribute (Bool nm True) = Just nm
displayAttribute (Bool _ False) = Nothing
displayAttribute (Event _)      = Nothing

export
displayAttributes : Attributes ev -> String
displayAttributes = fastConcat . intersperse " " . mapMaybe displayAttribute

export
getId : Attributes ev -> Maybe String
getId (Id v       :: _) = Just v
getId (Str "id" v :: t) = Just v
getId (_          :: t) = getId t
getId []                = Nothing

export
getEvents : Attributes ev -> List (DOMEvent ev)
getEvents = go Nil
  where go : List (DOMEvent ev) -> Attributes ev -> List (DOMEvent ev)
        go es []              = es
        go es (Event e :: xs) = go (e :: es) xs
        go es (_ :: xs)       = go es xs

export
dispAttr : String -> (a -> String) -> a -> Attribute ev
dispAttr nm f =  Str nm . f

export
showAttr : Show a => String -> a -> Attribute ev
showAttr nm = dispAttr nm show

export %inline
accesskey : String -> Attribute ev
accesskey = Str "accesskey"

export %inline
action : String -> Attribute ev
action = Str "action"

export %inline
alt : String -> Attribute ev
alt = Str "alt"

export %inline
autocapitalize : Bool -> Attribute ev
autocapitalize = Bool "autocapitalize"

export %inline
autocomplete : Bool -> Attribute ev
autocomplete = Bool "autocomplete"

export %inline
autofocus : Bool -> Attribute ev
autofocus = Bool "autofocus"

export %inline
autoplay : Bool -> Attribute ev
autoplay = Bool "autoplay"

export %inline
checked : Bool -> Attribute ev
checked = Bool "checked"

export %inline
cite : String -> Attribute ev
cite = Str "cite"

export %inline
class : String -> Attribute ev
class = Str "class"

export %inline
classes : List String -> Attribute ev
classes = dispAttr "class" (fastConcat . intersperse " ")

export %inline
cols : Bits32 -> Attribute ev
cols = showAttr "cols"

export %inline
colspan : Bits32 -> Attribute ev
colspan = showAttr "colspan"

export %inline
contenteditable : Bool -> Attribute ev
contenteditable = Bool "contenteditable"

export %inline
controls : Bool -> Attribute ev
controls = Bool "controls"

export %inline
data_ : String -> Attribute ev
data_ = Str "data"

export %inline
dir : Dir -> Attribute ev
dir = showAttr "dir"

export %inline
disabled : Bool -> Attribute ev
disabled = Bool "disabled"

export %inline
download : String -> Attribute ev
download = Str "download"

export %inline
draggable : Bool -> Attribute ev
draggable = Bool "draggable"

export %inline
for : String -> Attribute ev
for = Str "for"

export %inline
form : String -> Attribute ev
form = Str "form"

export %inline
height : Bits32 -> Attribute ev
height = showAttr "height"

export %inline
hidden : Bool -> Attribute ev
hidden = Bool "hidden"

export %inline
href : String -> Attribute ev
href = Str "href"

export %inline
hreflang : String -> Attribute ev
hreflang = Str "hreflang"

export %inline
id : String -> Attribute ev
id = Id

export %inline
label : String -> Attribute ev
label = Str "label"

export %inline
lang : String -> Attribute ev
lang = Str "lang"

export %inline
loading : LoadType -> Attribute ev
loading = showAttr "loading"

export %inline
list : String -> Attribute ev
list = Str "list"

export %inline
loop : Bool -> Attribute ev
loop = Bool "loop"

export %inline
maxlength : Bits32 -> Attribute ev
maxlength = showAttr "maxlength"

export %inline
minlength : Bits32 -> Attribute ev
minlength = showAttr "minlength"

export %inline
multiple : Bool -> Attribute ev
multiple = Bool "multiple"

export %inline
muted : Bool -> Attribute ev
muted = Bool "muted"

export %inline
name : String -> Attribute ev
name = Str "name"

export %inline
placeholder : String -> Attribute ev
placeholder = Str "placeholder"

export %inline
readonly : Bool -> Attribute ev
readonly = Bool "readonly"

export %inline
required : Bool -> Attribute ev
required = Bool "required"

export %inline
reverse : Bool -> Attribute ev
reverse = Bool "reverse"

export %inline
rows : Bits32 -> Attribute ev
rows = showAttr "rows"

export %inline
rowspan : Bits32 -> Attribute ev
rowspan = showAttr "rowspan"

export %inline
selected : Bool -> Attribute ev
selected = Bool "selected"

export %inline
spellcheck : Bool -> Attribute ev
spellcheck = Bool "spellcheck"

export %inline
src : String -> Attribute ev
src = Str "src"

export %inline
style : String -> Attribute ev
style = Str "style"

export %inline
target : String -> Attribute ev
target = Str "target"

export %inline
title : String -> Attribute ev
title = Str "title"

export %inline
type : InputType -> Attribute ev
type = showAttr "type"

export %inline
value : String -> Attribute ev
value = Str "value"

export %inline
width : Bits32 -> Attribute ev
width = showAttr "width"

export %inline
wrap : Bool -> Attribute ev
wrap = Bool "wrap"

--------------------------------------------------------------------------------
--          Events
--------------------------------------------------------------------------------

export %inline
click : (MouseInfo -> Maybe ev) -> Attribute ev
click = Event . Click

export %inline
onClick : ev -> Attribute ev
onClick = click . const . Just

export
onLeftClick : ev -> Attribute ev
onLeftClick va = click $ \mi => toMaybe (mi.button == 0) va

export
onRightClick : ev -> Attribute ev
onRightClick va = click $ \mi => toMaybe (mi.button == 2) va

export
onMiddleClick : ev -> Attribute ev
onMiddleClick va = click $ \mi => toMaybe (mi.button == 1) va

export %inline
dblClick : (MouseInfo -> Maybe ev) -> Attribute ev
dblClick = Event . DblClick

export %inline
onDblClick : ev -> Attribute ev
onDblClick = dblClick . const . Just

export
onChange : (String -> ev) -> Attribute ev
onChange f = Event . Change $ Just . f . value

export
onChecked : (Bool -> ev) -> Attribute ev
onChecked f = Event . Change $ Just . f . checked

export
onInput : (String -> ev) -> Attribute ev
onInput f = Event . Input $ Just . f . value

export
onEnterDown : ev -> Attribute ev
onEnterDown va = Event . KeyDown $ \k => toMaybe (k.key == "Enter") va

export
onEscDown : ev -> Attribute ev
onEscDown va = Event . KeyDown $ \k => toMaybe (k.key == "Escape") va

export
onBlur : ev -> Attribute ev
onBlur = Event . Blur

export
onFocus : ev -> Attribute ev
onFocus = Event . Focus


text:
-- ---------------------------------------------------------------- [ Edda.idr ]
-- Module    : Edda.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.Pattern.Convert.Edda

import Lightyear
import Lightyear.Strings

import GRL.Lang.GLang

import Edda
import Edda.Reader.Org

import Sif.Types
import Sif.Pattern.Model
import Sif.Pattern.API

-- import Sif.Pattern.Convert.Org

-- -------------------------------------------------------------- [ Directives ]

%access private
%default partial

-- ------------------------------------------------------------------- [ Utils ]

para' : String -> Edda STAR BLOCK
para' s =
  case parse para s of
    Left err  => Empty STAR
    Right res => res

inline' : String -> (List $ Edda STAR INLINE)
inline' s =
  case parse (some inline) s of
    Left err  => [Font SerifTy "Error"]
    Right res => res

sectionTemplate : Nat -> Maybe String -> String -> Edda STAR BLOCK
sectionTemplate n l t = Section STAR n l (inline' t) Nil

section' : Maybe String -> String -> Edda STAR BLOCK
section' l t = sectionTemplate 0 l t

subsection' : Maybe String -> String -> Edda STAR BLOCK
subsection' l t = sectionTemplate 1 l t

subsubsection' : Maybe String -> String -> Edda STAR BLOCK
subsubsection' l t = sectionTemplate 2 l t

subsubsubsection' : Maybe String -> String -> Edda STAR BLOCK
subsubsubsection' l t = sectionTemplate 3 l t

mkDescPara : Maybe String -> Edda STAR BLOCK
mkDescPara Nothing  = para' "Descriptino Missing\n\n"
mkDescPara (Just d) = para' (unlines [d,"\n"])

-- ------------------------------------------------------- [ Convert Functions ]

-- ---------------------------------------------------------------- [ Problems ]
convertReq : REQUIREMENT impl d -> List $ Edda STAR BLOCK
convertReq r = with SifExpr
    [ subsection' Nothing
        (unwords [show (getRTy r), ":", getTitle r])
    , mkDescPara (getDesc r)]

convertProblem : PROBLEM impl d -> List $ Edda STAR BLOCK
convertProblem p = with SifExpr
    [ section' Nothing (unwords ["Problem:", getTitle p])
    , mkDescPara (getDesc p)
    , section' Nothing "Forces"]
    ++ convRS
  where
    convRS : List $ Edda STAR BLOCK
    convRS = concatMap (convertReq) $ SifExpr.getReqs p

-- ---------------------------------------------------------------- [ Solution ]

convertAffect : AFFECT impl d -> List $ Edda STAR BLOCK
convertAffect a = [t,d]
  where
    t : Edda STAR BLOCK
    t = subsubsubsection' Nothing
           (unwords [ "/", show (SifExpr.getCValue a), "/"
                    , SifExpr.getTitle $ SifExpr.getReq a])

    d : Edda STAR BLOCK
    d = mkDescPara (SifExpr.getDesc a)

convertTrait : TRAIT impl d -> List $ Edda STAR BLOCK
convertTrait t = [tit,sVal,d] ++ as
  where
    tit : Edda STAR BLOCK
    tit = subsubsection' Nothing
            (unwords [ "Trait", show (SifExpr.getTTy t), ":"
                     , SifExpr.getTitle t])

    sVal : Edda STAR BLOCK
    sVal = DList STAR [MkPair (inline' "Evaluation Value")
                              (inline' $ show (SifExpr.getSValue t))]

    d : Edda STAR BLOCK
    d = mkDescPara (SifExpr.getDesc t)

    as : List $ Edda STAR BLOCK
    as = concatMap (convertAffect) $ SifExpr.getAffects t

convertProperty : PROPERTY impl d -> List $ Edda STAR BLOCK
convertProperty p = [t,d] ++ ts
  where
    t : Edda STAR BLOCK
    t = subsection' Nothing
          (unwords [ "Property:", SifExpr.getTitle p])

    d : Edda STAR BLOCK
    d = mkDescPara (SifExpr.getDesc p)

    ts : List $ Edda STAR BLOCK
    ts = concatMap (convertTrait) $ SifExpr.getTraits p

convertSolution : SOLUTION impl d -> List $ Edda STAR BLOCK
convertSolution s = [t,d] ++ ps
  where
    t : Edda STAR BLOCK
    t = section' Nothing
            (unwords [ "Solution:", SifExpr.getTitle s])

    d : Edda STAR BLOCK
    d = mkDescPara (SifExpr.getDesc s)

    ps : List $ Edda STAR BLOCK
    ps = concatMap (convertProperty) $ SifExpr.getProperties s

convertDomain : SifDomain -> List $ Edda STAR BLOCK
convertDomain (MkDomain t d) = [tblock, dblock]
  where
    tblock : Edda STAR BLOCK
    tblock = section' Nothing (unwords ["Context:", t])

    dblock : Edda STAR BLOCK
    dblock = mkDescPara d

convertPattern : PATTERN impl d -> Edda STAR MODEL
convertPattern p = EddaRaw as (intersperse (Empty STAR) body)
  where
    as : List (String, String)
    as = [MkPair "TITLE" (SifExpr.getTitle p)]

    dom : List $ Edda STAR BLOCK
    dom = convertDomain $ SifExpr.getDomain p

    prob : List $ Edda STAR BLOCK
    prob = convertProblem $ SifExpr.getProblem p

    sol : List $ Edda STAR BLOCK
    sol = convertSolution $ SifExpr.getSolution p

    body : List $ Edda STAR BLOCK
    body = [mkDescPara (SifExpr.getDesc p)] ++ dom ++ prob ++ sol

export
toEdda : PATTERN impl d -> Edda PRIME MODEL
toEdda pdoc = refineEdda (convertPattern pdoc)

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