text:
module Dijkstra

-- Based on https://www.fstar-lang.org/papers/dm4free/slides.pdf

data Unit : Type -> Type where
  U : Unit a

STwp : Type -> Type -> Type
STwp s a = s -> (a -> s -> Type) -> Type

ST : (s : Type) -> (a : Type) -> STwp s a -> Type
ST s a p  = (st : s) -> (k : (a -> s -> Type)) -> Unit (p st k) -> Type

returnwp : a -> STwp s a
returnwp v st k = k v st

getwp : () -> STwp s s
getwp () st k = k st st

setwp : s -> STwp s ()
setwp st _ k = k () st

bindwp : STwp s a -> (a -> STwp s b) -> STwp s b
bindwp wp f st k = wp st (\b, st' => f b st' k)

return : (v : a) -> ST s a (returnwp v)
return v st k _ = returnwp v st k

get : ST s s (getwp ())
get st k _ = (getwp ()) st k

set : (st : s) -> ST s () (setwp st)
set st st' k _ = (setwp st) st' k

(>>=) : {wa : STwp s a} -> {wb : a -> STwp s b} ->
        ST s a wa -> ((x : a) -> ST s b (wb x)) -> ST s b (bindwp wa wb)
(>>=) m f st k _ = m st (\v, st' => f v st' k U) U

incr : ST Nat () (\s, post => post () (S s))
incr = do x <- get
          set (S x)

test : incr 0 (\x, s => 1 = s) U
test = Refl

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
data Bar = MkBar
data Baz = MkBaz

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

desc : Type -> String
desc Int = "Int"
desc Nat = "Nat"
desc (Vect n a) = "Vector of " ++ show n ++ " " ++ desc a
desc Type = "Type"
desc _ = "Something else"

descNat : Type -> String
descNat t = "Function from Nat to " ++ desc t

descFn : (x : Type) -> String
descFn ((x : Nat) -> b) = descNat (b Z)
descFn (a -> b) = "Function on " ++ desc a
descFn x = desc x

main : IO ()
main = do printLn (descFn (Nat -> Nat))
          printLn (descFn ((x : Nat) -> Vect x Int))
          printLn (descFn (Type -> Int))

ext: idr

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Network.TLS.Certificate.System

import Data.Vect
import Data.Fin
import Control.Monad.Error.Either
import Control.Monad.Error.Interface
import System.Info
import System.FFI
import Data.Buffer
import Data.List
import Network.TLS.Certificate
import Network.TLS.Parse.PEM
import Data.String.Parser
import Data.Either
import System.File.Process
import System.File.ReadWrite
import System.Directory
import System

pem_to_certificate : PEMBlob -> Either String Certificate
pem_to_certificate (MkPEMBlob "CERTIFICATE" content) =
  bimap (\err => "error: \{err}, content:\n") id (parse_certificate content)
pem_to_certificate _ = Left "PEM is not a certificate"

--- START WINDOWS ---

%foreign "C:openCertStore,libidristls"
prim__open_cert_store : PrimIO AnyPtr

%foreign "C:closeCertStore,libidristls"
prim__close_cert_store : AnyPtr -> PrimIO Int

%foreign "C:nextCertInStore,libidristls"
prim__next_cert_in_store : AnyPtr -> AnyPtr -> PrimIO AnyPtr

%foreign "C:isNull, libidris2_support, idris_support.h"
prim__idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int

%foreign "C:certLenInfo,libidristls"
prim__cert_len_info : AnyPtr -> PrimIO Int

%foreign "C:certBody,libidristls"
prim__cert_body : AnyPtr -> Buffer -> PrimIO ()

nullPtr : HasIO io => AnyPtr -> io Bool
nullPtr p = do
  i <- primIO $ prim__idrnet_isNull p
  pure (i /= 0)

buffer_to_list : HasIO io => Buffer -> io (List Bits8)
buffer_to_list buffer = rawSize buffer >>= \cap => traverse (getBits8 buffer) [0..(cap-1)]

test_windows_cert : EitherT String IO (List Certificate)
test_windows_cert = do
  cert_store <- primIO prim__open_cert_store
  certs <- loop [] cert_store prim__getNullAnyPtr

  let certs_parsed = mapMaybe (getRight . parse_certificate) certs

  b <- primIO $ prim__close_cert_store cert_store
  if b == 0
    then throwE "error occured while closing certificate store"
    else pure certs_parsed
  where
    loop : HasIO io => List (List Bits8) -> AnyPtr -> AnyPtr -> io (List (List Bits8))
    loop acc cert_store prev_cert = do
      ctxptr <- primIO $ prim__next_cert_in_store cert_store prev_cert
      False <- nullPtr ctxptr
      | True => pure acc
      len <- primIO $ prim__cert_len_info ctxptr
      Just buffer <- newBuffer len
      | Nothing => loop acc cert_store ctxptr
      primIO $ prim__cert_body ctxptr buffer
      buffer_to_list buffer >>= \cert => loop (cert :: acc) cert_store ctxptr

--- END WINDOWS ---

--- START MACOS ---

rootCAKeyChain : String
rootCAKeyChain = "/System/Library/Keychains/SystemRootCertificates.keychain"

systemKeyChain : String
systemKeyChain = "/Library/Keychains/System.keychain"

command : List String
command = ["security", "find-certificate", "-pa", rootCAKeyChain, systemKeyChain]

read_pems : EitherT FileError IO String
read_pems = do
  file <- MkEitherT (popen command Read)
  MkEitherT (fRead file)

test_macos_cert : EitherT String IO (List Certificate)
test_macos_cert = do
  pems <- bimapEitherT (\err => "popen security failed: \{show err}") id read_pems
  (pemblobs, _) <- MkEitherT $ pure $ parse (many parse_pem_blob) pems
  pure (mapMaybe (getRight . pem_to_certificate) pemblobs)

--- END MACOS ---

--- START UNIX ---

default_paths : List String
default_paths =
  [ "/etc/ssl/certs/"                 -- linux
  , "/system/etc/security/cacerts/"   -- android
  , "/usr/local/share/certs/"         -- freebsd
  , "/etc/ssl/cert.pem"               -- openbsd
  ]

to_files : HasIO io => List String -> io (List String)
to_files folders = join <$> traverse go folders where
  go : String -> io (List String)
  go folder = case !(listDir folder) of
    Left _ => pure [folder]
    Right files => pure (map (folder <+> "/" <+>) files)

test_unix_certs : EitherT String IO (List Certificate)
test_unix_certs = do
  folder <- maybe default_paths (::[]) <$> getEnv "SYSTEM_CERTIFICATE_PATH"
  certpaths <- to_files folder
  pemtxts <- mapMaybe getRight <$> traverse readFile certpaths
  let pems = pemtxts >>= parse_pems_ignore_error
  pure (mapMaybe (getRight . pem_to_certificate) pems)
  where
    parse_pems_ignore_error : String -> List PEMBlob
    parse_pems_ignore_error = either (const []) fst . parse (many parse_pem_blob)

--- END UNIX

export
get_system_trusted_certs : IO (Either String (List Certificate))
get_system_trusted_certs =
  runEitherT $ if isWindows
     then test_windows_cert
     else (if os == "darwin" then test_macos_cert else test_unix_certs)


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

module Pf.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

TmRepr : Type
TmRepr = Cx -> Ty -> Type

infixl 1 :$
class ArrMpTm (tr : TmRepr) where
  var  : isTrue a tc                -> tr tc a
  lam' : (isTrue a tc -> tr tc b)   -> tr tc (a :=> b)
  (:$) : tr tc (a :=> b) -> tr tc a -> tr tc b

lam'' : {tr : TmRepr} -> ArrMpTm tr => (tr tc a -> tr tc b) -> tr tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

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

Thm : Ty -> Type
Thm a = {tr : TmRepr} -> {tc : Cx} -> ArrMpTm tr => tr 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)

-- TODO:
-- ./src/Pf/ArrMp.idr:63:6:When checking right hand side of tSKK:
-- Can't resolve type class ArrMpTm tr
-- tSKK : Thm (a :=> a)
-- tSKK {a} =
--   aS {b = a :=> a} :$ aK :$ aK

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
||| Miscellaneous functions for getting information about the system.
module System.Info

%default total

%extern prim__os : String
%extern prim__codegen : String

||| The current operating system.
export
os : String
os = prim__os

||| The codegen/backend used.
export
codegen : String
codegen = prim__codegen

||| Whether we are running on MS Windows, either directly or with a compability
||| layer (e.g. cygwin).
export
isWindows : Bool
isWindows = os `elem` ["windows", "mingw32", "cygwin32"]

%foreign "C:idris2_getNProcessors, libidris2_support, idris_support.h"
prim__getNProcessors : PrimIO Int

||| Get the number of processors on the system. Returns `Nothing` if we somehow
||| got 0 processors.
export
getNProcessors : IO (Maybe Nat)
getNProcessors = do
  i <- fromPrim prim__getNProcessors
  pure (if i < 0 then Nothing else Just (integerToNat (cast i)))


text:
||| Some utilities for defining and manipulating TTImp values
||| for writing elaborator scripts.
|||
||| Some notes: Use quotes whenever possible:
|||
||| Names can be quoted like so: `{{ AName }}, `{{ In.Namespace.AName }}.
||| Both examples are of type Language.Reflection.TT.Name.
|||
||| Expressions can be quoted like so: `(\x => x * x)
module Language.Reflection.Syntax

import public Data.String
import public Data.List1
import public Language.Reflection
import Language.Reflection.Pretty

%default total

--------------------------------------------------------------------------------
--          Names
--------------------------------------------------------------------------------

public export
FromString Name where
  fromString s = run (split ('.' ==) s) []
    where run : List1 String -> List String -> Name
          run (h ::: []) []        = UN $ Basic h
          run (h ::: []) ns        = NS (MkNS ns) (UN $ Basic h)
          run ll@(h ::: (y :: ys)) xs = run (assert_smaller ll $ y ::: ys) (h :: xs)

||| Takes a (probably fully qualified name) and generates a
||| identifier from this without the dots.
|||
||| Example : camelCase "Data.List1.List1" = "DataList1List1"
export
camelCase : Name -> String
camelCase = concat . split ('.' ==) . show

export
nameStr : Name -> String
nameStr (UN $ Basic x)  = x
nameStr (UN $ Field x)  = x
nameStr (UN Underscore) = "_"
nameStr (NS _ x) = nameStr x
nameStr (MN x y) = x ++ show y
nameStr (DN _ x) = nameStr x
nameStr (Nested (x,y) n) = #"nested_\#{nameStr n}_\#{show x}_\#{show y}"#
nameStr (CaseBlock x n) = #"case_n_\#{show x}"#
nameStr (WithBlock x n) = #"with_n_\#{show x}"#

--------------------------------------------------------------------------------
--          Vars
--------------------------------------------------------------------------------

||| Creates a variable from the given name
|||
||| Names are best created using quotes: `{{ AName }},
||| `{{ In.Namespacs.Name }}.
|||
||| Likewise, if the name is already known at the time of
||| writing, use quotes for defining variables directly: `(AName)
export
var : Name -> TTImp
var = IVar EmptyFC

||| Alias for `var . fromString`
export
varStr : String -> TTImp
varStr = var . fromString

||| Binds a new variable, for instance in a pattern match.
|||
||| This is an alias for `IBindVar EmptyFC`.
export
bindVar : String -> TTImp
bindVar = IBindVar EmptyFC

||| Implicit value bound if unsolved
|||
||| This is an alias for `Implicit EmptyFC True`
export
implicitTrue : TTImp
implicitTrue = Implicit EmptyFC True

||| Implicitly typed value unbound if unsolved
|||
||| This is an alias for `Implicit EmptyFC False`
export
implicitFalse : TTImp
implicitFalse = Implicit EmptyFC False

||| Primitive values.
|||
||| This is an alias for `IPrimVal EmptyFC`
export
primVal : (c : Constant) -> TTImp
primVal = IPrimVal EmptyFC

||| The type `Type`.
|||
||| This is an alias for `IType EmptyFC`.
export
type :  TTImp
type = IType EmptyFC

--------------------------------------------------------------------------------
--          Application
--------------------------------------------------------------------------------

||| Function application.
|||
||| This is an alias for `IApp EmptyFC`.
|||
||| Example: ```app (var "Just") (var "x")```
|||          is equivalent to `(Just x)
export
app : TTImp -> TTImp -> TTImp
app = IApp EmptyFC

infixl 6 .$

||| Infix version of `app`
|||
||| Example: ```var "Just" .$ var "x"```
export
(.$) : TTImp -> TTImp -> TTImp
(.$) = IApp EmptyFC

export
unApp : TTImp -> (TTImp,List TTImp)
unApp = run []
  where run : List TTImp -> TTImp -> (TTImp,List TTImp)
        run xs (IApp _ y z) = run (z :: xs) y
        run xs t            = (t,xs)

||| Applies a list of variables to a function.
|||
||| See `appNames` for an example
export
appAll : Name -> List TTImp -> TTImp
appAll fun = foldl (.$) (var fun)

||| Applies a list of variable names to a function.
|||
||| Example: appNames "either" ["f","g","val"]
|||          is equivalent to ~(either f g val)
export
appNames : (fun : Name) -> (args : List Name) -> TTImp
appNames fun = appAll fun . map var

||| Binds a list of parameters to a data constructor in
||| a pattern match.
|||
||| Example: bindAll "MkPair" ["a","b"]
|||          is the same as ~(MkPair a b)
export
bindAll : (fun : Name) -> (args : List String) -> TTImp
bindAll fun = appAll fun . map bindVar

export
autoApp : TTImp -> TTImp -> TTImp
autoApp = IAutoApp EmptyFC

export
namedApp : TTImp -> Name -> TTImp -> TTImp
namedApp = INamedApp EmptyFC

--------------------------------------------------------------------------------
--          Function Arguments
--------------------------------------------------------------------------------

public export
record Arg (nameMandatory : Bool) where
  constructor MkArg
  count   : Count
  piInfo  : PiInfo TTImp
  name    : if nameMandatory then Name else Maybe Name
  type    : TTImp

public export
NamedArg : Type
NamedArg = Arg True

export
namedArg : Elaboration m => Arg False -> m NamedArg
namedArg (MkArg c p m t) =
  map (\n => MkArg c p n t) $ maybe (genSym "x") pure m

export
arg : TTImp -> Arg False
arg = MkArg MW ExplicitArg Nothing

export
lambdaArg : Name -> Arg False
lambdaArg n = MkArg MW ExplicitArg (Just n) implicitFalse

export
isExplicit : Arg b -> Bool
isExplicit (MkArg _ ExplicitArg _ _) = True
isExplicit (MkArg _ _           _ _) = False

export
covering
Pretty NamedArg where
  pretty (MkArg count piInfo name type) =
    parens $ hsepH [count, piInfo, name, ":", type]

||| Extracts the arguments from a function type.
export
unPi : TTImp -> (List $ Arg False, TTImp)
unPi (IPi _ c p n at rt) = mapFst (MkArg c p n at ::) $ unPi rt
unPi tpe                 = ([],tpe)

||| Extracts properly named arguments from a function type.
export
unPiNamed : Elaboration m => TTImp -> m (List NamedArg, TTImp)
unPiNamed v = let (args,rt') = unPi v
               in (, rt') <$> traverse namedArg args

||| Extracts the arguments from a lambda.
export
unLambda : TTImp -> (List $ Arg False, TTImp)
unLambda (ILam _ c p n at rt) = mapFst (MkArg c p n at ::) $ unLambda rt
unLambda tpe                  = ([],tpe)

||| Extracts properly named arguments from a lambda.
export
unLambdaNamed : Elaboration m => TTImp -> m (List NamedArg, TTImp)
unLambdaNamed v = let (args,rt') = unLambda v
                  in (, rt') <$> traverse namedArg args

--------------------------------------------------------------------------------
--          Lambdas
--------------------------------------------------------------------------------

||| Defines an anonymous function (lambda).
|||
||| This passes the fields of `Arg` to `ILam EmptyFC`
export
lam : Arg False -> (lamTy : TTImp) -> TTImp
lam (MkArg c p n t) = ILam EmptyFC c p n t

infixr 3 .=>

||| Infix alias for `lam`.
export
(.=>) : Arg False -> TTImp -> TTImp
(.=>) = lam

--------------------------------------------------------------------------------
--          Function Types
--------------------------------------------------------------------------------

||| Defines a function type.
|||
||| This passes the fields of `Arg` to `IPi EmptyFC`
export
pi : Arg False -> (retTy : TTImp) -> TTImp
pi (MkArg c p n t) = IPi EmptyFC c p n t

infixr 5 .->

||| Infix alias for `pi`.
export
(.->) : Arg False -> TTImp -> TTImp
(.->) = pi

||| Extracts the arguments from a function type.
export
piAll : TTImp -> List (Arg False) -> TTImp
piAll res = foldr (.->) res

||| Extracts the arguments from a function type.
export
piAllImplicit : TTImp -> List Name -> TTImp
piAllImplicit res = piAll res . map toArg
  where toArg : Name -> Arg False
        toArg n = MkArg M0 ImplicitArg (Just n) implicitFalse

||| Extracts the arguments from a function type.
export
piAllAuto : TTImp -> List TTImp -> TTImp
piAllAuto res = piAll res . map (MkArg MW AutoImplicit Nothing)

--------------------------------------------------------------------------------
--          Pattern Matching
--------------------------------------------------------------------------------

||| An impossible clause in a pattern match.
|||
||| This is an alias for `ImpossibleClause EmptyFC`.
export
impossibleClause : (lhs : TTImp) -> Clause
impossibleClause = ImpossibleClause EmptyFC

||| A pattern clause consisting of the left-hand and
||| right-hand side of the pattern arrow "=>".
|||
||| This is an alias for `PatClause EmptyFC`.
export
patClause : (lhs : TTImp) -> (rhs : TTImp) -> Clause
patClause = PatClause EmptyFC

infixr 3 .=

||| Infix alias for `patClause`
export
(.=) : TTImp -> TTImp -> Clause
(.=) = patClause

||| A case expression.
|||
||| This is an alias for `ICase EmptyFC`.
export
iCase : TTImp -> (ty : TTImp) -> List Clause -> TTImp
iCase = ICase EmptyFC

||| "as"-pattern.
|||
||| This is an alias for `IAs EmptyFC UseLeft`.
export
as : Name -> TTImp -> TTImp
as = IAs EmptyFC EmptyFC UseLeft

--------------------------------------------------------------------------------
--          Function Declarations
--------------------------------------------------------------------------------

||| Named type.
|||
||| This is an alias for `MkTyp EmptyFC`.
export
mkTy : (n : Name) -> (ty : TTImp) -> ITy
mkTy = MkTy EmptyFC EmptyFC

||| Type declaration of a function.
|||
||| `claim c v opts n tp` is an alias for
||| `IClaim EmptyFC c v opts (MkTy EmptyFC n tp)`.
export
claim : Count -> Visibility -> List FnOpt -> Name -> TTImp -> Decl
claim c v opts n tp = IClaim EmptyFC c v opts (mkTy n tp)

||| `simpleClaim v n t` is an alias for `claim MW v [] (mkTy n t)`
export
simpleClaim : Visibility -> Name -> TTImp -> Decl
simpleClaim v = claim MW v []

||| Alias for `simpleClaim Public`
export
public' : Name -> TTImp -> Decl
public' = simpleClaim Public

||| Alias for `simpleClaim Private``
export
private' : Name -> TTImp -> Decl
private' = simpleClaim Private

||| Alias for `simpleClaim Export`
export
export' : Name -> TTImp -> Decl
export' = simpleClaim Export

||| `directHint v` is an alias for `claim MW v [Hint True]`
export
directHint : Visibility -> Name -> TTImp -> Decl
directHint v = claim MW v [Hint True]

||| `interfaceHint v opts` is an alias for `claim MW v (Hint False :: opts)`
export
interfaceHintOpts : Visibility -> List FnOpt -> Name -> TTImp -> Decl
interfaceHintOpts v opts = claim MW v (Hint False :: opts)

||| `interfaceHint v` is an alias for `claim MW v [Hint False]`
export
interfaceHint : Visibility -> Name -> TTImp -> Decl
interfaceHint v = claim MW v [Hint False]

||| Function definition (implementation)
|||
||| This is an alias for `IDef EmptyFC`.
export
def : Name -> List Clause -> Decl
def = IDef EmptyFC

||| Local definitions
|||
||| This is an alias for `ILocal EmptyFC`.
export
local : List Decl -> TTImp -> TTImp
local = ILocal EmptyFC

--------------------------------------------------------------------------------
--          Data Declarations
--------------------------------------------------------------------------------

||| Data declaration.
|||
||| This merges constructors `IData` and `MkData`.
export
iData :  Visibility
      -> Name
      -> (tycon : TTImp)
      -> (opts  : List DataOpt)
      -> (cons  : List ITy)
      -> Decl
iData v n tycon opts cons =
  IData EmptyFC v Nothing (MkData EmptyFC n tycon opts cons)

||| Simple data declaration of type `Type` (no options, no parameters,
||| no indices).
|||
||| `simpleData v n` is an alias for `iData v n type []`.
export
simpleData : Visibility -> Name -> (cons : List ITy) -> Decl
simpleData v n = iData v n type []

||| Alias for `simpleData Public`
export
simpleDataPublic : Name -> (cons : List ITy) -> Decl
simpleDataPublic = simpleData Public

||| Alias for `simpleData Export`
export
simpleDataExport : Name -> (cons : List ITy) -> Decl
simpleDataExport = simpleData Export

--------------------------------------------------------------------------------
--          Local Definitions
--------------------------------------------------------------------------------

||| Let bindings.
|||
||| This is an alias for `ILet EmptyFC`.
export
iLet : Count -> Name -> (nTy : TTImp) -> (nVal : TTImp)
    -> (scope : TTImp) -> TTImp
iLet = ILet EmptyFC EmptyFC

--------------------------------------------------------------------------------
--          Elab Utils
--------------------------------------------------------------------------------

export
listOf : List TTImp -> TTImp
listOf [] = `( Nil )
listOf (x :: xs) = `( ~(x) :: ~(listOf xs) )

private errMsg : Name -> List (Name,TTImp) -> String
errMsg n [] = show n ++ " is not in scope."
errMsg n xs = let rest = concat $ intersperse ", " $ map (show . fst) xs
               in show n ++ " is not unique: " ++ rest

||| Looks up a name in the current namespace.
export
lookupName : Elaboration m => Name -> m (Name, TTImp)
lookupName n = do pairs <- getType n
                  case (pairs,n) of
                       ([p],_)     => pure p
                       (ps,UN str) => inCurrentNS (UN str) >>= \m => assert_total {-now argument is NS, not UN-} $ lookupName m
                       (ps,_)      => fail $ errMsg n ps


text:
> module Tuple.Properties

> import Control.Isomorphism

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

> |||
> tuplePairIso3 : {A, B, C : Type} -> Iso (A, B, C) ((A, B), C)
> tuplePairIso3 {A} {B} {C} = MkIso to from ok1 ok2
>   where to : (A, B, C) -> ((A, B), C)
>         to (x, y, z) = ((x, y), z)
>         from : ((A, B), C) -> (A, B, C)
>         from ((x, y), z) = (x, y, z)
>         ok1 : (x : ((A, B), C)) -> to (from x) = x
>         ok1 ((x, y), z) = Refl
>         ok2 : (x : (A, B, C)) -> from (to x) = x
>         ok2 (x, y, z) = Refl

> |||
> tuplePairIso4 : {A, B, C, D : Type} -> Iso (A, B, C, D) ((A, B, C), D)
> tuplePairIso4 {A} {B} {C} {D} = MkIso to from ok1 ok2
>   where to : (A, B, C, D) -> ((A, B, C), D)
>         to (a, b, c, d) = ((a, b, c), d)
>         from : ((A, B, C), D) -> (A, B, C, D)
>         from ((a, b, c), d) = (a, b, c, d)
>         ok1 : (x : ((A, B, C), D)) -> to (from x) = x
>         ok1 ((a, b, c), d) = Refl
>         ok2 : (x : (A, B, C, D)) -> from (to x) = x
>         ok2 (a, b, c, d) = Refl

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module VectPerm

import Data.Vect

-- Auxillary functions

Nats: Type
Nats = (Nat, Nat)

FST: (Vect k Nat, Vect k Nat) -> Vect k Nat
FST (a, b) = a

SND: (Vect k Nat, Vect k Nat) -> Vect k Nat
SND (a, b) = b

headL: (s: List Nat) -> (Not (s = [])) -> Nat
headL [] x = 0
headL (y :: xs) x = y

-- converting lists to vectors

makeVectList: (n: Nat) -> (Vect n Nat) -> (List Nat)
makeVectList Z [] = []
makeVectList (S len) (x :: xs) = [x] ++ (makeVectList len xs)

makeVectPairListPair: (Vect n Nat, Vect n Nat) -> (List Nat, List Nat)
makeVectPairListPair {n} (a, b) = (makeVectList n a, makeVectList n b)

makeListVect: (s: List Nat) -> (Vect (length s) Nat)
makeListVect s = (fromList s)

makeListPairVectPair: (a: (List Nat, List Nat)) -> (Vect (length (fst a)) Nat, Vect (length (snd a)) Nat)
makeListPairVectPair a = (makeListVect (fst a), makeListVect (snd a))

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

-- same as Data.Vect.index, but a shorter name

Index : Fin len -> Vect len elem -> elem
Index FZ     (x::xs) = x
Index (FS k) (x::xs) = index k xs

-- nearly the same as Chinmaya's 'tofinNat', but this is total because I used modnatNZ instead of Eucl

intoFin : (a: Nat) -> (n : Nat) -> (Fin n)
intoFin Z Z = ?intoFin_rhs_3
intoFin Z (S k) = FZ
intoFin (S k) Z = ?intoFin_rhs_1
intoFin (S k) (S j) = case (isLTE (S k) (S j)) of
                           (Yes prf) => FS (intoFin k j)
                           (No contra) => assert_total (intoFin (modNatNZ (S k) (S j) SIsNotZ) (S j))

-- returns the element at position n in a vector (indexing starts with 0 as usual, as we are using Fin)

nPos: (a: Nat) -> (n: Nat) -> (x: Vect n Nat) -> Nat
nPos a n x = Index (intoFin a n) x

replaceWithZ: (x: Vect n Nat) -> (pos: Nat) -> (Vect n Nat)
replaceWithZ {n} x pos = replaceAt (intoFin pos n) (Z) (x)

-- The function below is a helper function to show where (with proof) an element occurs in a vector
-- This will be useful for checking (with proof) if a Vector is a permutation of another.

improveElem: (n: Nat) -> (iter: Nat) -> (x: Vect n Nat) -> (find: Nat) -> (List (k: Nat ** (nPos k n x) = find))
improveElem n Z x find = case (decEq (nPos Z n x) find) of
                               (Yes Refl) => [(Z** Refl)]
                               (No contra) => []
improveElem n (S k) x find = case (decEq (nPos (S k) n x) find) of
                                   (Yes prf) => [((S k) ** prf)] ++ (improveElem n k x find)
                                   (No contra) => (improveElem n k x find)

-- finds all the occurences of the element 'find' in the vector 'x' with proof for each occurrence

findIn: (x: Vect n Nat) -> (find: Nat) -> (List (k: Nat ** (nPos k n x) = find))
findIn {n} x find = (improveElem n (Pred n) x find)

-- Next step: take an element from a list, take a proof that it occurs at position 'k', get the resultant list
-- by deleting the element from the position k

-- This can be used to check whether one vector is a permutation of another.

-- gives all occurences of x[pos] in y with proof

thisElemthatVect: (x: Vect n Nat) -> (pos: Nat) -> (y: Vect n Nat) -> (List (k: Nat ** (nPos k n y) = (nPos pos n x)))
thisElemthatVect {n} x pos y = findIn y (nPos pos n x)

-- given a vector x, it removes the element at position 'pos' (indexing from 0)

removeElem: (x: Vect (S n) Nat) -> (pos: Nat) -> (Vect n Nat)
removeElem {n} (x :: xs) Z = xs
removeElem {n=Z} (x :: xs) (S k) = []
removeElem {n=(S j)} (x :: xs) (S k) = [x] ++ (removeElem xs k)

-- checks if x[pos] occurs in y, and if it does, deletes them from the arrays

checkEqualElement: (x: Vect (S n) Nat) -> (y: Vect (S n) Nat) -> (pos: Nat) -> (k: Nat ** (nPos k (S n) y) = (nPos pos (S n) x)) -> (Vect n Nat, Vect n Nat)
checkEqualElement {n=Z} (x :: xs) (y :: ys) Z z = ([],[])
checkEqualElement {n=Z} [a] [b] (S k) z = ([], [])
checkEqualElement {n=(S k)} (x :: xs) (y :: ys) pos z = ( (removeElem (x::xs) pos), (removeElem (y::ys) (fst z)) )

removeIfequal: (x: Vect (S n) Nat) -> (y: Vect (S n) Nat) -> (pos: Nat) -> Either ((Vect (S n) Nat), (Vect (S n) Nat)) ((Vect n Nat), (Vect n Nat))
removeIfequal {n} x y pos = case (nonEmpty (thisElemthatVect x pos y)) of
                           (Yes prf) => Right (checkEqualElement x y pos (head (thisElemthatVect x pos y)))
                           (No contra) => Left (x, y)

-- recursively removes all the elements which occur in both x and y

removeRepeatedly: (iter: Nat) -> (x: Vect n Nat) -> (y: Vect n Nat) -> (List Nat, List Nat)
removeRepeatedly iter [] [] = ([], [])
removeRepeatedly Z (x :: xs) (y :: ys) = case (removeIfequal (x::xs) (y::ys) Z) of
                                              (Left l) => (makeVectPairListPair l)
                                              (Right r) => (makeVectPairListPair r)
removeRepeatedly (S k) (x :: xs) (y :: ys) = case (removeIfequal (x::xs) (y::ys) (S k)) of
                                                  (Left l) => (removeRepeatedly k (FST l) (SND l))
                                                  (Right r) => (removeRepeatedly k (FST r) (SND r))

-- produces the elements which occur in only one list and not another (symmetric difference of lists)

listDifference: (x: Vect n Nat) -> (y: Vect n Nat) -> (List Nat, List Nat)
listDifference {n} x y = removeRepeatedly (Pred n) x y

-- Two Boolean tests for permutations. The first one checks if the list difference is zero.

PermutationTest: (x: Vect n Nat) -> (y: Vect n Nat) -> Bool
PermutationTest x y = case (fst (listDifference x y)) of
                           [] => True
                           (x :: xs) => False

-- The second one works recursively. This will be more suited to turning into a proof.

recursiveTest: (x: Vect n Nat) -> (y: Vect n Nat) -> Bool
recursiveTest {n = Z} x y = True
recursiveTest {n= (S Z)} [a] [b] = case (decEq a b) of
                                        (Yes prf) => True
                                        (No contra) => False
recursiveTest {n = (S k)} x y = case (thisElemthatVect x Z y) of
                                     [] => False
                                     (head :: rest) => recursiveTest (removeElem x Z) (removeElem y (fst head))

-- Permutations as Bijections

-- This function is a helper function which checks each position of the Vector x and finds a corresponding element in y. Then, to make
-- sure nothing is repeated, it replaces the instance of x[pos] in y with Zero (please use positive elements in the vector). This was
-- required for constructing bijections between Vectors with repeated elements; there is a simpler way to do it in case the elements
-- are not repeated.

reversedBiject: (x: Vect n Nat) -> (y: Vect n Nat) -> (xpos: Nat) -> (List Nat)
reversedBiject {n = Z} x y xpos = []
reversedBiject {n = (S k)} x y Z = case (thisElemthatVect x Z y) of
                                        [] => []
                                        (front :: rest) => [(fst front)]
reversedBiject {n = (S k)} (x :: xs) (y :: ys) (S j) = case (thisElemthatVect (x :: xs) (S j) (y :: ys)) of
                                            [] => []
                                            (front :: rest) => [(fst front)] ++ (reversedBiject (x::xs) (replaceWithZ (y::ys) (fst front)) j)

PermutationBijection: (x: Vect n Nat) -> (y: Vect n Nat) -> (List Nat)
PermutationBijection {n = Z} x y = []
PermutationBijection {n = (S k)} x y = reverse ((reversedBiject x y k))


text:
||| Interfaces for converting values from/to JSON.
|||
||| (C) The Idris Community, 2021
module Language.JSON.Interfaces

import Data.SortedMap
import Data.Strings
import Language.JSON.Lexer
import Language.JSON.Parser

import Language.JSON

%default total

-- TODO: Maybe we should be using a more expressive type than Maybe.
||| A type that can be converted to JSON.
||| An example type and implementation is:
||| ```idris example
||| record Position where
|||   constructor MkPosition
|||   x : Integer
|||   y : Integer
|||
||| ToJSON Position where
|||   toJSON pos = JObject [("x", toJSON pos.x), ("y", toJSON pos.y)]
||| ```
public export
interface ToJSON a where
  toJSON : a -> JSON

||| A type that can be possibly converted from JSON.
||| An example type and implementation is:
||| ```idris example
||| record Position where
|||   constructor MkPosition
|||   x : Integer
|||   y : Integer
|||
||| FromJSON Position where
|||   fromJSON (JObject arg) = do
|||     x <- lookup "x" arg >>= fromJSON
|||     y <- lookup "y" arg >>= fromJSON
|||     pure $ MkPosition x y
|||   fromJSON _ = neutral
||| ```
public export
interface FromJSON a where
  fromJSON : JSON -> Maybe a

export
ToJSON JSON where
  toJSON = id

export
FromJSON JSON where
  fromJSON = pure

export
ToJSON Integer where
  toJSON = JNumber . cast

-- NOTE: In JSON all numbers are `Double`, for integers we should cast or fail
-- for invalid values?
export
FromJSON Integer where
  fromJSON (JNumber x) = pure (cast x)
  fromJSON _ = neutral

export
ToJSON Int where
  toJSON = JNumber . cast

export
FromJSON Int where
  fromJSON (JNumber x) = pure (cast x)
  fromJSON _ = neutral

export
ToJSON Bits8 where
  toJSON = JNumber . cast . cast {to = Int}

export
FromJSON Bits8 where
  fromJSON (JNumber x) = pure (fromInteger $ cast x)
  fromJSON _ = neutral

export
ToJSON Bits16 where
  toJSON = JNumber . cast . cast {to = Int}

export
FromJSON Bits16 where
  fromJSON (JNumber x) = pure (fromInteger $ cast x)
  fromJSON _ = neutral

export
ToJSON Bits32 where
  toJSON = JNumber . cast . cast {to = Int}

export
FromJSON Bits32 where
  fromJSON (JNumber x) = pure (fromInteger $ cast x)
  fromJSON _ = neutral

export
ToJSON Bits64 where
  toJSON = JNumber . cast . cast {to = Int}

export
FromJSON Bits64 where
  fromJSON (JNumber x) = pure (fromInteger $ cast x)
  fromJSON _ = neutral

export
ToJSON Double where
  toJSON = JNumber

export
FromJSON Double where
  fromJSON (JNumber x) = pure x
  fromJSON _ = neutral

export
ToJSON Nat where
  toJSON = JNumber . cast

export
FromJSON Nat where
  fromJSON (JNumber x) = pure (fromInteger $ cast x)
  fromJSON _ = neutral

export
ToJSON String where
  toJSON = JString

export
FromJSON String where
  fromJSON (JString s) = pure s
  fromJSON _ = neutral

export
ToJSON Char where
  toJSON = toJSON . Strings.singleton

export
FromJSON Char where
  fromJSON (JString s) = case strM s of
                              StrCons c "" => pure c
                              _ => neutral
  fromJSON _ = neutral

export
ToJSON Bool where
  toJSON = JBoolean

export
FromJSON Bool where
  fromJSON (JBoolean b) = pure b
  fromJSON _ = neutral

export
ToJSON a => ToJSON (Maybe a) where
  toJSON Nothing = JNull
  toJSON (Just x) = toJSON x

export
FromJSON a => FromJSON (Maybe a) where
  fromJSON JNull = pure Nothing
  fromJSON json @{impl} = pure <$> fromJSON @{impl} json

export
ToJSON a => ToJSON (List a) where
  toJSON = JArray . map toJSON

export
FromJSON a => FromJSON (List a) where
  fromJSON (JArray xs) = traverse fromJSON xs
  fromJSON _ = neutral

export
ToJSON () where
  toJSON () = JObject empty

export
FromJSON () where
  fromJSON (JObject xs) = guard $ null xs
  fromJSON _ = neutral

export
(ToJSON a, ToJSON b) => ToJSON (a, b) where
  toJSON (x, y) = JArray [toJSON x, toJSON y]

export
(FromJSON a, FromJSON b) => FromJSON (a, b) where
  fromJSON (JArray [x, y]) = (,) <$> fromJSON x <*> fromJSON y
  fromJSON _ = neutral

export
ToJSON v => ToJSON (SortedMap String v) where
  toJSON m = JObject (toList $ toJSON <$> m)

export
FromJSON v => FromJSON (SortedMap String v) where
  fromJSON (JObject xs) = fromList <$> traverse (\(k, v) => (k,) <$> fromJSON v) xs
  fromJSON _ = neutral

export
ToJSON a => ToJSON (Inf a) where
  toJSON x = toJSON x

export
FromJSON a => FromJSON (Inf a) where
  fromJSON @{impl} x = map (\x => Delay x) (fromJSON @{impl} x)


text:
module Booleans

infixl 4 /\, \/

data MyBool : Type where
     True : MyBool
     False : MyBool

-- Alternate way of creating the MyBool datatype
-- data MyBool = True | False

negb : Bool -> Bool
negb False = True
negb True = False

public export
andb : (a : Bool) -> (b : Bool) -> Bool
andb False b = False
andb True b = b

orb : (a : Bool) -> (b : Bool) -> Bool
orb False b = b
orb True b = True

-- orb truth table as proofs
to1 : (orb True True) = True
to1 = Refl
to2 : (orb True False) = True
to2 = Refl
to3 : (orb False False) = False
to3 = Refl
to4 : (orb False True) = True
to4 = Refl

(/\) : Bool -> Bool -> Bool
(/\) = andb

(\/) : Bool -> Bool -> Bool
(\/) = orb

to5 : False \/ False \/ True = True
to5 = Refl

-- Exercise 11.1
idAppTwiceF : (f : Bool -> Bool) -> (idp : (x : Bool) -> f x = x) -> f (f False) = False
idAppTwiceF f idp = rewrite idp False in rewrite idp False in Refl

idAppTwiceT : (f : Bool -> Bool) -> (idp : (x : Bool) -> f x = x) -> f (f True) = True
idAppTwiceT f idp = rewrite idp True in rewrite idp True in Refl

idAppTwice : (f : Bool -> Bool) -> ((x : Bool) -> f x = x) -> (b : Bool) -> f (f b) = b
idAppTwice f idp False = idAppTwiceF f idp
idAppTwice f idp True = idAppTwiceT f idp

-- Exercise 11.1 - 2
negAppTwiceF : (f : Bool -> Bool) -> (g : (x : Bool) -> f x = negb x) -> f (f False) = False
negAppTwiceF f g = rewrite g False in rewrite g True in Refl

negAppTwiceT : (f : Bool -> Bool) -> (g : (x : Bool) -> f x = negb x) -> f (f True) = True
negAppTwiceT f g = rewrite g True in rewrite g False in Refl

negAppTwice : (f : Bool -> Bool) -> ((x : Bool) -> f x = negb x) -> (b : Bool) -> f (f b) = b
negAppTwice f g False = negAppTwiceF f g
negAppTwice f g True = negAppTwiceT f g


text:
module Hello

-- FFI call to `printHello` in `c/hello.c`.
%foreign "C:printHello,libhello"
hello : PrimIO ()

-- All commands below should be run from the project's root dir.
--
-- In order to run this, first build `c/hello.c`:
-- `cc -shared c/hello.c -o libhello.so`.
--
-- Now load this source file into an Idris2 session
-- `rlwrap idris2 --source-dir idris idris/Hello.idr`.
-- and execute main:
-- `Hello> :exec main`.
--
-- In order to build and run:
-- `idris2 --source-dir idris -o hello idris/Hello.idr`
-- Now, export system library path to current dir
-- `export LD_LIBRARY_PATH=/home/me/idris/cffi`
-- and run the program:
-- `build/exec/hello`.
main : IO ()
main = primIO hello


text:
foo : String
foo = "empty interp: \{}"


text:
module Text.RE

import Data.List.Views

%default total

data RE =
    RLit   Char    -- literals
  | R0Plus RE      -- *
  | R1Plus RE      -- +
  | ROpt   RE      -- ?
  | RConcat RE RE  -- <expr><expr>
  | RAlt RE RE     -- <expr>|<expr>

data REParseError = REError String

rtokens : List Char
rtokens = unpack "*+?()|"

format : List Char -> Either REParseError RE

formatStr : String -> Either REParseError RE
formatStr = format . unpack

max_stars_repo_name: jhmcstanton/idris-sandbox

max_issues_repo_name: jhmcstanton/idris-sandbox

max_forks_repo_name: jhmcstanton/idris-sandbox


text:
module Control.Monad.Reader.Reader

import Control.Monad.Identity
import Control.Monad.Trans

%default total

||| The transformer on which the Reader monad is based
public export
record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
  constructor MkReaderT
  1 runReaderT' : stateType -> m a

||| Transform the computation inside a @ReaderT@.
public export %inline
mapReaderT : (m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT f m = MkReaderT $ \st => f (runReaderT' m st)

||| Unwrap and apply a ReaderT monad computation
public export
%inline
runReaderT : stateType -> ReaderT stateType m a -> m a
runReaderT s action = runReaderT' action s

--------------------------------------------------------------------------------
--          Reader
--------------------------------------------------------------------------------

||| The Reader monad. The ReaderT transformer applied to the Identity monad.
public export
Reader : (stateType : Type) -> (a : Type) -> Type
Reader s a = ReaderT s Identity a

||| Unwrap and apply a Reader monad computation
public export %inline
runReader : stateType -> Reader stateType a -> a
runReader s = runIdentity . runReaderT s

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export
implementation Functor f => Functor (ReaderT stateType f) where
  map f (MkReaderT g) = MkReaderT $ \st => f <$> g st

public export
implementation Applicative f => Applicative (ReaderT stateType f) where
  pure x = MkReaderT $ \_ => pure x

  MkReaderT f <*> MkReaderT a =
    MkReaderT $ \st =>
      let f' = f st in
      let a' = a st in
      f' <*> a'

public export
implementation Monad m => Monad (ReaderT stateType m) where
  MkReaderT f >>= k =
    MkReaderT $ \st => f st >>= runReaderT st . k

public export
implementation MonadTrans (ReaderT stateType) where
  lift x = MkReaderT $ \_ => x

public export
implementation HasIO m => HasIO (ReaderT stateType m) where
  liftIO f = MkReaderT $ \_ => liftIO f

public export
implementation Alternative f => Alternative (ReaderT stateType f) where
  empty = MkReaderT $ const empty

  MkReaderT f <|> mg = MkReaderT $ \st => f st <|> runReaderT' mg st


text:
module Main

import Effect.State

data Tree a = Leaf
            | Node (Tree a) a (Tree a)

flattenTree : Tree a -> List a
flattenTree Leaf = []
flattenTree (Node l x r) = flattenTree l ++ (x :: flattenTree r)

testTree : Tree String
testTree = Node (Node Leaf "One" (Node Leaf "Two" Leaf))
                "Three"
                (Node (Node Leaf "Four" Leaf) "Five" Leaf)

data Tag : Type where
data Leaves : Type where

label : Tree a -> { [STATE Int] } Eff m (Tree (Int, a))
label Leaf = return Leaf
label (Node l x r) = do l' <- label l
                        lbl <- get
                        put (lbl + 1)
                        r' <- label r
                        return (Node l' (lbl, x) r')

main : IO ()
main = do let t = runPure (do put 1; label testTree)
          print (flattenTree t)

{-
label Leaf = return Leaf
label (Node l x r) = do l' <- label l
                        lbl <- get
                        put (lbl + 1)
                        r' <- label r
                        return (Node l' (lbl, x) r')
-}

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
-- ------------------------------------------------------------- [ Options.idr ]
-- Module    : Options.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Frigg.Options

-- ----------------------------------------------------------------- [ Imports ]
import Effects
import Effect.Exception

import ArgParse

import XML.DOM
import XML.Reader

import Freyja.Convert

%access export
-- -------------------------------------------------------------------- [ Mode ]

public export
data FriggMode = Read | Templ | Conv | REPL | VERS | HELP | Sif

-- ----------------------------------------------------------------- [ Options ]
public export
record FriggOpts where
  constructor MkFriggOpts
  mode    : Maybe FriggMode
  patt    : Maybe String
  weights : Maybe String
  gscale  : Maybe String
  to      : Maybe FreyjaOutFormat
  out     : Maybe String
  banner  : Bool

export
mkDefOpts : FriggOpts
mkDefOpts = MkFriggOpts
  (Just HELP) Nothing Nothing Nothing Nothing Nothing
  True

Default FriggOpts where
  default = mkDefOpts

convOpts : Arg -> FriggOpts -> Maybe FriggOpts
convOpts (Files (x::xs)) o = Nothing
convOpts (KeyValue k v)  o =
  case k of
    "pattern" => Just $ record {patt    = Just v} o
    "weights" => Just $ record {weights = Just v} o
    "gscale"  => Just $ record {gscale  = Just v} o
    "to"      => Just $ record {to      = readOutFMT v} o
    otherwise => Nothing
convOpts (Flag x) o =
  case x of
    "template" => Just $ record {mode    = Just Templ}  o
    "read"     => Just $ record {mode    = Just Read}   o
    "sif"      => Just $ record {mode    = Just Sif}    o
    "help"     => Just $ record {mode    = Just HELP}   o
    "version"  => Just $ record {mode    = Just VERS}   o
    "conv"     => Just $ record {mode    = Just Conv}   o
    "repl"     => Just $ record {mode    = Just REPL}   o
    "nobanner" => Just $ record {banner  = False}       o
    otherwise => Nothing

export
friggHelpStr : String
friggHelpStr = """Frigg (C) Jan de Muijnck-Hughes 2015

Available Options:

Flag                 | Description
---------------------|----------------------------------------------------------
--pattern="<fname>"  | The pattern to be analysed.
--weights="<fname>"  | A problem specification.
--gscale="<fname"    | A solution specification.
--to="<fmt>"         | The output format.
--sif                | Evaluate embedded sif model.

--help               | Display help
--version            | Display version
--eval               | Evaluate problem solution pairing
--conv               | Convert to problem solution pairing
--repl               | REPL
--nobanner           | Don't display banner
"""

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Divisors

import ZZ
%access public export
%default total
|||IsDivisibleZ a b can be constucted if b divides a
IsDivisibleZ : ZZ -> ZZ -> Type
IsDivisibleZ a b = (n : ZZ ** a = b * n)

|||1 divides everything
oneDiv : (a : ZZ) -> IsDivisibleZ a 1
oneDiv a = (a ** rewrite sym (multOneLeftNeutralZ a) in Refl)

|||Genetes a proof of (a+b) = d*(n+m) from (a=d*n)and (b=d*m)
distributeProof: (a:ZZ)->(b:ZZ)->(d:ZZ)->
  (n:ZZ)->(m:ZZ)->(a=d*n)->(b=d*m)->((a+b) = d*(n+m))
distributeProof a b d n m pf1 pf2 =
  rewrite  (multDistributesOverPlusRightZ d n m) in
    (trans (the (a+b=(d*n)+b) (v1)) v2) where
      v1 =plusConstantRightZ a (d*n) b pf1
      v2 =plusConstantLeftZ b (d*m) (d*n) pf2

|||The theorem d|a =>d|ac
multDiv:(IsDivisibleZ a d) ->(c:ZZ)->(IsDivisibleZ (a*c) d)
multDiv {d} (n**Refl) c =
  ((n*c)** (rewrite sym (multAssociativeZ d n c) in (Refl)))
|||The theorem d|a =>d|ca
multDivLeft:(IsDivisibleZ a d) ->(c:ZZ)->(IsDivisibleZ (c*a) d)
multDivLeft{a} x c = rewrite (multCommutativeZ c a) in (multDiv x c)

|||The theorem d|a and d|b =>d|(a+b)
plusDiv : (IsDivisibleZ a d)->(IsDivisibleZ b d)->(IsDivisibleZ (a+b) d)
plusDiv {d}{a}{b} (n**prf1) (m**prf2) =
  ((n+m)**(distributeProof a b d n m prf1 prf2))
|||The theorem b|a and c|b =>c|a
transDivide : (IsDivisibleZ a b)->(IsDivisibleZ b c)->(IsDivisibleZ a c)
transDivide {c} (x ** pf1) (y ** pf2) =
  (y*x ** (rewrite  multAssociativeZ c y x in
     (rewrite pf1 in (rewrite pf2 in Refl))))

|||If d divides a and b it divides a linear combination of a and b
linCombDiv:(m:ZZ)->(n:ZZ)->(IsDivisibleZ a d)->(IsDivisibleZ b d)->
   (IsDivisibleZ ((a*m)+(b*n)) d)
linCombDiv m n dDiva dDivb =
  plusDiv (multDiv  dDiva m) (multDiv  dDivb n)

|||The theorem that d|a and d|b implies d |(a+b*(-m)
euclidConservesDivisor:(m:ZZ)->(IsDivisibleZ a d)->(IsDivisibleZ b d)->
  (IsDivisibleZ (a+(b*(-m))) d)
euclidConservesDivisor m dDiva dDivb = plusDiv dDiva (multDiv dDivb (-m) )

|||Any integer divides zero
zzDividesZero:(a:ZZ)->(IsDivisibleZ 0 a )
zzDividesZero a = (0**(sym (multZeroRightZeroZ a)))
|||A type that is occupied iff c is a common factor of a and b
IsCommonFactorZ : (a:ZZ) -> (b:ZZ) -> (c:ZZ) -> Type
IsCommonFactorZ a b c = ((IsDivisibleZ a c),(IsDivisibleZ b c))
|||The theorem that  d is a common factor of a and b implies
|||d is a common factor of b and a
commonfactSym: IsCommonFactorZ a b d ->IsCommonFactorZ b a d
commonfactSym (dDiva, dDivb) = (dDivb,dDiva)

|||The GCD type that is occupied iff d = gcd (a,b).
||| Here GCD is defined as that positive integer such that any common factor
||| of a and b divides it
GCDZ : (a:ZZ) -> (b:ZZ) -> (d:ZZ) -> Type
GCDZ a b d = ((IsPositive d),(IsCommonFactorZ a b d),
  ({c:ZZ}->(IsCommonFactorZ a b c)->(IsDivisibleZ d c)))
|||Anything divides itself
selfDivide:(a:ZZ)->(IsDivisibleZ a a)
selfDivide a = (1**sym (multOneRightNeutralZ a))

|||Generates the proof that if c is a common factor of a and 0 then c divides a
gcdCondition : (a:ZZ) -> ({c:ZZ}->(IsCommonFactorZ a 0 c)->(IsDivisibleZ a c))
gcdCondition  a {c} (cDiva,cDiv0) = cDiva
|||Proves that the GCD of a and 0 is a
gcdOfZeroAndInteger:(a:ZZ)->IsPositive a ->GCDZ a 0 a
gcdOfZeroAndInteger a pf =
  (pf,((selfDivide a),(zzDividesZero a)),((gcdCondition a)))
|||The theorem, d|a =>d|(-a)
dDividesNegative:(IsDivisibleZ a d)->(IsDivisibleZ  (-a) d)
dDividesNegative{a}{d} (x ** pf) =
  ((-x)**(multNegateRightIsNegateZ a d x pf))
|||The theorem that d|(-a) implies d|a
dDividesNegative2:  (IsDivisibleZ (-a) d)->(IsDivisibleZ  a d)
dDividesNegative2 {a}x = rewrite (sym (doubleNegElim a)) in (dDividesNegative x)

|||The theorem c|b and c|(a+bp) then c|a
cDiva :{p:ZZ} ->(cDIvb :(IsDivisibleZ b c))->
  (cDIvExp:IsDivisibleZ (a+(b*p)) c)->(IsDivisibleZ a c)
cDiva {p}{b}{a}{c} cDivb cDivExp =
  rewrite (sym (addAndSubNeutralZ a (b*p))) in (
    plusDiv cDivExp (dDividesNegative(multDiv cDivb (p))))
|||A helper function for euclidConservesGcd function
genFunctionForGcd :(f:({c:ZZ}->(IsCommonFactorZ a b c)->(IsDivisibleZ d c)))->
  (({c:ZZ}->(IsCommonFactorZ b (a+(b*(-m)))  c)->(IsDivisibleZ d c)))
genFunctionForGcd f (cDivb,cDivExp) =
  f((cDiva cDivb cDivExp,cDivb))

|||The theorem, gcd(a,b)=d => gcd (b, a+ b(-m))=d
euclidConservesGcd :(m:ZZ)->(GCDZ a b d)->(GCDZ b  (a+(b*(-m))) d)
euclidConservesGcd m  (posProof, (dDiva,dDivb), f) =
  (posProof,(dDivb,(euclidConservesDivisor m  dDiva dDivb)),genFunctionForGcd f)
|||The theorem that if c and d are positive d|c => (d is less than or equal to c)
posDivPosImpliesLte:(IsDivisibleZ c d)->(IsPositive c)->
  (IsPositive d)->LTEZ d c
posDivPosImpliesLte {d}{c}(x ** pf) cPos dPos =
  posLteMultPosPosEqZ {q=x} d c dPos cPos pf

|||The Theorem that if c and d are positive, d|c and c|d =>(c=d)
posDivAndDivByImpliesEqual: (IsDivisibleZ c d)->(IsDivisibleZ d c)->(IsPositive c)
  ->(IsPositive d) -> (c=d)
posDivAndDivByImpliesEqual x y z x1 =lteAndGteImpliesEqualZ dLtec cLted where
  dLtec =posDivPosImpliesLte x z x1
  cLted =posDivPosImpliesLte y x1 z
|||Gcd of a and b is unique
gcdIsUnique: (GCDZ a b d)-> (GCDZ a b c)->(c=d)
gcdIsUnique {a}{b}{c}{d}(dPos, dCommonFactor,fd) (cPos, cCommonFactor,fc) =
  posDivAndDivByImpliesEqual (fc dCommonFactor) (fd cCommonFactor) cPos dPos
|||A helper function for GcdSym
genFunctionForGcdSym:({c:ZZ}->(IsCommonFactorZ a b c)->(IsDivisibleZ d c))->
   ({c:ZZ}->(IsCommonFactorZ b a c)->(IsDivisibleZ d c))
genFunctionForGcdSym f x = f (commonfactSym x)

|||A helper function for negatingPreservesGcdLeft
genFunctionForGcdNeg:({c:ZZ}->(IsCommonFactorZ (-a) b c)->(IsDivisibleZ d c))->
   ({c:ZZ}->(IsCommonFactorZ a b c)->(IsDivisibleZ d c))
genFunctionForGcdNeg f (cDiva,cDivb) = f (cDivNega,cDivb) where
  cDivNega = (dDividesNegative cDiva)
|||Proof that gcd (a,b)=gcd(b,a)
gcdSymZ: (GCDZ a b d)->(GCDZ b a d)
gcdSymZ (dPos,(dDiva,dDivb),fd) = (dPos, (dDivb, dDiva), (genFunctionForGcdSym fd))

|||Theorem that gcd(-a,b)=gcd(a,b)
negatingPreservesGcdLeft: (GCDZ (-a) b d)->(GCDZ a b d)
negatingPreservesGcdLeft (dPos,(dDivNega,dDivb),fd) =
    (dPos,(dDiva,dDivb),(genFunctionForGcdNeg fd)) where
      dDiva = dDividesNegative2 dDivNega
|||Theorem that gcd (p, -q) = gcd (p,q)
negatingPreservesGcdRight: (GCDZ p (-q) r)->(GCDZ p q r)
negatingPreservesGcdRight {p}{q} x =
  gcdSymZ{a=q}{b=p} (negatingPreservesGcdLeft (gcdSymZ {a=p}{b=(-q)} x))

|||Theorem that if d|rem , d|b and a = rem+(quot*b) then d|a
euclidConservesDivisorWithProof :{a:ZZ}->{b:ZZ}->{quot:ZZ}->{rem:ZZ}->
  (a=rem+(quot*b))->(IsDivisibleZ rem d)->(IsDivisibleZ b d)->(IsDivisibleZ a d)
euclidConservesDivisorWithProof {a}{b}{quot}{rem}equality dDivrem dDivb =
  rewrite equality in (plusDiv dDivrem (multDivLeft dDivb quot))

|||Theorem that a = rem +quot*b implies rem = a + (-quot)*b
auxEqProof:{a:ZZ}->{b:ZZ}->{quot:ZZ}->{rem:ZZ}->(a=rem+(quot *b))->
   (rem = (a + (-quot)*b))
auxEqProof {a}{b}{quot}{rem}prf =
  (rewrite (multNegateLeftZ quot b) in (sym (subOnBothSides a rem (quot*b) prf)))

|||A helper function for euclidConservesGcdWithProof
genfunction:(a=rem+(quot*b))->  ({c:ZZ}->(IsCommonFactorZ b rem c)->(IsDivisibleZ d c))->
     ({c:ZZ}->(IsCommonFactorZ a b c)->(IsDivisibleZ d c))
genfunction prf f (dDiva,dDivb) = f(dDivb,dDivrem) where
  dDivrem = euclidConservesDivisorWithProof (auxEqProof prf) dDiva dDivb

|||Proof that if a=rem +quot*b and gcd (b,rem)=d, then gcd(a,b)=d
euclidConservesGcdWithProof: {a:ZZ}->{b:ZZ}->{quot:ZZ}->{rem:ZZ}->
  (a=rem+(quot*b))->(GCDZ b rem d)->(GCDZ a b d)
euclidConservesGcdWithProof {a}{b}{quot}{rem}equality (dPos,(dDivb,dDivrem),fd) =
  (dPos,(dDiva,dDivb),(genfunction equality fd)) where
     dDiva = euclidConservesDivisorWithProof equality dDivrem dDivb


text:
{- This Source Code Form is subject to the terms of the Mozilla Public
 - License, v. 2.0. If a copy of the MPL was not distributed with this
 - file, You can obtain one at http://mozilla.org/MPL/2.0/. -}

module Main

import Todo
import TodoHtml

import Event
import Http
import Record

import FerryJS
import FerryJS.Util

import Sql
import Sql.JS

import Html as H

import Effects
import Data.String

import Debug.Error
import Debug.Trace

-- To use the error function
%language ElabReflection

Server : Type
Server = Event Multiple (Request, Response)

data Msg = NewRequest (Request, Response)

State : Type
State = (Callback Msg, DBConnection)

connection : JS_IO (Maybe DBConnection)
connection = do
  args <- getArgs
  (case args of
    -- Todo: better error handling
    [_, _, db, name, pass] => Just <$> newConnection {user=name} {database=db} {password=pass}
    _ => pure Nothing)

-- Next state function

ignore : JS_IO a -> JS_IO ()
ignore = map (const ())

respondWithTodos : Response -> List Todo -> JS_IO ()
respondWithTodos res ts = do
  str <- showTodos ts
  write res str

Route : Type
Route = State -> (Request, Response) -> JS_IO State

returnTodos : Route
returnTodos st@(cb, conn) (req, res) = do
  result <- runSelectQuery selectAll conn
  execute $ map (respondWithTodos res) (waitSelectResult result)
  pure st

respondMessageCode : String -> Nat -> Route
respondMessageCode msg code st (req, res) = do
  setStatusCode res code
  write res msg
  pure st

respondMessage : String -> Route
respondMessage msg = respondMessageCode msg 200

-- Todo: set 404 header
notFound : Route
notFound = respondMessageCode "Not found" 404

respondWithForm : Response -> List Todo -> JS_IO ()
respondWithForm res [t] = do
  page <- withinContent [todoForm t]
  write res page
respondWithForm res [] = write res "Could not find Todo with given id"
respondWithForm res _ =
  error "Todo error: should not find multiple values for private key 'id'"

displayForm : Int -> Route
displayForm id st@(cb, conn) (req, res) = do
  result <- runSelectQuery (selectWhereId id) conn
  execute $ map (respondWithForm res) (waitSelectResult result)
  pure st

editTodo : Route
editTodo st@(cb, conn) (req, res) =
  let url = getUrl req
  in let search = getQueryAs {sch=[("id", String)]} url
  in case search of
    Nothing => notFound st (req, res)
    Just rec =>
      let id = parseInteger (rec .. "id") {a=Int}
      in case id of
              Just id => displayForm id st (req, res)
              Nothing => respondMessage "Error converting id to Int" st (req, res)

newTodo : Route
newTodo st@(cb, conn) (req, res) = do
  page <- withinContent [emptyForm]
  write res page
  pure st

upsertTodo : Todo -> DBConnection -> JS_IO (Event Single Int)
upsertTodo t conn =
  case t .. "id" of
    Nothing => waitRowCountResult <$> runInsertQuery (insertTodo t) conn
    Just id => waitRowCountResult <$> runUpdateQuery (updateTodo t) conn

convertId : Maybe String -> Maybe Int
convertId = join . map (parseInteger {a=Int})

stringTodoSchema : Schema
stringTodoSchema = [("id", Maybe String), ("name", String), ("done", Maybe String)]

requestToStringTodo : Request -> Maybe (Record Main.stringTodoSchema)
requestToStringTodo req = getQueryAs {sch=stringTodoSchema} (getUrl req)

requestToTodo : Request -> Maybe Todo
requestToTodo req =
  (\rec => Record.update {se=S (S Z)} "done" isJust (Record.update {se=Z} "id" convertId rec))
    <$> requestToStringTodo req

saveTodo : Route
saveTodo st@(cb, conn) (req, res) =
  case requestToTodo req of
    Nothing => notFound st (req, res)
    Just todo => do
      ev <- upsertTodo todo conn
      doAfter ev (returnTodos st (req, res))
      pure st

deleteTodo : Route
deleteTodo st@(cb, conn) (req, res) =
  let maybeId = do
            rec <- getQueryAs {sch=[("id", Maybe String)]} (getUrl req)
            id <- rec .. "id"
            parseInteger {a=Int} id
  in case maybeId of
          Just id => do
            ev <- runDeleteQuery (removeTodoWithId id) conn
            doAfter (waitRowCountResult ev) (returnTodos st (req, res))
            pure st
          Nothing => notFound st (req, res)

Router : Type
Router = Url -> Maybe Route

pathRouter : List String -> Route -> Router
pathRouter s route url = if getPath url == s then Just route
                                             else Nothing
tryAll : List Router -> Router
tryAll [] _ = Nothing
tryAll (hd::tail) url = (hd url) <|> tryAll tail url

router : Router
router = tryAll [
  pathRouter [] returnTodos,
  pathRouter ["edit"] editTodo,
  pathRouter ["save"] saveTodo,
  pathRouter ["new"] newTodo,
  pathRouter ["delete"] deleteTodo]

computeState : ProgramMsg State Msg -> JS_IO (Maybe (State))

computeState (ProgramStart cb) = do
  maybeConn <- connection
  (case maybeConn of
    Nothing =>
      putStrLn' "Please pass database name, username and password as command line arguments"
          *> pure Nothing
    Just conn =>
      (let ev = map NewRequest $ Http.listen (httpServer 3001)
       in listen ev cb)
          *> putStrLn' "Listening on localhost:3001"
          *> pure (Just (cb, conn)))

computeState (ProgramNext st (NewRequest (req, res))) =
  Just <$>
    case router . getUrl $ req of
        Just route => route st (req, res)
        Nothing => notFound st (req, res)

main : JS_IO ()
main = run computeState

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
replicateTR : Nat -> a -> List a
replicateTR n v = go n Nil
  where go : Nat -> List a -> List a
        go 0     as = as
        go (S k) as = go k (v :: as)

main : IO ()
main =  printLn (length $ fastPack $ replicateTR 1000000 '0')
     >> putStrLn (fastConcat $ replicateTR 1000000 "")


text:
module Types.Finite

import Data.Fin
import Control.Isomorphism

%default total

to : Iso a b -> a -> b
to (MkIso to from toFrom fromTo) = to

from : Iso a b -> b -> a
from (MkIso to from toFrom fromTo) = from

class Finite a (n : Nat) where
  total
  isFinite : Iso a (Fin n)

total
toFin : Finite a n => a -> Fin n
toFin = to isFinite

total
fromFin : Finite a n => Fin n -> a
fromFin = from isFinite

instance Finite () 1 where
  isFinite = MkIso to from ok1 ok2
    where to : () -> Fin 1
          to () = FZ
          from : Fin 1 -> ()
          from FZ     = ()
          from (FS f) = absurd f
          ok2 : (x : ()) -> from (to x) = x
          ok2 () = Refl
          ok1 : (x : Fin 1) -> to (from x) = x
          ok1 FZ     = Refl
          ok1 (FS f) = absurd f

instance Finite Bool 2 where
  isFinite = MkIso to from ok1 ok2
    where to : Bool -> Fin 2
          to False = 0
          to True  = 1
          from : Fin 2 -> Bool
          from FZ = False
          from (FS FZ) = True
          from (FS (FS x)) = absurd x
          ok1 : (f : Fin 2) -> to (from f) = f
          ok1 FZ = Refl
          ok1 (FS FZ) = Refl
          ok1 (FS (FS x)) = absurd x
          ok2 : (b : Bool) -> from (to b) = b
          ok2 False = Refl
          ok2 True = Refl

-- Isomorphisms over Maybe
maybeVoidUnit2 : Iso (Maybe Void) ()
maybeVoidUnit2 = MkIso to from iso1 iso2
  where to : Maybe Void -> ()
        to Nothing = ()
        to (Just x) = absurd x
        from : () -> Maybe Void
        from () = Nothing
        iso1 : (x : ()) -> to (from x) = x
        iso1 () = Refl
        iso2 : (y : Maybe Void) -> from (to y) = y
        iso2 Nothing = Refl
        iso2 (Just x) = absurd x

max_stars_repo_name: david-christiansen/idris-utils

max_issues_repo_name: david-christiansen/idris-utils

max_forks_repo_name: david-christiansen/idris-utils


text:
import Data.List
import Data.Nat
import Data.SortedMap
import Control.Monad.State
import Control.Monad.State.State
import Control.Monad.State.Interface

record Player where
  constructor MkPlayer
  score : Nat
  pos : Nat

Eq Player where
  p1 == p2 = p1.score == p2.score && p1.pos == p2.pos

Ord Player where
  compare p1 p2 = compare (p1.score, p1.pos) (p2.score, p2.pos)

data Turn = P1 | P2

Eq Turn where
  P1 == P1 = True
  P2 == P2 = True
  _  == _  = False

Ord Turn where
  compare P1 P1 = EQ
  compare P1 P2 = LT
  compare P2 P1 = GT
  compare P2 P2 = EQ

next : Turn -> Turn
next P1 = P2
next P2 = P1

record Game where
  constructor MkGame
  player1, player2 : Player
  turn : Turn
  rolls : Nat

fromStart : Nat -> Nat -> Game
fromStart p1 p2 = MkGame (MkPlayer 0 p1) (MkPlayer 0 p2) P1 0

score : Game -> Nat
score (MkGame p1 p2 _ rolls) = (*) rolls $ max p1.score  p2.score

rollDet : State Game Nat
rollDet = do rolls <- gets (.rolls)
             modify { rolls $= S }
             pure $ 1 + (modNatNZ rolls 100 SIsNonZero)

movePlayer : Nat -> Player -> Player
movePlayer m (MkPlayer score pos) = let npos = (modNatNZ (pos + m) 10 SIsNonZero) in
                                         MkPlayer (score + npos + 1) npos

playDet : State Game ()
playDet = do rolls <- sequence $ replicate 3 rollDet
             let r = sum rolls
             turn <- gets (.turn)
             case turn of
                  P1 => modify { player1 $= movePlayer r }
                  P2 => modify { player2 $= movePlayer r }
             s1 <- gets (.player1.score)
             s2 <- gets (.player2.score)
             if s1 >= 1000 || s2 >= 1000
                then pure ()
                else modify { turn $= next } *> playDet

part1 : Game -> IO String
part1 a = do let g = execState a playDet
             pure $ show $ score g

Memoize : Type
Memoize = SortedMap (Player, Player, Turn) (Nat, Nat)

addPair : Num a => (a, a) -> (a, a) -> (a, a)
addPair (x, y) (z, w) = (x + z, y + w)

wins : Player -> Bool
wins (MkPlayer score pos) = score >= 21

playDirac : Nat -> Memoize -> Game -> ((Nat, Nat), Memoize)
playDirac _ m (MkGame p1 p2 turn 0) = case lookup (p1, p2, turn) m of
                                           (Just w) => (w, m)
                                           Nothing => let (w, m) = foldl (\(w, m) => \d => mapFst (addPair w) $ playDirac d m (MkGame p1 p2 turn 1)) ((0, 0), m) $ [1,2,3] in
                                                          (w, insert (p1, p2, turn) w m)
playDirac s m (MkGame p1 p2 P1 3) = let p1' = movePlayer s p1 in
                                        if wins p1'
                                           then ((1, 0), m)
                                           else playDirac 0 m (MkGame p1' p2 P2 0)
playDirac s m (MkGame p1 p2 P2 3) = let p2' = movePlayer s p2 in
                                        if wins p2'
                                           then ((0, 1), m)
                                           else playDirac 0 m (MkGame p1 p2' P1 0)
playDirac s m (MkGame p1 p2 turn r) = foldl (\(w, m) => \d => mapFst (addPair w) $ playDirac (s + d) m (MkGame p1 p2 turn (1 + r))) ((0, 0), m) $ [1,2,3]

part2 : Game -> IO String
part2 a = do let (wins, _) = playDirac 0 empty a
             pure $ show $ (uncurry max) wins

main : IO ()
main = do let g = fromStart 2 9
          part1 g >>= putStrLn
          part2 g >>= putStrLn


text:
module IR.Layout

import IR
import IR.StackSet

%default total

column : Rectangle -> (n : Nat) -> Vect n Rectangle
column r n = column' n r n
  where column' _ _ Z = []
        column' n (MkRectangle x y w h) (S m) =
          let w' = w / fromInteger (toIntegerNat n)
          in MkRectangle (x + w' * fromInteger (toIntegerNat m)) y w' h :: column' n r m

fullLayout : LayoutF wid
fullLayout rect s = zip (integrate s) (replicate (stackLength s) rect)

columnLayout : LayoutF wid
columnLayout rect s = zip (integrate s) (column rect (stackLength s))

mirrorLayout : LayoutF wid -> LayoutF wid
mirrorLayout l (MkRectangle x' y' w' h') s = map (\(wid, MkRectangle x y w h) => (wid, MkRectangle ((y - y') / h' * w' + x') ((x - x') / w' * h' + y') (h / h' * w') (w / w' * h'))) (l (MkRectangle x' y' w' h') s)

single : LayoutF wid -> Layout wid
single l = x
  where x = MkLayout l x

choose : Vect (S n) (LayoutF wid) -> Layout wid
choose {n} {wid} (x::xs) =
  let xs' : Vect (S n) (LayoutF wid) = rewrite plusCommutative 1 n in xs ++ [x]
  in MkLayout x (choose xs')

max_stars_repo_name: puffnfresh/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
module Example.Stream

import Data.Fin
import Flexidisc.Record

RecordMPair : (Type -> Type) -> Type
RecordMPair m = RecordM m (Fin 2) [FZ ::: Nat, FS FZ ::: Char]

test : RecordMPair Stream
test = [0 := [1..], 1 := pure 'c']

someOfTest : List (RecordMPair Basics.id)
someOfTest = take 10 (sequence test)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
{- IdrisWeb Session System
   Makes use of effects library to allow for persistent sessions.

   Exploits to prevent against:
    - Fixation
      - Session ID *MUST* be regenerated when the user logs in.
    - Brute force
      - Big numbers, cryptographically secure and random
    - Sniffing (also todo: SSL)
      - Only allow sessions to be sent over an SSL connection
-}
module IdrisWeb.Session.Session
import IdrisWeb.DB.SQLite.SQLiteNew
import Effects
import IdrisWeb.Common.Random.RandC
import SimpleParser
%access public

-- SessionID should be some long-ish random string (hash?)
SessionID : Type
SessionID = String

private
DB_NAME : String
DB_NAME = "/tmp/sessions.db"

-- I think in this circumstance, tagged data types
-- would be better, since we're not passing directly
-- to a function, more just providing other functions
-- with data.
data SessionDataType = SInt Int
                     | SString String
                     | SBool Bool
                     | SNull
total
showSerialisedVal : SessionDataType -> (String, String)
showSerialisedVal (SInt i) = ("SInt", show i)
showSerialisedVal (SString s) = ("SString", s)
showSerialisedVal (SBool b) = ("SBool", show b)
showSerialisedVal (SNull) = ("SNull", "")

-- Given a serialised value from the DB, construct
-- the appropriate data type.
-- TODO: Probably a better way of doing it than storing the
-- type as a string in the DB: an enum would likely be better
--total
deserialiseVal : String -> String -> Maybe SessionDataType
deserialiseVal tystr s =
  if tystr == "SInt" then case parse int s of
                               Left err => Nothing
                               Right (i, _) => Just $ SInt i
  else if tystr == "SString" then Just $ SString s
  else if tystr == "SBool" then case parse bool s of
                                     Left err => Nothing
                                     Right (b, _) => Just $ SBool b
  else if tystr == "SNull" then Just SNull
  else Nothing

-- SerialisedSession is a list of 3-tuples of <Key, Value, Type>.
SerialisedSessionEntry : Type
SerialisedSessionEntry = (String, String, String)

public -- this really shouldn't be public, TODO: change
SerialisedSession : Type
SerialisedSession = List SerialisedSessionEntry

-- SessionData is the user-facing data type, containing the session names and variables
public
SessionData : Type
SessionData = List (String, SessionDataType)

{-
deserialiseSession : SerialisedSession -> Maybe SessionData
deserialiseSession ss = sequence $ map (\(key, val, ty) => case (deserialiseVal ty val) of
  Just dat => Just (key, dat)
  Nothing => Nothing) ss
-}

deserialiseSession : SerialisedSession -> Maybe SessionData
deserialiseSession ss = traverse (\(key, val, ty) => case (deserialiseVal ty val) of
                                                       Just dat => Just (key, dat)
                                                       Nothing => Nothing) ss

-- showSerialisedVal : (String, String)
serialiseSession : SessionData -> SerialisedSession
serialiseSession sd = map (\(key, sdt) => let (tystr, valstr) = showSerialisedVal sdt in
                                              (key, valstr, tystr)) sd

-- Retrieves session data as a list of (String, String) k-v pairs.
-- We marshal this back to the required types in a later function.
collectResults : EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow) (SQLiteExecuting ValidRow))]
                         [SQLITE (SQLiteExecuting InvalidRow)]
                 SerialisedSession
collectResults =
  if_valid then do
    key <- getColumnText 0
    val <- getColumnText 1
    ty <- getColumnText 2
    step_result <- nextRow
    xs <- collectResults
    Effects.pure $ (key, val, ty) :: xs
  else Effects.pure []

retrieveSessionData : SessionID -> Eff IO [SQLITE ()] (Either QueryError SerialisedSession)
retrieveSessionData s_id = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let sql = "SELECT key, val, ty FROM `sessiondata` WHERE `session_key` = ?"
    ps_res <- prepareStatement sql
    if_valid then do
      bindText 1 s_id
      bind_res <- finishBind
      if_valid then do
        executeStatement
        results <- collectResults
        finaliseInvalid
        closeDB
        Effects.pure $ Right results
      else do
        let be = getBindError bind_res
        cleanupBindFail
        Effects.pure $ Left be
    else do
      cleanupPSFail
      Effects.pure . Left $ getQueryError ps_res
  else
    Effects.pure . Left $ getQueryError conn_res

--removeSessionData : SessionID -> Eff IO [SQLITE ()]

getInsertArg : SerialisedSession -> String
getInsertArg [] = ""
-- no comma needed at the end
getInsertArg ((key, val, ty) :: []) = "(\"" ++ key ++ "\", \"" ++ val ++ "\", \"" ++ ty ++ "\")"
getInsertArg ((key, val, ty) :: xs) = "(\"" ++ key ++ "\", \"" ++ val ++ "\", \"" ++ ty ++ "\")" ++ ", " ++ (getInsertArg xs)

storeSessionRow : SessionID -> SerialisedSessionEntry -> Eff IO [SQLITE ()] (Either QueryError ())
storeSessionRow s_id (key, val, ty) = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let insert_sql = "INSERT INTO `sessiondata` (`session_key`, `key`, `val`, `ty`) VALUES (?, ?, ?, ?)"
    ps_res <- prepareStatement insert_sql
    if_valid then do
      -- Bind the arguments to the prepared statement
      bindText 1 s_id
      bindText 2 key
      bindText 3 val
      bindText 4 ty
      bind_res <- finishBind
      if_valid then do
        executeStatement
        finalise
        closeDB
        Effects.pure $ Right ()
      else do
        let be = getBindError bind_res
        cleanupBindFail
        Effects.pure $ Left be
    else do
      cleanupPSFail
      Effects.pure . Left $ getQueryError ps_res
  else
    Effects.pure . Left $ getQueryError conn_res

storeSessionData : SessionID -> SerialisedSession -> Eff IO [SQLITE ()] (Either QueryError ())
storeSessionData s_id [] = Effects.pure $ Right ()
storeSessionData s_id (sr :: srs) = do res <- storeSessionRow s_id sr
                                       case res of
                                            Left err => Effects.pure $ Left err
                                            Right () => storeSessionData s_id srs

removeSession: SessionID -> Eff IO [SQLITE ()] (Either QueryError ())
removeSession s_id = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let delete_sql = "DELETE FROM `sessiondata` WHERE `session_key` = ?"
    ps_res <- prepareStatement delete_sql
    if_valid then do
      bindText 1 s_id
      bind_res <- finishBind
      if_valid then do
        executeStatement
        finalise
        closeDB
        Effects.pure $ Right ()
      else do
        let be = getBindError bind_res
        cleanupBindFail
        Effects.pure $ Left be
    else do
      cleanupPSFail
      Effects.pure . Left $ getQueryError ps_res
  else
    Effects.pure . Left $ getQueryError conn_res

-- Remove then store
updateSessionData : SessionID -> SessionData -> Eff IO [SQLITE ()] (Either QueryError ())
updateSessionData s_id sd = do
  del_res <- removeSession s_id
  case del_res of
       Left err => Effects.pure $ Left err
       Right () => do store_res <- storeSessionData s_id (serialiseSession sd)
                      case store_res of
                        Left err' => Effects.pure $ Left err'
                        Right () => Effects.pure $ Right ()

getSession : SessionID -> IO (Maybe SessionData)
getSession s_id = do db_res <- run [()] (retrieveSessionData s_id)
                     case db_res of
                          Left err => pure Nothing
                          Right ss => pure $ deserialiseSession ss

{- Session effect:
   We should be able to create, update and delete sessions.
   We should only be able to update and delete valid sessions.
   We should only be able to create sessions when we don't have an active session.
   We really should only be able to populate a session after authentication
      if we generate a new session (in order to prevent session fixation attacks (but how... hmmmm)
-}

data SessionStep = SessionUninitialised
                 | SessionInitialised

public
data SessionRes : SessionStep -> Type where
  InvalidSession : SessionRes s
  ValidSession : SessionID -> SessionData -> SessionRes s

data Session : Effect where
  -- Load a session from the database, given a session ID.
  LoadSession : SessionID -> Session (SessionRes SessionUninitialised) (SessionRes SessionInitialised) (Maybe SessionData)
  -- Updates the in-memory representation of the session
  UpdateSession : SessionData -> Session (SessionRes SessionInitialised) (SessionRes SessionInitialised) ()
  -- Given a session data set, creates a new session
  CreateSession : SessionData -> Session (SessionRes SessionUninitialised) (SessionRes SessionInitialised) (Maybe SessionID)
  -- Delete the current session
  DeleteSession : Session (SessionRes SessionInitialised) (SessionRes SessionUninitialised) Bool -- Hmmm... Error handling? How?
  -- Updates the DB with the new session data, discards the in-memory resources
  WriteToDB : Session (SessionRes SessionInitialised) (SessionRes SessionUninitialised) Bool
  -- Discards changes to the current session, disposes of resources
  DiscardSessionChanges : Session (SessionRes SessionInitialised) (SessionRes SessionUninitialised) ()

  GetSessionID : Session (SessionRes SessionInitialised) (SessionRes SessionInitialised) (Maybe SessionID)

  GetSessionData : Session (SessionRes SessionInitialised) (SessionRes SessionInitialised) (Maybe SessionData)

SESSION : Type -> EFFECT
SESSION t = MkEff t Session

loadSession : SessionID -> EffM m [SESSION (SessionRes SessionUninitialised)]
                                  [SESSION (SessionRes SessionInitialised)]
                                  (Maybe SessionData)
loadSession s_id = (LoadSession s_id)

updateSession : SessionData -> Eff m [SESSION (SessionRes SessionInitialised)] ()
updateSession sd = (UpdateSession sd)

createSession : SessionData -> EffM m [SESSION (SessionRes SessionUninitialised)]
                                      [SESSION (SessionRes SessionInitialised)]
                                      (Maybe SessionID)
createSession sd = (CreateSession sd)

deleteSession : EffM m [SESSION (SessionRes SessionInitialised)]
                       [SESSION (SessionRes SessionUninitialised)]
                       Bool
deleteSession = DeleteSession

writeSessionToDB : EffM m [SESSION (SessionRes SessionInitialised)]
                          [SESSION (SessionRes SessionUninitialised)]
                          Bool
writeSessionToDB = WriteToDB

discardSession : EffM m [SESSION (SessionRes SessionInitialised)]
                        [SESSION (SessionRes SessionUninitialised)]
                        ()
discardSession = DiscardSessionChanges

getSessionID : Eff m [SESSION (SessionRes SessionInitialised)]
                     (Maybe SessionID)
getSessionID = GetSessionID

getSessionData : Eff m [SESSION (SessionRes SessionInitialised)]
                       (Maybe SessionData)
getSessionData = GetSessionData

instance Handler Session IO where
  -- Grab the session from the DB given the session key.
  -- If it exists, construct the resource and return the data.
  -- If not, return nothing, and reflect the invalidity in the resource.

  -- This should never happen
  handle (ValidSession _ _) (LoadSession _) k = k InvalidSession Nothing

  handle InvalidSession (LoadSession s_id) k = do
    maybe_session <- getSession s_id
    case maybe_session of
         Just s_data => k (ValidSession s_id s_data) (Just s_data)
         Nothing => k InvalidSession Nothing

  -- Update the in-memory representation of the session.
  handle (ValidSession s_id s_dat) (UpdateSession s_dat') k =
    k (ValidSession s_id s_dat') ()

  -- If we're trying to update an invalid session, just let it fall
  -- through.
  handle (InvalidSession) (UpdateSession _) k =
   k (InvalidSession) ()

  -- Delete a session from the database, and dispose of our resources.
  handle (ValidSession s_id _) DeleteSession k = do
    delete_res <- run [()] (removeSession s_id)
    case delete_res of
         Left err => k InvalidSession False
         Right () => k InvalidSession True

  handle (InvalidSession) DeleteSession k = k InvalidSession False

  -- Writes a session to the DB, and disposes of the in-memory resources
  handle (ValidSession s_id s_dat) WriteToDB k = do
    update_res <- run [()] (updateSessionData s_id s_dat)
    case update_res of
         Left err => do putStrLn (show err)
                        k InvalidSession False
         Right () => k InvalidSession True

  handle InvalidSession WriteToDB k = k InvalidSession False

  -- Simply discard the resource without doing any writes
  handle (ValidSession _ _) DiscardSessionChanges k = k InvalidSession ()
  handle (InvalidSession) DiscardSessionChanges k = k InvalidSession ()

  handle (ValidSession _ _) (CreateSession _) k = k InvalidSession Nothing
  -- Creates a new session.
  -- BIG TODO: This random number gen is extremely rudimentary, and not
  -- secure enough for actual use.
  -- We've also got no guarantees that the IDs generated will be unique...
  -- This can be fixed by having some sort of property variable in the session
  -- DB, which we increment each time, and hash alongside the random number.
  -- While OK for a quick prototype, this *REALLY* must be fixed.
  handle InvalidSession (CreateSession sd) k = do
    rand_id <- getRandom 1000000000 21474836476 -- FIXME: This is a pathetic level of entropy...
    let s_id = show rand_id -- Some hash function would be here, typically
    store_res <- run [()] (storeSessionData s_id (serialiseSession sd))
    case store_res of
      Left err' => k InvalidSession Nothing
      Right () => k (ValidSession s_id sd) (Just s_id)

  handle (ValidSession s_id s_dat) GetSessionID k = k (ValidSession s_id s_dat) (Just s_id)
  handle (ValidSession s_id s_dat) GetSessionData k = k (ValidSession s_id s_dat) (Just s_dat)
  handle InvalidSession GetSessionID k = k InvalidSession Nothing
  handle InvalidSession GetSessionData k = k InvalidSession Nothing

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Data.SortedMap

import Data.Nat

-- TODO: write split

private
data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where
  Leaf : k -> v -> Tree Z k v o
  Branch2 : Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o
  Branch3 : Tree n k v o -> k -> Tree n k v o -> k -> Tree n k v o -> Tree (S n) k v o

branch4 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch4 a b c d e f g =
  Branch2 (Branch2 a b c) d (Branch2 e f g)

branch5 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch5 a b c d e f g h i =
  Branch2 (Branch2 a b c) d (Branch3 e f g h i)

branch6 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch6 a b c d e f g h i j k =
  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

branch7 :
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o -> k ->
  Tree n k v o ->
  Tree (S (S n)) k v o
branch7 a b c d e f g h i j k l m =
  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

merge1 : Tree n k v o -> k -> Tree (S n) k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge2 : Tree (S n) k v o -> k -> Tree n k v o -> k -> Tree (S n) k v o -> Tree (S (S n)) k v o
merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge3 : Tree (S n) k v o -> k -> Tree (S n) k v o -> k -> Tree n k v o -> Tree (S (S n)) k v o
merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

treeLookup : (Ord k) => k -> Tree n k v o -> Maybe v
treeLookup k (Leaf k' v) =
 if k == k'
 then Just v
 else Nothing
treeLookup k (Branch2 t1 k' t2) =
  if k <= k' then
    treeLookup k t1
  else
    treeLookup k t2
treeLookup k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    treeLookup k t1
  else if k <= k2 then
    treeLookup k t2
  else
    treeLookup k t3

treeInsert' : (Ord k) => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree n k v o, k, Tree n k v o)
treeInsert' k v (Leaf k' v') =
  case compare k k' of
    LT => Right (Leaf k v, k, Leaf k' v')
    EQ => Left (Leaf k v)
    GT => Right (Leaf k' v', k', Leaf k v)
treeInsert' k v (Branch2 t1 k' t2) =
  if k <= k' then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right (a, b, c) => Left (Branch3 a b c k' t2)
  else
    case treeInsert' k v t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right (a, b, c) => Left (Branch3 t1 k' a b c)
treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
  else
    if k <= k2 then
      case treeInsert' k v t2 of
        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
    else
      case treeInsert' k v t3 of
        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)

treeInsert : (Ord k) => k -> v -> Tree n k v o -> Either (Tree n k v o) (Tree (S n) k v o)
treeInsert k v t =
  case treeInsert' k v t of
    Left t' => Left t'
    Right (a, b, c) => Right (Branch2 a b c)

delType : Nat -> (k : Type) -> Type -> Ord k -> Type
delType Z k v o = ()
delType (S n) k v o = Tree n k v o

treeDelete : (Ord k) => {n : Nat} -> k -> Tree n k v o -> Either (Tree n k v o) (delType n k v o)
treeDelete k (Leaf k' v) =
  if k == k' then
    Right ()
  else
    Left (Leaf k' v)
treeDelete {n=S Z} k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right () => Right t2
  else
    case treeDelete k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right () => Right t1
treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right () => Left (Branch2 t2 k2 t3)
  else if k <= k2 then
    case treeDelete k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right () => Left (Branch2 t1 k1 t3)
  else
    case treeDelete k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right () => Left (Branch2 t1 k1 t2)
treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right t1' =>
        case t2 of
          Branch2 a b c => Right (Branch3 t1' k' a b c)
          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
  else
    case treeDelete k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right t2' =>
        case t1 of
          Branch2 a b c => Right (Branch3 a b c k' t2')
          Branch3 a b c d e => Left (branch4 a b c d e k' t2')
treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right t1' => Left (merge1 t1' k1 t2 k2 t3)
  else if k <= k2 then
    case treeDelete k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right t2' => Left (merge2 t1 k1 t2' k2 t3)
  else
    case treeDelete k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right t3' => Left (merge3 t1 k1 t2 k2 t3')

treeToList : {n: Nat} -> Tree n k v o -> List (k, v)
treeToList = treeToList' (:: [])
  where
    treeToList' : ((k, v) -> List (k, v)) -> {n: Nat} -> Tree n k v o -> List (k, v)
    treeToList' cont {n = Z} (Leaf k v) = cont (k, v)
    treeToList' cont (Branch2 t1 _ t2) = treeToList' (:: treeToList' cont t2) t1
    treeToList' cont (Branch3 t1 _ t2 _ t3) = treeToList' (:: treeToList' (:: treeToList' cont t3) t2) t1

public export
data SortedMap : Type -> Type -> Type where
  Empty : Ord k => SortedMap k v
  M : (o : Ord k) => (n:Nat) -> Tree n k v o -> SortedMap k v

export
empty : Ord k => SortedMap k v
empty = Empty

export
lookup : k -> SortedMap k v -> Maybe v
lookup _ Empty = Nothing
lookup k (M _ t) = treeLookup k t

export
insert : k -> v -> SortedMap k v -> SortedMap k v
insert k v Empty = M Z (Leaf k v)
insert k v (M _ t) =
  case treeInsert k v t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v
insertFrom = flip $ foldl $ flip $ uncurry insert

export
delete : k -> SortedMap k v -> SortedMap k v
delete _ Empty = Empty
delete k (M Z t) =
  case treeDelete k t of
    Left t' => (M _ t')
    Right () => Empty
delete k (M (S _) t) =
  case treeDelete k t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
fromList : Ord k => List (k, v) -> SortedMap k v
fromList l = foldl (flip (uncurry insert)) empty l

export
toList : SortedMap k v -> List (k, v)
toList Empty = []
toList (M _ t) = treeToList t

||| Gets the keys of the map.
export
keys : SortedMap k v -> List k
keys = map fst . toList

||| Gets the values of the map. Could contain duplicates.
export
values : SortedMap k v -> List v
values = map snd . toList

export
null : SortedMap k v -> Bool
null Empty = True
null (M _ _) = False

treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
treeMap f (Leaf k v) = Leaf k (f v)
treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
treeMap f (Branch3 t1 k1 t2 k2 t3)
    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

export
implementation Functor (SortedMap k) where
  map _ Empty = Empty
  map f (M n t) = M _ (treeMap f t)

||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
||| Uses the ordering of the first map given.
export
mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v
mergeWith f x y = insertFrom inserted x where
  inserted : List (k, v)
  inserted = do
    (k, v) <- toList y
    let v' = (maybe id f $ lookup k x) v
    pure (k, v')

||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
||| Uses mergeWith internally, so the ordering of the left map is kept.
export
merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v
merge = mergeWith (<+>)

||| Left-biased merge, also keeps the ordering specified  by the left map.
export
mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v
mergeLeft = mergeWith const

export
(Show k, Show v) => Show (SortedMap k v) where
   show m = "fromList " ++ (show $ toList m)

-- TODO: is this the right variant of merge to use for this? I think it is, but
-- I could also see the advantages of using `mergeLeft`. The current approach is
-- strictly more powerful I believe, because `mergeLeft` can be emulated with
-- the `First` monoid. However, this does require more code to do the same
-- thing.
export
Semigroup v => Semigroup (SortedMap k v) where
  (<+>) = merge

||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.
||| However, semantically, it should be equal.
export
(Ord k, Semigroup v) => Monoid (SortedMap k v) where
  neutral = empty

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames