text:
module SMTLib

import Data.Vect
import System

%access public export

data NumTyp = IntT | RealT

data TypeT : Type where
  BoolT : TypeT
  NumT : NumTyp -> TypeT
  BitVecT : Nat -> TypeT

Show TypeT where
  show BoolT = "Bool"
  show (NumT IntT) = "Int"
  show (NumT RealT) = "Real"
  show (BitVecT n) = "(_ BitVec " ++ show n ++ ")"

data Expr : TypeT -> Type where
  VarExpr : String -> (t : TypeT) -> Expr t
  BoolExpr : Bool -> Expr BoolT
  BvExpr : Int -> (n : Nat) -> Expr (BitVecT n)
  BvAddExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvSubExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvMulExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvUDivExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvURemExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvSDivExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvSModExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvShLExpr :  Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvLShRExpr :  Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvAShRExpr :  Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvNegExpr : Expr (BitVecT n) -> Expr (BitVecT n)
  BvAndExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvOrExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvXorExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvNotExpr : Expr (BitVecT n) -> Expr (BitVecT n)
  BvULeExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvULtExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvUGeExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvUGtExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvSLeExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvSLtExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvSGeExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  BvSGtExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
  IntExpr : Int -> Expr (NumT IntT)
  RealExpr : Double -> Expr (NumT RealT)
  AddExpr : Vect n (Expr (NumT a)) -> Expr (NumT a)
  MinusExpr : Vect n (Expr (NumT a)) -> Expr (NumT a)
  MulExpr : Vect n (Expr (NumT a)) -> Expr (NumT a)
  EqualExpr : Expr a -> Expr a -> Expr BoolT
  DistinctExpr : Vect n (Expr a) -> Expr BoolT
  LessExpr : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
  LessOrEqualExpr : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
  GreaterExpr : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
  GreaterOrEqualExpr : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
  AndExpr : Vect n (Expr BoolT) -> Expr BoolT
  OrExpr : Vect n (Expr BoolT) -> Expr BoolT
  NotExpr : Expr BoolT -> Expr BoolT
  ImpExpr : Expr BoolT -> Expr BoolT -> Expr BoolT
  IteExpr : Expr BoolT -> Expr a -> Expr a -> Expr a

bool : Bool -> Expr BoolT
bool x = BoolExpr x

bv : Int -> (n : Nat) -> Expr (BitVecT n)
bv x n = BvExpr x n

int : Int -> Expr (NumT IntT)
int x = IntExpr x

real : Double -> Expr (NumT RealT)
real x = RealExpr x

bvadd : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvadd l r = BvAddExpr l r

bvsub : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvsub l r = BvSubExpr l r

bvmul : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvmul l r = BvMulExpr l r

bvsdiv : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvsdiv l r = BvSDivExpr l r

bvsmod : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvsmod l r = BvSModExpr l r

bvudiv : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvudiv l r = BvUDivExpr l r

bvurem : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvurem l r = BvURemExpr l r

bvshl : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvshl l r = BvShLExpr l r

bvlshr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvlshr l r = BvLShRExpr l r

bvashr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvashr l r = BvAShRExpr l r

bvneg : Expr (BitVecT n) -> Expr (BitVecT n)
bvneg x = BvNegExpr x

bvand : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvand l r = BvAndExpr l r

bvor : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvor l r = BvOrExpr l r

bvxor : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvxor l r = BvXorExpr l r

bvnot : Expr (BitVecT n) -> Expr (BitVecT n)
bvnot x = BvNotExpr x

bvule : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvule l r = BvULeExpr l r

bvult : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvult l r = BvULtExpr l r

bvuge : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvuge l r = BvUGeExpr l r

bvugt : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvugt l r = BvUGtExpr l r

bvsle : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvsle l r = BvSLeExpr l r

bvslt : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvslt l r = BvSLtExpr l r

bvsge : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvsge l r = BvSGeExpr l r

bvsgt : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr BoolT
bvsgt l r = BvSGtExpr l r

(+) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
(+) l r = AddExpr [l, r]

(-) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
(-) l r = MinusExpr [l, r]

add : Vect n (Expr (NumT a)) -> Expr (NumT a)
add xs = AddExpr xs

(*) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
(*) l r = MulExpr [l, r]

mul : Vect n (Expr (NumT a)) -> Expr (NumT a)
mul xs = MulExpr xs

(==) : Expr a -> Expr a -> Expr BoolT
(==) l r = EqualExpr l r

distinct : Vect n (Expr a) -> Expr BoolT
distinct xs = DistinctExpr xs

(<) : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
(<) l r = LessExpr l r

(<=) : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
(<=) l r = LessOrEqualExpr l r

(>) : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
(>) l r = GreaterExpr l r

(>=) : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
(>=) l r = GreaterOrEqualExpr l r

(&&) : Expr BoolT -> Expr BoolT -> Expr BoolT
(&&) l r = AndExpr [l, r]

(||) : Expr BoolT -> Expr BoolT -> Expr BoolT
(||) l r = OrExpr [l, r]

and : Vect n (Expr BoolT) -> Expr BoolT
and xs = AndExpr xs

or : Vect n (Expr BoolT) -> Expr BoolT
or xs = OrExpr xs

not : Expr BoolT -> Expr BoolT
not x = NotExpr x

imp : Expr BoolT -> Expr BoolT -> Expr BoolT
imp l r = ImpExpr l r

ite' : Expr BoolT -> Expr BoolT -> Expr BoolT -> Expr BoolT
ite' p l r = and [imp p l, imp (not p) r]

ite : Expr BoolT -> Expr a -> Expr a -> Expr a
ite p l r = IteExpr p l r

data Cmd : Type -> Type where
  DeclareVarCmd : String -> (t : TypeT) -> Cmd (Expr t)
  DeclareVarsCmd : Traversable f => f String -> (t : TypeT) -> Cmd (f (Expr t))
  AssertCmd : Expr BoolT -> Cmd ()
  CheckSatCmd : Cmd ()
  GetModelCmd : Cmd ()
  SetOptionCmd : String -> Cmd ()
  SetLogicCmd : String -> Cmd ()

data Smt : Type -> Type where
  Pure : a -> Smt a
  Bind : Cmd a -> (a -> Smt b) -> Smt b

pure : a -> Smt a
pure x = Pure x

(>>=) : Smt a -> (a -> Smt b) -> Smt b
(>>=) (Pure x) f = f x
(>>=) (Bind cmd g) f = Bind cmd (\x => g x >>= f)

end : Smt ()
end = Pure ()

declareVar : String -> (t : TypeT) -> Smt (Expr t)
declareVar v t = Bind (DeclareVarCmd v t) pure

declareVars : Traversable f => f String -> (t : TypeT) -> Smt (f (Expr t))
declareVars vs t = Bind (DeclareVarsCmd vs t) pure

assert : Expr BoolT -> Smt ()
assert e = Bind (AssertCmd e) pure

checkSat : Smt ()
checkSat = Bind CheckSatCmd pure

getModel : Smt ()
getModel = Bind GetModelCmd pure

setOption : String -> Smt ()
setOption s = Bind (SetOptionCmd s) pure

setLogic : String -> Smt ()
setLogic s = Bind (SetLogicCmd s) pure

compileExpr : Expr t -> String
compileExpr (VarExpr x t) = x
compileExpr (BoolExpr x) = if x then "true" else "false"
compileExpr (BvExpr x n) = "(_ bv" ++ show x ++ " " ++ show n ++ ")"
compileExpr (IntExpr x) = show x
compileExpr (RealExpr x) = show x
compileExpr (BvAddExpr l r) = "(bvadd " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvMulExpr l r) = "(bvmul " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSDivExpr l r) = "(bvsdiv " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSModExpr l r) = "(bvsmod " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvUDivExpr l r) = "(bvudiv " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvURemExpr l r) = "(bvurem " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvShLExpr l r) = "(bvshl " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvLShRExpr l r) = "(bvlshr " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvAShRExpr l r) = "(bvashr " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvNegExpr x) = "(bvneg " ++ compileExpr x ++ ")"
compileExpr (BvAndExpr l r) = "(bvand " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSubExpr l r) = "(bvsub " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvOrExpr l r) = "(bvor " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvXorExpr l r) = "(bvxor " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvNotExpr x) = "(bvnot " ++ compileExpr x ++ ")"
compileExpr (BvULeExpr l r) = "(bvule " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvULtExpr l r) = "(bvult " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvUGeExpr l r) = "(bvuge " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvUGtExpr l r) = "(bvugt " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSLeExpr l r) = "(bvsle " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSLtExpr l r) = "(bvslt " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSGeExpr l r) = "(bvsge " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvSGtExpr l r) = "(bvsgt " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (AddExpr xs) = "(+ " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (MinusExpr xs) = "(- " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (MulExpr xs) = "(* " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (EqualExpr l r) = "(= " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (DistinctExpr xs) = "(distinct " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (LessExpr l r) = "(< " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (LessOrEqualExpr l r) = "(<= " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (GreaterExpr l r) = "(> " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (GreaterOrEqualExpr l r) = "(>= " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (AndExpr xs) = "(and " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (OrExpr xs) = "(or " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (NotExpr x) = "(not " ++ compileExpr x ++ ")"
compileExpr (ImpExpr l r) = "(=> " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (IteExpr p l r) = "(if " ++ compileExpr p ++ " " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"

compileCmd : Cmd a -> (a, String)
compileCmd (DeclareVarCmd x t) = (VarExpr x t, "(declare-const " ++ x ++ " " ++ show t ++ ")")
compileCmd (DeclareVarsCmd xs t) = (map (\x => VarExpr x t) xs,
                                    (unlines . toList . map (\x => "(declare-const " ++ x ++ " " ++ show t ++ ")")) xs)
compileCmd (AssertCmd e) = ((), "(assert " ++ compileExpr e ++ ")")
compileCmd CheckSatCmd = ((), "(check-sat)")
compileCmd GetModelCmd = ((), "(get-model)")
compileCmd (SetOptionCmd s) = ((), "(set-option " ++ s ++ ")")
compileCmd (SetLogicCmd s) = ((), "(set-logic " ++ s ++ ")")

compile : Smt () -> String
compile smt = unlines $ compile' smt
  where
    compile' : Smt () -> List String
    compile' (Pure ()) = [""]
    compile' (Bind cmd f) = let (a, s) = compileCmd cmd in
                           let s' = compile' $ f a in
                           s :: s'

example0 : Expr BoolT
example0 = (bool True) && (bool True)

example1 : Expr BoolT
example1 = (bv 1 8) == (bv 1 8)

example2 : Smt ()
example2 = checkSat

example3 : Smt ()
example3 = do x <- declareVar "x" BoolT
              y <- declareVar "y" BoolT
              assert $ x && y
              checkSat
              getModel
              end

example4 : Smt ()
example4 = do [x, y] <- declareVars {f = Vect 2} ["x", "y"] BoolT
              assert $ not (x && y) == (not x || not y)
              checkSat
              getModel
              end

exec : String -> String -> IO Int
exec input output = system $ "z3 -smt2 " ++ input ++ " > " ++ output

data Result = Sat | UnSat | Unknown

Show Result where
  show Sat = "sat"
  show UnSat = "unsat"
  show Unknown = "unknown"

Model : Type
Model = List (String, String)

parseResult : List String -> Maybe (Result, List String)
parseResult ("sat" :: "(model " :: xs) = Just (Sat, xs)
parseResult ("unsat" :: xs) = Just (UnSat, xs)
parseResult ("unknown" :: xs) = Just (Unknown, xs)
parseResult _ = Nothing

parseVar : List Char -> Maybe (List Char)
parseVar ('(' :: 'd' :: 'e' :: 'f' :: 'i' :: 'n' :: 'e' :: '-' :: 'f' :: 'u' :: 'n' :: ' ' :: xs) = parseVar' xs
  where
    parseVar' : List Char -> Maybe (List Char)
    parseVar' (' ' :: xs) = Just []
    parseVar' (x :: xs) = do xs <- parseVar' xs
                             Just (x :: xs)
    parseVar' _ = Nothing
parseVar _ = Nothing

parseValue' : List Char -> Maybe (List Char)
parseValue' [] = Just []
parseValue' (')' :: _) = Just []
parseValue' (' ' :: _) = Just []
parseValue' [_] = Nothing
parseValue' (x :: xs) = do xs <- parseValue' xs
                           Just (x :: xs)

parseValue : List Char -> Maybe (List Char)
parseValue ('(' :: '_' :: ' ' :: 'b' :: 'v' :: xs) = parseValue' xs
parseValue xs = parseValue' xs

parseModel : List String -> Maybe (Model, List String)
parseModel [")"] = Just ([], [])
parseModel (x :: y :: xs) = do (model, xs) <- parseModel xs
                               var <- parseVar (unpack (ltrim x))
                               value <- parseValue (unpack (ltrim y))
                               Just ((pack var, pack value) :: model, xs)
parseModel _ = Nothing

sat : Smt () -> IO (Maybe (Result, Model))
sat smt = do _ <- writeFile "input.smt2" $ compile smt
             putStrLn "z3 solving"
             _ <- exec "input.smt2" "output.smt2"
             r <- readFile "output.smt2"
             case r of
               Left err => do printLn err; pure Nothing
               Right str => let r = parseResult $ filter (\line => not $ line == "") $ lines str in
                            case r of
                              Nothing => do putStrLn "Error parsing result"; pure Nothing
                              Just (Sat, xs) => let r = parseModel xs in
                                                case r of
                                                  Nothing => do putStrLn "Error parsing model"; pure Nothing
                                                  Just (model, xs) => pure $ Just (Sat, model)
                              Just (UnSat, xs) => pure $ Just (UnSat, [])
                              Just (Unknown, xs) => pure $ Just (Unknown, [])

print : Smt () -> IO ()
print smt = putStrLn $ compile smt

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Data.ArrayLike

import Decidable.Equality

%default total

infix 7 !!

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

public export
interface ArrayLike arr where
  elemType : Type
  length : arr -> Int
  findByV : (elemType -> Bool) -> (xs:arr)
         -> Maybe (i:Int ** (0 <= i = True, i < length xs = True))
  findrByV : (elemType -> Bool) -> (xs:arr)
          -> Maybe (i:Int ** (0 <= i = True, i < length xs = True))

  (!!) : (xs:arr) -> (i:Int)            -- WHY THE HELL THIS CANN'T IMPLEMENT
      -> {auto _: 0 <= i = True }
      -> {auto _: i < length xs = True }
      -> elemType

  findBy : (elemType -> Bool) -> (xs:arr) -> Maybe Int
  findBy f xs with (findByV f xs)
    findBy f xs | Nothing = Nothing
    findBy f xs | Just (i ** _) = Just i

  findrBy : (elemType -> Bool) -> (xs:arr) -> Maybe Int
  findrBy f xs with (findrByV f xs)
    findrBy f xs | Nothing = Nothing
    findrBy f xs | Just (i ** _) = Just i

at' : ArrayLike arr => Int -> arr -> Maybe (elemType{arr=arr})
at' i xs with (decEq (0 <= i) True, decEq (i < length xs) True)
  at' i xs | (Yes pr0, Yes pr1) = Just $ xs !! i
  at' i xs | _ = Nothing

-- ---------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :

ext: idr


text:
module PrimIO

import Builtin

%default total

public export
data IORes : Type -> Type where
     MkIORes : (result : a) -> (1 x : %World) -> IORes a

||| Idris's primitive IO, for building abstractions on top of.
public export
PrimIO : Type -> Type
PrimIO a = (1 x : %World) -> IORes a

export
data IO : Type -> Type where
     MkIO : (1 fn : PrimIO a) -> IO a

export
prim__io_pure : a -> PrimIO a
prim__io_pure = MkIORes

%inline
export
io_pure : a -> IO a
io_pure x = MkIO (MkIORes x)

export
prim__io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b
prim__io_bind fn k w
    = let MkIORes x' w' = fn w in k x' w'

-- There's a special case for inlining this is Compiler.Inline, because
-- the inliner is cautious about case blocks at the moment. Once it's less
-- cautious, add an explicit %inline directive and take out the special case.
-- See also dealing with the newtype optimisation via %World in
-- Compiler.CompileExpr
export
io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
io_bind (MkIO fn) k
    = MkIO (\w => let MkIORes x' w' = fn w
                      MkIO res = k x' in
                      res w')

-- A pointer representing a given parameter type
-- The parameter is a phantom type, to help differentiate between
-- different pointer types
public export
data Ptr : Type -> Type where [external]

-- A pointer to any type (representing a void* in foreign calls)
public export
data AnyPtr : Type where [external]

-- As Ptr, but associated with a finaliser that is run on garbage collection
public export
data GCPtr : Type -> Type where [external]

-- As AnyPtr, but associated with a finaliser that is run on garbage collection
public export
data GCAnyPtr : Type where [external]

public export
data ThreadID : Type where [external]

export %inline
fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
fromPrim op = MkIO op

export %inline
toPrim : (1 act : IO a) -> PrimIO a
toPrim (MkIO fn) = fn

%foreign "C:idris2_isNull, libidris2_support, idris_support.h"
         "javascript:lambda:x=>x===undefined||x===null?1:0"
         "jvm:isNull,io/github/mmhelloworld/idrisjvm/runtime/Objects"
export
prim__nullAnyPtr : AnyPtr -> Int

%foreign "C:idris2_getNull, libidris2_support, idris_support.h"
export
prim__getNullAnyPtr : AnyPtr

export
prim__castPtr : AnyPtr -> Ptr t
prim__castPtr = believe_me

export
prim__forgetPtr : Ptr t -> AnyPtr
prim__forgetPtr = believe_me

export %inline
prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)

unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
unsafeCreateWorld f = f %MkWorld

unsafeDestroyWorld : (1 x : %World) -> a -> a
unsafeDestroyWorld %MkWorld x = x

export
unsafePerformIO : IO a -> a
unsafePerformIO (MkIO f)
    = unsafeCreateWorld (\w => case f w of
                               MkIORes res w' => unsafeDestroyWorld w' res)


text:
module Test.Spec

import Specdris.Spec
import Data.Functor.Foldable
import Data.Vect
import Control.Comonad.Cofree

-- FIXME morphisms with constraints? particularly re: symmteries
-- "safe" compilation using this?
-- particularly discrete pseudo-hamiltonian dynamics
-- oh man finite symplectic geometry

-- TODO computation of pi from http://www.cs.ox.ac.uk/jeremy.gibbons/publications/metamorphisms-mpc.pdf

naturals : Nat -> ListF Nat Nat
naturals Z = NilF
naturals (S n) = Cons (n + 1) n

-- This is also an instructive use of cofree comonads!
-- Do note that it indexes starting at 0.
catalan : Nat -> Nat
catalan = dyna coalgebra naturals
  where
    coalgebra : ListF Nat (Cofree (ListF Nat) Nat) -> Nat
    coalgebra NilF = 1
    coalgebra (Cons n table) = sum (Prelude.List.zipWith (*) xs (reverse xs))
      where
        xs = take n table
        take : Nat -> (Cofree (ListF Nat) Nat) -> List Nat
        take Z _ = []
        take (S n) (Co a NilF) = [a]
        take (S n) (Co a (Cons v as)) = a :: take n as

roundedSqrt : Nat -> Nat
roundedSqrt = cast . cast {to=Integer} . sqrt . cast

toN : Nat -> List Nat
toN = reverse . ana naturals

isPrime : Nat -> List Nat -> Bool
isPrime n ns = all (\a => mod n a /= 0) (filter (<= (roundedSqrt n)) ns)

dedup : (Eq a) => List a -> List a
dedup = para pseudoalgebra where
  pseudoalgebra : (Eq a) => ListF a (List a, List a) -> List a
  pseudoalgebra NilF                 = []
  pseudoalgebra (Cons x (past, xs))  = if elem x past then xs else x :: xs

evenOdd : Nat -> Bool
evenOdd = mutu odd even where
  odd : Maybe (Bool, Bool) -> Bool
  odd Nothing = False
  odd (Just (_, b)) = b
  even : Maybe (Bool, Bool) -> Bool
  even Nothing = True
  even (Just (_, b)) = b

collatzCoalgebra : Int -> Either (List Int) (ListF Int Int)
collatzCoalgebra 1 = Left [1]
collatzCoalgebra 2 = Left [2, 1]
collatzCoalgebra 3 = Left [3, 10, 5, 16, 8, 4, 2, 1]
collatzCoalgebra 4 = Left [6, 3, 10, 5, 16, 8, 4, 2, 1]
collatzCoalgebra n with (modInt n 2)
  | 0 = Right $ Cons n (divInt n 2)
  | _ = Right $ Cons n (3 * n + 1)

collatz : Int -> List Int
collatz = micro collatzCoalgebra

elgotCoalgebra : List a -> Either (List (List a)) (ListF (List a) (List a))
elgotCoalgebra [] = Right NilF
elgotCoalgebra (x :: []) = Left ([[x]])
elgotCoalgebra (x :: xs) = Right (Cons (x :: xs) xs)

-- fibonacci zygomorphism?

zygoPseudoalgebra : ListF Int (Bool, Int) -> Int
zygoPseudoalgebra NilF = 0
zygoPseudoalgebra (Cons n (b, x)) = if b then (n+x) else (n-x)

zygoAlgebra : ListF Int Bool -> Bool
zygoAlgebra NilF = False
zygoAlgebra (Cons _ bool) = not bool

plusMinus : List Int -> Int
plusMinus = zygo zygoAlgebra zygoPseudoalgebra

algebra' : ListF (List a) (List a) -> List a
algebra' NilF = []
algebra' (Cons x xs) = x ++ xs

cataConcat : List (List a) -> List a
cataConcat = cata algebra'

algebra : ListF (List a) (List (List a)) ->  List (List a)
algebra NilF = []
algebra (Cons x xs) = x::xs

coalgebra : List a -> ListF (List a) (List a)
coalgebra (x::xs) = Cons (x::xs) xs
coalgebra [] = NilF

suffix : List a -> List (List a)
suffix = hylo algebra coalgebra . drop 1

export
specSuite : IO ()
specSuite =
  spec $ do
    describe "hylo" $
      it "should be able to implement the suffix function" $
        (suffix . unpack) "ego" `shouldBe` [['g','o'], ['o']]
    describe "cata" $
      it "should be able to implement 'concat'" $
      (cataConcat . map unpack) [ "I", "am" ] `shouldBe` ['I', 'a', 'm']
    describe "zygo" $
      it "should be able to implement plusMinus" $
        plusMinus [1,2,3] `shouldBe` -4
    describe "micro" $
      it "should provide a simple way to compute the Collatz sequence associated with a number" $
        collatz 12 `shouldBe` [12, 6, 3, 10, 5, 16, 8, 4, 2, 1]
    describe "mutu" $
      it "should be able to do recursion on the natural numbers to check for parity" $
        (evenOdd . fromIntegerNat) 10 `shouldBe` True
    describe "para" $
      it "should provide an elegant way to remove duplicates from a list when order doesn't matter" $
        dedup [1,1,2,3,4,5,4] `shouldBe` [1,2,3,5,4]
    describe "dyna" $
      it "should do something with catalan numbers" $
        catalan 6 `shouldBe` 132
    describe "ana" $
      it "should give the first n naturals" $
        toN 5 `shouldBe` [1,2,3,4,5]


text:
||| A MonadRef instance with heap and locations indexed by a universe.
module Data.Heap.Untyped

import public Control.Monad.Ref
import        Control.Monad.State
import        Data.Vect
import        Data.Vect.Views

%default total

%hide Language.Reflection.Ref
%hide Language.Reflection.Universe

panic : String -> a
panic = idris_crash

-- Heap ------------------------------------------------------------------------

||| Note we paramentrise over the universe, not the type!
||| Parametrising over the universe will force us to specify that functions or data
||| should all work over *the same universe implementation* not only the same universe type!!!
export
data Loc : (u : Universe t) -> (e : t) -> Type where
  MkLoc : Nat -> Loc u e

||| Heap consisting of a list of type and element pairs over a universe.
Heap : (u : Universe t) -> Type
Heap {t} _ = ( n : Nat ** Vect n (e : t ** typeOf e) )

||| An empty heap over a universe.
empty : Heap u
empty = (0 ** [])

sub : (n : Nat) -> (m : Nat) -> Fin n
sub n m =
  case isLTE m n of
    Yes prf => case natToFin (n - m) n of
      Just k  => k
      Nothing => panic "Index is out of bounds, this should not happen"
    No cont => panic "Index is bigger than vector length, this should not happen"

extend : Monad m => {u : Universe t} -> typeOf e -> StateT (Heap u) m (Loc u e)
extend {e} x = do
  ( n ** xs ) <- get
  put ( S n ** ( e ** x ) :: xs )
  pure $ MkLoc n

update : Monad m => {u : Universe t} -> Loc u e -> typeOf e -> StateT (Heap u) m ()
update (MkLoc {e} i) y = do
  ( n ** xs ) <- get
  put $ ( n ** Vect.replaceAt (sub n i) ( e ** y ) xs )

lookup : Monad m => {u : Universe t} -> Loc u e -> StateT (Heap u) m (typeOf e)
lookup (MkLoc {e} i) = do
    ( n ** xs ) <- get
    let ( e' ** x ) = Vect.index (sub n i) xs
    case decEq e e' of
      Yes Refl => pure x
      No contr => panic "Types of location and cell do not match, this should not happen"

-- Transformer -----------------------------------------------------------------

export
data RefT : (u : Universe t) -> (m : Type -> Type) -> (a : Type) -> Type where
  Pure  : (x : a) -> RefT u m a
  Bind  : (this : RefT u m a) -> (next : a -> RefT u m b) -> RefT u m b

  New   : (x : typeOf @{u} e) -> RefT u m (Loc u e)
  Read  : (l : Loc u e) -> RefT u m (typeOf @{u} e)
  Write : (l : Loc u e) -> (x : typeOf @{u} e) -> RefT u m ()

public export
Ref : (u : Universe t) -> (a : Type) -> Type
Ref u = RefT u Identity

-- Running ---------------------------------------------------------------------

export
runRefT : Monad m => RefT u m a -> m a
runRefT r = fst <$> runStateT (go r) empty
where
  go : Monad m => RefT u m a -> StateT (Heap u) m a
  go (Pure x) =
      pure x
  go (Bind this next) = do
      x <- go this
      go $ next x
  go (New x) = do
      l <- extend x
      pure l
  go (Read l) = do
      x <- lookup l
      pure x
  go (Write l x) = do
      update l x

-- Interfaces ------------------------------------------------------------------
--NOTE: These are just the free monad implementations

Functor (RefT u m) where
    map f m = Bind m (Pure . f)

Applicative (RefT u m) where
    pure = Pure

    f <*> x = Bind f (\f => map f x)

Monad (RefT u m) where
    (>>=) = Bind

MonadRef u (Loc u) (RefT u m) where
    ref    = New
    deref  = Read
    assign = Write

{-------------------------------------------------------------------------------

-------------------------------------------------------------------------------}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Intro
import Data.Vect
-- a term with its type
three: Nat
three = 3

-- next is a term with type the function type `Nat -> Nat`
next: Nat -> Nat
next n = S n

fct: Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k)

fibPair: Nat -> (Nat, Nat)
fibPair Z = (1, 1)
fibPair (S k) = case (fibPair k) of
                     (a, b) => (b, a + b)

fibo: Nat -> Nat
fibo n = fst (fibPair n)

-- Nat is itself a term with type `Type`
naturals: Type
naturals = Nat

-- as is Nat -> Nat
natToNat: Type
natToNat = Nat -> Nat

-- functions of two variables can be viewed as iterated functions by Currying
add: Nat -> Nat -> Nat
add k j = k + j

-- we can define inductive types by listing all intro rules. `BinTree` is a type
data BinTree: Type where
  Leaf: BinTree
  Node : (left: BinTree) -> (right: BinTree) -> BinTree

vertices: BinTree -> Nat
vertices Leaf = 1
vertices (Node left right) = (vertices left) + (vertices right)

-- We have labelled trees, which depend on a type.
data LTree: Type -> Type where
  LLeaf : (a: Type) -> (label: a) -> LTree a
  LNode : (a: Type) -> (left: LTree a) -> (right: LTree a) -> LTree a

vertexList: (a: Type) -> LTree a -> List a
vertexList a (LLeaf a label) = [label]
vertexList a (LNode a left right) = (vertexList a left) ++ (vertexList a right)

-- a type family
Tuple: Nat -> Type
Tuple Z = Unit
Tuple (S k) = (Nat, Tuple k)

--- countdown is a dependent function, and its type is a Pi-Type
countdown: (n: Nat) -> Tuple n
countdown Z = ()
countdown (S k) = ((S k), countdown k)

cntd : (n: Nat) -> Vect (S n) Nat
cntd Z = [0]
cntd (S k) = (S k) :: (cntd k)

append: (n: Nat) -> (a: Type) -> Vect n a -> a -> Vect (S n) a
append Z a [] x = x :: []
append (S len) a (y :: xs) x = y :: (append len a xs x)

reverse: (n: Nat) -> (a: Type) -> Vect n a -> Vect n a
reverse Z a [] = []
reverse (S len) a (x :: xs) = append len a (reverse len a xs) x

zip : (n: Nat) -> (a: Type) -> (b: Type) -> Vect n a -> Vect n b -> Vect n (a, b)
zip Z a b [] [] = []
zip (S len) a b (x :: xs) (y :: ys) = (x, y) :: (zip _ _ _ xs ys)

filter : (n: Nat) -> (a: Type) -> (vec: Vect n a) -> (p: a -> Bool) -> (m: Nat ** Vect m a)
filter Z a [] condition = (Z ** [])
filter (S len) a (x :: xs) p =
  case filter len a xs p of
        (m ** pf) => if (p x) then (S m ** x :: pf) else (m ** pf)

max_stars_repo_name: siddhartha-gadgil/TrainLogic

max_issues_repo_name: siddhartha-gadgil/TrainLogic

max_forks_repo_name: siddhartha-gadgil/TrainLogic


text:
module Mult

import public Nat

public export
mult : Nat -> Nat -> Nat
mult Z y = Z
mult (S k) y = plus y (mult k y)


text:
module Main

interface Symantics (repr : Type -> Type) where
  int : Int -> repr Int
  bool : Bool -> repr Bool
  string : String -> repr String
  nil : repr (List a)
  not : repr Bool -> repr Bool
  (==) : Eq a => repr a -> repr a -> repr Bool
  (*) : Num a => repr a -> repr a -> repr a
  lam : (repr a -> repr b) -> repr (a -> b)
  app : repr (a -> b) -> repr a -> repr b
  foreach : Lazy (repr (List a)) -> (repr a -> repr (List b)) -> repr (List b)
  where' : repr Bool -> Lazy (repr (List a)) -> repr (List a)
  yield : repr a -> repr (List a)
  union_all : repr (List a) -> repr (List a) -> repr (List a)

record Product where
  constructor MkProduct
  pid : Int
  name : String
  price : Int

record Order where
  constructor MkOrder
  oid : Int
  opid : Int
  qty : Int

record Sale where
  constructor MkSale
  spid : Int
  sname : String
  amount : Int

interface Symantics repr => SymSchema (repr : Type -> Type) where
  product : repr Int -> repr String -> repr Int -> repr Product
  pid : repr Product -> repr Int
  name : repr Product ->  repr String
  price : repr Product -> repr Int
  products : Lazy (repr (List Product))

  order : repr Int -> repr Int -> repr Int -> repr Order
  oid : repr Order -> repr Int
  opid : repr Order -> repr Int
  qty : repr Order -> repr Int
  orders : Lazy (repr (List Order))

  sale : repr Int -> repr String -> repr Int -> repr Sale

listFive : Symantics r => r (List Int)
listFive = yield (int 5)

-- products
tablet : SymSchema r => r Product
tablet = product (int 1) (string "Tablet") (int 500)
laptop : SymSchema r => r Product
laptop = product (int 2) (string "Laptop") (int 1000)
desktop : SymSchema r => r Product
desktop = product (int 3) (string "Desktop") (int 1000)
router : SymSchema r => r Product
router = product (int 4) (string "Router") (int 150)
hdd : SymSchema r => r Product
hdd = product (int 5) (string "HDD") (int 100)
ssd : SymSchema r => r Product
ssd = product (int 6) (string "SSD") (int 500)

-- orders
o1 : SymSchema r => r Order
o1 = order (int 1) (int 1) (int 5)
o2 : SymSchema r => r Order
o2 = order (int 1) (int 2) (int 5)
o3 : SymSchema r => r Order
o3 = order (int 1) (int 4) (int 2)
o4 : SymSchema r => r Order
o4 = order (int 2) (int 5) (int 10)
o5 : SymSchema r => r Order
o5 = order (int 2) (int 6) (int 20)
o6 : SymSchema r => r Order
o6 = order (int 3) (int 2) (int 50)

data Evaluator a = R a

eval : Evaluator a -> a
eval (R a) = a

Symantics Evaluator where
  int = R
  bool = R
  string = R
  not (R b) = R (not b)
  nil = R []
  (==) (R a) (R b) = R (a == b)
  (*) (R a) (R b) = R (a * b)
  lam f = R (\a => eval (f (R a)))
  app (R f) (R a) = R (f a)
  foreach t f =
    case eval t of
      []        => R []
      (x :: xs) => R (eval (f (R x)) ++ (eval (foreach (R xs) f)))
  where' (R b) r = if b then r else R []
  yield (R x) = R [x]
  union_all (R as) (R bs) = R (as ++ bs)

Symantics Evaluator => SymSchema Evaluator where
  product (R pid) (R name) (R price) = R (MkProduct pid name price)
  pid (R p) = R (pid p)
  name (R p) = R (name p)
  price (R p) = R (price p)
  products = R (map eval [tablet, laptop, desktop, router, hdd, ssd]) -- yield tablet `union_all` yield laptop

  order (R oid) (R opid) (R qty) = R (MkOrder oid opid qty)
  oid (R o) = R (oid o)
  opid (R o) = R (opid o)
  qty (R o) = R (qty o)
  orders = R (map eval [o1, o2, o3, o4, o5, o6])

  sale (R spid) (R sname) (R amount) = R (MkSale spid sname amount)

-- eval (foreach products (\p => yield (pid p)) `union_all` foreach orders (\o => yield (opid o)))

-- Q1
q1 : SymSchema r => r Int -> r (List Order)
q1 xoid = foreach orders $ \o =>
            where' (oid o == xoid) $
              yield o

q1_2 : SymSchema r => r (List Order)
q1_2 = q1 (int 2) -- I'm not using `app` and `lam` anywhere. Is that a problem?

-- eval q1_2

q2 : SymSchema r => r Order -> r (List Sale)
q2 o = foreach products $ \p =>
         where' (not (not (pid p == opid o))) $
           yield $ sale (pid p) (name p) (price p * qty o)

-- eval (q2 (order (int 2) (int 5) (int 10)))
q3 : SymSchema r => r Int -> r (List Sale)
q3 x = foreach (q1 x) $ \y =>
         q2 y
-- Still no app and lam... Oleg et. al. use app, but no lam either

-- eval (q3 (int 2))

data Printer a = P String

print : Printer a -> String
print (P a) = a

Symantics Printer where
  int i = P (show i)
  bool b = P (show b)
  string s = P s
  not (P b) = P ("(NOT " ++ b ++ ")")
  nil = P "[]"
  (==) (P a) (P b) = P (a ++ " == " ++ b)
  (*) (P a) (P b) = P ("(" ++ a ++ " * " ++ b ++ ")")
  lam f = P "lam"
  app (P f) (P a) = P "app"
  foreach t f =
    let ts : String = print t
        fs : String = print (f (P "$arg"))
    in P ("FOREACH (" ++ ts ++ ") " ++ fs)
  where' (P b) r = P ("WHERE " ++ b ++ " " ++ (print r))
  yield (P x) = P ("YIELD " ++ x)
  union_all (P as) (P bs) = P (as ++ " UNION ALL " ++ bs)

Symantics Printer => SymSchema Printer where
  product _ _ _ = P "product"
  pid (P x) = P (x ++ ".pid")
  name (P x) = P (x ++ ".name")
  price (P x) = P (x ++ ".price")
  products = P "products"
  order x y z = P "order"
  oid (P x) = P (x ++ ".oid")
  opid (P x) = P (x ++ ".pid")
  qty (P x) = P (x ++ ".qty")
  orders = P "orders"
  sale x y z = P $ "(MkSale " ++ print x ++ " " ++ print y ++ " " ++ print z ++ ")"

-- λΠ> print (q3 (int 2))
-- "FOREACH (FOREACH (orders) WHERE $arg.oid == 2 YIELD $arg) FOREACH (products) WHERE $arg.pid == $arg.pid YIELD (MkSale $arg.pid $arg.name ($arg.price * $arg.qty))" : String

data ConstantFolder : (repr : Type -> Type) -> (a : Type) -> Type where
  Empty : ConstantFolder repr (List a)
  Unknown : (repr a) -> ConstantFolder repr a

dyn : Symantics repr => ConstantFolder repr a -> repr a
dyn Empty = nil
dyn (Unknown x) = x

Symantics r => Symantics (ConstantFolder r) where
  nil = Empty
  union_all Empty y = y
  union_all (Unknown x) y = Unknown (union_all x (dyn y))
  -- boilerplate
  int x = Unknown (int x)
  bool x = Unknown (bool x)
  string x = Unknown (string x)
  not b = Unknown (not (dyn b))
  lam f = Unknown (lam (\x => dyn (f (Unknown x))))
  app x y = Unknown (app (dyn x) (dyn y))
  foreach t f = Unknown $ foreach (Delay (dyn t)) (\x => dyn (f (Unknown x)))
  where' x y = Unknown (where' (dyn x) (dyn y))
  yield x = Unknown (yield (dyn x))
  (==) x y = Unknown (dyn x == dyn y)
  (*) x y = Unknown (dyn x * dyn y)

SymSchema r => SymSchema (ConstantFolder r) where
-- (Symantics (ConstantFolder r), SymSchema r) => SymSchema (ConstantFolder r) where
  product x y z = Unknown $ product (dyn x) (dyn y) (dyn z)
  pid = pid
  name = name
  price = price
  products = products
  order = order
  oid = oid
  opid = opid
  qty = qty
  orders = Unknown $ Force orders -- not sure I like this Force
  sale = sale

cfp' : ConstantFolder Printer (List Int)
cfp' = union_all nil (yield (int 2))

-- print (dyn (union_all nil (yield (int 2))))

