text:
module IntCasts

import IntNum

-- This file to be deleted once these interfaces are added to prelude

-- To String

export
Cast Int8 String where
  cast = prim__cast_Int8String

export
Cast Int16 String where
  cast = prim__cast_Int16String

export
Cast Int32 String where
  cast = prim__cast_Int32String

export
Cast Int64 String where
  cast = prim__cast_Int64String

-- To Integer

export
Cast Int8 Integer where
  cast = prim__cast_Int8Integer

export
Cast Int16 Integer where
  cast = prim__cast_Int16Integer

export
Cast Int32 Integer where
  cast = prim__cast_Int32Integer

export
Cast Int64 Integer where
  cast = prim__cast_Int64Integer

-- To Int

export
Cast Int8 Int where
  cast = prim__cast_Int8Int

export
Cast Int16 Int where
  cast = prim__cast_Int16Int

export
Cast Int32 Int where
  cast = prim__cast_Int32Int

export
Cast Int64 Int where
  cast = prim__cast_Int64Int

-- To Int8

export
Cast Int Int8 where
  cast = prim__cast_IntInt8

export
Cast Int16 Int8 where
  cast = prim__cast_Int16Int8

export
Cast Int32 Int8 where
  cast = prim__cast_Int32Int8

export
Cast Int64 Int8 where
  cast = prim__cast_Int64Int8

export
Cast Integer Int8 where
  cast = prim__cast_IntegerInt8

export
Cast Char Int8 where
  cast = prim__cast_CharInt8

export
Cast Double Int8 where
  cast = prim__cast_DoubleInt8

export
Cast String Int8 where
  cast = prim__cast_StringInt8

export
Cast Nat Int8 where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int8 where
  cast = prim__cast_Bits8Int8

export
Cast Bits16 Int8 where
  cast = prim__cast_Bits16Int8

export
Cast Bits32 Int8 where
  cast = prim__cast_Bits32Int8

export
Cast Bits64 Int8 where
  cast = prim__cast_Bits64Int8

-- To Int16

export
Cast Int Int16 where
  cast = prim__cast_IntInt16

export
Cast Int8 Int16 where
  cast = prim__cast_Int8Int16

export
Cast Int32 Int16 where
  cast = prim__cast_Int32Int16

export
Cast Int64 Int16 where
  cast = prim__cast_Int64Int16

export
Cast Integer Int16 where
  cast = prim__cast_IntegerInt16

export
Cast Char Int16 where
  cast = prim__cast_CharInt16

export
Cast Double Int16 where
  cast = prim__cast_DoubleInt16

export
Cast String Int16 where
  cast = prim__cast_StringInt16

export
Cast Nat Int16 where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int16 where
  cast = prim__cast_Bits8Int16

export
Cast Bits16 Int16 where
  cast = prim__cast_Bits16Int16

export
Cast Bits32 Int16 where
  cast = prim__cast_Bits32Int16

export
Cast Bits64 Int16 where
  cast = prim__cast_Bits64Int16

-- To Int32

export
Cast Int Int32 where
  cast = prim__cast_IntInt32

export
Cast Int8 Int32 where
  cast = prim__cast_Int8Int32

export
Cast Int16 Int32 where
  cast = prim__cast_Int16Int32

export
Cast Int64 Int32 where
  cast = prim__cast_Int64Int32

export
Cast Integer Int32 where
  cast = prim__cast_IntegerInt32

export
Cast Char Int32 where
  cast = prim__cast_CharInt32

export
Cast Double Int32 where
  cast = prim__cast_DoubleInt32

export
Cast String Int32 where
  cast = prim__cast_StringInt32

export
Cast Nat Int32 where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int32 where
  cast = prim__cast_Bits8Int32

export
Cast Bits16 Int32 where
  cast = prim__cast_Bits16Int32

export
Cast Bits32 Int32 where
  cast = prim__cast_Bits32Int32

export
Cast Bits64 Int32 where
  cast = prim__cast_Bits64Int32

-- To Int64

export
Cast Int Int64 where
  cast = prim__cast_IntInt64

export
Cast Int8 Int64 where
  cast = prim__cast_Int8Int64

export
Cast Int16 Int64 where
  cast = prim__cast_Int16Int64

export
Cast Int32 Int64 where
  cast = prim__cast_Int32Int64

export
Cast Integer Int64 where
  cast = prim__cast_IntegerInt64

export
Cast Char Int64 where
  cast = prim__cast_CharInt64

export
Cast Double Int64 where
  cast = prim__cast_DoubleInt64

export
Cast String Int64 where
  cast = prim__cast_StringInt64

export
Cast Nat Int64 where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int64 where
  cast = prim__cast_Bits8Int64

export
Cast Bits16 Int64 where
  cast = prim__cast_Bits16Int64

export
Cast Bits32 Int64 where
  cast = prim__cast_Bits32Int64

export
Cast Bits64 Int64 where
  cast = prim__cast_Bits64Int64

-- To Char

export
Cast Int8 Char where
  cast = prim__cast_Int8Char

export
Cast Int16 Char where
  cast = prim__cast_Int16Char

export
Cast Int32 Char where
  cast = prim__cast_Int32Char

export
Cast Int64 Char where
  cast = prim__cast_Int64Char

-- To Double

export
Cast Int8 Double where
  cast = prim__cast_Int8Double

export
Cast Int16 Double where
  cast = prim__cast_Int16Double

export
Cast Int32 Double where
  cast = prim__cast_Int32Double

export
Cast Int64 Double where
  cast = prim__cast_Int64Double

-- To Bits8

export
Cast Int8 Bits8 where
  cast = prim__cast_Int8Bits8

export
Cast Int16 Bits8 where
  cast = prim__cast_Int16Bits8

export
Cast Int32 Bits8 where
  cast = prim__cast_Int32Bits8

export
Cast Int64 Bits8 where
  cast = prim__cast_Int64Bits8

-- To Bits16

export
Cast Int8 Bits16 where
  cast = prim__cast_Int8Bits16

export
Cast Int16 Bits16 where
  cast = prim__cast_Int16Bits16

export
Cast Int32 Bits16 where
  cast = prim__cast_Int32Bits16

export
Cast Int64 Bits16 where
  cast = prim__cast_Int64Bits16

-- To Bits32

export
Cast Int8 Bits32 where
  cast = prim__cast_Int8Bits32

export
Cast Int16 Bits32 where
  cast = prim__cast_Int16Bits32

export
Cast Int32 Bits32 where
  cast = prim__cast_Int32Bits32

export
Cast Int64 Bits32 where
  cast = prim__cast_Int64Bits32

-- To Bits64

export
Cast Int8 Bits64 where
  cast = prim__cast_Int8Bits64

export
Cast Int16 Bits64 where
  cast = prim__cast_Int16Bits64

export
Cast Int32 Bits64 where
  cast = prim__cast_Int32Bits64

export
Cast Int64 Bits64 where
  cast = prim__cast_Int64Bits64

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

data EqNat : (n1 : Nat) -> (n2 : Nat) -> Type where
  Same : (n : Nat) -> EqNat n n

Show (EqNat n m) where
  show (Same n) = "Same " ++ show n

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

checkEqNat : (n1 : Nat) -> (n2 : Nat) -> Maybe (EqNat n1 n2)
checkEqNat Z Z = Just $ Same 0
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
  Nothing => Nothing
  Just eq => Just (sameS _ _ eq)

exactLength : (len : Nat) -> (input : Vect n a) -> Maybe (Vect len a)
exactLength {n} len input = case checkEqNat n len of
  Nothing => Nothing
  Just (Same len0) => Just input

checkEqNat2 : (n1 : Nat) -> (n2 : Nat) -> Maybe (n1 = n2)
checkEqNat2 Z Z = Just Refl
checkEqNat2 Z (S k) = Nothing
checkEqNat2 (S k) Z = Nothing
checkEqNat2 (S k) (S j) = map cong (checkEqNat2 k j)

sameCons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
sameCons prf = cong prf

sameList : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
sameList Refl prf2 = cong prf2

main : IO ()
main = do
  printLn $ Same 4
  printLn $ Same 5
  printLn $ the (EqNat 3 3) (Same _)
  printLn $ Same (2 + 2)
  printLn $ isJust $ exactLength 2 (0 :: 1 :: Nil)
  printLn $ isJust $ checkEqNat2 10 10
  printLn $ isNothing $ checkEqNat2 10 9

ext: idr

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module LightClick.DSL.AST

import Data.Vect

import Toolkit.Data.Location

import Language.SystemVerilog.Gates

import LightClick.Types.Direction
import LightClick.Types.Sensitivity
import LightClick.Types.WireType

%default total

public export
data AST : Type where
  Ref  : FileContext -> String -> AST
  Bind : FileContext -> String -> AST -> AST -> AST
  Seq  : AST -> AST -> AST

  DataLogic  : FileContext -> AST
  DataArray  : FileContext -> AST -> Nat -> AST
  DataStruct : {n : Nat} -> FileContext -> (kvs : Vect (S n) (Pair String AST)) -> AST
  DataUnion  : {n : Nat} -> FileContext -> (kvs : Vect (S n) (Pair String AST)) -> AST

  Port  : FileContext
       -> (label : String)
       -> (dir : Direction)
       -> (sense: Sensitivity)
       -> (wty : Wire)
       -> (type : AST)
       -> AST

  ModuleDef : {n : Nat} -> FileContext -> (kvs : Vect (S n) AST) -> AST

  Index  : FileContext -> AST -> String -> AST
  Connect : FileContext -> AST -> AST -> AST
  FanOut : {n : Nat} -> FileContext -> AST -> (ps : Vect (S (S n)) AST) -> AST
  Mux    : {n : Nat} -> FileContext -> (ps : Vect (S (S n)) AST) -> AST -> AST -> AST

  NOT  : FileContext -> AST -> AST -> AST
  GATE : {n : Nat} -> FileContext -> (ty : TyGateComb) -> (ps : Vect (S (S n)) AST) -> AST -> AST

  End : AST

mutual
  setKvsFS : String -> Vect n (Pair String AST) -> Vect n (Pair String AST)
  setKvsFS x [] = Nil
  setKvsFS x ((y, z) :: xs)
    = (y, setFileName x z) :: setKvsFS x xs

  setFSs : String -> Vect n AST -> Vect n AST
  setFSs x [] = []
  setFSs x (y :: xs) = (setFileName x y) :: setFSs x xs

  export
  setFileName : String -> AST -> AST
  setFileName fn (Ref x y)
    = Ref (setSource fn x) y

  setFileName fn (Bind x y z w)
    = Bind (setSource fn x) y (setFileName fn z) (setFileName fn w)

  setFileName fn (Seq x y)
    = Seq (setFileName fn x) (setFileName fn y)

  setFileName fn (DataLogic x)
    = DataLogic (setSource fn x)

  setFileName fn (DataArray x y k)
    = DataArray (setSource fn x) (setFileName fn y) k

  setFileName fn (DataStruct x kvs)
    = DataStruct (setSource fn x) (setKvsFS fn kvs)

  setFileName fn (DataUnion x kvs)
    = DataUnion (setSource fn x) (setKvsFS fn kvs)

  setFileName fn (Port x label dir sense wty type)
    = (Port (setSource fn x) label dir sense wty (setFileName fn type))

  setFileName fn (ModuleDef x kvs)
    = ModuleDef (setSource fn x) (setFSs fn kvs)

  setFileName fn (Index x y z)
    = Index (setSource fn x) (setFileName fn y) z

  setFileName fn (Connect x y z)
    = Connect (setSource fn x) (setFileName fn y) (setFileName fn z)

  setFileName fn (FanOut x y ps)
    = FanOut (setSource fn x) (setFileName fn y) (setFSs fn ps)

  setFileName fn (Mux x ps y z)
    = Mux (setSource fn x) (setFSs fn ps) (setFileName fn y) (setFileName fn z)

  setFileName fn (NOT x y z)
    = NOT (setSource fn x) (setFileName fn y) (setFileName fn z)

  setFileName fn (GATE x ty ps y)
    = GATE (setSource fn x) ty (setFSs fn ps) (setFileName fn y)
  setFileName fn End = End

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Compiler.Erlang.IR.ErlExpr

import public Data.Vect
import Control.Monad.State

%default total

public export
Line : Type
Line = Int

-- LOCAL VARIABLES

namespace LocalVars
  public export
  record LocalVar where
    constructor MkLocalVar
    varPrefix : String
    index : Int

  export
  Show LocalVar where
    show (MkLocalVar varPrefix index) = varPrefix ++ show index

  public export
  record LocalVars where
    constructor MkLocalVars
    varPrefix : String
    nextIndex : Int

  export
  initLocalVars : String -> LocalVars
  initLocalVars varPrefix = MkLocalVars varPrefix 0

  export
  newLocalVar : State LocalVars LocalVar
  newLocalVar = do
    MkLocalVars varPrefix nextIndex <- get
    put $ MkLocalVars varPrefix (nextIndex + 1)
    pure $ MkLocalVar varPrefix nextIndex

-- EXPRESSIONS

-- Notes:
-- * Erlang case expressions are represented using function expressions, because pattern variables
--   in case expressions can't be shadowed.
-- * Erlang let expressions are represented using function expressions, because let variables can't
--   be shadowed.
-- * EConstCase and EMatcherCase are restricted versions of Erlang case expressions.

public export
data IdrisConstant
  = IInt Int
  | IInteger Integer
  | IB8 Int
  | IB16 Int
  | IB32 Int
  | IB64 Integer
  | IString String
  | IChar Char
  | IDouble Double
  | IWorldVal
  | IIntType
  | IIntegerType
  | IBits8Type
  | IBits16Type
  | IBits32Type
  | IBits64Type
  | IStringType
  | ICharType
  | IDoubleType
  | IWorldType

mutual
  public export
  data ErlExpr : Type where
    ELocal : Line -> LocalVar -> ErlExpr
    ERef : Line -> (modName : ErlExpr) -> (fnName : ErlExpr) -> ErlExpr
    ELam : Line -> (args : List LocalVar) -> ErlExpr -> ErlExpr
    ELet : Line -> (newVar : LocalVar) -> (value : ErlExpr) -> (body : ErlExpr) -> ErlExpr
    ESequence : Line -> (statements : Vect (S k) ErlExpr) -> ErlExpr
    EApp : Line -> ErlExpr -> List ErlExpr -> ErlExpr
    EOp : Line -> (op : String) -> (lhs : ErlExpr) -> (rhs : ErlExpr) -> ErlExpr
    ECon : Line -> (name : String) -> List ErlExpr -> ErlExpr
    EConstCase : Line -> (sc : ErlExpr) -> List ErlConstAlt -> (def : ErlExpr) -> ErlExpr
    EMatcherCase : Line -> (sc : ErlExpr) -> List ErlMatcher -> (def : ErlExpr) -> ErlExpr
    EReceive : Line -> List ErlMatcher -> (timeout : ErlExpr) -> (def : ErlExpr) -> ErlExpr
    ETryCatch : Line -> (tryExpr : ErlExpr) -> (okVar : LocalVar) -> (okExpr : ErlExpr) -> (errorVar : LocalVar) -> (errorExpr : ErlExpr) -> ErlExpr
    EBinaryConcat : Line -> (bin1 : ErlExpr) -> (bin2 : ErlExpr) -> ErlExpr

    EIdrisConstant : Line -> IdrisConstant -> ErlExpr
    EAtom : Line -> String -> ErlExpr
    EChar : Line -> Char -> ErlExpr
    EFloat : Line -> Double -> ErlExpr
    EInteger : Line -> Integer -> ErlExpr
    ECharlist : Line -> String -> ErlExpr
    EBinary : Line -> String -> ErlExpr
    ENil : Line -> ErlExpr
    ECons : Line -> ErlExpr -> ErlExpr -> ErlExpr
    ETuple : Line -> List ErlExpr -> ErlExpr
    EMap : Line -> List (ErlExpr, ErlExpr) -> ErlExpr

    EBufferNew       : Line -> (size : ErlExpr) -> ErlExpr
    EBufferResize    : Line -> (bin : ErlExpr) -> (newSize : ErlExpr) -> ErlExpr
    EBufferFlatten   : Line -> (bin : ErlExpr) -> (maxbytes : ErlExpr) -> ErlExpr
    EBufferSetBits8  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetBits8  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetBits16 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetBits16 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetBits32 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetBits32 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetBits64 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetBits64 : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetInt32  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetInt32  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetInt64  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetInt64  : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetDouble : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetDouble : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> ErlExpr
    EBufferSetString : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (value : ErlExpr) -> ErlExpr
    EBufferGetString : Line -> (bin : ErlExpr) -> (loc : ErlExpr) -> (len : ErlExpr) -> ErlExpr

  public export
  data ErlConstAlt : Type where
    MkConstAlt : IdrisConstant -> ErlExpr -> ErlConstAlt

  public export
  data ErlMatcher : Type where
    MExact        : ErlExpr -> ErlMatcher
    MAny          : ErlMatcher
    MCodepoint    : ErlMatcher
    MInteger      : ErlMatcher
    MFloat        : ErlMatcher
    MAtom         : ErlMatcher
    MBinary       : ErlMatcher
    MMap          : ErlMatcher
    MPid          : ErlMatcher
    MRef          : ErlMatcher
    MPort         : ErlMatcher
    MAnyList      : ErlMatcher
    MNil          : ErlMatcher
    MCons         : ErlMatcher -> ErlMatcher -> (hdVar : LocalVar) -> (tlVar : LocalVar) -> ErlExpr -> ErlMatcher
    MList         : List (LocalVar, ErlMatcher) -> ErlExpr -> ErlMatcher
    MTuple        : List (LocalVar, ErlMatcher) -> ErlExpr -> ErlMatcher
    MTaggedTuple  : String -> List (LocalVar, ErlMatcher) -> ErlExpr -> ErlMatcher
    MMapSubset    : List (LocalVar, ErlExpr, ErlMatcher) -> ErlExpr -> ErlMatcher
    MFun          : (arity : Nat) -> ErlMatcher
    MTransform    : ErlMatcher -> (newVar : LocalVar) -> ErlExpr -> ErlMatcher
    MConst        : ErlMatcher -> ErlExpr -> ErlMatcher

public export
data ErlModuleName : Type where
  MkModuleName : Line -> (name : String) -> ErlModuleName

public export
data ErlAttribute : Type where
  NoAutoImport : Line -> ErlAttribute
  Inline       : Line -> ErlAttribute
  InlineSize   : Line -> Nat -> ErlAttribute

public export
data ErlVisibility = Private | Public

export
Eq ErlVisibility where
  Private == Private = True
  Public == Public = True
  _ == _ = False

public export
data ErlFunDecl : Type where
  MkFunDecl : Line -> (visibility : ErlVisibility) -> (name : String) -> (vars : List LocalVar) -> ErlExpr -> ErlFunDecl

public export
record ErlModule where
  constructor MkModule
  name : ErlModuleName
  attributes : List ErlAttribute
  funDecls : List ErlFunDecl


text:
module Maybe

%default total

maybeAdd : Maybe Int -> Maybe Int -> Maybe Int
maybeAdd x y = case x of
                    Nothing => Nothing
                    Just a => case y of
                                   Nothing => Nothing
                                   Just b => Just (a + b)

mAdd : Maybe Int -> Maybe Int -> Maybe Int
mAdd mx my = do x <- mx
                y <- my
                Just (x + y)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


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

import Effects
import Effect.Exception

%access public export

data SifError : Type where
  IndexOutOfBounds  : SifError
  NoSuchPattern     : SifError
  UnSuppFormat      : SifError
  ResultInvalid     : SifError
  NoSuchCommand     : SifError
  InternalErr       : SifError
  ImportError       : SifError
  NoFileGiven       : SifError
  NoModeSpecified   : SifError
  NoFormatSpecified : SifError
  FeatureNotImpl    : SifError
  ContextMismatch : SifError

  CannotWriteFile : String -> SifError
  NoSuchBackend   : String -> SifError
  IDMissing       : String -> SifError
  DuplicateID     : String -> SifError
  FileMissing     : String -> SifError
  ParseError      : String -> String -> SifError
  MismatchError   : String -> String -> SifError
  GeneralError    : String -> SifError

Show SifError where
  show IndexOutOfBounds  = "Index Out of Bounds"
  show NoSuchPattern     = "No Such Pattern"
  show UnSuppFormat      = "Unsupported output format"
  show ResultInvalid     = "Invalid evaluation result"
  show NoSuchCommand     = "No such command"
  show ImportError       = "Import Error"
  show NoFileGiven       = "No File Given"
  show NoModeSpecified   = "Node Mode Specified"
  show NoFormatSpecified = "No output format specified"
  show FeatureNotImpl    = "Feature Not Implemented"
  show InternalErr       = "Internal Error"
  show ContextMismatch   = "Solution Problem Context Mismatch"

  show (GeneralError m) = m

  show (CannotWriteFile f) = unwords ["Cannot write file:", show f]
  show (NoSuchBackend b)   = unwords ["No Such Backend:", show b]
  show (IDMissing id)      = unwords ["Identifier Missing:", show id]
  show (DuplicateID id)    = unwords ["Identifier already Exists:", show id]
  show (FileMissing fname) = unwords ["File Missing", show fname]

  show (ParseError fn err) =
      unlines [ unwords ["Error Parsing file", show fn, "error was:"]
              , err]

  show (MismatchError g e)  =
      unwords ["Given ID:", show g, "but got", show e, "instead."]

namespace Sif
  raise : SifError -> Eff b ['sif ::: EXCEPTION SifError]
  raise err = 'sif :- Exception.raise err

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
data SnocList ty = Empty | Snoc (Main.SnocList ty) ty

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


text:
module Hezarfen.Simplify

import Hezarfen.Prover
import Language.Reflection.Utils
import Language.Reflection.Elab

%access public export

||| subst n u t = t [u/n]
||| Different from `alphaRaw` in Pruviloj in the sense that we can replace
||| names with terms here, not just names with names.
subst : (n : TTName) -> (u : Raw) -> (t : Raw) -> Elab Raw
subst n u (Var n') = pure $ if n == n' then u else Var n'
subst n u (RBind n' b t) =
  if n == n'
    then RBind n' <$> sequence (map (subst n u) b) <*> pure t
    else do fr <- fresh
            t' <- subst n' (Var fr) t
            RBind fr <$> sequence (map (subst n u) b)
                     <*> subst n u t'
subst n u (RApp t1 t2) = RApp <$> subst n u t1 <*> subst n u t2
subst n u t = pure t

||| Check if `n` occurs in `t` freely.
isBound : (n : TTName) -> (t : Raw) -> Bool
isBound n (Var n') = n == n'
isBound n (RBind n' b t) =
  let isInB = or (map (Delay . isBound n) b) in
  if n == n' then isInB else (isBound n t || isInB)
isBound n (RApp t1 t2) = (isBound n t1) || (isBound n t2)
isBound n t = False

||| Count how many times `n` occurs in `t` freely.
countOccurrences : (n : TTName) -> (t : Raw) -> Nat
countOccurrences n (Var n') = if n == n' then 1 else 0
countOccurrences n (RBind n' b t) =
  let countInB = sum (map (countOccurrences n) b) in
  if n == n' then countInB else (countOccurrences n t + countInB)
countOccurrences n (RApp t1 t2) = countOccurrences n t1 + countOccurrences n t2
countOccurrences _ _ = 0

reduce : Raw -> Elab Raw
reduce t = case t of
  -- Eta reduction
  -- (\x => f x) becomes f
  RBind n (Lam b) (RApp t' (Var n')) =>
    if n == n'
      then reduce t'
      else pure $ RBind n (Lam b) !(reduce (RApp !(reduce t') (Var n')))

  -- ((\x => x) y) becomes y
  RApp (RBind n (Lam b) (Var n')) y =>
    if n == n'
    then reduce y
    else pure $ RApp (RBind n (Lam b) (Var n')) !(reduce y)

  -- (id x) becomes x
  RApp (RApp (Var `{id}) c) x => reduce x

  -- (id . f) becomes f
  RApp (RApp (RApp (RApp (RApp (Var `{(.)}) c) a) b) (RApp (Var `{id}) _)) f => reduce f

  -- (f . id) becomes f
  RApp (RApp (RApp (RApp (RApp (Var `{(.)}) c) a) b) f) (RApp (Var `{id}) _) => reduce f

  -- (\x => x) becomes id
  RBind n (Lam b) (Var n') =>
    if n == n'
    then reduce (RApp (Var `{id}) b)
    else pure t

  -- (\x => g (f x)) becomes (g . f)
  -- This is a bit problematic because composition takes the types
  -- as implicit arguments, however we don't have the types here.
  -- It works for now if we erase the types in the composition.
  -- We might need to test this more.
  RBind n (Lam b) (RApp g (RApp f (Var n'))) => do
    g' <- reduce g
    f' <- reduce f
    if n == n' && not (n `isBound` g) && not (n `isBound` f)
      then pure `((.) {c = ~idk} {a = ~b} {b = ~idk} ~g' ~f')
      else pure $ RBind n (Lam b) (RApp g' (RApp f' (Var n')))

  -- (let x = t in x) becomes t
  RBind n (Let ty v) (Var n') =>
    pure $ if n == n'
    then v
    else (Var n') -- let binding unused, so remove

  RBind n (Let ty v) t' => do
    t'' <- reduce t'
    case countOccurrences n t' of
      -- If a let binding isn't used, remove it.
      Z => pure t''
      -- If a let binding is only used once,
      -- remove the binding and replace the occurrence
      S Z => subst n v t''
      -- If it's used more than once, leave the binding
      _ => pure $ RBind n (Let ty v) t''

  RBind n b t' => pure $ RBind n b !(reduce t')
  RApp t1 t2 => pure $ RApp !(reduce t1) !(reduce t2)
  _ => pure t

untilFixpointM : (Monad m, Eq a) => (a -> m a) -> a -> m a
untilFixpointM f x =
  do x' <- f x ; if x == x' then pure x else untilFixpointM f x'

||| Not efficient, but works for now.
reduceLoop : Raw -> Elab Raw
reduceLoop = untilFixpointM reduce

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen


text:
module Expr

%default total

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs

eval : (Abs num, Neg num, Integral num) => Expr num -> num
eval (Val n) = n
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

e1 : Expr Int
e1 = Add (Val 6) (Mul (Val 3) (Val 12))


text:
module Naturality

import public TypesAndFunctions
import public Category
import public Isomorphism

%default total

public export
Naturality : {cat : Category} -> {a, b, x, y : Object cat} ->
  (f : Morphism cat a b) -> (g : Morphism cat y x) ->
  (preCompose {cat} {a=y} {b=x} {c=b} g) .
    (postCompose {cat} {a=x} {b=a} {c=b} f) =
  (postCompose {cat} {a=y} {b=a} {c=b} f) .
    (preCompose {cat} {a=y} {b=x} {c=a} g)
Naturality f g =
  functionalExtensionality (\h : Morphism cat x a => Associativity cat f h g)

public export
SubjectChange : {cat : Category} -> (subjectA, subjectB : Object cat) -> Type
SubjectChange {cat} subjectA subjectB =
  (observer : Object cat) ->
  Morphism cat observer subjectA -> Morphism cat observer subjectB

public export
ObserverChange : {cat : Category} -> (observerA, observerB : Object cat) -> Type
ObserverChange {cat} observerA observerB =
  (subject : Object cat) ->
  Morphism cat observerA subject -> Morphism cat observerB subject

public export
InvertibleSubjectChange : {cat : Category} ->
  (subjectA, subjectB : Object cat) -> Type
InvertibleSubjectChange subjectA subjectB =
  DPair (SubjectChange subjectA subjectB) IsBijectionForEach

public export
InvertibleObserverChange : {cat : Category} ->
  (observerA, observerB : Object cat) -> Type
InvertibleObserverChange observerA observerB =
  DPair (ObserverChange observerA observerB) IsBijectionForEach

public export
SubjectChangeIsNatural : {cat : Category} ->
  {subjectA, subjectB : Object cat} ->
  SubjectChange {cat} subjectA subjectB -> Type
SubjectChangeIsNatural {cat} alpha =
  (x, y : Object cat) -> (g : Morphism cat y x) ->
    alpha y . preCompose g = preCompose g . alpha x

public export
ObserverChangeIsNatural : {cat : Category} ->
  {observerA, observerB : Object cat} ->
  ObserverChange {cat} observerA observerB -> Type
ObserverChangeIsNatural {cat} beta =
  (x, y : Object cat) -> (g : Morphism cat x y) ->
    postCompose g . beta x = beta y . postCompose g

public export
SubjectChangeInducedMorphism : {cat : Category} ->
  {subjectA, subjectB : Object cat} ->
  (alpha : SubjectChange {cat} subjectA subjectB) ->
  Morphism cat subjectA subjectB
SubjectChangeInducedMorphism {subjectA} {subjectB} alpha =
  alpha subjectA (catId subjectA)

public export
SubjectChangeIsPostComposition : {cat : Category} ->
  {subjectA, subjectB : Object cat} ->
  (alpha : SubjectChange {cat} subjectA subjectB) ->
  (natural : SubjectChangeIsNatural {cat} {subjectA} {subjectB} alpha) ->
  (x : Object cat) -> alpha x =
    postCompose {cat} {a=x} {b=subjectA} {c=subjectB}
      (SubjectChangeInducedMorphism {cat} {subjectA} {subjectB} alpha)
SubjectChangeIsPostComposition {subjectA} {subjectB} alpha natural x =
  functionalExtensionality (\g =>
    replace
      {p=(\g' =>
        alpha x g' = After cat (alpha subjectA (Identity cat subjectA)) g)}
    (LeftIdentity cat g)
    (appEq {x=(catId subjectA)} (natural _ _ g)))

public export
ObserverChangeInducedMorphism : {cat : Category} ->
  {observerA, observerB : Object cat} ->
  (beta : ObserverChange {cat} observerA observerB) ->
  Morphism cat observerB observerA
ObserverChangeInducedMorphism {observerA} {observerB} beta =
  beta observerA (catId observerA)

public export
ObserverChangeIsPreComposition : {cat : Category} ->
  {observerA, observerB : Object cat} ->
  (beta : ObserverChange {cat} observerA observerB) ->
  (natural : ObserverChangeIsNatural {cat} {observerA} {observerB} beta) ->
  (y : Object cat) -> beta y =
    preCompose {cat} {a=observerB} {b=observerA} {c=y}
      (ObserverChangeInducedMorphism {cat} {observerA} {observerB} beta)
ObserverChangeIsPreComposition {observerA} {observerB} beta natural y =
  functionalExtensionality (\f =>
    replace
      {p=(\f' =>
        beta y f' = After cat f (beta observerA (Identity cat observerA)))}
    (RightIdentity cat f)
    (sym (appEq {x=(catId observerA)} (natural _ _ f))))

public export
NaturalBijectiveSubjectChangeInducesIsomorphism :
  {cat : Category} ->
  {subjectA, subjectB : Object cat} ->
  (alpha : SubjectChange {cat} subjectA subjectB) ->
  (natural : SubjectChangeIsNatural {cat} {subjectA} {subjectB} alpha) ->
  (bijective : IsBijectionForEach alpha) ->
  IsIsomorphism {cat} {a=subjectA} {b=subjectB}
    (SubjectChangeInducedMorphism {cat} {subjectA} {subjectB} alpha)
NaturalBijectiveSubjectChangeInducesIsomorphism
  {subjectA} {subjectB} alpha natural bijective =
    let
      bRight = snd (ForEachInverseIsInverse bijective subjectB) (catId subjectB)
    in
    ((fst (bijective subjectB) (Identity cat subjectB)) **
     (HasLeftInverseImpliesInjective
        {f=(alpha subjectA)} {g=(fst (bijective subjectA))}
        {x=(After cat
          (fst (bijective subjectB) (Identity cat subjectB))
          (alpha subjectA (Identity cat subjectA)))}
        {x'=(catId subjectA)}
        (fst (ForEachInverseIsInverse bijective subjectA))
        (trans
          (replace
            {p=
              (\g' =>
                alpha subjectA
                  (After cat
                     (fst (bijective subjectB) (Identity cat subjectB))
                       (alpha subjectA (Identity cat subjectA))) =
                     After cat g' (alpha subjectA (Identity cat subjectA)))}
                     bRight
                     (appEq
                       {x=(fst (bijective subjectB) (Identity cat subjectB))}
                       (natural _ _ (alpha _ (catId subjectA)))))
          (LeftIdentity cat (alpha subjectA (Identity cat subjectA)))),
      (trans
        (replace
          {p=
            (\g' =>
              After cat
                (alpha subjectA (Identity cat subjectA))
                   (fst (bijective subjectB) (Identity cat subjectB)) =
                      alpha subjectB g')}
           (LeftIdentity cat (fst (bijective subjectB) (Identity cat subjectB)))
           (sym
             (appEq {x=(catId subjectA)}
             (natural _ _ (fst (bijective subjectB) (catId subjectB))))))
        bRight)))

public export
NaturalBijectiveObserverChangeInducesIsomorphism :
  {cat : Category} ->
  {observerA, observerB : Object cat} ->
  (beta : ObserverChange {cat} observerA observerB) ->
  (natural : ObserverChangeIsNatural {cat} {observerA} {observerB} beta) ->
  (bijective : IsBijectionForEach beta) ->
  IsIsomorphism {cat} {a=observerB} {b=observerA}
    (ObserverChangeInducedMorphism {cat} {observerA} {observerB} beta)
NaturalBijectiveObserverChangeInducesIsomorphism
  {observerA} {observerB} beta natural bijective =
    let
      bRight =
        snd (ForEachInverseIsInverse bijective observerB) (catId observerB)
    in
    (fst (bijective observerB) (catId observerB) **
     (trans
       (replace
          {p=
            (\g' =>
              After cat
                (fst (bijective observerB) (Identity cat observerB))
                (beta observerA (Identity cat observerA)) =
              beta observerB g'
            )}
          (RightIdentity cat
            (fst (bijective observerB) (Identity cat observerB)))
          (appEq {x=(catId observerA)}
             (natural _ _ (fst (bijective observerB) (catId observerB))))
      ) bRight,
      HasLeftInverseImpliesInjective
        {f=(beta observerA)} {g=(fst (bijective observerA))}
        (fst (ForEachInverseIsInverse bijective observerA))
        (trans (sym (
           replace
             {p=(\g' =>
                   After cat (beta observerA (Identity cat observerA)) g' =
                   beta observerA (After cat
                     (beta observerA (Identity cat observerA))
                      (fst (bijective observerB) (Identity cat observerB))))}
             bRight
             (appEq {x=(fst (bijective observerB) (catId observerB))}
              (natural _ _ (beta _ (catId observerA))))
        )) (RightIdentity cat _))))

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
module Network.Curl.Types.CurlMOption

import Network.Curl.Types.Code
import Network.Curl.Types.OptType
import public Network.Curl.Types.Handle

import Data.Buffer

import Derive.Enum
%language ElabReflection

public export
data CurlMOption : OptType -> Type where
  CURLMOPT_SOCKETFUNCTION : CurlMOption CURLOPTTYPE_FUNCTIONPOINT -- 1
  CURLMOPT_SOCKETDATA : CurlMOption CURLOPTTYPE_OBJECTPOINT
  CURLMOPT_PIPELINING : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_TIMERFUNCTION : CurlMOption CURLOPTTYPE_FUNCTIONPOINT
  CURLMOPT_TIMERDATA : CurlMOption CURLOPTTYPE_OBJECTPOINT
  CURLMOPT_MAXCONNECTS : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_MAX_HOST_CONNECTIONS : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_MAX_PIPELINE_LENGTH : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_CONTENT_LENGTH_PENALTY_SIZE : CurlMOption CURLOPTTYPE_OFF_T
  CURLMOPT_CHUNK_LENGTH_PENALTY_SIZE : CurlMOption CURLOPTTYPE_OFF_T
  CURLMOPT_PIPELINING_SITE_BL : CurlMOption UnusedOptType
  CURLMOPT_PIPELINING_SERVER_BL : CurlMOption UnusedOptType
  CURLMOPT_MAX_TOTAL_CONNECTIONS : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_PUSHFUNCTION : CurlMOption CURLOPTTYPE_FUNCTIONPOINT
  CURLMOPT_PUSHDATA : CurlMOption CURLOPTTYPE_OBJECTPOINT
  CURLMOPT_MAX_CONCURRENT_STREAMS : CurlMOption CURLOPTTYPE_LONG
  CURLMOPT_LASTENTRY : CurlMOption UnusedOptType -- not used

curlMOptEnumList : List Int
curlMOptEnumList = [1..17]

[derivedToCode] ToCode (CurlMOption ty) where
  toCode = enumTo curlMOptEnumList

-- Automate toCode plussing with the power of named instances
public export
{ty : _} -> ToCode (CurlMOption ty) where
  toCode opt = toCode @{derivedToCode} opt + toCode ty

export
Show (CurlMOption ty) where
  show = showEnum

public export
data CurlPollInfo : Type where
  CURL_POLL_NONE : CurlPollInfo
  CURL_POLL_IN : CurlPollInfo
  CURL_POLL_OUT : CurlPollInfo
  CURL_POLL_INOUT : CurlPollInfo
  CURL_POLL_REMOVE : CurlPollInfo

export
ToCode CurlPollInfo where
  toCode = enumTo [0..4]

FromCode CurlPollInfo where
  fromCode = enumFrom [0..4]

export
Show CurlPollInfo where
  show = showEnum

export
Eq CurlPollInfo where
  (==) = eqEnum

export
Ord CurlPollInfo where
  compare = compareEnum

public export
total
paramType : {ty : _} -> CurlMOption ty -> Type
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLMOPT_SOCKETFUNCTION
  = Ptr HandlePtr -> (socket : Int) -> (pollinfo : Int) ->
    (socketdata : AnyPtr) -> (multi_assign : AnyPtr) -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLMOPT_TIMERFUNCTION
  = Ptr HandlePtr -> (timeout_ms : Int) -> AnyPtr -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLMOPT_PUSHFUNCTION
  = (parent : Ptr HandlePtr) -> (easy : Ptr HandlePtr) -> (num_headers : Int) ->
    (pushheaders_struct : AnyPtr) -> (userp : AnyPtr) -> PrimIO Int
paramType opt = optType ty


text:
-- Local Variables:
-- idris-load-packages: ("prelude" "effects" "contrib" "base")
-- End:

import Data.Vect
import Effects
import Effect.State

-- Here we're going to include some algorithms related to Huth and Ryan's book, for practice

data Formula = Atom String | Disj Formula Formula | Conj Formula Formula
             | Imp Formula Formula | Neg Formula

-- we could do a CNF conversion to a different type but I'd also like to try seeing if
-- I can do a thing of converting to the same type and actually proving that it won't
-- produce terms outside the subset

noImp : Formula -> Formula
noImp (Atom x) = (Atom x)
noImp (Disj x y) = Disj (noImp x) (noImp y)
noImp (Conj x y) = Conj (noImp x) (noImp y)
noImp (Imp x y) = Disj (Neg x) y
noImp (Neg x) = Neg (noImp x)

-- now how do we state our property? Maybe something like

noImpCorrect : (f : Formula) -> (g : Formula) -> (h : Formula) -> (Imp g h) = (noImp f) -> Void
noImpCorrect (Atom _) _ _ Refl impossible
noImpCorrect (Disj _ _) _ _ Refl impossible
noImpCorrect (Conj _ _) _ _ Refl impossible
noImpCorrect (Imp _ _) _ _ Refl impossible
noImpCorrect (Neg _) _ _ Refl impossible

data Lit = PosAtom String | NegAtom String -- yes this is really just an either type

negLit : Lit -> Lit
negLit (PosAtom x) = NegAtom x
negLit (NegAtom x) = PosAtom x

instance Eq Lit where
  (PosAtom x) == (PosAtom y) = x == y
  (NegAtom x) == (NegAtom y) = x == y
  x == y = False

CNF : Type
CNF = List (List Lit) -- the outer ones are conjunctions the inner lists are disjunctions

aux : List Lit -> Bool
aux [] = True
aux (x :: xs) = (elem (negLit x) xs) || (aux xs)

-- Okay I'm really confused why it can't figure out the type instance if I put cnf instead of List (List Lit).
cnfValid : CNF -> Bool
cnfValid c = all aux c

data ImpFree = IConj ImpFree ImpFree | IDisj ImpFree ImpFree | INeg ImpFree
             | IAtom String

impFree : Formula -> ImpFree
impFree (Atom x) = (IAtom x)
impFree (Disj x y) = IDisj (impFree x) (impFree y)
impFree (Conj x y) = IConj (impFree x) (impFree y)
impFree (Imp x y) = IDisj (INeg (impFree x)) (impFree y)
impFree (Neg x) = INeg (impFree x)

data NNF = NConj NNF NNF | NDisj NNF NNF | NLit Lit

toNNF : ImpFree -> NNF
toNNF (IConj x y) = NConj (toNNF x) (toNNF y)
toNNF (IDisj x y) = NDisj (toNNF x) (toNNF y)
toNNF (INeg (IConj x y)) = NDisj (toNNF arg1)
                                 (toNNF arg2)
    where arg1 = assert_smaller (INeg (IConj x y)) (INeg x)
          arg2 = assert_smaller (INeg (IConj x y)) (INeg y)

toNNF (INeg (IDisj x y)) = NConj (toNNF (assert_smaller (INeg (IDisj x y)) (INeg x)))
                                  (toNNF (assert_smaller (INeg (IDisj x y)) (INeg y)))
toNNF (INeg (INeg x)) = toNNF x
toNNF (INeg (IAtom x)) = NLit (NegAtom x)
toNNF (IAtom x) = NLit (PosAtom x)

accumLits : NNF -> List Lit
accumLits (NConj x y) = accumLits x ++ accumLits y -- this case won't happen in disjLift
accumLits (NDisj x y) = accumLits x ++ accumLits y
accumLits (NLit x) = [x]

disjLift : (x : NNF) -> (y : NNF) -> List (List Lit)
disjLift (NConj x1 x2) y = (disjLift x1 y) ++ (disjLift x2 y)
disjLift x (NConj y1 y2) = (disjLift x y1) ++ (disjLift x y2)
disjLift x y = [(accumLits x) ++ (accumLits y)]

nnfTocnf : NNF -> CNF
nnfTocnf (NConj x y) = nnfTocnf x ++ nnfTocnf y
nnfTocnf (NDisj x y) = disjLift x y
nnfTocnf (NLit x) = [[x]]

isValid : Formula -> Bool
isValid = cnfValid . nnfTocnf . toNNF . impFree

-- okay then!

{-
  Now let's get to horn clauses. These are going to be built up inductively as
-}

data P = PBot | PTop | PLit Lit

data Clause p = CImp (List p) p

Horn : Type -> Type
Horn p = List (Clause p)

blah : Clause P -> List P
blah (CImp xs x) = xs ++ [x]

collectPs : Horn P -> List P
collectPs = concat . map blah

data IsMarked = Marked P | Unmarked P

satHorn : Horn (Fin n) -> Vect n IsMarked -> Bool
satHorn h v = ?rhs

{-
  Now the problem here is that the Huth and Ryan algorithm for this is a while loop that translates rather uglily from an imperative language to a functional one.

  Now, we could do a translation of the loop with just recursion, yes
-}

markTop : IsMarked -> IsMarked
markTop (Marked x) = (Marked x)
markTop a@(Unmarked PBot) = a
markTop (Unmarked PTop) = Marked PTop
markTop a@(Unmarked (PLit x)) = a

isDone : Horn (Fin n) -> Bool
isDone h = ?fdas

notBot : IsMarked -> Bool
notBot m = ?asdf

uglySatAux : (h : List (Clause (Fin n))) ->  Vect n IsMarked -> Bool
uglySatAux h vs = if (isDone h) then (and (map notBot vs)) else ?blee

uglySat : Horn (Fin n) -> Vect n IsMarked -> Bool
uglySat h v = uglySatAux h (map markTop v)

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


text:
import Data.List.Views
import Data.Vect
import Data.Vect.Views
import Data.Nat.Views

total equalSuffixHelper: Eq a => List a -> List a -> List a
equalSuffixHelper input1 input2 with (snocList input1)
  equalSuffixHelper [] input2          | Empty = []
  equalSuffixHelper (xs ++ [x]) input2 | (Snoc xs_rec) with (snocList input2)
    equalSuffixHelper (xs ++ [x]) []          | (Snoc xs_rec) | Empty      = []
    equalSuffixHelper (xs ++ [x]) (ys ++ [y]) | (Snoc xs_rec) | (Snoc ys_rec) =
      if x == y
      then x :: (equalSuffixHelper xs ys | xs_rec | ys_rec)
      else []

total equalSuffix: Eq a => List a -> List a -> List a
equalSuffix xs ys = reverse (equalSuffixHelper xs ys)

total mergeSort: Ord a => Vect n a -> Vect n a
mergeSort input with (splitRec input)
  mergeSort []  | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) =
    merge (mergeSort lefts  | lrec)
          (mergeSort rights | rrec)

total toBinary: Nat -> String
toBinary input with (halfRec input)
  toBinary Z           | HalfRecZ          = ""
  toBinary (n + n)     | (HalfRecEven rec) = (toBinary n | rec) ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec)  = (toBinary n | rec) ++ "1"

total palindrome: Eq a => List a -> Bool
palindrome input with (vList input)
  palindrome []  | VNil = True
  palindrome [x] | VOne = True
  palindrome (first :: (mid ++ [last])) | (VCons rec) =
    if first == last
    then palindrome mid | rec
    else False

list : List Int
list = [1..5]

test1 : List Int
test1 = [1,2,4,5]

vect1 : Vect 10 Integer
vect1 = [1,2,3,4,5,6,7,8,9,0]

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module FuncImpl

public export
interface Monad m => FooBar m where
  Foo    : {A : Type} -> A -> m A -> Type
  bar    : {A : Type} -> (ma : m A) -> m (DPair A (\ a => Foo a ma))
  foobar : {A : Type} -> (ma : m A) -> map DPair.fst (bar ma) = ma


text:
import Data.List.Views

list1: List Int
list1 = [1,2,3]

data ListLast: List a -> Type where
  Empty: ListLast []
  NonEmpty: (xs: List a) -> (x: a) -> ListLast (xs ++ [x])

total listLast: (xs: List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
  Empty => NonEmpty [] x
  (NonEmpty ys y) => NonEmpty (x :: ys) y

total describeHelper: (input: List Int) -> (form: ListLast input) -> String
describeHelper []          Empty           = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x) = "NonEmpty - All but one: " ++ show xs

total describeListEnd: List Int -> String
describeListEnd xs with (listLast xs)
  describeListEnd []          | Empty           = "Empty!"
  describeListEnd (ys ++ [x]) | (NonEmpty ys x) = "Non-empty :) All but last: " ++ show ys

myReverse: List a -> List a
myReverse input with (listLast input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs

data SplitList: List a -> Type where
  SplitNil:  SplitList []
  SplitOne:  SplitList [x]
  SplitPair: (lefts: List a) -> (rights: List a) -> SplitList (lefts ++ rights)

total splitList: (input: List a) -> SplitList input
splitList input = splitListHelp input input
  where
    splitListHelp: List a -> (input: List a) -> SplitList input
    splitListHelp _  []  = SplitNil
    splitListHelp _  [x] = SplitOne
    splitListHelp (_ :: _ :: counter) (item :: items) =
      case splitListHelp counter items of
        SplitNil               => SplitOne
        SplitOne {x}           => SplitPair [item] [x]
        SplitPair lefts rights => SplitPair (item :: lefts) rights
    splitListHelp _ items = SplitPair [] items

mergeSort: Ord a => List a -> List a
mergeSort input with (splitList input)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ rights) | (SplitPair lefts rights) =
    merge (mergeSort lefts) (mergeSort rights)

total mergeSort2: Ord a => List a -> List a
mergeSort2 input with (splitRec input)
  mergeSort2 []   | SplitRecNil = []
  mergeSort2 [x]  | SplitRecOne = [x]
  mergeSort2 (lefts ++ rights) | (SplitRecPair lrec rrec) =
    merge (mergeSort2 lefts  | lrec)
          (mergeSort2 rights | rrec)

example: List Int
example = [6,5,4,3,3,1,3,7,3,4,5,1,2,1,2,4,6,9,6]


text:
module AutoSearchHide2

import AutoSearchHide1

myZero : Value === 0
myZero = Refl

[OneA] A where
  Value = 1

%hint
HintOneA : A
HintOneA = OneA

-- Want to use the OneA (via HintOneA) instance here.

-- `%hide` should block the auto-search from
-- including the `HintZeroA` hint into the list of solutions.
-- Thus, we don't get into the `multiple solutions` situation.
%hide HintZeroA
myOne : Value === 1
myOne = Refl


text:
module LuaAst

import Core.Name
import Core.TT

import Data.Vect

%hide Core.TT.Visibility

public export
data Visibility = Local
                | Global

export
Eq Visibility where
 (==) Local Local = True
 (==) Global Global = True
 (==) _ _ = False

public export
data LuaExpr =  LLVar Name -- references some local variable
              | LGVar Name -- references some global variable defined inside `idris` table
              | LLambda (List Name) LuaExpr
              | LApp LuaExpr (List LuaExpr)
              | LPrimFn (PrimFn arity) (Vect arity LuaExpr)
              | LTrue          --literal 'true'
              | LFalse         --literal 'false'
              | LNil           --literal 'nil'
              | LNumber String --literal number
              | LBigInt String --literal bigint
              | LString String --literal string
              | LTable (List (LuaExpr, LuaExpr))
              | LIndex LuaExpr LuaExpr
              | LSeq LuaExpr LuaExpr
              | LReturn LuaExpr
              | LAssign (Maybe Visibility) LuaExpr LuaExpr  --decl with initial val and reassignment
              | LDeclVar Visibility Name
              | LIfThenElse LuaExpr LuaExpr LuaExpr
              | LBreak
              | LWhile LuaExpr LuaExpr
              | LDoNothing
              | LComment String

public export
Semigroup LuaExpr where
  LDoNothing <+> y = y
  x <+> LDoNothing = x
  x <+> y = LSeq x y

public export
Monoid LuaExpr where
  neutral = LDoNothing

public export
primFnNames : List String
primFnNames =
   ["prim__cast_IntChar"
   ,"prim__cast_IntegerDouble"
   ,"prim__cast_IntDouble"
   ,"prim__cast_StringDouble"
   ,"prim__cast_DoubleInt"
   ,"prim__cast_CharInt"
   ,"prim__cast_IntegerInt"
   ,"prim__cast_StringInt"
   ,"prim__cast_DoubleInteger"
   ,"prim__cast_CharInteger"
   ,"prim__cast_IntInteger"
   ,"prim__cast_StringInteger"
   ,"prim__cast_DoubleString"
   ,"prim__cast_CharString"
   ,"prim__cast_IntegerString"
   ,"prim__cast_IntString"
   ,"prim__doubleCeiling"
   ,"prim__doubleFloor"
   ,"prim__doubleSqrt"
   ,"prim__doubleATan"
   ,"prim__doubleACos"
   ,"prim__doubleASin"
   ,"prim__doubleTan"
   ,"prim__doubleCos"
   ,"prim__doubleSin"
   ,"prim__doubleLog"
   ,"prim__doubleExp"
   ,"prim__crash"
   ,"prim__believe_me"
   ,"prim__strSubstr"
   ,"prim__strReverse"
   ,"prim__strAppend"
   ,"prim__strCons"
   ,"prim__strIndex"
   ,"prim__strTail"
   ,"prim__strHead"
   ,"prim__strLength"
   ,"prim__gt_String"
   ,"prim__gt_Double"
   ,"prim__gt_Char"
   ,"prim__gt_Integer"
   ,"prim__gt_Int"
   ,"prim__gte_String"
   ,"prim__gte_Double"
   ,"prim__gte_Char"
   ,"prim__gte_Integer"
   ,"prim__gte_Int"
   ,"prim__eq_String"
   ,"prim__eq_Double"
   ,"prim__eq_Char"
   ,"prim__eq_Integer"
   ,"prim__eq_Int"
   ,"prim__lte_String"
   ,"prim__lte_Double"
   ,"prim__lte_Char"
   ,"prim__lte_Integer"
   ,"prim__lte_Int"
   ,"prim__lt_String"
   ,"prim__lt_Double"
   ,"prim__lt_Char"
   ,"prim__lt_Integer"
   ,"prim__lt_Int"
   ,"prim__xor_Int"
   ,"prim__or_Integer"
   ,"prim__or_Int"
   ,"prim__and_Integer"
   ,"prim__and_Int"
   ,"prim__shr_Integer"
   ,"prim__shr_Int"
   ,"prim__shl_Integer"
   ,"prim__shl_Int"
   ,"prim__negate_Double"
   ,"prim__mod_Integer"
   ,"prim__mod_Int"
   ,"prim__div_Double"
   ,"prim__div_Integer"
   ,"prim__div_Int"
   ,"prim__mul_Double"
   ,"prim__mul_Integer"
   ,"prim__mul_Int"
   ,"prim__sub_Double"
   ,"prim__sub_Integer"
   ,"prim__sub_Int"
   ,"prim__add_Double"
   ,"prim__add_Integer"
   ,"prim__add_Int"
   ]


text:
module Main

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

import System
import System.Directory
import System.File
import System.Info
import System.Path

%default covering

------------------------------------------------------------------------
-- Test cases

ttimpTests : List String
ttimpTests
    = ["basic001", "basic002", "basic003", "basic004", "basic005",
       "basic006",
       "coverage001", "coverage002",
       "dot001",
       "eta001", "eta002",
       "lazy001",
       "nest001", "nest002",
       "perf001", "perf002", "perf003",
       "record001", "record002", "record003",
       "qtt001", "qtt003",
       "total001", "total002", "total003"]

idrisTests : List String
idrisTests
    = -- Fundamental language feturea
      ["basic001", "basic002", "basic003", "basic004", "basic005",
       "basic006", "basic007", "basic008", "basic009", "basic010",
       "basic011", "basic012", "basic013", "basic014", "basic015",
       "basic016", "basic017", "basic018", "basic019", "basic020",
       "basic021", "basic022", "basic023", "basic024", "basic025",
       "basic026", "basic027", "basic028", "basic029", "basic030",
       "basic031", "basic032", "basic033", "basic034", "basic035",
       "basic036", "basic037", "basic038", "basic039", "basic040",
       "basic041", "basic042", "basic043", "basic044", "basic045",
       "basic046",
       -- Coverage checking
       "coverage001", "coverage002", "coverage003", "coverage004",
       "coverage005", "coverage006", "coverage007", "coverage008",
       "coverage009", "coverage010",
       -- Documentation strings
       "docs001", "docs002",
       -- Evaluator
       "evaluator001", "evaluator002",
       -- Error messages
       "error001", "error002", "error003", "error004", "error005",
       "error006", "error007", "error008", "error009", "error010",
       "error011", "error012", "error013",
       -- Modules and imports
       "import001", "import002", "import003", "import004", "import005",
       -- Interactive editing support
       "interactive001", "interactive002", "interactive003", "interactive004",
       "interactive005", "interactive006", "interactive007", "interactive008",
       "interactive009", "interactive010", "interactive011", "interactive012",
       "interactive013", "interactive014", "interactive015", "interactive016",
       "interactive017", "interactive018",
       -- Interfaces
       "interface001", "interface002", "interface003", "interface004",
       "interface005", "interface006", "interface007", "interface008",
       "interface009", "interface010", "interface011", "interface012",
       "interface013", "interface014", "interface015", "interface016",
       "interface017",
       -- Miscellaneous REPL
       "interpreter001", "interpreter002", "interpreter003",
       -- Implicit laziness, lazy evaluation
       "lazy001",
       -- QTT and linearity related
       "linear001", "linear002", "linear003", "linear004", "linear005",
       "linear006", "linear007", "linear008", "linear009", "linear010",
       "linear011", "linear012",
       -- Literate
       "literate001", "literate002", "literate003", "literate004",
       "literate005", "literate006", "literate007", "literate008",
       "literate009", "literate010", "literate011", "literate012",
       "literate013", "literate014",
       -- Namespace blocks
       "namespace001",
       -- Parameters blocks
       "params001",
       -- Performance: things which have been slow in the past, or which
       -- pose interesting challenges for the elaborator
       "perf001", "perf002", "perf003", "perf004", "perf005",
       -- Parse errors
       "perror001", "perror002", "perror003", "perror004", "perror005",
       "perror006",
       -- Packages and ipkg files
       "pkg001", "pkg002", "pkg003", "pkg004", "pkg005",
       -- Positivity checking
       "positivity001", "positivity002", "positivity003",
       -- Larger programs arising from real usage. Typically things with
       -- interesting interactions between features
       "real001", "real002",
       -- Records, access and dependent update
       "record001", "record002", "record003", "record004", "record005",
       "record007",
       -- Quotation and reflection
       "reflection001", "reflection002", "reflection003", "reflection004",
       "reflection005", "reflection006", "reflection007", "reflection008",
       "reflection009",
       -- Miscellaneous regressions
       "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
       "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
       "reg029", "reg030", "reg031", "reg032", "reg033", "reg034",
       -- Totality checking
       "total001", "total002", "total003", "total004", "total005",
       "total006", "total007", "total008", "total009", "total010",
       -- The 'with' rule
       "with001", "with002",
       -- with-disambiguation
       "with003"]

typeddTests : List String
typeddTests
   = ["chapter01", "chapter02", "chapter03", "chapter04", "chapter05",
      "chapter06", "chapter07", "chapter08", "chapter09", "chapter10",
      "chapter11", "chapter12", "chapter13", "chapter14"]

chezTests : List String
chezTests
   = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
      "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
      "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
      "chez019", "chez020", "chez021", "chez022", "chez023", "chez024",
      "chez025", "chez026", "chez027", "chez028", "chez029", "chez030",
      "chez031",
      "reg001"]

nodeTests : List String
nodeTests
  = [ "node001", "node002", "node003", "node004", "node005", "node006", "node007", "node008", "node009"
    , "node011", "node012", "node015", "node017", "node018", "node019" -- node014
    , "node021", "node022" --, "node020"
    , "reg001"
    , "syntax001"
    , "tailrec001"
    ]

ideModeTests : List String
ideModeTests
  =  [ "ideMode001", "ideMode002", "ideMode003", "ideMode004" ]

preludeTests : List String
preludeTests
  =  [ "reg001" ]

erlangTests : List String
erlangTests
   = ["erlang001", "erlang002", "erlang003", "erlang004", "erlang005",
      "erlang006", "erlang007", "erlang008", "erlang009", "erlang010",
      "erlang011", "erlang012",
      "chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
      "chez007", "chez008", "chez009",            "chez011", "chez012",
                            "chez015", "chez016", "chez017", "chez018",
      "chez019",            "chez021",                       "chez024",
      "chez025", "chez026", "chez027", "chez028",
      "reg001"]
      -- Disabled tests:
      -- * chez010: Calling C functions is not supported
      -- * chez013: Calling C functions is not supported
      -- * chez014: Calling C functions is not supported
      -- * chez020: Require System.File.popen (Might be possible to implement)
      -- * chez022: Calling C functions is not supported
      -- * chez023: Uses Control.App (which transitively depends on Data.IORef and System.File)

------------------------------------------------------------------------
-- Options

||| Options for the test driver.
record Options where
  constructor MkOptions
  ||| Name of the idris2 executable
  idris2      : String
  ||| Should we only run some specific cases?
  onlyNames   : List String
  ||| Should we run the test suite interactively?
  interactive : Bool

usage : String
usage = "Usage: runtests <idris2 path> [--interactive] [--only [NAMES]]"

options : List String -> Maybe Options
options args = case args of
    (_ :: idris2 :: rest) => go rest (MkOptions idris2 [] False)
    _ => Nothing

  where

    go : List String -> Options -> Maybe Options
    go rest opts = case rest of
      []                      => pure opts
      ("--interactive" :: xs) => go xs (record { interactive = True } opts)
      ("--only" :: xs)        => pure $ record { onlyNames = xs } opts
      _ => Nothing

------------------------------------------------------------------------
-- Actual test runner

fail : String -> IO ()
fail err
    = do putStrLn err
         exitWith (ExitFailure 1)

-- on Windows, we just ignore backslashes and slashes when comparing,
-- similarity up to that is good enough. Leave errors that depend
-- on the confusion of slashes and backslashes to unix machines.
normalize : String -> String
normalize str =
    if isWindows
      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
      else str

runTest : Options -> String -> IO Bool
runTest opts testPath
    = do changeDir testPath
         isSuccess <- runTest'
         changeDir "../.."
         pure isSuccess
    where
        getAnswer : IO Bool
        getAnswer = do
          str <- getLine
          case str of
            "y" => pure True
            "n" => pure False
            _   => do putStrLn "Invalid Answer."
                      getAnswer

        printExpectedVsOutput : String -> String -> IO ()
        printExpectedVsOutput exp out = do
          putStrLn "Expected:"
          printLn exp
          putStrLn "Given:"
          printLn out

        mayOverwrite : Maybe String -> String -> IO ()
        mayOverwrite mexp out = do
          the (IO ()) $ case mexp of
            Nothing => putStr $ unlines
              [ "Golden value missing. I computed the following result:"
              , out
              , "Accept new golden value? [yn]"
              ]
            Just exp => do
              putStrLn "Golden value differs from actual value."
              code <- system "git diff --no-index --exit-code --word-diff=color expected output"
              when (code < 0) $ printExpectedVsOutput exp out
              putStrLn "Accept actual value as new golden value? [yn]"
          b <- getAnswer
          when b $ do Right _ <- writeFile "expected" out
                          | Left err => print err
                      pure ()
        runTest' : IO Bool
        runTest'
            = do putStr $ testPath ++ ": "
                 system $ "sh ./run " ++ idris2 opts ++ " | tr -d '\\r' > output"
                 Right out <- readFile "output"
                     | Left err => do print err
                                      pure False
                 Right exp <- readFile "expected"
                     | Left FileNotFound => do
                         if interactive opts
                           then mayOverwrite Nothing out
                           else print FileNotFound
                         pure False
                     | Left err => do print err
                                      pure False
                 let result = normalize out == normalize exp
                 if result
                    then putStrLn "success"
                    else do
                      putStrLn "FAILURE"
                      if interactive opts
                         then mayOverwrite (Just exp) out
                         else printExpectedVsOutput exp out

                 pure result

exists : String -> IO Bool
exists f
    = do Right ok <- openFile f Read
             | Left err => pure False
         closeFile ok
         pure True

firstExists : List String -> IO (Maybe String)
firstExists [] = pure Nothing
firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs

pathLookup : List String -> IO (Maybe String)
pathLookup names = do
  path <- getEnv "PATH"
  let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
  let candidates = [p ++ "/" ++ x | p <- pathList,
                                    x <- names]
  firstExists candidates

findChez : IO (Maybe String)
findChez
    = do Just chez <- getEnv "CHEZ" | Nothing => pathLookup ["chez", "chezscheme9.5", "scheme", "scheme.exe"]
         pure $ Just chez

findNode : IO (Maybe String)
findNode
    = do Just chez <- getEnv "NODE" | Nothing => pathLookup ["node"]
         pure $ Just chez

runChezTests : Options -> List String -> IO (List Bool)
runChezTests opts tests
    = do chexec <- findChez
         maybe (do putStrLn "Chez Scheme not found"
                   pure [])
               (\c => do putStrLn $ "Found Chez Scheme at " ++ c
                         traverse (runTest opts) tests)
               chexec

runNodeTests : Options -> List String -> IO (List Bool)
runNodeTests opts tests
    = do nodeexec <- findNode
         maybe (do putStrLn "node not found"
                   pure [])
               (\c => do putStrLn $ "Found node at " ++ c
                         traverse (runTest opts) tests)
               nodeexec

runErlangTests : Options -> List String -> IO (List Bool)
runErlangTests opts tests = traverse (runTest opts) tests

filterTests : Options -> List String -> List String
filterTests opts = case onlyNames opts of
  [] => id
  xs => filter (\ name => any (`isInfixOf` name) xs)

main : IO ()
main
    = do args <- getArgs
         let (Just opts) = options args
              | _ => do print args
                        putStrLn usage
         let filteredNonCGTests =
              filterTests opts $ concat $
                 [ testPaths "ttimp" ttimpTests
                 , testPaths "idris2" idrisTests
                 , testPaths "typedd-book" typeddTests
                 , testPaths "ideMode" ideModeTests
                 , testPaths "prelude" preludeTests
                 ]
         let filteredChezTests = filterTests opts (testPaths "chez" chezTests)
         let filteredNodeTests = filterTests opts (testPaths "node" nodeTests)
         let filteredErlangTests = filterTests opts (testPaths "erlang" erlangTests)
         nonCGTestRes <- traverse (runTest opts) filteredNonCGTests
         chezTestRes <- if length filteredChezTests > 0
              then runChezTests opts filteredChezTests
              else pure []
         nodeTestRes <- if length filteredNodeTests > 0
              then runNodeTests opts filteredNodeTests
              else pure []
         let res = nonCGTestRes ++ chezTestRes ++ nodeTestRes
         erlangTestRes <- if length filteredErlangTests > 0
              then runErlangTests opts filteredErlangTests
              else pure []
         let res = nonCGTestRes ++ chezTestRes ++ nodeTestRes ++ erlangTestRes
         putStrLn (show (length (filter id res)) ++ "/" ++ show (length res)
                       ++ " tests successful")
         if (any not res)
            then exitWith (ExitFailure 1)
            else exitWith ExitSuccess
    where
         testPaths : String -> List String -> List String
         testPaths dir tests = map (\test => dir ++ "/" ++ test) tests


text:
module Size

public export
record Size where
  constructor CreateSize
  src : String
  width : Integer
  height : Integer
  type : String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
interface Add a where
  add : a -> a

testAdd : Nat -> Nat -> Nat
testAdd x y = add x
  where
    Add Nat where
      add Z = y
      add (S k) = add k


text:
module Skeletons.Pipeline

import System
import System.Concurrency
import System.Concurrency.BufferedChannel

%default total

||| Representation of the data in a pipeline. Data flows through the stage(s)
||| using NEXT, until we are DONE.
public export
data PipelineData : Type -> Type where
  DONE : PipelineData a
  NEXT : a -> PipelineData a

||| A stage in a pipeline, processing a type of @PipelineData@.
data PipelineStage : Type -> Type -> Type where
  MkDStep : (PipelineData a -> PipelineData b) -> PipelineStage a b

||| A Pipeline from a -> b is a skeleton typically consisting of multiple
||| independent stages, with the final stage producing something of type `b`,
||| and the other stages doing intermediary work towards this. Since the stages
||| are independent, each stage can be run in parallel.
export
data Pipeline : Type -> Type -> Type where
  -- A Data Pipeline consists of either its Endpoint, where the final processing
  -- step happens; or a Stage where some processing happens, followed by a
  -- continuation Pipeline where the rest of the processing happens.
  DEndpoint : (lastly : PipelineStage a b) -> Pipeline a b
  DStage    : (thisStage : PipelineStage a b)
            -> (continuation : Pipeline b c)
            -> Pipeline a c

||| Declare a new pipeline, with initStage as its only stage.
|||
||| @initStage A stage to use as the basis for a new pipeline.
export
initPipeline : (initStage : PipelineData a -> PipelineData b) -> Pipeline a b
initPipeline initStage = DEndpoint $ MkDStep initStage

||| Add a stage to the end of an existing @Pipeline@, changing the output-type
||| of the Pipeline.
|||
||| @pl       The Pipeline to add the stage to.
||| @newStage The stage to add.
export
addStage : (pl : Pipeline a b)
         -> (newStage : PipelineData b -> PipelineData c)
         -> Pipeline a c
addStage (DEndpoint lastly) newStage =
  DStage lastly (DEndpoint $ MkDStep newStage)  -- newStage becomes new `lastly`

addStage (DStage thisStage continuation) newStage =
  DStage thisStage $ addStage continuation newStage

infixl 8 |>

||| Shorthand for `addStage`.
export
(|>) : {b : _} -> Pipeline a b -> (PipelineData b -> PipelineData c) -> Pipeline a c
(|>) = addStage

||| Given some input, process it and keep receiving input. If the input was
||| initially `DONE` / When the loop eventually gets a `DONE`, no processing is
||| computed and the `DONE` is simply passed along on the `outChan`
||| BufferedChannel.
loop : (stage : (PipelineStage a b))
     -> (plData : PipelineData a)
     -> (inRef : IORef (BufferedChannel (PipelineData a) ))
     -> (outRef : IORef (BufferedChannel (PipelineData b) ))
     -> IO ()
loop _ DONE _ outRef =
  do (MkDPair outChan send) <- becomeSender outRef
     send Signal outChan DONE

loop stage@(MkDStep f) next inRef outRef =
  do (MkDPair outChan send) <- becomeSender outRef
     (MkDPair inChan  recv) <- becomeReceiver Blocking inRef

     send Signal outChan (f next)
     next' <- recv inChan
     let inRef' = assert_smaller inRef inRef
     --           ^ Idris cannot know recv reduces the size of a shared channel
     loop stage next' inRef' outRef

||| Given a @Pipeline@ and a @BufferedChannel@ which supplies input for the
||| first stage, run each stage of the Pipeline in parallel, linking them up
||| using BufferedChannels. Returns the @ThreadID@ of the last stage in the
||| Pipeline, and an @IORef@ to a BufferedChannel over which to receive the
||| final results.
|||
||| @pl    The Pipeline to run.
||| @inRef An IORef to a BufferedChannel containing the input for the initial
|||        stage.
export
runPipeline : (pl : Pipeline x y)
             -> (inRef : IORef (BufferedChannel (PipelineData x)))
             -> IO (ThreadID, IORef (BufferedChannel (PipelineData y)))
runPipeline (DEndpoint lastly) inRef =
  do outRef <- makeBufferedChannel
     (MkDPair inChan  recv) <- becomeReceiver Blocking inRef

     input <- recv inChan
     threadID <- fork $ loop lastly input inRef outRef
     pure (threadID, outRef)

runPipeline (DStage thisStage continuation) inRef =
  do linkRef <- makeBufferedChannel
     (MkDPair inChan recv) <- becomeReceiver Blocking inRef

     input <- recv inChan
     doWeCare <- fork $ loop thisStage input inRef linkRef
     -- ^ I don't think we do...
     runPipeline continuation linkRef


text:
module Circuits.Idealised.Lexer

import public Circuits.Common.Lexer

%default total

namespace Idealised

  symbols : List String
  symbols = ["[", "]", ";", "{", "}", ":", ",", "=", "?", "(", ")", ".", "#", "!", "&", "|", "+"]

  keywords : List String
  keywords = [ "input", "output"
             , "module", "endmodule"
             , "wire"
             , "logic", "as", "in"
             , "and", "ior", "xor", "nand", "nior", "xnor", "not"
             , "copy", "join"
             , "extract", "insert"
             , "first", "last"
             , "index", "merge"
             , "mux"
             ]

  export
  Lexer : Lexer Token
  Lexer = Common.Lexer (langSpec symbols keywords)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module GridOps

import Data.Vect
import src.Tensor

%access public export

shiftLeft : a -> Vect n a -> Vect n a
shiftLeft e [] = []
shiftLeft {n = S n} e (x :: xs) = replace {P = (\x => Vect x a)} (plusCommutative n 1) (xs ++ [e])

shiftRight : a -> Vect n a -> Vect n a
shiftRight e xs = reverse $ shiftLeft e $ reverse xs

data Dir = Left | Right | Up | Down

shift : List Dir -> a -> Vect n (Vect m a) -> Vect n (Vect m a)
shift [] e xss = xss
shift (Left :: ds) e xss = shift ds e (map (shiftLeft e) xss)
shift (Right :: ds) e xss = shift ds e (map (shiftRight e) xss)
shift (Up :: ds) e xss = shift ds e (shiftLeft (replicate _ e) xss)
shift (Down :: ds) e xss = shift ds e (shiftRight (replicate _ e) xss)

data Pos = First | Last | Middle

toPos : Fin n -> Pos
toPos {n} fin with (finToNat fin)
 toPos {n} fin | Z = First
 toPos {n} fin | n' = if n == (S n') then Last else Middle

lookup : Fin n -> Fin m -> List Dir -> a -> Vect n (Vect m a) -> a
lookup n m ds x xss = index n m $ shift ds x xss

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Transducer

import Data.Vect
import Set
import Graph as G

%access public export

record TransLabel (n : Nat) (m : Nat) where
  constructor MkTransLabel
  input : Fin n
  output : Fin m

Show (Fin n) where
  show = show . finToNat

Show (TransLabel n m) where
  show (MkTransLabel input output)
    = "\"" ++ show input ++ " : " ++ show output ++ "\""

data Transducer : (stt : Type) -> Vect ipl ipt -> Vect opl opt -> Type where
  MkTransducer : (ipa : Vect ipl ipt) -> -- Input alphabet, length `ipl`, type `ipt`
                 (opa : Vect opl opt) -> -- Output alphabet, length `opl`, type `opt`
                 Graph stt (TransLabel ipl opl) ->
                 Transducer stt ipa opa

isSeq : List (Fin n) -> Bool
isSeq = isSeq' FZ where
  isSeq' : Fin (S k) -> List (Fin k) -> Bool
  isSeq' _ [] = True
  isSeq' x (y :: ys) = x == (weaken y) && (isSeq' (FS x) (map weaken ys))

mkTransducer : (ipa : Vect ipl ipt) ->
               (opa : Vect opl opt) ->
               Graph stt (TransLabel ipl opl) ->
               Maybe (Transducer stt ipa opa)
mkTransducer ipa opa g
  = if all (isSeq .
            sort .
            (map (input . Edge.label)) .
            (out g)) (nodes g)
       then Just (MkTransducer ipa opa g)
       else Nothing

empty : (ipa : Vect ipl ipt) -> (opa : Vect opl opt) -> Transducer stt ipa opa
empty ipa opa = MkTransducer ipa opa empty

groupByInput : List (LEdge (TransLabel ipl opl)) ->
               Vect ipl (List (LEdge (TransLabel ipl opl)))
groupByInput
  = let bin = replicate _ [] in
    foldr (\ledge => updateAt (input (label ledge)) ((::) ledge)) bin

groupByOutput : List (LEdge (TransLabel ipl opl)) ->
                Vect opl (List (LEdge (TransLabel ipl opl)))
groupByOutput
  = let bin = replicate _ [] in
    foldr (\ledge => updateAt (output (label ledge)) ((::) ledge)) bin

reorder : Ord a => (a, a) -> (a, a)
reorder (x1, x2) = if x1 > x2 then (x2, x1) else (x1, x2)

ambiguities : Transducer stt ipa opa -> Set (NodeID, NodeID)
ambiguities (MkTransducer _ _ g)
  = concat (map (formPairs . groupByInput) (groupByOutput . labEdges $ g)) where
    -- Each element of the vector is a list of edges sharing the same input
    -- All edges share the same output
    formPairs : Vect n (List (LEdge (TransLabel ipl' opl'))) -> Set (NodeID, NodeID)
    formPairs [] = empty
    formPairs (ledges :: rest)
      = union
          (fromList [reorder (q1, q2) | q1 <- map target ledges,
                                q2 <- map target (concat rest)])
          (formPairs rest)

propagate : Transducer stt ipa opa -> (NodeID, NodeID) -> Set (NodeID, NodeID)
propagate (MkTransducer _ _ g) (q1, q2)
  = concat (zipWith formPairs (listOutput q1) (listOutput q2)) where
    listOutput : NodeID -> Vect opl (List (LEdge (TransLabel ipl opl)))
    listOutput node = groupByOutput (out g node)
    formPairs : List (LEdge (TransLabel ipl' opl')) ->
                List (LEdge (TransLabel ipl' opl')) ->
                Set (NodeID, NodeID)
    formPairs l1 l2 = fromList [reorder (q1, q2) | q1 <- map target l1, q2 <- map target l2]

isInvertible : Transducer stt ipa opa -> Bool
isInvertible t =  ?qef
-- For each state, group it by producing

graph : Transducer stt ipa {ipl} opa {opl} -> Graph stt (TransLabel ipl opl)
graph (MkTransducer _ _ g) = g

transdu : Transducer String [0, 1] ["a", "b"]
transdu = maybe (empty [0, 1] ["a", "b"]) id (mkTransducer [0, 1] ["a", "b"] g) where
  g : Graph String (TransLabel 2 2)
  g = ([(MkTransLabel 1 0, 1)], 2, "q2", [(MkTransLabel 1 1, 2), (MkTransLabel 0 1, 1)])
       & ([], 1, "q1", [(MkTransLabel 0 0, 1)])
       & empty

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
module Addition.Digit

import Common.Util
import Common.Interfaces
import Specifications.TranslationInvariance
import Proofs.Interval

%default total
%access public export

data Digit : (leq : Binrel s) -> (neg : s -> s) -> s -> Type where
  MkDigit : (x : s) -> .InSymRange leq neg u x -> Digit leq neg u

val : Digit {s} _ _ _ -> s
val (MkDigit x _) = x

implementation Show s => Show (Digit {s} leq neg u) where
  show (MkDigit x _) = show x

||| adding two digits makes the range twice as big
addDigits : Ringops s => PartiallyOrderedGroupSpec {s} (+) Zero Ng leq ->
  OuterBinop (Digit leq Ng) u u (u + u)
addDigits spec (MkDigit x p) (MkDigit y q) =
  MkDigit (x + y) (addInSymRange spec p q)

||| To produce test input, full decidability is overkill
maybeDigit : Decidable [s,s] leq => (neg : s -> s) -> (u : s) ->
  s -> Maybe (Digit leq neg u)
maybeDigit {leq} neg u x =
  case decideBetween {leq} (neg u) u x of
    Yes prf => Just (MkDigit x prf)
    No _ => Nothing

||| To produce test input, full decidability is overkill
maybeDigits : (Traversable trav, Decidable [s,s] leq) =>
  (neg : s -> s) -> (u : s) -> trav s -> Maybe (trav (Digit leq neg u))
maybeDigits {leq} neg u = sequence . map (maybeDigit {leq} neg u)

max_stars_repo_name: jeroennoels/verified-exact-real

max_issues_repo_name: jeroennoels/verified-exact-real

max_forks_repo_name: jeroennoels/verified-exact-real


text:
%flag C "-L/usr/local/Cellar/cairo/1.14.6_1/lib -lcairo"
%flag C "-I/usr/local/Cellar/cairo/1.14.6_1/include/cairo -I/usr/local/Cellar/glib/2.50.1/include/glib-2.0 -I/usr/local/Cellar/glib/2.50.1/lib/glib-2.0/include -I/usr/local/opt/gettext/include -I/usr/local/Cellar/pcre/8.39/include -I/usr/local/Cellar/pixman/0.34.0/include/pixman-1 -I/usr/local/Cellar/fontconfig/2.12.1_2/include -I/usr/local/opt/freetype/include/freetype2 -I/usr/local/Cellar/libpng/1.6.25/include/libpng16"

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


text:
module arkaghosh.Odds

import Evens

import Intro

||| inductive type family IsOdd (Ques 1)
data IsOdd : Nat -> Type where
    SZOdd : IsOdd (S Z)
    SSOdd : (n : Nat) -> (IsOdd n) -> (IsOdd (S (S n)))

||| witness that 3 is odd (Ques 2)
threeOddProof : IsOdd 3
threeOddProof = SSOdd 1 SZOdd

||| witness that 2 is not odd (Ques 3)
total
twoNotOdd : (IsOdd 2) -> Void
twoNotOdd SZOdd impossible -- twoNotOdd will be total even without this line
twoNotOdd (SSOdd Z pf) impossible

||| Property 1 - If n is odd then (S n) is even (Ques 4)
total
prop1 : (n : Nat) -> (IsOdd n) -> (IsEven (S n))
prop1 (S Z) SZOdd = SSEven Z ZEven
prop1 (S (S n)) (SSOdd n pf) = SSEven (S n) (prop1 n pf)

||| Property 2 - If n is even then (S n) is odd (Ques 5)
total
prop2 : (n : Nat) -> (IsEven n) -> (IsOdd (S n))
prop2 Z ZEven = SZOdd
prop2 (S (S n)) (SSEven n pf) = SSOdd (S n) (prop2 n pf)

||| Property 3 -  No number is both even and odd (Ques 7)
total
prop3 : (n : Nat) -> (IsOdd n) -> (IsEven n) -> Void
prop3 Z pf ZEven impossible
prop3 (S Z) SZOdd pf impossible
prop3 (S (S n)) (SSOdd n pf1) (SSEven n pf2) = prop3 n pf1 pf2

||| Property 4 - If n and m are odd, then (n + m) is even (Ques 8)
total
prop4 : (n : Nat) -> (m : Nat) -> (IsOdd n) -> (IsOdd m) -> (IsEven (add n m))
prop4 Z m pf1 pf2 impossible
prop4 (S Z) m pf1 pf2 = prop1 m pf2
prop4 (S (S n)) m (SSOdd n pf1) pf2 = SSEven (add n m) (prop4 n m pf1 pf2)

||| Property 5 -  Every number n : Nat is either even or odd (Ques 6)
total
prop5 : (n : Nat) -> Either (IsEven n) (IsOdd n)
prop5 Z = Left ZEven
prop5 (S n) = f n  (prop5 n)
    where f : (m : Nat) -> (Either (IsEven m) (IsOdd m)) -> (Either (IsEven (S m)) (IsOdd (S m)))
          f m (Left pf) = Right (prop2 m pf)
          f m (Right pf) = Left (prop1 m pf)

||| Congruence : If n = m then f(n) = f(m)
total
congruence : (a : Type) -> (f : a -> a) -> (n : a) -> (m : a) -> (n = m) -> (f(n) = f(m))
congruence typ f n n Refl = Refl

||| Property 6 - if n is odd, then there exists m such that n = 2m + 1 (Ques 9)
total
prop6 : (n : Nat) -> (IsOdd n) -> ( k: Nat ** S(double k) = n )
prop6 (S Z) SZOdd = (Z ** Refl)
prop6 (S (S n)) (SSOdd n pf) = ( (S m) ** pf1)
    where m : Nat
          pf2 : S(double m) = n
          m = fst(prop6 n pf)
          pf2 = snd(prop6 n pf)
          pf1 : S(double (S m)) = (S (S n))
          pf1 = congruence Nat f (S(double m)) n pf2
              where f : Nat -> Nat
                    f x = S( S x)


text:
module Counters

public export
record Counters where
  constructor CreateCounters
  albums : Integer
  audios : Integer
  followers : Integer
  friend : Integer
  groups : Integer
  mutualFriends : Integer
  notes : Integer
  onlineFriends : Integer
  pages : Integer
  photos : Integer
  userVideos : Integer
  videos : Integer


text:
module Mrk.Document

import public Control.Monad.Writer
import public Control.Monad.Identity

import Mrk.Elements

%default total
%access public export

Document : (parent : NodeName) -> Type
Document parent = Writer (Element parent) ()

fromDocument : Document parent -> Element parent
fromDocument = snd . runIdentity . runWriterT

Show (Document parent) where
  show children =
    show (fromDocument children)

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Data.Compress.Interface

public export
interface Decompressor a where
  ||| decompress a part of the compressed stream
  feed : a -> List Bits8 -> Either String (List Bits8, a)
  ||| signify the compressed stream has been completely consumed
  ||| return the leftover data
  done : a -> Either String (List Bits8)
  ||| init state
  init : a

public export
data IdentityState = Id

public export
Decompressor IdentityState where
  feed Id content = Right (content, Id)
  done Id = Right []
  init = Id

export
decompress : a -> Decompressor a => List Bits8 -> Either String (List Bits8)
decompress _ compressed = do
  (uncompressed, state) <- feed {a} init compressed
  [] <- done state
  | x => Left "{\show (length x)} leftover bytes"
  pure uncompressed


text:
module complexity

-- Computation complexity

data Cost : Nat -> Type -> Type where
    MkCost : t -> Cost n t

uncost : Cost n t -> t
uncost (MkCost x) = x

return : t -> Cost n t
return x = MkCost x

-- a Monad!
-- cost of doing dependant computations is the cost of doing both
(>>=) : Cost n a -> (a -> Cost m b) -> Cost (n + m) b
(>>=) (MkCost x) f = MkCost (uncost (f x))

doTimes : Semigroup a =>
          (n : Nat) ->
          Cost m a ->
          a ->
          Cost (n * m) a
doTimes Z _ accum = return accum
doTimes (S k) cost accum = do
    a <- cost
    doTimes k cost (accum <+> a)

-- Complexity of factorial
day : (n : Nat) -> Cost (fact n) String
day Z = return "."
day (S k) = doTimes (S k) (day k) "$"

-- Finite sets are numbers strictly less than some bound
run : (n : Fin 7) -> Cost (fact (finToNat n)) String
run n = day (finToNat n)

max_stars_repo_name: ExpandingShapes/idris-experiments

max_issues_repo_name: ExpandingShapes/idris-experiments

max_forks_repo_name: ExpandingShapes/idris-experiments


text:
--- Day 3: Binary Diagnostic ---

{--
A lot of stuff influenced by:
https://github.com/ryanorendorff/aoc2021/blob/main/src/AOC/Day/Three.idr
https://github.com/jumper149/AoC2021/blob/main/03/src/Main.idr
--}

module BinaryDiagnostic
import System
import System.File
import Data.List
import Data.List1
import Data.String
import Data.Vect
import Data.Bits
import Data.String.Parser

data Bit = Low | High

Show Bit where
    show Low = "0"
    show High = "1"

Cast Bool Bit where
    cast False = Low
    cast True = High

Cast Bit Integer where
    cast Low = 0
    cast High = 1

parseBit : Parser Bit
parseBit = char '0' $> Low
       <|> char '1' $> High

getLength : List a -> (len ** Vect len a)
getLength [] = (Z ** [])
getLength (x :: xs) with (getLength xs)
        _ | (n ** xs') = ((S n) ** x :: xs')

parseBits : Parser (n ** Vect n Bit)
parseBits = getLength <$> many parseBit

InputType : Type
InputType = (n ** List1 (Vect n Bit))

exactLengths : (len : Nat) -> Traversable t => t (n ** Vect n a) -> Maybe (t (Vect len a))
exactLengths len xs = traverse (\(_ **  bits) => exactLength len bits) xs

validateBinaryList : List1 (n ** Vect n Bit) -> Maybe InputType
validateBinaryList ((len ** bits) ::: tail) = exactLengths len tail >>= (\list => pure (len ** bits ::: list))

countBit : Bit -> Integer -> Integer
countBit Low x = x - 1
countBit High x = x + 1

mostCommon : Vect n Integer -> Vect n Bit
mostCommon = map $ cast . (> 0)

calculateGamma : {n : Nat} -> List1 (Vect n Bit) -> Vect n Integer
calculateGamma list = foldr (\x, acc => zipWith countBit x acc) (replicate n 0) list

bitsToInteger : Vect n Bit -> Integer
bitsToInteger [] = 0
bitsToInteger (b :: xs) = 2 * bitsToInteger xs + (cast b)

calculatePowerConsumption : InputType -> Integer
calculatePowerConsumption (n ** list) = let
                                            gamma = (bitsToInteger . reverse . mostCommon . calculateGamma) list
                                            epsilon = gamma `xor` (bitsToInteger $ replicate n High)
                                        in
                                            gamma * epsilon

main : IO ()
main = do
        args <- getArgs
        let (file :: _) = drop 1 args | [] => printLn "No file provided!"
        (Right symbols) <- readFile file | (Left error) => printLn error
        let (Right bits) = parse (sepBy1 parseBits (char '\n')) symbols | (Left error) => printLn error
        let (Just input) = (validateBinaryList . fst) bits | Nothing => printLn "Lengths of binary arrays are not equal!"
        (printLn . calculatePowerConsumption) input


text: module PQ.Schema.Query


text:
module Replica.App.Replica

import Control.App
import Control.App.Console

import Data.List
import Data.Maybe
import Data.String

import Language.JSON

import System.Path

import Replica.App.FileSystem
import Replica.App.System
import Replica.Command.Run
import Replica.Core.Parse
import Replica.Core.Types
import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

%default total

export
data CurrentTest : Type where

export
data GlobalConfig : Type where

public export
data ReplicaError
  = CantAccessTestFile String
  | InvalidJSON (List String)

export
Show ReplicaError where
  show (CantAccessTestFile x) = "Can't access file \{x}"
  show (InvalidJSON xs) = removeTrailingNL $ unlines $ "Can't parse JSON:" ::xs

export
testDir : String -> String
testDir = (</> "test")

export
logDir : String -> String
logDir = (</> "log")

export
lastRunLog : String -> String
lastRunLog rdir = logDir rdir </> "last.json"

export
getReplicaDir : State GlobalConfig Global e => App e String
getReplicaDir = replicaDir <$> get GlobalConfig

export
getGoldenDir : State GlobalConfig Global e => App e String
getGoldenDir = do
  gd <- goldenDir <$> get GlobalConfig
  maybe (testDir <$> getReplicaDir) pure gd

export
setAbsoluteReplicaDir : Has [State GlobalConfig Global, FileSystem] e => App e ()
setAbsoluteReplicaDir = do
  rdir <- getReplicaDir
  if isAbsolute rdir
     then pure ()
     else do
       pwd <- getCurrentDir
       modify GlobalConfig (record {replicaDir = pwd </> rdir})

export
getSingleTestDir : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getSingleTestDir = do
  d <- getReplicaDir
  t <- get CurrentTest
  pure $ testDir d </> t.name

export
getSingleTestFileDir : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getSingleTestFileDir = (</> defaultFile) <$> getSingleTestDir

export
getSingleTestGoldenDir : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getSingleTestGoldenDir = do
  d <- getGoldenDir
  t <- get CurrentTest
  pure $ d </> t.name

export
getSingleTestGoldenFileDir : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getSingleTestGoldenFileDir = (</> defaultFile) <$> getSingleTestGoldenDir

export
getErrorFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getErrorFile = do
  t <- getSingleTestDir
  pure $ t </> defaultError

export
getInputFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getInputFile = do
  t <- getSingleTestDir
  pure $ t </> defaultInput

export
getOutputFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getOutputFile = do
  t <- getSingleTestDir
  pure $ t </> defaultOutput

export
getStatusFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getStatusFile = do
  t <- getSingleTestDir
  pure $ t </> defaultStatus

export
getWatchedFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => String -> App e String
getWatchedFile f = do
  t <- get CurrentTest
  pure $ maybe f (</> f) t.workingDir

export
getExpectedOutput : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getExpectedOutput = do
  t <- getSingleTestGoldenDir
  pure $ t </> defaultExpectedOutput

export
getExpectedError : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getExpectedError = do
  t <- getSingleTestGoldenDir
  pure $ t </> defaultExpectedError

export
getExpectedFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => String -> App e String
getExpectedFile s = do
  t <- getSingleTestGoldenFileDir
  pure $ t </> s

export
getReplica :
  FileSystem (FSError :: e) =>
  Has [ State GlobalConfig Global
      , Exception ReplicaError ] e => App e Replica
getReplica = do
  ctx <- get GlobalConfig
  let fs = ctx.files
  content <- traverse readReplica fs
  let Just jsons = traverse parse content
        | Nothing => throw $ InvalidJSON []
  let res = traverse jsonToReplica jsons
  let Valid repl = map (>>= (\(MkReplica xs) => xs)) res
        | Error xs => throw $ InvalidJSON xs
  let ([], _) = duplicatedKeys repl
      | (dup, _) => throw $ InvalidJSON ["Duplicated key(s): \{show dup}"]
  pure $ MkReplica repl
  where
    readReplica : String -> App e String
    readReplica f = handle (readFile f)
      pure (\err : FSError => throw $ CantAccessTestFile f)
    go : (List String, List String) -> Test -> (List String, List String)
    go (dup, names) t = if t.name `elem` names
                           then if t.name `elem` dup
                                   then (dup, names)
                                   else (t.name :: dup, names)
                           else (dup, t.name :: names)
    duplicatedKeys : List Test -> (List String, List String)
    duplicatedKeys xs = foldl go ([], []) xs

export
when : Bool -> App e () -> App e ()
when cond x = if cond then x else pure ()

export
catchNew : App (err :: e) a -> (err -> App e a) -> App e a
catchNew x f = handle x pure (\er : err => f er)

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
-- --------------------------------------------------------------- [ Queue.idr ]
-- Module    : Queue.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Testing Queues
module Data.Test.Queue

import Test.Unit

import Data.Queue

%access export

covering
test2 : IO Bool
test2 = genericTest (Just "Enqueue") (pushQThings [1,2,3] mkQueue) (pushQ 3 $ pushQ 2 $ pushQ 1 mkQueue) (==)

partial
test3 : IO Bool
test3 = genericTest (Just "Dequeue") (popQ' (pushQThings [1,2,3] mkQueue)) (Just (1, setQueue Nil [2,3])) (==)

partial
runTest : IO ()
runTest = do
  putStrLn "Testing Queue"
  putStrLn infoLine
  NonReporting.runTests [
    test2
  , test3
  ]

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
-- Primitive Imperative Language --
module Example.Pil

import Data.List
import Data.List.Elem
import Data.Maybe

%default total

------------------------------------------------------
--- Auxiliary data definitions and their instances ---
------------------------------------------------------

export
data Name = MkName String

%name Name n, m

export
FromString Name where
  fromString = MkName

export
Eq Name where
  MkName n == MkName m = n == m

--- Static context in terms of which we are formulating an invariant ---

public export
Context : Type
Context = List (Name, Type)

%name Context ctx

-----------------------------------------------
--- List lookup with propositional equality ---
-----------------------------------------------

public export
data Lookup : a -> List (a, b) -> Type where
  There : Lookup z xys -> Lookup z $ (x, y)::xys
  Here : (y : b) -> Lookup x $ (x, y)::xys
  -- !!! Idris searches from the bottom !!!

public export
reveal : Lookup {b} x xys -> b
reveal (Here y) = y
reveal (There subl) = reveal subl

-----------------------------------
--- The main language structure ---
-----------------------------------

public export
data Expression : (ctx : Context) -> (res : Type) -> Type where
  -- Constant expression
  C : (x : ty) -> Expression ctx ty
  -- Value of the variable
  V : (n : Name) -> (0 ty : Lookup n ctx) => Expression ctx $ reveal ty
  -- Unary operation over the result of another expression
  U : (f : a -> b) -> Expression ctx a -> Expression ctx b
  -- Binary operation over the results of two another expressions
  B : (f : a -> b -> c) -> Expression ctx a -> Expression ctx b -> Expression ctx c

infix 2 #=, ?#=
infixr 1 *>

public export
data Statement : (pre : Context) -> (post : Context) -> Type where
  nop  : Statement ctx ctx
  (.)  : (0 ty : Type) -> (n : Name) -> Statement ctx $ (n, ty)::ctx
  (#=) : (n : Name) -> (0 ty : Lookup n ctx) => (v : Expression ctx $ reveal ty) -> Statement ctx ctx
  for  : (init : Statement outer_ctx inside_for)  -> (cond : Expression inside_for Bool)
      -> (upd  : Statement inside_for inside_for) -> (body : Statement inside_for after_body)
      -> Statement outer_ctx outer_ctx
  if__ : (cond : Expression ctx Bool) -> Statement ctx ctx_then -> Statement ctx ctx_else -> Statement ctx ctx
  (*>) : Statement pre mid -> Statement mid post -> Statement pre post
  block : Statement outer inside -> Statement outer outer
  print : Show ty => Expression ctx ty -> Statement ctx ctx

public export %inline
(>>=) : Statement pre mid -> (Unit -> Statement mid post) -> Statement pre post
a >>= f = a *> f ()

public export %inline
if_  : (cond : Expression ctx Bool) -> Statement ctx ctx_then -> Statement ctx ctx
if_ c t = if__ c t nop

public export %inline
while : Expression ctx Bool -> Statement ctx after_body -> Statement ctx ctx
while cond = for nop cond nop

-- Define with derived type and assign immediately
public export %inline
(?#=) : (n : Name) -> Expression ((n, ty)::ctx) ty -> Statement ctx $ (n, ty)::ctx
n ?#= v = ty. n *> n #= v

namespace AlternativeDefineAndAssign

  public export %inline
  (#=) : (p : (Name, Type)) -> Expression (p::ctx) (snd p) -> Statement ctx $ p::ctx
  (n, _) #= v = n ?#= v

  public export %inline
  (.) : a -> b -> (b, a)
  (.) a b = (b, a)

-------------------------
--- Examples of usage ---
-------------------------

--- Functions lifted to the expression level ---

export %inline
(+) : Expression ctx Int -> Expression ctx Int -> Expression ctx Int
(+) = B (+)

export %inline
div : Expression ctx Int -> Expression ctx Int -> Expression ctx Int
div = B div

export %inline
mod : Expression ctx Int -> Expression ctx Int -> Expression ctx Int
mod = B mod

export %inline
(<) : Expression ctx Int -> Expression ctx Int -> Expression ctx Bool
(<) = B (<)

export %inline
(>) : Expression ctx Int -> Expression ctx Int -> Expression ctx Bool
(>) = B (>)

export %inline
(==) : Eq a => Expression ctx a -> Expression ctx a -> Expression ctx Bool
(==) = B (==)

export %inline
(/=) : Eq a => Expression ctx a -> Expression ctx a -> Expression ctx Bool
(/=) = B (/=)

export %inline
(&&) : Expression ctx Bool -> Expression ctx Bool -> Expression ctx Bool
(&&) = B (\a, b => a && b) -- recoded because of laziness

export %inline
(++) : Expression ctx String -> Expression ctx String -> Expression ctx String
(++) = B (++)

export %inline
show : Show ty => Expression ctx ty -> Expression ctx String
show = U show

--- Example statements ---

simple_ass : Statement ctx $ ("x", Int)::ctx
simple_ass = do
  Int. "x"
  "x" #= C 2

lost_block : Statement ctx ctx
lost_block = do
  block $ do
    Int. "x"
    "x" #= C 2
    Int. "y" #= V "x"
    Int. "z" #= C 3
    print $ V "y" + V "z" + V "x"

some_for : Statement ctx ctx
some_for = for (do Int. "x" #= C 0; Int. "y" #= C 0) (V "x" < C 5 && V "y" < C 10) ("x" #= V "x" + C 1) $ do
             "y" #= V "y" + V "x" + C 1

--bad_for : Statement ctx ctx
--bad_for = for (do Int. "x" #= C 0; Int. "y" #= C 0)
--                (V "y")
--                  ("x" #= V "x" + C 1) $ do
--             "y" #= V "y" `div` V "x" + C 1

euc : {0 ctx : Context} -> let c = ("a", Int)::("b", Int)::ctx in Statement c $ ("res", Int)::c
euc = do
  while (V "a" /= C 0 && V "b" /= C 0) $ do
    if__ (V "a" > V "b")
      ("a" #= V "a" `mod` V "b")
      ("b" #= V "b" `mod` V "a")
  Int. "res" #= V "a" + V "b"

name_shadowing : Statement ctx ctx
name_shadowing = block $ do
  Int. "x" #= C 0
  block $ do
    Int. "x" #= C 3
    Int. "y" #= V "x" + C 2
    String. "x" #= C "foo"
    print $ V "x" ++ C "bar" ++ show (V "y")
  Int. "z" #= V "x" + C 2

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:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> (1 xs : Vect k a) -> Vect (S k) a

partial
append : (1 _ : Vect n a) -> Vect m a -> Vect (n + m) a
append (x :: zs@(y :: ws)) ys = ?foo -- zs usable, y+ws not

cappend : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) $a
cappend xs ys
    = case xs of
           Nil => ys
           x :: zs => ?bar -- zs usable, xs not

cappend2 : (1 _ : Vect n a) -> Vect m a -> Vect (plus n m) a
cappend2 xs ys
    = case xs of
           Nil => ys
           x :: zs => let ts = zs in ?baz -- ts usable, xs+zs not