text:
module Idris.Elab.Interface

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.TT
import Core.Unify
import Core.Value

import Idris.Resugar
import Idris.Syntax

import TTImp.BindImplicits
import TTImp.ProcessDecls
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Unelab
import TTImp.TTImp
import TTImp.Utils

import Data.ANameMap
import Data.List
import Data.Maybe

%default covering

-- TODO: Check all the parts of the body are legal
-- TODO: Deal with default superclass implementations

mkDataTy : FC -> List (Name, RawImp) -> RawImp
mkDataTy fc [] = IType fc
mkDataTy fc ((n, ty) :: ps)
    = IPi fc top Explicit (Just n) ty (mkDataTy fc ps)

mkIfaceData : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> Visibility -> Env Term vars ->
              List (Maybe Name, RigCount, RawImp) ->
              Name -> Name -> List (Name, RawImp) ->
              List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
mkIfaceData {vars} fc vis env constraints n conName ps dets meths
    = let opts = if isNil dets
                    then [NoHints, UniqueSearch]
                    else [NoHints, UniqueSearch, SearchBy dets]
          retty = apply (IVar fc n) (map (IVar fc) (map fst ps))
          conty = mkTy Implicit (map jname ps) $
                  mkTy Explicit (map bhere constraints ++ map bname meths) retty
          con = MkImpTy fc conName !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars) conty) in
          pure $ IData fc vis (MkImpData fc n
                                  !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars)
                                                  (mkDataTy fc ps))
                                  opts [con])
  where
    jname : (Name, RawImp) -> (Maybe Name, RigCount, RawImp)
    jname (n, t) = (Just n, erased, t)

    bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
    bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t)

    bhere : (Maybe Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
    bhere (n, c, t) = (n, c, IBindHere (getFC t) (PI erased) t)

    mkTy : PiInfo RawImp ->
           List (Maybe Name, RigCount, RawImp) -> RawImp -> RawImp
    mkTy imp [] ret = ret
    mkTy imp ((n, c, argty) :: args) ret
        = IPi fc c imp n argty (mkTy imp args ret)

-- Give implicit Pi bindings explicit names, if they don't have one already,
-- because we need them to be consistent everywhere we refer to them
namePis : Int -> RawImp -> RawImp
namePis i (IPi fc r AutoImplicit Nothing ty sc)
    = IPi fc r AutoImplicit (Just (MN "i_con" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r Implicit Nothing ty sc)
    = IPi fc r Implicit (Just (MN "i_imp" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r p n ty sc)
    = IPi fc r p n ty (namePis i sc)
namePis i (IBindHere fc m ty) = IBindHere fc m (namePis i ty)
namePis i ty = ty

-- Get the implicit arguments for a method declaration or constraint hint
-- to allow us to build the data declaration
getMethDecl : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Env Term vars -> NestedNames vars ->
              (params : List (Name, RawImp)) ->
              (mnames : List Name) ->
              (FC, RigCount, List FnOpt, n, (Bool, RawImp)) ->
              Core (n, RigCount, RawImp)
getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
    = do ty_imp <- bindTypeNames [] (map fst params ++ mnames ++ vars) ty
         pure (n, c, stripParams (map fst params) ty_imp)
  where
    -- We don't want the parameters to explicitly appear in the method
    -- type in the record for the interface (they are parameters of the
    -- interface type), so remove it here
    stripParams : List Name -> RawImp -> RawImp
    stripParams ps (IPi fc r p mn arg ret)
        = if (maybe False (\n => n `elem` ps) mn)
             then stripParams ps ret
             else IPi fc r p mn arg (stripParams ps ret)
    stripParams ps ty = ty

-- bind the auto implicit for the interface - put it after all the other
-- implicits
bindIFace : FC -> RawImp -> RawImp -> RawImp
bindIFace _ ity (IPi fc rig Implicit n ty sc)
       = IPi fc rig Implicit n ty (bindIFace fc ity sc)
bindIFace _ ity (IPi fc rig AutoImplicit n ty sc)
       = IPi fc rig AutoImplicit n ty (bindIFace fc ity sc)
bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN "__con")) ity sc

-- Get the top level function for implementing a method
getMethToplevel : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  Env Term vars -> Visibility ->
                  Name -> Name ->
                  (constraints : List (Maybe Name)) ->
                  (allmeths : List Name) ->
                  (params : List (Name, RawImp)) ->
                  (FC, RigCount, List FnOpt, Name, (Bool, RawImp)) ->
                  Core (List ImpDecl)
getMethToplevel {vars} env vis iname cname constraints allmeths params
                (fc, c, opts, n, (d, ty))
    = do let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
         -- Make the constraint application explicit for any method names
         -- which appear in other method types
         let ty_constr =
             bindPs params $ substNames vars (map applyCon allmeths) ty
         ty_imp <- bindTypeNames [] vars (bindIFace fc ity ty_constr)
         cn <- inCurrentNS n
         let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
                                            else [Inline])
                                      (MkImpTy fc cn ty_imp)
         let conapp = apply (IVar fc cname)
                         (map (const (Implicit fc True)) constraints ++
                          map (IBindVar fc) (map bindName allmeths))
         let argns = getExplicitArgs 0 ty
         -- eta expand the RHS so that we put implicits in the right place
         let fnclause = PatClause fc (IImplicitApp fc (IVar fc cn)
                                                   (Just (UN "__con"))
                                                   conapp)
                                  (mkLam argns
                                    (apply (IVar fc (methName n))
                                           (map (IVar fc) argns)))
         let fndef = IDef fc cn [fnclause]
         pure [tydecl, fndef]
  where
    -- Bind the type parameters given explicitly - there might be information
    -- in there that we can't infer after all
    bindPs : List (Name, RawImp) -> RawImp -> RawImp
    bindPs [] ty = ty
    bindPs ((n, pty) :: ps) ty
        = IPi (getFC pty) erased Implicit (Just n) pty (bindPs ps ty)

    applyCon : Name -> (Name, RawImp)
    applyCon n = (n, IImplicitApp fc (IVar fc n)
                             (Just (UN "__con")) (IVar fc (UN "__con")))

    getExplicitArgs : Int -> RawImp -> List Name
    getExplicitArgs i (IPi _ _ Explicit n _ sc)
        = MN "arg" i :: getExplicitArgs (i + 1) sc
    getExplicitArgs i (IPi _ _ _ n _ sc) = getExplicitArgs i sc
    getExplicitArgs i tm = []

    mkLam : List Name -> RawImp -> RawImp
    mkLam [] tm = tm
    mkLam (x :: xs) tm
       = ILam fc top Explicit (Just x) (Implicit fc False) (mkLam xs tm)

    bindName : Name -> String
    bindName (UN n) = "__bind_" ++ n
    bindName (NS _ n) = bindName n
    bindName n = show n

    methName : Name -> Name
    methName n = UN (bindName n)

-- Get the function for chasing a constraint. This is one of the
-- arguments to the record, appearing before the method arguments.
getConstraintHint : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    FC -> Env Term vars -> Visibility ->
                    Name -> Name ->
                    (constraints : List Name) ->
                    (allmeths : List Name) ->
                    (params : List Name) ->
                    (Name, RawImp) -> Core (Name, List ImpDecl)
getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)
    = do let ity = apply (IVar fc iname) (map (IVar fc) params)
         let fty = IPi fc top Explicit Nothing ity con
         ty_imp <- bindTypeNames [] (meths ++ vars) fty
         let hintname = DN ("Constraint " ++ show con)
                          (UN ("__" ++ show iname ++ "_" ++ show con))
         let tydecl = IClaim fc top vis [Inline, Hint False]
                          (MkImpTy fc hintname ty_imp)
         let conapp = apply (IVar fc cname)
                        (map (IBindVar fc) (map bindName constraints) ++
                         map (const (Implicit fc True)) meths)
         let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)
                                  (IVar fc (constName cn))
         let fndef = IDef fc hintname [fnclause]
         pure (hintname, [tydecl, fndef])
  where
    bindName : Name -> String
    bindName (UN n) = "__bind_" ++ n
    bindName (NS _ n) = bindName n
    bindName n = show n

    constName : Name -> Name
    constName n = UN (bindName n)

getSig : ImpDecl -> Maybe (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
getSig (IClaim _ c _ opts (MkImpTy fc n ty))
    = Just (fc, c, opts, n, (False, namePis 0 ty))
getSig (IData _ _ (MkImpLater fc n ty))
    = Just (fc, erased, [Invertible], n, (True, namePis 0 ty))
getSig _ = Nothing

getDefault : ImpDecl -> Maybe (FC, List FnOpt, Name, List ImpClause)
getDefault (IDef fc n cs) = Just (fc, [], n, cs)
getDefault _ = Nothing

mkCon : FC -> Name -> Name
mkCon loc (NS ns (UN n))
   = NS ns (DN (n ++ " at " ++ show loc) (UN ("__mk" ++ n)))
mkCon loc n
   = DN (show n ++ " at " ++ show loc) (UN ("__mk" ++ show n))

updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Name -> Name -> List Name -> List Name -> List RawImp ->
                 List (Name, RigCount, List FnOpt, (Bool, RawImp)) -> List (Name, List ImpClause) ->
                 Core ()
updateIfaceSyn iname cn impps ps cs ms ds
    = do syn <- get Syn
         ms' <- traverse totMeth ms
         let info = MkIFaceInfo cn impps ps cs ms' ds
         put Syn (record { ifaces $= addName iname info,
                           saveIFaces $= (iname :: ) } syn)
 where
    findSetTotal : List FnOpt -> Maybe TotalReq
    findSetTotal [] = Nothing
    findSetTotal (Totality t :: _) = Just t
    findSetTotal (_ :: xs) = findSetTotal xs

    totMeth : (Name, RigCount, List FnOpt, (Bool, RawImp)) ->
              Core (Name, RigCount, Maybe TotalReq, (Bool, RawImp))
    totMeth (n, c, opts, t)
        = do let treq = findSetTotal opts
             pure (n, c, treq, t)

-- Read the implicitly added parameters from an interface type, so that we
-- know to substitute an implicit in when defining the implementation
getImplParams : Term vars -> List Name
getImplParams (Bind _ n (Pi _ _ Implicit _) sc)
    = n :: getImplParams sc
getImplParams _ = []

export
elabInterface : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto s : Ref Syn SyntaxInfo} ->
                {auto m : Ref MD Metadata} ->
                FC -> Visibility ->
                Env Term vars -> NestedNames vars ->
                (constraints : List (Maybe Name, RawImp)) ->
                Name ->
                (params : List (Name, RawImp)) ->
                (dets : List Name) ->
                (conName : Maybe Name) ->
                List ImpDecl ->
                Core ()
elabInterface {vars} fc vis env nest constraints iname params dets mcon body
    = do fullIName <- getFullName iname
         ns_iname <- inCurrentNS fullIName
         let conName_in = maybe (mkCon fc fullIName) id mcon
         -- Machine generated names need to be qualified when looking them up
         conName <- inCurrentNS conName_in
         let meth_sigs = mapMaybe getSig body -- (FC, RigCount, List FnOpt, Name, (Bool, RawImp))
         let meth_decls = map (\ (f, c, o, n, b, ty) => (n, c, o, b, ty)) meth_sigs
         let meth_names = map fst meth_decls
         let defaults = mapMaybe getDefault body

         elabAsData conName meth_names meth_sigs
         elabConstraintHints conName meth_names
         elabMethods conName meth_names meth_sigs
         ds <- traverse (elabDefault meth_decls) defaults

         ns_meths <- traverse (\mt => do n <- inCurrentNS (fst mt)
                                         pure (n, snd mt)) meth_decls
         defs <- get Ctxt
         Just ty <- lookupTyExact ns_iname (gamma defs)
              | Nothing => throw (UndefinedName fc iname)
         let implParams = getImplParams ty

         updateIfaceSyn ns_iname conName
                        implParams (map fst params) (map snd constraints)
                        ns_meths ds
  where
    nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
    nameCons i [] = []
    nameCons i ((_, ty) :: rest)
        = (UN ("__con" ++ show i), ty) :: nameCons (i + 1) rest

    -- Elaborate the data declaration part of the interface
    elabAsData : (conName : Name) -> List Name ->
                 List (FC, RigCount, List FnOpt, Name, (Bool, RawImp)) ->
                 Core ()
    elabAsData conName meth_names meth_sigs
        = do -- set up the implicit arguments correctly in the method
             -- signatures and constraint hints
             meths <- traverse (getMethDecl env nest params meth_names) meth_sigs
             log "elab.interface" 5 $ "Method declarations: " ++ show meths

             consts <- traverse (getMethDecl env nest params meth_names)
                                (map (\c => (fc, linear, [], c))
                                   (map notData constraints))
             log "elab.interface" 5 $ "Constraints: " ++ show consts

             dt <- mkIfaceData fc vis env consts iname conName params
                                  dets meths
             log "elab.interface" 10 $ "Methods: " ++ show meths
             log "elab.interface" 5 $ "Making interface data type " ++ show dt
             processDecls nest env [dt]
             pure ()
      where
        notData : (n, t) -> (n, (Bool, t))
        notData (x, y) = (x, (False, y))

    elabMethods : (conName : Name) -> List Name ->
                  List (FC, RigCount, List FnOpt, Name, (Bool, RawImp)) ->
                  Core ()
    elabMethods conName meth_names meth_sigs
        = do -- Methods have same visibility as data declaration
             fnsm <- traverse (getMethToplevel env vis iname conName
                                               (map fst constraints)
                                               meth_names
                                               params) meth_sigs
             let fns = concat fnsm
             log "elab.interface" 5 $ "Top level methods: " ++ show fns
             traverse (processDecl [] nest env) fns
             traverse_ (\n => do mn <- inCurrentNS n
                                 setFlag fc mn Inline
                                 setFlag fc mn TCInline
                                 setFlag fc mn Overloadable) meth_names

    -- Check that a default definition is correct. We just discard it here once
    -- we know it's okay, since we'll need to re-elaborate it for each
    -- instance, to specialise it
    elabDefault : List (Name, RigCount, List FnOpt, Bool, RawImp) ->
                  (FC, List FnOpt, Name, List ImpClause) ->
                  Core (Name, List ImpClause)
    elabDefault tydecls (fc, opts, n, cs)
        = do -- orig <- branch
             let dn_in = MN ("Default implementation of " ++ show n) 0
             dn <- inCurrentNS dn_in

             (rig, dty) <-
                   the (Core (RigCount, RawImp)) $
                       case lookup n tydecls of
                          Just (r, _, _, t) => pure (r, t)
                          Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))

             let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))

             -- Substitute the method names with their top level function
             -- name, so they don't get implicitly bound in the name
             methNameMap <- traverse (\n =>
                                do cn <- inCurrentNS n
                                   pure (n, applyParams (IVar fc cn)
                                                     (map fst params)))
                               (map fst tydecls)
             let dty = substNames vars methNameMap dty

             dty_imp <- bindTypeNames [] (map fst tydecls ++ vars)
                                      (bindIFace fc ity dty)
             log "elab.interface" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
             let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp)
             processDecl [] nest env dtydecl

             let cs' = map (changeName dn) cs
             log "elab.interface" 5 $ "Default method body " ++ show cs'

             processDecl [] nest env (IDef fc dn cs')
             -- Reset the original context, we don't need to keep the definition
             -- Actually we do for the metadata and name map!
--              put Ctxt orig
             pure (n, cs)
      where
        applyParams : RawImp -> List Name -> RawImp
        applyParams tm [] = tm
        applyParams tm (UN n :: ns)
            = applyParams (IImplicitApp fc tm (Just (UN n)) (IBindVar fc n)) ns
        applyParams tm (_ :: ns) = applyParams tm ns

        changeNameTerm : Name -> RawImp -> RawImp
        changeNameTerm dn (IVar fc n')
            = if n == n' then IVar fc dn else IVar fc n'
        changeNameTerm dn (IApp fc f arg)
            = IApp fc (changeNameTerm dn f) arg
        changeNameTerm dn (IImplicitApp fc f x arg)
            = IImplicitApp fc (changeNameTerm dn f) x arg
        changeNameTerm dn tm = tm

        changeName : Name -> ImpClause -> ImpClause
        changeName dn (PatClause fc lhs rhs)
            = PatClause fc (changeNameTerm dn lhs) rhs
        changeName dn (WithClause fc lhs wval flags cs)
            = WithClause fc (changeNameTerm dn lhs) wval
                         flags (map (changeName dn) cs)
        changeName dn (ImpossibleClause fc lhs)
            = ImpossibleClause fc (changeNameTerm dn lhs)

    elabConstraintHints : (conName : Name) -> List Name ->
                          Core ()
    elabConstraintHints conName meth_names
        = do let nconstraints = nameCons 0 constraints
             chints <- traverse (getConstraintHint fc env vis iname conName
                                                 (map fst nconstraints)
                                                 meth_names
                                                 (map fst params)) nconstraints
             log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints
             traverse (processDecl [] nest env) (concatMap snd chints)
             traverse_ (\n => do mn <- inCurrentNS n
                                 setFlag fc mn TCInline) (map fst chints)


text:
module Depling

import Data.Vect
import Debug.Trace
import Utils

infixl 10 =!=
mutual
	public export
	data DAST : Nat -> Type where
		ʌ : Fin n -> DAST n
		λ : DAST n -> DAST (S n) -> DAST n
		λT : DAST n -> DAST (S n) -> DAST n
		(=!=) : DAST n -> DAST n -> DAST n
		𝕋 : DAST n
		𝔽 : DAST n -> DAST (S n) -> DAST (S$ S$ n) -> DAST n
		𝕌 : String -> DAST n -> DAST n
		ℂ : DCon a -> Vect a (DAST n) -> DAST n
		ℙ : DAST n -> DCon a -> DAST (a + n) -> DAST n -> DAST n
		𝔹 : DAST n -> DAST n

	public export
	data DCon : Nat -> Type where
		DConV : String -> DRCtx a 0 -> DAST a -> DCon a

	public export
	data DRCtx : Nat -> Nat -> Type where
		Nil : DRCtx Z n
		(::) : DAST n -> DRCtx l (S n) -> DRCtx (S l) n

Show (Fin n) where
	show = show . finToNat

Show (DAST n) where
	showPrec d (ʌ v) = show v
	showPrec d (λ at b) = showParens (d > Open) $ "λ" ++ showPrec Eq at ++ "=" ++ showPrec Open b
	showPrec d (λT at rt) = showParens (d > Open) $ "λ" ++ showPrec Eq at ++ ":" ++ showPrec Open rt
	showPrec d (f =!= a) = showParens (d >= App) $ showPrec Eq f ++ "!" ++ showPrec App a
	showPrec d 𝕋 = "Type"
	showPrec d (𝔽 at rt b) = showParens (d > Open) $ "𝔽" ++ showPrec Eq at ++ "=" ++ showPrec Open b
	showPrec d (𝕌 n t) = showParens (d > Open) $ "𝕌" ++ n ++ ":" ++ showPrec Open t
	showPrec d (ℂ (DConV n ats rt) as) = "ℂ" ++ n ++ "(" ++ (pack $ intercalate [',', ' '] $ toList $ map (unpack . showPrec Open) as) ++ ")"
	showPrec d (ℙ v (DConV n ats rt) t f) = "ℙ(" ++ showPrec Eq v ++ " of " ++ n ++ " then " ++ showPrec Eq t ++ " else " ++ showPrec Eq f ++ ")"
	showPrec d (𝔹 t) = "𝔹(" ++ showPrec Open t ++ ")"

mutual
	export Eq (DAST n) where
		(ʌ a) == (ʌ b) = a == b
		(λ aa ba) == (λ ab bb) = aa == ab && ba == bb
		(λT aa ra) == (λT ab rb) = aa == ab && ra == rb
		(fa =!= aa) == (fb =!= ab) = fa == fb && aa == ab
		𝕋 == 𝕋 = True
		(𝔽 aa ra fa) == (𝔽 ab rb fb) = aa == ab && ra == rb && fa == fb
		(𝕌 na ta) == (𝕌 nb tb) = na == nb && ta == tb
		(ℂ {a=aa} cna asa) == (ℂ {a=ab} cnb asb) = assert_total $ aa == ab && cna == believe_me cnb && asa == believe_me asb
		(ℙ {a=aa} va cna ta fa) == (ℙ {a=ab} vb cnb tb fb) = assert_total $ aa == ab && va == vb && cna == believe_me cnb && ta == believe_me tb && fa == fb
		(𝔹 ta) == (𝔹 tb) = ta == tb
		_ == _ = False

	export Eq (DCon a) where
		(DConV na atsa rta) == (DConV nb atsb rtb) = na == nb && atsa == atsb && rta == rtb

	export Eq (DRCtx l n) where
		Nil == Nil = True
		(ha :: ta) == (hb :: tb) = assert_total $ ha == hb && ta == tb
		_ == _ = False

total
export
dAppN : DAST n -> List (DAST n) -> DAST n
dAppN f [] = f
dAppN f (h :: t) = dAppN (f =!= h) t

total
export
dLamN : {a : Nat} -> {n : Nat} -> DRCtx a n -> DAST (a + n) -> DAST n
dLamN {a=Z} [] rt = rt
dLamN {a=S a} {n} (h :: t) rt = λ h $ dLamN t $ replace (plusSuccRightSucc a n) $ rt

ext: idr

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Logic

disjNot : Either (a -> Void) (b -> Void) -> (a, b) -> Void
disjNot (Left l)  (a, _) = l a
disjNot (Right r) (_, b) = r b

notEx : {p : a -> Type} -> ((x : a ** p x) -> Void) -> (y : a) -> p y -> Void
notEx ne y py = ne (y ** py)

nnnEl : (((a -> Void) -> Void) -> Void) -> (a -> Void)
nnnEl f x = f (\p => absurd $ p x)

nnnLe : (a -> Void) -> (((a -> Void) -> Void) -> Void)
nnnLe f g = g f

depCurr : {p : a -> Type} -> ((x : a ** p x) -> b) -> ((y : a) -> p y -> b)
depCurr f y x = f (y ** x)

depUncurr : {p : a -> Type} -> ((y : a) -> p y -> b) -> ((x : a ** p x) -> b)
depUncurr f (z ** q) = f z q

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Algebra.Solver.Monoid

import Algebra.Monoid
import Syntax.PreorderReasoning

%default total

public export
data Expr : (a : Type) -> Type where
  Var     : (x : a) -> Expr a
  Neutral : Expr a
  Append  : Expr a -> Expr a -> Expr a

public export
Semigroup (Expr a) where
  (<+>) = Append

public export
Monoid (Expr a) where
  neutral = Neutral

public export
eval : LMonoid a => Expr a -> a
eval (Var x)      = x
eval Neutral      = neutral
eval (Append x y) = eval x <+> eval y

--------------------------------------------------------------------------------
--          Sum
--------------------------------------------------------------------------------

public export
esum : LMonoid a => List a -> a
esum []       = neutral
esum (h :: t) = h <+> esum t

public export
normalize : Expr a -> List a
normalize (Var x)      = x :: []
normalize Neutral      = []
normalize (Append x y) = normalize x ++ normalize y

--------------------------------------------------------------------------------
--          Proofs
--------------------------------------------------------------------------------

0 psum :  LMonoid a
       => (xs,ys : List a)
       -> esum (xs ++ ys) === esum xs <+> esum ys
psum []        ys = sym appendLeftNeutral
psum (x :: xs) ys = Calc $
  |~ x <+> esum (xs ++ ys)
  ~~ x <+> (esum xs <+> esum ys) ... cong (x <+>) (psum xs ys)
  ~~ (x <+> esum xs) <+> esum ys ... appendAssociative

0 pnorm : LMonoid a => (e : Expr a) -> eval e === esum (normalize e)
pnorm (Var x)      = sym appendRightNeutral
pnorm Neutral      = Refl
pnorm (Append x y) = Calc $
  |~ eval x <+> eval y
  ~~ esum (normalize x) <+> eval y
     ... cong (<+> eval y) (pnorm x)
  ~~ esum (normalize x) <+> esum (normalize y)
     ... cong (esum (normalize x) <+>) (pnorm y)
  ~~ esum (normalize x ++ normalize y)
     ..< psum (normalize x) (normalize y)

--------------------------------------------------------------------------------
--          Solver
--------------------------------------------------------------------------------

export
0 solve :  LMonoid a
        => (e1,e2 : Expr a)
        -> (prf : normalize e1 === normalize e2)
        => eval e1 === eval e2
solve e1 e2 = Calc $
  |~ eval e1
  ~~ esum (normalize e1) ... pnorm e1
  ~~ esum (normalize e2) ... cong esum prf
  ~~ eval e2             ..< pnorm e2

--------------------------------------------------------------------------------
--          Example
--------------------------------------------------------------------------------

0 solverExample : {x,y,z : String}
                -> x ++ ((y ++ "") ++ z) === ("" ++ x) ++ (y ++ z)
solverExample =
  solve (Var x <+> ((Var y <+> Neutral) <+> Var z))
        ((Neutral <+> Var x) <+> (Var y <+> Var z))


text:
module Control.Permutation.Types

import Data.List
import Data.Vect
import Data.Fin
import Data.Group

%default total

infixr 7 :*

||| This is something like `Vector k a`, except we restrict ourselves to only 1,...,n for `Permutation n`.
public export
data Permutation : Nat -> Type where
  Nil : Permutation Z
  (:*) : Fin (S n) -> Permutation n -> Permutation (S n)

implementation Eq (Permutation n) where
  (==) Nil Nil = True
  (==) (x :* xs) (y :* ys) = x == y && xs == ys

private
id : {n : Nat} -> Permutation n
id {n=Z} = []
id {n=S _} = FZ :* id

export
debug : Permutation n -> String
debug Nil = "Nil"
debug (p:*ps) = show (finToNat p) ++ " :* " ++ (debug ps)

||| This is essentially a group action. Given a permutation, we apply it to a vector.
sigma : {n : Nat} -> Permutation n -> Vect n a -> Vect n a
sigma _ [] = []
sigma {n=S _} (p:*ps) (x::xs) = insert (sigma ps xs) p
  where
    insert : Vect n a -> Fin (S n) -> Vect (S n) a
    insert l FZ = x::l
    insert Data.Vect.Nil _ = [x]
    insert (e::es) (FS k) = e :: insert es k

export
toVector : {n : Nat} -> Permutation n -> Vect n (Fin n)
toVector {n} p = sigma p (sequential n)
  where
    sequential : (n : Nat) -> Vect n (Fin n)
    sequential Z = []
    sequential (S k) = FZ :: map FS (sequential k)

private
indices : {n : Nat} -> Permutation n -> Vect n (Fin n)
indices [] = Nil
indices (p :* ps) = p :: map (thin p) (indices ps)
  where
    thin : {n : Nat} -> Fin (S n) -> Fin n -> Fin (S n)
    thin FZ i = FS i
    thin _ FZ = FZ
    thin (FS i) (FS j) = FS (thin i j)

private
delete : {n : Nat} -> Fin (S n) -> Permutation (S n) -> Permutation n
delete FZ (j :* p) = p
delete {n=Z} (FS _)  _ = Nil
delete {n=S _} (FS i) (j :* p) = fromMaybe (lifter j) (strengthen j) :* delete i p
  where
    lifter : {n : Nat} -> Fin (S n) -> Fin n
    lifter {n=Z} _ = ?hole
    lifter {n=S _} (FS k) = k
    lifter {n=S _} FZ = FZ

private
compose : {n : Nat} -> Permutation n -> Permutation n -> Permutation n
compose Nil p = p
compose (i :* p) p' = index i (indices p') :* compose p (delete i p')

export
invert : {n : Nat} -> Permutation n -> Permutation n
invert Nil = Nil
invert p@(i :* is) = index (i' p) (indices p) :* delete (i' p) p
  where
    i' : Permutation n -> Fin n
    i' p = index i (indices p)

export
implementation {n : Nat} -> Semigroup (Permutation n) where
  (<+>) = compose

export
implementation {n : Nat} -> Monoid (Permutation n) where
  neutral = id

export
implementation {n : Nat} -> Group (Permutation n) where
  inverse = invert

max_stars_repo_name: vmchale/permutations

max_issues_repo_name: vmchale/permutation

max_forks_repo_name: vmchale/permutation


text:
module Compat
import Data.Vect
import Data.HVect
import Cam.FFI
import Cam.IO
import Cam.Data.Collections

%access export

public export
interface Mapping a b | a where
    toNative     : a -> b
    toForeign   : b -> a

implementation Mapping (Boxed Int) Int where
    toNative =  believe_me
    toForeign = believe_me

implementation Mapping (Boxed Double) Double where
    toNative =  believe_me
    toForeign = believe_me

implementation Mapping (Boxed Integer) Integer where
    toNative =  believe_me
    toForeign = believe_me

implementation Mapping (Boxed Unit) Unit where
    toNative =  believe_me
    toForeign = believe_me

implementation Mapping (Boxed Char) Char where
    toNative =  believe_me
    toForeign = believe_me

implementation Mapping (FList t) (List (Boxed t)) where
    toNative a = believe_me . unsafePerformIO $ fcall1 "flist_to_native" $ believe_me a
    toForeign b = believe_me . unsafePerformIO $ fcall1 "list_to_foreign" $ believe_me b

implementation Mapping (FVect n t) (Vect n (Boxed t)) where
    toNative {n} a = believe_me . unsafePerformIO $
                        let sig = Integer -> FVect n t -> FFI.IO Ptr in
                        let n = believe_me . the Integer $ fromNat n in
                        fcall2 "fvect_to_native" n $ believe_me a

    toForeign {n} b = believe_me . unsafePerformIO $
                        let sig = Integer -> Ptr -> FFI.IO  (FVect n t) in
                        let n = believe_me . the Integer $ fromNat n in
                        fcall2 "vect_to_foreign" n $ believe_me b

mapTypes : Vect n Type -> Vect n Type
mapTypes ts = map Boxed ts

implementation Mapping (FHVect xs) (HVect (mapTypes xs)) where
    toNative {xs} a = believe_me . unsafePerformIO $
                        let sig = Integer -> FHVect xs -> FFI.IO Ptr in
                        let n = believe_me . the Integer . fromNat $ size xs in
                        fcall2 "fhvect_to_native" n $ believe_me a
    toForeign {xs} b = believe_me . unsafePerformIO $
                        let sig = Integer -> Ptr -> FFI.IO  (FHVect xs) in
                        let n = believe_me . the Integer . fromNat $ size xs in
                        fcall2 "hvect_to_foreign" n $ believe_me b

implementation Mapping (Boxed String) String where
    toNative a = believe_me . unsafePerformIO $ fcall1 "fstr_to_native" $ believe_me a
    toForeign b = believe_me . unsafePerformIO $ fcall1 "str_to_foreign" $ believe_me b

implementation Show (FList t) where
    show = toNative . toText

implementation Show (FVect n t) where
    show = toNative . toText

implementation Show (FHVect xs) where
    show = toNative . toText

public export
data FModuleSpec : String -> Type where
  TheModule : (s : String) -> FModuleSpec s

||| foreign module
public export
FModule : String -> Type
FModule s = Boxed (FModuleSpec s)

%inline
camImport : FModuleSpec s -> FFI.IO (FModule s)
camImport {s} _ = believe_me $ fcall1 "get_module" $ believe_me s

%inline
camImportFrom : FModule mod_name -> String -> FFI.IO Unsafe
camImportFrom {mod_name} m str =
    let fieldname = believe_me $ the (Boxed String) $ toForeign str in
    fcall2 "module_property" (believe_me m) fieldname

%inline
unsafe : a -> Unsafe
unsafe a = unsafePerformIO $ fcall1 "identity" (believe_me a)

%inline
unsafeCall : Unsafe -> Unsafe -> FFI.IO Unsafe
unsafeCall f args = fcall2 "unsafe_call" f args

implicit iList2FList : List (Boxed a) -> FList a
iList2FList = toForeign

implicit iVect2FVect : Vect n (Boxed a) -> FVect n a
iVect2FVect = toForeign

implicit iHVect2FHVect : {xs1: Vect n Type} ->  HVect (map Boxed xs1) -> FHVect xs1
iHVect2FHVect = toForeign

implicit iString2Text : String -> Boxed String
iString2Text = toForeign

implicit iFList2List : FList a -> List (Boxed a)
iFList2List = toNative

implicit iFVect2Vect : FVect n a -> Vect n (Boxed a)
iFVect2Vect = toNative

implicit iFHVect2HVect : {xs1: Vect n Type} ->  FHVect xs1 -> HVect (map Boxed xs1)
iFHVect2HVect = toNative

implicit iText2String : Boxed String -> String
iText2String = toNative

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
%default total

identity_fn_applied_twice : (f : Bool -> Bool) -> ((x : Bool) -> f x = x) -> (b : Bool) -> f (f b) = b
identity_fn_applied_twice f g b = rewrite g b in g b

negation_fn_applied_twice : (f : Bool -> Bool) -> ((x : Bool) -> f x = not x) -> (b : Bool) -> f (f b) = b
negation_fn_applied_twice f g False = rewrite g (f False) in rewrite g False in Refl
negation_fn_applied_twice f g True = rewrite g (f True) in rewrite g True in Refl

andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
andb_eq_orb False False prf = Refl
andb_eq_orb False True Refl impossible
andb_eq_orb True False Refl impossible
andb_eq_orb True True prf = Refl

data Bin : Type where
    Z : Bin
    Odd : Bin -> Bin
    Even : Bin -> Bin

incr : Bin -> Bin
incr Z = Odd Z
incr (Odd x) = Even x
incr b@(Even x) = Odd b

binToNat : Bin -> Nat
binToNat Z = Z
binToNat (Odd x) = S (binToNat x)
binToNat (Even x) = S (S (binToNat x))

bin_to_nat_pres_incr : (b : Bin) -> binToNat $ incr b = S (binToNat b)
bin_to_nat_pres_incr Z = Refl
bin_to_nat_pres_incr (Odd x) = Refl
bin_to_nat_pres_incr (Even x) = Refl

natToBin : (n : Nat) -> Bin
natToBin Z = Z
natToBin (S k) = incr $ natToBin k

bin_to_nat_reverse_eq : (n : Nat) -> binToNat $ natToBin n = n
bin_to_nat_reverse_eq Z = Refl
bin_to_nat_reverse_eq (S k) =
    rewrite bin_to_nat_pres_incr (natToBin k) in
        rewrite bin_to_nat_reverse_eq k in
            Refl

nat_to_bin_reverse_eq : (b : Bin) -> natToBin $ binToNat b = b
nat_to_bin_reverse_eq Z = Refl
nat_to_bin_reverse_eq k = rewrite nat_to_bin_reverse_eq k in Refl


text:
module User

import Data.Config
import Data.Date
import Data.List
import Data.Promise
import Data.PullRequest
import Data.Review
import Data.String
import Data.User
import FFI.GitHub
import PullRequest
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
import Util

%default total

replicate' : Color -> Nat -> Char -> Doc AnsiStyle
replicate' c n char =
  annotate (color c) (pretty $ String.replicate n char)

namespace Reflect
  prCount : Fin 101
  prCount = 100

  reviewDetailsCount : Fin 101
  reviewDetailsCount = 25

  leftTitle : String
  leftTitle = "requested"

  rightTitle : String
  rightTitle = "authored"

  header : (leftPadding : Nat)
        -> Doc AnsiStyle
  header leftPadding =
    indent (cast leftPadding) $
      hsep [ital leftTitle, pretty " ", ital rightTitle]
    where
      ital : String -> Doc AnsiStyle
      ital = annotate italic . pretty

  intro : String
  intro = "Your current pull request summary (out of the past \{show prCount} PRs):"

  parameters (pageWidth : Nat, reviews : Nat, openReq : Nat, closedReq : Nat, closedAuth : Nat, openAuth : Nat)
    chart : (leftPadding : Nat)
         -> Doc AnsiStyle
    chart leftPadding =
      indent (cast leftPadding) $
             replicate' Green reviews '·'
         <+> replicate' Red  closedReq  '◦'
         <+> replicate' Yellow openReq    '<'
        <++> pretty "|"
        <++> replicate' Yellow openAuth   '>'
         <+> replicate' Green  closedAuth '·'

    graph : Doc AnsiStyle
    graph =
      let req      = openReq  + closedReq
          auth     = openAuth + closedAuth
          left     = (foldr max (length leftTitle ) [req + reviews, auth])
          right    = (foldr max (length rightTitle) [req, auth])
          full     = left + right + 3 -- center divider is 3 characters
          centerOffset : Double = ((cast pageWidth) / 2) - ((cast full) / 2)
          padTitle = (cast centerOffset) + (left `minus` (length leftTitle))
          padChart = (cast centerOffset) + (left `minus` (req + reviews))
      in  vsep [header padTitle, chart padChart]

    parameters (mostRecentReview : Maybe Date, earliestOpenAuth : Maybe Date, earliestOpenReq : Maybe Date)
      details : Doc AnsiStyle
      details =
        vsep [
          pretty intro
        , emptyDoc
        , annotate underline $ pretty "Requested Reviews:"
        , indent 2 . vsep $ catMaybes [
            Just $ pretty "unreviewed:"
          , Just $ indent 2 . vsep $ catMaybes [
              Just $ hsep [pretty "open:", annotate (color Yellow) $ pretty openReq]
            , earliestOpenReq <&> \date => indent 2 $ hsep [pretty "earliest:", pretty $ show date]
            , Just $ hsep [pretty "closed:", annotate (color Red) $ pretty closedReq]
            ]
          , Just $ hsep [pretty "reviews*:", annotate (color Green) $ pretty reviews]
          , mostRecentReview <&> \date => indent 2 $ hsep [pretty "most recent:", pretty $ show date]
          ]
        , emptyDoc
        , annotate underline $ pretty "Authored Pulls:"
        , indent 2 . vsep $ catMaybes [
            Just $ hsep [pretty "open:", annotate (color Yellow) $ pretty openAuth]
          , earliestOpenAuth <&> \date => indent 2 $ hsep [pretty "earliest:", pretty $ show date]
          , Just $ hsep [pretty "closed:", annotate (color Green) $ pretty closedAuth]
          ]
        , emptyDoc
        , annotate italic $ pretty "*review count (not PR count) of most recent \{show reviewDetailsCount} PRs."
        ]

      print : Doc AnsiStyle
      print = vsep [
                emptyDoc
              , graph
              , emptyDoc
              , details
              , emptyDoc
              ]

  export
  reflectOnSelf : Config => Octokit =>
                  Promise ()
  reflectOnSelf =
    do prs     <- listPartitionedPRs prCount {pageBreaks=4}
       myLogin <- login <$> getSelf
       reviews <- reviewsForUser myLogin (take (cast reviewDetailsCount) . reverse . sortBy (compare `on` createdAt) $ combined prs)
       let mostRecentReview = map submittedAt . head' $ sortBy (compare `on` submittedAt) reviews
       let history = tuple prs
       let (openAuthored, closedAuthored) =
         mapHom (filter ((== myLogin) . author)) history
       let (openRequested, closedRequested) =
         mapHom (filter (any (== myLogin) . reviewers)) history
       let (earliestOpenAuth, earliestOpenReq) =
         mapHom (head' . sort . map createdAt) (openAuthored, openRequested)
       -- TODO: get Terminal width from somewhere to set the page width
       --       to the min of the Terminal width or the intro length.
       putStrLn . renderString $
         print (length intro)
               (length reviews)
               (length openRequested)
               (length closedRequested)
               (length closedAuthored)
               (length openAuthored)
               mostRecentReview
               earliestOpenAuth
               earliestOpenReq

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
import Data.List

%default total

data WareAction = CreateNew | UpdateExist | RemoveExist | GetWareInfo

implementation Eq WareAction where
  (==) CreateNew   CreateNew   = True
  (==) UpdateExist UpdateExist = True
  (==) RemoveExist RemoveExist = True
  (==) GetWareInfo GetWareInfo = True
  (==) _           _           = False

implementation DecEq WareAction where
  decEq wa1 wa2 =
    case wa1 == wa2 of
      False => Yes theyEqual
      True  => No theyNotEqual
    where
      theyEqual : wa1 = wa2
      theyEqual = really_believe_me (Refl {x = wa1})
      theyNotEqual : wa1 = wa2 -> Void
      theyNotEqual prf = believe_me {b = Void} ()

record Ware where
  constructor MkWare
  name: String
  price: Double

data Role = SuperUser | Operator | Guest

roleToActions : Role -> List WareAction
roleToActions SuperUser = CreateNew :: UpdateExist :: RemoveExist :: GetWareInfo :: Nil
roleToActions Operator  = CreateNew :: UpdateExist :: GetWareInfo :: Nil
roleToActions Guest     = GetWareInfo :: Nil

record User where
  constructor MkUser
  firstName: String
  secondName: String
  role: Role

userActions : User -> List WareAction
userActions = roleToActions . role

checkUserRights: (user: User) -> (reqAction: WareAction) -> Bool
checkUserRights user reqAction =
  let
    userActions = roleToActions(role user)
  in
    any (\action => action == reqAction) userActions

ActionResult: Type
ActionResult = Either String Ware

createNewWare: (name: String) -> (price: Double) -> (user: User) -> ActionResult
createNewWare name price user = case checkUserRights user CreateNew of
  False => Left  ("Have no rights")
  True  => Right (MkWare name price)

HasAccess : (user: User) -> (action: WareAction) -> Type
HasAccess user action = Elem action (userActions user)

data ContainsAccess: User -> WareAction -> Type where
  Positive: (user: User) -> (action: WareAction) -> Elem action (userActions user) -> ContainsAccess user action

proveNegative : (contra : Elem req (userActions user) -> Void) -> ContainsAccess user req -> Void
proveNegative contra (Positive user req prf) = contra prf

proveContainsAccess: (user: User) -> (req: WareAction) -> Dec (ContainsAccess user req)
proveContainsAccess user req =
  case isElem req (userActions user) of
    (Yes prf) => Yes (Positive user req prf)
    (No contra) => No (proveNegative contra)

proveUserRights: (userActions: List WareAction) -> (req: WareAction) -> Dec(Elem req userActions)
proveUserRights userActions req = isElem req userActions

proveUserAccess: (user: User) -> (req: WareAction) -> Dec (HasAccess user req)
proveUserAccess user req = proveUserRights (roleToActions(role user)) req

createProved: (user: User) -> (prf: ContainsAccess user CreateNew) -> Ware
createProved user (Positive user CreateNew x) = ?createProved_rhs_1

testGuest: User
testGuest = MkUser "Test" "Guest" Guest

testSuperUser: User
testSuperUser = MkUser "Test" "SuperUser" SuperUser

guestCreatesWare: ActionResult
guestCreatesWare = createNewWare "Test Ware" 10.0 testGuest

superUserCreatesWare: ActionResult
superUserCreatesWare = createNewWare "Test Ware" 10.0 testSuperUser

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Language.LSP.Message.RegularExpressions

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#regExp
public export
record RegularExpressionsClientCapabilities where
  constructor MkRegularExpressionsClientCapabilities
  engine  : String
  version : Maybe String
%runElab deriveJSON defaultOpts `{{RegularExpressionsClientCapabilities}}


text:
module SizedStrings

import Data.Fin
import MaybeFin

%default total
%access public

||| A string with length encoded in the type
||| Need to investigate this PR:
||| https://github.com/idris-lang/Idris-dev/pull/2628
||| It may be that his work, if completed, would make this module obsolete!!
abstract data SizedString : Nat -> Type where
  SizedString' : (n : Nat) -> (s : String) -> SizedString n

%name SizedString str

||| This is the only was to create a SizedString
sizeString : (s : String) -> SizedString (length s)
sizeString s = SizedString' (length s) s

empty : SizedString Z
empty = sizeString ""

||| Length of the string, equal to the Nat carried in the type
length : SizedString n -> Nat
length {n} _ = n

length_is_embedded_in_type : (str : SizedString n) -> length str = n
length_is_embedded_in_type str = Refl

||| Typesafe way to get a character from a string at the specified index.
||| The order of arguments is patterned after Strings.strIndex, not, say, List.index.
||| Under the covers it does an assert_total call because the underlying
||| String.strIndex function is partial. However, we know this is safe as long
||| as SizedString is only created via the sizeString function from this module.
strIndex : SizedString n -> Fin n -> Char
strIndex (SizedString' _ s) x =
  assert_total $ strIndex s $ cast $ finToNat x

maybeStrIndex : SizedString n -> MaybeFin n -> Maybe Char
maybeStrIndex str NoFin = Nothing
maybeStrIndex str (SomeFin x) = Just $ strIndex str x

instance Cast (SizedString n) String where
  cast (SizedString' _ s) = s

replaceAt : Fin (S n) -> Char -> SizedString (S n) -> SizedString (S n)
replaceAt {n} i c (SizedString' _ str) =
  let charsBefore = finToNat i
      indexAfter = S charsBefore
      size = S n
      firstChunk = substr 0 charsBefore str
      secondChunk = substr indexAfter size str
  in SizedString' size $ firstChunk ++ (strCons c $ secondChunk)

maybeReplaceAt : MaybeFin n -> Char -> SizedString n -> SizedString n
maybeReplaceAt NoFin _ str = str
maybeReplaceAt (SomeFin x) c str = replaceAt x c str

(++) : SizedString n -> SizedString m -> SizedString (n + m)
(SizedString' _ str1) ++ (SizedString' _ str2) = SizedString' _ $ str1 ++ str2

private
splitAt : Nat -> SizedString n -> (String, String)
splitAt idx (SizedString' n str) =
  (substr 0 idx str, substr idx n str)

insertAfter : SizedString n -> (idx : MaybeFin n) -> SizedString m -> SizedString (n + m)
insertAfter str1 NoFin str2 = str1 ++ str2
insertAfter str (SomeFin x) (SizedString' _ infixStr) =
  let idx = S $ finToNat x
      splitStr = splitAt idx str
  in SizedString' _ $ (fst splitStr) ++ infixStr ++ (snd splitStr)

insertBefore : SizedString n -> (idx : MaybeFin n) -> SizedString m -> SizedString (m + n)
insertBefore str1 NoFin str2 = str2 ++ str1
insertBefore str (SomeFin x) (SizedString' _ infixStr) =
  let idx = finToNat x
      splitStr = splitAt idx str
  in SizedString' _ $ (fst splitStr) ++ infixStr ++ (snd splitStr)

deleteAt : MaybeFin n -> SizedString n -> SizedString (pred n)
deleteAt NoFin str = str
deleteAt (SomeFin x) (SizedString' (S k) str) =
  let idx = finToNat x
  in SizedString' k $ (substr 0 idx str) ++ (substr (S idx) (S k) str)


text:
module PPM

%default total

record Color : Type where
  C : (red, green, blue : Bits8) -> Color

data PPM : Nat -> Nat -> Type where
  MkPPM: (x, y: Nat) ->
         (image : Vect x (Vect y Color)) ->
         PPM x y

data VectZipper : Nat -> Nat -> Type -> Type where
  VZ : (left : Vect n a) -> (right : Vect m a) -> VectZipper n m a

toVect : VectZipper n m a -> Vect (n + m) a
toVect (VZ l r) = reverse l ++ r

goLeft : VectZipper (S n) m a -> VectZipper n (S m) a
goLeft (VZ (x :: l) r) = VZ l (x :: r)

goRight : VectZipper n (S m) a -> VectZipper (S n) m a
goRight (VZ l (x :: r)) = VZ (x :: l) r

zipper : Vect n a -> VectZipper 0 n a
zipper v = VZ [] v

instance Cast Bits8 Int where
  cast = prim__zextB8_Int

toString : PPM n m -> String
toString (MkPPM x y image) = header ++ concatMap {t=Vect x} row image
  where header : String
        header = concat (the (List String)
                             [ "P3\n"
                             , show x, " "
                             , show y, "\n"
                             ])
        component : Bits8 -> String
        component b = show (cast {to=Int} b)
        pixel : Color -> String
        pixel (C r g b) = component r ++ " " ++
                          component g ++ " " ++
                          component b ++ "\n"
        row : Vect n Color -> String
        row = concatMap pixel

max_stars_repo_name: david-christiansen/idris-raytracer

max_issues_repo_name: david-christiansen/idris-raytracer

max_forks_repo_name: david-christiansen/idris-raytracer


text:
module RandomTest

import Crypto.Random
import Crypto.Random.C
import Data.Vect
import Data.Fin
import Control.Monad.Error.Either

%default partial

b8_to_fin : Bits8 -> Fin 256
b8_to_fin b = case natToFin (cast b) 256 of Just x => x

incr : Vect 256 Bits32 -> Bits8 -> Vect 256 Bits32
incr vect byte = updateAt (b8_to_fin byte) (+1) vect

mean : (Cast a Double, Num a) => {n : Nat} -> Vect n a -> Double
mean vect = (sum $ map cast vect) / (cast n)

export
test_random : EitherT String IO ()
test_random = do
  let random_bytes_size = 262144.0
  data' <- random_bytes (cast random_bytes_size)
  let distribution = foldl incr (replicate _ 0) data'
  let delta_mean = abs (mean data' - 128)
  let True = delta_mean < 2
  | False => throwE "random generated bytes mean deviates too far from 128: \{show delta_mean}"

  let expected_mean = random_bytes_size / 256.0
  let delta_distri_mean = abs (mean distribution - expected_mean)
  let True = delta_distri_mean < 1.5
  | False => throwE "random generated bytes distribution mean deviates too far from \{show expected_mean}: \{show delta_mean}"

  pure ()


text:
module Printf

-- Based on https://strathprints.strath.ac.uk/68800/

import Data.Vect
import src.GenericArity

data Chunk : Type where
  IntC : Chunk
  RawC : Char -> Chunk

Format : Type
Format = List Chunk

size' : Format -> Nat
size' [] = 0
size' (IntC :: xs) = 1 + size' xs
size' ((RawC x) :: xs) = size' xs

parse : List Char -> Format
parse [] = []
parse ('%' :: 'd' :: xs) = IntC :: parse xs
parse (x :: xs) = RawC x :: parse xs

format : (fmt : Format) -> Types (size' fmt)
format [] = []
format (IntC :: fmt) = Int :: format fmt
format ((RawC _) :: fmt) = format fmt

assemble : (fmt : Format) -> Product (size' fmt) (format fmt) -> List String
assemble [] () = []
assemble (IntC :: fmt) (n, vs) = show n :: assemble fmt vs
assemble ((RawC c) :: fmt) vs = pack (the (List Char) [c])  :: assemble fmt vs

printf : (str : String) -> Arrows (size' (parse (unpack str))) (format (parse (unpack str))) String
printf str = let fmt = parse (unpack str) in curryn (size' fmt) (concat . assemble fmt)

lessThan : Int -> Int -> String
lessThan = printf "%d < %d"

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Main

import Data.Vect

append' : Vect n elem -> Vect m elem -> Vect (n+m) elem

tri : Vect 3 (Double, Double)
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

Position : Type
Position = (Double, Double)

quad : Vect 4 Position

Polygon : Nat -> Type
Polygon n = Vect n Position

quint : Polygon 5
quint = ?quint_rhs

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True  = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety nine"
getStringOrInt True  = 99

stringify : (isInt : Bool) -> StringOrInt isInt -> String
stringify False x = trim x
stringify True  x = cast x

valToString : (isInt : Bool) ->
              (
                case isInt of
                     True => Int
                     False => String
              ) ->
              String

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType =  (next : numType) -> AdderType k numType

adder : Num numType =>
        (numargs : Nat) -> numType -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

data Format = Character Format
            | Float Format
            | Number Format
            | Str Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Character fmt) = (c : Char) -> PrintfType fmt
PrintfType (Float fmt) = (d : Float) -> PrintfType fmt
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (s : String) -> PrintfType fmt
PrintfType (Lit _ fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Character fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Float fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'c' :: chars) = Character (toFormat chars)
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Float (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

Matrix : Num t => (n : Nat) -> (m : Nat) -> (t : Type) -> Type
Matrix n m t = Vect n (Vect m t)

testMatrix : Matrix 2 3 Double
testMatrix = [[0.0, 0.0, 0.0],
              [0.0, 0.0, 0.0]]

TupleVect : (n : Nat) -> (t : Type) -> Type
TupleVect Z t = ()
TupleVect (S k) t = (t, TupleVect k t)

Pair : (Nat, (Nat, ()))
-- (Nat, (Nat, ())) === (Nat, Nat, ())

testTupleVect : TupleVect 4 Nat
testTupleVect = (1,2,3,4,())

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Data.Colist

import Data.Maybe
import Data.List
import Data.List1
import public Data.Zippable

%default total

||| A possibly finite Stream.
public export
data Colist : (a : Type) -> Type where
  Nil : Colist a
  (::) : a -> Inf (Colist a) -> Colist a

--------------------------------------------------------------------------------
--          Creating Colists
--------------------------------------------------------------------------------

||| Convert a list to a `Colist`.
public export
fromList : List a -> Colist a
fromList []        = Nil
fromList (x :: xs) = x :: fromList xs

||| Convert a stream to a `Colist`.
public export
fromStream : Stream a -> Colist a
fromStream (x :: xs) = x :: fromStream xs

||| Create a `Colist` of only a single element.
public export
singleton : a -> Colist a
singleton a = a :: Nil

||| An infinite `Colist` of repetitions of the same element.
public export
repeat : a -> Colist a
repeat v = v :: repeat v

||| Create a `Colist` of `n` replications of the given element.
public export
replicate : Nat -> a -> Colist a
replicate 0     _ = Nil
replicate (S k) x = x :: replicate k x

||| Produce a `Colist` by repeating a sequence.
public export
cycle : List a -> Colist a
cycle Nil       = Nil
cycle (x :: xs) = run x xs
  where run : a -> List a -> Colist a
        run v []        = v :: run x xs
        run v (y :: ys) = v :: run y ys

||| Generate an infinite `Colist` by repeatedly applying a function.
public export
iterate : (a -> a) -> a -> Colist a
iterate f a = a :: iterate f (f a)

||| Generate a `Colist` by repeatedly applying a function.
||| This stops once the function returns `Nothing`.
public export
iterateMaybe : (f : a -> Maybe a) -> Maybe a -> Colist a
iterateMaybe _ Nothing  = Nil
iterateMaybe f (Just x) = x :: iterateMaybe f (f x)

||| Generate an `Colist` by repeatedly applying a function
||| to a seed value.
||| This stops once the function returns `Nothing`.
public export
unfold : (f : s -> Maybe (s,a)) -> s -> Colist a
unfold f s = case f s of
                  Just (s2,a) => a :: unfold f s2
                  Nothing     => Nil

--------------------------------------------------------------------------------
--          Basic Functions
--------------------------------------------------------------------------------

||| True, if this is the empty `Colist`.
public export
isNil : Colist a -> Bool
isNil [] = True
isNil _  = False

||| True, if the given `Colist` is non-empty.
public export
isCons : Colist a -> Bool
isCons [] = False
isCons _  = True

||| Concatenate two `Colist`s.
public export
append : Colist a -> Colist a -> Colist a
append []        ys = ys
append (x :: xs) ys = x :: append xs ys

||| Append a `Colist` to a `List`.
public export
lappend : List a -> Colist a -> Colist a
lappend xs = append (fromList xs)

||| Append a `List` to a `Colist`.
public export
appendl : Colist a -> List a -> Colist a
appendl xs = append xs . fromList

||| Try to extract the head and tail of a `Colist`.
public export
uncons : Colist a -> Maybe (a, Colist a)
uncons [] = Nothing
uncons (x :: xs) = Just (x, xs)

||| Try to extract the first element from a `Colist`.
public export
head : Colist a -> Maybe a
head []       = Nothing
head (x :: _) = Just x

||| Try to drop the first element from a `Colist`.
||| This returns `Nothing` if the given `Colist` is
||| empty.
public export
tail : Colist a -> Maybe (Colist a)
tail []        = Nothing
tail (_ :: xs) = Just xs

||| Take up to `n` elements from a `Colist`.
public export
take : (n : Nat) -> Colist a -> List a
take 0     _         = Nil
take (S k) []        = Nil
take (S k) (x :: xs) = x :: take k xs

||| Take elements from a `Colist` up to and including the
||| first element, for which `p` returns `True`.
public export
takeUntil : (p : a -> Bool) -> Colist a -> Colist a
takeUntil _ []        = Nil
takeUntil p (x :: xs) = if p x then [x] else x :: takeUntil p xs

||| Take elements from a `Colist` up to (but not including) the
||| first element, for which `p` returns `True`.
public export
takeBefore : (a -> Bool) -> Colist a -> Colist a
takeBefore _ []        = Nil
takeBefore p (x :: xs) = if p x then [] else x :: takeBefore p xs

||| Take elements from a `Colist` while the given predicate
||| returns `True`.
public export
takeWhile : (a -> Bool) -> Colist a -> Colist a
takeWhile p = takeBefore (not . p)

||| Extract all values wrapped in `Just` from the beginning
||| of a `Colist`. This stops, once the first `Nothing` is encountered.
public export
takeWhileJust : Colist (Maybe a) -> Colist a
takeWhileJust []              = []
takeWhileJust (Nothing :: _)  = []
takeWhileJust (Just x  :: xs) = x :: takeWhileJust xs

||| Drop up to `n` elements from the beginning of the `Colist`.
public export
drop : (n : Nat) -> Colist a -> Colist a
drop _ []            = Nil
drop 0           xs  = xs
drop (S k) (x :: xs) = drop k xs

||| Try to extract the `n`-th element from a `Colist`.
public export
index : (n : Nat) -> Colist a -> Maybe a
index _     []        = Nothing
index 0     (x :: _)  = Just x
index (S k) (_ :: xs) = index k xs

||| Produce a `Colist` of left folds of prefixes of the given `Colist`.
||| @ f the combining function
||| @ acc the initial value
||| @ xs the `Colist` to process
public export
scanl : (f : a -> b -> a) -> (acc : a) -> (xs : Colist b) -> Colist a
scanl _ acc Nil       = [acc]
scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs

--------------------------------------------------------------------------------
-- InBounds and inBounds for Colists
--------------------------------------------------------------------------------

||| Satisfiable if `k` is a valid index into `xs`
|||
||| @ k the potential index
||| @ xs the Colist into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : Colist a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : {0 xs : Inf (Colist a)} -> InBounds Z (x :: xs)
    ||| Valid indices can be extended
    InLater : {0 xs : Inf (Colist a)} -> InBounds k xs -> InBounds (S k) (x :: xs)

public export
Uninhabited (Data.Colist.InBounds k []) where
  uninhabited InFirst impossible
  uninhabited (InLater _) impossible

export
Uninhabited (Colist.InBounds k xs) => Uninhabited (Colist.InBounds (S k) (x::xs)) where
  uninhabited (InLater y) = uninhabited y

||| Decide whether `k` is a valid index into Colist `xs`
public export
inBounds : (k : Nat) -> (xs : Colist a) -> Dec (InBounds k xs)
inBounds k [] = No uninhabited
inBounds Z (x::xs) = Yes InFirst
inBounds (S k) (x::xs) = case inBounds k xs of
  Yes p => Yes $ InLater p
  No up => No $ \(InLater p) => up p

||| Find a particular element of a Colist using InBounds
|||
||| @ ok a proof that the index is within bounds
public export
index' : (k : Nat) -> (xs : Colist a) -> {auto 0 ok : InBounds k xs} -> a
index' Z (x::_) {ok = InFirst} = x
index' (S k) (_::xs) {ok = InLater _} = index' k xs

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

public export
Semigroup (Colist a) where
  (<+>) = append

public export
Monoid (Colist a) where
  neutral = Nil

public export
Functor Colist where
  map f []        = []
  map f (x :: xs) = f x :: map f xs

public export
Applicative Colist where
  pure = repeat

  [] <*> _  = []
  _  <*> [] = []
  f :: fs <*> a :: as = f a :: (fs <*> as)

public export
Zippable Colist where
  zipWith f as bs = [| f as bs |]

  zipWith3 f as bs cs = [| f as bs cs |]

  unzip xs = (map fst xs, map snd xs)

  unzip3 xs = ( map (\(a,_,_) => a) xs
              , map (\(_,b,_) => b) xs
              , map (\(_,_,c) => c) xs
              )

  unzipWith f = unzip . map f

  unzipWith3 f = unzip3 . map f


text:
module Data.Bytes.Lazy.IO

-- functions for reading/writing Bytes to and from files

-- Data.Bytes.Strict.IO should be safe and stable to depend on, though the
-- module might move over time. Conversely Data.Bytes.Lazy.IO is not a good
-- idea to depend on despite being the more useful API. It is being provided
-- for the purposes of developing this library and for people to prototype with
-- but it is lazy IO, and one of the lessons of Haskell is that while lazyness
-- is good, lazy io isn't. There's just no way to deal with IO errors in pure
-- code, and doing IO lazily will give you exactly that. Say we've read some
-- file into a lazy bytes and pass it along to our pure code. If the file is
-- closed before we start consuming the LBytes, we'll get a file error in a
-- place it can't be addressed/handled. We don't have an exception mechanism in
-- idris2 currently so this is slightly less of a problem than it is in haskell
-- but at the same time it'd be a real hassle to make every LBytes method end
-- with `Either Error a`. The ideal way to go is a streaming IO library that
-- provides our LBytes rather than lazy io because you can structure your
-- program around the streaming lib and have confidence about when issues will
-- crop up and where to handle them.

import Data.Bytes.Lazy
import Data.Bytes.Strict
import Data.Bytes.Util

import Data.Word.Word8

import System.File

-------------------------------------------------
-- primmmmmsssss
-------------------------------------------------

-- fGetChar grabs an `c unsigned char` and casts it to idris2 Char
-- Should really just have our own that casts to Word8
-- an fGetByte iow, idris2 just calls fgetc and so can we

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"

%foreign support "idris2_fileError"
prim_error' : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
prim_fileErrno' : PrimIO Int

%foreign support "fgetc"
prim__readChar' : FilePtr -> PrimIO Int

returnError : IO (Either FileError a)
returnError
    = do err <- primIO prim_fileErrno'
         case err of
              0 => pure $ Left FileReadError
              1 => pure $ Left FileWriteError
              2 => pure $ Left FileNotFound
              3 => pure $ Left PermissionDenied
              4 => pure $ Left FileExists
              _ => pure $ Left (GenericFileError (err-5))

fGetByte : (h : File) -> IO (Either FileError Word8)
fGetByte (FHandle h)
    = do c <- primIO (prim__readChar' h)
         ferr <- primIO (prim_error' h)
         if (ferr /= 0)
            then returnError
            else pure (Right (cast c))

-------------------------------------------------

-- read some number of file chacters, crash with msg on problem or eof, this is
-- to check if we're reading lazily.
-- If we eof crash then we read the whole file at once.
partial
readN : File -> Int -> IO (List Word8)
readN f n = if 0 >= n then pure []
                      else
                        do Right c <- fGetByte f
                             | Left err => idris_crash "readN Left"
                           False <- fEOF f
                             | True => pure []
                             -- If we're at fEOF then c was \NUL !
                           [| pure c :: readN f (n-1) |]

take : Nat -> LBytes -> LBytes
take Z lb = Empty
take (S k) Empty = Empty
take (S k) (Chunk b bs) = Chunk b (take k bs)

partial
fileTest : IO LBytes
fileTest = do Right f <- openFile "foo.txt" Read
                | Left err => idris_crash (show err)
              r <- make f []
              pure $ buildup f r
  where
    partial
    make : File -> List Word8 -> IO (Bytes, List Word8)
    make f rem
      = do rs@(_::_) <- readN f 32
             | [] => pure (empty,[])
           pure (packUpToNBytes 32 (rem ++ rs))
    partial
    buildup : File -> (Bytes, List Word8) -> LBytes
    buildup f (b,rem)
      = if null b then Empty
                  else Chunk b (buildup f (unsafePerformIO $ make f rem))
    -- ^ unsafePerformIO is so that we're not in IO, so we can do this creation
    -- lazily, don't do this yourself! Make or use a streaming IO lib. In the
    -- real world we desire predictable errors, thus our use of IO should be
    -- predictable, who knows where in our program our errrors are going to
    -- explode up now that we've lied and said `make` is pure.

printo : LBytes -> IO ()
printo lb = go 0 lb
  where
    go : Int -> LBytes -> IO ()
    go n Empty = putStrLn $ "End of lazy bytes. If you didn't get an eof"
      ++ "error\nthen we succeeded in reading only part of the file."
    go n (Chunk _ lbs) = do
      putStrLn $ "Chunk " ++ show n
      go (n + 1) lbs

export
partial
lazyIOTest : IO ()
lazyIOTest = do f <- fileTest
                putStrLn "Lazy Bytes test:"
                printo (take 2 f)
                putStrLn "Eat to eof test:"
                printo f -- This should eof crash.

-- super basic boys

readFile : (filename : String) -> IO (Either FileError LBytes)

writeFile : File -> (filename : String) -> LBytes -> IO (Maybe FileError)


text:
import DoesntExist

foo : Int
foo = 94


text:
> module SequentialDecisionProblems.applications.AvailableUnavailable

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

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

* Available / Unavailable emissions:

> data AvailableUnavailable = Available | Unavailable

* |AvailableUnavailable| is finite and non-empty:

> to : AvailableUnavailable -> Fin 2
> to Available  =    FZ
> to Unavailable = FS FZ

> from : Fin 2 -> AvailableUnavailable
> from             FZ   = Available
> from         (FS FZ)  = Unavailable
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : AvailableUnavailable) -> from (to a) = a
> fromTo Available  = Refl
> fromTo Unavailable = Refl

> |||
> finiteAvailableUnavailable : Finite AvailableUnavailable
> finiteAvailableUnavailable = MkSigma 2 (MkIso to from toFrom fromTo)

> |||
> cardNotZAvailableUnavailable : CardNotZ finiteAvailableUnavailable
> cardNotZAvailableUnavailable = cardNotZLemma finiteAvailableUnavailable Available

* |AvailableUnavailable| is in |DecEq|:

> availableNotUnavailable : Available = Unavailable -> Void
> availableNotUnavailable Refl impossible

> implementation [DecEqAvailableUnavailable] DecEq AvailableUnavailable where
>   decEq Available  Available    = Yes Refl
>   decEq Available  Unavailable  = No availableNotUnavailable
>   decEq Unavailable Available   = No (negEqSym availableNotUnavailable)
>   decEq Unavailable Unavailable = Yes Refl

* |AvailableUnavailable| is in |Eq|:

> implementation Eq AvailableUnavailable where
>   (==)   Available   Available = True
>   (==)   Available Unavailable = False
>   (==) Unavailable   Available = False
>   (==) Unavailable Unavailable = True

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Idris.Doc.String

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.TT

import Idris.Pretty
import Idris.Pretty.Render
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax

import TTImp.TTImp
import TTImp.Elab.Prim

import Data.List
import Data.List1
import Data.Maybe
import Data.Strings

import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.StringMap as S
import Libraries.Data.String.Extra

import Libraries.Control.ANSI.SGR
import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Util

import Parser.Lexer.Source

%default covering

public export
data IdrisDocAnn
  = TCon Name
  | DCon
  | Fun Name
  | Header
  | Declarations
  | Decl Name
  | DocStringBody
  | Syntax IdrisSyntax

export
styleAnn : IdrisDocAnn -> AnsiStyle
styleAnn (TCon _) = color BrightBlue
styleAnn DCon = color BrightRed
styleAnn (Fun _) = color BrightGreen
styleAnn Header = underline
styleAnn _ = []

export
tCon : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
tCon n = annotate (TCon n)

export
dCon : Doc IdrisDocAnn -> Doc IdrisDocAnn
dCon = annotate DCon

export
fun : Name -> Doc IdrisDocAnn -> Doc IdrisDocAnn
fun n = annotate (Fun n)

export
header : Doc IdrisDocAnn -> Doc IdrisDocAnn
header d = annotate Header d <+> colon

-- Add a doc string for a name in the current namespace
export
addDocString : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Name -> String ->
               Core ()
addDocString n_in doc
    = do n <- inCurrentNS n_in
         log "doc.record" 50 $
           "Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)"
         syn <- get Syn
         put Syn (record { docstrings $= addName n doc,
                           saveDocstrings $= insert n () } syn)

-- Add a doc string for a name, in an extended namespace (e.g. for
-- record getters)
export
addDocStringNS : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Namespace -> Name -> String ->
                 Core ()
addDocStringNS ns n_in doc
    = do n <- inCurrentNS n_in
         let n' = case n of
                       NS old root => NS (old <.> ns) root
                       root => NS ns root
         syn <- get Syn
         put Syn (record { docstrings $= addName n' doc,
                           saveDocstrings $= insert n' () } syn)

export
getDocsForPrimitive : {auto c : Ref Ctxt Defs} ->
                      {auto s : Ref Syn SyntaxInfo} ->
                      Constant -> Core (List String)
getDocsForPrimitive constant = do
    let (_, type) = checkPrim EmptyFC constant
    let typeString = show constant ++ " : " ++ show !(resugar [] type)
    pure [typeString ++ "\n\tPrimitive"]

prettyTerm : PTerm -> Doc IdrisDocAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm

export
getDocsForName : {auto o : Ref ROpts REPLOpts} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 FC -> Name -> Core (Doc IdrisDocAnn)
getDocsForName fc n
    = do syn <- get Syn
         defs <- get Ctxt
         let extra = case nameRoot n of
                       "-" => [NS numNS (UN "negate")]
                       _ => []
         resolved <- lookupCtxtName n (gamma defs)
         let all@(_ :: _) = extra ++ map fst resolved
             | _ => undefinedName fc n
         let ns@(_ :: _) = concatMap (\n => lookupName n (docstrings syn)) all
             | [] => pure $ pretty ("No documentation for " ++ show n)
         docs <- traverse showDoc ns
         pure $ vcat (punctuate Line docs)
  where

    -- Avoid generating too much whitespace by not returning a single empty line
    reflowDoc : String -> List (Doc IdrisDocAnn)
    reflowDoc "" = []
    reflowDoc str = map (indent 2 . reflow) (forget $ Extra.lines str)

    showTotal : Name -> Totality -> Doc IdrisDocAnn
    showTotal n tot
        = case isTerminating tot of
               Unchecked => ""
               _ => header "Totality" <++> pretty tot

    prettyName : Name -> Doc IdrisDocAnn
    prettyName n =
      let root = nameRoot n in
      if isOpName n then parens (pretty root) else pretty root

    getDConDoc : Name -> Core (Doc IdrisDocAnn)
    getDConDoc con
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact con (gamma defs)
                  -- should never happen, since we know that the DCon exists:
                  | Nothing => pure Empty
             syn <- get Syn
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             let conWithTypeDoc = annotate (Decl con) (hsep [dCon (prettyName con), colon, prettyTerm ty])
             let [(n, str)] = lookupName con (docstrings syn)
                  | _ => pure conWithTypeDoc
             pure $ vcat
               [ conWithTypeDoc
               , annotate DocStringBody $ vcat $ reflowDoc str
               ]

    getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
    getImplDoc n
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure []
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             pure [annotate (Decl n) $ prettyTerm ty]

    getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
    getMethDoc meth
        = do syn <- get Syn
             let [(n, str)] = lookupName meth.name (docstrings syn)
                  | _ => pure []
             ty <- pterm meth.type
             let nm = prettyName meth.name
             pure $ pure $ vcat [
               annotate (Decl meth.name) (hsep [fun (meth.name) nm, colon, prettyTerm ty])
               , annotate DocStringBody $ vcat (
                 toList (indent 2 . pretty . show <$> meth.totalReq)
                 ++ reflowDoc str)
               ]

    getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getInfixDoc n
        = do let Just (fixity, assoc) = S.lookupName n (infixes !(get Syn))
                    | Nothing => pure []
             pure $ pure $ hsep
                  [ pretty (show fixity)
                  , "operator,"
                  , "level"
                  , pretty (show assoc)
                  ]

    getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getPrefixDoc n
        = do let Just assoc = S.lookupName n (prefixes !(get Syn))
                    | Nothing => pure []
             pure $ ["prefix operator, level" <++> pretty (show assoc)]

    getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))
    getFixityDoc n =
      pure $ case toList !(getInfixDoc n) ++ toList !(getPrefixDoc n) of
        []  => []
        [f] => [header "Fixity Declaration" <++> f]
        fs  => [header "Fixity Declarations" <+> Line <+>
                 indent 2 (vcat fs)]

    getIFaceDoc : (Name, IFaceInfo) -> Core (Doc IdrisDocAnn)
    getIFaceDoc (n, iface)
        = do let params =
                case params iface of
                     [] => []
                     ps => [hsep (header "Parameters" :: punctuate comma (map (pretty . show) ps))]
             let constraints =
                case !(traverse pterm (parents iface)) of
                     [] => []
                     ps => [hsep (header "Constraints" :: punctuate comma (map (pretty . show) ps))]
             mdocs <- traverse getMethDoc (methods iface)
             let meths = case concat mdocs of
                           [] => []
                           docs => [vcat [header "Methods", annotate Declarations $ vcat $ map (indent 2) docs]]
             sd <- getSearchData fc False n
             idocs <- case hintGroups sd of
                           [] => pure (the (List (List (Doc IdrisDocAnn))) [])
                           ((_, tophs) :: _) => traverse getImplDoc tophs
             let insts = case concat idocs of
                           [] => []
                           [doc] => [header "Implementation" <++> annotate Declarations doc]
                           docs => [vcat [header "Implementations"
                                   , annotate Declarations $ vcat $ map (indent 2) docs]]
             pure (vcat (params ++ constraints ++ meths ++ insts))

    getFieldDoc : Name -> Core (Doc IdrisDocAnn)
    getFieldDoc nm
      = do syn <- get Syn
           defs <- get Ctxt
           Just def <- lookupCtxtExact nm (gamma defs)
                -- should never happen, since we know that the DCon exists:
                | Nothing => pure Empty
           ty <- resugar [] =<< normaliseHoles defs [] (type def)
           let prettyName = pretty (nameRoot nm)
           let projDecl = hsep [ fun nm prettyName, colon, prettyTerm ty ]
           let [(_, str)] = lookupName nm (docstrings syn)
                  | _ => pure projDecl
           pure $ annotate (Decl nm)
                $ vcat [ projDecl
                       , annotate DocStringBody $ vcat (reflowDoc str)
                       ]

    getFieldsDoc : Name -> Core (List (Doc IdrisDocAnn))
    getFieldsDoc recName
      = do let (Just ns, n) = displayName recName
               | _ => pure []
           let recNS = ns <.> mkNamespace n
           defs <- get Ctxt
           let fields = getFieldNames (gamma defs) recNS
           syn <- get Syn
           case fields of
             [] => pure []
             [proj] => pure [header "Projection" <++> annotate Declarations !(getFieldDoc proj)]
             projs => pure [vcat [header "Projections"
                                 , annotate Declarations $
                                      vcat $ map (indent 2) $ !(traverse getFieldDoc projs)]]

    getExtra : Name -> GlobalDef -> Core (List (Doc IdrisDocAnn))
    getExtra n d = do
      do syn <- get Syn
         let [] = lookupName n (ifaces syn)
             | [ifacedata] => pure <$> getIFaceDoc ifacedata
             | _ => pure [] -- shouldn't happen, we've resolved ambiguity by now
         case definition d of
           PMDef _ _ _ _ _ => pure [showTotal n (totality d)]
           TCon _ _ _ _ _ _ cons _ =>
             do let tot = [showTotal n (totality d)]
                cdocs <- traverse (getDConDoc <=< toFullNames) cons
                cdoc <- case cdocs of
                  [] => pure []
                  [doc] => pure
                         $ (header "Constructor" <++> annotate Declarations doc)
                         :: !(getFieldsDoc n)
                  docs => pure [vcat [header "Constructors"
                                     , annotate Declarations $
                                         vcat $ map (indent 2) docs]]
                pure (tot ++ cdoc)
           _ => pure []

    showCategory : GlobalDef -> Doc IdrisDocAnn -> Doc IdrisDocAnn
    showCategory d = case definition d of
      TCon _ _ _ _ _ _ _ _ => tCon (fullname d)
      DCon _ _ _ => dCon
      PMDef _ _ _ _ _ => fun (fullname d)
      ForeignDef _ _ => fun (fullname d)
      Builtin _ => fun (fullname d)
      _ => id

    showDoc : (Name, String) -> Core (Doc IdrisDocAnn)
    showDoc (n, str)
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => undefinedName fc n
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             let cat = showCategory def
             nm <- aliasName n
             let docDecl = annotate (Decl n) (hsep [cat (pretty (show nm)), colon, prettyTerm ty])
             let docText = reflowDoc str
             extra <- getExtra n def
             fixes <- getFixityDoc n
             let docBody = annotate DocStringBody $ vcat $ docText ++ (map (indent 2) (extra ++ fixes))
             pure (vcat [docDecl, docBody])

export
getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  PTerm -> Core (List String)
getDocsForPTerm (PRef fc name) = pure $ [!(render styleAnn !(getDocsForName fc name))]
getDocsForPTerm (PPrimVal _ constant) = getDocsForPrimitive constant
getDocsForPTerm (PType _) = pure ["Type : Type\n\tThe type of all types is Type. The type of Type is Type."]
getDocsForPTerm (PString _ _) = pure ["String Literal\n\tDesugars to a fromString call"]
getDocsForPTerm (PList _ _ _) = pure ["List Literal\n\tDesugars to (::) and Nil"]
getDocsForPTerm (PSnocList _ _ _) = pure ["SnocList Literal\n\tDesugars to (:<) and Empty"]
getDocsForPTerm (PPair _ _ _) = pure ["Pair Literal\n\tDesugars to MkPair or Pair"]
getDocsForPTerm (PDPair _ _ _ _ _) = pure ["Dependant Pair Literal\n\tDesugars to MkDPair or DPair"]
getDocsForPTerm (PUnit _) = pure ["Unit Literal\n\tDesugars to MkUnit or Unit"]
getDocsForPTerm pterm = pure ["Docs not implemented for " ++ show pterm ++ " yet"]

summarise : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Name -> Core String
summarise n -- n is fully qualified
    = do syn <- get Syn
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
             | _ => pure ""
         let doc = case lookupName n (docstrings syn) of
                        [(_, doc)] => case Extra.lines doc of
                                           ("" ::: _) => Nothing
                                           (d ::: _) => Just d
                        _ => Nothing
         ty <- normaliseHoles defs [] (type def)
         pure (nameRoot n ++ " : " ++ show !(resugar [] ty) ++
                  maybe "" ((++) "\n\t") doc)

-- Display all the exported names in the given namespace
export
getContents : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Namespace -> Core (List String)
getContents ns
   = -- Get all the names, filter by any that match the given namespace
     -- and are visible, then display with their type
     do defs <- get Ctxt
        ns <- allNames (gamma defs)
        let allNs = filter inNS ns
        allNs <- filterM (visible defs) allNs
        traverse summarise (sort allNs)
  where
    visible : Defs -> Name -> Core Bool
    visible defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (visibility def /= Private)

    inNS : Name -> Bool
    inNS (NS xns (UN _)) = ns `isParentOf` xns
    inNS _ = False

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Extra.String

import Data.Fin
import Data.Nat
import Data.String
import Data.String.Extra
import Data.Vect
import Extra.Binary
import Extra.Fin
import Extra.Proof

-- TODO: I have no idea how should I be implementing this
public export
data NonEmpty : StrM xs -> Type where
  IsNonEmpty : {x : Char} -> {xs : String} -> NonEmpty (StrCons x xs)

export
Uninhabited (NonEmpty StrNil) where
  uninhabited IsNonEmpty impossible

export
hexLower : Fin 16 -> Char
hexLower 0 = '0'
hexLower 1 = '1'
hexLower 2 = '2'
hexLower 3 = '3'
hexLower 4 = '4'
hexLower 5 = '5'
hexLower 6 = '6'
hexLower 7 = '7'
hexLower 8 = '8'
hexLower 9 = '9'
hexLower 10 = 'a'
hexLower 11 = 'b'
hexLower 12 = 'c'
hexLower 13 = 'd'
hexLower 14 = 'e'
hexLower 15 = 'f'

export
hexUpper : Fin 16 -> Char
hexUpper = toUpper . hexLower

||| Turn a `Bits8` into a pair of bytes in `Fin` representation
private
bits8ToBytesFin : Bits8 -> (Fin 16, Fin 16)
bits8ToBytesFin x = divmodFinNZ (bits8ToFin x) 16 SIsNotZ

private
bits8ToHexChars : Bits8 -> (Char, Char)
bits8ToHexChars = bimap hexUpper hexUpper . bits8ToBytesFin

||| Turn a foldable of Bits8 into a upper hex string without '0x' prefix
export
hexString : Foldable f => f Bits8 -> String
hexString = foldr (\x, str => let (a, b) = bits8ToHexChars x in strCons a $ strCons b $ str) ""

export
asciiString : Foldable f => f Bits8 -> String
asciiString = foldr (\x, str => strCons (chr $ cast x) str) ""

||| Turn a string (NO UTF8) into a list of Bits8 by casting the ordinals of the chars of the string
export
unpackVect : (str : String) -> Vect (length str) Char
unpackVect str = case toVect (length str) (unpack str) of
  Nothing => crash "Extra.String.unpackVect: impossible case"
  Just t => t


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

{-
  FFI for include/armv7a/am335x/beaglebone.h:
    https://github.com/mokshasoft/starterwarefree/blob/master/include/armv7a/am335x/beaglebone.h
-}

module StarterWareFree.Platform

%access public export
%default total
%include C "beaglebone.h"

GPIO1ModuleClkConfig : IO ()
GPIO1ModuleClkConfig =
    foreign FFI_C "GPIO1ModuleClkConfig" (IO ())

GPIO1Pin23PinMuxSetup : IO ()
GPIO1Pin23PinMuxSetup =
    foreign FFI_C "GPIO1Pin23PinMuxSetup" (IO ())

max_stars_repo_name: mokshasoft/starterwarefree-idris-ffi

max_issues_repo_name: mokshasoft/starterwarefree-idris-ffi

max_forks_repo_name: mokshasoft/starterwarefree-idris-ffi


text:
||| N-ary simple (non-dependent) functions using telescopes
|||
||| Compare with `base/Data.Fun` and `contrib/Data.Fun.Extra` and with:
||| Guillaume Allais. 2019. Generic level polymorphic n-ary functions. TyDe 2019.
module Data.Telescope.SimpleFun

import Data.Telescope.Telescope
import Data.Telescope.Segment

||| An n-ary function whose codomain does not depend on its
||| arguments. The arguments may have dependencies.
public export
0 SimpleFun : (env : Left.Environment gamma) -> {n : Nat} -> (0 delta : Segment n gamma)
           -> (cod : Type) -> Type
SimpleFun env {n = 0  } [] cod = cod
SimpleFun env {n = S n} (ty :: delta) cod = (x : ty env) -> SimpleFun (env ** x) delta cod

public export
target : {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma} -> {cod : Type}
      -> SimpleFun env delta cod -> Type
target {cod} _ = cod

public export
uncurry : {n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
       -> (f : SimpleFun env delta cod) -> Environment env delta -> cod
uncurry {n = Z}   {delta = []}     f xs        = f
uncurry {n = S n} {delta = _ :: _} f (x .= xs) = uncurry (f x) xs

public export
curry : {n : Nat} -> {0 env : Left.Environment gamma} -> {0 delta : Segment n gamma}
     -> (f : Environment env delta -> cod)
     -> SimpleFun env delta cod
curry {n = 0  } {delta = []         } f = f Empty
curry {n = S n} {delta = ty :: delta} f = \x => curry (\xs => f (x .= xs))


text:
module Client.Skeleton.BaseWithTest.Test.Test

import Fmt

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

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

import IdrTest.Test
import IdrTest.Expectation

import %s

export
suite : Test
suite =
  describe \"%s Tests\"
    [ test \"1 == 1\" (\\_ => assertEq 1 1 )
    ]
""" packageName packageName packageName

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import System
import System.Directory

panic : String -> IO a
panic s = do putStrLn s
             exitFailure

main : IO ()
main = do Right ["a"] <- listDir "dir"
            | Left e => panic (show e)
            | Right x => panic ("wrong entries: " ++ (show x))
          pure ()


text:
module Hedgehog.Internal.Shrink

import Data.Colist
import Data.Cotree
import Data.Nat

import Hedgehog.Internal.Util

%default total

public export
halvesInteger : Integer -> Colist Integer
halvesInteger = iterateBefore0 (`safeDiv` 2)

public export %inline
halves : ToInteger a => a -> Colist a
halves = map fromInteger . halvesInteger . toInteger

public export
towardsInteger : (destination, val : Integer) -> Colist Integer
towardsInteger dest x =
  if dest == x then []
               else let diff = (x `safeDiv` 2) - (dest `safeDiv` 2)
                     in dest `consNub` map (x -) (halvesInteger diff)

||| Shrink an integral number by edging towards a destination.
|||
||| >>> towards 0 100
||| [0,50,75,88,94,97,99]
|||
||| >>> towards 500 1000
||| [500,750,875,938,969,985,993,997,999]
|||
||| >>> towards (-50) (-26)
||| [-50,-38,-32,-29,-27]
|||
||| Note we always try the destination first, as that is the optimal shrink.
public export
towards : ToInteger a => (destination, val : a) -> Colist a
towards dest x = map fromInteger
               $ towardsInteger (toInteger dest) (toInteger x)

public export
towardsDouble : Double -> Double -> Colist Double
towardsDouble destination x =
  if destination == x
    then []
    else let diff = x - destination
             ok = (/= x)
          in takeWhile ok .  map (x -) $ iterate (/ 2) diff

public export
removes : Nat -> List a -> Colist $ List a
removes 0     _ = []
removes (S n) x = run (S n) [] x
  where run : Nat -> List a -> List a -> Colist $ List a
        run 0     _   []       = [[]]
        run 0     xs (y :: ys) = let rest = run n [y] ys
                                  in (y :: ys) :: map (prepRev xs) rest
        run (S k) _  []        = []
        run (S k) xs (y :: ys) = run k (y :: xs) ys

||| All ways a list can be split
|||
||| Note: The first list in the triple will be in reverse order
public export
splits : (a -> b) -> List a -> List (List a, b, List a)
splits _ []        = []
splits f (x :: xs) = run [] x xs
  where run : List a -> a -> List a -> List (List a, b, List a)
        run xs x []          = [(xs,f x,[])]
        run xs x l@(y :: ys) = (xs,f x,l) :: run (x::xs) y ys

||| Shrink a list by edging towards the empty list.
|||
||| >>> list [1,2,3]
||| [[],[2,3],[1,3],[1,2]]
|||
||| >>> list "abcd"
||| ["","cd","ab","bcd","acd","abd","abc"]
|||
||| Note we always try the empty list first, as that is the optimal shrink.
public export
list : (minLength : Nat) -> List a -> Colist $ List a
list ml xs = let diff = length xs `minus` ml
              in concatMapColist (`removes` xs) (halves diff)

public export
interleave : (minLength : Nat) -> List (Cotree a) -> Cotree (List a)
interleave ml ts = MkCotree (map value ts) $ dropThenShrink (list ml ts)
  where shrinkOne :  List (List (Cotree a), Coforest a, List (Cotree a))
                  -> Coforest (List a)
        shrinkOne []                      = []
        shrinkOne ((xs,[]   ,ys) :: rest) = shrinkOne rest
        shrinkOne ((xs,t::ts,ys) :: rest) = interleave ml (prepRev xs (t::ys)) ::
                                            shrinkOne ((xs,ts,ys) :: rest)

        dropThenShrink : Colist (List $ Cotree a) -> Coforest (List a)
        dropThenShrink []        = shrinkOne (splits (\t => t.forest) ts)
        dropThenShrink (x :: xs) = interleave ml x :: dropThenShrink xs

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

HalvesFrom10 : List Int
HalvesFrom10 = take 10 $ halves 10

halvesFrom10Test : HalvesFrom10 = [10,5,2,1]
halvesFrom10Test = Refl

Towards0_100 : List Int
Towards0_100 = take 10 $ towards 0 100

Towards500_1000 : List Int
Towards500_1000 = take 10 $ towards 500 1000

Towards50_26 : List Int
Towards50_26 = take 10 $ towards (-50) (-26)

towards0_100Test : Towards0_100 = [0,50,75,88,94,97,99]
towards0_100Test = Refl

towards500_1000Test : Towards500_1000 = [500,750,875,938,969,985,993,997,999]
towards500_1000Test = Refl

towards50_26Test : Towards50_26 = [-50,-38,-32,-29,-27]
towards50_26Test = Refl

TowardsFloat0_100 : List Double
TowardsFloat0_100 = take 7 $ towardsDouble 0.0 100

TowardsFloat1_5 : List Double
TowardsFloat1_5 = take 7 $ towardsDouble 1 0.5

towardsFloat0_100Test : TowardsFloat0_100 = [0.0,50.0,75.0,87.5,93.75,96.875,98.4375]
towardsFloat0_100Test = Refl

towardsFloat1_5Test : TowardsFloat1_5 = [1.0,0.75,0.625,0.5625,0.53125,0.515625,0.5078125]
towardsFloat1_5Test = Refl

Removes2_2 : List $ List Int
Removes2_2 = take 10 $ removes 2 [1,2]

removes2_2Test : Removes2_2 = [[]]
removes2_2Test = Refl

Removes2_3 : List $ List Int
Removes2_3 = take 10 $ removes 2 [1,2,3]

removes2_3Test : Removes2_3 = [[3]]
removes2_3Test = Refl

Removes2_4 : List $ List Int
Removes2_4 = take 10 $ removes 2 [1,2,3,4]

removes2_4Test : Removes2_4 = [[3,4],[1,2]]
removes2_4Test = Refl

Removes2_5 : List $ List Int
Removes2_5 = take 10 $ removes 2 [1,2,3,4,5]

removes2_5Test : Removes2_5 = [[3,4,5],[1,2,5]]
removes2_5Test = Refl

Removes2_6 : List $ List Int
Removes2_6 = take 10 $ removes 2 [1,2,3,4,5,6]

removes2_6Test : Removes2_6 = [[3,4,5,6],[1,2,5,6],[1,2,3,4]]
removes2_6Test = Refl

Removes3_10 : List $ List Int
Removes3_10 = take 10 $ removes 3 [1,2,3,4,5,6,7,8,9,10]

removes3_10Test : Removes3_10 = [[4,5,6,7,8,9,10],[1,2,3,7,8,9,10],[1,2,3,4,5,6,10]]
removes3_10Test = Refl

List3 : List $ List Int
List3 = take 10 $ list 0 [1,2,3]

List4 : List $ List Int
List4 = take 10 $ list 0 [1,2,3,4]

List5 : List $ List Int
List5 = take 10 $ list 2 [1,2,3,4,5]

list3Test : List3 = [[],[2,3],[1,3],[1,2]]
list3Test = Refl

list4Test : List4 = [[],[3,4],[1,2],[2,3,4],[1,3,4],[1,2,4],[1,2,3]]
list4Test = Refl

list5Test : List5 = [[4,5],[2,3,4,5],[1,3,4,5],[1,2,4,5],[1,2,3,5],[1,2,3,4]]
list5Test = Refl


text:
module System.File

import Data.Buffer

import public System.File.Buffer
import public System.File.Error
import public System.File.Handle
import public System.File.Meta
import public System.File.Mode
import public System.File.Permissions
import public System.File.Process
import public System.File.ReadWrite
import public System.File.Types
import public System.File.Virtual

||| Copy the file at the specified source to the given destination.
|||
||| @ src  the file to copy
||| @ dest the place to copy the file to
export
copyFile : HasIO io => (src : String) -> (dest : String) -> io (Either FileError ())
copyFile src dest
    = do Right buf <- createBufferFromFile src
             | Left err => pure (Left err)
         writeBufferToFile dest buf !(rawSize buf)