-- From http://okmij.org/ftp/tagless-final/course/RR.hs
--
-- {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

-- -- * Reflection-Reification pair

-- module RR where

-- class RR t repr where
--   fwd :: repr a -> t repr a
--   bwd :: t repr a -> repr a

--   map1 :: (repr a -> repr b) -> (t repr a -> t repr b)
--   map1 f = fwd . f . bwd

--   map2 :: (repr a -> repr b -> repr c) ->
--           (t repr a -> t repr b -> t repr c)
--   map2 f e1 e2 = fwd (f (bwd e1) (bwd e2))

-- -- * fwd is generally not surjective and bwd is not injective
-- -- * bwd . fwd == id,  fwd . bwd /= id

-- -- * QUIZ
-- -- * map1 looks like fmap of a Functor. Can it be defined or related
-- -- * to Functor?

interface RR (t : (Type -> Type) -> Type -> Type) (repr : Type -> Type) where
  fwd : repr a -> t repr a
  bwd : t repr a -> repr a

  map1 : (repr a -> repr b) -> (t repr a -> t repr b)
  map1 f = fwd . f . bwd

  map2 : (repr a -> repr b -> repr c) -> (t repr a -> t repr b -> t repr c)
  map2 f e1 e2 = fwd (f (bwd e1) (bwd e2))

-- print (q_3 (int 2))

data N2N : (repr : Type -> Type) -> (a : Type) -> Type where
  Unk : repr a -> N2N repr a           -- no annotation
  Neg : repr Bool -> N2N repr Bool     -- it is a negation

-- instance Symantics repr => RR N2N repr where
--   bwd (Unk e) = e
--   bwd (Neg x) = neg x

--   fwd = Unk

Symantics repr => RR N2N repr where
  bwd (Unk e) = e
  bwd (Neg x) = not x

  fwd = Unk

-- instance Symantics repr => Symantics (N2N repr) where
--   lit = fwd . lit

--   neg (Unk e) = Neg e                   -- we statically know we negated
--   neg (Neg x) = Unk x

--   -- and e1 e2 = Unk $ and (bwd e1) (bwd e2)
--   and = map2 and
--   or  = map2 or

Symantics repr => Symantics (N2N repr) where
  bool = fwd . bool

  not (Unk e) = Neg e                   -- we statically know we negated
  not (Neg x) = Unk x

  int = fwd . int
  string = fwd . string
  (==) = map2 (==)
  (*) = map2 (*)
  nil = fwd nil
  lam f = fwd (lam (\x => bwd (f (fwd x))))
  app = map2 app
  foreach x f = fwd $ foreach (bwd x) (\x => bwd (f (fwd x)))
  where' x y = fwd $ where' (bwd x) (bwd y)
  yield = map1 yield -- not sure..
  union_all = map2 union_all

-- instance SymInput repr => SymInput (N2N repr) where
--   wireX = fwd wireX
--   wireY = fwd wireY
--   wireZ = fwd wireZ

SymSchema r => SymSchema (N2N r) where
  product x y z = fwd $ product (bwd x) (bwd y) (bwd z)
  pid = map1 pid
  name = map1 name
  price = map1 price
  products = fwd $ Force products
  order x y z = fwd $ order (bwd x) (bwd y) (bwd z)
  oid = map1 oid
  opid = map1 opid
  qty = map1 qty
  orders = fwd $ Force orders
  sale x y z = fwd $ sale (bwd x) (bwd y) (bwd z)

-- -- * Observe the result
-- -- A type-specific version of bwd
-- obsN2N :: Symantics repr => N2N repr a -> repr a
-- obsN2N = bwd
obsN2N : Symantics repr => N2N repr a -> repr a
obsN2N = bwd

-- print (obsN2N (q3 (int 2)))

max_stars_repo_name: fehrenbach/furry-parakeet

max_issues_repo_name: fehrenbach/furry-parakeet

max_forks_repo_name: fehrenbach/furry-parakeet


text:
module Examples.Auction

import Data.Vect
import Data.Vect.Quantifiers

import DepSec.Labeled
import DepSec.DIO
import DepSec.Declassification

import Examples.TwoPointLattice

%default total
%access export

--------------------------------------------------------------------------------
--- Auction Hatch Example
--------------------------------------------------------------------------------
Bid : Type
Bid = (String, Nat)

BidLog : Nat -> Type
BidLog n = Vect n (Labeled H Bid)

data MaxL : Bid -> Labeled H Bid -> Type where
  IsMaxL : (b1 : Bid)
        -> (b2 : Labeled H Bid)
        -> (b : Bid ** (maximum (snd b1) (snd b) = (snd b1), label b = b2))
        -> MaxL b1 b2

data MaxBid : Bid -> BidLog n -> Type where
  IsMax : (bid : Bid)
       -> (bids : BidLog n)
       -> All (\b => MaxL bid b) bids
       -> MaxBid bid bids

HighestBid : BidLog _ -> Bid -> Type
HighestBid = \rec, b => (Elem (label b) rec, MaxBid b rec)

HighestBidHatch : BidLog _ -> Type
HighestBidHatch rec = Labeled H (b : Bid ** HighestBid rec b) -> Labeled L Bid

HatchPair : Nat -> Type
HatchPair n = (rec : BidLog n ** Labeled H (b : Bid ** HighestBid rec b) -> Labeled L Bid)

aHatchPair : HatchPair 2
aHatchPair =
  let rec : BidLog 2 = [(label ("Alice", 1337)), (label ("Bob", 1336))]
  in predicateHatch rec HighestBid

printBid : Labeled L Bid -> DIO L ()
printBid (MkLabeled (n, b)) = lift $ putStrLn n

--------------------------------------------------------------------------------
-- UTCB
--------------------------------------------------------------------------------
-- Lemmas
--------------------------------------------------------------------------------
maximum_trans : maximum a c = a -> maximum b a = b -> maximum b c = b
maximum_trans {a} {b} {c} prf prf1 =
  rewrite sym prf1 in
  rewrite sym $ maximumAssociative b a c in
  rewrite sym prf in Refl

maximum_inj : (maximum (S a) (S b) = (S a) -> Void) -> (maximum a b = a -> Void)
maximum_inj {a} {b} f prf =
  void $ f (rewrite prf in Refl)

maximum_l_void : (maximum a b = a -> Void) -> maximum a b = b
maximum_l_void {a = Z} {b = b} f = Refl
maximum_l_void {a = (S k)} {b = Z} f = void $ f Refl
maximum_l_void {a = (S k)} {b = (S j)} f =
  let ihPrf = maximum_inj {a = k} {b = j} f
      ih : (maximum k j = j) = maximum_l_void ihPrf
  in rewrite ih in Refl

all_max_ext : {b1, b2 : Bid}
      -> All (\b => MaxL b2 b) bs
      -> maximum (snd b1) (snd b2) = (snd b1)
      -> All (\b => MaxL b1 b) bs
all_max_ext [] prf = []
all_max_ext {bs = x :: _} {b1} (y :: z) prf =
  let (IsMaxL _ x (c ** (d, e))) = y
  in  (IsMaxL b1 x (c ** (maximum_trans d prf, e))) :: all_max_ext z prf

maxBid_ext : {b1, b2 : Bid}
     -> maximum (snd b1) (snd b2) = (snd b1)
     -> MaxBid b2 bs
     -> MaxBid b1 ((label b1) :: bs)
maxBid_ext {b1} {b2} {bs} maxPrf maxbid =
  let (IsMax _ _ maxbidAll) = maxbid
      headPrf = IsMaxL b1 (label b1) (b1 ** (maximumIdempotent (snd b1), Refl))
      tailPrf = all_max_ext maxbidAll maxPrf
  in IsMax b1 ((label b1) :: bs) (headPrf :: tailPrf)

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

auction : HatchPair n -> DIO L (Labeled L Bid)
auction ([] ** _) = pure $ label ("no bid", 0)
auction (r :: rs ** hatch) =
     do max <- plug $ getMaxBid (r :: rs)
        let max' : Labeled L Bid = hatch max
        printBid max'
        pure max'
  where
    getMaxBid : (r : BidLog (S n))
             -> DIO H (b : Bid ** HighestBid r b)
    getMaxBid (x :: []) =
      do (x' ** prfx) <- unlabel' x
         let elemPrf : Elem (label x') [x] = rewrite prfx in Here
         let maxlemma = (x' ** (maximumIdempotent (snd x'), prfx))
         let maxPrf : MaxBid x' [x] = IsMax x' [x] ((IsMaxL x' x maxlemma) :: Nil)
         pure (x' ** (elemPrf, maxPrf))
    getMaxBid (x :: y :: zs) =
      do (x' ** prfx) <- unlabel' x
         (tail' ** (prftailElem, prftailMax)) <- getMaxBid (y :: zs)
         let (IsMax _ _ tailprfAll) = prftailMax
         case decEq (maximum (snd x') (snd tail')) (snd x') of
           Yes prf => pure (x' ** (rewrite prfx in Here, rewrite sym prfx in maxBid_ext prf prftailMax))
           No cont => pure (tail' ** (There prftailElem, IsMax tail' (x :: y :: zs)
             ((IsMaxL tail' x (x' ** (
             rewrite maximumCommutative (snd tail') (snd x') in maximum_l_void {b=(snd tail')} cont, prfx))) :: tailprfAll)))

--------------------------------------------------------------------------------
-- TCB
--------------------------------------------------------------------------------
main : IO ()
main =
  do putStrLn "##### Welcome to the auction! #####"
     putStrLn "Announcing winner: "
     max <- run $ auction aHatchPair
     putStrLn "##### Bye bye! #####"
     pure ()

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Hangman

import Data.Vect
import removeElem

data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkWordState : (word : String) -> (missing : Vect letters Char) -> WordState guesses_remaining letters

data Finished : Type where
     Lost : (game : WordState 0 (S letters)) -> Finished
     Won : (game : WordState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
     Letter : (c : Char) -> ValidInput [c]

validNil : ValidInput [] -> Void
validNil (Letter _) impossible

validNotSingle : ValidInput (x :: (y :: xs)) -> Void
validNotSingle (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No $ validNil
isValidInput (x :: []) = Yes $ Letter x
isValidInput (x :: (y :: xs)) = No validNotSingle

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

readGuess : IO (g ** ValidInput g)
readGuess = do putStr "Enter a guess: "
               a <- getLine
               case isValidString a of
                    (Yes prf) => pure (_ ** prf)
                    (No contra) => putStrLn "Please enter a single character" >>= \_ => readGuess

processGuess : (letter : Char) -> WordState (S guesses) (S letters) -> Either (WordState guesses (S letters)) (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
                                                      Yes prf => Right $ MkWordState word $ removeElemAuto letter missing
                                                      No contra => Left $ MkWordState word missing

game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st = do (_ ** Letter c) <- readGuess
                                 case (processGuess c st) of
                                         (Left l) => do putStrLn "Your guess was wrong."
                                                        case guesses of
                                                            Z => pure $ Lost l
                                                            (S k) => game l
                                         (Right r) => do putStrLn "Correct!"
                                                         case letters of
                                                              Z => pure $ Won r
                                                              (S k) => game r

main : IO ()
main = let guessWord = "lambda"
           guessLetters = fromList (unpack guessWord)
           numGuesses = 3 in
        do gameres <- game {guesses=numGuesses-1} (MkWordState guessWord guessLetters)
           case gameres of
                (Lost game) => putStrLn $ "Thou hast lost. The word was: " ++ guessWord
                (Won game) => putStrLn "Congrats, you win!"


text:
||| SipHash24 copied from C [reference implementation](https://github.com/veorq/SipHash/blob/master/siphash.c)
module Data.Hashable.SipHash

import Data.Buffer
import Data.IORef

%default total

%inline
CROUNDS : Nat
CROUNDS = 2

%inline
DROUNDS : Nat
DROUNDS = 4

record State where
    constructor MkState
    v0 : Bits64
    v1 : Bits64
    v2 : Bits64
    v3 : Bits64

%inline
shl : Bits64 -> Bits64 -> Bits64
shl = prim__shl_Bits64

%inline
shr : Bits64 -> Bits64 -> Bits64
shr = prim__shr_Bits64

%inline
bor : Bits64 -> Bits64 -> Bits64
bor = prim__or_Bits64

%inline
xor : Bits64 -> Bits64 -> Bits64
xor = prim__xor_Bits64

%inline
and : Int -> Int -> Int
and = prim__and_Int

%inline
%spec b
rotl : Bits64 -> (b : Bits64) -> Bits64
rotl x b = (x `shl` b) `bor` (x `shr` (64 - b))

||| Make the length the smallest multiple of 8 bytes >= the given number
%inline
fullSize : Int -> Int
fullSize x =
    let left = x `prim__and_Int` 7
     in if (x `prim__and_Int` 7) == 0
        then x
        else x - left + 8

-- %inline
compress : IORef State -> IO ()
compress stref = do
    MkState v0 v1 v2 v3 <- readIORef stref
    let v0 = v0 + v1;
        v1 = v1 `rotl` 13;
        v1 = v1 `xor` v0;
        v0 = v0 `rotl` 32;
        v2 = v2 + v3;
        v3 = v3 `rotl` 16;
        v3 = v3 `xor` v2;
        v0 = v0 + v3;
        v3 = v3 `rotl` 21;
        v3 = v3 `xor` v0;
        v2 = v2 + v1;
        v1 = v1 `rotl` 17;
        v1 = v1 `xor` v2;
        v2 = v2 `rotl` 32;
    writeIORef stref $ MkState v0 v1 v2 v3

-- this could all be in ST, but Buffer doesn't support it
%inline
siphashInit : IO (IORef State)
siphashInit = newIORef $ MkState
    { v0 = 0x736f6d6570736575
    , v1 = 0x646f72616e646f6d
    , v2 = 0x6c7967656e657261
    , v3 = 0x7465646279746573
    }

%inline
%spec count
repeat : (count : Nat) -> IO () -> IO ()
repeat Z _ = pure ()
repeat (S k) act = act >> repeat k act

siphashLoop : IORef State -> Buffer -> Int -> Int -> IO ()
siphashLoop stref buf idx len = if idx >= len
    then pure ()
    else do
        m <- getBits64 buf idx
        repeat CROUNDS $ compress stref
        siphashLoop stref buf (assert_smaller idx $ idx + 8) len

%inline
siphashLeftover : IORef State -> Buffer -> Int -> Int -> Int -> IO Bits64
siphashLeftover stref buf size left idx = do
    x <- getBits64 buf idx
    pure $ x `bor` (cast size `shl` 56)

siphash : Buffer -> IO Bits64
siphash buf = do
    stref <- siphashInit
    size <- fullSize <$> rawSize buf
    siphashLoop stref buf 0 size
    let left = size `and` 7
    b <- siphashLeftover stref buf size (size - left) left
    modifyIORef stref $ record { v3 $= (`xor` b) }
    repeat DROUNDS $ compress stref
    modifyIORef stref $ record { v0 $= (`xor` b) }
    MkState v0 v1 v2 v3 <- readIORef stref
    pure $ (v0 `xor` v1) `xor` (v2 `xor` v3)

export
siphashString : String -> Bits64
siphashString str = unsafePerformIO $ do
    Just buf <- newBuffer $ fullSize $ stringByteLength str
        | Nothing => assert_total $ idris_crash "Error allocating buffer"
    setString buf 0 str
    siphash buf


text:
module Main

import Data.Vect

-- data DataStore: Type -> Type where
--   MkData : (size : Nat) -> (items : Vect size schema) -> DataStore schema

infixr 5 .+.

data Schema = SString
     | SInt
     | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

data DataStore : Type where
  MkData : (schema : Schema) -> (size : Nat) -> (items  : Vect size (SchemaType schema)) -> DataStore

size : DataStore -> Nat
size (MkData schema' size' items') = size'

schema : DataStore -> Schema
schema (MkData schema' _ _) = schema'

items : (store: DataStore) -> Vect (size store) (SchemaType (schema store))
items (MkData _ _ items') = items'

addToStore : (store: DataStore) -> (SchemaType (schema store)) -> DataStore
addToStore (MkData schema size items) newitem = MkData schema _ (addToData items) where
  addToData : Vect old (SchemaType schema) -> Vect (S old) (SchemaType schema)
  addToData [] = [newitem]
  addToData (x :: xs) = x :: addToData xs

display: SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (item1, item2) =
  (display item1) ++ ", " ++ (display item2)

parsePrefix : (schema: Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString x = getQuoted (unpack x) where
  getQuoted : List Char -> Maybe (String, String)
  getQuoted ('"':: xs) = case span (/= '"') xs of
    (quoted, '"':: rest) => Just (pack quoted, ltrim (pack rest))
    _ => Nothing
parsePrefix SInt x = case Prelude.Strings.span isDigit x of
  ("", rest) => Nothing
  (num, rest) => Just (cast num, ltrim rest)
parsePrefix (y .+. z) x = do
  (res1, rest) <- parsePrefix y x
  (res2, rest') <- parsePrefix z rest
  pure ((res1, res2), rest')

parseBySchema : (schema: Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema str = case parsePrefix schema str of
  Just (res, "") => Just res
  Just _ => Nothing
  Nothing => Nothing

getEntry : (pos: Integer) -> (store: DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
  case integerToFin pos (size store) of
    Nothing => Just ("out of range\n", store)
    Just id => Just (display (index id store_items), store)

data Command : Schema -> Type where
  Add : (SchemaType schema) -> Command schema
  Get : Integer -> Command a
  Quit: Command a

parseCommand : (schema: Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" str = case parseBySchema schema str of
  Just restok => Just (Add restok)
  Nothing => Nothing
parseCommand schema "get" val = case all isDigit (unpack val) of
  False => Nothing
  True => Just (Get (cast val))
parseCommand schema "quit" _ = Just Quit
parseCommand _ _ _ = Just Quit

-- processCommand : Command schema -> DataStore -> Maybe (String, DataStore)
-- processCommand (Add x) ds = Just (?show_size, addToStore ds x)
-- processCommand (Get x) ds = getEntry x ds
-- processCommand Quit _ = Nothing

-- processInput : DataStore -> String -> Maybe (String, DataStore)
-- processInput ds s = case parse s of
--   Nothing => Just ("Invalid command " ++ s ++ "\n", ds)
--   Just command => processCommand command ds

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Examples.ConferenceLattice

import public DepSec.Lattice
import Decidable.Equality
import Pruviloj.Derive.DecEq
import Pruviloj.Disjoint
import Pruviloj.Injective

%language ElabReflection
%access public export

data Id : Type where
  Top : Id
  Nat : Nat -> Id
  Bot : Id

Uid : Type
Uid = Id

Sid : Type
Sid = Id

natInjective : (Nat a) = (Nat b) -> a = b
natInjective Refl = Refl

DecEq Id where
  decEq Top Top = Yes Refl
  decEq Top (Nat k) = No (%runElab disjoint)
  decEq Top Bot = No (%runElab disjoint)
  decEq (Nat k) Top = No (%runElab disjoint)
  decEq (Nat k) (Nat j) with (decEq k j)
    | (Yes prf) = Yes $ cong prf
    | (No contra) = No $ \a => contra $ natInjective a
  decEq (Nat k) Bot = No (%runElab disjoint)
  decEq Bot Top = No (%runElab disjoint)
  decEq Bot (Nat k) = No (%runElab disjoint)
  decEq Bot Bot = Yes Refl

Eq Id where
  Top == Top         = True
  Top == (Nat k)     = False
  Top == Bot         = False
  (Nat k) == Top     = False
  (Nat k) == (Nat j) = k == j
  (Nat k) == Bot     = False
  Bot == Top         = False
  Bot == (Nat k)     = False
  Bot == Bot         = True

data Compartment : Type where
  U  : Uid -> Compartment
  A  : Uid -> Sid -> Compartment
  PC : Uid -> Sid -> Compartment

total
joinId : (x, y : Id) -> Id
joinId Top y = Top
joinId (Nat k) Top = Top
joinId (Nat k) (Nat j) with (decEq k j)
  | (Yes _) = Nat k
  | (No _) = Top
joinId (Nat k) Bot = (Nat k)
joinId Bot y = y

total
joinComp : (x , y : Compartment) -> Compartment
joinComp (U x) (U y) = U (joinId x y)
joinComp (U x) (A y z) = A (joinId x y) z
joinComp (U x) (PC y z) = PC y z
joinComp (A x z) (U y) = A (joinId x y) z
joinComp (A x z) (A y w) = A (joinId x y) (joinId z w)
joinComp (A x z) (PC y w) = PC y (joinId z w)
joinComp (PC x z) (U y) = PC x z
joinComp (PC x z) (A y w) = PC x (joinId z w)
joinComp (PC x z) (PC y w) = PC (joinId x y) (joinId z w)

lemma1 : a = b -> joinId (Nat a) (Nat b) = (Nat a)
lemma1 {a} {b} prf with (decEq a b)
  | (Yes x) = Refl
  | (No contra) = void $ contra prf

lemma2 : (a = b -> Void) -> joinId (Nat a) (Nat b) = Top
lemma2 {a} {b} contra with (decEq a b)
  | (Yes prf) = void $ contra prf
  | (No f) = Refl

lemma3 : a = b -> (b = c -> Void) -> a = c -> Void
lemma3 prf contra prf' = contra $ trans (sym prf) prf'

implementation JoinSemilattice Id where
  join = joinId
  associative Top y z = Refl
  associative (Nat k) Top z = Refl
  associative (Nat k) (Nat j) Top with (decEq k j)
    | (Yes prf) = Refl
    | (No contra) = Refl
  associative (Nat k) (Nat j) (Nat i) with (decEq k j, decEq j i)
    | (Yes prf, Yes prf') =
        rewrite lemma1 prf in
        rewrite lemma1 prf' in
        rewrite lemma1 (trans prf prf') in
        lemma1 prf
    | (Yes prf, No contra) =
        rewrite lemma1 prf in
        rewrite lemma2 contra in
        rewrite lemma2 $ lemma3 prf contra in
        Refl
    | (No contra, Yes prf) =
        rewrite lemma2 contra in
        rewrite lemma1 prf in
        lemma2 contra
    | (No contra, No contra') =
        rewrite lemma2 contra in
        rewrite lemma2 contra' in
        Refl
  associative (Nat k) (Nat j) Bot with (decEq k j)
    | (Yes _) = Refl
    | (No _) = Refl
  associative (Nat k) Bot z = Refl
  associative Bot y z = Refl

  commutative Top Top = Refl
  commutative Top (Nat k) = Refl
  commutative Top Bot = Refl
  commutative (Nat k) Top = Refl
  commutative (Nat k) (Nat j) with (decEq k j)
    | (Yes prf) = rewrite lemma1 $ sym prf in cong prf
    | (No contra) = sym $ lemma2 $ negEqSym contra
  commutative (Nat k) Bot = Refl
  commutative Bot Top = Refl
  commutative Bot (Nat k) = Refl
  commutative Bot Bot = Refl

  idempotent Top = Refl
  idempotent (Nat k) with (decEq k k)
    | (Yes _) = Refl
    | (No contra) = void $ contra Refl
  idempotent Bot = Refl

implementation BoundedJoinSemilattice Id where
  Bottom = Bot

  unitary Top = Refl
  unitary (Nat k) = Refl
  unitary Bot = Refl

implementation JoinSemilattice Compartment where
  join = joinComp

  associative (U x) (U y) (U z) = cong $ associative x y z
  associative (U x) (U y) (A z w) = rewrite associative x y z in Refl
  associative (U x) (U y) (PC z w) = Refl
  associative (U x) (A y w) (U z) = rewrite associative x y z in Refl
  associative (U x) (A y w) (A z s) = rewrite associative x y z in Refl
  associative (U x) (A y w) (PC z s) = Refl
  associative (U x) (PC y w) (U z) = Refl
  associative (U x) (PC y w) (A z s) = Refl
  associative (U x) (PC y w) (PC z s) = Refl
  associative (A x w) (U y) (U z) = rewrite associative x y z in Refl
  associative (A x w) (U y) (A z s) = rewrite associative x y z in Refl
  associative (A x w) (U y) (PC z s) = Refl
  associative (A x w) (A y s) (U z) = rewrite associative x y z in Refl
  associative (A x w) (A y s) (A z t) =
    rewrite associative x y z in
    rewrite associative w s t in Refl
  associative (A x w) (A y s) (PC z t) = rewrite associative w s t in Refl
  associative (A x w) (PC y s) (U z) = Refl
  associative (A x w) (PC y s) (A z t) = rewrite associative w s t in Refl
  associative (A x w) (PC y s) (PC z t) = rewrite associative w s t in Refl
  associative (PC x w) (U y) (U z) = Refl
  associative (PC x w) (U y) (A z s) = Refl
  associative (PC x w) (U y) (PC z s) = Refl
  associative (PC x w) (A y s) (U z) = Refl
  associative (PC x w) (A y s) (A z t) = rewrite associative w s t in Refl
  associative (PC x w) (A y s) (PC z t) = rewrite associative w s t in Refl
  associative (PC x w) (PC y s) (U z) = Refl
  associative (PC x w) (PC y s) (A z t) = rewrite associative w s t in Refl
  associative (PC x w) (PC y s) (PC z t) =
    rewrite associative x y z in
    rewrite associative w s t in Refl

  commutative (U x) (U y) = cong $ commutative x y
  commutative (U x) (A y z) = rewrite commutative x y in Refl
  commutative (U x) (PC y z) = Refl
  commutative (A x z) (U y) = rewrite commutative x y in Refl
  commutative (A x z) (A y w) =
    rewrite commutative x y in
    rewrite commutative z w in
    Refl
  commutative (A x z) (PC y w) = rewrite commutative w z in Refl
  commutative (PC x z) (U y) = Refl
  commutative (PC x z) (A y w) = rewrite commutative z w in Refl
  commutative (PC x z) (PC y w) =
    rewrite commutative x y in
    rewrite commutative z w in
    Refl

  idempotent (U x) = cong $ idempotent x
  idempotent (A x y) =
     rewrite idempotent x in
     rewrite idempotent y in
     Refl
  idempotent (PC x y) =
     rewrite idempotent x in
     rewrite idempotent y in
     Refl

implementation BoundedJoinSemilattice Compartment where
  Bottom = U Bot

  unitary (U x) = cong $ unitary x
  unitary (A x y) = rewrite unitary x in Refl
  unitary (PC x y) = Refl

--------------------------------------------------------------------------------
-- Lemmas
--------------------------------------------------------------------------------
U_leq_A : U uid `leq` A uid sid
U_leq_A {uid} = rewrite reflexive uid in Refl

A_leq_PC : A uid1 sid `leq` PC uid2 sid
A_leq_PC {sid} = rewrite reflexive sid in Refl


text:
module Minecraft.Base.PreClassic

import public Minecraft.Base.PreClassic.Air.Export
import public Minecraft.Base.PreClassic.Cobblestone.Export
import public Minecraft.Base.PreClassic.Dirt.Export
import public Minecraft.Base.PreClassic.GrassBlock.Export
import public Minecraft.Base.PreClassic.Stone.Export
import public Minecraft.Core.Univ

%default total

exists : String -> Maybe (Ctx Deserialize)
exists "Air.Block"         = Just ((#) Air.Block)
exists "Cobblestone.Block" = Just ((#) Cobblestone.Block)
exists "Dirt.Block"        = Just ((#) Dirt.Block)
exists "GrassBlock.Block"  = Just ((#) GrassBlock.Block)
exists "Stone.Block"       = Just ((#) Stone.Block)
exists _ = Nothing

reflect : (ty : Type) -> Maybe (Vtbl ty)
reflect Air.Block         = Just %search
reflect Cobblestone.Block = Just %search
reflect Dirt.Block        = Just %search
reflect GrassBlock.Block  = Just %search
reflect Stone.Block       = Just %search
reflect _ = Nothing

export
preClassic : Univ
preClassic = MkUniv exists reflect

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
import Data.Vect
import Data.Vect.Elem
import Decidable.Equality
import Data.String
import RemoveElem

data WordState : (guesses_remaining : Nat) -> (letters : Nat) -> Type where
     MkWordState : (word : String) ->
                   (missing : Vect letters Char) ->
                   WordState guesses_remaining letters

data Finished : Type where
     Lost : (game : WordState 0 (S letters)) -> Finished
     Won  : (game : WordState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
     Letter : (c : Char) -> ValidInput [c]

-- proofs
isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No isValidNil where
                     isValidNil : ValidInput [] -> Void
                     isValidNil (Letter c) impossible
isValidInput (x :: []) = Yes (Letter x)
isValidInput (x :: (y :: xs)) = No isValidTooLong where
                                   isValidTooLong : ValidInput (x :: y :: xs) -> Void
                                   isValidTooLong (Letter _ ) impossible

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

-- game logic
readGuess : IO (x ** ValidInput x)
readGuess = do putStr "Guess: "
               x <- getLine
               case isValidString (toUpper x) of
                    Yes prf => pure (_ ** prf)
                    No contra => do putStrLn "Invalid guess"
                                    readGuess

processGuess : {letters : _} ->
               (letter : Char) ->
               WordState (S guesses) (S letters) ->
               Either (WordState guesses (S letters))
                      (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) = case isElem letter missing of
                                                      Yes prf => Right (MkWordState word (removeElem letter missing))
                                                      No contra => Left (MkWordState word missing)

game : {guesses : _} -> {letters : _} -> WordState (S guesses) (S letters) -> IO Finished
game st = do (_ ** Letter letter) <- readGuess
             case processGuess letter st of
                  Left l => do putStrLn "Wrong!"
                               case guesses of
                                    0 => pure (Lost l)
                                    (S k) => game l
                  Right r => do putStrLn "Right!"
                                case letters of
                                     0 => pure (Won r)
                                     (S k) => game r

main : IO ()
main = do result <- game {guesses = 2} (MkWordState "Test" ['T', 'E', 'S'])
          case result of
               Lost (MkWordState word missing) => putStrLn ("You lost. The word was " ++ word)
               Won  (MkWordState word missing) => putStrLn ("You won! The word was " ++ word)


text:
import Language.Reflection

%language ElabReflection

powerFn : Nat -> TTImp
powerFn Z = `(const 1)
powerFn (S k) = `(\x => mult x (~(powerFn k) x))

-- Note: this example doesn't quite do what we want yet. Ideally, we'd find
-- a way to block reduction under the 'pure' while running the script
powerFn' : Nat -> Elab (Nat -> Nat)
powerFn' Z = pure (const 1)
powerFn' (S k)
    = do powerk <- powerFn' k
         pure (\x => mult (powerk x) x)

%macro
power : Nat -> Elab (Nat -> Nat)
power n = check (powerFn n)

%macro
power' : Nat -> Elab (Nat -> Nat)
power' n = powerFn' n

cube : Nat -> Nat
cube = power 3

cube' : Nat -> Nat
cube' = power' 3


text:
module NewEden.NaturalPropertiesHelpers

import Prelude.Either

import NewEden.Algebra
import NewEden.NaturalAxioms

{- Internal -
   This is intended to be a private module which just provides internal
   plumbing used to create the properties of Natural p, but due to issue #144,
   these functions must be public, so for now just use private prefixes.
-}

zero : NaturalProperties t -> t
zero (ProofNaturalProperties Zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = Zero

one : NaturalProperties t -> t
one (ProofNaturalProperties _ One _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = One

privateZeroIsNotOne : (p:NaturalProperties t) -> (zero p = one p -> Void)
privateZeroIsNotOne (ProofNaturalProperties _ _ lemmaDistinction _ _ _ _ _ _ _ _ _ _ _ _ _ _) prf = lemmaDistinction prf

privatePlus : NaturalProperties t -> (t -> t -> t)
privatePlus (ProofNaturalProperties _ _ _ plus _ _ _ _ _ _ _ _ _ _ _ _ _) = plus

privatePlusCommutative : (p:NaturalProperties t) -> CommutativeFunction t (privatePlus p)
privatePlusCommutative (ProofNaturalProperties _ _ _ _ lemmaPlusCommut _ _ _ _ _ _ _ _ _ _ _ _) = lemmaPlusCommut

privatePlusMonoid : (p:NaturalProperties t) -> Monoid t (privatePlus p) (zero p)
privatePlusMonoid (ProofNaturalProperties _ _ _ _ _ lemmaPlusMonoid _ _ _ _ _ _ _ _ _ _ _) = lemmaPlusMonoid

privatePlusLacksInverses : (p:NaturalProperties t) -> StrictMonoid $ privatePlusMonoid p
privatePlusLacksInverses (ProofNaturalProperties _ _ _ _ _ _ lemmaPlusNoInverses _ _ _ _ _ _ _ _ _ _) = lemmaPlusNoInverses

privatePlusMonomorphic : (p:NaturalProperties t) -> ((a:t) -> MonomorphicFunction $ privatePlus p a)
privatePlusMonomorphic (ProofNaturalProperties _ _ _ _ _ _ _ lemmaPlusMonomorphic _ _ _ _ _ _ _ _ _) = lemmaPlusMonomorphic

privateMultiply : NaturalProperties t -> (t -> t -> t)
privateMultiply (ProofNaturalProperties _ _ _ _ _ _ _ _ multiply _ _ _ _ _ _ _ _) = multiply

privateMultiplyCommutative : (p:NaturalProperties t) -> CommutativeFunction t (privateMultiply p)
privateMultiplyCommutative (ProofNaturalProperties _ _ _ _ _ _ _ _ _ lemmaMultCommut _ _ _ _ _ _ _) = lemmaMultCommut

privateMultiplyMonoid : (p:NaturalProperties t) -> Monoid t (privateMultiply p) (one p)
privateMultiplyMonoid (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ lemmaMultMonoid _ _ _ _ _ _) = lemmaMultMonoid

privateMultiplyLacksInverses : (p:NaturalProperties t) -> StrictMonoid $ privateMultiplyMonoid p
privateMultiplyLacksInverses (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ lemmaMultNoInverses _ _ _ _ _) = lemmaMultNoInverses

privateMultiplyMonomorphic : (p:NaturalProperties t) -> ((a:t) -> MonomorphicFunction $ privateMultiply p a)
privateMultiplyMonomorphic (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ _ lemmaMultMonomorphic _ _ _ _) = lemmaMultMonomorphic

privateMultiplyByZero : (p:NaturalProperties t) -> ((a:t) -> (privateMultiply p) a (zero p) = (zero p))
privateMultiplyByZero (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ _ _ lemmaMultByZeroIsZero _ _ _) = lemmaMultByZeroIsZero

privateDistributiveProperty : (p:NaturalProperties t) -> ((a:t) -> (b:t) -> (c:t) -> privateMultiply p a (privatePlus p b c) = privatePlus p (privateMultiply p a b) (privateMultiply p a c))
privateDistributiveProperty (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ _ _ _ lemmaDistributive _ _) = lemmaDistributive

privateSequenceProperty : (p:NaturalProperties t) -> ((a:t) -> (b:t) -> (p1:((a = (zero p) -> Void))) -> (p2: privatePlus p a b = one p) -> a = (one p))
privateSequenceProperty (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ lemmaSequence _) = lemmaSequence

privateCompare : (p:NaturalProperties t) -> ((a:t) -> (b:t) -> Either (a = b) (Either (c ** (privatePlus p a c = b, (c = zero p -> Void))) (c ** (privatePlus p b c = a, (c = zero p -> Void)))))
privateCompare (ProofNaturalProperties _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ compare) = compare

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module Main

import Control.ST
import Data.Fuel
import System

import Brainfeck.ST

CharIO IO where
  getChar = lift getChar
  putChar = lift . putChar
  info    = lift . putStrLn

FilePath : Type
FilePath = String

usage : IO ()
usage =
  let lines = [
      ""
    , "Brainfeck: A somewhat well typed Brainfuck Interpreter."
    , ""
    , "Usage:"
    , "    brainfeck PATH/TO/BRAINFUCK/PROGRAM"
  ] in
  traverse putStrLn lines >>= \_ => pure ()

programFile : IO String
programFile = do
  args <- getArgs
  case inBounds 1 args of
    No contra => do putStrLn "Exactly 1 argument should be provided."
                    usage
                    exitFailure
    Yes prf   => pure (index 1 args)

export
main : IO ()
main = do
  programPath <- programFile
  Left e  <- readFile programPath | (Right prog) =>
                                      run (runProgram False False forever prog)
  putStrLn ("Error reading file: " ++ programPath)
  printLn e

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
-- --------------------------------------------------------------- [ Day03.idr ]
-- Module      : Data.Advent.Day03
-- Description : My solution to the Day 3 puzzle of the 2016 Advent of Code.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : http://adventofcode.com/2016/day/3
-- --------------------------------------------------------------------- [ EOH ]
||| Day 3: Squares with Three Sides
module Data.Advent.Day03

import public Data.Advent.Day

import Data.Vect

-- -------------------------------------------------------------- [ Data Types ]

%access export

||| A triangle, comprised of three side lengths, is equilateral or il/logical.
data Triangle : Type where

     ||| Given side lengths `a`, `b` and `c`, and proofs that `a = b`
     ||| and `b = c`, return a `Triangle.`
     Equilateral : (a, b, c : Integer) -> a = b -> b = c -> Triangle

     ||| Given side lengths `a`, `b` and `c`, and proofs that they satisfy the
     ||| triangle inequality theorem, return a `Triangle`.
     ||| @ p1 a proof that `a` is strictly less than `b + c`
     ||| @ p2 a proof that `b` is strictly less than `a + c`
     ||| @ p3 a proof that `c` is strictly less than `a + b`
     Logical : (a, b, c : Integer) ->
               (p1 : LT (fromIntegerNat a) (fromIntegerNat (b + c))) ->
               (p2 : LT (fromIntegerNat b) (fromIntegerNat (a + c))) ->
               (p3 : LT (fromIntegerNat c) (fromIntegerNat (a + b))) ->
               Triangle

     ||| Construct a triangle that is neither equilateral nor logical.
     Illogical : (a, b, c : Integer) -> Triangle

||| Given side lengths `a`, `b` and `c`, if they are all equal,
||| return `Just` a `Triangle`, otherwise `Nothing`.
equilateral : (a, b, c : Integer) -> Maybe Triangle
equilateral a b c with (decEq a b)
  equilateral _ _ _ | No _              = Nothing
  equilateral a b c | Yes ab with (decEq b c)
    equilateral _ _ _ | _ | No _        = Nothing
    equilateral a b c | Yes ab | Yes bc = Just (Equilateral a b c ab bc)

||| Given side lengths `a`, `b` and `c`, return `Just` a `Triangle` if they
||| satisfy the triangle inequality theorem, otherwise `Nothing`.
logical : (a, b, c : Integer) -> Maybe Triangle
logical a b c with (isLTE (S (fromIntegerNat a)) (fromIntegerNat (b + c)))
  logical _ _ _| No _                             = Nothing
  logical a b c | Yes abc with (isLTE (S (fromIntegerNat b))
                                      (fromIntegerNat (a + c)))
    logical _ _ _| _ | No _                       = Nothing
    logical a b c | Yes abc | Yes bac with (isLTE (S (fromIntegerNat c))
                                                  (fromIntegerNat (a + b)))
      logical _ _ _ | _       | _       | No _    = Nothing
      logical a b c | Yes abc | Yes bac | Yes cab =
          Just (Logical a b c abc bac cab)

namespace Triangle

  ||| Construct a `Triangle` from the given side lengths.
  triangle : (a, b, c : Integer) -> Triangle
  triangle a b c = fromMaybe (Illogical a b c) $
                   equilateral a b c <|> logical a b c

  ||| Construct a `Triangle` from a `Vect` of (three) side lengths (integers).
  fromVect : Vect 3 Integer -> Triangle
  fromVect [a,b,c] = triangle a b c

-- ----------------------------------------------------------------- [ Parsers ]

||| Parse three side lengths.
partial sides : Parser (Vect 3 Integer)
sides = ntimes 3 (spaces *> integer)

{-
||| Parse three side lengths and construct a `Triangle`.
partial triangle : Parser Triangle
triangle = do [a,b,c] <- sides
              pure $ triangle a b c
-}

-- ------------------------------------------------------------------- [ Logic ]

||| Given a foldable structure containing `Triangle`s,
||| count which of them are not `Illogical`.
countPossible : Foldable t => t Triangle -> Nat
countPossible = foldl go 0
  where
    go : Nat -> Triangle -> Nat
    go n (Illogical _ _ _) = n
    go n _                 = S n

-- ---------------------------------------------------------------- [ Part One ]

partial partOne : List (Vect 3 Integer) -> IO String
partOne = pure . show . countPossible . map fromVect

-- ---------------------------------------------------------------- [ Part Two ]

partial partTwo : List (Vect 3 Integer) -> IO String
partTwo = pure . show . countPossible .
          concatMap (toList . map fromVect . transpose) .
          go
  where
    go : List (Vect 3 Integer) -> List (Vect 3 (Vect 3 Integer))
    go (x::y::z::zs) = [x,y,z] :: go zs
    go _             = []

-- -------------------------------------------------------------------- [ Main ]

namespace Main

  partial main : IO ()
  main = runDay $ MkDay 3
         (some (sides <* spaces))
         partOne
         partTwo

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

max_stars_repo_name: yurrriq/advent-of-code


text:
module Main

import Data.Vect
import Data.Fin

%default total

infixr 5 .+.
data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType SChar = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

data Command : Schema -> Type where
  Quit : Command s
  Size : Command s
  Get  : Nat -> Command s
  ShowEntries : Command s
  Add  : SchemaType schema -> Command schema
  SetSchema : Schema -> Command s

consToTheEnd : a -> Vect n a -> Vect (S n) a
consToTheEnd x [] = [x]
consToTheEnd x (y :: xs) = y :: consToTheEnd x xs

appendToStore : (ds : DataStore) -> (SchemaType $ schema ds) -> DataStore
appendToStore (MkData schema size items) item =
  MkData schema (S size) (consToTheEnd item items)

getEntry : (store : DataStore) -> (i : Nat) -> Maybe (SchemaType $ schema store)
getEntry store i = case natToFin i (size store) of
                        Nothing => Nothing
                        (Just fin) => Just $ Vect.index fin (items store)

chompChar : Char -> String -> Maybe String
chompChar char str = case span (\c => c == char) str of
                          ("", _) => Nothing
                          (chomped, rest) => (case chomped == cast char of
                                                   False => Nothing
                                                   True => Just rest)

stringUncons : String -> Maybe (Char, String)
stringUncons str = case unpack str of
                      [] => Nothing
                      (x :: xs) => Just (x, pack xs)

parsePrefix : (s : Schema) -> String -> Maybe (SchemaType s, String)
parsePrefix SString str = case chompChar '"' str of
                               Nothing => Nothing
                               (Just rest) =>
                                 case span (\c => c /= '"') rest of
                                      (string, rest') =>
                                         case chompChar '"' rest' of
                                              Nothing => Nothing
                                              (Just rest'' ) => Just (string, ltrim rest'')

parsePrefix SInt str = case span isDigit str of
                          ("", rest) => Nothing
                          (digit, rest) => Just (cast digit, ltrim rest)

parsePrefix SChar str = case stringUncons str of
                             Nothing => Nothing
                             (Just (c, rest)) => Just (c, ltrim rest)

parsePrefix (x .+. y) str = do
  (pX, rest)  <- parsePrefix x str
  (pY, rest') <- parsePrefix y rest
  pure ((pX, pY), rest')

readSchema : List String -> Maybe Schema
readSchema ("String" :: []) = Just SString
readSchema ((::) "String" rest@(x :: xs)) = [| pure SString .+. readSchema rest |]
readSchema ("Int" :: []) = Just SInt
readSchema ((::) "Int" rest@(x :: xs)) = [| pure SInt .+. readSchema rest |]
readSchema ("Char" :: []) = Just SChar
readSchema ((::) "Char" rest@(x :: xs)) = [| pure SChar .+. readSchema rest |]
readSchema _ = Nothing

readValueOfSchema : (s : Schema) -> String -> Maybe (SchemaType s)
readValueOfSchema s str = case parsePrefix s str of
                               -- The value must be all there is
                               (Just (val, "")) => Just val
                               _ => Nothing

parseCommandHelper : (s : Schema) -> (cmd : String) -> (rest : String)
                     -> Maybe (Command s)
parseCommandHelper schema "add" rest = [| Add (readValueOfSchema schema rest) |]
parseCommandHelper schema "get" rest = case all isDigit (unpack rest) of
                                     False => Nothing
                                     True => Just $ Get (cast rest)
parseCommandHelper schema "quit" "" = Just Quit
parseCommandHelper schema "size" "" = Just Size
-- parseCommandHelper schema "search" searchQuery = Just $ Search searchQuery
parseCommandHelper schema "schema" rest = [| SetSchema (readSchema $ words rest) |]
parseCommandHelper _ _ _ = Nothing

parseCommand : (s : Schema) -> String -> Maybe (Command s)
parseCommand schema str = case span (/= ' ') str of
                     (cmd, rest) => parseCommandHelper schema cmd (ltrim rest)

vectFilter : (a -> Bool) -> Vect n a -> List a
vectFilter f [] = []
vectFilter f (x :: xs) = case f x of
                              False => vectFilter f xs
                              True => x :: vectFilter f xs

--searchInDataStore : DataStore -> String -> List String
--searchInDataStore (MkData size items) query = vectFilter (isInfixOf query) items

mapFst : (a -> b) -> (a, c) -> (b, c)
mapFst f (a, b) = (f a, b)

vectWithIndices : Vect n a -> Vect n (Fin n, a)
vectWithIndices [] = []
vectWithIndices (x :: xs) = (FZ, x) :: map (mapFst FS) (vectWithIndices xs)

--searchWithIndices : DataStore -> String -> List (Nat, String)
--searchWithIndices (MkData size items) query =
--  map (mapFst finToNat) $ vectFilter (isInfixOf query . snd) (vectWithIndices items)

joinWithNewlines : Vect n String -> String
joinWithNewlines [] = ""
joinWithNewlines (x :: xs) = x ++ "\n" ++ joinWithNewlines xs

formatWithId : Vect n (Fin n, SchemaType schema) -> String
-- formatWithId = joinWithNewlines . map (\(id, item) => show (the Nat (cast id)) ++ ": " ++ (showSchemaItem item))
formatWithId [] = ""
formatWithId ((index, item) :: xs) = (show (the Nat $ cast index) ++ ": ") -- ++ (showSchemaItem item) -- ++ "\n" -- ++ (formatWithId xs)

showSchemaItem : SchemaType s -> String
showSchemaItem {s = SString} str = str
showSchemaItem {s = SInt} i = cast i
showSchemaItem {s = SChar} c = "'" ++ cast c ++ "'"
showSchemaItem {s = (l .+. r)} (lVal, rVal) = "(" ++ (showSchemaItem lVal) ++ ", " ++ (showSchemaItem rVal) ++ ")"

-- Update kind of like in model view update
update : (store : DataStore) -> (input : String) -> Maybe (String, DataStore)
update store input =
  case parseCommand (schema store) input of
       Nothing => Just ("Whaaat?", store)
       (Just Quit) => Nothing
       (Just (Get i)) => Just ( fromMaybe "Invalid index"
                                  [| showSchemaItem $ getEntry store i |]
                              , store
                              )
       (Just (Add str)) => Just ( "ID " ++ show (size store)
                                , appendToStore store str
                                )
       (Just Size) => Just (show (size store), store)
       (Just (SetSchema s)) => Just ("Nice!", MkData s 0 [])
       (Just (ShowEntries)) => Just (formatWithId $ vectWithIndices (items store), store)
    -- (Just (Search query)) => Just (formatWithId $ searchWithIndices store query, store)

partial main : IO ()
main = replWith (MkData (SString .+. SInt) 0 []) "\nInstruction: " update

--------
plusOneIsSucc : n + 1 = S n
plusOneIsSucc {n = Z} = Refl
plusOneIsSucc {n = (S k)} = cong $ plusOneIsSucc {n=k}


text:
module Crypto.Random

import Control.Monad.Error.Either
import Control.Monad.State
import Crypto.ChaCha
import Data.Bits
import Data.Fin
import Data.List
import Data.Nat
import Data.Stream
import Data.Vect
import Utils.Bytes
import Utils.Misc

public export
interface DRG (0 a : Type) where
  next_bytes : (n : Nat) -> a -> (a, Vect n Bits8)

public export
interface Monad m => MonadRandom (0 m : Type -> Type) where
  random_bytes : (n : Nat) -> m (Vect n Bits8)

public export
{s : _} -> DRG s => MonadRandom (State s) where
  random_bytes n = state (next_bytes n)

public export
next_integer : MonadRandom m => Nat -> m Integer
next_integer bytes = do
  randoms <- random_bytes bytes
  pure $ foldr (\(i,x),a => (shiftL {a=Integer} x i) .|. a) 0 $ zip ((*8) <$> [0..bytes]) (cast <$> toList randoms)

bytes_needed : Integer -> Nat
bytes_needed = (`div` 8) . cast . go 0
  where
    go : Nat -> Integer -> Nat
    go x n = if (n .&. ((bit x) - 1)) == n then x else go (x+8) n

random_num_uniform : MonadRandom m => Nat -> Integer -> m Integer
random_num_uniform bytes min = next_integer bytes >>= (\r => if r >= min then pure r else random_num_uniform bytes min)

public export
uniform_random : MonadRandom m => Integer -> m Integer
uniform_random {m} upper_bound =
  if upper_bound < 0 then negate <$> (uniform_random {m=m} $ abs upper_bound)
    else if upper_bound < 2 then pure 0
      else
        let bytes = bytes_needed upper_bound
        in (`mod` upper_bound) <$> random_num_uniform bytes ((bit bytes) `mod` upper_bound)

public export
uniform_random' : MonadRandom m => Integer -> Integer -> m Integer
uniform_random' {m} lower_bound upper_bound = do
  r <- uniform_random (upper_bound - lower_bound)
  pure (r + lower_bound)

public export
data ChaCha12DRG : Type where
  MkChaCha12DRG : (key : Vect 8 Bits32) -> ChaCha12DRG

public export
new_chacha12_drg : MonadRandom m => m ChaCha12DRG
new_chacha12_drg {m} = (\r => MkChaCha12DRG (from_le <$> group 8 4 r)) <$> (random_bytes {m=m} 32)

chacha12_stream : Vect 8 Bits32 -> Stream Bits8
chacha12_stream key = stream_concat $ map go nats
  where
    go : Nat -> List Bits8
    go iv = toList $ chacha_rfc8439_block 6 (cast iv) key (map (cast . finToNat) range)

public export
DRG ChaCha12DRG where
  next_bytes Z state = (state, [])
  next_bytes bytes (MkChaCha12DRG key) =
    let stream = chacha12_stream key
        key = map (from_le {n=4}) $ group 8 4 $ take 32 stream
        stream = drop 32 stream
    in (MkChaCha12DRG key, take bytes stream)