text:
module Circuits.NetList.Types

import Decidable.Equality

import Data.List.Elem

import public Circuits.Common

%default total

namespace Direction

  public export
  data Direction = INPUT | OUTPUT | INOUT

  Uninhabited (INPUT = OUTPUT) where
    uninhabited Refl impossible

  Uninhabited (OUTPUT = INOUT) where
    uninhabited Refl impossible

  Uninhabited (INPUT = INOUT) where
    uninhabited Refl impossible

  export
  DecEq Direction where
    decEq INPUT INPUT   = Yes Refl
    decEq INPUT OUTPUT  = No absurd
    decEq INPUT INOUT   = No absurd

    decEq OUTPUT INPUT  = No (negEqSym absurd)
    decEq OUTPUT OUTPUT = Yes Refl
    decEq OUTPUT INOUT  = No absurd

    decEq INOUT INPUT   = No (negEqSym absurd)
    decEq INOUT OUTPUT  = No (negEqSym absurd)
    decEq INOUT INOUT   = Yes Refl

  export
  Show Direction where
    show INPUT  = "input"
    show OUTPUT = "output"
    show INOUT  = "inout"

namespace Proj

  public export
  data Project : Direction -> Type where
    WRITE : Project OUTPUT
    READ  : Project INPUT

namespace Cast

  public export
  data Cast : (from,to : Direction) -> Type where
    BI : Cast INOUT INPUT
    BO : Cast INOUT OUTPUT

  export
  Show (Types.Cast.Cast f t) where
    show BI = "down"
    show BO = "up"

  Uninhabited (Cast OUTPUT flow) where
    uninhabited BI impossible
    uninhabited BO impossible

  Uninhabited (Cast INPUT flow) where
    uninhabited BI impossible
    uninhabited BO impossible

  Uninhabited (Cast INOUT INOUT) where
    uninhabited BI impossible
    uninhabited BO impossible

  export
  cast : (f,t : Direction) -> Dec (Cast f t)
  cast INPUT _  = No absurd
  cast OUTPUT _ = No absurd
  cast INOUT INPUT = Yes BI
  cast INOUT OUTPUT = Yes BO
  cast INOUT INOUT = No absurd

namespace Index

  public export
  data Up : (flow : Direction) -> Type where
    UO : Up OUTPUT
    UB : Up INOUT

  public export
  data Down : (flow : Direction) -> Type where
    DI : Down INPUT
    DB : Down INOUT

  public export
  data Index : (flow : Direction) -> Type where
    UP   : Up f -> Index f
    DOWN : Down f -> Index f

  export
  Show (Index f) where
    show (UP _) = "UP"
    show (DOWN _) = "DOWN"

  export
  dirFromCast : Cast INOUT flow -> Index INOUT
  dirFromCast BI = DOWN DB
  dirFromCast BO = UP UB

namespace Gate

  namespace Binary
    public export
    data Kind = AND  | IOR  | XOR
              | ANDN | IORN | XORN

    export
    Show Kind where
      show AND  = "and"
      show IOR  = "or"
      show XOR  = "xor"
      show ANDN = "nand"
      show IORN = "nor"
      show XORN = "xnor"

  namespace Unary
    public export
    data Kind = NOT

    export
    Show Unary.Kind where
      show NOT = "not"

namespace Types

  public export
  data Ty  : Type where
    TyUnit : Ty
    TyPort : (Direction, DType) -> Ty
    TyChan : DType -> Ty
    TyGate : Ty

  export
  Show Ty where
    show TyUnit         = "()"
    show (TyPort (d,t)) = "TyPort(" <+> show d <+> "," <+> show t <+> ")"
    show TyGate         = "TyGate"
    show (TyChan t)     = "TyChan(" <+> show t <+> ")"

  Uninhabited (TyUnit = TyPort x) where
    uninhabited Refl impossible

  Uninhabited (TyUnit = TyChan x) where
   uninhabited Refl impossible

  Uninhabited (TyUnit = TyGate) where
    uninhabited Refl impossible

  Uninhabited (TyPort x = TyGate) where
    uninhabited Refl impossible

  Uninhabited (TyPort x = TyChan y) where
    uninhabited Refl impossible

  Uninhabited (TyGate = TyChan y) where
    uninhabited Refl impossible

  export
  DecEq Ty where
    decEq TyUnit TyUnit = Yes Refl
    decEq TyUnit (TyPort x) = No absurd
    decEq TyUnit TyGate = No absurd
    decEq TyUnit (TyChan x) = No absurd

    decEq (TyPort x) TyUnit = No (negEqSym absurd)
    decEq (TyPort x) (TyPort y) with (decEq x y)
      decEq (TyPort x) (TyPort x) | (Yes Refl)
        = Yes Refl
      decEq (TyPort x) (TyPort y) | (No contra)
        = No (\Refl => contra Refl)
    decEq (TyPort x) TyGate = No (absurd)
    decEq (TyPort x) (TyChan c) = No (absurd)

    decEq TyGate TyUnit = No (negEqSym absurd)
    decEq TyGate (TyPort x) = No (negEqSym absurd)
    decEq TyGate TyGate = Yes Refl
    decEq TyGate (TyChan x) = No absurd

    decEq (TyChan ty) TyUnit = No (negEqSym absurd)
    decEq (TyChan ty) (TyPort x) = No (negEqSym absurd)
    decEq (TyChan ty) TyGate = No (negEqSym absurd)
    decEq (TyChan x) (TyChan y) with (decEq x y)
      decEq (TyChan x) (TyChan x) | (Yes Refl) = Yes Refl
      decEq (TyChan x) (TyChan y) | (No contra) = No (\Refl => contra Refl)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Crypto.RawSodium

%lib     C "sodium"
%link    C "sodium_glue.o"
%include C "sodium_glue.h"

-- RAW INTERFACE

-- Key and nonce lengths

export
box_nonceLength : IO Int
box_nonceLength = foreign FFI_C "box_nonceLength" (IO Int)

export
box_secretKeyLength : IO Int
box_secretKeyLength = foreign FFI_C "box_secretKeyLength" (IO Int)

export
box_publicKeyLength : IO Int
box_publicKeyLength =  foreign FFI_C "box_publicKeyLength" (IO Int)

export
secretbox_nonceLength : IO Int
secretbox_nonceLength = foreign FFI_C "secretbox_nonceLength" (IO Int)

export
secretbox_keyLength : IO Int
secretbox_keyLength = foreign FFI_C "secretbox_keyLength" (IO Int)

-- Create/read/write keys

export
do_newKey : Int -> IO ManagedPtr
do_newKey len = do p <- foreign FFI_C "mkKey" (Int -> IO Ptr) len
                   pure $ prim__registerPtr p (len+16)

export
do_getKeyLen : ManagedPtr -> IO Int
do_getKeyLen p = foreign FFI_C "keyLen" (ManagedPtr -> IO Int) p

export
do_getKeyIdx : ManagedPtr -> Int -> IO Int
do_getKeyIdx p i = foreign FFI_C "keyIdx" (ManagedPtr -> Int -> IO Int) p i

export
do_setKeyIdx : ManagedPtr -> Int -> Int -> IO ()
do_setKeyIdx p i b
     = foreign FFI_C "setKeyIdx" (ManagedPtr -> Int -> Int -> IO ()) p i b

-- Create/read/write nonces

export
do_newNonce : Int -> IO ManagedPtr
do_newNonce len = do p <- foreign FFI_C "mkNonce" (Int -> IO Ptr) len
                     pure $ prim__registerPtr p (len+16)

export
do_newNonceFromString : String -> IO ManagedPtr
do_newNonceFromString s
     = do p <- foreign FFI_C "mkNonceFromString" (String -> IO Ptr) s
          pure $ prim__registerPtr p (cast (length s) + 16)

export
do_setNonceIdx : ManagedPtr -> Int -> Int -> IO ()
do_setNonceIdx p i b
     = foreign FFI_C "setNonceIdx" (ManagedPtr -> Int -> Int -> IO ()) p i b

-- Making/reading boxes

export
do_newBox : Int -> IO ManagedPtr
do_newBox len = do p <- foreign FFI_C "newBox" (Int -> IO Ptr) len
                   pure $ prim__registerPtr p (len + 16)

export
do_newSecretBox : Int -> IO ManagedPtr
do_newSecretBox len = do p <- foreign FFI_C "newBox" (Int -> IO Ptr) len
                         pure $ prim__registerPtr p (len + 16)

export
do_getBoxLen : ManagedPtr -> IO Int
do_getBoxLen p = foreign FFI_C "getEncLen" (ManagedPtr -> IO Int) p

export
do_getBoxIdx : ManagedPtr -> Int -> IO Int
do_getBoxIdx p i = foreign FFI_C "getEncByte" (ManagedPtr -> Int -> IO Int) p i

do_setBoxIdx : ManagedPtr -> Int -> Int -> IO ()
do_setBoxIdx p i b
     = foreign FFI_C "setEncByte" (ManagedPtr -> Int -> Int -> IO ()) p i b

-- Reading results of operations (symmetric or public key)

export
do_readBoxOpen : ManagedPtr -> IO String
do_readBoxOpen p = foreign FFI_C "getDec" (ManagedPtr -> IO String) p

-- Symmetric keys

export
do_cryptoSecretBox : (msg : String) ->
                     (nonce : ManagedPtr) ->
                     (key : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoSecretBox m n k
   = do p <- foreign FFI_C "do_crypto_secretbox"
                     (String -> ManagedPtr -> ManagedPtr -> IO Ptr) m n k
        if !(nullPtr p)
           then pure Nothing
           else do boxlen <- foreign FFI_C "getEncSize" (Ptr -> IO Int) p
                   pure $ Just (prim__registerPtr p (boxlen + 16))

export
do_cryptoSecretBoxOpen : (ciphertext : ManagedPtr) ->
                         (nonce : ManagedPtr) ->
                         (key : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoSecretBoxOpen c n k
   = do p <- foreign FFI_C "do_crypto_secretbox_open"
                     (ManagedPtr -> ManagedPtr -> ManagedPtr -> IO Ptr) c n k
        if !(nullPtr p)
           then pure Nothing
           else do boxlen <- foreign FFI_C "getDecSize" (Ptr -> IO Int) p
                   pure $ Just (prim__registerPtr p (boxlen + 16))

-- Public keys

export
do_newKeyPair : IO Ptr
do_newKeyPair = foreign FFI_C "newKeyPair" (IO Ptr)

export
do_getPublic : Ptr -> IO ManagedPtr
do_getPublic kp = do p <- foreign FFI_C "getPublic" (Ptr -> IO Ptr) kp
                     len <- foreign FFI_C "keyLen" (Ptr -> IO Int) p
                     pure $ prim__registerPtr p (len + 16)

export
do_getSecret : Ptr -> IO ManagedPtr
do_getSecret kp = do p <- foreign FFI_C "getSecret" (Ptr -> IO Ptr) kp
                     len <- foreign FFI_C "keyLen" (Ptr -> IO Int) p
                     pure $ prim__registerPtr p (len + 16)

export
do_cryptoBox : (msg : String) ->
               (nonce : ManagedPtr) ->
               (pkey : ManagedPtr) ->
               (skey : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoBox m n pk sk
   = do p <- foreign FFI_C "do_crypto_box"
                     (String -> ManagedPtr -> ManagedPtr -> ManagedPtr -> IO Ptr) m n pk sk
        if !(nullPtr p)
           then pure Nothing
           else do boxlen <- foreign FFI_C "getEncSize" (Ptr -> IO Int) p
                   pure $ Just (prim__registerPtr p (boxlen + 16))

export
do_cryptoBoxOpen : (ciphertext : ManagedPtr) ->
                   (nonce : ManagedPtr) ->
                   (pkey : ManagedPtr) ->
                   (skey : ManagedPtr) -> IO (Maybe ManagedPtr)
do_cryptoBoxOpen c n pk sk
   = do p <- foreign FFI_C "do_crypto_box_open"
                     (ManagedPtr -> ManagedPtr -> ManagedPtr -> ManagedPtr -> IO Ptr) c n pk sk
        if !(nullPtr p)
           then pure Nothing
           else do boxlen <- foreign FFI_C "getDecSize" (Ptr -> IO Int) p
                   pure $ Just (prim__registerPtr p (boxlen + 16))

-- Releasing memory for keys and results of encryption/decryption

-- do_freeBox : Ptr -> IO ()
-- do_freeBox p = foreign FFI_C "freeEnc" (Ptr -> IO ()) p
--
-- do_freeBoxOpen : Ptr -> IO ()
-- do_freeBoxOpen p = foreign FFI_C "freeDec" (Ptr -> IO ()) p
--
-- do_freeKey : Ptr -> IO ()
-- do_freeKey p = foreign FFI_C "freeKey" (Ptr -> IO ()) p

export
do_freeKeyPair : Ptr -> IO ()
do_freeKeyPair p = foreign FFI_C "freeKeyPair" (Ptr -> IO ()) p

ext: idr


text:
module Invincy.Gen
import Language.Reflection.Elab

%access public export

-- todo: multiple and dependent arguments

-- TFoo -> Sigma Type (\x => x -> Foo)

argClause : TTName -> TTName -> (TTName, List CtorArg, Raw) ->
  (TTName, List CtorArg, Raw) -> FunClause Raw
argClause t' fn (cn, [], _) (en, [], _) =
  MkFunClause (RApp (Var fn) (Var en)) $
    -- `(MkSigma {P=(\x => x -> ~(Var t'))} Unit (\y => ~(Var cn)))
    RApp (RApp `(MkSigma {P=(\x => x -> ~(Var t'))}) (Var "Unit"))
      (RBind "y" (Lam (Var "Unit")) (Var cn))
argClause t' fn (cn, [CtorField ta], _) (en, [], _) =
  MkFunClause (RApp (Var fn) (Var en)) $
    RApp (RApp `(MkSigma {P=(\x => x -> ~(Var t'))}) (type ta))
      (RBind "y" (Lam (type ta)) (RApp (Var cn) (Var "y")))

cArgs : TTName -> Elab ()
cArgs fn = do
  (_, Ref, sig') <- lookupTyExact fn
  case sig' of
    -- (App _ (Bind _ _ (P _ t' _)))
    (Bind _ (Pi (P _ e' _) _) (App _ (Bind _ (Lam _) (Bind _ (Pi _ _) (P _ t' _))))) => do
      t <- lookupDatatypeExact t'
      e <- lookupDatatypeExact e'
      let clauses = zipWith (argClause t' fn) (constructors t) (constructors e)
      defineFunction $ DefineFun fn clauses
    _ => fail [TextPart "failed", TermPart sig']

-- Foo -> Sigma TFoo (\x => getWitness (args x))

dargClause : Raw -> TTName -> TTName -> (TTName, List CtorArg, Raw) ->
  (TTName, List CtorArg, Raw) -> FunClause Raw
dargClause f t' fn (cn, [], _) (en, [], ent) =
  MkFunClause (RApp (Var fn) (Var cn)) $
    RApp (RApp
          `(MkSigma {a=~(ent)} {P=~(f)})
           (Var en))
        `(MkUnit)
dargClause f t' fn (cn, [CtorField x], _) (en, [], ent) =
  MkFunClause (RBind (name x) (PVar (type x)) (RApp (Var fn) (RApp (Var cn) (Var (name x))))) $
    RBind (name x) (PVar (type x)) $
      RApp (RApp `(MkSigma {a=~(ent)} {P=~(f)}) (Var en)) (Var (name x))

dArgs : Raw -> TTName -> Elab ()
dArgs f fn = do
  (_, Ref, sig') <- lookupTyExact fn
  case sig' of
    (Bind _ (Pi (P _ t' _) _) (App (App _ (P _ e' _)) _)) => do
      t <- lookupDatatypeExact t'
      e <- lookupDatatypeExact e'
      let clauses = zipWith (dargClause f t' fn)
                            (constructors t)
                            (constructors e)
      defineFunction $ DefineFun fn clauses
    _ => fail [TextPart "failed", TermPart sig']

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
||| The content of this file is taken from the paper
||| Heterogeneous Binary Random-access lists

module Data.Vect.Binary

import Data.Binary.Digit
import Data.Binary
import Data.IMaybe
import Data.Nat
import Data.Nat.Exponentiation
import Data.Tree.Perfect

%default total

public export
data BVect : Nat -> Bin -> Type -> Type where
  Nil  : BVect n [] a
  (::) : IMaybe (isI b) (Tree n a) -> BVect (S n) bs a -> BVect n (b :: bs) a

public export
data Path : Nat -> Bin -> Type where
  Here  : Path n -> Path n (I :: bs)
  There : Path (S n) bs -> Path n (b :: bs)

public export
zero : {bs : Bin} -> {n : Nat} -> Path n (suc bs)
zero {bs} = case bs of
  [] => Here (fromNat 0 n (ltePow2 {m = n}))
  (O :: bs) => Here (fromNat 0 n (ltePow2 {m = n}))
  (I :: bs) => There zero

public export
lookup : BVect n bs a -> Path n bs -> a
lookup (hd :: _) (Here p) = lookup (fromJust hd) p
lookup (_ :: tl) (There p) = lookup tl p

public export
cons : {bs : _} -> Tree n a -> BVect n bs a -> BVect n (suc bs) a
cons t [] = [Just t]
cons {bs = b :: _} t (u :: us) = case b of
  I => Nothing :: cons (Node t (fromJust u)) us
  O => Just t :: us


text:
module Verified.Functor.Vect

import Data.Vect
import Verified.Functor

instance VerifiedFunctor (Vect n) where
  functorIdentity [] = Refl
  functorIdentity (x :: xs) =
    let IHxs = functorIdentity xs in ?lemma1
  functorComposition [] g1 g2 = Refl
  functorComposition (x :: xs) g1 g2 =
    let IHxs = functorComposition xs g1 g2 in ?lemma2

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

Verified.Functor.Vect.lemma2 = proof
  intros
  rewrite IHxs
  exact Refl

Verified.Functor.Vect.lemma1 = proof
  intros
  rewrite IHxs
  exact Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
> module InfiniteHorizonSequentialDecisionProblems.DeterministicTheory

> import Data.Vect
> import Syntax.PreorderReasoning

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Vect.Operations
> import Vect.Properties

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

* -----------------------------
* Sequential decision processes
* -----------------------------

> State  :  Type
> Ctrl   :  (x : State) -> Type
> next   :  (x : State) -> (y : Ctrl x) -> State

* ----------------------------
* Sequential decision problems
* ----------------------------

> Val              :  Type
> reward           :  (x : State) -> (y : Ctrl x) -> (x' : State) -> Val
> (<+>)            :  Val -> Val -> Val
> LTE              :  Val -> Val -> Type

* --------
* Policies
* --------

> Policy  :  Type
> Policy  =  (x : State) -> Ctrl x

* ---------------------
* The value of policies
* ---------------------

The value of making infinite many decision steps with a policy by
starting from a given state is given by a "value" function

> val : Policy -> State -> Val

that fulfils the specification

> valSpec  :  Type
> valSpec  =  (p : Policy) -> (x : State) ->
>             val p x = reward x (p x) (next x (p x)) <+> val p (next x (p x))

A naive attempt at implementing |val| directly "from its specification"

< val p x = reward x (p x) (next x (p x)) <+> val p (next x (p x))

yiels a possibly non total function. In contrast to SDPs with a finite
number of decision steps, we cannot rely on an induction principle for
decision problems over an infinite number of steps. Obviously, there are
cases in which |val| can be implemented. For instance, if all states
have the same successor. An important case is when |State| is finite. We
discuss this case below.

* ----------------------
* Optimality of policies
* ----------------------

> Opt    :  Policy -> Type
> Opt p  =  (p' : Policy) -> (x : State) -> val p' x `LTE` val p x

* ----------------
* Optimal policies
* ----------------

Let |LTE| be a preorder

> reflexiveLTE     :  (a : Val) -> a `LTE` a
> transitiveLTE    :  {a, b, c : Val} -> a `LTE` b -> b `LTE` c -> a `LTE` c

and let |<+>| be monotonous w.r.t. |LTE|

> monotonePlusLTE  :  {a, b, c, d : Val} -> a `LTE` b -> c `LTE` d -> (a <+> c) `LTE` (b <+> d)

We can compute the value of making a first decision step with a given
control and then infinitely many further steps with a given policy in
terms of the (yet to be implemented) |val| function:

> cval        :  (p : Policy) -> (x : State) -> Ctrl x -> Val
> cval p x y  =  reward x y (next x y) <+> val p (next x y)

Assume that, for an arbitrary policy |p| and for an arbitrary state |x|,
we can pick up a control that maximises |cval p x|:

> cvalmax         :  (p : Policy) -> (x : State) -> Val
> cvalargmax      :  (p : Policy) -> (x : State) -> Ctrl x

> cvalargmaxSpec  :  (p : Policy) -> (x : State) -> cvalmax p x = cval p x (cvalargmax p x)
> cvalmaxSpec     :  (p : Policy) -> (x : State) -> (y : Ctrl x) -> cval p x y `LTE` cvalmax p x

This is certainly the case if |Ctrl x| is non empty and finite for any
|x| but there are more interesting cases in which we can compute "best"
controls. In these cases, a policy

> opt : Policy

that fulfils Bellman's equation

> optSpec  :  Type
> optSpec  =  (x : State) -> opt x = cvalargmax opt x

is optimal

> optLemma : (vs : valSpec) -> (os : optSpec) -> Opt opt

As in the case of |val|, we cannot implement |optLemma| in general. But
it is useful to look at a (possibly non total) implementation:

> optLemma vs os p' x = s9 where
>   s1 : val p' (next x (p' x)) `LTE` val opt (next x (p' x))
>   s1 = assert_total (optLemma vs os p' (next x (p' x)))
>   s2 : cval p' x (p' x) `LTE` cval opt x (p' x)
>   s2 = monotonePlusLTE (reflexiveLTE (reward x (p' x) (next x (p' x)))) s1
>   s3 : cval opt x (p' x) `LTE` cvalmax opt x
>   s3 = cvalmaxSpec opt x (p' x)
>   s4 : cvalmax opt x = cval opt x (cvalargmax opt x)
>   s4 = cvalargmaxSpec opt x
>   s5 : cval opt x (cvalargmax opt x) = cval opt x (opt x)
>   s5 = replace {P = \ U => cval opt x U = cval opt x (opt x)} (os x) Refl
>   s6 : cval opt x (opt x) = val opt x
>   s6 = sym (vs opt x)
>   s7 : cval p' x (p' x) `LTE` cvalmax opt x
>   s7 = transitiveLTE s2 s3
>   s8 : val p' x `LTE` cvalmax opt x
>   s8 = replace {P = \ W => W `LTE` cvalmax opt x} (sym (vs p' x)) s7
>   s9 : val p' x `LTE` val opt x
>   s9 = replace {P = \ W => val p' x `LTE` W} (trans (trans s4 s5) s6) s8

* -------------------------
* The case of finite states
* -------------------------

If |State| is finite

> finiteState : Finite State

we can compute the number of values of type |State|

> cardState : Nat
> cardState = card finiteState

and collect them in a vector

> vectState : Vect cardState State
> vectState = toVect finiteState

This representation of |State| is guaranteed to be complete

> completeVectState : (x : State) -> Elem x vectState
> completeVectState = toVectComplete finiteState

and injective

> inj1VectState : Injective1 vectState
> inj1VectState = toVectInjective1 finiteState

> inj2VectState : Injective2 vectState
> inj2VectState = injectiveLemma vectState inj1VectState

by construction. We can also represent the value of a policy by a value
table

> vt : Policy -> Vect cardState Val

and implement |val| in terms of the values of the table

> val p x = index k (vt p) where
>   k : Fin cardState
>   k = lookup x vectState (completeVectState x)

In this case, the specification of |val| defines a linear system of
equations for the components of the value table. To derive these
equations, consider, first the representation of |next|

> nextR : (k : Fin cardState) -> (y : Ctrl (index k vectState)) -> Fin cardState
> nextR k y = lookup x' vectState (completeVectState x') where
>   x' : State
>   x' = next (index k vectState) y

|nextR| is a representations of |next| in the sense that

> nextLemma  : (k : Fin cardState) -> (y : Ctrl (index k vectState)) ->
>              index (nextR k y) vectState = next (index k vectState) y

A proof of |nextLemma| is straightforward, see Appendix below. It is
also useful to define a representation for the reward function

> rewardR : (k : Fin cardState) -> (y : Ctrl (index k vectState)) -> Val
> rewardR k y = reward x y (next x y) where
>   x : State
>   x = index k vectState

and for policies:

> pR : (p : Policy) -> (k : Fin cardState) -> Ctrl (index k vectState)
> pR p k = p (index k vectState)

With |nextR|, |rewardR| and |pR|, we can derive the system of equations for
the components of |vt| by rewriting |valSpec p| for each component of
|vectState|:

> equation : (vs : valSpec) -> (p : Policy) -> (k : Fin cardState) ->
>            index k (vt p)
>            =
>            rewardR k (pR p k) <+> index (nextR k (pR p k)) (vt p)

To derive |equation|, it is useful to prove three intermediate results:

> lemma1 : (p : Policy) -> (k : Fin cardState) -> index k (vt p) = val p (index k vectState)

> lemma2 : (p : Policy) -> (k : Fin cardState) ->
>          reward (index k vectState) (p (index k vectState)) (next (index k vectState) (p (index k vectState)))
>          =
>          rewardR k (pR p k)

> lemma3 : (p : Policy) -> (k : Fin cardState) ->
>          val p (next (index k vectState) (p (index k vectState)))
>          =
>          index (nextR k (pR p k)) (vt p)

The implementations are given in the Appendix. With these lemmas, the
implementation of |equation| is directly follows from the definition of
|valSpec|:

> equation vs p k = let x = index k vectState in
>                   ( index k (vt p) )
>                 ={ lemma1 p k }=
>                   ( val p x )
>                 ={ vs p x }=
>                   ( reward x (p x) (next x (p x)) <+> val p (next x (p x)) )
>                 ={ replace {P = \ W => reward x (p x) (next x (p x)) <+> val p (next x (p x)) = W <+> val p (next x (p x))} (lemma2 p k) Refl }=
>                   ( rewardR k (pR p k) <+> val p (next x (p x)) )
>                 ={ replace {P = \ W => rewardR k (pR p k) <+> val p (next x (p x)) = rewardR k (pR p k) <+> W} (lemma3 p k) Refl }=
>                   ( rewardR k (pR p k) <+> index (nextR k (pR p k)) (vt p) )
>                 QED

* --------
* Appendix
* --------

> nextLemma k y = ( index (nextR k y) vectState )
>               ={ Refl }=
>                 ( index (lookup (next (index k vectState) y) vectState (completeVectState (next (index k vectState) y))) vectState )
>               ={ indexLookupLemma (next (index k vectState) y) vectState (completeVectState (next (index k vectState) y)) }=
>                 ( next (index k vectState) y )
>               QED

> lemma1 p k = ( index k (vt p) )
>            ={ replace {P = \ W => index k (vt p) = index W (vt p)} (sym (lookupIndexLemma k vectState inj2VectState (toVectComplete finiteState (index k vectState)))) Refl }=
>              ( index (lookup (index k vectState) vectState (toVectComplete finiteState (index k vectState))) (vt p) )
>            ={ Refl }=
>              ( val p (index k vectState) )
>            QED

> lemma2 p k = Refl

> lemma3 p k = ( val p (next (index k vectState) (p (index k vectState))) )
>            ={ Refl }= -- def. pR
>              ( val p (next (index k vectState) (pR p k)) )
>            ={ Refl }= -- def. val
>              ( index (lookup (next (index k vectState) (pR p k)) vectState (completeVectState (next (index k vectState) (pR p k)))) (vt p) )
>            ={ Refl }= -- def. nextR
>              ( index (nextR k (pR p k)) (vt p) )
>            QED

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module CH07

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

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

area : Shape -> Double
area (Triangle x y) = x * y / 2
area (Rectangle x y) = x * y
area (Circle x) = pi * x * x

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

Eq Shape where
  (Triangle x0 y0) == (Triangle x1 y1)   = x0 == x1 && y0 == y1
  (Rectangle x0 y0) == (Rectangle x1 y1) = x0 == x1 && y0 == y1
  (Circle x0) == (Circle x1)             = x0 == x1
  _ == _                                 = False

Ord Shape where
  compare shape0 shape1 = compare (area shape0) (area shape1)

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

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

Show ty => Show (Expr ty) where
  show (Val n)   = show n
  show (Add l r) = "(" ++ show l ++ " + " ++ show r ++ ")"
  show (Sub l r) = "(" ++ show l ++ " - " ++ show r ++ ")"
  show (Mul l r) = "(" ++ show l ++ " * " ++ show r ++ ")"
  show (Div l r) = "(" ++ show l ++ " / " ++ show r ++ ")"
  show (Abs e)   = "(abs " ++ show e ++ ")"

(Neg ty, Integral ty, Eq ty) => Eq (Expr ty) where
  l == r = (eval l) == (eval r)

(Neg from_ty, Integral from_ty) => Cast (Expr from_ty) from_ty where
  cast expr = eval expr

Functor Expr where
  map f (Val n)   = Val $ f n
  map f (Add l r) = Add (map f l) (map f r)
  map f (Sub l r) = Sub (map f l) (map f r)
  map f (Mul l r) = Mul (map f l) (map f r)
  map f (Div l r) = Div (map f l) (map f r)
  map f (Abs e)   = Abs $ map f e

Functor (Vect n) where
  map f Nil       = Nil
  map f (x :: xs) = f x :: map f xs

Foldable (Vect n) where
  foldr f acc Nil       = acc
  foldr f acc (x :: xs) = f x (foldr f acc xs)

  foldl f acc Nil       = acc
  foldl f acc (x :: xs) = foldl f (f acc x) xs

Eq e => Eq (Vect n e) where
  Nil == Nil             = True
  (x :: xs) == (y :: ys) = x == y && xs == ys


text:
module Main

import PLFI.Part1.Naturals
import PLFI.Part1.Induction
import PLFI.Part1.Relations
import PLFI.Part1.Equality
import PLFI.Part1.Isomorphism
import PLFI.Part1.Connectives
import PLFI.Part1.Negation

main : IO ()
main = do
  putStrLn "[x] Part1.Naturals"
  putStrLn "[x] Part1.Induction"
  putStrLn "[x] Part1.Relations"
  putStrLn "[x] Part1.Equality"
  putStrLn "[x] Part1.Isomorphism"
  putStrLn "[x] Part1.Connectives"
  putStrLn "[ ] Part1.Negation"

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
> module Pair.Properties

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

> pairLemma : {A, B : Type} -> (ab : (A, B)) -> ab = (fst ab, snd ab)
> pairLemma (a, b) = Refl

> pairEqElimFst : {A, B : Type} -> {a, a' : A} -> {b, b' : B} -> (a, b) = (a', b') -> a = a'
> pairEqElimFst Refl = Refl

> pairEqElimSnd : {A, B : Type} -> {a, a' : A} -> {b, b' : B} -> (a, b) = (a', b') -> b = b'
> pairEqElimSnd Refl = Refl


text:
module IxFreer

Eff : Type -> Type
Eff r = r -> (a : Type) -> (a -> r) -> Type

data IxFreer : {r : Type} -> (f : Eff r) -> Eff r where
  Pure : (x : a) -> IxFreer f (s' x) a s'
  Bind : {f : Eff r} -> f s a s' -> ((x : a) -> IxFreer f (s' x) b s'') -> IxFreer f s b s''

(>>=) : IxFreer f s a s' -> ((x : a) -> IxFreer f (s' x) b s'') -> IxFreer f s b s''
(>>=) (Pure x) f = f x
(>>=) (Bind x f) g = Bind x (\y => f y >>= g)

-- Example from https://www.idris-lang.org/drafts/sms.pdf
data Access = LoggedOut | LoggedIn
data LoginResult = OK | BadPassword

data Store : Access -> (ty : Type) -> (ty -> Access) -> Type where
  Login : Store LoggedOut LoginResult (\res => case res of
                                                  OK => LoggedIn
                                                  BadPassword => LoggedOut)

  Logout : Store LoggedIn () (const LoggedOut)
  ReadSecret : Store LoggedIn String (const LoggedIn)
  Lift : IO ty -> Store st ty (const st)

login : IxFreer Store LoggedOut LoginResult (\res => case res of
                                                      OK => LoggedIn
                                                      BadPassword => LoggedOut)
login = Bind Login Pure

logout : IxFreer Store LoggedIn () (const LoggedOut)
logout = Bind Logout Pure

readSecret : IxFreer Store LoggedIn String (const LoggedIn)
readSecret = Bind ReadSecret Pure

lift : IO ty -> IxFreer Store st ty (const st)
lift io = Bind (Lift io) Pure

getData : IxFreer Store LoggedOut () (const LoggedOut)
getData = do result <- login
             case result of
               OK => do secret <- readSecret
                        lift (putStr ("Secret: " ++ show secret ++ "\n"))
                        logout
               BadPassword => lift (putStr "Failure\n")

run : IxFreer Store s () s' -> IO ()
run (Pure x) = pure x
run (Bind Login g) = run (g OK)
run (Bind Logout g) = run (g ())
run (Bind ReadSecret g) = run (g "secret")
run (Bind (Lift io) g) = io >>= \x => run (g x)

test : IO ()
test = run getData

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
-- This regtest tests for incorrect erasure from underapplied data constructors.

data T : Type where
    C : Nat -> Nat -> Nat -> T

data Q : Type where
    D : (Nat -> T) -> Q

-- The bug was here: (C 3 4) would compile to plain data,
-- not to a function that would expect another (albeit erased) argument.
f : Q
f = D (C 3 4)

proj : Nat -> Q -> Nat -> T
proj    Z  (D f) = f
proj (S n)    q  = proj n q

g : T -> Nat
g (C x y z) = x + y

-- Here, we'd apply the not-a-function to the erased argument 4,
-- which would make the program go wrong.
main : IO ()
main = printLn $ g (proj 3 f 4)

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:
--- Day 1: Sonar Sweep ---

module SonarSweep
import System
import System.File
import Data.List
import Data.String

countIncreased : (nums : List Integer) -> List Integer
countIncreased nums = zipWith (\a, b => if b > a then 1 else 0) nums $ drop 1 nums

countIncreased3 : (nums: List Integer) -> List Integer
countIncreased3 nums = countIncreased $ sum <$> transpose [drop 2 nums, drop 1 nums, nums]

main : IO ()
main = do
      args <- getArgs
      let (file :: _) = drop 1 args | [] => printLn "No file provided!"
      (Right symbols) <- readFile file | (Left error) => printLn error
      let nums = catMaybes $ parsePositive <$> lines symbols
      (printLn . sum) $ countIncreased nums
      (printLn . sum) $ countIncreased3 nums


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains definitions of function optimizers.
module Optimize

import Tensor

||| An `Optimizer` finds the value, in a `Tensor`-valued feature space, which (approximately)
||| optimizes a scalar-valued function over that space.
|||
||| If the function is not well-defined at points in the feature space, and this is expressed by
||| wrapping function values in some context, this extra context can be captured in the value `m`.
||| For example, a function `a -> Maybe (Tensor [] Double)`, can be optimized by an
||| `Optimizer {m=Maybe} a`.
|||
||| @domain The type of the domain over which to find the optimizer.
public export 0
Optimizer : {default id 0 m : Type -> Type} -> (0 domain : Type) -> Type
Optimizer a = (a -> m $ Tensor [] Double) -> m a

||| Construct an `Optimizer` that implements grid search over a scalar feature space. Grid search
||| approximates the optimum by evaluating the objective over a finite, evenly-spaced grid.
|||
||| @density The density of the grid.
||| @lower The lower (inclusive) bound of the grid.
||| @upper The upper (exclusive) bound of the grid.
export
gridSearch : (density : Tensor [d] Int) ->
             (lower : Tensor [d] Double) ->
             (upper : Tensor [d] Double) ->
             Optimizer (Tensor [d] Double)

||| The limited-memory BFGS (L-BFGS) optimization tactic, see
|||
||| Nocedal, Jorge, Updating quasi-Newton matrices with limited storage.
||| Math. Comp. 35 (1980), no. 151, 773–782.
|||
||| available at
|||
||| https://www.ams.org/journals/mcom/1980-35-151/S0025-5718-1980-0572855-7/
|||
||| @initial_points The points from which to start optimization.
export
lbfgs : (initial_points : Tensor [n] Double) -> Optimizer (Tensor [n] Double)

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
||| Here we present the syntax for our local types.
||| Local Types present a role-oriented view of the protocol.
|||
||| We are inspired from the Tech Report 'A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming' (DTRS12-2).
||| The author's note that sending and receiving are special cases of select and branch..
|||
|||
module Sessions.Local

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta

public export
data Local : (role, label, msg  : Type)
          -> (rvars : List Ty)
          -> (type  : Ty)
                   -> Type
  where
    End : Local typeR typeL typeM rs G

    Call : Elem R rs -> Local typeR typeL typeM rs R

    Rec : Local typeR typeL typeM (R::rs) R
       -> Local typeR typeL typeM     rs  R

    Choice : (type : ChoiceTy)
          -> (whom : typeR)
          -> (selections : List1 (typeL, typeM, Local typeR typeL typeM rs g))
                        -> Local typeR typeL typeM rs g

public export
Branch : (role, label, msg : Type)
      -> (rvars : List Ty)
      -> (type  : Ty)
               -> Type
Branch role label msg rvars type
  = (label, msg, Local role label msg rvars type)

public export
Branches : (role, label, msg : Type)
        -> (rvars : List Ty)
        -> (type  : Ty)
                 -> Type
Branches role label msg rvars type
  = List1 (Branch role label msg rvars type)

public export
Branches' : (role, label, msg : Type)
         -> (rvars : List Ty)
         -> (type  : Ty)
                  -> Type
Branches' role label msg rvars type
  = List (Branch role label msg rvars type)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Eval

-- Evaluators for terms in the simply-typed
-- lambda calculus.

import BigStep
import Equivalence
import Determinism
import Progress
import Step
import Subst
import Term

%access export

------------------------------------------------------------
-- Begin: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS

eval : (e : Term [] t) -> (e' : Term [] t ** (Value e', TransStep e e'))
eval e = case progress e of
  Left v           => (e ** (v, TStRefl e))
  Right (e' ** s') => let (e'' ** (v'', s'')) = eval e'
                      in (e'' ** (v'', TStTrans s' s''))

-- End: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS
----------------------------------------------------------

----------------------------------------------------------
-- Begin: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS

eval' : Term [] t -> Term [] t
eval' (TVar i)       = absurd $ FinZAbsurd i
eval' (TAbs e)       = TAbs e
eval' (TApp e1 e2)   = let (TAbs e1v) = eval' e1
                           e2v        = eval' e2
                       in eval' $ subst e2v FZ e1v
eval' (TRec e e0 e1) = case eval' e of
                            TZero   => eval' e0
                            TSucc n => eval' $ (subst n FZ (subst (TRec n e0 e1) FZ e1))
eval' TZero          = TZero
eval' (TSucc e)      = TSucc (eval' e)
eval' (TPred e)      = case eval' e of
                            TZero     => TZero
                            TSucc ev' => ev'
eval' (TIfz e1 e2 e3) = case eval' e1 of
                             TZero   => eval' e2
                             TSucc _ => eval' e3

-- End: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS
--------------------------------------------------------

--------------------------------------------------------
-- Begin: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS

evalBigStep : (e : Term [] t) -> (e' : Term [] t ** (Value e', BigStep e e'))
evalBigStep (TVar i)     = absurd $ FinZAbsurd i
evalBigStep (TAbs x)     = (TAbs x ** (VAbs, BStValue VAbs))
evalBigStep (TApp x y)   = case evalBigStep x of
  (ex ** (VZero  , bStx))   impossible
  (ex ** (VSucc _, bStx))   impossible
  (TAbs ex ** (VAbs, bStx)) => let (ey ** (_ , bSty)) = evalBigStep y
                                   (er ** (vr, bStr)) = evalBigStep (subst ey FZ ex)
                               in (er ** (vr, BStApp bStx bSty bStr))
evalBigStep (TRec x y z) = case evalBigStep x of
  (TZero    ** (_, bStx)) => let (ey ** (vy, bSty)) = evalBigStep y
                             in (ey ** (vy, BStRecZero bStx bSty))
  (TSucc ex ** (_, bStx)) => let (es ** (vs, bSts)) = evalBigStep (subst ex FZ (subst (TRec ex y z) FZ z))
                             in (es ** (vs, BStRecSucc bStx bSts))
evalBigStep TZero        = (TZero ** (VZero, BStValue VZero))
evalBigStep (TSucc x)    = let (ex ** (vx, bStx)) = evalBigStep x
                           in (TSucc ex ** (VSucc vx, BStSucc bStx))
evalBigStep (TPred x)    = case evalBigStep x of
  (TZero    ** (_, bStx)) => (TZero ** (VZero, BStPredZero bStx))
  (TSucc ex ** (VSucc vx, bStx)) => (ex ** (vx, BStPredSucc bStx))
evalBigStep (TIfz x y z) = case evalBigStep x of
  (TZero    ** (_, bStx)) => let (ey ** (vy, bSty)) = evalBigStep y
                             in (ey ** (vy, BStIfzZero bStx bSty))
  (TSucc ex ** (VSucc vx, bStx)) => let (ez ** (vz, bStz)) = evalBigStep z
                                    in (ez ** (vz, BStIfzSucc bStx bStz))

-- End: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS
------------------------------------------------------

-----------------------------------
-- Begin: EQUIVALENCE OF EVALUATORS

total equivEval : (eval e1) = (e2 ** (v2, tst2)) ->
                  (evalBigStep e1) = (e3 ** (v3, bSt3)) ->
                  e2 = e3
equivEval {v2 = v2} {tst2 = tst2} {bSt3 = bSt3} _ _ =
  let (tst3, v3) = bigStepToTransStep bSt3
  in transStepDeterministic v2 tst2 v3 tst3

-- End: EQUIVALENCE OF EVALUATORS
---------------------------------

--------------------------------------------------
-- Begin: ENVIRONMENT-BASED/DENOTATIONAL EVALUATOR

total denoteType : Ty -> Type
denoteType TyNat         = Nat
denoteType (TyFun t1 t2) = denoteType t1 -> denoteType t2

data Env : Context n -> Type where
  ENil  : Env []
  ECons : denoteType t -> Env ctx -> Env (t::ctx)

total lookup : {ctx : Context n} ->
               (i : Fin n) -> Env ctx -> denoteType (index i ctx)
lookup FZ      (ECons x _)    = x
lookup (FS i') (ECons _ env') = lookup i' env'

total primRec : Nat -> t -> (Nat -> t -> t) -> t
primRec Z     e0 e1 = e0
primRec (S n) e0 e1 = e1 n (primRec n e0 e1)

total evalEnv' : Env ctx -> Term ctx t -> denoteType t
evalEnv' env (TVar i {prf}) = rewrite (sym prf) in lookup i env
evalEnv' env (TAbs e)       = \x => evalEnv' (ECons x env) e
evalEnv' env (TApp e1 e2)   = (evalEnv' env e1) (evalEnv' env e2)
evalEnv' env (TRec e e0 e1) = let e'  = evalEnv' env e
                                  e0' = evalEnv' env e0
                                  e1' = \n => \x => (evalEnv' (ECons x (ECons n env)) e1)
                              in primRec e' e0' e1'
evalEnv' env TZero          = Z
evalEnv' env (TSucc e)      = S (evalEnv' env e)
evalEnv' env (TPred e)      = case evalEnv' env e of
                                   Z   => Z
                                   S n => n
evalEnv' env (TIfz e1 e2 e3) = case evalEnv' env e1 of
                                    Z   => evalEnv' env e2
                                    S _ => evalEnv' env e3

total evalEnv : Term [] TyNat -> Nat
evalEnv = evalEnv' ENil

-- End: ENVIRONMENT-BASED/DENOTATIONAL EVALUATOR
------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
||| Sets and display version of Idris.
module Idris.Version

import IdrisPaths
import Data.List

%default total

||| Semantic versioning with optional tag
||| See [semver](https://semver.org/) for proper definition of semantic versioning
public export
record Version where
  constructor MkVersion
  ||| Semantic version
  ||| Should follow the (major, minor, patch) convention
  semVer : (Nat, Nat, Nat)
  ||| Optional tag
  ||| Usually contains git sha1 of this software's build in between releases
  versionTag : Maybe String

export
version : Version
version with (idrisVersion)
 version | (s,"") = MkVersion s Nothing
 version | (s,t) = MkVersion s (Just t)

export
showVersion : Bool -> Version -> String
showVersion tag (MkVersion (maj,min,patch) versionTag) =
  concat (intersperse "." (map show [ maj, min, patch])) ++
         if tag then showTag else ""
  where
    showTag : String
    showTag = case versionTag of
                Nothing => ""
                Just tag => "-" ++ tag


text:
> module Num.Refinements

> %default total

> %access public export

> |||
> interface (Num t) => NumPlusZeroNeutral t where
>   plusZeroLeftNeutral  : (x : t) -> 0 + x = x
>   plusZeroRightNeutral : (x : t) -> x + 0 = x

> |||
> interface (NumPlusZeroNeutral t) => NumPlusAssociative t where
> -- interface (Num t) => NumPlusAssociative t where
>   plusAssociative : (x, y, z : t) -> x + (y + z) = (x + y) + z

> |||
> interface (NumPlusAssociative t) => NumMultZeroOne t where
> -- interface (Num t) => NumMultZeroOne t where
>   multZeroRightZero   : (x : t) -> x * 0 = 0
>   multZeroLeftZero    : (x : t) -> 0 * x = 0
>   multOneRightNeutral : (x : t) -> x * 1 = x
>   multOneLeftNeutral  : (x : t) -> 1 * x = x

> |||
> interface (NumMultZeroOne t) => NumMultDistributesOverPlus t where
> -- interface (Num t) => NumMultDistributesOverPlus t where
>   multDistributesOverPlusRight : (x, y, z : t) -> x * (y + z) = (x * y) + (x * z)
>   multDistributesOverPlusLeft  : (x, y, z : t) -> (x + y) * z = (x * z) + (y * z)


text:
module Main

greet : IO ()
greet = do putStr "What is your name? "
           name <- getLine
           putStrLn ("Hello, dear " ++ name)

max_stars_repo_name: nunet-io/snet-ai-dsl

max_issues_repo_name: nunet-io/snet-ai-dsl

max_forks_repo_name: nunet-io/snet-ai-dsl


text:
-- %logging compile.casetree 5
-- %logging eval.casetree 5

-- %logging declare.def.lhs 5

bad : (a : Type) -> (x : a) -> String
bad String "good" = "good"
bad (List Nat) [1,2] = "good"
bad Char 'c' = "good"
bad _ _ = "bad"


text:
import Data.Vect

insSort: Vect n elem -> Vect n elem
insSort xs = ?insSort_rhs


text:
module Extra.Applicative

import Data.Vect

infixl 3 <*>|, *>|, <*|

||| Lazy version of Applicative, provides `<*>|`
public export
interface Applicative f => LazyApplicative f where
  (<*>|) : f (a -> b) -> Lazy (f a) -> f b

||| Lazy version of `*>|`
export
(*>|) : LazyApplicative f => f a -> Lazy (f b) -> f b
a *>| b = map (const id) a <*>| b

||| Lazy version of `<*|`
export
(<*|) : LazyApplicative f => f a -> Lazy (f b) -> f a
a <*| b = map (\a => const a) a <*>| b

||| 'Execute' an applicative repeatedly for `n` times
export
count : Applicative f => (n : Nat) -> f a -> f (Vect n a)
count Z p = pure Nil
count (S n) p = (::) <$> p <*> count n p

||| 'Execute' an applicative and neglect the output
export
skip : Applicative f => f a -> f ()
skip p = p $> ()


text:
module Scheme.DParser

import Data.List

%default total
%access public export

namespace Helpers

  data NonEmptyList : Type -> Type where
    MkNEList : (xs : List a ** NonEmpty xs) -> NonEmptyList a

  -- Functor NonEmptyList where
  --   map f (MkNEList (x :: xs ** IsNonEmpty)) = MkNEList (f x :: map f xs ** IsNonEmpty)

  neWeaken : NonEmptyList a -> List a
  neWeaken (MkNEList (xs ** _)) = xs

  neLeftApp : NonEmptyList a -> List a -> NonEmptyList a
  neLeftApp (MkNEList ((x :: xs) ** _)) ys = MkNEList (x :: (xs ++ ys) ** IsNonEmpty)

  neRightApp : List a -> NonEmptyList a -> NonEmptyList a
  neRightApp []        ys = ys
  neRightApp (x :: xs) ys = MkNEList (x :: (xs ++ neWeaken ys) ** IsNonEmpty)

  neBothApp : NonEmptyList a -> NonEmptyList a -> NonEmptyList a
  neBothApp xs ys = neRightApp (neWeaken xs) ys

  Semigroup (NonEmptyList a) where
    (<+>) = neBothApp

  data EqTo : {a : Type} -> (t : a) -> Type where
    MkET : (x : a ** x = t) -> EqTo t

  etWeaken : {t : a} -> EqTo t -> a
  etWeaken (MkET (x ** _)) = x

  data OneOf : {a : Type} -> List a -> Type where
    MkOO : (o : a ** Elem o os) -> OneOf os

  ooWeaken : {os : List a} -> OneOf os -> a
  ooWeaken (MkOO (o ** _)) = o

  eqPromoteToChoice : EqTo t -> OneOf [t]
  eqPromoteToChoice (MkET (x ** prf)) = MkOO (x ** rewrite sym prf in Here)

namespace Parser

  ||| Left values are for parse errors
  ||| Right values are parsed symbols and the rest of the string
  record Parser a where
    constructor MkParser
    parse : String -> Either String (a, String)

  Functor Parser where
    map f (MkParser u) =
      MkParser $ \inp =>
      case u inp of
           Left  err       => Left err
           Right (r, inp') => Right (f r, inp')

  Applicative Parser where
    pure x =
      MkParser $ \inp =>
      Right (x, inp)
    (<*>) (MkParser f) u =
      MkParser $ \inp =>
      case f inp of
           Left  err        => Left err
           Right (f', inp') => parse (map f' u) inp'

  ||| Left-biased "or"
  Alternative Parser where
    empty = MkParser $ const $ Left "No parse"
    (<|>) (MkParser u) (MkParser v) =
      MkParser $ \inp =>
      case u inp of
           Left  _   => v inp
           Right res => Right res

  Monad Parser where
    (>>=) u f =
      MkParser $ \inp =>
      case parse u inp of
           Left  err       => Left err
           Right (r, inp') => parse (f r) inp'

  Semigroup a => Semigroup (Parser a) where
    (<+>) u v = [| u <+> v |]

  Monoid a => Monoid (Parser a) where
    neutral = MkParser $ \inp => Right (neutral, inp)

  noParse : String -> Parser a
  noParse err = MkParser $ \_ => Left err

  infixr 10 <?>
  (<?>) : Parser a -> String -> Parser a
  (<?>) u err = u <|> noParse err

  optional : Parser a -> Parser (Maybe a)
  optional u =
    MkParser $ \inp =>
    case parse u inp of
         Left  err       => Right (Nothing, inp )
         Right (r, inp') => Right (Just r , inp')

  many : Parser a -> Parser (List a)
  many u = do
    r <- optional u
    case r of
         Nothing => neutral
         Just x  => [| pure x :: assert_total (many u) |]

  some : Parser a -> Parser (NonEmptyList a)
  some u = do
    x  <- u
    xs <- many u
    pure $ MkNEList (x :: xs ** IsNonEmpty)

  exactly : Parser a -> Parser (NonEmptyList a)
  exactly u = do
    x <- u
    pure $ MkNEList ([x] ** IsNonEmpty)

  notFollowedBy : Parser a -> Parser ()
  notFollowedBy u =
    MkParser $ \inp =>
    case parse u inp of
         Left  _         => Right ((), inp)
         Right (_, inp') => Left $ "Shouldn't have parsed a token. Rest of the input: " ++ show inp'

  satisfy : (Char -> Bool) -> Parser Char
  satisfy p =
    MkParser $ \inp =>
    case unpack inp of
         []        => Left "Unexpected EOF"
         (x :: xs) => case p x of
                           False => Left $ "Can't match char '" ++ pack [x] ++ "'"
                           True  => Right (x, pack xs)

  anyChar : Parser Char
  anyChar = satisfy (const True)

  eof : Parser ()
  eof = notFollowedBy anyChar

  char : Char -> Parser Char
  char c = satisfy (c ==)

  notChar : Char -> Parser Char
  notChar c = satisfy (c /=)

  oneOf : List Char -> Parser Char
  oneOf cs = satisfy (\c => elem c cs)

  noneOf : List Char -> Parser Char
  noneOf cs = satisfy (\c => not $ elem c cs)

  string : List Char -> Parser (List Char)
  string = sequence . map char

  sepBy1 : Parser a -> Parser sep -> Parser (NonEmptyList a)
  sepBy1 u v = do
    x  <- u
    xs <- many (v *> u)
    pure $ MkNEList (x :: xs ** IsNonEmpty)

  sepBy : Parser a -> Parser sep -> Parser (List a)
  sepBy u v = map neWeaken (sepBy1 u v) <|> neutral

  endBy1 : Parser a -> Parser sep -> Parser (NonEmptyList a)
  endBy1 u v = sepBy1 u v <* v

  endBy : Parser a -> Parser sep -> Parser (List a)
  endBy u v = map neWeaken (endBy1 u v) <|> neutral

  skipMany : Parser a -> Parser ()
  skipMany u = many u *> pure ()

  skipSome : Parser a -> Parser ()
  skipSome u = some u *> pure ()

  -- Concrete useful parsers

  lower : Parser Char
  lower = satisfy isLower

  upper : Parser Char
  upper = satisfy isUpper

  letter : Parser Char
  letter = satisfy isAlpha

  digit : Parser Char
  digit = satisfy isDigit

  alphaNum : Parser Char
  alphaNum = satisfy isAlphaNum

namespace DependentParser

  char' : (c : Char) -> Parser (EqTo c)
  char' c =
    MkParser $ \inp =>
    case unpack inp of
         []        => Left "Unexpected EOF"
         (x :: xs) => case (decEq x c) of
                           Yes prf => Right (MkET (x ** prf), pack xs)
                           No  _   => Left $ "Can't match char '" ++ pack [x] ++ "'"

  string' : (s : List Char) -> Parser (EqTo s)
  string' []        = pure $ (MkET ([] ** Refl))
  string' (c :: cs) = do
    MkET (x  ** p) <- char' c
    MkET (xs ** q) <- string' cs
    pure $ MkET $
      rewrite sym p in
      rewrite sym q in
      (x :: xs ** Refl)

  oneOf' : (cs : List Char) -> Parser (OneOf cs)
  oneOf' cs =
    MkParser $ \inp =>
    case unpack inp of
         []        => Left "Unexpected EOF"
         (x :: xs) => case (isElem x cs) of
                           Yes prf => Right (MkOO (x ** prf), pack xs)
                           No  _   => Left $ "Can't match char '" ++ pack [x] ++ "'"

  infixr 10 <%>
  ||| like <|> but preserves restrictions
  (<%>): Parser (EqTo w) -> Parser (EqTo z) -> Parser (OneOf [w, z])
  (<%>) u v =
    MkParser $ \inp =>
    case parse u inp of
         Left  _ => case parse v inp of
                         Left  _ => Left "Can't match both chars" -- FIXME
                         Right (MkET (x ** prf), inp') => Right (rewrite sym prf in MkOO (x ** There Here), inp')
         Right (MkET (x ** prf), inp') => Right (rewrite sym prf in MkOO (x ** Here), inp')

  -- TODO rethink the restrictions in terms of boolean predicates so we can just compute some && and ||
  -- Too much structure, the order of elements is irrelevant here
  -- strangeConsOr : Parser (EqTo w) -> Parser (OneOf zs) -> Parser (OneOf (w :: zs))
  -- strangeConsApp : Parser (OneOf ws) -> Parser (OneOf zs) -> Parser (OneOf (ws ++ zs))
  -- seq' : {s1, s2 : List Char} -> Parser (EqTo s1) -> Parser (EqTo s2) ->


text:
> module SequentialDecisionProblems.TabBackwardsInductionOptDefaults

> import Data.Vect

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> 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.TabBackwardsInduction.tcvalargmax {n} x r v ps =
>   Opt.Operations.argmax totalPreorderLTE (finiteGoodCtrl n x) (cardNotZGoodCtrl n x v) (tcval x r v ps)

> {-

> ---}


text:
module Srirams.Odds
-- S.Sriram (14487)

import Evens

import Intro

-- 1 --
data IsOdd : Nat -> Type where
  OOdd : IsOdd 1
  SSOdd : (x : Nat) -> (IsOdd x) -> IsOdd (S (S x))

-- 2 --
threeOdd : IsOdd 3
threeOdd = SSOdd 1 OOdd

-- 3 --
twoOdd : IsOdd 2 -> Void
twoOdd (SSOdd Z OOdd) impossible
twoOdd (SSOdd Z (SSOdd _ _)) impossible

-- 4 --
nOddSnEven : (n : Nat) -> (IsOdd n) -> (IsEven (S n))
nOddSnEven (S Z) OOdd = SSEven 0 ZEven
nOddSnEven (S (S x)) (SSOdd x y) = SSEven (S x) (nOddSnEven x y)

-- 5 --
nEvenSnOdd : (n : Nat) -> (IsEven n) -> (IsOdd (S n))
nEvenSnOdd Z ZEven = OOdd
nEvenSnOdd (S (S x)) (SSEven x y) = SSOdd (S x) (nEvenSnOdd x y)

-- 6 --
nEvenOrOdd : (n : Nat) -> Either (IsEven n) (IsOdd n)
nEvenOrOdd Z = Left ZEven
nEvenOrOdd (S k) = case (nEvenOrOdd k) of
                        (Left l) => Right (nEvenSnOdd k l)
                        (Right r) => Left (nOddSnEven k r)

-- 7 --
nNotBothEandO : (n : Nat) -> IsEven n -> IsOdd n -> Void
nNotBothEandO Z ZEven OOdd impossible
nNotBothEandO Z ZEven (SSOdd _ _) impossible
nNotBothEandO (S (S k)) (SSEven k x) (SSOdd k y) = nNotBothEandO k x y

-- 8 --
nmOddaddEven : (n : Nat) -> IsOdd n -> (m: Nat) -> IsOdd m -> IsEven (add n m)
nmOddaddEven (S Z) OOdd (S Z) OOdd = SSEven 0 ZEven
nmOddaddEven (S Z) OOdd (S (S x)) (SSOdd x y) = SSEven (S x) (nOddSnEven x y)
nmOddaddEven (S (S x)) (SSOdd x z) m y = (nOddSnEven (S (add x m)) (nEvenSnOdd (add x m) (nmOddaddEven x z m y)))

-- Auxillary --
aux : (f : Nat -> Nat) -> (n : Nat) -> (m : Nat) -> n = m -> f n = f m
aux f m m (Refl {x = m}) = Refl {x = f m}

-- 9 --
minuOnebyTwo : (n: Nat) -> IsOdd n -> (k: Nat ** S (double k) = n)
minuOnebyTwo (S Z) OOdd = (Z ** Refl {x = 1})
minuOnebyTwo (S (S k)) (SSOdd k x) = step where
  step = case (minuOnebyTwo k x) of
            (m ** pf) => ((S m) ** aux (\l => S (S l)) (S (double m)) k pf)


text:
module Text.Parser.Core

import Data.Bool
import Data.List
import Data.List1

import public Control.Delayed
import public Text.Bounded

%default total

-- TODO: Add some primitives for helping with error messages.
-- e.g. perhaps set a string to state what we're currently trying to
-- parse, or to say what the next expected token is in words

||| Description of a language's grammar. The `tok` parameter is the type
||| of tokens, and the `consumes` flag is True if the language is guaranteed
||| to be non-empty - that is, successfully parsing the language is guaranteed
||| to consume some input.
export
data Grammar : (state : Type) -> (tok : Type) -> (consumes : Bool) -> Type -> Type where
     Empty : (val : ty) -> Grammar state tok False ty
     Terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
     NextIs : String -> (tok -> Bool) -> Grammar state tok False tok
     EOF : Grammar state tok False ()

     Fail : (location : Maybe Bounds) -> (fatal : Bool) -> String -> Grammar state tok c ty
     Try : Grammar state tok c ty -> Grammar state tok c ty

     Commit : Grammar state tok False ()
     MustWork : Grammar state tok c a -> Grammar state tok c a

     SeqEat : {c2 : Bool} ->
              Grammar state tok True a -> Inf (a -> Grammar state tok c2 b) ->
              Grammar state tok True b
     SeqEmpty : {c1, c2 : Bool} ->
                Grammar state tok c1 a -> (a -> Grammar state tok c2 b) ->
                Grammar state tok (c1 || c2) b

     ThenEat : {c2 : Bool} ->
               Grammar state tok True () -> Inf (Grammar state tok c2 a) ->
               Grammar state tok True a
     ThenEmpty : {c1, c2 : Bool} ->
                 Grammar state tok c1 () -> Grammar state tok c2 a ->
                 Grammar state tok (c1 || c2) a

     Alt : {c1, c2 : Bool} ->
           Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) ->
           Grammar state tok (c1 && c2) ty
     Bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
     Position : Grammar state tok False Bounds

     Act : state -> Grammar state tok False ()

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume some input. If the first one consumes input, the
||| second is allowed to be recursive (because it means some input has been
||| consumed and therefore the input is smaller)
export %inline
(>>=) : {c1, c2 : Bool} ->
        Grammar state tok c1 a ->
        inf c1 (a -> Grammar state tok c2 b) ->
        Grammar state tok (c1 || c2) b
(>>=) {c1 = False} = SeqEmpty
(>>=) {c1 = True}  = SeqEat

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume some input. If the first one consumes input, the
||| second is allowed to be recursive (because it means some input has been
||| consumed and therefore the input is smaller)
public export %inline %tcinline
(>>) : {c1, c2 : Bool} ->
        Grammar state tok c1 () ->
        inf c1 (Grammar state tok c2 a) ->
        Grammar state tok (c1 || c2) a
(>>) {c1 = False} = ThenEmpty
(>>) {c1 = True} = ThenEat

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume input. This is an explicitly non-infinite version
||| of `>>=`.
export %inline
seq : {c1,c2 : Bool} ->
      Grammar state tok c1 a ->
      (a -> Grammar state tok c2 b) ->
      Grammar state tok (c1 || c2) b
seq = SeqEmpty

||| Sequence a grammar followed by the grammar it returns.
export %inline
join : {c1,c2 : Bool} ->
       Grammar state tok c1 (Grammar state tok c2 a) ->
       Grammar state tok (c1 || c2) a
join {c1 = False} p = SeqEmpty p id
join {c1 = True} p = SeqEat p id

||| Allows the result of a grammar to be mapped to a different value.
export
{c : _} ->
Functor (Grammar state tok c) where
  map f (Empty val)  = Empty (f val)
  map f (Fail bd fatal msg) = Fail bd fatal msg
  map f (Try g) = Try (map f g)
  map f (MustWork g) = MustWork (map f g)
  map f (Terminal msg g) = Terminal msg (map f . g)
  map f (Alt x y)    = Alt (map f x) (map f y)
  map f (SeqEat act next)
      = SeqEat act (\val => map f (next val))
  map f (SeqEmpty act next)
      = SeqEmpty act (\ val => map f (next val))
  map f (ThenEat act next)
      = ThenEat act (map f next)
  map f (ThenEmpty act next)
      = ThenEmpty act (map f next)
  map {c} f (Bounds act)
    = rewrite sym $ orFalseNeutral c in
      SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act)
  -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
  -- so a sequence must be used.
  map {c = False} f p = SeqEmpty p (Empty . f)

||| Give two alternative grammars. If both consume, the combination is
||| guaranteed to consume.
export %inline
(<|>) : {c1,c2 : Bool} ->
        Grammar state tok c1 ty ->
        Lazy (Grammar state tok c2 ty) ->
        Grammar state tok (c1 && c2) ty
(<|>) = Alt

infixr 2 <||>
||| Take the tagged disjunction of two grammars. If both consume, the
||| combination is guaranteed to consume.
export
(<||>) : {c1,c2 : Bool} ->
        Grammar state tok c1 a ->
        Lazy (Grammar state tok c2 b) ->
        Grammar state tok (c1 && c2) (Either a b)
(<||>) p q = (Left <$> p) <|> (Right <$> q)

||| Sequence a grammar with value type `a -> b` and a grammar
||| with value type `a`. If both succeed, apply the function
||| from the first grammar to the value from the second grammar.
||| Guaranteed to consume if either grammar consumes.
export %inline
(<*>) : {c1, c2 : Bool} ->
        Grammar state tok c1 (a -> b) ->
        Grammar state tok c2 a ->
        Grammar state tok (c1 || c2) b
(<*>) x y = SeqEmpty x (\f => map f y)

||| Sequence two grammars. If both succeed, use the value of the first one.
||| Guaranteed to consume if either grammar consumes.
export %inline
(<*) : {c1,c2 : Bool} ->
       Grammar state tok c1 a ->
       Grammar state tok c2 b ->
       Grammar state tok (c1 || c2) a
(<*) x y = map const x <*> y

||| Sequence two grammars. If both succeed, use the value of the second one.
||| Guaranteed to consume if either grammar consumes.
export %inline
(*>) : {c1,c2 : Bool} ->
       Grammar state tok c1 a ->
       Grammar state tok c2 b ->
       Grammar state tok (c1 || c2) b
(*>) x y = map (const id) x <*> y

export %inline
act : state -> Grammar state tok False ()
act = Act

||| Produce a grammar that can parse a different type of token by providing a
||| function converting the new token type into the original one.
export
mapToken : (a -> b) -> Grammar state b c ty -> Grammar state a c ty
mapToken f (Empty val) = Empty val
mapToken f (Terminal msg g) = Terminal msg (g . f)
mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
mapToken f EOF = EOF
mapToken f (Fail bd fatal msg) = Fail bd fatal msg
mapToken f (Try g) = Try (mapToken f g)
mapToken f (MustWork g) = MustWork (mapToken f g)
mapToken f Commit = Commit
mapToken f (SeqEat act next)
  = SeqEat (mapToken f act) (\x => mapToken f (next x))
mapToken f (SeqEmpty act next)
  = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
mapToken f (ThenEat act next)
  = ThenEat (mapToken f act) (mapToken f next)
mapToken f (ThenEmpty act next)
  = ThenEmpty (mapToken f act) (mapToken f next)
mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
mapToken f (Bounds act) = Bounds (mapToken f act)
mapToken f Position = Position
mapToken f (Act action) = Act action

||| Always succeed with the given value.
export %inline
pure : (val : ty) -> Grammar state tok False ty
pure = Empty

||| Check whether the next token satisfies a predicate
export %inline
nextIs : String -> (tok -> Bool) -> Grammar state tok False tok
nextIs = NextIs

||| Look at the next token in the input
export %inline
peek : Grammar state tok False tok
peek = nextIs "Unrecognised token" (const True)

||| Succeeds if running the predicate on the next token returns Just x,
||| returning x. Otherwise fails.
export %inline
terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
terminal = Terminal

||| Always fail with a message
export %inline
fail : String -> Grammar state tok c ty
fail = Fail Nothing False

||| Always fail with a message and a location
export %inline
failLoc : Bounds -> String -> Grammar state tok c ty
failLoc b = Fail (Just b) False

||| Fail with no possibility for recovery (i.e.
||| no alternative parsing can succeed).
export %inline
fatalError : String -> Grammar state tok c ty
fatalError = Fail Nothing True

||| Fail with no possibility for recovery (i.e.
||| no alternative parsing can succeed).
export %inline
fatalLoc : Bounds -> String -> Grammar state tok c ty
fatalLoc b = Fail (Just b) True

||| Catch a fatal error
export %inline
try : Grammar state tok c ty -> Grammar state tok c ty
try = Try

||| Succeed if the input is empty
export %inline
eof : Grammar state tok False ()
eof = EOF

||| Commit to an alternative; if the current branch of an alternative
||| fails to parse, no more branches will be tried
export %inline
commit : Grammar state tok False ()
commit = Commit

||| If the parser fails, treat it as a fatal error
export %inline
mustWork : {c : Bool} -> Grammar state tok c ty -> Grammar state tok c ty
mustWork = MustWork

export %inline
bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
bounds = Bounds

export %inline
position : Grammar state tok False Bounds
position = Position

public export
data ParsingError tok = Error String (Maybe Bounds)

data ParseResult : Type -> Type -> Type -> Type where
     Failure : (committed : Bool) -> (fatal : Bool) ->
               List1 (ParsingError tok) -> ParseResult state tok ty
     Res : state -> (committed : Bool) ->
           (val : WithBounds ty) -> (more : List (WithBounds tok)) -> ParseResult state tok ty

mergeWith : WithBounds ty -> ParseResult state tok sy -> ParseResult state tok sy
mergeWith x (Res s committed val more) = Res s committed (mergeBounds x val) more
mergeWith x v = v

doParse : Semigroup state => state -> (commit : Bool) ->
          (act : Grammar state tok c ty) ->
          (xs : List (WithBounds tok)) ->
          ParseResult state tok ty
doParse s com (Empty val) xs = Res s com (irrelevantBounds val) xs
doParse s com (Fail location fatal str) xs
    = Failure com fatal (Error str (location <|> (bounds <$> head' xs)) ::: Nil)
doParse s com (Try g) xs = case doParse s com g xs of
  -- recover from fatal match but still propagate the 'commit'
  Failure com _ errs => Failure com False errs
  res => res
doParse s com Commit xs = Res s True (irrelevantBounds ()) xs
doParse s com (MustWork g) xs =
  case assert_total (doParse s com g xs) of
       Failure com' _ errs => Failure com' True errs
       res => res
doParse s com (Terminal err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
doParse s com (Terminal err f) (x :: xs) =
  case f x.val of
       Nothing => Failure com False (Error err (Just x.bounds) ::: Nil)
       Just a => Res s com (const a <$> x) xs
doParse s com EOF [] = Res s com (irrelevantBounds ()) []
doParse s com EOF (x :: xs) = Failure com False (Error "Expected end of input" (Just x.bounds) ::: Nil)
doParse s com (NextIs err f) [] = Failure com False (Error "End of input" Nothing ::: Nil)
doParse s com (NextIs err f) (x :: xs)
      = if f x.val
           then Res s com (removeIrrelevance x) (x :: xs)
           else Failure com False (Error err (Just x.bounds) ::: Nil)
doParse s com (Alt {c1} {c2} x y) xs
    = case doParse s False x xs of
           Failure com' fatal errs
              => if com' || fatal
                        -- If the alternative had committed, don't try the
                        -- other branch (and reset commit flag)
                   then Failure com fatal errs
                   else case (assert_total doParse s False y xs) of
                             (Failure com'' fatal' errs') => if com'' || fatal'
                                                                     -- Only add the errors together if the second branch
                                                                     -- is also non-committed and non-fatal.
                                                             then Failure com'' fatal' errs'
                                                             else Failure False False (errs ++ errs')
                             (Res s _ val xs) => Res s com val xs
           -- Successfully parsed the first option, so use the outer commit flag
           Res s _ val xs => Res s com val xs
doParse s com (SeqEmpty act next) xs
    = case assert_total (doParse s com act xs) of
           Failure com fatal errs => Failure com fatal errs
           Res s com v xs =>
             mergeWith v (assert_total $ doParse s com (next v.val) xs)
doParse s com (SeqEat act next) xs
    = case assert_total (doParse s com act xs) of
           Failure com fatal errs => Failure com fatal errs
           Res s com v xs =>
             mergeWith v (assert_total $ doParse s com (next v.val) xs)
doParse s com (ThenEmpty act next) xs
    = case assert_total (doParse s com act xs) of
           Failure com fatal errs => Failure com fatal errs
           Res s com v xs =>
             mergeWith v (assert_total $ doParse s com next xs)
doParse s com (ThenEat act next) xs
    = case assert_total (doParse s com act xs) of
           Failure com fatal errs => Failure com fatal errs
           Res s com v xs =>
             mergeWith v (assert_total $ doParse s com next xs)
doParse s com (Bounds act) xs
    = case assert_total (doParse s com act xs) of
           Failure com fatal errs => Failure com fatal errs
           Res s com v xs => Res s com (const v <$> v) xs
doParse s com Position [] = Failure com False (Error "End of input" Nothing ::: Nil)
doParse s com Position (x :: xs)
    = Res s com (irrelevantBounds x.bounds) (x :: xs)
doParse s com (Act action) xs = Res (s <+> action) com (irrelevantBounds ()) xs

||| Parse a list of tokens according to the given grammar. If successful,
||| returns a pair of the parse result and the unparsed tokens (the remaining
||| input).
export
parse : {c : Bool} -> (act : Grammar () tok c ty) -> (xs : List (WithBounds tok)) ->
        Either (List1 (ParsingError tok)) (ty, List (WithBounds tok))
parse act xs
    = case doParse neutral False act xs of
           Failure _ _ errs => Left errs
           Res _ _ v rest => Right (v.val, rest)

export
parseWith : Monoid state => {c : Bool} -> (act : Grammar state tok c ty) -> (xs : List (WithBounds tok)) ->
        Either (List1 (ParsingError tok)) (state, ty, List (WithBounds tok))
parseWith act xs
    = case doParse neutral False act xs of
           Failure _ _ errs => Left errs
           Res s _ v rest => Right (s, v.val, rest)


text:
{-
Copyright 2019, 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.
-}

module StwfFFI.Utils

%access public export
%default total

%include C "consoleUtils.h"
%include C "soc_AM335x.h"
%include C "beaglebone.h"

-- Initialize the UART console
consoleUtilsInit : IO ()
consoleUtilsInit =
    foreign FFI_C "ConsoleUtilsInit" (IO ())

-- Select the console type based on compile time check
consoleUtilsSetType : Int -> IO ()
consoleUtilsSetType t =
    foreign FFI_C "ConsoleUtilsSetType" (Int -> IO ()) t

consoleUtilsPrintf : String -> IO ()
consoleUtilsPrintf str =
    foreign FFI_C "ConsoleUtilsPrintf" (String -> IO ()) str

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
import System.Concurrency.Channels

data Message = Add Nat Nat

data MessagePID = MkMessage PID

data ProcState = Ready | Sent | Looping

data Process : Type -> ProcState -> ProcState -> Type where
     Request : MessagePID -> Message -> Process Nat st st
     Respond : ((msg : Message) -> Process Nat Ready Ready) ->
               Process (Maybe Message) st Sent
     Spawn : Process () Ready Looping ->
             Process (Maybe MessagePID) st st

     Loop : Inf (Process a Ready Looping) ->
            Process a Sent Looping
     Action : IO a -> Process a st st
     Pure : a -> Process a st st
     (>>=) : Process a st1 st2 -> (a -> Process b st2 st3) ->
             Process b st1 st3

public export
data Fuel = Dry | More (Lazy Fuel)

export partial
forever : Fuel
forever = More forever

total
run : Fuel -> Process t in_state out_state -> IO (Maybe t)
run fuel (Request (MkMessage process) msg)
          = do Just chan <- connect process
                    | _ => pure Nothing
               ok <- unsafeSend chan msg
               if ok then do Just x <- unsafeRecv Nat chan
                                  | Nothing => pure Nothing
                             pure (Just x)
                     else pure Nothing
run fuel (Respond f)
          = do Just sender <- listen 1
                    | Nothing => pure (Just Nothing)
               Just msg <- unsafeRecv Message sender
                    | Nothing => pure (Just Nothing)
               Just res <- run fuel (f msg)
                    | Nothing => pure Nothing
               unsafeSend sender res
               pure (Just (Just msg))
run (More fuel) (Loop proc) = run fuel proc
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                                | Nothing => pure (Just Nothing)
                           pure (Just (Just (MkMessage pid)))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                                  | Nothing => pure Nothing
                             run fuel (next x)
run Dry _ = pure Nothing

Service : Type -> Type
Service a = Process a Ready Looping

Client : Type -> Type
Client a = Process a Ready Ready

{-
procAdder_bad1 : Process () Ready Looping
procAdder_bad1 = do Action (putStrLn "I'm out of the office today")
                    Loop procAdder_bad1

procAdder_bad2 : Process () Ready Looping
procAdder_bad2 = Loop procAdder_bad2
                    -}

procAdder : Service ()
procAdder = do Respond (\msg => case msg of
                                     Add x y => Pure (x + y))
               Loop procAdder

procMain : Client ()
procMain = do Just adder_id <- Spawn procAdder
                   | Nothing => Action (putStrLn "Spawn failed")
              answer <- Request adder_id (Add 2 3)
              Action (printLn answer)

partial
runProc : Process () in_state out_state -> IO ()
runProc proc = do run forever proc
                  pure ()

main : IO ()
main = runProc procMain

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
> import Data.Vect

> import Enumerated.Enumerated

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

> data Foo = Zero | One
>
> implementation Enumerated Foo 2 where
>   values = [Zero, One]
>   toFin Zero = 0
>   toFin  One = 1
>   values_match_toFin = Refl
>
> implementation Eq Foo where
>   x  == y  = toFin x == toFin y


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Const
import Data.Contravariant

||| Const Functor.
public export
data Const : (0 a : Type) -> (b : Type) -> Type where
  MkConst: a -> Const a b

public export
getConst : Const a b -> a
getConst (MkConst x) = x

public export
Functor (Const a) where
  map _ (MkConst x) = (MkConst x)

public export
Contravariant (Const a) where
  contramap _ (MkConst x) = (MkConst x)

public export
implementation Monoid m => Applicative (Const m) where
  pure _                      = MkConst neutral
  (MkConst f) <*> (MkConst v) = MkConst (f <+> v)

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


text:
module Python.Lib.Queue

import Python
import Data.Erased

%default total
%access public export

Queue : Type -> Signature
Queue a f = case f of
  "put" => [a]   ~~> ()
  "get" => [Int] ~~> a
  "task_done" => [] ~~> ()
  _ => Object f

QueueM : Signature
QueueM f = case f of
  "Queue" => fun $
    forall a : Type .
      default maxSize : Int = 0 .  -- default: 0 = no limit
        Return $ Obj (Queue a)

  _ => Module f

import_ : PIO $ Obj QueueM
import_ = importModule "Queue"  -- this is lowercase in python3

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Elabs
import Language.Reflection.Elab
import Derive.Show

%language ElabReflection
-- https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Language/Reflection/Elab.idr

addDecls : Elab ()
addDecls = do
--  declareType (Declare (UN "Tpe") [] (RType) )
--  intro `{{x}}
--  declareType $ Declare `{{FF}} []  RType
  declareDatatype $ Declare `{{FF}} []  RType
  defineDatatype $ DefineDatatype `{{FF}} []
--  let xs = map (\x=>declareType (Declare (UN x) [] (RType) )) [""]
  pure ()

-- data FF
%runElab addDecls

xx : FF -> ()
xx x = ()

%runElab (deriveShow `{{FF}})
-- %runElab defineFunction (DefineFun (UN "myf") [MkFunClause (Var `{{x}}) (Var `{{x}})  ])
-- %runElab `{{}}`
{-
xxx : Tpe -> IO ()
xxx _  = do
  print ""
-}

idNat : Nat -> Nat
idNat = %runElab (do intro `{{x}}
                     fill (Var `{{x}})
                     solve)

max_stars_repo_name: justjoheinz/tensorflow-idris

max_issues_repo_name: doofin/differentiable-idris

max_forks_repo_name: doofin/differentiable-idris


text:
module Data.Crypto

%default total

public
class Masher m (b : Nat) where
  blockLength : Nat

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
%foreign "scheme:my-mul"
myMul : Int -> Int -> Int

main : IO ()
main = do
  putStrLn $ "6 * 7 = " ++ show (myMul 6 7)


text:
module Inigo.PkgTree

import Data.List
import Data.SortedMap
import Data.SortedSet as Set
import Inigo.Paths

%default total

public export
interface Ord name => HasDeps pkg name where
    getDeps : Bool -> pkg -> List name

-- DEBUG
export
Ord name => HasDeps (List name) name where
    getDeps _ deps = deps

parameters (dev : Bool)

    %inline
    lengthNotIn :
        (done : SortedSet name) ->
        (deps : SortedSet name) ->
        Nat
    lengthNotIn done deps = foldl go 0 deps
    where
        go : Nat -> name -> Nat
        go len dep = if contains dep done
            then len
            else 1 + len

    %inline
    %spec hasDeps
    lookupDeps :
        Show name =>
        (hasDeps : HasDeps pkg name) =>
        SortedMap name pkg ->
        name ->
        Either String (SortedSet name)
    lookupDeps ctxt n = case lookup n ctxt of
        Nothing => Left "Unkown package: \{show n}"
        Just pkg => Right $ fromList $ getDeps dev pkg

    %inline
    %spec hasDeps
    findLeaves :
        Show name =>
        (hasDeps : HasDeps pkg name) =>
        (ctxt : SortedMap name pkg) ->
        List name ->
        (done : SortedSet name) ->
        (todo : SortedSet name) ->
        Either String (List name)
    findLeaves ctxt build done todo = foldlM go [] todo
    where
        go : List name -> name -> Either String (List name)
        go leaves n = do
            deps <- lookupDeps ctxt n
            case lengthNotIn done deps of
                0 => Right $ n :: leaves
                _ => Right leaves

    deleteFrom :
        List a ->
        SortedSet a ->
        SortedSet a
    deleteFrom [] set = set
    deleteFrom (x :: xs) set = deleteFrom xs (delete x set)

    insertFrom :
        List a ->
        SortedSet a ->
        SortedSet a
    insertFrom [] set = set
    insertFrom (x :: xs) set = insertFrom xs (insert x set)

    export
    %spec hasDeps
    kahn :
        Show name =>
        (hasDeps : HasDeps pkg name) =>
        (ctxt : SortedMap name pkg) ->
        (build : List name) ->
        (done : SortedSet name) ->
        (todo : SortedSet name) ->
        Either String (List name)
    kahn ctxt build done todo = if null todo
        then Right $ reverse build
        else do
            leaves@(_ :: _) <- findLeaves ctxt build done todo
                | [] => do
                    let todoList = Set.toList todo
                    deps <- traverse (\pkg => (pkg,) . Set.toList <$> lookupDeps ctxt pkg) todoList
                    if DEBUG
                        then Left "Cyclic dependencies:\n\{show todoList},\ndeps: \{show deps},\nbuild so far: \{show $ reverse build}"
                        else Left "Cyclic dependencies: \{show todoList}"
            kahn ctxt (leaves ++ build) (insertFrom leaves done) (assert_smaller todo $ deleteFrom leaves todo)

    export
    %spec hasDeps
    %inline
    getBuildOrder :
        Show name =>
        (hasDeps : HasDeps pkg name) =>
        (ctxt : SortedMap name pkg) ->
        SortedSet name ->
        Either String (List name)
    getBuildOrder ctxt todo = kahn ctxt [] empty todo

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Lightyear
import Lightyear.Strings

import HydraBot.Types

numeric : Parser Int
numeric = foldl (\x,y => x * 10 + y) 0 . map (cast . finToNat) <$> ntimes 3 digit

middle : Parser String
middle = pack <$> (some $ satisfy $ not . isSpace)

trailing : Parser String
trailing = pack <$> many (satisfy $ not . flip List.elem ['\r', '\n'])

params : Parser (List String)
params = space *> ((pure <$> (char ':' *> trailing)) <|> ((::) <$> middle <*>| params))

command : Parser (Either String Int)
command = Right <$> numeric <|> Left <$> middle

prefix' : Parser Prefix
prefix' = User <$> (uname <* (char '!' *> middle))
        <|> Server <$> middle
  where
    uname : Parser String
    uname = pack <$> (some $ satisfy (not . flip List.elem ['\r', '\n', ' ', '!']))

message : Parser Message
message = Msg
        <$> ((char ':' *> Just <$> prefix' <* space) <|> (pure Nothing))
        <*> command
        <*> params
        <*  string "\r\n"

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
import Data.Vect

total allLengths' : Vect len String -> Vect len Nat
allLengths' [] = []
allLengths' (word :: words) = length word :: allLengths' words

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
data PowerSource = Petrol | Pedal | Electic

data Vehicle : PowerSource -> Type where
  Unicycle : Vehicle Pedal
  Bicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : (battery : Nat) -> Vehicle Electic
  ElectricCar : (battery : nat) -> Vehicle Electic

wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Bicycle = 2
wheels (Motorcycle fuel) = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels (Tram battery) = 16
wheels (ElectricCar battery) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Motorcycle fuel) = Motorcycle 50
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Tram battery) = Tram 1000
refuel (ElectricCar battery) = ElectricCar 300


text:
{-
HOW TO:
1) install cabal and idris
2) run:
$ idris hello.idr -o hello
$ ./hello
-}

module Main

main : IO ()
main = putStrLn "Hello world"

max_stars_repo_name: kennethsequeira/Hello-world

max_issues_repo_name: kennethsequeira/Hello-world

max_forks_repo_name: kennethsequeira/Hello-world


text:
-- Implementation based on https://www.newspipe.org/article/public/309714

module Crypto.Hash.Poly1305

import Data.Vect
import Utils.Misc
import Utils.Bytes
import Data.Bits
import Crypto.Hash

export
record Poly1305 where
  constructor MkPoly1305
  buffer : List Bits8
  h : Vect 3 Bits64
  r : Vect 2 Bits64
  s : Vect 2 Bits64

record Bits128 where
  constructor MkBits128
  lo : Bits64
  hi : Bits64

mask_low_2_bits : Bits64
mask_low_2_bits  = 0x0000000000000003

mask_not_low_2_bits : Bits64
mask_not_low_2_bits = complement mask_low_2_bits

p0 : Bits64
p0 = 0xFFFFFFFFFFFFFFFB

p1 : Bits64
p1 = 0xFFFFFFFFFFFFFFFF

p2 : Bits64
p2 = 0x0000000000000003

add64 : Bits64 -> Bits64 -> Bits64 -> (Bits64, Bits64)
add64 x y carry =
  let sum = x + y + carry
      carry = shiftR ((x .&. y) .|. ((x .|. y) .&. (complement sum))) 63
  in (sum, carry)

sub64 : Bits64 -> Bits64 -> Bits64 -> (Bits64, Bits64)
sub64 x y borrow =
  let diff = x - y - borrow
      borrow_out = shiftR ((complement x .&. y) .|. (diff .&. complement (x `xor` y))) 63
  in (diff, borrow_out)

mul64_mask32 : Bits64
mul64_mask32 = cast (the Bits32 oneBits)

mul64 : Bits64 -> Bits64 -> Bits128
mul64 x y =
  let x0 = x .&. mul64_mask32
      x1 = shiftR x 32
      y0 = y .&. mul64_mask32
      y1 = shiftR y 32
      w0 = x0 * y0
      t = (x1 * y0) + (shiftR w0 32)
      w1 = t .&. mul64_mask32
      w2 = shiftR t 32
      w1 = w1 + (x0 * y1)
  in MkBits128 (x * y) (x1 * y1 + w2 + (shiftR w1 32))

add128 : Bits128 -> Bits128 -> Bits128
add128 a b =
  let (lo, c) = add64 a.lo b.lo 0
      (hi, _) = add64 a.hi b.hi c
  in MkBits128 lo hi

shiftr2 : Bits128 -> Bits128
shiftr2 a = MkBits128 ((shiftR a.lo 2) .|. (shiftL (a.hi .&. 3) 62)) (shiftR a.hi 2)

-- select64 returns x if v == 1 and y if v == 0, in constant time
select64 : Bits64 -> Bits64 -> Bits64 -> Bits64
select64 v x y = (x .&. complement (v - 1)) .|. (y .&. (v - 1))

core : Poly1305 -> Bits64 -> Bits64 -> Bits64 -> (Bits64, Bits64, Bits64)
core state h0 h1 h2 =
  let [r0, r1] = state.r

      h0r0 = mul64 h0 r0
      h1r0 = mul64 h1 r0
      h2r0 = mul64 h2 r0
      h0r1 = mul64 h0 r1
      h1r1 = mul64 h1 r1
      h2r1 = mul64 h2 r1

      m0 = h0r0
      m1 = add128 h1r0 h0r1
      m2 = add128 h2r0 h1r1
      m3 = h2r1

      t0 = m0.lo
      (t1, c) = add64 m1.lo m0.hi 0
      (t2, c) = add64 m2.lo m1.hi c
      (t3, _) = add64 m3.lo m2.hi c

      h0 = t0
      h1 = t1
      h2 = t2 .&. mask_low_2_bits
      cc = MkBits128 (t2 .&. mask_not_low_2_bits) t3

      (h0, c) = add64 h0 cc.lo 0
      (h1, c) = add64 h1 cc.hi c
      h2 = h2 + c

      cc = shiftr2 cc

      (h0, c) = add64 h0 cc.lo 0
      (h1, c) = add64 h1 cc.hi c
      h2 = h2 + c
  in (h0, h1, h2)

update' : Poly1305 -> Poly1305
update' state =
  case splitAtExact 16 state.buffer of
    Just (buf, rest) =>
      let (a, b) = bimap from_le from_le (splitAt 8 buf)
          [h0, h1, h2] = state.h
          (h0, c) = add64 h0 a 0
          (h1, c) = add64 h1 b c
          h2 = h2 + c + 1
          (h0, h1, h2) = core state h0 h1 h2
      in {h := [h0, h1, h2]} state
    Nothing => state

finalize' : Poly1305 -> Vect 16 Bits8
finalize' state =
  case exactLength 16 (fromList state.buffer) of
    Just buf =>
      let (a, b) = bimap from_le from_le (splitAt 8 buf)
          [h0, h1, h2] = state.h
          (h0, c) = add64 h0 a 0
          (h1, c) = add64 h1 b c
          h2 = h2 + c
          (h0, h1, h2) = core state h0 h1 h2

          (t0, b) = sub64 h0 p0 0
          (t1, b) = sub64 h1 p1 b
          (_ , b) = sub64 h2 p2 b

          h0 = select64 b h0 t0
          h1 = select64 b h1 t1

          [s0, s1] = state.s
          (h0, c) = add64 h0 s0 0
          (h1, _) = add64 h1 s1 c
      in to_le {n=8} h0 ++ to_le {n=8} h1
    Nothing =>
      finalize' $ { buffer := pad_zero 16 (state.buffer <+> [ 0x01 ]) } (update' state)

export
Digest Poly1305 where
  digest_nbyte = 16
  update message state = update' $ {buffer := state.buffer <+> message} state
  finalize = finalize'

export
MAC (Vect 32 Bits8) Poly1305 where
  initialize_mac key =
    let ([r0, r1], s) = splitAt 2 $ map from_le $ group 4 8 key
        r0 = r0 .&. 0x0FFFFFFC0FFFFFFF
        r1 = r1 .&. 0x0FFFFFFC0FFFFFFC
    in MkPoly1305 [] [0,0,0] [r0, r1] s


text:
module Libraries.Text.Distance.Levenshtein

import Data.List
import Data.Maybe
import Data.String
import Libraries.Data.IOMatrix
import Libraries.Data.List.Extra

%default total

||| Self-evidently correct but O(3 ^ (min mn)) complexity
spec : String -> String -> Nat
spec a b = loop (fastUnpack a) (fastUnpack b) where

  loop : List Char -> List Char -> Nat
  loop [] ys = length ys -- deletions
  loop xs [] = length xs -- insertions
  loop (x :: xs) (y :: ys)
    = if x == y then loop xs ys -- match
      else 1 + minimum [ loop (x :: xs) ys -- insert y
                       , loop xs (y :: ys) -- delete x
                       , loop xs ys        -- substitute y for x
                       ]

||| Dynamic programming
export
compute : HasIO io => String -> String -> io Nat
compute a b = do
  let w = strLength a
  let h = strLength b
  -- In mat[i][j], we store the distance between
  -- * the suffix of a of size i
  -- * the suffix of b of size j
  -- So we need a matrix of size (|a|+1) * (|b|+1)
  mat <- new (w+1) (h+1)
  -- Whenever one of the two suffixes of interest is empty, the only
  -- winning move is to:
  -- * delete all of the first
  -- * insert all of the second
  -- i.e. the cost is the length of the non-zero suffix
  for_ [0..w] $ \ i => write mat i 0 i -- deletions
  for_ [0..h] $ \ j => write mat 0 j j -- insertions

  -- We introduce a specialised `read` for ease of use
  let get = \i, j => case !(read {io} mat i j) of
        Nothing => assert_total $
          idris_crash "INTERNAL ERROR: Badly initialised matrix"
        Just n => pure n

  -- We fill the matrix from the bottom up, using the same formula we used
  -- in the specification's `loop`.
  for_ [1..h] $ \ j => do
    for_ [1..w] $ \ i => do
      -- here we change Levenshtein slightly so that we may only substitute
      -- alpha / numerical characters for similar ones. This avoids suggesting
      -- "#" as a replacement for an out of scope "n".
      let cost = let c = assert_total $ strIndex a (i-1)
                     d = assert_total $ strIndex b (j-1)
                 in if c == d then 0 else
                    if isAlpha c && isAlpha d then 1 else
                    if isDigit c && isDigit d then 1 else 2
      write mat i j $
        minimum [ 1    + !(get i (j-1))     -- insert y
                , 1    + !(get (i-1) j)     -- delete x
                , cost + !(get (i-1) (j-1)) -- equal or substitute y for x
                ]

  -- Once the matrix is fully filled, we can simply read the top right corner
  integerToNat . cast <$> get w h


text:
module Web.Raw.Clipboard

import JS
import Web.Internal.ClipboardPrim
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace Clipboard

  export
  read : (obj : Clipboard) -> JSIO (Promise (Array ClipboardItem))
  read a = primJS $ Clipboard.prim__read a

  export
  readText : (obj : Clipboard) -> JSIO (Promise String)
  readText a = primJS $ Clipboard.prim__readText a

  export
  write :  (obj : Clipboard)
        -> (data_ : Array ClipboardItem)
        -> JSIO (Promise Undefined)
  write a b = primJS $ Clipboard.prim__write a b

  export
  writeText : (obj : Clipboard) -> (data_ : String) -> JSIO (Promise Undefined)
  writeText a b = primJS $ Clipboard.prim__writeText a b

namespace ClipboardEvent

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem ClipboardEventInit (Types t1)}
      -> (type : String)
      -> (eventInitDict : Optional t1)
      -> JSIO ClipboardEvent
  new a b = primJS $ ClipboardEvent.prim__new a (optUp b)

  export
  new' : (type : String) -> JSIO ClipboardEvent
  new' a = primJS $ ClipboardEvent.prim__new a undef

  export
  clipboardData : (obj : ClipboardEvent) -> JSIO (Maybe DataTransfer)
  clipboardData a = tryJS "ClipboardEvent.clipboardData"
                  $ ClipboardEvent.prim__clipboardData a

namespace ClipboardItem

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem ClipboardItemOptions (Types t1)}
      -> (items : Record String (Promise (Union2 String Blob)))
      -> (options : Optional t1)
      -> JSIO ClipboardItem
  new a b = primJS $ ClipboardItem.prim__new a (optUp b)

  export
  new' :  (items : Record String (Promise (Union2 String Blob)))
       -> JSIO ClipboardItem
  new' a = primJS $ ClipboardItem.prim__new a undef

  export
  createDelayed :  (0 _ : JSType t1)
                => {auto 0 _ : Elem ClipboardItemOptions (Types t1)}
                -> (items : Record String ClipboardItemDelayedCallback)
                -> (options : Optional t1)
                -> JSIO ClipboardItem
  createDelayed a b = primJS $ ClipboardItem.prim__createDelayed a (optUp b)

  export
  createDelayed' :  (items : Record String ClipboardItemDelayedCallback)
                 -> JSIO ClipboardItem
  createDelayed' a = primJS $ ClipboardItem.prim__createDelayed a undef

  export
  delayed : (obj : ClipboardItem) -> JSIO Bool
  delayed a = tryJS "ClipboardItem.delayed" $ ClipboardItem.prim__delayed a

  export
  lastModified : (obj : ClipboardItem) -> JSIO JSInt64
  lastModified a = primJS $ ClipboardItem.prim__lastModified a

  export
  presentationStyle : (obj : ClipboardItem) -> JSIO PresentationStyle
  presentationStyle a = tryJS "ClipboardItem.presentationStyle"
                      $ ClipboardItem.prim__presentationStyle a

  export
  types : (obj : ClipboardItem) -> JSIO (Array String)
  types a = primJS $ ClipboardItem.prim__types a

  export
  getType : (obj : ClipboardItem) -> (type : String) -> JSIO (Promise Blob)
  getType a b = primJS $ ClipboardItem.prim__getType a b

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace ClipboardEventInit

  export
  new :  (clipboardData : Optional (Maybe DataTransfer))
      -> JSIO ClipboardEventInit
  new a = primJS $ ClipboardEventInit.prim__new (toFFI a)

  export
  new' : JSIO ClipboardEventInit
  new' = primJS $ ClipboardEventInit.prim__new undef

  export
  clipboardData :  (0 _ : JSType t)
                => {auto 0 _ : Elem ClipboardEventInit (Types t)}
                -> t
                -> Attribute True Optional (Maybe DataTransfer)
  clipboardData v = fromUndefOrPrim "ClipboardEventInit.getclipboardData"
                                    prim__clipboardData
                                    prim__setClipboardData
                                    Nothing
                                    (v :> ClipboardEventInit)

namespace ClipboardItemOptions

  export
  new :  (presentationStyle : Optional PresentationStyle)
      -> JSIO ClipboardItemOptions
  new a = primJS $ ClipboardItemOptions.prim__new (toFFI a)

  export
  new' : JSIO ClipboardItemOptions
  new' = primJS $ ClipboardItemOptions.prim__new undef

  export
  presentationStyle :  (0 _ : JSType t)
                    => {auto 0 _ : Elem ClipboardItemOptions (Types t)}
                    -> t
                    -> Attribute False Optional PresentationStyle
  presentationStyle v = fromUndefOrPrimNoDefault "ClipboardItemOptions.getpresentationStyle"
                                                 prim__presentationStyle
                                                 prim__setPresentationStyle
                                                 (v :> ClipboardItemOptions)

namespace ClipboardPermissionDescriptor

  export
  new :  (allowWithoutGesture : Optional Bool)
      -> JSIO ClipboardPermissionDescriptor
  new a = primJS $ ClipboardPermissionDescriptor.prim__new (toFFI a)

  export
  new' : JSIO ClipboardPermissionDescriptor
  new' = primJS $ ClipboardPermissionDescriptor.prim__new undef

  export
  allowWithoutGesture :  (0 _ : JSType t)
                      => {auto 0 _ : Elem ClipboardPermissionDescriptor (Types t)}
                      -> t
                      -> Attribute True Optional Bool
  allowWithoutGesture v = fromUndefOrPrim "ClipboardPermissionDescriptor.getallowWithoutGesture"
                                          prim__allowWithoutGesture
                                          prim__setAllowWithoutGesture
                                          False
                                          (v :> ClipboardPermissionDescriptor)

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

namespace ClipboardItemDelayedCallback

  export
  toClipboardItemDelayedCallback :  (() -> IO (Promise (Union2 String Blob)))
                                 -> JSIO ClipboardItemDelayedCallback
  toClipboardItemDelayedCallback cb = primJS $ prim__toClipboardItemDelayedCallback cb


text:
{-
 Proofs for Functor Laws!
 (Redefined from Idris' Interfaces.Verified)
-}

module Play.FunctorLaws

||| Redefined from Interfaces.Verified with slight name changes
interface Functor f => VerifiedFunctor (f : Type -> Type) where
  identityLaw : (x : f a) -> map Basics.id x = Basics.id x
  distLaw : (x : f a) ->
        (g : b -> c) -> (h : a -> b) -> map (g . h) x = (map g) . (map h) $ x

VerifiedFunctor Maybe where
  identityLaw Nothing = Refl
  identityLaw (Just _) = Refl

  distLaw Nothing _ _ = Refl
  distLaw (Just _) _ _  = Refl

||| Hurah! Who needs unit tests!
VerifiedFunctor List where
  identityLaw [] = Refl
  identityLaw (x::xs) = let ih = (identityLaw xs) in cong ih

  distLaw [] _ _ = Refl
  distLaw (x::xs) g h  = let ih = (distLaw xs g h) in cong ih

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes