text:
> module FastSimpleProb.MeasuresProperties

> import Data.So
> import Syntax.PreorderReasoning

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicPostulates
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.Predicates
> import FastSimpleProb.Functor
> import FastSimpleProb.Measures
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Measures
> import NonNegDouble.LTEProperties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Rel.TotalPreorder
> import Pairs.Operations
> import Functor.Predicates
> import Functor.Properties

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

* Monotonicity (of |SimpleProb| measures):

> ||| Monotonicity
> Monotone : (SimpleProb NonNegDouble -> NonNegDouble) -> Type
> Monotone = Functor.Predicates.Monotone {B = NonNegDouble} {C = NonNegDouble} {F = SimpleProb} LTE LTE

* General monotonicity results

> ||| |monotoneNaturalLemma| for |SimpleProb|s
> normalizePreservesMonotonicity : (m : SimpleProb NonNegDouble -> NonNegDouble) ->
>                                  Monotone m ->
>                                  Monotone (m . normalize)
> normalizePreservesMonotonicity m mm =
>   monotoneNaturalLemma {B = NonNegDouble} {C = NonNegDouble} {F = SimpleProb}
>                        LTE LTE m mm normalize naturalNormalize

* Monotonicity of measures

> using implementation NumNonNegDouble
>   ||| |(uncurry (*)) . (cross f id)| is monotone
>   monotoneUncurryMultCrossId : {A : Type} ->
>                                (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
>                                (p : (a : A) -> f a `LTE` g a) ->
>                                (ap : (A, NonNegDouble)) ->
>                                uncurry (*) ((cross f id) ap) `LTE` uncurry (*) ((cross g id) ap)
>   monotoneUncurryMultCrossId {A} f g p (a, x) = s3 where
>     s1 : f a `LTE` g a
>     s1 = p a
>     s2 : (f a) * x `LTE` (g a) * x
>     s2 = monotoneMultLTE s1 (reflexiveLTE x)
>     s3 : uncurry (*) ((cross f id) (a, x)) `LTE` uncurry (*) ((cross g id) (a, x))
>     s3 = s2

> using implementation NumNonNegDouble
>   ||| |sum| is monotone
>   monotoneSum : Monotone sum
>   monotoneSum = ms where
>     ms  : {A : Type} ->
>           (f : A -> NonNegDouble) ->
>           (g : A -> NonNegDouble) ->
>           (p : (a : A) -> f a `LTE` g a) ->
>           (sp : SimpleProb A) ->
>           sum (map f sp) `LTE` sum (map g sp)
>     ms {A} f g p sp = s6 where
>       f'  : (A, NonNegDouble) -> NonNegDouble
>       f'  = uncurry (*) . (cross f id)
>       g'  : (A, NonNegDouble) -> NonNegDouble
>       g'  = uncurry (*) . (cross g id)
>       p'  : (ap : (A, NonNegDouble)) -> f' ap `LTE` g' ap
>       p'  = monotoneUncurryMultCrossId f g p
>       aps : List (A, NonNegDouble)
>       aps = toList sp
>       s1  : Prelude.Foldable.sum (map f' aps) `LTE` Prelude.Foldable.sum (map g' aps)
>       s1  = monotoneSum {A = (A, NonNegDouble)} f' g' p' aps
>       s2  : map f' aps = map (uncurry (*)) (toList (fmap f sp))
>       s2  = ( map f' aps )
>           ={ Refl }=
>             ( map ((uncurry (*)) . (cross f id)) aps )
>           ={ sym (mapFusion (uncurry (*)) (cross f id) aps) }=
>             ( map (uncurry (*)) (fmap (cross f id) aps) )
>           ={ cong (sym (toListFmapLemma f sp)) }=
>             ( map (uncurry (*)) (toList (fmap f sp)) )
>           QED
>       s3  : map g' aps = map (uncurry (*)) (toList (fmap g sp))
>       s3  = ( map g' aps )
>           ={ Refl }=
>             ( map ((uncurry (*)) . (cross g id)) aps )
>           ={ sym (mapFusion (uncurry (*)) (cross g id) aps) }=
>             ( map (uncurry (*)) (fmap (cross g id) aps) )
>           ={ cong (sym (toListFmapLemma g sp)) }=
>            ( map (uncurry (*)) (toList (fmap g sp)) )
>           QED
>       s4  : Prelude.Foldable.sum (map (uncurry (*)) (toList (fmap f sp))) `LTE` Prelude.Foldable.sum (map g' aps)
>       s4  = replace {P = \ X => Prelude.Foldable.sum X `LTE` (Prelude.Foldable.sum (map g' aps))} s2 s1
>       s5  : Prelude.Foldable.sum (map (uncurry (*)) (toList (fmap f sp))) `LTE` Prelude.Foldable.sum (map (uncurry (*)) (toList (fmap g sp)))
>       s5  = replace {P = \ X => Prelude.Foldable.sum (map (uncurry (*)) (toList (fmap f sp))) `LTE` Prelude.Foldable.sum X} s3 s4
>       s6  : sum (fmap f sp) `LTE` sum (fmap g sp)
>       s6  = s5

> ||| |expectedValue| is monotone
> monotoneExpectedValue : Monotone expectedValue
> monotoneExpectedValue = normalizePreservesMonotonicity sum monotoneSum

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module SequentialDecisionProblems.FullTheoryOptDefaults

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.CoreTheoryOptDefaults

> import Finite.Predicates
> import Finite.Operations
> import Opt.Operations
> import Rel.TotalPreorder

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

> SequentialDecisionProblems.FullTheory.cvalmax {n} x r v ps =
>  Opt.Operations.max totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalmaxSpec {n} x r v ps =
>   Opt.Operations.maxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> SequentialDecisionProblems.FullTheory.cvalargmaxSpec {n} x r v ps =
>   Opt.Operations.argmaxSpec totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (cval x r v ps)

> {-

> ---}


text:
module FoldFusion

Array : Type -> Type
Var : Type -> Type -> Type

interface Symantics (rep : Type -> Type) where
  int : Int -> rep Int
  bool : Bool -> rep Bool
  (==) : rep Int -> rep Int -> rep Bool
  (>) : rep Int -> rep Int -> rep Bool
  (<) : rep Int -> rep Int -> rep Bool
  (&&) : rep Bool -> rep Bool -> rep Bool
  (||) : rep Bool -> rep Bool -> rep Bool
  (+) : rep Int -> rep Int -> rep Int
  (*) : rep Int -> rep Int -> rep Int
  ite : rep Bool -> rep a -> rep a -> rep a
  deref : rep (Var s a) -> rep a
  assign : rep a -> rep (Var s a) -> rep ()
  newVar : rep a -> ({s : Type} -> rep (Var s a) -> rep b) -> rep b
  foreach : rep (Array a) -> (rep a -> rep ()) -> rep ()
  seq : rep a -> rep b -> rep b
  lam : (rep a -> rep b) -> rep (a -> b)
  app : rep (a -> b) -> rep a -> rep b

data Code : Type -> Type where
  C : (Int -> String) -> Code a

Symantics Code where
  int x = C (\_ => show x)
  bool x = C (\_ => if x then "true" else "false")
  (==) (C l) (C r) = C (\v => "( " ++ l v ++ " = " ++ r v ++ " )")
  (>) (C l) (C r) = C (\v => "( " ++ l v ++ " > " ++ r v ++ " )")
  (<) (C l) (C r) = C (\v => "( " ++ l v ++ " < " ++ r v ++ " )")
  (&&) (C l) (C r) = C (\v => "( " ++ l v ++ " && " ++ r v ++ " )")
  (||) (C l) (C r) = C (\v => "( " ++ l v ++ " || " ++ r v ++ " )")
  (+) (C l) (C r) = C (\v => "( " ++ l v ++ " + " ++ r v ++ " )")
  (*) (C l) (C r) = C (\v => "( " ++ l v ++ " * " ++ r v ++ " )")
  ite (C b) (C l) (C r) = C (\v => "(if " ++ b v ++ " then " ++ l v ++ " else " ++ r v ++ ")")
  deref (C x) = C (\v => "!" ++ x v)
  assign (C val) (C var) = C (\v => var v ++ " := " ++ val v)
  newVar {a} (C s) f = C (\v => let x = "x" ++ show v in
                                let (C c) = f $ the (Code (Var () a)) (C (\_ => x)) in
                                "let " ++ x ++ " = ref " ++ s v ++ " in " ++ c (v + 1))
  foreach (C arr) f = C (\v =>  let x = "x" ++ show v in
                                let (C c) = f (C (\_ => x)) in
                                "(for " ++ x ++ " in " ++ arr v ++ " do " ++ c (v + 1) ++ ")")
  seq (C fs) (C sn) = C (\v => "(" ++ fs v ++ "; " ++ sn v ++ ")")
  lam f = C (\v => let x = "x" ++ show v in
                   let (C g) = f (C (\_ => x)) in
                   "(fun " ++ x ++ " -> " ++ g (v + 1) ++ ")" )
  app (C f) (C g) = C (\v => "(" ++ f v ++ " " ++ g v ++ ")" )

data Fold : (rep : Type -> Type) -> (a : Type) -> Type where
  FC : ({r : Type} -> (rep a -> rep r -> rep r) -> rep r -> rep r) -> Fold rep a

ofArray : Symantics rep => rep (Array a) -> Fold rep a
ofArray arr = FC (\f, seed => newVar seed (\v => seq (foreach arr (\x => assign (f x (deref v)) v)) (deref v)))

fold : (rep a -> rep r -> rep r) -> rep r -> Fold rep a -> rep r
fold f seed (FC g) = g f seed

map : (rep a -> rep b) -> Fold rep a -> Fold rep b
map f (FC g) = FC (\h => g (\x, r => h (f x) r))

flatMap : (rep a -> Fold rep b) -> Fold rep a -> Fold rep b
flatMap f (FC g) = FC (\h => g (\x, r => fold h r (f x)))

filter : Symantics rep => (rep a -> rep Bool) -> Fold rep a -> Fold rep a
filter f (FC g) = FC (\h => g (\x, r =>  ite (f x) (h x r) r))

count : Symantics rep => Fold rep a -> rep Int
count = fold (\x, acc => acc + (int 1)) (int 0)

sum : Symantics rep => Fold rep Int -> rep Int
sum = fold (\x, acc => x + acc) (int 0)

example : Symantics rep => rep (Array Int) -> rep Int
example = sum . map (\x => x * (int 2)) . filter (\x => x < (int 5)) . ofArray

test : Code (Array Int -> Int)
test = lam example

code : String
code = let (C c) = test in c 0

ext: idr

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
--Loc : Nat -> Nat -> Type
--Loc start end = (Nat, Nat)

--data Loc a = Nat -> Nat -> Type

{-
record Loc where
  constructor NewLoc
  start : Nat
  end : Nat

Loc : Type
Loc = (Nat, Nat)

NewLoc : Nat -> Nat -> (Nat, Nat)
NewLoc start end = (start, end)
-}

-- CONSTANTS -----------------------------------

INDENT : String
INDENT = "  "

-- DATA TYPES ----------------------------------

Loc : Type
Loc = (Nat, Nat)

data Node : Type where
  Text : String -> Loc -> Node
  Block : List Node -> Loc -> Node

data AST : Type where
  Document : List Node -> Loc -> AST

data Action =
  Insert Nat String

-- FUNCTIONS ------------------------------------

parse : String -> AST

renderWispy : AST -> String
renderWispy (Document rootNodes _) = concat (map renderNode rootNodes) where
  renderNode : Node -> String
  renderNode (Text value _) = value
  renderNode (Block nodes _) = INDENT ++ concat (map renderNode nodes)

renderJs : AST -> String -> String

-- incomplete
substring : String -> Nat -> Nat -> String
substring str Z Z = ""
substring str Z (S end) = case unpack str of
  (c :: cs) => pack [c] ++ substring (pack cs) Z end
substring str (S start) (S end) = case unpack str of
  (c :: cs) => substring (pack cs) start end

-- how do I prove that pos is greater than start?
-- incomplete
safeSubtract : Nat -> Nat -> Nat
safeSubtract x Z = x
safeSubtract (S x) (S y) = safeSubtract x y

insert : Node -> String -> Nat -> String
insert (Text nodeValue (start, end)) insertValue pos =
  let insertPos = safeSubtract pos start in
  let first = substring nodeValue 0 insertPos in
  let last = substring nodeValue insertPos (length nodeValue) in
  first ++ insertValue ++ last

edit : AST -> Action -> AST
edit (Document rootNodes loc) action =
  --let pos = (case action of
  --  Insert position value => position) in
  Document (map editNode rootNodes) loc where
    nodeLoc : Node -> Loc
    nodeLoc node = case node of
      Text _ loc => loc
      Block _ loc => loc

    editNode : Node -> Node
    editNode node =
      let (start, end) = nodeLoc node in
      case action of
        Insert actionStart actionValue =>
          let inNode = actionStart >= start && actionStart < end in
          case node of
            Text nodeValue loc => Text (if inNode then insert node actionValue actionStart else nodeValue) loc
            Block nodes loc => Block (if inNode then (map editNode nodes) else nodes) loc

-- MAIN ------------------------------------

sample : AST
sample = Document
  [
    Text "aaa" (0, 3),
    Block [
      Text "bbbbb" (4, 9)
    ] (4, 9),
    Text "ccc\n" (10, 14)
  ]
  (0, 14)

sampleInsert : Action
sampleInsert = Insert 5 "!!!"

--renderWispy sample
--renderWispy (edit sample sampleInsert)

max_stars_repo_name: raineorshine/wispy

max_issues_repo_name: raineorshine/wispy

max_forks_repo_name: raineorshine/wispy


text:
module TestLazy

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.Testing

%default partial
%access export

public export
data Ty = ATOM | EXPR

export
data SExpr : Ty -> Type where
  Atom : String -> SExpr ATOM
  AtomExpr : SExpr ATOM -> SExpr EXPR
  Expr : SExpr tyA -> SExpr tyB -> SExpr EXPR

Show (SExpr ty) where
  show (Atom a) = unwords ["Atom", a]
  show (Expr a b) = unwords ["Expr", show a, show b]

Show (SExpr ty) => Show (ty : Ty ** SExpr ty) where
  show (x ** pf) {ty = ATOM} = show pf
  show (x ** pf) {ty = EXPR} = show pf

atom : Parser $ SExpr ATOM
atom = do
  cs <- some $ satisfy isAlphaNum
  pure $ Atom (pack cs)
 <?> "Atom"

expr : Parser $ SExpr EXPR
expr = do
  a <- atom
  pure $ AtomExpr a
 <|>| do
   token "("
   exprA <- expr
   spaces
   exprB <- expr
   token ")"
   pure $ Expr exprA exprB
 <?> "EXPR"

tests : IO ()
tests = runTests
  [ parseTest "Atoms"          atom "Test"
  , parseTest "Numbers"        atom "1"
  , parseTest "Simple Expr 1"  expr "Test"
  , parseTest "Simple Expr 2"  expr "(id x)"
  , parseTest "Complex Expr 1" expr "(add (1 2))"
  , parseTest "Complex Expr 2" expr "(a (b (c (d (e (f (g (h (i (j (k (l (m (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))"
  , parseTestNot "Complex Expr 3" expr """(a
  (b
    (c
      (d
        (e
          f
            (g
              (h
                (i
                  (j
                    (k
                      (l
                        (m
                          (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))
"""
  , parseTestCmpNot "Complex Expr 4"
                    expr
                    """(a
  (b
    (c
      (d
        (e
          f
            (g
              (h
                (i
                  (j
                    (k
                      (l
                        (m
                          (n (o (p (q (r (s (t (u (v (w (x (y (z NIL))))))))))))))))))))))))))"""
                          """At 1:1:
	EXPR
At 1:1:
	Atom
At 1:1:
	a different token
At 2:3:
	EXPR
At 2:3:
	Atom
At 2:3:
	a different token
At 3:5:
	EXPR
At 3:5:
	Atom
At 3:5:
	a different token
At 4:7:
	EXPR
At 4:7:
	Atom
At 4:7:
	a different token
At 5:9:
	EXPR
At 5:9:
	Atom
At 5:9:
	a different token
At 6:12:
	token ")"
At 6:12:
	string ")"
At 6:12:
	character ')'
At 6:12:
	a different token"""
  ]


text:
import Data.Vect

data StackCmd : Type -> Nat -> Nat -> Type where
  Push : Integer -> StackCmd ()      height     (S height)
  Pop :             StackCmd Integer (S height) height
  Top :             StackCmd Integer (S height) (S height)

  Pure : ty -> StackCmd ty height height
  (>>=) : StackCmd a height1 height2 ->
          (a -> StackCmd b height2 height3) ->
          StackCmd b height1 height3

runStack : (stk : Vect inHeight Integer) ->
           StackCmd ty inHeight outHeight ->
           (ty, Vect outHeight Integer)
runStack stk (Push val) = ((), val :: stk)
runStack (val :: stk) Pop = (val, stk)
runStack (val :: stk) Top = (val, val :: stk)
runStack stk (Pure x) = (x, stk)
runStack stk (x >>= f) = let (x', newStk) = runStack stk x in
                             runStack newStk (f x')

testAdd : StackCmd Integer 0 0
testAdd = do Push 10
             Push 20
             val1 <- Pop
             val2 <- Pop
             Pure (val1 + val2)

doAdd : StackCmd () (S (S height)) (S height)
doAdd = do val1 <- Pop
           val2 <- Pop
           Push (val1 + val2)


text:
||| Module partially based on McBride's paper:
||| Turing-Completeness Totally Free
|||
||| It gives us a type to describe computation using general recursion
||| and functions to run these computations for a while or to completion
||| if we are able to prove them total.
|||
||| The content of the Erased section is new. Instead of producing the
||| domain/evaluation pair by computing a Dybjer-Setzer code we build a
||| specialised structure that allows us to make the domain proof runtime
||| irrelevant.

module Data.Recursion.Free

import Data.Late
import Data.InductionRecursion.DybjerSetzer

%default total

------------------------------------------------------------------------
-- Type

||| Syntax for a program using general recursion
public export
data General : (a : Type) -> (b : a -> Type) -> (x : Type) -> Type where
  ||| We can return a value without performing any recursive call.
  Tell : x -> General a b x
  ||| Or we can pick an input and ask an oracle to give us a return value
  ||| for it. The second argument is a continuation explaining what we want
  ||| to do with the returned value.
  Ask  : (i : a) -> (b i -> General a b x) -> General a b x

||| Type of functions using general recursion
public export
PiG : (a : Type) -> (b : a -> Type) -> Type
PiG a b = (i : a) -> General a b (b i)

||| Recursor for General
public export
fold : (x -> y) -> ((i : a) -> (b i -> y) -> y) -> General a b x -> y
fold pure ask (Tell x) = pure x
fold pure ask (Ask i k) = ask i (\ o => fold pure ask (k o))

------------------------------------------------------------------------
-- Basic functions

||| Perform a recursive call and return the value provided by the oracle.
public export
call : PiG a b
call i = Ask i Tell

||| Monadic bind (defined outside of the interface to be able to use it for
||| map and (<*>)).
public export
bind : General a b x -> (x -> General a b y) -> General a b y
bind m f = fold f Ask m

||| Given a monadic oracle we can give a monad morphism interpreting a
||| function using general recursion as a monadic process.
public export
monadMorphism : Monad m => (t : (i : a) -> m (b i)) -> General a b x -> m x
monadMorphism t = fold pure (\ i => (t i >>=))

------------------------------------------------------------------------
-- Instances

public export
Functor (General a b) where
  map f = fold (Tell . f) Ask

public export
Applicative (General a b) where
  pure = Tell
  gf <*> gv = bind gf (\ f => map (f $) gv)

public export
Monad (General a b) where
  (>>=) = bind

------------------------------------------------------------------------
-- Fuel-based (partial) evaluation

||| Check whehther we are ready to return a value
public export
already : General a b x -> Maybe x
already = monadMorphism (\ i => Nothing)

||| Use a function using general recursion to expand all of the oracle calls.
public export
expand : PiG a b -> General a b x -> General a b x
expand f = monadMorphism f

||| Recursively call expand a set number of times.
public export
engine : PiG a b -> Nat -> General a b x -> General a b x
engine f Z     = id
engine f (S n) = engine f n . expand f

||| Check whether recursively calling expand a set number of times is enough
||| to produce a value.
public export
petrol : PiG a b -> Nat -> (i : a) -> Maybe (b i)
petrol f n i = already $ engine f n $ f i

------------------------------------------------------------------------
-- Late-based evaluation

||| Rely on an oracle using general recursion to convert a function using
||| general recursion into a process returning a value in the (distant) future.
public export
late : PiG a b -> General a b x -> Late x
late f = monadMorphism (\ i => Later (assert_total $ late f (f i)))

||| Interpret a function using general recursion as a process returning
||| a value in the (distant) future.
public export
lazy : PiG a b -> (i : a) -> Late (b i)
lazy f i = late f (f i)

------------------------------------------------------------------------
-- Domain as a Dybjer-Setzer code and total evaluation function

namespace DybjerSetzer

  ||| Compute, as a Dybjer-Setzer code for an inductive-recursive type, the domain
  ||| of a function defined by general recursion.
  public export
  Domain : PiG a b -> (i : a) -> Code b (b i)
  Domain f i = monadMorphism ask (f i) where

    ask : (i : a) -> Code b (b i)
    ask i = Branch () (const i) $ \ t => Yield (t ())

  ||| If a given input is in the domain of the function then we may evaluate
  ||| it fully on that input and obtain a pure return value.
  public export
  evaluate : (f : PiG a b) -> (i : a) -> Mu (Domain f) i -> b i
  evaluate f i inDom = Decode inDom

  ||| If every input value is in the domain then the function is total.
  public export
  totally : (f : PiG a b) -> ((i : a) -> Mu (Domain f) i) ->
            (i : a) -> b i
  totally f allInDomain i = evaluate f i (allInDomain i)

------------------------------------------------------------------------
-- Runtime irrelevant domain and total evaluation function

namespace Erased

  ------------------------------------------------------------------------
  -- Domain and evaluation functions

  ||| What it means to describe a terminating computation
  ||| @ f is the function used to answer questions put to the oracle
  ||| @ d is the description of the computation
  public export
  data Layer : (f : PiG a b) -> (d : General a b (b i)) -> Type

  ||| The domain of a function (i.e. the set of inputs for which it terminates)
  ||| as a predicate on inputs
  ||| @ f is the function whose domain is being described
  ||| @ i is the input that is purported to be in the domain
  Domain : (f : PiG a b) -> (i : a) -> Type

  ||| Fully evaluate a computation known to be terminating.
  ||| Because of the careful design of the inductive family Layer, we can make
  ||| the proof runtime irrelevant.
  evaluateLayer : (f : PiG a b) -> (d : General a b (b i)) -> (0 _ : Layer f d) -> b i

  ||| Fully evaluate a function call for an input known to be in its domain.
  evaluate : (f : PiG a b) -> (i : a) -> (0 _ : Domain f i) -> b i

  -- In a classic Dybjer-Setzer situation this is computed by induction over the
  -- index of type `General a b (b i)` and the fixpoint called `Domain` is the
  -- one thing defined as an inductive type.
  -- Here we have to flip the script because Idris will only trust inductive data
  -- as a legitimate source of termination metric for a recursive function. This
  -- makes our definition of `evaluateLayer` obviously terminating.
  data Layer : PiG a b -> General a b (b i) -> Type where
    ||| A computation returning a value is trivially terminating
    MkTell : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
             (o : b i) -> Layer f (Tell o)

    ||| Performing a call to the oracle is termnating if the input is in its
    ||| domain and if the rest of the computation is also finite.
    MkAsk  : {0 a : Type} -> {0 b : a -> Type} -> {0 f : PiG a b} -> {0 i : a} ->
             (j : a) -> (jprf : Domain f j) ->
             (k : b j -> General a b (b i)) -> Layer f (k (evaluate f j jprf)) ->
             Layer f (Ask j k)

  -- Domain is simply defined as the top layer leading to a terminating
  -- computation with the function used as its own oracle.
  Domain f i = Layer f (f i)

  ||| A view that gives us a pattern-matching friendly presentation of the
  ||| @ d computation known to be terminating
  ||| @ l proof that it is
  ||| This may seem like a useless definition but the function `view`
  ||| demonstrates a very important use case: even if the proof is runtime
  ||| irrelevant, we can manufacture a satisfying view of it.
  data View : {d : General a b (b i)} -> (l : Layer f d) -> Type where
    TView : {0 b : a -> Type} -> {0 f : PiG a b} -> (o : b i) -> View (MkTell {b} {f} o)
    AView : {0 f : PiG a b} ->
            (j : a) -> (0 jprf : Domain f j) ->
            (k : b j -> General a b (b i)) -> (0 kprf : Layer f (k (evaluate f j jprf))) ->
            View (MkAsk j jprf k kprf)

  ||| Function computing the view by pattern-matching on the computation and
  ||| inverting the proof. Note that the proof is runtime irrelevant even though
  ||| the resulting view is not: this is possible because the relevant constructor
  ||| is uniquely determined by the shape of `d`.
  public export
  view : (d : General a b (b i)) -> (0 l : Layer f d) -> View l
  view (Tell o)  (MkTell o)            = TView o
  view (Ask j k) (MkAsk j jprf k kprf) = AView j jprf k kprf

  -- Just like `Domain` is defined in terms of `Layer`, the evaluation of a
  -- function call for an input in its domain can be reduced to the evaluation
  -- of a layer.
  evaluate f i l = evaluateLayer f (f i) l

  -- The view defined earlier allows us to pattern on the runtime irrelevant
  -- proof that the layer describes a terminating computation and therefore
  -- define `evaluateLayer` in a way that is purely structural.
  -- This becomes obvious if one spells out the (forced) pattern corresponding
  -- to `d` in each branch of the case.
  evaluateLayer f d l = case view d l of
    TView o => o
    AView j jprf k kprf => evaluateLayer f (k (evaluate f j jprf)) kprf

  ||| If a function's domain is total then it is a pure function.
  public export
  totally : (f : PiG a b) -> (0 _ : (i : a) -> Domain f i) ->
            (i : a) -> b i
  totally f dom i = evaluate f i (dom i)

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

  ||| Domain is a singleton type
  export
  irrelevantDomain : (f : PiG a b) -> (i : a) -> (p, q : Domain f i) -> p === q

  ||| Layer is a singleton type
  irrelevantLayer
    : (f : PiG a b) -> (d : General a b (b i)) -> (l, m : Layer f d) -> l === m

  irrelevantDomain f i p q = irrelevantLayer f (f i) p q

  irrelevantLayer f (Tell o)
    (MkTell o) (MkTell o) = Refl
  irrelevantLayer f (Ask j k)
    (MkAsk j jprf1 k kprf1) (MkAsk j jprf2 k kprf2)
    with (irrelevantDomain f j jprf1 jprf2)
      irrelevantLayer f (Ask j k)
        (MkAsk j jprf k kprf1) (MkAsk j jprf k kprf2)
        | Refl = cong (MkAsk j jprf k)
               $ irrelevantLayer f (k (evaluate f j jprf)) kprf1 kprf2

  ||| The result of `evaluateLayer` does not depend on the specific proof that
  ||| `i` is in the domain of the layer of computation at hand.
  export
  evaluateLayerIrrelevance
    : (f : PiG a b) -> (d : General a b (b i)) -> (0 p, q : Layer f d) ->
      evaluateLayer f d p === evaluateLayer f d q
  evaluateLayerIrrelevance f d p q
    = rewrite irrelevantLayer f d p q in Refl

  ||| The result of `evaluate` does not depend on the specific proof that `i`
  ||| is in the domain of the function at hand.
  export
  evaluateIrrelevance
    : (f : PiG a b) -> (i : a) -> (0 p, q : Domain f i) ->
      evaluate f i p === evaluate f i q
  evaluateIrrelevance f i p q
    = evaluateLayerIrrelevance f (f i) p q

  ||| The result computed by a total function is independent from the proof
  ||| that it is total.
  export
  totallyIrrelevance
    : (f : PiG a b) -> (0 p, q : (i : a) -> Domain f i) ->
      (i : a) -> totally f p i === totally f q i
  totallyIrrelevance f p q i = evaluateIrrelevance f i (p i) (q i)


text:
module Language.JSON.String.Lexer

import Data.Nat
import Language.JSON.String.Tokens
import Text.Lexer

%default total

export
quo : Lexer
quo = is '"'

export
esc : Lexer -> Lexer
esc = escape (is '\\')

private
unicodeEscape : Lexer
unicodeEscape = esc $ is 'u' <+> count (exactly 4) hexDigit

private
simpleEscape : Lexer
simpleEscape = esc $ oneOf "\"\\/bfnrt"

private
legalChar : Lexer
legalChar = non (quo <|> is '\\' <|> control)

private
jsonStringTokenMap : TokenMap JSONStringToken
jsonStringTokenMap = toTokenMap $
  [ (quo, JSTQuote)
  , (unicodeEscape, JSTUnicodeEscape)
  , (simpleEscape, JSTSimpleEscape)
  , (legalChar, JSTChar)
  ]

export
lexString : String -> Maybe (List (WithBounds JSONStringToken))
lexString x = case lex jsonStringTokenMap x of
                   (toks, _, _, "") => Just $ toks
                   _ => Nothing


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

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

{-
  ported from file /kernel/include/arch/x86/arch/types.h
-}

module seL4.Types

%access public export
%default total

SeL4_Word : Type
SeL4_Word = Int

SeL4_Uint8 : Type
SeL4_Uint8 = Int

SeL4_NodeId : Type
SeL4_NodeId = Int

SeL4_Domain : Type
SeL4_Domain = Int


text:
module Data.List.NotElem

%default total
%access public export

data NotElem : (prfEq : a -> a -> Type) -> a -> List a -> Type where
  IsEmpty : NotElem prfEq x Nil
  NotFirst : (prf : Not (prfEq x y)) -> NotElem prfEq x Nil -> NotElem prfEq x [y]
  NotThere : (prf : Not (prfEq x y))
          -> (notLater : NotElem prfEq x there)
          -> NotElem prfEq x (y::there)

isFirstElem : (decEq : (x : a) -> (y : a) -> Dec (prfSame x y))
           -> (prf : prfSame n x)
           -> NotElem prfSame n (x :: xs)
           -> Void
isFirstElem decEq prf (NotFirst f x) = f prf
isFirstElem decEq prf (NotThere f notLater) = f prf

isFoundLater : (decEq : (x : a) -> (y : a) -> Dec (prfSame x y))
            -> (contra : prfSame n x -> Void)
            -> (f : NotElem prfSame n xs -> Void)
            -> NotElem prfSame n (x :: xs)
            -> Void
isFoundLater decEq contra f (NotFirst prf x) = f x
isFoundLater decEq contra f (NotThere prf notLater) = f notLater

notElem : (decEq : (x,y : a) -> Dec (prfSame x y))
       -> (n : a)
       -> (ns : List a)
       -> Dec (NotElem prfSame n ns)
notElem decEq n [] = Yes IsEmpty
notElem decEq n (x :: xs) with (decEq n x)
  notElem decEq n (x :: xs) | (Yes prf) = No (isFirstElem decEq prf)
  notElem decEq n (x :: xs) | (No contra) with (notElem decEq n xs)
    notElem decEq n (x :: xs) | (No contra) | (Yes prf) = Yes (NotThere contra prf)
    notElem decEq n (x :: xs) | (No contra) | (No f) = No (isFoundLater decEq contra f)

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


text:
-- ---------------------------------------------------------------- [ Sign.idr ]
-- Module      :
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Std.Sign

import Crypto.Common
import Crypto.Message

import Crypto.Std.Key

||| Representation of a digital signature scheme.
class SignScheme s where
  ||| Generate a sign and verify key pair.
  signKeyGen : (Key Public Sign n, Key Private Sign m)

  ||| Sign a message and return a signed message.
  |||
  ||| @ sigkey The senders signing key.
  ||| @ msg The message to be signed.
  signMsg : (sigkey : Key Private Sign m)
            -> (msg : Vect a Bits32)
            -> Signed b

  ||| Verify a signed message and return the message.
  |||
  ||| @ verkey The senders verification key.
  ||| @ sigmsg The signed message.
  verifyMsg : (verkey : Key Public Sign n)
              -> (sigmsg : Signed b)
              -> Maybe (Vect a Bits32)

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

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Data.Functor.Tagged

import Data.Profunctor
import Data.Profunctor.Choice

public export
data Tagged : (a : Type) -> (b : Type) -> Type where
  MkTagged : b -> Tagged a b

export
retag : Tagged s b -> Tagged t b
retag (MkTagged b) = MkTagged b

export
untag : Tagged s b -> b
untag (MkTagged b) = b

export
Semigroup b => Semigroup (Tagged a b) where
  MkTagged x <+> MkTagged x' = MkTagged (x <+> x')

export
Monoid b => Monoid (Tagged a b) where
  neutral = MkTagged neutral

export
Functor (Tagged a) where
  map f (MkTagged x) = MkTagged (f x)

export
Applicative (Tagged a) where
  pure = MkTagged
  (MkTagged f) <*> (MkTagged x) = MkTagged (f x)

export
Monad (Tagged a) where
  MkTagged m >>= k = k m

export
Bifunctor Tagged where
  bimap f g (MkTagged b) = MkTagged (g b)

export
Profunctor Tagged where
  lmap _ = retag
  rmap = map

export
Choice Tagged where
  left' (MkTagged b) = MkTagged (Left b)
  right' (MkTagged b) = MkTagged (Right b)


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : UML.Component.Parser
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Component.Parser

import Lightyear
import Lightyear.Strings

import UML.Types

import UML.Code.Model
import UML.Code.Parser

import UML.Component.Model
import UML.Utils.Parsing

-- --------------------------------------------------------------- [ Interface ]
actual : Parser $ ComponentModel INTERFACE
actual = do
    token "interface"
    id <- ident <* space
    fs <- braces (some (funcs <* space) <* space)
    pure $ Actual id fs

provides : Parser $ ComponentModel INTERFACE
provides = do
    token "provides"
    id <- ident <* space
    orig <- (token "from" *> ident)
    space
    pure $ Provided id orig
  <?> "Provides"

requires : Parser $ ComponentModel INTERFACE
requires = do
    token "requires"
    id <- ident <* space
    token "from"
    orig <- ident <* space
    pure $ Required id orig
   <?> "Requires"

interface : Parser $ ComponentModel INTERFACE
interface = provides <|> requires <|> actual <?> "Interface"

-- --------------------------------------------------------------- [ Component ]

component : Parser $ ComponentModel COMPONENT
component = do
    token "component"
    name <- ident <* space
    (is, cs) <- braces (cbody <* space)
    pure $ MkComponent name is cs
   <?> "Component"
  where
    cbody : Parser (List $ ComponentModel INTERFACE, (List $ ComponentModel COMPONENT))
    cbody = do
      is <- some (interface <* space)
      cs <- opt $ some (component <* space)
      pure (is, fromMaybe Nil cs)

-- ----------------------------------------------------------------- [ Diagram ]

public
componentModel : Parser UML
componentModel = do
    ds <- some (dtype <* space)
    space
    cs <- some (component <* space)
    pure $ Component $ MkComponentModel ds cs
  <?> "Component Model"

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Dart.FFI.Constructors

import public System.FFI
import public Data.HVect
import public Data.List.Elem
import public Dart.FFI.Upcast

public export
data Parameter : (tag : Type) -> Type where
  MkParameter : (name : String) -> (ty : Type) -> (0 tag : Type) -> Parameter tag

%inline
public export
mkParameter : {tag : Type} -> String -> Type -> Parameter tag
mkParameter name ty = MkParameter name ty tag

%inline
public export
typeOf : Parameter tag -> Type
typeOf (MkParameter _ ty _) = ty

public export
data Argument : Parameter tag -> Type where
  Assign : {0 tag : Type} -> {ty : Type} -> (name : String) -> (value : ty) -> Argument (MkParameter name ty tag)

%inline
public export
Schema : (tag : Type) -> Type
Schema tag = List (Parameter tag)

public export
data Parameters : Schema tag -> Type where
  Nil : {0 schema : Schema tag} -> Parameters schema
  (::) : {0 p : Parameter tag} -> {0 schema : Schema tag}
      -> Argument p -> Parameters schema -> {auto 0 isValid : Elem p schema} -> Parameters schema

namespace Parameters
  %inline
  public export
  none : Parameters {tag = Void} []
  none = []

infix 1 @=
infix 1 @=>

%inline
public export
(@=) : {tag : Type} -> (p : Parameter tag) -> typeOf p -> Argument p
(@=) (MkParameter name _ _) value = Assign {tag = tag} name value

||| Upcast assignment.
%inline
public export
(@=>) : {tag : Type} -> {ty : Type} -> (p : Parameter tag) -> ty -> {auto isAssignable : typeOf p `IsAssignableFrom` ty} -> Argument p
(@=>) (MkParameter name _ _) value = Assign {tag = tag} name (upcast value)

public export
%extern prim__dart_new
  : (ty : Type)
 -> {positionalArgumentTys : Vect k Type}
 -> (constructorName : String)
 -> (positionalArguments : HVect positionalArgumentTys)
 -> (namedArguments : Parameters schema)
 -> (1 x : %World)
 -> IORes ty

public export
%extern prim__dart_new_const
  : (ty : Type)
 -> {positionalArgumentTys : Vect k Type}
 -> (constructorName : String)
 -> (positionalArguments : HVect positionalArgumentTys)
 -> (namedArguments : Parameters schema)
 -> ty

public export
%extern prim__dart_get_pure
  : {0 res : Type}
 -> {thisTy : Type}
 -> (foreignName : String)
 -> (this : thisTy)
 -> res

public export
%extern prim__dart_get
  : {0 propertyTy : Type}
 -> {thisTy : Type}
 -> (foreignName : String)
 -> (this : thisTy)
 -> (1 x : %World)
 -> IORes propertyTy

public export
%extern prim__dart_set
  : {thisTy : Type}
 -> {propertyTy : Type}
 -> (foreignName : String)
 -> (value : propertyTy)
 -> (this : thisTy)
 -> (1 x : %World)
 -> IORes propertyTy

public export
%extern prim__dart_invoke
  : {0 res : Type}
 -> {positionalArgumentTys : Vect k Type}
 -> (foreignName : String)
 -> (typeArguments : List Type)
 -> (positionalArguments : HVect positionalArgumentTys)
 -> (namedArguments : Parameters schema)
 -> (1 x : %World)
 -> IORes res

public export
%extern prim__dart_invoke_pure
  : {0 res : Type}
 -> {positionalArgumentTys : Vect k Type}
 -> (foreignName : String)
 -> (typeArguments : List Type)
 -> (positionalArguments : HVect positionalArgumentTys)
 -> (namedArguments : Parameters schema)
 -> res


text:
module Main

randoms : Int -> Stream Int
randoms seed =
  let seed' = 1664525 * seed + 1013904223
  in (seed' `shiftR` 2) :: randoms seed'

main : IO ()
main = do
  printLn $ take 100 $ randoms 52816

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module Idris.Codegen.ExtSTG.SemiDecEq

public export
interface SemiDecEq t where
  semiDecEq : (x : t) -> (y : t) -> Maybe (x = y)

export
SemiDecEq Nat where
  semiDecEq Z      Z      = Just Refl
  semiDecEq (S n1) (S n2) = do
    Refl <- semiDecEq n1 n2
    Just Refl
  semiDecEq _      _      = Nothing

export
SemiDecEq a => SemiDecEq (List a) where
  semiDecEq []        []        = Just Refl
  semiDecEq (x :: xs) (y :: ys) = do
    Refl <- semiDecEq x y
    Refl <- semiDecEq xs ys
    Just Refl
  semiDecEq _ _ = Nothing

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module LightClick.Connection

import Data.Vect

import Toolkit.Decidable.Informative
import Toolkit.Data.Rig

import LightClick.Types
import LightClick.Types.Equality
import LightClick.Types.Compatibility

%default total

namespace Port

  public export
  data Compatible : (left  : Ty (PORT l))
                 -> (right : Ty (PORT r))
                          -> Type
    where
      IsSafe : (flow  : Safe                   dl dr)
            -> (sens  : Sensitivity.Compatible sl sr)
            -> (wtype : WireType.Compatible    wl wr)
            -> (dtype : Data.Compatible        tl tr)
            -> Port.Compatible (TyPort l dl sl wl tl ul)
                               (TyPort r dr sr wr tr ur)

  directionUnsafe : (Safe dir x -> Void)
                 -> Compatible (TyPort l dir sense wty type usage) (TyPort r x y z t w)
                 -> Void
  directionUnsafe contra (IsSafe flow sens wtype dtype) = contra flow

  sensitivityInCompatible : (Compatible sense y -> Void)
                         -> Compatible (TyPort l dir sense wty type usage) (TyPort r x y z t w)
                         -> Void
  sensitivityInCompatible contra (IsSafe flow sens wtype dtype) = contra sens

  wireTypesInCompatible : (Compatible wty z -> Void)
                       -> Compatible (TyPort l dir sense wty type usage) (TyPort r x y z t w)
                       -> Void
  wireTypesInCompatible contra (IsSafe flow sens wtype dtype) = contra wtype

  dataTypeInCompatible : (Compatible type t -> Void)
                    -> Compatible (TyPort l dir sense wty type usage) (TyPort r x y z t w) -> Void
  dataTypeInCompatible contra (IsSafe flow sens wtype dtype) = contra dtype

  public export
  data Error = InCompatSensitivity Sensitivity.Error
             | InCompatDirection   Direction.Safe.Error
             | InCompatWTypes      Wire.Error
             | InCompatDTypes      Data.Error

  export
  compatible : (left  : Ty (PORT l))
            -> (right : Ty (PORT r))
                     -> DecInfo Port.Error
                               (Compatible left right)
  compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) with (safe dx dy)
    compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) with (compatible sx sy)
      compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (Yes prfS) with (compatible wx wy)
        compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (Yes prfS) | (Yes prfW) with (compatible tx ty)
          compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (Yes prfS) | (Yes prfW) | (Yes prfT)
            = Yes (IsSafe prfD prfS prfW prfT)

          compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (Yes prfS) | (Yes prfW) | (No msg contra)
            = No (InCompatDTypes msg) (dataTypeInCompatible contra)
        compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (Yes prfS) | (No msg contra)
          = No (InCompatWTypes msg) (wireTypesInCompatible contra)
      compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (Yes prfD) | (No msg contra)
        = No (InCompatSensitivity msg) (sensitivityInCompatible contra)
    compatible (TyPort l dx sx wx tx ux) (TyPort r dy sy wy ty uy) | (No msg contra)
      = No (InCompatDirection msg) (directionUnsafe contra)

namespace Fanout

  namespace PortList

    public export
    data Compatible : (input : Ty (PORT s))
                   -> (fan   : DVect String (Ty . PORT) n names)
                            -> Type
      where
        Empty : PortList.Compatible i Nil
        Cons : {x : Ty (PORT s)}
            -> {rest : DVect String (Ty . PORT) n names}
            -> Port.Compatible i x
            -> PortList.Compatible i rest
            -> PortList.Compatible i (x::rest)

    headNotCompat : {xs : DVect String (Ty . PORT) n names}
                 -> (Port.Compatible i x -> Void)
                 -> PortList.Compatible i (x `DVect.(::)` xs)
                 -> Void
    headNotCompat contra (Cons prf rest) = contra prf

    restNotCompat : {xs : DVect String (Ty . PORT) n names}
                 -> (Compatible i xs -> Void)
                 -> Compatible i (x `DVect.(::)` xs)
                 -> Void
    restNotCompat contra (Cons prf rest) = contra rest

    public export
    data Error = PListError Nat (Ty (PORT s)) Port.Error

    export
    compatible : (input : Ty (PORT s))
              -> (ports : DVect String (Ty . PORT) n names)
                      -> DecInfo PortList.Error
                                 (PortList.Compatible input ports)
    compatible i Nil = Yes Empty
    compatible i (x :: xs) with (compatible i x)
      compatible i (x :: xs) | (Yes prfX) with (compatible i xs)
        compatible i (x :: xs) | (Yes prfX) | Yes prfXs = Yes (Cons prfX prfXs)

        compatible i (x :: xs) | (Yes prfX) | (No (PListError pos y err) contra)
          = No (PListError (S pos) y err) (restNotCompat contra)
      compatible i (x :: xs) | (No msg contra) = No (PListError Z x msg) (headNotCompat contra)

  public export
  data Compatible : (input : Ty (PORT s))
                 -> (fan   : DVect String (Ty . PORT) (S (S n)) names)
                 -> Type
    where
      CompatFanout : PortList.Compatible input fan
                  -> Compatible input fan

  notCompatFanout : (PortList.Compatible input (x :: (y :: fan)) -> Void)
                 -> Fanout.Compatible input (x :: (y :: fan)) -> Void
  notCompatFanout contra (CompatFanout prf) = contra prf

  export
  compatible : (input : Ty (PORT s))
            -> (fan   : DVect String (Ty . PORT) (S (S n)) names)
                     -> DecInfo PortList.Error
                                (Fanout.Compatible input fan)

  compatible input (x::y::fan) with (PortList.compatible input (x::y::fan))
    compatible input (x::y::fan) | Yes prf = Yes (CompatFanout prf)
    compatible input (x::y::fan) | No msg contra = No msg (notCompatFanout contra)

namespace Mux

  public export
  data Error = CtrlNotSafe (Ty (PORT s)) Port.Error
             | MuxNotSafe (PortList.Error)

  namespace PortList

    public export
    data Compatible : (ports : DVect String (Ty . PORT) n names)
                   -> (o     : Ty (PORT s))
                            -> Type
      where
        Empty : Compatible Nil o
        Cons : {x : Ty (PORT s)}
            -> {rest : DVect String (Ty . PORT) n names}
            -> Port.Compatible x o
            -> PortList.Compatible     rest o
            -> PortList.Compatible (x::rest) o

    headNotCompat : {xs : DVect String (Ty . PORT) n names}
                 -> (Port.Compatible x o -> Void)
                 -> PortList.Compatible (x `DVect.(::)` xs) o
                 -> Void
    headNotCompat contra (Cons prf rest) = contra prf

    restNotCompat : {xs : DVect String (Ty . PORT) n names}
                 -> (Compatible xs o -> Void)
                 -> Compatible (x `DVect.(::)` xs) o
                 -> Void
    restNotCompat contra (Cons prf rest) = contra rest

    export
    compatible : (ports : DVect String (Ty . PORT) n names)
              -> (o     : Ty (PORT s))
                        -> DecInfo PortList.Error
                                   (PortList.Compatible ports o)
    compatible Nil o = Yes Empty
    compatible (x :: xs) o with (compatible x o)
      compatible (x :: xs) o | (Yes prfX) with (compatible xs o)
        compatible (x :: xs) o | (Yes prfX) | Yes prfXs = Yes (Cons prfX prfXs)

        compatible (x :: xs) o | (Yes prfX) | (No (PListError pos y err) contra)
          = No (PListError (S pos) y err) (restNotCompat contra)
      compatible (x :: xs) o | (No msg contra) = No (PListError Z x  msg) (headNotCompat contra)

  namespace Fanin

    public export
    data Compatible : (fan   : DVect String (Ty . PORT) (S (S n)) names)
                   -> (output : Ty (PORT s))
                   -> Type
      where
        CompatFanin : PortList.Compatible fan output
                   -> Compatible fan output

    notCompatFanin : (PortList.Compatible (x :: (y :: fan)) output -> Void)
                   -> Fanin.Compatible (x :: (y :: fan)) output -> Void
    notCompatFanin contra (CompatFanin prf) = contra prf

    export
    compatible : (fan    : DVect String (Ty . PORT) (S (S n)) names)
              -> (output : Ty (PORT s))
                       -> DecInfo PortList.Error
                                  (Fanin.Compatible fan output)

    compatible (x::y::fan) output with (PortList.compatible (x::y::fan) output)
      compatible (x::y::fan) output | Yes prf = Yes (CompatFanin prf)
      compatible (x::y::fan) output | No msg contra = No msg (notCompatFanin contra)

  public export
  data Compatible : (fan    : DVect String (Ty . PORT) (S (S n)) names)
                 -> (ctrl   : Ty (PORT c))
                 -> (output : Ty (PORT o))
                           -> Type
    where
      CompatMux : (fan  : DVect String (Ty . PORT) (S (S n)) names)
               -> (ctrl : Ty (PORT c))
               -> (out  : Ty (PORT o))
               -> (safeCTRL  : Port.Compatible ctrl (Control.mkDual ctrl))
               -> (safeFanIn : Fanin.Compatible fan out)
                            -> Compatible fan ctrl out

  faninNotCompat : (Fanin.Compatible fan output -> Void)
                -> Compatible fan ctrl output -> Void
  faninNotCompat contra (CompatMux f c o prfCtrl prfFanin) = contra prfFanin

  ctrlNotCompat : {fan : DVect String (Ty . PORT) (S (S n)) names}
               -> (Port.Compatible ctrl (Control.mkDual ctrl) -> Void)
               -> Compatible fan ctrl output
               -> Void
  ctrlNotCompat contra (CompatMux f c o prfCtrl prfFanin) = contra prfCtrl

  export
  compatible : (fanin  : DVect String (Ty . PORT) (S (S n)) names)
            -> (ctrl   : Ty (PORT c))
            -> (output : Ty (PORT o))
            -> DecInfo Mux.Error
                       (Compatible fanin ctrl output)
  compatible fan ctrl output with (Fanin.compatible fan output)
    compatible fan ctrl output | (Yes prfFan) with (compatible ctrl (Control.mkDual ctrl))
      compatible fan ctrl output | (Yes prfFan) | Yes prfCtrl = Yes (CompatMux fan ctrl output prfCtrl prfFan)

      compatible fan ctrl output | (Yes prfFan) | No msg contra
        = No (CtrlNotSafe (Control.mkDual ctrl) msg) (ctrlNotCompat contra)
    compatible fan ctrl output | No msg contra
      = No (MuxNotSafe msg) (faninNotCompat contra)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Cpu

import System
import Data.Vect

import Utilities
import Constants

%default total

export
record Cpu where
  constructor MkCpu
  -- 16 general purpose 8-bit registers, V0 to Vf
  V : Vect 16 Bits8
  -- 16-bit register called I
  I : Bits16
  -- pseudo PC (16-bit)
  PC : Bits16
  -- stack is an array of 16 16-bit values
  Stack : Vect 16 Bits16
  -- pseudo SP
  SP : Fin 16
  -- delay time register DT
  DT : Bits8
  -- sound timer register ST
  ST : Bits8

export
Show Cpu where
  show c = show (PC c) ++ " " ++ show (V c) ++ " " ++ show (I c)

export
newCpu : Cpu
newCpu =
  let v = Vect.replicate 16 0 in
  let stack = Vect.replicate 16 0 in
  let pc : Bits16 = cast StartingAddress in
  MkCpu v 0 pc stack 0 0 0

export
incrementPC : (cpu : Cpu) -> Cpu
incrementPC c =
  record { PC $= (+ 2) } c

export
setPC : (cpu : Cpu) -> (value : Bits16) -> Cpu
setPC c v =
  record { PC = v } c

export
getPC : (cpu : Cpu) -> Bits16
getPC = PC

partial
export
getRegisters : (cpu : Cpu) -> (len : Fin n) -> Vect n Bits8
getRegisters {n} cpu len =
  takeRegisters n $ V cpu
  where
    -- similar to Vect.take except that input is not `Vect (n + m) elem`
    partial
    takeRegisters : (n : Nat) -> (v : Vect m elem) -> Vect n elem
    takeRegisters Z v = []
    takeRegisters (S n) (x :: xs) = x :: takeRegisters n xs

partial
export
setRegisters : (cpu : Cpu) -> (len : Fin 16) -> (subset : Vect (finToNat len) Bits8) -> Cpu
setRegisters cpu len subset =
  let n = finToNat len in
  let (_, registers) = foldl (replaceRegisters n) (0, V cpu) subset in
  record { V = registers } cpu
  where
    replaceRegisters : (limit : Nat) -> (accum : (Nat, Vect 16 elem)) -> (reg : elem) -> (Nat, Vect 16 elem)
    replaceRegisters limit (n, accum) reg =
      let index = restrict 15 $ cast n in
      (n + 1, Vect.replaceAt index reg accum)

export
getRegister : (cpu : Cpu) -> (index : Fin 16) -> Bits8
getRegister c i =
  Vect.index i $ V c

export
setRegister : (cpu : Cpu) -> (index : Fin 16) -> (value : Bits8) -> Cpu
setRegister c i v =
  let newV = Vect.replaceAt i v (V c) in
  record { V = newV } c

export
setRegisterFlag : (cpu : Cpu) -> (value : Bits8) -> Cpu
setRegisterFlag c v =
  let newV = Vect.replaceAt 0xf v (V c) in
  record { V = newV } c

export
getRegisterI : (cpu : Cpu) -> Bits16
getRegisterI = I

export
setRegisterI : (cpu : Cpu) -> (value : Bits16) -> Cpu
setRegisterI c v =
  record { I = v } c

export
pushStack : (cpu : Cpu) -> (value : Bits16) -> Cpu
pushStack c address =
  let index = SP c in
  case toIntegerNat $ finToNat index of
    15 => idris_crash "Cpu: tried to push to full stack"
    n =>
      let newIndex = restrict 15 (n + 1) in
      let newStack = replaceAt newIndex (PC c) (Stack c) in
      record { SP = newIndex, Stack = newStack, PC = address } c

export
popStack : (cpu : Cpu) -> Cpu
popStack c =
  let index = SP c in
  case index of
    FZ => idris_crash "Cpu: tried to pop from empty stack"
    FS n =>
      let stack = Stack c in
      let newIndex = restrict 15 $ cast n in
      let newPC = Vect.index index stack in
      let newStack = replaceAt index 0 stack in
      record { SP = newIndex, Stack = newStack, PC = newPC } c

export
getDelayTimer : (cpu : Cpu) -> Bits8
getDelayTimer = DT

export
setDelayTimer : (cpu : Cpu) -> (countdown : Bits8) -> Cpu
setDelayTimer c v =
  record { DT = v } c

export
setSoundTimer : (cpu : Cpu) -> (countdown : Bits8) -> Cpu
setSoundTimer c v =
  record { ST = v } c

export
delayTimerIsActive : (cpu : Cpu) -> Bool
delayTimerIsActive c = DT c > 0

export
soundTimerIsActive : (cpu : Cpu) -> Bool
soundTimerIsActive c = ST c > 0

export
updateCPUTimers : (cpu : Cpu) -> (tick : Bool) -> Cpu
updateCPUTimers c tick =
  let currentDT = DT c in
  let currentST = ST c in
  let newDT = if tick && delayTimerIsActive c then decrement currentDT else currentDT in
  let newST = if tick && soundTimerIsActive c then decrement currentST else currentST in
  record { ST = newST, DT = newDT } c
  where
    decrement : (x : Bits8) -> Bits8
    decrement x =
      let xAsInt : Int = cast x in
      case xAsInt of
        0 => 0
        n => cast $ n - 1


text:
module Test.ColorTest

import IdrTest.Test
import IdrTest.Expectation

import Color

simpleTest : Test
simpleTest =
  test "Red & Bold" (\_ => assertEq
    (decorate (Text Red <&> BG Blue <&> Bold) "Hello")
    "\ESC[31m\ESC[44m\ESC[1mHello\ESC[0m\ESC[0m\ESC[0m"
  )

export
suite : Test
suite =
  describe "Color Tests"
    [ simpleTest
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Injective

%default total

interface Injective (op : t -> t) where
  inj : (a : t) -> (b : t) -> op a = op b -> a = b

  inj' : {a : t} -> {b : t} -> op a = op b -> a = b
  inj' {a} {b} = inj a b

Injective S where
  inj = succInjective

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Data.SortedMap
import Data.Fuel
import Control.ST

import Scheme.Core
import Scheme.Print
import Scheme.Parse
import Scheme.Eval

%default total

namespace Main

  replStep : String -> (env, qql : Var) -> ST m (Maybe String) [env ::: State SEnv, qql ::: State Nat]
  replStep userInput env qql = do
    case userInput of
         "quit" => pure Nothing
         ""     => pure $ Just ""
         "env"  => do
           MkSEnv defs <- read env
           pure $ Just $ show defs
         _      => case runParseExpr userInput of
                        Left  err => do
                          pure $ Just $ "Parse error!\n" ++ err
                        Right x   => do
                          case !(eval {env} {qql} x) of
                               Left  err => do
                                 pure $ Just $ "Evaluation error!\n" ++ err
                               Right res => do
                                 pure $ Just $ show res

  -- FIXME Tricking the totality checker is bad, mkay
  repl2 : ConsoleIO io => (env, qql : Var) -> ST io () [env ::: State SEnv, qql ::: State Nat]
  repl2 env qql = do
    putStr "descheme> "
    userInput <- getStr
    res <- replStep userInput env qql
    case res of
         Nothing => pure ()
         Just r  => do
           putStrLn r
           assert_total $ repl2 env qql

  createDefaultREPL : ConsoleIO io => ST io () []
  createDefaultREPL = do
    qql <- new $ the Nat 0
    env <- new $ defaultEnv
    repl2 env qql
    delete env
    delete qql
    pure ()

  -- FIXME Control+D ruins it
  main : IO ()
  main = assert_total $ do
    run createDefaultREPL
    pure ()


text:
module Builtin

%default total

-- The most primitive data types; things which are used by desugaring

-- Totality assertions

||| Assert to the totality checker that the given expression will always
||| terminate.
|||
||| The multiplicity of its argument is 1, so `assert_total` won't affect how
||| many times variables are used. If you're not writing a linear function,
||| this doesn't make a difference.
|||
||| Note: assert_total can reduce at compile time, if required for unification,
||| which might mean that it's no longer guarded a subexpression. Therefore,
||| it is best to use it around the smallest possible subexpression.
%inline
public export
assert_total : (1 _ : a) -> a
assert_total x = x

||| Assert to the totality checker that y is always structurally smaller than x
||| (which is typically a pattern argument, and *must* be in normal form for
||| this to work).
|||
||| The multiplicity of x is 0, so in a linear function, you can pass values to
||| x even if they have already been used.
||| The multiplicity of y is 1, so `assert_smaller` won't affect how many times
||| its y argument is used.
||| If you're not writing a linear function, the multiplicities don't make a
||| difference.
|||
||| @ x the larger value (typically a pattern argument)
||| @ y the smaller value (typically an argument to a recursive call)
%inline
public export
assert_smaller : (0 x : a) -> (1 y : b) -> b
assert_smaller x y = y

-- Unit type and pairs

||| The canonical single-element type, also known as the trivially true
||| proposition.
public export
data Unit =
  ||| The trivial constructor for `()`.
  MkUnit

||| The non-dependent pair type, also known as conjunction.
public export
data Pair : Type -> Type -> Type where
  ||| A pair of elements.
  ||| @ a the left element of the pair
  ||| @ b the right element of the pair
  MkPair : {0 a, b : Type} -> (x : a) -> (y : b) -> Pair a b

||| Return the first element of a pair.
public export
fst : {0 a, b : Type} -> (a, b) -> a
fst (x, y) = x

||| Return the second element of a pair.
public export
snd : {0 a, b : Type} -> (a, b) -> b
snd (x, y) = y

-- This directive tells auto implicit search what to use to look inside pairs
%pair Pair fst snd

infix 5 #

||| A pair type where each component is linear
public export
data LPair : Type -> Type -> Type where
  ||| A linear pair of elements.
  ||| If you take one copy of the linear pair apart
  ||| then you only get one copy of its left and right elements.
  ||| @ a the left element of the pair
  ||| @ b the right element of the pair
  (#) : (1 _ : a) -> (1 _ : b) -> LPair a b

namespace DPair
  ||| Dependent pairs aid in the construction of dependent types by providing
  ||| evidence that some value resides in the type.
  |||
  ||| Formally, speaking, dependent pairs represent existential quantification -
  ||| they consist of a witness for the existential claim and a proof that the
  ||| property holds for it.
  |||
  ||| @ a the value to place in the type.
  ||| @ p the dependent type that requires the value.
  public export
  record DPair a (p : a -> Type) where
    constructor MkDPair
    fst : a
    snd : p fst

  ||| A dependent variant of LPair, pairing a result value with a resource
  ||| that depends on the result value
  public export
  data Res : (a : Type) -> (a -> Type) -> Type where
       (#) : (val : a) -> (1 r : t val) -> Res a t

-- The empty type

||| The empty type, also known as the trivially false proposition.
|||
||| Use `void` or `absurd` to prove anything if you have a variable of type
||| `Void` in scope.
public export
data Void : Type where

-- Equality

public export
data Equal : forall a, b . a -> b -> Type where
     [search a b]
     Refl : {0 x : a} -> Equal x x

%name Equal prf

infix 6 ===, ~=~

-- An equality type for when you want to assert that each side of the
-- equality has the same type, but there's not other evidence available
-- to help with unification
public export
(===) : (x : a) -> (y : a) -> Type
(===) = Equal

||| Explicit heterogeneous ("John Major") equality.  Use this when Idris
||| incorrectly chooses homogeneous equality for `(=)`.
||| @ a the type of the left side
||| @ b the type of the right side
||| @ x the left side
||| @ y the right side
public export
(~=~) : (x : a) -> (y : b) -> Type
(~=~) = Equal

||| Perform substitution in a term according to some equality.
|||
||| Like `replace`, but with an explicit predicate, and applying the rewrite in
||| the other direction, which puts it in a form usable by the `rewrite` tactic
||| and term.
%inline
public export
rewrite__impl : {0 x, y : a} -> (0 p : _) ->
                (0 rule : x = y) -> (val : p y) -> p x
rewrite__impl p Refl prf = prf

%rewrite Equal rewrite__impl

||| Perform substitution in a term according to some equality.
%inline
public export
replace : forall x, y, p . (0 rule : x = y) -> p x -> p y
replace Refl prf = prf

||| Symmetry of propositional equality.
%inline
public export
sym : (0 rule : x = y) -> y = x
sym Refl = Refl

||| Transitivity of propositional equality.
%inline
public export
trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
trans Refl Refl = Refl

||| Injectivity of MkDPair (first components)
export
mkDPairInjectiveFst : MkDPair a pa === MkDPair b qb -> a === b
mkDPairInjectiveFst Refl = Refl

||| Injectivity of MkDPair (snd components)
export
mkDPairInjectiveSnd : MkDPair a pa === MkDPair a qa -> pa === qa
mkDPairInjectiveSnd Refl = Refl

||| Subvert the type checker.  This function is abstract, so it will not reduce
||| in the type checker.  Use it with care - it can result in segfaults or
||| worse!
public export
believe_me : a -> b
believe_me = prim__believe_me _ _

||| Assert to the usage checker that the given function uses its argument linearly.
public export
assert_linear : (1 f : a -> b) -> (1 val : a) -> b
assert_linear = believe_me id
  where
    id : (1 f : a -> b) -> a -> b
    id f = f

export partial
idris_crash : String -> a
idris_crash = prim__crash _

public export %inline
delay : a -> Lazy a
delay x = Delay x

public export %inline
force : Lazy a -> a
force x = Force x

%stringLit fromString

||| Interface for types that can be constructed from string literals.
public export
interface FromString ty where
  constructor MkFromString
  ||| Conversion from String.
  fromString : String -> ty

%allow_overloads fromString

%inline
public export
FromString String where
  fromString s = s

%defaulthint
%inline
public export
defaultString : FromString String
defaultString = %search

%charLit fromChar

||| Interface for types that can be constructed from char literals.
public export
interface FromChar ty where
  constructor MkFromChar
  ||| Conversion from Char.
  fromChar : Char -> ty

%allow_overloads fromChar

%inline
public export
FromChar Char where
  fromChar s = s

%defaulthint
%inline
public export
defaultChar : FromChar Char
defaultChar = %search

%doubleLit fromDouble

||| Interface for types that can be constructed from double literals.
public export
interface FromDouble ty where
  constructor MkFromDouble
  ||| Conversion from Double.
  fromDouble : Double -> ty

%allow_overloads fromDouble

%inline
public export
FromDouble Double where
  fromDouble s = s

%defaulthint
%inline
public export
defaultDouble : FromDouble Double
defaultDouble = %search


text:
module Specdris.Core

import Specdris.Data.SpecInfo
import Specdris.Data.SpecResult
import Specdris.Data.SpecState

%access export
%default total

||| BTree with elements in the leafs.
public export
data Tree : Type -> Type where
     Leaf : (elem : a) -> Tree a
     Node : (left : Tree a) -> (right : Tree a) -> Tree a

public export
SpecTree' : FFI -> Type
SpecTree' ffi = Tree (Either SpecInfo (IO' ffi SpecResult))

public export
SpecTree : Type
SpecTree = SpecTree' FFI_C

namespace SpecTreeDo
  (>>=) : SpecTree' ffi -> (() -> SpecTree' ffi) -> SpecTree' ffi
  (>>=) leftTree f = let rightTree = f () in
                         Node leftTree rightTree

{- Evaluates every leaf in the `SpecTree` and folds the different `IO`s to collect
   a final `SpecState`.

   Test:
     describe "a" $ do
       describe "b" $ do
         it "c" test_io_c
       it "d" test_io_d

   Tree from Test:
                        Node
                         |
         ----------------------------------
         |                                |
    Leaf Desc "a"                        Node
                                          |
                                 ---------------------
                                 |                   |
                                Node                Node
                                 |                   |
                       -------------               ---------------
                       |           |               |             |
                 Leaf Desc "b"    Node        Leaf It "d"  Leaf test_io_d
                                   |
                            ----------------
                            |              |
                       Leaf It "c"   Leaf test_io_c
 -}
evaluateTree : SpecTree' ffi ->
               SpecState ->
               (around : IO' ffi SpecResult -> IO' ffi SpecResult) ->
               (storeOutput : Bool) ->
               (level : Nat) ->
               IO' ffi SpecState
-- description or it
evaluateTree (Leaf (Left info)) state _ store level         = let out = evalInfo info level in
                                                                  if store then
                                                                    pure $ addLine out state
                                                                  else do
                                                                    putStrLn' out
                                                                    pure state

-- test case
evaluateTree (Leaf (Right specIO)) state around store level = evalResult !(around specIO) state store level

-- recursive step
evaluateTree (Node left right) state around store level
  = case left of
        -- node containing a description/it -> new level of output indentation
        (Leaf _) => do newState <- evaluateTree left state around store (level + 1)
                       evaluateTree right newState around store (level + 1)

        _        => do newState <- evaluateTree left state around store level
                       evaluateTree right newState around store level

evaluate : (around : IO' ffi SpecResult -> IO' ffi SpecResult) -> (storeOutput : Bool) -> SpecTree' ffi -> IO' ffi SpecState
evaluate around store tree = evaluateTree tree neutral around store 0

randomBase : Integer
randomBase = pow 2 32

randomInt : (seed : Integer) -> Integer
randomInt seed = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` randomBase)

randomDouble : (seed : Integer) -> Double
randomDouble seed = let value = randomInt seed in
                      (cast {to = Double} value) / (cast {to = Double} randomBase)

partial
shuffle : {default randomDouble rand : Integer -> Double} -> SpecTree' ffi -> (seed : Integer) -> SpecTree' ffi
shuffle {rand} (Node left@(Leaf _) right@(Leaf _)) seed          = Node left right
shuffle {rand} (Node left@(Leaf (Left (Describe _))) right) seed = Node left (shuffle {rand = rand} right seed)
shuffle {rand} (Node left@(Node _ _) right@(Node _ _)) seed      = let randVal  = rand seed
                                                                       nextSeed = (cast {to = Integer} randVal) * 100 in
                                                                     if randVal > 0.5 then
                                                                       Node (shuffle {rand = rand} left nextSeed) (shuffle {rand = rand} right nextSeed)
                                                                     else
                                                                       Node (shuffle {rand = rand} right nextSeed) (shuffle {rand = rand} left nextSeed)

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
%default total

data Ty = Ctor Int

fn : Ty -> Ty
fn m@(Ctor _) = y
  where
    y = m -- from @ pattern

asPatternVisibleInWhere : fn (Ctor 42) = Ctor 42
asPatternVisibleInWhere = Refl

fn2 : Ty -> Ty
fn2 m@(Ctor _) = y (Ctor 99)
  where
    y m = m -- should be the arg `m`, not the @ pattern

lhsVariablesShadowAsPattern : fn2 (Ctor 42) = Ctor 99
lhsVariablesShadowAsPattern = Refl

fn3 : Ty -> Ty
fn3 m@(Ctor _) = y (Ctor 99)
  where
    y m = z
      where
        z = m -- should be y's arg `m`, not @ pattern

nestedWhereShadowsAsPattern : fn3 (Ctor 42) = Ctor 99
nestedWhereShadowsAsPattern = Refl

fn4 : Ty -> Ty
fn4 m@(Ctor _) = y (Ctor 99)
  where
    y _ = z
      where
        z = m -- should be @ pattern

nestedWhereExposesAsPattern : fn4 (Ctor 42) = Ctor 42
nestedWhereExposesAsPattern = Refl

main : IO ()
main = putStrLn "OK"

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 BoundedVect
import Data.Vect
import NatHelpers

%default total

||| A bounded Vect is a vector with a maximum capacity that cannot be exceeded.
|||
||| The only way to append an element to the vector is to provide a prood that
||| it's size is strictly less than it's capacity. Therefore the size of a BoundedVect
||| will always be less or equal to its maximum capacity
public export
data BoundedVect : (max, size: Nat) -> (elem : Type) -> Type where
  Nil : BoundedVect max Z elem
  Cons : (prf : size `LT` max) -> (x : elem) -> BoundedVect max size elem -> BoundedVect max (S size) elem
%name BoundedVect xs, ys, zs, ws

export
fromVect : Vect size elem -> (ok : size `LTE` max) -> BoundedVect max size elem
fromVect [] ok = []
fromVect (x :: xs) ok = Cons ok x (fromVect xs (lteSuccLeft ok))

export
fromVectAuto : Vect size elem -> {auto ok : size `LTE` max} -> BoundedVect max size elem
fromVectAuto xs {ok} = fromVect xs ok

||| attempt to append an element to a bounded vect, if the vect is at max capacity
||| return nothing, otherwise, return the new boundedVect with the same bounds
export maybeAppendBoundedVect : (x : elem) -> BoundedVect max size elem -> Maybe (BoundedVect max (S size) elem)
maybeAppendBoundedVect x xs {max} {size}  with (cmp size max)
  maybeAppendBoundedVect x xs {max = (size + (S y))} {size = size} | (CmpLT y) =
    let lte = LTESucc $ lteRightPlusNat {k = y} (size) in
      Just (Cons (lteRighPlusSuccRightSucc lte) x xs)
  maybeAppendBoundedVect x xs {max = max} {size = max} | CmpEQ = Nothing
  maybeAppendBoundedVect x xs {max = max} {size = (max + (S k))} | (CmpGT k) = Nothing

||| Appends an element to a boundedVect and increase the size of its bound
export
appendVectExtendBound : (x : elem) -> BoundedVect max size elem -> BoundedVect (S max) (S size) elem
appendVectExtendBound x [] = Cons (LTESucc LTEZero) x []
appendVectExtendBound x (Cons prf y xs) with (appendVectExtendBound y xs)
  appendVectExtendBound x (Cons prf y xs) | (Cons z w ys) = Cons (LTESucc prf) w (Cons z w ys)


text:
module Vending

data DoorState = DoorClosed | DoorOpen

data Matter = Solid | Liquid | Gas

data MatterOperation : Type -> Matter -> Matter -> Type where
    Melt: MatterOperation () Solid Liquid
    Boil: MatterOperation () Liquid Gas
    Condense: MatterOperation () Gas Liquid
    Freeze: MatterOperation () Liquid Solid

    Bind: MatterOperation a state1 state2 -> (a->MatterOperation b state2 state3) -> MatterOperation b state1 state3

(>>=) : MatterOperation a state1 state2 -> (a->MatterOperation b state2 state3) -> MatterOperation b state1 state3
(>>=) = Bind

iceSteam : MatterOperation () Solid Gas
iceSteam = do Melt
              Boil
              Condense
              Freeze
              Melt
              Boil

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Main

main : IO ()
main = putStrLn "Hello world!"
-- main = putStrLn ?greeting -- so called `hole`, allows to leave pending code


text:
module Compiler.Scheme.ChezSep

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Generated
import Compiler.Inline
import Compiler.Scheme.Common
import Compiler.Scheme.Chez
import Compiler.Separate

import Core.Core
import Core.Hash
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
import Core.TT
import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.Vect

import Idris.Env

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

import Libraries.Data.NameMap
import Libraries.Data.Version
import Libraries.Utils.String

%default covering

schHeader : List String -> List String -> String
schHeader libs compilationUnits = unlines
  [ "(import (chezscheme) (support) "
      ++ unwords ["(" ++ cu ++ ")" | cu <- compilationUnits]
      ++ ")"
  , "(case (machine-type)"
  , "  [(i3le ti3le a6le ta6le tarm64le) (load-shared-object \"libc.so.6\")]"
  , "  [(i3osx ti3osx a6osx ta6osx tarm64osx) (load-shared-object \"libc.dylib\")]"
  , "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")"
  , "                           (load-shared-object \"ws2_32.dll\")]"
  , "  [else (load-shared-object \"libc.so\")]"
  , unlines ["  (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs]
  , ")"
  ]

schFooter : String
schFooter = "(collect 4)\n(blodwen-run-finalisers)\n"

startChez : String -> String -> String -> String
startChez chez appDirSh targetSh = Chez.startChezPreamble ++ unlines
    [ "export LD_LIBRARY_PATH=\"$DIR/" ++ appDirSh ++ ":$LD_LIBRARY_PATH\""
    , "\"" ++ chez ++ "\" -q "
        ++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" "
        ++ "--program \"$DIR/" ++ targetSh ++ "\" "
        ++ "\"$@\""
    ]

startChezCmd : String -> String -> String -> String
startChezCmd chez appDirSh targetSh = unlines
    [ "@echo off"
    , "set APPDIR=%~dp0"
    , "set PATH=%APPDIR%" ++ appDirSh ++ ";%PATH%"
    , "\"" ++ chez ++ "\" -q "
        ++ "--libdirs \"%APPDIR%" ++ appDirSh ++ "\" "
        ++ "--program \"%APPDIR%" ++ targetSh ++ "\" "
        ++ "%*"
    ]

startChezWinSh : String -> String -> String -> String
startChezWinSh chez appDirSh targetSh = unlines
    [ "#!/bin/sh"
    , "# " ++ (generatedString "Chez")
    , ""
    , "set -e # exit on any error"
    , ""
    , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")"
    , "PATH=\"$DIR/" ++ appDirSh ++ ":$PATH\""
    , "\"" ++ chez ++ "\" --program \"$DIR/" ++ targetSh ++ "\" \"$@\""
    , "\"" ++ chez ++ "\" -q "
        ++ "--libdirs \"$DIR/" ++ appDirSh ++ "\" "
        ++ "--program \"$DIR/" ++ targetSh ++ "\" "
        ++ "\"$@\""
    ]

-- TODO: parallelise this
compileChezLibraries : (chez : String) -> (libDir : String) -> (ssFiles : List String) -> Core ()
compileChezLibraries chez libDir ssFiles = coreLift_ $ system $ unwords
  [ "echo"
  , unwords
    [ "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ chezString ssFile ++ "))'"
      ++ " '(delete-file " ++ chezString ssFile ++ ")'"
      -- we must delete the SS file to prevent it from interfering with the SO files
      -- we keep the .hash file, though, so we still keep track of what to rebuild
    | ssFile <- ssFiles
    ]
  , "|", chez, "-q", "--libdirs", libDir
  ]

compileChezLibrary : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core ()
compileChezLibrary chez libDir ssFile = coreLift_ $ system $ unwords
  [ "echo"
  , "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-library " ++ chezString ssFile ++ "))'"
  , "'(delete-file " ++ chezString ssFile ++ ")'"
  , "|", chez, "-q", "--libdirs", libDir
  ]

compileChezProgram : (chez : String) -> (libDir : String) -> (ssFile : String) -> Core ()
compileChezProgram chez libDir ssFile = coreLift_ $ system $ unwords
  [ "echo"
  , "'(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++ chezString ssFile ++ "))'"
  , "'(delete-file " ++ chezString ssFile ++ ")'"
  , "|", chez, "-q", "--libdirs", libDir
  ]

chezNS : Namespace -> String
chezNS ns = case showNSWithSep "-" ns of
  "" => "unqualified"
  nss => nss

-- arbitrarily name the compilation unit
-- after the alphabetically first namespace contained within
chezLibraryName : CompilationUnit def -> String
chezLibraryName cu = chezNS (min1 cu.namespaces)
  where
    -- the stdlib of the previous stable version
    -- has some strange version of List1.foldl1
    -- so we reimplement it here for compatibility
    min1 : List1 Namespace -> Namespace
    min1 (ns ::: nss) = foldl min ns nss

-- TODO: use a proper exec function without shell injection
touch : String -> Core ()
touch s = coreLift_ $ system ("touch \"" ++ s ++ "\"")

record ChezLib where
  constructor MkChezLib
  name : String
  isOutdated : Bool  -- needs recompiling

||| Compile a TT expression to a bunch of Chez Scheme files
compileToSS : Ref Ctxt Defs -> String -> String -> ClosedTerm -> Core (Bool, List ChezLib)
compileToSS c chez appdir tm = do
  -- process native libraries
  ds <- getDirectives Chez
  libs <- findLibs ds
  traverse_ copyLib libs
  version <- coreLift $ chezVersion chez

  -- get the material for compilation
  cdata <- getCompileData False Cases tm
  let ctm = forget (mainExpr cdata)
  let ndefs = namedDefs cdata
  let cui = getCompilationUnits ndefs

  -- copy the support library
  support <- readDataFile "chez/support-sep.ss"
  let supportHash = show $ hash support
  supportChanged <-
    coreLift (readFile (appdir </> "support.hash")) >>= \case
      Left err => pure True
      Right fileHash => pure (fileHash /= supportHash)
  when supportChanged $ do
    Core.writeFile (appdir </> "support.ss") support
    Core.writeFile (appdir </> "support.hash") supportHash

  -- TODO: add extraRuntime
  -- the problem with this is that it's unclear what to put in the (export) clause of the library
  -- extraRuntime <- getExtraRuntime ds

  -- for each compilation unit, generate code
  chezLibs <- for cui.compilationUnits $ \cu => do
    let chezLib = chezLibraryName cu

    -- check if the hash has changed
    -- TODO: also check that the .so file exists
    let cuHash = show (hash cu)
    hashChanged <-
      coreLift (readFile (appdir </> chezLib <.> "hash")) >>= \case
        Left err       => pure True
        Right fileHash => pure (fileHash /= cuHash)

    -- generate code only when necessary
    when hashChanged $ do
      defs <- get Ctxt
      l <- newRef {t = List String} Loaded ["libc", "libc 6"]
      s <- newRef {t = List String} Structs []

      -- create imports + exports + header + footer
      let imports = unwords
            [ "(" ++
                maybe
                  "unqualified"
                  chezLibraryName
                  (SortedMap.lookup cuid cui.byId)
              ++ ")"
            | cuid <- SortedSet.toList cu.dependencies
            ]
      let exports = unwords $ concat
            -- constructors don't generate Scheme definitions
            [ case d of
                MkNmCon _ _ _ => []
                _ => [schName dn]
            | (dn, fc, d) <- cu.definitions
            ]
      let header =
            "(library (" ++ chezLib ++ ")\n"
            ++ "  (export " ++ exports ++ ")\n"
            ++ "  (import (chezscheme) (support) " ++ imports ++ ")\n\n"
      let footer = ")"

      fgndefs <- traverse (Chez.getFgnCall version) cu.definitions
      compdefs <- traverse (getScheme Chez.chezExtPrim Chez.chezString) cu.definitions
      loadlibs <- traverse (loadLib appdir) (mapMaybe fst fgndefs)

      -- write the files
      log "compiler.scheme.chez" 3 $ "Generating code for " ++ chezLib
      Core.writeFile (appdir </> chezLib <.> "ss") $ fastAppend $
        [header]
        ++ map snd fgndefs  -- definitions using foreign libs
        ++ compdefs
        ++ loadlibs  -- foreign library load statements
        ++ [footer]

      Core.writeFile (appdir </> chezLib <.> "hash") cuHash

    pure (MkChezLib chezLib hashChanged)

  -- main module
  main <- schExp Chez.chezExtPrim Chez.chezString 0 ctm
  Core.writeFile (appdir </> "mainprog.ss") $ unlines $
    [ schHeader (map snd libs) [lib.name | lib <- chezLibs]
    , "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))"
    , main
    , schFooter
    ]

  pure (supportChanged, chezLibs)

makeSh : String -> String -> String -> String -> Core ()
makeSh chez outShRel appDirSh targetSh =
  Core.writeFile outShRel (startChez chez appDirSh targetSh)

||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> Core ()
makeShWindows chez outShRel appDirSh targetSh = do
  let cmdFile = outShRel ++ ".cmd"
  Core.writeFile cmdFile (startChezCmd chez appDirSh targetSh)
  Core.writeFile outShRel (startChezWinSh chez appDirSh targetSh)

||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile = do
  -- set up paths
  Just cwd <- coreLift currentDir
       | Nothing => throw (InternalError "Can't get current directory")
  let appDirSh  = outfile ++ "_app"  -- relative to the launcher shell script
  let appDirRel = outputDir </> appDirSh  -- relative to CWD
  let appDirAbs = cwd </> appDirRel
  coreLift_ $ mkdirAll appDirRel

  -- generate the code
  chez <- coreLift $ findChez
  (supportChanged, chezLibs) <- compileToSS c chez appDirRel tm

  -- compile the code
  logTime "++ Make SO" $ when makeitso $ do
    -- compile the support code
    when supportChanged $ do
      log "compiler.scheme.chez" 3 $ "Compiling support"
      compileChezLibrary chez appDirRel (appDirRel </> "support.ss")

    -- compile every compilation unit
    compileChezLibraries chez appDirRel
      [appDirRel </> lib.name <.> "ss" | lib <- chezLibs, lib.isOutdated]

    -- touch them in the right order to make the timestamps right
    -- even for the libraries that were not recompiled
    for_ chezLibs $ \lib => do
      log "compiler.scheme.chez" 3 $ "Touching " ++ lib.name
      touch (appDirRel </> lib.name <.> "so")

    -- compile the main program
    compileChezProgram chez appDirRel (appDirRel </> "mainprog.ss")

  -- generate the launch script
  let outShRel = outputDir </> outfile
  let launchTargetSh = appDirSh </> "mainprog" <.> (if makeitso then "so" else "ss")
  if isWindows
     then makeShWindows chez outShRel appDirSh launchTargetSh
     else makeSh        chez outShRel appDirSh launchTargetSh
  coreLift_ $ chmodRaw outShRel 0o755
  pure (Just outShRel)

||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
            | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift_ $ system sh

||| Codegen wrapper for Chez scheme implementation.
export
codegenChezSep : Codegen
codegenChezSep = MkCG (compileExpr True) executeExpr Nothing Nothing


text:
module Node.FS

export
data FS : Type where [external]

%foreign "node:lambda: () => require('fs')"
ffi_require : PrimIO FS

export
require : HasIO io => io FS
require = primIO ffi_require

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
import Data.Vect

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         Just idx => Just $ index idx xs

vecTake : (n : Nat) -> (vec : Vect (n + m) a) -> Vect n a
vecTake Z vec = []
vecTake (S k) (x :: xs) = x :: vecTake k xs

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                                Nothing => Nothing
                                Just idx => Just $ index idx xs + index idx ys

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
||| Properties of Data.Vect.index
module Data.Vect.Properties.Index

import Data.Vect.Properties.Tabulate

import Data.Vect
import Data.Vect.Elem
import Data.Fin

import Syntax.PreorderReasoning

||| Recall an element by its position, as we may not have the element
||| at runtime
public export
recallElem : {xs : Vect n a} -> x `Elem` xs -> a
recallElem {xs = x :: _ }  Here         = x
recallElem {xs = _ :: xs} (There later) = recallElem later

||| Recalling by a position of `x` does yield `x`
export
recallElemSpec : (pos : x `Elem` xs) -> recallElem pos = x
recallElemSpec  Here         = Refl
recallElemSpec (There later) = recallElemSpec later

||| `index i : Vect n a -> a` is a natural transformation
export
indexNaturality : (i : Fin n) -> (f : a -> b) -> (xs : Vect n a)
  -> index i (map f xs) = f (index i xs)
indexNaturality  FZ    f (x :: xs) = Refl
indexNaturality (FS x) f (_ :: xs)  = indexNaturality x f xs

||| Replication tabulates the constant function
export
indexReplicate : (i : Fin n) -> (x : a)
  -> index i (replicate n x) = x
indexReplicate  FZ    x = Refl
indexReplicate (FS i) x = indexReplicate i x

||| `range` tabulates the identity function (by definition)
export
indexRange : (i : Fin n) -> index i (range {len = n}) === i
indexRange i = irrelevantEq $ indexTabulate id i

||| Inductive step auxiliary lemma for indexTranspose
indexZipWith_Cons : (i : Fin n) -> (xs : Vect n a) -> (xss : Vect n (Vect m a))
  -> index i (zipWith (::) xs xss)
  = (index i xs)       :: (index i xss)
indexZipWith_Cons  FZ    (x :: _ ) (xs:: _  ) = Refl
indexZipWith_Cons (FS i) (_ :: xs) (_ :: xss) = indexZipWith_Cons i xs xss

||| The `i`-th vector in a transposed matrix is the vector of `i`-th components
export
indexTranspose : (xss : Vect m (Vect n a)) -> (i : Fin n)
  -> index i (transpose xss) = map (index i) xss
indexTranspose     []      i = indexReplicate i []
indexTranspose (xs :: xss) i = Calc $
  |~ index i (transpose (xs :: xss))
  ~~ index i (zipWith (::) xs (transpose xss))  ...(Refl)
  ~~ index i xs :: index i (transpose xss)      ...(indexZipWith_Cons i xs (transpose xss))
  ~~ index i xs :: map (index i) xss            ...(cong (index i xs ::)
                                                         $ indexTranspose xss i)


text:
module GRIN.Opts.UnusedParameterElim

import Data.SortedSet as Set
import Data.SortedMap

import GRIN.AST
import GRIN.GrinM

number : List a -> List (Nat, a)
number = number' 0
  where
    number' : Nat -> List a -> List (Nat, a)
    number' _ [] = []
    number' i (x :: xs) = (i, x) :: number' (i + 1) xs

collectWhen : Bool -> a -> SortedSet a -> SortedSet a
collectWhen True a = insert a
collectWhen False _ = id

collectUsedVar : SortedSet Var -> Var -> SortedSet Var -> SortedSet Var
collectUsedVar params var = collectWhen (contains var params) var

collectUsedSVal : SortedSet Var -> SVal -> SortedSet Var -> SortedSet Var
collectUsedSVal params = \case
    SLit _ => id
    SVar var => collectUsedVar params var

collectUsedVal : SortedSet Var -> Val name -> SortedSet Var -> SortedSet Var
collectUsedVal params v m = case v of
    SimpleVal val => collectUsedSVal params val m
    ConstTagNode _ args => foldr (collectUsedSVal params) m args
    ConstTag _ => m
    VarTagNode _ args => foldr (collectUsedSVal params) m args
    VUnit => m

mutual
    collectUsedSExp : SortedSet Var -> SExp name -> SortedSet Var -> SortedSet Var
    collectUsedSExp params e m = case e of
        Do exp => collectUsedExp params exp m
        App _ args => foldr (collectUsedVar params) m args
        Pure val => collectUsedVal params val m
        Store val => collectUsedVal params val m
        Fetch _ var => collectUsedVar params var m
        FetchI _ _ var => collectUsedVar params var m
        Update var val => collectUsedVar params var $ collectUsedVal params val m

    collectUsedExp : SortedSet Var -> Exp name -> SortedSet Var -> SortedSet Var
    collectUsedExp params e m = case e of
        SimpleExp exp => collectUsedSExp params exp m
        Bind _ rhs rest => collectUsedSExp params rhs $ collectUsedExp params rest m
        Case val alts =>
            collectUsedVal params val
            $ foldr (collectUsedExp params . altExp) m alts

    -- collectUsedAlt : SortedSet Var -> Alt name -> SortedSet Var -> SortedSet Var
    -- collectUsedAlt params (MkAlt _ exp) = collectUsedExp params exp

0 UsedVarMap : Type -> Type
UsedVarMap name = SortedMap name (SortedSet Nat)

collectUsedDef : Ord name => Def name -> (name, SortedSet Nat)
collectUsedDef (MkDef n params exp _) =
    let used = Set.toList $ collectUsedExp (fromList params) exp empty
    in (n, fromList [idx | (idx, arg) <- number params, arg `elem` used])

getFnName : Tag name -> Maybe name
getFnName (MkTag ty n) = case ty of
    UThunk => Just n
    NUThunk => Just n
    Partial _ => Just n
    _ => Nothing

removeUnusedArgs : UsedVarMap name -> name -> List a -> List a
removeUnusedArgs nm n xs =
    let usedVars = lookup n nm
        idxUsed : Nat -> Bool
        idxUsed = \idx => case usedVars of
            Nothing => True
            Just used => contains idx used
    in [x | (idx, x) <- number xs, idxUsed idx]

removeUnusedVal : UsedVarMap name -> Val name -> Val name
removeUnusedVal nm = \case
    val@(ConstTagNode tag args) => case getFnName tag of
        Nothing => val
        Just n => ConstTagNode tag $ removeUnusedArgs nm n args
    val => val

removeUnusedCPat : UsedVarMap name -> CasePat name -> CasePat name
removeUnusedCPat nm pat@(NodePat tag args) = case getFnName tag of
    Nothing => pat
    Just n => NodePat tag $ removeUnusedArgs nm n args
removeUnusedCPat _ pat = pat

mutual
    removeUnusedSExp : UsedVarMap name -> SExp name -> SExp name
    removeUnusedSExp nm = \case
        Do exp => Do (removeUnusedExp nm exp)
        App n args => App n (removeUnusedArgs nm n args)
        Pure val => Pure (removeUnusedVal nm val)
        Store val => Store (removeUnusedVal nm val)
        Fetch i var => Fetch i var
        FetchI i n var => FetchI i n var
        Update var val => Update var (removeUnusedVal nm val)

    removeUnusedExp : UsedVarMap name -> Exp name -> Exp name
    removeUnusedExp nm = \case
        SimpleExp exp => SimpleExp (removeUnusedSExp nm exp)
        Bind val rhs rest => Bind val (removeUnusedSExp nm rhs) (removeUnusedExp nm rest)
        Case val alts => Case val (removeUnusedAlt nm <$> alts)

    removeUnusedAlt : UsedVarMap name -> Alt name -> Alt name
    removeUnusedAlt nm (MkAlt pat exp) = MkAlt (removeUnusedCPat nm pat) (removeUnusedExp nm exp)

removeUnusedDef : UsedVarMap name -> Def name -> Def name
removeUnusedDef nm (MkDef n args exp ty) =
    MkDef n (removeUnusedArgs nm n args) (removeUnusedExp nm exp) Nothing

removeUnusedProg : UsedVarMap name -> SortedMap name (Def name) -> SortedMap name (Def name)
removeUnusedProg nm defs = removeUnusedDef nm <$> defs

Semigroup (Prog name) where
    p <+> _ = p

export
unusedParamElim : Monad m => Ord name => GrinT name m ()
unusedParamElim = do
    MkProg exts defs m <- gets prog
    let nm = foldMap (uncurry singleton . collectUsedDef) defs
    putProg $ MkProg exts (removeUnusedProg nm defs) m


text:
module Presentation

import Control.Linear.LIO
import Utils

-- dup : (1 _ : Int) -> (Int,Int)
-- dup x = (x,x)

-- greetAudience : (1 _ : String) -> String
-- greetAudience city = "Hello Sydney"

picture : (url : String) -> Image
picture url = fetchImage url $ \image =>
  let croppedImage = cropImage image
      transposedImage = transposeImage croppedImage
  in transposedImage

readFile : (1 _ : String) -> IO String
readFile filename = let (>>=) = myBind in do
  file <- openFile filename
  (content # filehandler) <- read file
  closeFile filehandler `seq` pure (utf8Decode content)

-- Local Variables:
-- idris-load-packages: ("support" "prelude" "network" "lib" "base" "contrib")
-- End:


text:
module Collections.Util.Bnd

import Decidable.Equality
import Control.Relation
import Control.Order
import Decidable.Order.Strict

||| Extends a type with `Bot` and `Top` values, making it a "bounded" type.
|||
||| Used for orderings in order to allow a value which precedes all other values (`Bot`), and a
||| value which follows all other values (`Top`).
public export
data Bnd : (0 a : Type) -> Type where
  Bot : Bnd a
  Mid : (x : a) -> Bnd a
  Top : Bnd a

export
Uninhabited (Bot = Mid x) where
  uninhabited Refl impossible

export
Uninhabited (Bot = Top) where
  uninhabited Refl impossible

export
Uninhabited (Mid x = Bot) where
  uninhabited Refl impossible

export
Uninhabited (Mid x = Top) where
  uninhabited Refl impossible

export
Uninhabited (Top = Bot) where
  uninhabited Refl impossible

export
Uninhabited (Top = Mid x) where
  uninhabited Refl impossible

||| Proof that if two `Mid` values are equal, then their wrapped values are equal
export
midEq : Mid x = Mid y -> x = y
midEq Refl = Refl

||| Proof that if two `Mid` values are not equal, then their wrapped values are not equal
export
midNotEq : Not (Mid x = Mid y) -> Not (x = y)
midNotEq ctra prf = ctra $ cong Mid prf

export
DecEq t => DecEq (Bnd t) where
  decEq Bot     Bot     = Yes Refl
  decEq Bot     (Mid _) = No absurd
  decEq Bot     Top     = No absurd
  decEq (Mid _) Bot     = No absurd
  decEq (Mid x) (Mid y) = case decEq x y of
                               Yes prf => Yes $ cong Mid prf
                               No ctra => No $ ctra . midEq
  decEq (Mid x) Top     = No absurd
  decEq Top     Bot     = No absurd
  decEq Top     (Mid _) = No absurd
  decEq Top     Top     = Yes Refl

||| Given a LTE (less than or equal) relation on `a`, produces an LTE relation extended to `Bnd a`
|||
||| @ o The ordering to extend
public export
data BndLTE : (o : a -> a -> Type) -> Bnd a -> Bnd a -> Type where
  ||| `Bot` is less than or equal to everything
  BotLTEAll : BndLTE o Bot y
  ||| Two `Mid`s are ordered iff their wrapped values are ordered
  MidLTEMid : {0 o : a -> a -> Type} -> o x y -> BndLTE o (Mid x) (Mid y)
  ||| Everything is less than or equal to `Top`
  AllLTETop : BndLTE o x Top

export
Reflexive ty rel => Reflexive (Bnd ty) (BndLTE rel) where
  reflexive {x=Bot}   = BotLTEAll
  reflexive {x=Mid x} = MidLTEMid $ reflexive {x=x}
  reflexive {x=Top}   = AllLTETop

export
Transitive ty rel => Transitive (Bnd ty) (BndLTE rel) where
  transitive {x=Bot}                       BotLTEAll      yz             = BotLTEAll
  transitive {x=Mid x} {y=Mid y} {z=Mid z} (MidLTEMid xy) (MidLTEMid yz) = MidLTEMid $ transitive {x} {y} {z} xy yz
  transitive {x=Mid _} {y=Mid _} {z=Top}   (MidLTEMid xy) AllLTETop      = AllLTETop
  transitive           {y=Top}   {z=Top}   AllLTETop      AllLTETop      = AllLTETop

export
Antisymmetric ty rel => Antisymmetric (Bnd ty) (BndLTE rel) where
  antisymmetric {x=Bot}   {y=Bot}   BotLTEAll      BotLTEAll      = Refl
  antisymmetric {x=Mid x} {y=Mid y} (MidLTEMid xy) (MidLTEMid yx) = cong Mid $ antisymmetric {x} {y} xy yx
  antisymmetric {x=Top}   {y=Top}   AllLTETop      AllLTETop      = Refl

export
Connex ty rel => Connex (Bnd ty) (BndLTE rel) where
  connex {x=Bot}             _   = Left BotLTEAll
  connex           {y=Bot}   _   = Right BotLTEAll
  connex {x=Top}             _   = Right AllLTETop
  connex           {y=Top}   _   = Left AllLTETop
  connex {x=Mid x} {y=Mid y} prf = case connex {rel} {x} {y} (midNotEq prf) of
                                        Left  xy => Left  $ MidLTEMid xy
                                        Right yx => Right $ MidLTEMid yx

||| Given a LT (less than) relation on `a`, produces a LT relation extended to `Bnd a`
|||
||| @ so The strict ordering to extend
public export
data BndLT : (so : a -> a -> Type) -> Bnd a -> Bnd a -> Type where
  BotLTMid : BndLT so Bot (Mid x)
  BotLTTop : BndLT so Bot Top
  MidLTMid : {0 so : a -> a -> Type} -> so x y -> BndLT so (Mid x) (Mid y)
  MidLTTop : BndLT so (Mid x) Top

export
Transitive ty rel => Transitive (Bnd ty) (BndLT rel) where
  transitive {x=Bot}   {y=Mid _} {z=Mid _} BotLTMid      (MidLTMid _)  = BotLTMid
  transitive {x=Bot}   {y=Mid _} {z=Top}   BotLTMid      MidLTTop      = BotLTTop
  transitive {x=Bot}   {y=Top}             BotLTTop      BotLTMid      impossible
  transitive {x=Bot}   {y=Top}             BotLTTop      BotLTTop      impossible
  transitive {x=Bot}   {y=Top}             BotLTTop      (MidLTMid x)  impossible
  transitive {x=Bot}   {y=Top}             BotLTTop      MidLTTop      impossible
  transitive {x=Mid x} {y=Mid y} {z=Mid z} (MidLTMid xy) (MidLTMid yz) = MidLTMid $ transitive {x} {y} {z} xy yz
  transitive {x=Mid x} {y=Mid y} {z=Top}   (MidLTMid w)  MidLTTop      = MidLTTop
  transitive {x=Mid _} {y=Top}             MidLTTop      BotLTMid      impossible
  transitive {x=Mid _} {y=Top}             MidLTTop      BotLTTop      impossible
  transitive {x=Mid _} {y=Top}             MidLTTop      (MidLTMid y)  impossible
  transitive {x=Mid _} {y=Top}             MidLTTop      MidLTTop      impossible

export
Irreflexive ty rel => Irreflexive (Bnd ty) (BndLT rel) where
  irreflexive {x=Mid x} (MidLTMid xx) = irreflexive {x} xx

export
Asymmetric ty rel => Asymmetric (Bnd ty) (BndLT rel) where
  asymmetric BotLTMid BotLTMid impossible
  asymmetric BotLTMid BotLTTop impossible
  asymmetric BotLTMid (MidLTMid _) impossible
  asymmetric BotLTMid MidLTTop impossible
  asymmetric BotLTTop BotLTMid impossible
  asymmetric BotLTTop BotLTTop impossible
  asymmetric BotLTTop (MidLTMid _) impossible
  asymmetric BotLTTop MidLTTop impossible
  asymmetric (MidLTMid xy) (MidLTMid yx) = asymmetric {rel} xy yx
  asymmetric MidLTTop BotLTMid impossible
  asymmetric MidLTTop BotLTTop impossible
  asymmetric MidLTTop (MidLTMid _) impossible
  asymmetric MidLTTop MidLTTop impossible

export
StrictPreorder ty rel => StrictPreorder (Bnd ty) (BndLT rel) where

export
StrictOrdered ty rel => StrictOrdered (Bnd ty) (BndLT rel) where
  order Bot     Bot     = DecEQ Refl
  order Bot     (Mid _) = DecLT BotLTMid
  order Bot     Top     = DecLT BotLTTop
  order (Mid _) Bot     = DecGT BotLTMid
  order (Mid x) (Mid y) = case order x y of
                               DecLT xy => DecLT $ MidLTMid xy
                               DecEQ prf => DecEQ $ cong Mid prf
                               DecGT yx => DecGT $ MidLTMid yx
  order (Mid _) Top     = DecLT MidLTTop
  order Top     Bot     = DecGT BotLTTop
  order Top     (Mid _) = DecGT MidLTTop
  order Top     Top     = DecEQ Refl

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections