text:
module Erlang.Types.Map

import Erlang.Types
import Erlang.Decode
import Erlang.IO

%default total

-- This module contains functions to create Erlang maps and to get values from
-- Erlang maps. Erlang maps are allowed to store any Erlang value in its
-- keys and values.

||| A predicate that a certain key and type exists in a list of entries.
public export
data ErlMapElem : key -> Type -> List ErlMapEntry -> Type where
  [search key]
  Here : ErlMapElem key valueTy (MkMapEntry key valueTy :: _)
  There : ErlMapElem key valueTy xs -> ErlMapElem key valueTy (_ :: xs)

||| Convert an `ErlMapSubset` to `ErlAnyMap`.
|||
||| This conversion is always safe because `ErlAnyMap` represents any Erlang
||| maps, independent of which keys/values it contains.
export %inline
toAnyMap : ErlMapSubset xs -> ErlAnyMap
toAnyMap = believe_me

-- MANIPULATE MAPS

||| Create an empty Erlang map.
export
empty : ErlAnyMap
empty = erlUnsafeCall ErlAnyMap "maps" "new" []

||| Insert a key/value into an Erlang map.
export
insert : (ErlType key, ErlType value) => key -> value -> ErlAnyMap -> ErlAnyMap
insert key value m = erlUnsafeCall ErlAnyMap "maps" "put" [key, value, m]

||| Delete a key from an Erlang map.
export
delete : ErlType key => key -> ErlAnyMap -> ErlAnyMap
delete key m = erlUnsafeCall ErlAnyMap "maps" "remove" [key, m]

-- QUERY MAPS

||| Get the number of keys in an Erlang map.
export
size : ErlMapSubset xs -> Nat
size m =
  let size = erlUnsafeCall Integer "maps" "size" [toAnyMap m]
  in integerToNat size

||| Get all keys in an Erlang map.
export
keys : ErlMapSubset xs -> List ErlTerm
keys m = erlUnsafeCall (List ErlTerm) "maps" "keys" [toAnyMap m]

||| Get all values in an Erlang map.
export
values : ErlMapSubset xs -> List ErlTerm
values m = erlUnsafeCall (List ErlTerm) "maps" "values" [toAnyMap m]

||| Get all entries in an Erlang map.
export
entries : ErlMapSubset xs -> List (ErlTerm, ErlTerm)
entries m =
  let xs = erlUnsafeCall (List (ErlTuple2 ErlTerm ErlTerm)) "maps" "to_list" [toAnyMap m]
  in map (\(MkTuple2 x1 x2) => (x1, x2)) xs

||| Look for a key in an Erlang map. The value for the key must match the
||| given decoder.
|||
||| Returns `Nothing` if no valid entry is found.
export
lookup : ErlType key => key -> ErlDecoder a -> ErlMapSubset xs -> Maybe a
lookup key decoder m = erlDecodeMay (mapEntry key decoder) (toAnyMap m)

||| Get a specific key from an Erlang map.
|||
||| The key must be specified as an entry in the type of `ErlMapSubset`.
export
get : (key : a) -> ErlMapSubset xs -> ErlMapElem key b xs => b
get key m =
  let MkRaw res = erlUnsafeCall (Raw b) "maps" "get" [MkRaw key, toAnyMap m]
  in res


text:
module JS.Undefined

import Data.List.Elem
import JS.Util
import JS.Inheritance
import JS.Marshall
import JS.Nullable

--------------------------------------------------------------------------------
--          Undefined
--------------------------------------------------------------------------------

export
data Undefined : Type where [external]

||| The `undefined` constant
export
%foreign "javascript:lambda:()=>undefined"
undefined : Undefined

export
Eq Undefined where
  _ == _ = True

export
Show Undefined where
  show _ = "undefined"

%foreign "javascript:lambda:x=>x === undefined?1:0"
prim__isUndefined : AnyPtr -> Double

||| Tests, whether a value of questionable origin is undefined
export
isUndefined : a -> Bool
isUndefined v = doubleToBool $ prim__isUndefined (believe_me v)

export
ToFFI Undefined Undefined where
  toFFI = id

export
FromFFI Undefined Undefined where
  fromFFI = Just

export
SafeCast Undefined where
  safeCast ptr = if isUndefined ptr then Just undefined else Nothing

--------------------------------------------------------------------------------
--          UndefOr
--------------------------------------------------------------------------------

export
data UndefOr : Type -> Type where [external]

export
undef : UndefOr a
undef = believe_me undefined

export
def : a -> UndefOr a
def = believe_me

export
SafeCast a => SafeCast (UndefOr a) where
  safeCast ptr = if isUndefined ptr
                    then Just undef
                    else map def $ safeCast ptr

--------------------------------------------------------------------------------
--          Optional
--------------------------------------------------------------------------------

public export
data Optional : (a : Type) -> Type where
  Undef : Optional a
  Def   : a -> Optional a

export
Show a => Show (Optional a) where
  showPrec _ Undef   = "Undef"
  showPrec p (Def a) = showCon p "Def" (showArg a)

public export
Eq a => Eq (Optional a) where
  Undef == Undef = True
  Def x == Def y = x == y
  _     == _     = False

public export
Ord a => Ord (Optional a) where
  compare Undef Undef     = EQ
  compare Undef (Def _)   = LT
  compare (Def _) Undef   = GT
  compare (Def x) (Def y) = compare x y

public export
Functor Optional where
  map _ Undef   = Undef
  map f (Def x) = Def $ f x

public export
Applicative Optional where
  pure = Def
  Def f <*> Def a = Def $ f a
  _     <*>     _ = Undef

public export
Monad Optional where
  Undef >>= _ = Undef
  Def x >>= f = f x

public export
Alternative Optional where
  empty = Undef
  Undef <|> x = x
  Def v <|> _ = Def v

public export
Foldable Optional where
  foldr _ acc Undef   = acc
  foldr f acc (Def x) = f x acc

  foldl _ acc Undef   = acc
  foldl f acc (Def x) = f acc x

  null Undef   = True
  null (Def _) = False

public export
Traversable Optional where
  traverse f Undef   = pure Undef
  traverse f (Def x) = Def <$> f x

public export
optional : Lazy b -> (a -> b) -> Optional a -> b
optional x f Undef   = x
optional _ f (Def y) = f y

public export
fromOptional : Lazy a -> Optional a -> a
fromOptional a Undef   = a
fromOptional _ (Def a) = a

export
optionalToUndefOr : Optional a -> UndefOr a
optionalToUndefOr = optional undef def

export
optUp : (0 _ : JSType a) => Optional a -> {auto 0 _ : Elem b (Types a)} -> UndefOr b
optUp x = optional undef (\v => def $ up v) x

export
omyUp :  (0 _ : JSType a)
      => Optional (Maybe a)
      -> {auto 0 _ : Elem b (Types a)}
      -> UndefOr (Nullable b)
omyUp x = optionalToUndefOr $ map (\m => mayUp m) x

public export
maybeToOptional : Maybe a -> Optional a
maybeToOptional = maybe Undef Def

public export
optionalToMaybe : Optional a -> Maybe a
optionalToMaybe = optional Nothing Just

export
undeforToOptional : UndefOr a -> Optional a
undeforToOptional v = if isUndefined v then Undef else Def (believe_me v)

export
undeforToMaybe : UndefOr a -> Maybe a
undeforToMaybe v = if isUndefined v then Nothing else Just (believe_me v)

export
ToFFI a b => ToFFI (Optional a) (UndefOr b) where
  toFFI = optionalToUndefOr . map toFFI

export
FromFFI a b => FromFFI (Optional a) (UndefOr b) where
  fromFFI v = case undeforToOptional v of
                   Undef => Just Undef
                   Def x => map Def $ fromFFI x

ext: idr


text:
import VISD.Common

-- List Bool <-> Nat, with size and endianness

data Endianness = BE | LE

snoc : {n : Nat} -> {a : Type} -> (x : a) -> Vect n a -> Vect (S n) a
snoc x [] = [x]
snoc x (y :: xs) = (y :: snoc x xs)

reverse : {n : Nat} -> Vect n a -> Vect n a
reverse [] = []
reverse (x :: xs) = (snoc x (reverse xs))

reverse_snoc : {a : Type} -> {n : Nat} -> (x : a) -> (v : Vect n a) -> reverse (snoc x v) = x :: reverse v
reverse_snoc x [] = Refl
reverse_snoc x (y :: xs) = rewrite (reverse_snoc x xs) in Refl

double_reverse : (v : Vect n a) -> reverse (reverse v) = v
double_reverse [] = Refl
double_reverse (x :: xs) = rewrite (reverse_snoc x (reverse xs)) in
  rewrite (double_reverse xs) in Refl

order : Endianness -> Vect n Bool -> Vect n Bool
order BE v = reverse v
order LE v = v

double_order : (e : Endianness) -> (v : Vect n Bool) -> order e (order e v) = v
double_order BE v = (double_reverse v)
double_order LE v = Refl

div2 : Nat -> Nat
div2 Z = 0
div2 (S Z) = 0
div2 (S (S k)) = div2' (S k)
  where -- a hack for totality checker
    div2' : Nat -> Nat
    div2' Z = 0
    div2' (S n) = S (div2 n)

div2_zero : (k : Nat) -> (lte k (S Z) = True) -> div2 k = Z
div2_zero Z prf = Refl
div2_zero (S Z) prf = Refl
div2_zero (S (S k)) prf = (void (trueNotFalse (sym prf)))

mul2 : Nat -> Nat
mul2 Z = 0
mul2 (S k) = (S (S (mul2 k)))

mul2_n_zero : (n : Nat) -> (mul2 n = Z) -> n = Z
mul2_n_zero Z prf = Refl
mul2_n_zero (S k) prf = void $ OnotS (sym prf)

mul2_zero_n : (n : Nat) -> n = Z -> mul2 n = Z
mul2_zero_n n prf = rewrite prf in Refl

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

even_inv : (n : Nat) -> (even (S n) = not (even n))
even_inv Z = Refl
even_inv (S Z) = Refl
even_inv (S (S k)) = (even_inv k)

mul2_even : (n : Nat) -> even (mul2 n) = True
mul2_even Z = Refl
mul2_even (S k) = (mul2_even k)

mul2_not_odd : (n : Nat) -> odd (mul2 n) = False
mul2_not_odd Z = Refl
mul2_not_odd (S k) = (mul2_not_odd k)

div2_mul2_n_eq_n : (n : Nat) -> div2 (mul2 n) = n
div2_mul2_n_eq_n Z = Refl
div2_mul2_n_eq_n (S k) = cong {f=S} $ div2_mul2_n_eq_n k

div2_S_mul2_n_eq_n : (n : Nat) -> div2 (S (mul2 n)) = n
div2_S_mul2_n_eq_n Z = Refl
div2_S_mul2_n_eq_n (S k) = cong {f=S} $ div2_S_mul2_n_eq_n k

mul2_div2_even : (n : Nat) -> (even n = True) -> mul2 (div2 n) = n
mul2_div2_even Z prf = Refl
mul2_div2_even (S Z) prf = (void (trueNotFalse (sym prf)))
mul2_div2_even (S (S k)) prf = cong {f=S} $ cong {f=S} (mul2_div2_even k prf)

mul2_div2_eq : (n, m : Nat) -> (even m = True) -> (n = div2 m) -> mul2 n = m
mul2_div2_eq n m evp eqp = rewrite eqp in (mul2_div2_even m evp)

div2_S_even : (n : Nat) -> (even n = True) -> div2 (S n) = div2 n
div2_S_even Z prf = Refl
div2_S_even (S Z) prf = (void (trueNotFalse (sym prf)))
div2_S_even (S (S k)) prf = cong {f=S} (div2_S_even k prf)

natToBitsLe : (k : Nat) -> Nat -> Maybe (Vect k Bool)
natToBitsLe bits Z = Just $ replicate bits False
natToBitsLe Z n = Nothing
natToBitsLe (S bits) n = do
  next <- natToBitsLe bits (div2 n)
  return $ odd n :: next

bitsToNatLe : Vect k Bool -> Nat
bitsToNatLe [] = Z
bitsToNatLe (v :: l) = (if v then 1 else 0) + (mul2 $ bitsToNatLe l)

btnl_zero_step : (xs : Vect k Bool) -> (bitsToNatLe (False :: xs) = Z) -> bitsToNatLe xs = Z
btnl_zero_step xs prf = mul2_n_zero (bitsToNatLe xs) $
  replace {P=(\x => 0 + x = Z)} (plusZeroLeftNeutral (mul2 $ bitsToNatLe xs)) prf

btnl_zero : (n : Nat) -> (v : Vect n Bool) -> bitsToNatLe v = Z -> v = Vect.replicate n False
btnl_zero Z [] prf = Refl
btnl_zero (S k) (False :: xs) prf = cong {f=((Vect.(::)) False)} (btnl_zero k xs (btnl_zero_step xs prf))
btnl_zero (S k) (True :: xs) prf = (void $ OnotS (sym prf))

ntbl_zero : (x : Nat) -> (xs : Vect x Bool) -> natToBitsLe x Z = Just xs -> xs = Vect.replicate x False
ntbl_zero Z [] prf = Refl
ntbl_zero (S n) (y :: xs) prf =
  rewrite (justInjective (replace {P=(\z => z = Just (y :: xs))} (ntbl_zero' (S n)) prf)) in Refl
  where
    ntbl_zero' : (x : Nat) -> natToBitsLe x Z = Just $ Vect.replicate x False
    ntbl_zero' x = Refl

ntbl_step_false : (n : Nat) -> (xs : Vect n Bool) ->
  natToBitsLe n (bitsToNatLe xs) = Just xs ->
  natToBitsLe (S n) (mul2 (bitsToNatLe xs)) = Just (False :: xs)
ntbl_step_false x xs prf with (bitsToNatLe xs)
  | Z = rewrite (ntbl_zero x xs prf) in Refl
  | S m = rewrite (div2_mul2_n_eq_n (S m)) in
    rewrite prf in
      rewrite (mul2_not_odd m) in Refl

ntbl_step_true : (n : Nat) -> (xs : Vect n Bool) ->
  natToBitsLe n (bitsToNatLe xs) = Just xs ->
  natToBitsLe (S n) (S (mul2 (bitsToNatLe xs))) = Just (True :: xs)
ntbl_step_true n xs prf = rewrite (mul2_even (bitsToNatLe xs)) in
  rewrite (div2_S_mul2_n_eq_n (bitsToNatLe xs)) in
    rewrite prf in Refl

ntbl_btnl : (k : Nat) -> (v : Vect k Bool) -> natToBitsLe k (bitsToNatLe v) = Just v
ntbl_btnl Z [] = Refl
ntbl_btnl (S n) (x :: xs) with (inspect $ bitsToNatLe xs)
    | match Z {eq=eq} = rewrite eq in
      rewrite (btnl_zero n xs eq) in case (inspect x) of
        match True {eq=eq1} => rewrite eq1 in Refl
        match False {eq=eq1} => rewrite eq1 in Refl
    | match (S m) {eq=eq} = case (inspect x) of
      match True {eq=eq1} => rewrite eq1 in (ntbl_step_true n xs (ntbl_btnl n xs))
      match False {eq=eq1} => rewrite eq1 in (ntbl_step_false n xs (ntbl_btnl n xs))

btnl_rep_false : (k : Nat) -> bitsToNatLe (replicate k False) = Z
btnl_rep_false Z = Refl
btnl_rep_false (S k) = (mul2_zero_n (bitsToNatLe (replicate k False)) (btnl_rep_false k))

btnl_ntbl : (k, n : Nat) -> maybe () (\x => bitsToNatLe x = n) $ natToBitsLe k n
btnl_ntbl k Z = (btnl_rep_false k)
btnl_ntbl Z (S j) = ()
btnl_ntbl (S k) (S j) with (inspect $ natToBitsLe k (div2 (S j)))
  | match Nothing {eq=eq} = rewrite eq in ()
  | match (Just xs) {eq=eq} = rewrite eq in case (inspect $ even j) of
    match True {eq=eq1} => rewrite eq1 in cong {f=S} $
      mul2_div2_eq (bitsToNatLe xs) j eq1 $
        replace {P=(\p => maybe () (\x => bitsToNatLe x = div2 j) p)}
          (replace {P=(\p => natToBitsLe k p = Just xs)} (div2_S_even j eq1) eq)
          (btnl_ntbl k (div2 j))
    match False {eq=eq1} => rewrite eq1 in
      mul2_div2_eq (bitsToNatLe xs) (S j) (replace {P=(\p => even (S j) = not p)} eq1 (even_inv j)) $
        replace {P=(\p => maybe () ((\x => bitsToNatLe x = div2 (S j))) p)} eq (btnl_ntbl k (div2 $ S j))

just_btnl_ntbl : (k, n : Nat) -> maybe () (\x => Just (bitsToNatLe x) = Just n) $ natToBitsLe k n
just_btnl_ntbl k n with (inspect $ natToBitsLe k n)
      | match Nothing {eq=eq} = rewrite eq in ()
      | match (Just v) {eq=eq} = rewrite eq in cong {f=Just} $ case (btnl_ntbl k n) of
        wojust => replace eq wojust

natLeIso : (k : Nat) -> PartIso (Vect k Bool) Nat
natLeIso k = MkPartIso (Just . bitsToNatLe) (natToBitsLe k) tf ft
  where
    tf n = just_btnl_ntbl k n
    ft v = ntbl_btnl k v

natLe : Syntax d Bool => (k : Nat) -> d Nat Bool
natLe k = natLeIso k <$> rep k item

natToBits : Endianness -> (k : Nat) -> Nat -> Maybe (Vect k Bool)
natToBits e k n = natToBitsLe k n >>= Just . order e

bitsToNat : Endianness -> Vect n Bool -> Maybe Nat
bitsToNat e v = Just $ bitsToNatLe (order e v)

btn_ntb : (k, n : Nat) -> (e : Endianness) -> maybe () (\x => bitsToNat e x = Just n) $ natToBits e k n
btn_ntb k n e with (inspect $ natToBitsLe k n)
  | match Nothing {eq=eq} = rewrite eq in ()
  | match (Just as) {eq=eq} = rewrite eq in rewrite (double_order e as) in
    cong {f=Just} (replace eq {P=(\y => maybe () (\x => bitsToNatLe x = n) y)} (btnl_ntbl k n))

ntb_btn : (k : Nat) -> (e : Endianness) -> (v : Vect k Bool) ->
  maybe () (\x => natToBits e k x = Just v) $ bitsToNat e v
ntb_btn k e v = rewrite (ntbl_btnl k (order e v)) in rewrite (double_order e v) in Refl

natIso : (e : Endianness) -> (k : Nat) -> PartIso (Vect k Bool) Nat
natIso e k = MkPartIso (bitsToNat e) (natToBits e k) tf ft
  where
    tf n = (btn_ntb k n e)
    ft v = (ntb_btn k e v)

nat : Syntax d Bool => Endianness -> Nat -> d Nat Bool
nat endianness size = natIso endianness size <$> rep size item

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
-- ------------------------------------------------------------ [ DeBruijn.idr ]
-- Module    : DeBruijn.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Data structure to compute de Bruijn indices.
|||
||| Thanks to christiansen's Galois tutorials for the accessor and
||| mutator functions for environments/object store.
module Data.DeBruijn

import Data.DList

||| A de Bruijn Index.
|||
||| @T    The type of type's collected.
||| @ctxt The collection of types.
||| @t    The element collected at the current position.
public export
data Index : (T : Type)
          -> (ctxt : List T)
          -> (t : T)
          -> Type where
  ||| The first element in the index.
  First : Index ty (t::ts) t

  ||| The next element in the index.
  Next  : Index ty ts t -> Index ty (t'::ts) t

||| Sometimes it is bettern to think that we have this thing called an
||| environment and not a `DList`.
|||
||| @t    The Type for Types in our environment.
||| @obj  How we interpret the types in our DSL. Either this is a
|||       dependent type or a function that computes a type.
||| @ctxt The typing context.
public export
Env : (t : Type) -> (obj : t -> Type) -> (ctxt : List t) -> Type
Env ty obj ctxt = DList ty (\x => obj x) ctxt

||| Read an object from our typing environment.
|||
||| @idx The typing context.
||| @env The typing environment.
export
read : (idx : Index ty ctxt t)
    -> (env : Env ty e ctxt)
    -> e t
read First    (obj::store) = obj
read (Next x) (obj::store) = read x store

||| Add an object to our typnig environment.
|||
||| @idx The typing context.
||| @obj The object to add.
||| @env The environment to which the object is added.
export
write : (idx : Index ty ctxt t )
     -> (obj : e t)
     -> (env : Env ty e ctxt)
     -> Env ty e ctxt
write First    obj (_    :: store) = obj  :: store
write (Next x) obj (obj' :: store) = obj' :: write x obj store

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
import Aoc
import Data.List
import Data.List1
%default total

partial
main : IO ()
main = do
  ps <- readParagraphs
  putStr "*   "; printLn $ sum $ map (maybe 0 length . foldl1' union     . map unpack) ps
  putStr "**  "; printLn $ sum $ map (maybe 0 length . foldl1' intersect . map unpack) ps


text:
module Main

%lib C "tensorflow"
%include C "tensorflow/c/c_api.h"
-- %include C "/usr/include/tensorflow/c/c_api.h"
-- %link C "testlib.o"

-- data TF_Tensor
-- IO (Raw TF_Tensor) works,but c warns assignment from incompatible pointer type
data TF_Status2:(a:Type)->Type where --safer way
  TF_Status22:TF_Status2 Ptr

TF_Status : Type
TF_Status = Ptr -- attention!

-- Tfs : Raw TF_Status
-- Tfs = MkRaw TF_Status

tfNewStatus : IO TF_Status
tfNewStatus = foreign FFI_C "TF_NewStatus" (IO TF_Status)

tfGetCode : TF_Status ->IO Int
tfGetCode = foreign FFI_C "TF_Code" (TF_Status ->IO Int)

tfVersion : IO String
tfVersion = foreign FFI_C "TF_Version" (IO String)

main : IO ()
main = do
     x<-tfVersion
     s<-tfNewStatus
     c<-tfGetCode s
--     print c
     putStrLn x

max_stars_repo_name: justjoheinz/tensorflow-idris

max_issues_repo_name: justjoheinz/tensorflow-idris

max_forks_repo_name: justjoheinz/tensorflow-idris


text:
||| Slightly different lexer than the source language because we are more free
||| as to what can be identifiers, and fewer tokens are supported. But otherwise,
||| we can reuse the standard stuff
module Idris.IDEMode.Parser

import Idris.IDEMode.Commands

import Data.Maybe
import Data.List
import Data.Strings
import Parser.Lexer.Source
import Parser.Source
import Parser.Support
import Text.Lexer
import Text.Parser
import Utils.Either
import Utils.String

%default total

%hide Text.Lexer.symbols
%hide Parser.Lexer.Source.symbols

symbols : List String
symbols = ["(", ":", ")"]

ideTokens : TokenMap Token
ideTokens =
    map (\x => (exact x, Symbol)) symbols ++
    [(digits, \x => IntegerLit (cast x)),
     (stringLit, \x => StringLit (fromMaybe "" (escape (stripQuotes x)))),
     (identAllowDashes, \x => Ident x),
     (space, Comment)]

idelex : String -> Either (Int, Int, String) (List (WithBounds Token))
idelex str
    = case lex ideTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (tok, (l, c, "")) => Right (filter notComment tok ++
                                      [MkBounded EndInput False l c l c])
           (_, fail) => Left fail
    where
      notComment : WithBounds Token -> Bool
      notComment t = case t.val of
                          Comment _ => False
                          _ => True

covering
sexp : Rule SExp
sexp
    = do symbol ":"; exactIdent "True"
         pure (BoolAtom True)
  <|> do symbol ":"; exactIdent "False"
         pure (BoolAtom False)
  <|> do i <- intLit
         pure (IntegerAtom i)
  <|> do str <- strLit
         pure (StringAtom str)
  <|> do symbol ":"; x <- unqualifiedName
         pure (SymbolAtom x)
  <|> do symbol "("
         xs <- many sexp
         symbol ")"
         pure (SExpList xs)

ideParser : {e : _} -> String -> Grammar Token e ty -> Either (ParseError Token) ty
ideParser str p
    = do toks   <- mapError LexFail $ idelex str
         parsed <- mapError toGenericParsingError $ parse p toks
         Right (fst parsed)

export
covering
parseSExp : String -> Either (ParseError Token) SExp
parseSExp inp
    = ideParser inp (do c <- sexp; eoi; pure c)


text:
module Main
import System.File

main : IO ()
main = do myFile <- openFile "out_string.txt" WriteTruncate
          case myFile of
              Right myFile => do fPutStr myFile "Alpha Beta"
                                 closeFile myFile
              Left err => printLn err


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html
module WebAssembly.Structure.Modules

import WebAssembly.Structure.Types

import public WebAssembly.Structure.Modules.Indices
import public WebAssembly.Structure.Modules.Functions
import public WebAssembly.Structure.Modules.Tables
import public WebAssembly.Structure.Modules.Memories
import public WebAssembly.Structure.Modules.Globals
import public WebAssembly.Structure.Modules.ElementSegments
import public WebAssembly.Structure.Modules.DataSegments
import public WebAssembly.Structure.Modules.StartFunction
import public WebAssembly.Structure.Modules.Exports
import public WebAssembly.Structure.Modules.Imports

import Decidable.Equality

||| Spec: https://webassembly.github.io/spec/core/syntax/modules.html#modules
public export
record Module where
  constructor MkModule
  types    : List FuncType
  funcs    : List Func
  tables   : List Table
  mems     : List Mem
  globals  : List Global
  elem     : List Elem
  wdata    : List Data
  start    : Maybe Start
  imports  : List Import
  exports  : List Export

-- Equality

total public export
lemma_module__types_injective : ((ty1 = ty2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__types_injective ty1_not_ty2 Refl = ty1_not_ty2 Refl

total public export
lemma_module__funcs_injective : ((fu1 = fu2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__funcs_injective fu1_not_fu2 Refl = fu1_not_fu2 Refl

total public export
lemma_module__tables_injective : ((ta1 = ta2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__tables_injective ta1_not_ta2 Refl = ta1_not_ta2 Refl

total public export
lemma_module__mems_injective : ((me1 = me2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__mems_injective me1_not_me2 Refl = me1_not_me2 Refl

total public export
lemma_module__globals_injective : ((gl1 = gl2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__globals_injective gl1_not_gl2 Refl = gl1_not_gl2 Refl

total public export
lemma_module__elem_injective : ((el1 = el2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__elem_injective el1_not_el2 Refl = el1_not_el2 Refl

total public export
lemma_module__data_injective : ((da1 = da2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__data_injective da1_not_da2 Refl = da1_not_da2 Refl

total public export
lemma_module__start_injective : ((st1 = st2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__start_injective st1_not_st2 Refl = st1_not_st2 Refl

total public export
lemma_module__imports_injective : ((im1 = im2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__imports_injective im1_not_im2 Refl = im1_not_im2 Refl

total public export
lemma_module__exports_injective : ((ex1 = ex2) -> Void)
  -> ( MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1
     = MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
  -> Void
lemma_module__exports_injective ex1_not_ex2 Refl = ex1_not_ex2 Refl

-- Decidable Equality

public export
implementation DecEq Module where
  decEq (MkModule ty1 fu1 ta1 me1 gl1 el1 da1 st1 im1 ex1) (MkModule ty2 fu2 ta2 me2 gl2 el2 da2 st2 im2 ex2)
    = case decEq ty1 ty2 of
      No ty1_not_ty2 => No $ lemma_module__types_injective ty1_not_ty2
      Yes Refl       => case decEq fu1 fu2 of
        No fu1_not_fu2 => No $ lemma_module__funcs_injective fu1_not_fu2
        Yes Refl       => case decEq ta1 ta2 of
          No ta1_not_ta2 => No $ lemma_module__tables_injective ta1_not_ta2
          Yes Refl       => case decEq me1 me2 of
            No me1_not_me2 => No $ lemma_module__mems_injective me1_not_me2
            Yes Refl       => case decEq gl1 gl2 of
              No gl1_not_gl2 => No $ lemma_module__globals_injective gl1_not_gl2
              Yes Refl       => case decEq el1 el2 of
                No el1_not_el2 => No $ lemma_module__elem_injective el1_not_el2
                Yes Refl       => case decEq da1 da2 of
                  No da1_not_da2 => No $ lemma_module__data_injective da1_not_da2
                  Yes Refl       => case decEq st1 st2 of
                    No st1_not_st2 => No $ lemma_module__start_injective st1_not_st2
                    Yes Refl       => case decEq im1 im2 of
                      No im1_not_im2 => No $ lemma_module__imports_injective im1_not_im2
                      Yes Refl       => case decEq ex1 ex2 of
                        No ex1_not_ex2 => No $ lemma_module__exports_injective ex1_not_ex2
                        Yes Refl      => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module subway

%default partial

data Subway : Type where
  Sub : List Subway -> Subway

Eq Subway where
  (Sub ls) == (Sub ls') = ls  == ls'

Ord Subway where
  compare (Sub ls) (Sub ls') = compare ls ls'

fromChars : Subway -> List Subway -> List Char -> Subway
fromChars _ [root] [] = root
fromChars cur@(Sub ys) stack ('0' :: xs) =
  let newSub = Sub []
  in fromChars newSub (Sub (newSub :: ys) :: stack) xs
fromChars cur@(Sub ys) (sub :: subs) ('1' :: xs) =
  fromChars sub subs xs

fromString : String -> Subway
fromString = fromChars (Sub []) [] . unpack

canonical : Subway -> Subway
canonical (Sub ss) = Sub $ sort (map canonical ss)

-- traverseSub : Subway -> List Char
-- traverseSub sub = traverseSub' sub []
--   where
--     traverseSub' : Subway -> Maybe Subway -> List Char -> List Char
--     traverseSub' (Sub [])
-- toString : Subway -> String
-- toString  = pack . traverseSub . canonical

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
||| Utilities for Language.Reflection.Refined
module Language.Reflection.Refined.Util

import public Data.Maybe
import public Data.So

%default total

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export
maybeSo : (b : Bool) -> Maybe (So b)
maybeSo True  = Just Oh
maybeSo False = Nothing

public export
refineSo :  {f : a -> Bool}
         -> (make : (v : a) -> (0 prf : So $ f v) -> b)
         -> (val : a)
         -> Maybe b
refineSo make val = case maybeSo (f val) of
                         Just oh => Just $ make val oh
                         Nothing => Nothing


text:
> module List.DecIn
> import Data.List
> %access public export

A type can have decidable list membership:

> ||| Decision procedures for determining list membership.
> interface DecIn (t: Type) where
>     decIn: (x:t) -> (xs : List t) -> Dec (Elem x xs)

Decidable equality and decidable list membership are equivalent. The first half
of the proof is quite easy - if we have decidable list membership, then
deciding $x=y$ can be solved by determining $`DecIn` x [y]$.

> ||| Given an implementation of DecIn t, t has decidable equality.
> ||| Note: the implementation must be named due to a bug in Idris 1,
> ||| see (#4296)[https://github.com/idris-lang/Idris-dev/issues/4296]
> [decInToDecEqImpl] DecIn t => DecEq t where
>       decEq x y = case (decIn x [y]) of
>                        Yes Here => Yes Refl
>                        No contra => No (\eq => contra (rewrite eq in Here))

For the second half of the equivalence, we will need a trivial helper lemmas:

> matchingSingleton : Data.List.Elem x [y] -> (x = y)
> matchingSingleton Here = Refl
> matchingSingleton (There later) impossible

Using this, proving decidable equality gives decidable list memership is a bit
intricate, but mostly straightforward. The small difficulty arises from the fact
that, when deciding list membership, we traverse the list head-to-tail, but the
Idris prelude `Elem` goes from tail-to-head (building up `There` and `Here`
calls). So we will need to make a recursive call on the tail of the list.

Note: perhaps this can be cleaned up a bit, it seems rather circuitous.

> DecEq t => DecIn t where
>   decIn x [] = No absurd
>   decIn x (y::ys) with (decIn x ys)
>       decIn x (y::ys) | No notLater = case decEq x y of
>           Yes Refl => Yes Here
>           No contra => No (\later =>
>                           case later of
>                               Here => contra (matchingSingleton Here)
>                               (There t) => notLater t)
>       decIn x (y::ys) | Yes later = Yes (There later)

> ElementPreservingCorrespondence : DecIn t => List t -> List t -> Type
> ElementPreservingCorrespondence xs ys = (x : t) -> (Elem x xs -> Elem x ys, Elem x ys -> Elem x xs)

> ||| ElementPreservingCorrespondence is a reflexive relation on lists.
> elementPreservingCorrespondenceReflexive : DecIn t => {xs : List t} -> ElementPreservingCorrespondence xs xs
> elementPreservingCorrespondenceReflexive {xs=[]} _ = (\a => absurd a, \b => absurd b)
> elementPreservingCorrespondenceReflexive {xs = (y::ys)} x =
>   case decIn x (y::ys) of
>       Yes pf => (\a => pf,\b => pf)
>       No contra => (\a => absurd (contra a), \b => absurd (contra b))

> ||| ElementPreservingCorrespondence is a symmetric relation on lists.
> elementPreservingCorrespondenceSymmetric : DecIn t => {xs,ys : List t} -> ElementPreservingCorrespondence xs ys -> ElementPreservingCorrespondence ys xs
> elementPreservingCorrespondenceSymmetric pf x = (snd (pf x),fst (pf x))

> ||| ElementPreservingCorrespondence is a transitive relation on lists.
> elementPreservingCorrespondenceTransitive :
>       DecIn t => {xs,ys,zs : List t} ->
>       ElementPreservingCorrespondence xs ys ->
>       ElementPreservingCorrespondence ys zs ->
>       ElementPreservingCorrespondence xs zs
> elementPreservingCorrespondenceTransitive pf1 pf2 x =
>       ((fst (pf2 x)) . (fst (pf1 x)), (snd (pf1 x)) . (snd (pf2 x)))

ext: lidr

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
module RegExp.Types

import Data.List
import Decidable.Equality

||| A regular expression specification.
public export
data RegExp : (0 a : Type) -> Type where
  ||| Denotes the empty set
  Null : RegExp a
  ||| Denotes the empty string
  Empty : RegExp a
  ||| Denotes a single literal character
  Lit : a -> RegExp a
  ||| Denotes concatenation
  Cat : RegExp a -> RegExp a -> RegExp a
  ||| Denotes disjunction (OR)
  Disj : RegExp a -> RegExp a -> RegExp a
  ||| Denotes conjunction (AND)
  Conj : RegExp a -> RegExp a -> RegExp a
  ||| Denotes the Kleene star
  Star : RegExp a -> RegExp a

||| The property of a regular expression matching an input string.
public export
data Matches: RegExp a -> List a -> Type where
  ||| Rule: `[]` is in `Empty`
  InEmpty : Matches Empty []
  ||| Rule: `[x]` is in `Lit x`
  InLit : {x : a} -> Matches (Lit x) [x]
  ||| Rule: If `xs` is in regular expressions `r` and `ys` is in regular expression `s`, then
  ||| `xs ++ ys` is in `Cat r s`
  InCat : {xs : List a} ->
          {ys : List a} ->
          {zs : List a} ->
          {r : RegExp a} ->
          {s : RegExp a} ->
          (p : zs = xs ++ ys) ->
          Matches r xs ->
          Matches s ys ->
          Matches (Cat r s) zs
  ||| Rule: If `xs` is in regular expression `r`, then `xs` is in `Disj r _` (i.e. left side)
  InDisjL : {xs : List a} ->
            {r : RegExp a} ->
            {s : RegExp a} ->
            Matches r xs ->
            Matches (Disj r s) xs
  ||| Rule: If `xs` is in regular expression `s`, then `xs` is in `Disj _ s` (i.e. right side)
  InDisjR : {xs : List a} ->
            {r : RegExp a} ->
            {s: RegExp a} ->
            Matches s xs ->
            Matches (Disj r s) xs
  ||| Rule: If `xs` is in regular expressions `r` and `s`, then `xs` is in `Conj r s`
  InConj : {xs : List a} ->
           {r : RegExp a} ->
           {s : RegExp a} ->
           Matches r xs ->
           Matches s xs ->
           Matches (Conj r s) xs
  ||| Rule: For all regular expression `r`, the empty string is in `Star r`.
  InStarZ : {r: RegExp a} ->
            Matches (Star r) []
  ||| Rule: If `xs` is in regular expression `r` and `ys` is in `Star r`, then `xs ++ ys` is also
  ||| in `Star r`.
  InStarS : {xs : List a} ->
            {ys : List a} ->
            {zs : List a} ->
            {r : RegExp a} ->
            (p : zs = xs ++ ys) ->
            Matches r xs ->
            Matches (Star r) ys ->
            Matches (Star r) (xs ++ ys)

export
Uninhabited (Matches Null xs) where
  uninhabited _ impossible

export
Uninhabited (Matches Empty (x::xs)) where
  uninhabited _ impossible

export
Uninhabited (Matches (Lit x) []) where
  uninhabited _ impossible

----------------------------------------------------------------------------------------------------
-- Interface Implementations                                                                      --
----------------------------------------------------------------------------------------------------

export
DecEq a => DecEq (RegExp a) where
  decEq Null Null = Yes Refl
  decEq (Lit x) (Lit y) with (decEq x y)
    decEq (Lit x) (Lit x) | (Yes Refl)  = Yes Refl
    decEq (Lit x) (Lit y) | (No contra) = No $ \p => case p of
                                                     Refl => contra Refl
  decEq (Cat r s) (Cat t u) with (decEq r t)
    decEq (Cat r s) (Cat r u) | (Yes Refl) with (decEq s u)
      decEq (Cat r s) (Cat r s) | (Yes Refl) | (Yes Refl) = Yes Refl
      decEq (Cat r s) (Cat r u) | (Yes Refl) | (No contra) = No $ \p => case p of
                                                                             Refl => contra Refl
    decEq (Cat r s) (Cat t u) | (No contra) = No \p => case p of
                                                            Refl => contra Refl
  decEq (Disj r s) (Disj t u) with (decEq r t)
    decEq (Disj r s) (Disj r u) | (Yes Refl) with (decEq s u)
      decEq (Disj r s) (Disj r s) | (Yes Refl) | (Yes Refl)  = Yes Refl
      decEq (Disj r s) (Disj r u) | (Yes Refl) | (No contra) = No $ \p => case p of
                                                                               Refl => contra Refl
    decEq (Disj r s) (Disj t u) | (No contra) = No $ \p => case p of
                                                                Refl => contra Refl
  decEq (Conj r s) (Conj t u) with (decEq r t)
    decEq (Conj r s) (Conj r u) | (Yes Refl) with (decEq s u)
      decEq (Conj r s) (Conj r s) | (Yes Refl) | (Yes Refl)  = Yes Refl
      decEq (Conj r s) (Conj r u) | (Yes Refl) | (No contra) = No $ \p => case p of
                                                                               Refl => contra Refl
    decEq (Conj r s) (Conj t u) | (No contra) = No $ \p => case p of
                                                                Refl => contra Refl
  decEq (Star r) (Star s) with (decEq r s)
    decEq (Star r) (Star r) | (Yes Refl) = Yes Refl
    decEq (Star r) (Star s) | (No contra) = No $ \p => case p of
                                                            Refl => contra Refl
  -- This is plain old structural equality, so I figure it's better to use a `believe_me` catch-all
  -- than to write out a million trivial `No` cases.
  decEq _ _ = No believe_me

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

||| Proof that if the result of a concatenation is empty, then both inputs are empty
appendOutputNil : {xs : List a} ->
                  {ys : List a} ->
                  xs ++ ys = [] ->
                  (xs = [], ys = [])
appendOutputNil {xs=[]} {ys=[]}    p = (Refl, Refl)
appendOutputNil {xs=[]} {ys=y::ys} p = absurd p
appendOutputNil {xs=(x::xs)} {ys}  p = absurd p

||| Proof that if an `Empty` regular expression matches a string, then the string is empty.
export
emptyMatch_implies_emptyList : Matches Empty xs -> xs = []
emptyMatch_implies_emptyList InEmpty = Refl

||| Proof that for all `Lit x` matches, `x` is equal to the head of the string.
export
litMatches_implies_headEqual : DecEq a =>
                               {x : a} ->
                               {y : a} ->
                               {ys : List a} ->
                               Matches (Lit x) (y::ys) ->
                               x = y
litMatches_implies_headEqual {x} {y=x} {ys=[]} InLit = Refl

||| Proof that if `Lit` matches `x::xs`, then `xs = []`
export
litMatchesCons_implies_restEmpty : Matches (Lit x) (x::xs) -> xs = []
litMatchesCons_implies_restEmpty InLit = Refl

||| Proof that if the `Cat r s` matches empty, then both `r` and `s` also match empty
export
catNotEmpty : {r : RegExp a} ->
              {s : RegExp a} ->
              Matches (Cat r s) [] ->
              (Matches r [], Matches s [])
catNotEmpty (InCat p r s) with (appendOutputNil $ sym p)
  catNotEmpty (InCat p r s) | (Refl, Refl) = (r, s)

||| Proof that if `Disj r s` matches empty, then at least one of `r` and `s` matches empty
export
disjNotEmpty : {r : RegExp a} ->
               {s : RegExp a} ->
               Matches (Disj r s) [] ->
               Either (Matches r []) (Matches s [])
disjNotEmpty (InDisjL r) = Left r
disjNotEmpty (InDisjR r) = Right r

||| Proof that if the `Conj r s` matches empty, then both `r` and `s` also match empty
export
conjNotEmpty : {r : RegExp a} ->
               {s : RegExp a} ->
               Matches (Conj r s) [] ->
               (Matches r [], Matches s [])
conjNotEmpty (InConj r s) = (r, s)

max_stars_repo_name: polendri/idris-regex

max_issues_repo_name: polendri/idris-regex

max_forks_repo_name: polendri/idris-regexp


text:
module Lemmas

import Data.Nat
import Data.Vect
import Decidable.Equality
import Injection
import Complex

%default total

export
lemmaplusOneRight : (n : Nat) -> n + 1 = S n
lemmaplusOneRight n = rewrite plusCommutative n 1 in Refl

export
lemmaPlusSRight : (n : Nat) -> (k : Nat) -> plus n (S k) = S (plus n k)
lemmaPlusSRight Z     k = Refl
lemmaPlusSRight (S p) k = rewrite lemmaPlusSRight p k in Refl

--LEMMAS ABOUT &&

export
lemmaAndLeft : {a : Bool} -> {b : Bool} -> (a && b = True) -> (a = True)
lemmaAndLeft {a = True} {b} p =  Refl
lemmaAndLeft {a = False} {b} p impossible

export
lemmaAndRight : {a : Bool} -> {b : Bool} -> (a && b = True) -> (b = True)
lemmaAndRight {a} {b = True} p = Refl
lemmaAndRight {a = True} {b = False} p impossible
lemmaAndRight {a = False} {b = False} p impossible

export
lemmaAnd : {a : Bool} -> {b : Bool} -> (a = True) -> (b = True) -> (a && b = True)
lemmaAnd {a = True} {b = True} p1 p2 = Refl

--LEMMAS ABOUT <, >, =, /=, <=, >= : TRANSITIVITY
export
lemmaTransLTELT : (i : Nat) -> (n : Nat) -> (p : Nat) -> (i <= n) = True -> (n < p) = True -> (i < p) = True
lemmaTransLTELT 0 0 (S k) _ _ = Refl
lemmaTransLTELT 0 (S k) (S j) _ _ = Refl
lemmaTransLTELT (S k) (S n) (S p) prf1 prf2 = rewrite lemmaTransLTELT k n p prf1 prf2 in Refl

export
lemmaTransLTLTE : (i : Nat) -> (n : Nat) -> (p : Nat) -> (i < n) = True -> (n <= p) = True -> (i < p) = True
lemmaTransLTLTE 0 (S n) (S k) prf prf1 = Refl
lemmaTransLTLTE (S k) (S n) (S p) prf prf1 = rewrite lemmaTransLTLTE k n p prf prf1 in Refl

export
lemmaTransitivity : (i : Nat) -> (n : Nat) -> (p : Nat) -> (i < n) = True -> (n < p) = True -> (i < p) = True
lemmaTransitivity 0 (S k) (S m) prf prf1 = Refl
lemmaTransitivity (S k) (S m) (S l) prf prf1 = lemmaTransitivity k m l prf prf1

--BASIC LEMMAS ABOUT <, >, =, /=, <=, >=

export
lemmaLTERefl : (n : Nat) -> (n <= n) = True
lemmaLTERefl 0 = Refl
lemmaLTERefl (S k) = lemmaLTERefl k

export
lemmaSymDiff : {x : Nat} -> {y : Nat} -> (x /= y) = True -> (y /= x) = True
lemmaSymDiff {x = 0} {y = (S m)} _ = Refl
lemmaSymDiff {x = (S k)} {y = 0} _ = Refl
lemmaSymDiff {x = (S k)} {y = (S j)} prf = lemmaSymDiff {x = k} {y = j} prf

export
lemma0LTSucc : (k : Nat) -> 0 < S k = True
lemma0LTSucc k = Refl

export
lemma1LTESucc : (k : Nat) -> 1 <= S k = True
lemma1LTESucc 0 = Refl
lemma1LTESucc (S k) = Refl

export
lemmaLTEAddR : (n : Nat) -> (p : Nat) -> n <= (n + p) = True
lemmaLTEAddR Z 0 = Refl
lemmaLTEAddR Z (S k) = Refl
lemmaLTEAddR (S n) p = lemmaLTEAddR n p

export
lemmaLTEAddL : (n : Nat) -> (p : Nat) -> p <= (n + p) = True
lemmaLTEAddL n p = rewrite plusCommutative n p in lemmaLTEAddR p n

export
lemmaDiffSuccPlus : (k : Nat) -> (p : Nat) -> (k /= S (p + k)) = True
lemmaDiffSuccPlus 0 p = Refl
lemmaDiffSuccPlus (S k) j = rewrite sym $ plusSuccRightSucc j k in lemmaDiffSuccPlus k j

export
lemmaLTSuccPlus : (k : Nat) -> (p : Nat) -> (k < S (k + p)) = True
lemmaLTSuccPlus 0 p = Refl
lemmaLTSuccPlus (S k) j = lemmaLTSuccPlus k j

export
lemmaLTSucc : (k : Nat) -> (k < S k) = True
lemmaLTSucc 0 = Refl
lemmaLTSucc (S k) = lemmaLTSucc k

export
lemmakLTSk : (k : Nat) -> (S k) < S (k + 1) = True
lemmakLTSk k = rewrite lemmaplusOneRight k in lemmaLTSucc k

export
lemmaLTSuccLT : (k : Nat) -> (n : Nat) -> (S k) < n = True -> k < n = True
lemmaLTSuccLT k 0 prf impossible
lemmaLTSuccLT 0 (S j) prf = Refl
lemmaLTSuccLT (S k) (S j) prf = lemmaLTSuccLT k j prf

export
lemmaLTESuccLT : (k : Nat) -> (n : Nat) -> (S k) <= n = True -> k < n = True
lemmaLTESuccLT k 0 prf impossible
lemmaLTESuccLT 0 (S j) prf = Refl
lemmaLTESuccLT (S k) (S j) prf = lemmaLTESuccLT k j prf

export
lemmaLTESuccLTE : (k : Nat) -> (n : Nat) -> (S k) <= n = True -> k <= n = True
lemmaLTESuccLTE k 0 prf impossible
lemmaLTESuccLTE 0 (S j) prf = Refl
lemmaLTESuccLTE (S k) (S j) prf = lemmaLTESuccLTE k j prf

export
lemmaSuccsLT : (k : Nat) -> (n : Nat) -> (S k) < (S n) = True -> k < n = True
lemmaSuccsLT k n prf = prf

export
lemmaCompLT0 : (n : Nat) -> (j : Nat) -> {auto prf : j < n = True} -> 0 < n = True
lemmaCompLT0 n 0 {prf} = prf
lemmaCompLT0 (S p) (S k) = Refl

--LEMMAS USED BY THE APPLY FUNCTION
export
indexInjectiveVect : (j : Nat) -> (n : Nat) -> (v : Vect i Nat) ->
                     {prf : isInjective n v = True} -> {prf1 : j < i = True} ->
                     (index j v < n) = True
indexInjectiveVect Z n (x :: xs) {prf} = lemmaAndLeft (lemmaAndLeft prf)
indexInjectiveVect (S k) n (x :: xs) {prf} =
      indexInjectiveVect k n xs {prf = lemmaAnd (lemmaAndRight (lemmaAndLeft prf)) (lemmaAndRight (lemmaAndRight prf))}

export
different' : (x : Nat) -> (m : Nat) -> (xs : Vect i Nat) ->
             {prf1 : m < i = True} -> {prf2 : isDifferent x xs = True} ->
             (x /= index m xs) = True
different' x 0 (y :: xs) = lemmaAndLeft prf2
different' x (S k) (y :: xs) =
  different' x k xs {prf1} {prf2 = lemmaAndRight prf2}

private
different'' : (x : Nat) -> (m : Nat) -> (xs : Vect i Nat) ->
             {prf1 : m < i = True} -> {prf2 : isDifferent x xs = True} ->
             (index m xs /= x) = True
different'' x m xs = lemmaSymDiff (different' x m xs {prf1} {prf2})

export
differentIndexInjectiveVect : (c : Nat) -> (t : Nat) -> (n : Nat) -> {prf1 : (c /= t) = True} ->
                              (v : Vect i Nat) -> {prf2 : isInjective n v = True} ->
                              {prf3 : c < i = True} -> {prf4 : t < i = True} ->
                              (index c v /= index t v) = True
differentIndexInjectiveVect 0 (S m) n (x :: xs) =
      different' x m xs {prf1 = prf4} {prf2 = lemmaAndLeft (lemmaAndRight prf2)}
differentIndexInjectiveVect (S k) 0 n (x :: xs) =
      different'' x k xs {prf1 = prf3} {prf2 = lemmaAndLeft (lemmaAndRight prf2)}
differentIndexInjectiveVect (S k) (S j) n (x :: xs) =
  let p2 = lemmaAnd (lemmaAndRight (lemmaAndLeft prf2)) (lemmaAndRight (lemmaAndRight prf2)) in
  differentIndexInjectiveVect k j n {prf1} xs {prf2 = p2} {prf3} {prf4}

--LEMMAS USED BY THE CONTROLLED FUNCTION

export
lemmaControlledInj : (n : Nat) -> (j : Nat) -> {auto prf : j < n = True} -> isInjective (S n) [0, S j] = True
lemmaControlledInj 0 0 impossible
lemmaControlledInj 0 (S k) {prf} = prf
lemmaControlledInj (S k) 0 = Refl
lemmaControlledInj (S p) (S k) {prf} = lemmaControlledInj p k {prf}

export
lemmaControlledInj2 : (n : Nat) -> (c : Nat) -> (t : Nat) ->
                      {auto prf1 : (c < n) = True} -> {auto prf2 : (t < n) = True} -> {auto prf3 : (c /= t) = True} ->
                      isInjective (S n) [0, S c, S t] = True
lemmaControlledInj2 0 0 t impossible
lemmaControlledInj2 0 (S k) t {prf1} = prf1
lemmaControlledInj2 (S k) 0 0 {prf3} = prf3
lemmaControlledInj2 (S k) 0 (S j) = lemmaAnd (lemmaAnd prf2 Refl) Refl
lemmaControlledInj2 (S k) (S j) 0 = lemmaAnd (lemmaAnd prf1 Refl) Refl
lemmaControlledInj2 (S k) (S j) (S i) = lemmaControlledInj2 k j i {prf1} {prf2} {prf3}

--LEMMAS USED BY THE TENSOR FUNCTION
export
isDiffRangeVect : (k : Nat) -> (length : Nat) -> (p : Nat) -> isDifferent k (rangeVect (S (p + k)) length) = True
isDiffRangeVect k 0 _ = Refl
isDiffRangeVect k (S j) p =
  lemmaAnd (lemmaDiffSuccPlus k p) (isDiffRangeVect k j (S p))

export
allDiffRangeVect : (startIndex : Nat) -> (length : Nat) -> allDifferent (rangeVect startIndex length) = True
allDiffRangeVect startIndex 0 = Refl
allDiffRangeVect startIndex (S k) =
  let p1 = isDiffRangeVect startIndex k 0
  in lemmaAnd p1 (allDiffRangeVect (S startIndex) k)

export
allSmallerRangeVect : (startIndex : Nat) -> (length : Nat) -> allSmaller (rangeVect startIndex length) (startIndex + length) = True
allSmallerRangeVect startIndex 0 = Refl
allSmallerRangeVect startIndex (S k) =
  rewrite sym $ plusSuccRightSucc startIndex k in
          lemmaAnd (lemmaLTSuccPlus startIndex k) (allSmallerRangeVect (S startIndex) k)

export
allSmallerPlus : (n : Nat) -> (p : Nat) -> (v : Vect k Nat) -> allSmaller v n = True -> allSmaller v (n + p) = True
allSmallerPlus n p [] prf = Refl
allSmallerPlus n p (x :: xs) prf =
  let p1 = lemmaAndLeft prf
      p2 = lemmaTransLTLTE x n (n + p) p1 (lemmaLTEAddR n p)
      p3 = lemmaAndRight prf
  in lemmaAnd p2 (allSmallerPlus n p xs p3)

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Main

import Graph

test : Graph String String
test = ([("a", 0)], 1, "World", [("loop", 1)]) & ([], 0, "Hello", []) & empty

main : IO ()
main = putStrLn . graphToDot $ test

max_stars_repo_name: gpyh/idris-graph

max_issues_repo_name: gpyh/idris-graph

max_forks_repo_name: gpyh/idris-graph


text:
module Main

main : IO ()
main = putStrLn (cast 'x')

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris


text:
module Hedgehog.Internal.Gen

import Data.Colist
import Data.Cotree
import Data.Fin
import Data.List
import Data.List1
import Data.Nat
import Data.SOP
import Data.String
import Data.Tree
import Data.Vect

import Control.Monad.Maybe

import Hedgehog.Internal.Range
import Hedgehog.Internal.Seed
import Hedgehog.Internal.Shrink
import Hedgehog.Internal.Util

%hide Prelude.Range

%default total

--------------------------------------------------------------------------------
--          Random Value Generator with Integrated Shrinking
--------------------------------------------------------------------------------

||| Generates random values of type `a`
public export
record Gen (a : Type) where
  constructor MkGen
  unGen   : Size -> Seed -> Cotree a

public export %inline
runGen : Size -> Seed -> Gen a -> Cotree a
runGen si se g = unGen g si se

public export %inline
mapGen :  (f : Cotree a -> Cotree b) -> Gen a -> Gen b
mapGen f (MkGen run) = MkGen $ \si,se => f (run si se)

||| Lift a predefined shrink tree in to a generator, ignoring the seed and the
||| size.
public export %inline
fromTree : Cotree a -> Gen a
fromTree ct = MkGen $ \_,_ => ct

||| Observe a generator's shrink tree.
public export %inline
toTree : Gen a -> Gen (Cotree a)
toTree (MkGen unGen) = MkGen $ \si,se => pure (unGen si se)

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

public export
Functor Gen where
  map f (MkGen g) = MkGen $ \si,se => map f (g si se)

public export
Applicative Gen where
  pure a = MkGen $ \_,_ => pure a

  MkGen ff <*> MkGen fa =
    MkGen $ \si,se => let (se1,se2) = split se
                     in interleave (ff si se1) (fa si se2)

public export
Monad Gen where
  MkGen run >>= f =
    MkGen $ \si,se => let (se1,se2) = split se
                          ta        = run si se1
                       in bind ta (runGen si se2 . f)

--------------------------------------------------------------------------------
--          Combinators
--------------------------------------------------------------------------------

public export %inline
generate : (Size -> Seed -> a) -> Gen a
generate  f = MkGen $ \si,se => pure (f si se)

--------------------------------------------------------------------------------
--          Shrinking
--------------------------------------------------------------------------------

public export %inline
shrink : (a -> Colist a) -> Gen a -> Gen a
shrink f = mapGen (expand f)

public export %inline
prune : Gen a -> Gen a
prune = mapGen prune

--------------------------------------------------------------------------------
--          Size
--------------------------------------------------------------------------------

||| Construct a generator that depends on the size parameter.
public export %inline
sized : (Size -> Gen a) -> Gen a
sized f = generate (\si,_ => si) >>= f

||| Adjust the size parameter by transforming it with the given function.
public export %inline
scale : (Size -> Size) -> Gen a -> Gen a
scale f (MkGen run) = MkGen $ \si,se => run (f si) se

||| Override the size parameter. Returns a generator which uses the given size
||| instead of the runtime-size parameter.
public export %inline
resize : Size -> Gen a -> Gen a
resize size = scale (const size)

||| Scale a size using the golden ratio.
|||
|||   > golden x = x / φ
|||   > golden x = x / 1.61803..
public export %inline
golden : Size -> Size
golden = resize $ \n => round (0.61803398875 * cast n)

||| Make a generator smaller by scaling its size parameter.
public export %inline
small : Gen a -> Gen a
small = scale golden

--------------------------------------------------------------------------------
--          Integral
--------------------------------------------------------------------------------

||| Generates a random integral number in the [inclusive,inclusive] range.
|||
||| This generator does not shrink.
public export
integral_ : ToInteger a => Range a -> Gen a
integral_ range = generate $ \si,se =>
    let (x, y) = bounds si range
     in fromInteger . fst $ nextIntegerR (toInteger x, toInteger y) se

||| Generates a random integral number in the given @[inclusive,inclusive]@ range.
|||
||| When the generator tries to shrink, it will shrink towards the
||| 'Range.origin' of the specified 'Range'.
|||
||| For example, the following generator will produce a number between @1970@
||| and @2100@, but will shrink towards @2000@:
|||
||| ```
||| integral (Range.'Range.constantFrom' 2000 1970 2100) :: 'Gen' 'Int'
||| ```
|||
|||   Some sample outputs from this generator might look like:
|||
|||   > === Outcome ===
|||   > 1973
|||   > === Shrinks ===
|||   > 2000
|||   > 1987
|||   > 1980
|||   > 1976
|||   > 1974
|||
|||   > === Outcome ===
|||   > 2061
|||   > === Shrinks ===
|||   > 2000
|||   > 2031
|||   > 2046
|||   > 2054
|||   > 2058
|||   > 2060
|||
public export %inline
integral : ToInteger a => Range a -> Gen a
integral range = shrink (towards $ origin range) (integral_ range)

||| Generates a random machine integer in the given range.
|||
||| This is a specialization of `integral`, offered for convenience.
public export %inline
int : Range Int -> Gen Int
int = integral

||| Generates a random 8-bit integer in the given range.
|||
||| This is a specialization of `integral`, offered for convenience.
public export %inline
int8 : Range Int8 -> Gen Int8
int8 = integral

||| Generates a random 16-bit integer in the given range.
|||
||| This is a specialization of `integral`, offered for convenience.
public export %inline
int16 : Range Int16 -> Gen Int16
int16 = integral

||| Generates a random 32-bit integer in the given range.
|||
||| This is a specialization of `integral`, offered for convenience.
public export %inline
int32 : Range Int32 -> Gen Int32
int32 = integral

||| Generates a random 64-bit integer in the given range.
|||
||| This is a specialization of `integral`, offered for convenience.
public export %inline
int64 : Range Int64 -> Gen Int64
int64 = integral

||| Generates a random 8-bit integer in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
bits8 : Range Bits8 -> Gen Bits8
bits8 = integral

||| Generates a random 16-bit integer in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
bits16 : Range Bits16 -> Gen Bits16
bits16 = integral

||| Generates a random 32-bit integer in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
bits32 : Range Bits32 -> Gen Bits32
bits32 = integral

||| Generates a random 64-bit integer in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
bits64 : Range Bits64 -> Gen Bits64
bits64 = integral

||| Generates a random Integer in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
integer : Range Integer -> Gen Integer
integer = integral

||| Generates a random Nat in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
nat : Range Nat -> Gen Nat
nat = integral

||| Generates a random Size in the given range.
|||
||| This is a specialization of 'integral', offered for convenience.
public export %inline
size : Range Size -> Gen Size
size = integral

||| Generates a random (Fin n) in the given range.
public export %inline
fin : {n : _} -> Range (Fin n) -> Gen (Fin n)
fin range = let rangeInt = map finToInteger range
             in map toFin (integer rangeInt)
  where toFin : Integer -> Fin n
        toFin k = fromMaybe range.origin (integerToFin k n)

--------------------------------------------------------------------------------
--          Floating Point
--------------------------------------------------------------------------------

||| Generates a random fractional number in the [inclusive,exclusive) range.
|||
||| This generator does not shrink.
export %inline
double_ : Range Double -> Gen Double
double_ range = generate $ \si,se => let (x, y) = bounds si range
                                      in fst $ nextDoubleR x y se

||| Generates a random floating-point number in the given range.
|||
||| This generator works the same as 'integral', but for floating point numbers.
|||
export %inline
double : Range Double -> Gen Double
double range = shrink (towardsDouble $ origin range) (double_ range)

--------------------------------------------------------------------------------
--          Choice
--------------------------------------------------------------------------------

||| Trivial generator that always produces the same element.
|||
||| This is another name for `pure`.
public export %inline
constant : a -> Gen a
constant = pure

||| Randomly selects one of the elements in the vector.
|||
||| This generator shrinks towards the first element in the vector.
public export %inline
element : {k : _} -> Vect (S k) a -> Gen a
element vs = map (`index` vs) (fin $ constant FZ last)

||| Randomly selects one of the elements in the vector.
|||
||| This generator does not shrink.
public export %inline
element_ : {k : _} -> Vect (S k) a -> Gen a
element_ = prune . element

||| Randomly selects one of the generators in the vector.
|||
||| This generator shrinks towards the first generator in the vector.
public export %inline
choice : {k : _} -> Vect (S k) (Gen a) -> Gen a
choice vs = element vs >>= id

||| Randomly selects one of the generators in the vector.
|||
||| This generator does not shrink towards a particular
||| generator in the vector
public export %inline
choice_ : {k : _} -> Vect (S k) (Gen a) -> Gen a
choice_ vs = element_ vs >>= id

||| Uses a weighted distribution to randomly select one of the generators in
||| the vector.
|||
||| This generator shrinks towards the first generator in the vector.
|||
||| Note that if the given frequencies sum up to 0, the first element
||| of the vector
public export %inline
frequency : Vect (S k) (Nat, Gen a) -> Gen a
frequency ps =
  let acc    = scanl1 addFst $ map (mapFst toInteger) ps
      gen    = integral_ . constant 0 . fst $ last acc
      lower  = \n => takeWhile (< n) (fromFoldable $ map fst acc)

  in shrink lower gen >>= choose acc
  where addFst : (Integer,x) -> (Integer,x) -> (Integer,x)
        addFst (x,_) (y,v) = (x + y,v)

        choose : Vect n (Integer, Gen a) -> Integer -> Gen a
        choose []             _ = snd $ head ps
        choose ((i, v) :: ps) k = if i >= k then v else choose ps k

||| Generates a random boolean.
|||
||| This generator shrinks to `False`.
public export %inline
bool : Gen Bool
bool = element [False,True]

--------------------------------------------------------------------------------
--          Character
--------------------------------------------------------------------------------

||| Generates a character in the given `Range`.
|||
||| Shrinks towards the origin of the range.
export %inline
char : Range Char -> Gen Char
char = map chr . int . map ord

||| Generates a character in the interval [lower,uppper].
|||
||| Shrinks towards the lower value.
export %inline
charc : (lower : Char) -> (upper : Char) -> Gen Char
charc l u = char $ constant l u

||| Generates an ASCII binit: `'0'..'1'`
export %inline
binit : Gen Char
binit = charc '0' '1'

||| Generates an ASCII octit: `'0'..'7'`
export %inline
octit : Gen Char
octit = charc '0' '7'

||| Generates an ASCII digit: `'0'..'9'`
export %inline
digit : Gen Char
digit = charc '0' '9'

||| Generates an ASCII hexit: `'0'..'9', 'a'..'f', 'A'..'F'`
export %inline
hexit : Gen Char
hexit = frequency [(10, digit),(6, charc 'a' 'z'),(6, charc 'A' 'Z')]

||| Generates an ASCII lowercase letter: `'a'..'z'`
export %inline
lower : Gen Char
lower = charc 'a' 'z'

||| Generates an ASCII uppercase letter: `'A'..'Z'`
export %inline
upper : Gen Char
upper = charc 'A' 'Z'

||| Generates an ASCII letter: `'a'..'z', 'A'..'Z'`
export %inline
alpha : Gen Char
alpha = choice [lower,upper]

||| Generates an ASCII letter or digit: `'a'..'z', 'A'..'Z', '0'..'9'`
export %inline
alphaNum : Gen Char
alphaNum = frequency [(10,digit),(24,lower),(24,upper)]

||| Generates an ASCII character: `'\0'..'\127'`
export %inline
ascii : Gen Char
ascii = charc '\0' '\127'

||| Generates an printable ASCII character: `'\32'..'\126'`
||| Note: This includes the space character but no
|||       line breaks or tabs
export %inline
printableAscii : Gen Char
printableAscii = charc '\32' '\126'

||| Generates a latin character: `'\0'..'\255'`
export %inline
latin : Gen Char
latin = charc '\0' '\255'

||| Generates a printable latin character: `'\32'..'\126'` and `'\160'..'\255'`
export %inline
printableLatin : Gen Char
printableLatin = frequency [ (95, printableAscii), (96, charc '\160' '\255') ]

||| Generates a Unicode character, excluding noncharacters
||| and invalid standalone surrogates:
||| `'\0'..'\1114111'` (excluding '\55296'..'\57343', '\65534', '\65535')`
export %inline
unicode : Gen Char
unicode = frequency [ (55296, charc '\0' '\55295')
                    , (8190, charc '\57344' '\65533')
                    , (1048576, charc '\65536' '\1114111')
                    ]

||| Generates a Unicode character, including noncharacters
||| and invalid standalone surrogates: `'\0'..'\1114111'`
export %inline
unicodeAll : Gen Char
unicodeAll = charc '\0' '\1114111'

--------------------------------------------------------------------------------
--          Containers
--------------------------------------------------------------------------------

||| Generates a 'Nothing' some of the time.
export %inline
maybe : Gen a -> Gen (Maybe a)
maybe gen = sized $ \s => frequency [ (2, constant Nothing)
                                    , (S s.size, Just <$> gen)
                                    ]

||| Generates either an 'a' or a 'b'.
|||
||| As the size grows, this generator generates @Right@s more often than @Left@s.
export %inline
either : Gen a -> Gen b -> Gen (Either a b)
either genA genB = sized $ \s => frequency [ (2, Left <$> genA)
                                           , (S s.size, Right <$> genB)
                                           ]
||| Generates either an 'a' or a 'b', without bias.
|||
||| This generator generates as many @Right@s as it does @Left@s.
export %inline
either_ : Gen a -> Gen b -> Gen (Either a b)
either_ genA genB = choice [Left <$> genA, Right <$> genB]

||| Generates a list using a 'Range' to determine the length.
export %inline
vect : (n : Nat) -> Gen a -> Gen (Vect n a)
vect 0     _ = pure []
vect (S k) g = [| g :: vect k g |]

||| Generates a list using a 'Range' to determine the length.
export %inline
list : Range Nat -> Gen a -> Gen (List a)
list range gen =
  sized $ \si => let minLength = lowerBound si range
                  in  mapGen (interleave minLength . value)
                    $ integral_ range >>= (\n => map toList (vect n (toTree gen)))
||| Generates a non-empty list using a `Range` to determine the length.
export %inline
list1 : Range Nat -> Gen a -> Gen (List1 a)
list1 range gen = [| gen ::: list (map pred range) gen |]

||| Generates a string using 'Range' to determine the length.
export %inline
string : Range Nat -> Gen Char -> Gen String
string range = map fastPack . list range

--------------------------------------------------------------------------------
--          SOP
--------------------------------------------------------------------------------

collapseNPV : NP (K a) ks -> {auto 0 _ : NonEmpty ks} -> (k ** Vect (S k) a)
collapseNPV {ks = _} [] impossible
collapseNPV {ks = _} (v::[]) = (0 ** [v])
collapseNPV {ks = t::t2::ts}(v::v2::vs) =
  let (k ** vs2) = collapseNPV {ks = t2 :: ts} (v2 :: vs)
   in (S k ** (v :: vs2))

||| Turns an n-ary product of generators into a generator
||| of n-ary products of the same type.
export %inline
np : NP Gen ts -> Gen (NP I ts)
np = sequenceNP

||| Turns an n-ary product of generators into a generator
||| of n-ary sums of the same type. This is a generalisation
||| of choice and shrinks towards the first sum type
||| in the list.
export %inline
ns : NP Gen ts -> {auto 0 prf : NonEmpty ts} -> Gen (NS I ts)
ns np = let (_ ** vs) = collapseNPV (apInjsNP_ np)
         in choice (map sequenceNS vs)

||| Turns an n-ary product of generators into a generator
||| of n-ary sums of the same type. This is a generalisation
||| of `choice_` and does not shrink towards a particular
||| sum type.
export %inline
ns_ : NP Gen ts -> {auto 0 prf : NonEmpty ts} -> Gen (NS I ts)
ns_ np = let (_ ** vs) = collapseNPV (apInjsNP_ np)
         in choice_ (map sequenceNS vs)

export %inline
sop : POP Gen tss -> {auto 0 prf : NonEmpty tss} -> Gen (SOP I tss)
sop p = let (_ ** vs) = collapseNPV {a = SOP Gen tss} (apInjsPOP_ p)
         in choice (map sequenceSOP vs)

--------------------------------------------------------------------------------
--          Sampling
--------------------------------------------------------------------------------

||| Print the value produced by a generator, and the first level of shrinks,
||| for the given size and seed.
|||
||| Use 'print' to generate a value from a random seed.
export
printWith : (HasIO io, Show a) => Size -> Seed -> Gen a -> io ()
printWith si se gen = let (MkCotree v fo) = runGen si se gen
                          shrinks         = value <$> take 1000 fo
                       in do putStrLn "=== Outcome ==="
                             putStrLn (show v)
                             putStrLn "=== Shrinks ==="
                             traverse_ printLn shrinks
||| Run a generator with a random seed and print the outcome, and the first
||| level of shrinks.
|||
||| @
||| Gen.print (Gen.'enum' \'a\' \'f\')
||| @
|||
|||   > === Outcome ===
|||   > 'd'
|||   > === Shrinks ===
|||   > 'a'
|||   > 'b'
|||   > 'c'
export
print : (HasIO io, Show a) => Gen a -> io ()
print gen = initSMGen >>= \se => printWith 100 se gen

||| Generate a sample from a generator.
export
sample : HasIO io => Gen a -> io a
sample gen = (value . gen.unGen 100) <$> initSMGen

||| Render the shrink tree produced by a generator, for the given size and
||| seed up to the given depth and width.
export
renderTree :  Show a
           => (maxDepth : Nat)
           -> (maxWidth : Nat)
           -> Size
           -> Seed
           -> Gen a
           -> String
renderTree md mw si se = drawTree
                       . map show
                       . toTree md mw
                       . runGen si se

||| Print the shrink tree produced by a generator, for the given size and
||| seed.
|||
||| Use 'printTree' to generate a value from a random seed.
export
printTreeWith :  (HasIO io, Show a)
              => (maxDepth : Nat)
              -> (maxWidth : Nat)
              -> Size
              -> Seed
              -> Gen a
              -> io ()
printTreeWith md mw si se = putStrLn . renderTree md mw si se

||| Run a generator with a random seed and print the resulting shrink tree.
|||
||| @
||| Gen.printTree (Gen.'enum' \'a\' \'f\')
||| @
|||
|||   > 'd'
|||   >  ├╼'a'
|||   >  ├╼'b'
|||   >  │  └╼'a'
|||   >  └╼'c'
|||   >     ├╼'a'
|||   >     └╼'b'
|||   >        └╼'a'
|||
|||   /This may not terminate when the tree is very large./
|||
export
printTree :  (HasIO io, Show a)
          => (maxDepth : Nat)
          -> (maxWidth : Nat)
          -> Gen a
          -> io ()
printTree md mw gen = initSMGen >>= \se => printTreeWith md mw 100 se gen


text:
module VectMissing

import Data.Fin
import Data.Vect

export
shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys) Here = ys
shrink (y :: []) (There p) = absurd p
shrink (y :: (x :: xs)) (There p) = y :: shrink (x :: xs) p

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Twicer

import RealizedFunction

%default total

-- Realized twicer
public export
twicer : Int -> Int
twicer = (*2)

public export
twicer_attrs : RealizedAttributes
twicer_attrs = MkRealizedAttributes (MkCosts 200 20 2) 0.9

public export
rlz_twicer : RealizedFunction (Int -> Int) Twicer.twicer_attrs
rlz_twicer = MkRealizedFunction twicer twicer_attrs

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
--
-- The Computer Language Benchmarks Game
-- https://salsa.debian.org/benchmarksgame-team/benchmarksgame/
--
-- Contributed by Don Stewart
-- *reset*
--
-- import System.Environment
import Data.Bits
-- import Text.Printf

--
-- an artificially strict tree.
--
-- normally you would ensure the branches are lazy, but this benchmark
-- requires strict allocation.
--
data Tree = Nil | Node Int Tree Tree

minN : Int
minN = 4

-- io s n t = printf "%s of depth %d\t check: %d\n" s n t
-- io : String -> Int -> Int -> IO ()
-- io s n t = putStrLn (s ++ " of depth " ++ (show d) ++ "\t check: " ++ (show t))

-- traverse the tree, counting up the nodes
ccheck : Tree -> Int
ccheck Nil          = 0
ccheck (Node i l r) = 1 + ccheck l + ccheck r

-- build a tree
make : Int -> Int -> Tree
make i 0 = Node i Nil Nil
make i d = Node i (make d d2) (make d2 d2)
  where d2 = d-1

-- allocate and check lots of trees
sumT : Int -> Int -> Int -> Int
sumT d 0 t = t
sumT d i t = sumT d (i-1) (t + a)
  where a = ccheck (make 0 d)

-- generate many trees
depth : Int -> Int -> List (Int, Int, Int)
depth d m =
    if d <= m then (n, d, (sumT d n 0)) :: depth (d+2) m
    else []
    where n = 2 * (m - d + minN)

main : IO ()
main = do
    -- n <- getArgs >>= readIO . head
    let n = 25
    let maxN     = max (minN + 2) n
    let stretchN = maxN + 1

    -- stretch memory tree
    let c = ccheck (make 0 stretchN)
    -- io "stretch tree" stretchN c

    -- allocate a long lived tree
    let long    = make 0 maxN

    -- allocate, walk, and deallocate many bottom-up binary trees
    let vs = depth minN maxN
    -- traverse (\ (m,d,i) => io (show m ++ "\t trees") d i) vs
    traverse_ (putStrLn . show) vs

    -- confirm the the long-lived binary tree still exists
    -- io "long lived tree" maxN (ccheck long)

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Remotelib1

export
rem1 : String
rem1 = "More strings"

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
module Depling.Decr

import Depling
import Depling.Incr
import Utils
import Data.Fin
import Data.Vect

mutual
	total
	decr_ℙ : Fin (S n) -> DAST n -> DAST (a + (S n)) -> DAST (a + n)
	decr_ℙ {a = Z} rv ra ast = decr rv ra ast
	decr_ℙ {a = S a} {n} rv ra ast = assert_total $ replace (sym $ plusSuccRightSucc _ _) $ decr_ℙ (FS rv) (incr 0 ra) $ replace (plusSuccRightSucc _ _) ast

	total
	export
	decr : Fin (S n) -> DAST n -> DAST (S n) -> DAST n
	decr rv ra (ʌ v) = case fcompare v rv of
		FLT lt => ʌ $ finDown v {lt}
		FEQ eq => ra
		FGT gt => ʌ $ finD v {gt}
	decr rv ra (λ at b) = λ (decr rv ra at) (decr (FS rv) (incr FZ ra) b)
	decr rv ra (λT at rt) = λT (decr rv ra at) (decr (FS rv) (incr FZ ra) rt)
	decr rv ra (f =!= a) = decr rv ra f =!= decr rv ra a
	decr rv ra 𝕋 = 𝕋
	decr rv ra (𝔽 at rt b) =
		𝔽
			(decr (        rv) (                    ra) at)
			(decr (    FS$ rv) (          incr FZ $ ra) rt)
			(decr (FS$ FS$ rv) (incr FZ $ incr FZ $ ra) b )
	decr rv ra (𝕌 n t) = 𝕌 n $ decr rv ra t
	decr rv ra (ℂ cn as) = assert_total $ ℂ cn $ map (decr rv ra) as
	decr rv ra (ℙ v cn t f) = ℙ (decr rv ra v) cn (decr_ℙ rv ra t) (decr rv ra f)
	decr rv ra (𝔹 t) = 𝔹 $ decr rv ra t

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Main
import Effects
import SQLite
import CgiTypes

-- We could also have SQLITE, or CGI here perhaps
sampleHandler : Maybe String -> Maybe Int -> Maybe Int -> FormHandler [CGI (InitialisedCGI TaskRunning)] Bool
sampleHandler (Just name) (Just age) (Just num) = ((output ("Your name is " ++ name
              ++ " and you are " ++ (show age) ++ " years old. You selected: " ++ (show num))) >>= (\_ pure True))
sampleHandler _ _ _ = output "There was an error processing input data." >>= (\_ => pure False)

-- Effects.>>= : (EffM m xs xs' a) -> (a -> EffM m xs' xs'' b) -> EffM xs xs'' b
-- addTextBox str >>= addTextBox int : EffM m [] [FormString] () -> EffM m [FormString] [FormInt, FormString] () -> EffM m [] [FormInt, FormString]
myForm : UserForm
myForm = do addTextBox FormString "Simon"
            addTextBox FormInt 21
            addSelectionBox FormInt [1,2,3,4] ["One", "Two", "Three", "Four"]
            addSubmit sampleHandler [CgiEffect] FormBool
  --(addTextBox FormString "Simon") >>= ((\_ => addTextBox FormInt 21) >>= (\_ => addSubmit sampleHandler))

main : IO ()
main = do let ser_form = mkForm "myform" myForm
          putStrLn ser_form

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Dart.FFI.Upcast

||| Instances of type [subType] can be [upcast] to type [superType].
public export
interface IsAssignableFrom superType subType where

%inline
export
upcast : {0 subType : Type}
  -> {0 superType : Type}
  -> subType
  -> IsAssignableFrom superType subType
  => superType
upcast sub = believe_me sub

%inline
public export
IsAssignableFrom superType subType => Cast subType superType where
  cast sub = upcast sub

||| Every type is assignable from itself.
export
IsAssignableFrom a a where

-- public export
-- (IsAssignableFrom a b, IsAssignableFrom b c) => IsAssignableFrom a c where

public export
data UpcastList : Type -> Type where
  MkUpcastList : List element -> UpcastList element

namespace UpcastList

  %inline
  export
  Nil : UpcastList _
  Nil = MkUpcastList []

  %inline
  export
  (::) : IsAssignableFrom element ty => ty -> UpcastList element -> UpcastList element
  (::) e (MkUpcastList es) = MkUpcastList (upcast e :: es)

  %inline
  export
  toList : UpcastList element -> List element
  toList (MkUpcastList es) = es


text:
module Main

import Effects
import Effect.SDL
import Effect.State
import Effect.StdIO
import Effect.File

import Grid
import GridSDL
import GridIO

data PlayStatus
    = Playing
    | Paused
    | Step

implementation Eq PlayStatus where
    Playing == Playing = True
    Paused  == Paused  = True
    Step    == Step    = True
    _       == _       = False

NavigateStatus : Type
NavigateStatus = (Int, Int)

data IOStatus
    = NoIO
    | WantRead
    | WantWrite

implementation Eq IOStatus where
    NoIO      == NoIO      = True
    WantRead  == WantRead  = True
    WantWrite == WantWrite = True
    _         == _         = False

config : Config
config = MkConfig 640 480

Prog : Type -> Type -> Type
Prog i t = Eff t
    [ SDL i
    , 'Grid ::: STATE Grid
    , 'GridWindow ::: STATE GridWindow
    , 'PlayStatus ::: STATE PlayStatus
    , 'NavigateStatus ::: STATE NavigateStatus
    , 'IOStatus ::: STATE IOStatus
    , 'Frames ::: STATE Integer
    , STDIO
    , FILE ()
    ]

Running : Type -> Type
Running t = Prog SDLSurface t

resetState : Running ()
resetState = do
    'Grid :- put (MkGrid 0 0 128 96 (fromList [(1, 1), (1, 2), (2, 1), (3, 4), (4, 3), (4, 4)]))
    'GridWindow :- put (MkGridWindow 0 0 32 24)
    'PlayStatus :- put Paused
    'NavigateStatus :- put (0, 0)
    'IOStatus :- put NoIO

greeting : String
greeting = """Controls:
  ARROW KEYS — pan;
  =          — zoom in;
  -          — zoom out;

  SPACE      — play / pause;
  n          — next generation;

  c          — reset grid;
  r I        — read grid number 'I';
  w I        — save current grid by number 'I';
  u          — cancel I/O operation.

Sample grid is saved by number '1'.
"""

emain : Prog () ()
emain = do
    putStr greeting
    initialise (width config) (height config)
    resetState
    eventLoop
    quit
  where
    processIOAction : Char -> Running Bool
    processIOAction c = do
        ioStatus <- 'IOStatus :- get
        'IOStatus :- put NoIO

        when (ioStatus == WantRead) $ do
            resetState
            Success <- open ("data/" ++ pack [c] ++ ".life") Read | FError err => pure ()
            grid <- readGrid 128 96
            'Grid :- put grid
            close

        when (ioStatus == WantWrite) $ do
            Success <- open ("data/" ++ pack [c] ++ ".life") WriteTruncate | FError err => pure ()
            grid <- 'Grid :- get
            writeGrid grid
            close

        pure True

    -- TODO get rid of copy-paste
    process : Maybe Event -> Running Bool
    process (Just AppQuit) = pure False

    -- I/O
    process (Just (KeyDown (KeyAny 'c'))) = do
        resetState
        pure True
    process (Just (KeyDown (KeyAny 'u'))) = do
        'IOStatus :- put NoIO
        pure True
    process (Just (KeyDown (KeyAny 'r'))) = do
        'IOStatus :- put WantRead
        pure True
    process (Just (KeyDown (KeyAny 'w'))) = do
        'IOStatus :- put WantWrite
        pure True
    process (Just (KeyDown (KeyAny '1'))) = processIOAction '1'
    process (Just (KeyDown (KeyAny '2'))) = processIOAction '2'
    process (Just (KeyDown (KeyAny '3'))) = processIOAction '3'
    process (Just (KeyDown (KeyAny '4'))) = processIOAction '4'
    process (Just (KeyDown (KeyAny '5'))) = processIOAction '5'
    process (Just (KeyDown (KeyAny '6'))) = processIOAction '6'
    process (Just (KeyDown (KeyAny '7'))) = processIOAction '7'
    process (Just (KeyDown (KeyAny '8'))) = processIOAction '8'
    process (Just (KeyDown (KeyAny '9'))) = processIOAction '9'
    process (Just (KeyDown (KeyAny '0'))) = processIOAction '0'

    -- Editing
    process (Just (MouseButtonDown Left mouseX mouseY)) = do
        gridWindow <- 'GridWindow :- get
        let point = mouseToPoint (mouseX, mouseY) config gridWindow
        'Grid :- update (addLife point)
        pure True
    process (Just (MouseButtonDown Right mouseX mouseY)) = do
        gridWindow <- 'GridWindow :- get
        let point = mouseToPoint (mouseX, mouseY) config gridWindow
        'Grid :- update (removeLife point)
        pure True

    -- Navigation
    process (Just (KeyDown KeyLeftArrow)) = do
        (_, dy) <- 'NavigateStatus :- get
        'NavigateStatus :- put (-1, dy)
        pure True
    process (Just (KeyDown KeyUpArrow)) = do
        (dx, _) <- 'NavigateStatus :- get
        'NavigateStatus :- put (dx, -1)
        pure True
    process (Just (KeyDown KeyRightArrow)) = do
        (_, dy) <- 'NavigateStatus :- get
        'NavigateStatus :- put (1, dy)
        pure True
    process (Just (KeyDown KeyDownArrow)) = do
        (dx, _) <- 'NavigateStatus :- get
        'NavigateStatus :- put (dx, 1)
        pure True
    process (Just (KeyUp KeyLeftArrow)) = do
        (_, dy) <- 'NavigateStatus :- get
        'NavigateStatus :- put (0, dy)
        pure True
    process (Just (KeyUp KeyUpArrow)) = do
        (dx, _) <- 'NavigateStatus :- get
        'NavigateStatus :- put (dx, 0)
        pure True
    process (Just (KeyUp KeyRightArrow)) = do
        (_, dy) <- 'NavigateStatus :- get
        'NavigateStatus :- put (0, dy)
        pure True
    process (Just (KeyUp KeyDownArrow)) = do
        (dx, _) <- 'NavigateStatus :- get
        'NavigateStatus :- put (dx, 0)
        pure True
    process (Just (KeyUp (KeyAny '-'))) = do
        gridWindow <- 'GridWindow :- get
        when (columnN gridWindow <= 32) ('GridWindow :- put
                (record { columnN $= (*2), rowN $= (*2) } gridWindow))
        pure True
    process (Just (KeyDown (KeyAny '='))) = do
        gridWindow <- 'GridWindow :- get
        when (columnN gridWindow >= 32) ('GridWindow :- put
                (record { columnN $= (flip div 2), rowN $= (flip div 2) } gridWindow))
        pure True

    -- Playing
    process (Just (KeyDown KeySpace)) = do
        playStatus <- 'PlayStatus :- get
        case playStatus of
             Playing => 'PlayStatus :- put Paused
             _       => 'PlayStatus :- put Playing
        pure True
    process (Just (KeyDown (KeyAny 'n'))) = do
        'PlayStatus :- put Step
        pure True
    process _        = pure True

    draw : Running ()
    draw = do
        rectangle black 0 0 (width config) (height config)
        grid <- 'Grid :- get
        gridWindow <- 'GridWindow :- get
        drawGrid config gridWindow grid
        flip

    updateWorld : Running ()
    updateWorld = do
        f <- 'Frames :- get
        'Frames :- put (f + 1)
        --when ((f `mod` 1000) == 0) (putStrLn (show f))

        gridWindow <- 'GridWindow :- get
        let speedFactor = \x => (x * 32 * 32 `div` columnN gridWindow) `div` columnN gridWindow

        let navigateCycle = speedFactor 4
        (dx, dy) <- 'NavigateStatus :- get
        when ((f `mod` (the Integer (cast navigateCycle))) == 0) $ do
            'GridWindow :- update (\window => record { leftX $= (+dx), topX $= (+dy) } window)

        let playCycle = speedFactor 12
        playStatus <- 'PlayStatus :- get
        when (playStatus /= Paused && (f `mod` (the Integer (cast playCycle))) == 0) $ do
            'Grid :- update nextGeneration
            when (playStatus == Step) $ 'PlayStatus :- put Paused
        pure ()

    eventLoop : Running ()
    eventLoop = do
        draw
        updateWorld
        e <- poll
        continue <- process e
        when continue eventLoop

main : IO ()
main = runInit
    [ ()
    , 'Grid := MkGrid 0 0 1 1 empty
    , 'GridWindow := MkGridWindow 0 0 32 24
    , 'PlayStatus := Paused
    , 'NavigateStatus := (0, 0)
    , 'IOStatus := NoIO
    , 'Frames := 0
    , ()
    , ()
    ] emain

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
module Examples.Declassification.TimeHatch

import System

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

import Examples.TwoPointLattice

%default total

--------------------------------------------------------------------------------
-- Library
--------------------------------------------------------------------------------
data Time : Type where
  ||| TCB
  MkTime : (t : Integer) -> Time

implementation Eq Time where
  (MkTime t1) == (MkTime t2) = t1 == t2

implementation Ord Time where
  compare (MkTime t1) (MkTime t2) = compare t1 t2

tick : DIO l Time
tick = pure (MkTime !(lift time))

print : String -> DIO L ()
print x = lift $ putStrLn x

usleep : (i : Int) -- microseconds
      -> {auto prf : So (i >= fromInteger 0)}
      -> DIO L ()
usleep i = lift $ usleep i

TimeHatch : Time -> Type
TimeHatch t = (t' : Time ** t <= t' = True) -> Labeled H Nat -> Labeled L Nat

data Fuel = Dry | More (Lazy Fuel)

--------------------------------------------------------------------------------
-- Bob (untrusted)
--------------------------------------------------------------------------------
bob : Fuel
   -> (secret : Labeled H Nat)
   -> TimeHatch t
   -> DIO L ()
bob Dry _ _ = pure ()
bob (More x) secret timeHatch {t} =
  do time <- tick
     case decEq (t <= time) True of
       Yes prf =>
         let declassified : Labeled L Nat  = timeHatch (time ** prf) secret
         in print $ "Yay! The secret is: " ++ cast !(unlabel declassified)
       No _ =>
          do print "No secret for me yet. Trying again in 500 ms ..."
             usleep 500000
             bob x secret timeHatch
     pure ()

--------------------------------------------------------------------------------
-- Alice (trusted)
--------------------------------------------------------------------------------
partial
forever : Fuel
forever = More forever

partial
alice : DIO L ()
alice =
  do let secret : Labeled H Nat = label 42
     (MkTime t) <- tick
     let declassifyTime = MkTime (t + 4)
     let hatch : TimeHatch declassifyTime = tokenHatch (\t' => declassifyTime <= t' = True)
     bob forever secret hatch

partial
main : IO ()
main = run alice

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Main

import System
import System.Concurrency.Process

ping : ProcID String -> ProcID String -> Process String ()
ping main proc
   = do Lift (usleep 1000)
        send proc "Hello!"
        Lift (putStrLn "Sent ping")
        msg <- recv
        Lift (putStrLn ("Reply: " ++ show msg))
        send main "Done"
        pure ()

pong : Process String ()
pong = do -- Lift (putStrLn "Waiting for message")
          (sender, m) <- recvWithSender
          Lift $ putStrLn ("Received " ++ m)
          send sender ("Hello back!")
          pure ()

mainProc : Process String ()
mainProc = do mainID <- myID
              pongth <- create pong
              pingth <- create (ping mainID pongth)
              recv -- block until everything done
              pure ()

repeatIO : Int -> IO ()
repeatIO 0 = pure ()
repeatIO n = do printLn n
                run mainProc
                repeatIO (n - 1)

main : IO ()
main = repeatIO 100


text:
module Main

main : IO ()
main = putStrLn "hello QuantumProgramming!"

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming