text:
module VectRankedElem

import Data.Vect
import Decidable.Order

%default total

public export
data RankedElem : ty -> Vect _ ty -> (idx : Nat) -> Type where
  Here : {v : Vect (S _) ty} -> RankedElem (head v) v Z
  There : RankedElem a xs idx -> RankedElem a (x::xs) (S idx)

export
indexSmallerThanSize : {v : Vect size ty} -> {idx : Nat} -> RankedElem x v idx -> LT idx size
indexSmallerThanSize {size = Z} _ impossible
indexSmallerThanSize {size = S len} Here = shift Z len zeroAlwaysSmaller
indexSmallerThanSize {size = S len} {v = (x::xs)} {idx = S n} (There elem)
  = shift (S n) len $ indexSmallerThanSize elem

export
Uninhabited (RankedElem _ [] _) where
  uninhabited _ impossible

export
cons_ : (x : ty) -> (v : Vect size ty)
     -> (ret : Vect (S size) ty
         ** ({a : ty} -> {n : Nat} -> RankedElem a v n -> RankedElem a ret (S n),
             RankedElem x ret Z))
cons_ x [] = ([x] ** (absurd, Here))
cons_ x (y::ys) = (x::y::ys ** (f, Here))
                  where f : {a : ty} -> {n : Nat} -> RankedElem a (y::ys) n -> RankedElem a (x::y::ys) (S n)
                        f elem = There elem

export
cons : ty -> Vect size ty -> Vect (S size) ty
cons x v = fst $ cons_ x v

export
concat_ : {size1, size2 : Nat}
       -> (v1 : Vect size1 ty) -> (v2 : Vect size2 ty)
       -> (ret : Vect (size1 + size2) ty
           ** ({a : ty} -> {n : Nat} -> RankedElem a v1 n -> RankedElem a ret n,
               {a : ty} -> {n : Nat} -> RankedElem a v2 n -> RankedElem a ret (size1 + n)))
concat_ [] ys = (ys ** (absurd, id))
concat_ {size1} xs [] = rewrite plusZeroRightNeutral size1 in
                        (xs ** (id, absurd))
concat_ (x::xs) (y::ys) = let (ret ** (f, g)) = xs `concat_` (y::ys) in
                          (x :: ret ** (ff f, gg g))
                          where ff : {ret : Vect (size1 + size2) ty}
                                  -> ({a : ty} -> {n : Nat} -> RankedElem a xs n -> RankedElem a ret n)
                                  -> {a : ty} -> {n : Nat} -> (RankedElem a (x::xs) n -> RankedElem a (x::ret) n)
                                ff f Here = Here
                                ff f (There elem) = There $ f elem
                                gg : {ret : Vect (size1 + size2) ty}
                                  -> ({a : ty} -> {n : Nat} -> RankedElem a (y::ys) n -> RankedElem a ret (size1 + n))
                                  -> {a : ty} -> {n : Nat} -> (RankedElem a (y::ys) n -> RankedElem a (x::ret) (S $ size1 + n))
                                gg g elem = There $ g elem

export
concat : {size1, size2 : Nat} -> Vect size1 ty -> Vect size2 ty -> Vect (size1 + size2) ty
concat v1 v2 = fst $ concat_ v1 v2

export
rev_ : {size : Nat} -> (orig : Vect size ty)
    -> (ret : Vect size ty ** {a : ty} -> {n : Nat} -> RankedElem a orig n -> RankedElem a ret (size `minus` (S n)))
rev_ [] = ([] ** absurd)
rev_ ((::) {len} x xs) = rewrite plusCommutative 1 len in
                         let (sx ** h) = rev_ xs
                             (ret ** (f, g)) = sx `concat_` [x] in
                         (ret ** fgh f g h)
                         where fgh : ({a : ty} -> {n : Nat} -> RankedElem a sx n -> RankedElem a ret n)
                                  -> ({a : ty} -> {n : Nat} -> RankedElem a [x] n -> RankedElem a ret (len + n))
                                  -> ({a : ty} -> {n : Nat} -> RankedElem a xs n -> RankedElem a sx (len `minus` (S n)))
                                  -> {a : ty} -> {n : Nat} -> RankedElem a (x::xs) n -> RankedElem a ret (len `minus` n)
                               fgh f g h Here = rewrite minusZeroRight len in
                                                rewrite sym $ plusZeroRightNeutral len in
                                                g Here
                               fgh f g h (There elem) = f $ h elem

export
rev : {size : Nat} -> Vect size ty -> Vect size ty
rev v = fst $ rev_ v

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect

data ShellCmd : (ty : Type) -> Access -> (ty -> Access) -> Type where
    Password : String -> ShellCmd PwdCheck LoggedOut
        (\check =>
            case check of
                Correct => LoggedIn
                Incorrect => LoggedOut)
    Logout : ShellCmd () LoggedIn (const LoggedOut)
    GetSecret : ShellCmd String LoggedIn (const LoggedIn)

    PutStr : String -> ShellCmd () state (const state)
    Pure : (res : ty) -> ShellCmd ty (stateFn res) stateFn
    (>>=) : ShellCmd a state1 state2Fn ->
            ((res : a) -> ShellCmd b (state2Fn res) state3Fn) ->
            ShellCmd b state1 state3Fn

session : ShellCmd () LoggedOut (const LoggedOut)
session =
    do
        Correct <- Password "wurzel"
            | Incorrect => PutStr "Wrong password"
        msg <- GetSecret
        PutStr ("Secret code: " ++ show msg ++ "\n")
        Logout

-- sessionBad : ShellCmd () LoggedOut (const LoggedOut)
-- sessionBad =
--     do
--         Password "wurzel"
--         msg <- GetSecret
--         PutStr ("Secret code: " ++ show msg ++ "\n")
--         Logout

-- noLogout : ShellCmd () LoggedOut (const LoggedOut)
-- noLogout =
--     do
--         Correct <- Password "wurzel"
--             | Incorrect => PutStr "Wrong password"
--         msg <- GetSecret
--         PutStr ("Secret code: " ++ show msg ++ "\n")

ext: idr


text:
module Toolkit.Data.DList.Any

import Toolkit.Decidable.Informative

import Toolkit.Data.DList

import public Toolkit.Decidable.Equality.Indexed

%default total

||| Proof that some element satisfies the predicate
|||
||| @idx   The type of the element's index.
||| @type  The type of the list element.
||| @p     A predicate
||| @xs      The list itself.
public export
data Any : (idx    : Type)
        -> (type   : idx -> Type)
        -> (p      : {i : idx} -> (x : type i) -> Type)
        -> {is     : List idx}
        -> (xs     : DList idx type is)
                  -> Type
    where
      ||| Proof that the element is at the front of the list.
      H : {p : {i : idx} -> (x : type i) -> Type}
       -> {i   : idx}
       -> {y   : type i}
       -> (prf : p y)
              -> Any idx type p (y :: xs)

      ||| Proof that the element is found later in the list.
      T : {p : {i : idx} -> (x : type i) -> Type}
       -> (contra : p x' -> Void)
       -> (later : Any idx type p       xs)
                -> Any idx type p (x' ::xs)

empty : {p : {i : idx} -> (x : type i) -> Type} -> Any idx type p Nil -> Void
empty (H prf) impossible
empty (T contra later) impossible

isNotThere : {p : {i : idx} -> (x : type i) -> Type}
          -> (Any idx type p rest -> Void)
          -> (p i -> Void)
          -> Any idx type p (i :: rest) -> Void
isNotThere f g (H prf) = g prf
isNotThere f g (T contra later) = f later

export
any : {p : {i : idx} -> (x : type i) -> Type}
   -> (f : {i : idx} -> (x : type i) -> DecInfo err (p x))
   -> (xs : DList idx type is)
         -> Dec (Any idx type p xs)
any f [] = No empty

any f (elem :: rest) with (f elem)
  any f (elem :: rest) | (Yes prfWhy)
    = Yes (H prfWhy)

  any f (elem :: rest) | (No msgWhyNot prfWhyNot) with (any f rest)
    any f (elem :: rest) | (No msgWhyNot prfWhyNot) | (Yes prfWhy)
      = Yes (T prfWhyNot prfWhy)
    any f (elem :: rest) | (No msgWhyNot prfWhyNot) | (No g)
      = No (isNotThere g prfWhyNot)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Main

main : IO ()
main = do printLn $ the Integer 429496729500000000000000
--           printLn $ the Integer 4294967296
--           printLn $ the Integer 4294967297
--           printLn $ the Int 4294967295
--           printLn $ the Int 4294967296
--           printLn $ the Int 4294967297

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module xquant.Core.Interpretation

import xquant.Core.Types

%default total

||| Represents a mapping of a model (vector space) to
||| a physical system. Denoted by descriptive strings
data Interpretation : Nat -> Type where
  Interpret : Vect n String -> Interpretation n

dim : Interpretation n -> Nat
dim {n} i = n

Interp : Type
Interp = (n : Nat ** Interpretation n)

{-}
||| Representation of a possibly-composite quantum system
||| @ n the dimensionality of the physical system
data System : (n : Nat) -> List Interp -> Type where
  ||| Representation of a quantum system with a distinct interpretation
  Single : (i : Interpretation n) -> System n [i]
  ||| Extend an quantum system by tensor multiplying by another hilbert space
  Extend : (i : Interpretation n) -> System m -> System (n * m)

-}

qubit : Interpretation 2
qubit = Interpret ["Spin up", "Spin down"]

||| Type-safe representation of choice combinatorics
||| @ n total objects
||| @ m remaining unchosen
|||
||| For example this works fine:
|||````idris example
|||Choose FZ . Choose (FS FZ) $ (ChZero 2)
|||````
||| However both of these do not:
|||````idris example
|||Choose FZ . Choose FZ . Choose FZ $ (ChZero 2)
|||````
|||````idris example
|||Choose (FS FZ) . Choose FZ $ (ChZero 2)
|||````
data Choice : (n : Nat) -> (m : Nat) -> Type where
  ||| No Choices yet
  ChZero : (n : Nat) -> Choice n n
  |||
  Choose : (f : Fin (S m)) -> Choice n (S m) -> Choice n m

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


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

import WebAssembly.Structure.Values
import WebAssembly.Structure.Modules.Indices

import Decidable.Equality

-- Definition

public export
data ExportDesc : Type where
  FuncExport   : FuncIdx   -> ExportDesc
  TableExport  : TableIdx  -> ExportDesc
  MemExport    : MemIdx    -> ExportDesc
  GlobalExport : GlobalIdx -> ExportDesc

public export
record Export where
  constructor MkExport
  name : Name
  desc : ExportDesc

-- Equality

total public export
lemma_funcexport__injective : ((f1 = f2) -> Void) -> (FuncExport f1 = FuncExport f2) -> Void
lemma_funcexport__injective f1_not_f2 Refl = f1_not_f2 Refl

total public export
lemma_tableexport__injective : ((t1 = t2) -> Void) -> (TableExport t1 = TableExport t2) -> Void
lemma_tableexport__injective t1_not_t2 Refl = t1_not_t2 Refl

total public export
lemma_memexport__injective : ((m1 = m2) -> Void) -> (MemExport m1 = MemExport m2) -> Void
lemma_memexport__injective m1_not_m2 Refl = m1_not_m2 Refl

total public export
lemma_globalexport__injective : ((g1 = g2) -> Void) -> (GlobalExport g1 = GlobalExport g2) -> Void
lemma_globalexport__injective g1_not_g2 Refl = g1_not_g2 Refl

total public export
lemma_funcexport_not_tableexport : (FuncExport f = TableExport t) -> Void
lemma_funcexport_not_tableexport Refl impossible

total public export
lemma_funcexport_not_memexport : (FuncExport f = MemExport m) -> Void
lemma_funcexport_not_memexport Refl impossible

total public export
lemma_funcexport_not_globalexport : (FuncExport f = GlobalExport g) -> Void
lemma_funcexport_not_globalexport Refl impossible

total public export
lemma_tableexport_not_funcexport : (TableExport t = FuncExport f) -> Void
lemma_tableexport_not_funcexport Refl impossible

total public export
lemma_tableexport_not_memexport : (TableExport t = MemExport m) -> Void
lemma_tableexport_not_memexport Refl impossible

total public export
lemma_tableexport_not_globalexport : (TableExport t = GlobalExport g) -> Void
lemma_tableexport_not_globalexport Refl impossible

total public export
lemma_memexport_not_tableexport : (MemExport m = TableExport t) -> Void
lemma_memexport_not_tableexport Refl impossible

total public export
lemma_memexport_not_funcxport : (MemExport m = FuncExport f) -> Void
lemma_memexport_not_funcxport Refl impossible

total public export
lemma_memexport_not_globalexport : (MemExport m = GlobalExport g) -> Void
lemma_memexport_not_globalexport Refl impossible

total public export
lemma_globalexport_not_tableexport : (GlobalExport g = TableExport t) -> Void
lemma_globalexport_not_tableexport Refl impossible

total public export
lemma_globalexport_not_funcxport : (GlobalExport g = FuncExport m) -> Void
lemma_globalexport_not_funcxport Refl impossible

total public export
lemma_globalexport_not_memexport : (GlobalExport g = MemExport m) -> Void
lemma_globalexport_not_memexport Refl impossible

total public export
lemma_export__name_injective : ((n1 = n2) -> Void) -> (MkExport n1 d1 = MkExport n2 d2) -> Void
lemma_export__name_injective n1_not_n2 Refl = n1_not_n2 Refl

total public export
lemma_export__desc_injective : ((d1 = d2) -> Void) -> (MkExport n1 d1 = MkExport n2 d2) -> Void
lemma_export__desc_injective d1_not_d2 Refl = d1_not_d2 Refl

-- Decidable Equality

public export
implementation DecEq ExportDesc where
  decEq (FuncExport x)   (FuncExport y)   = case decEq x y of
    No x_not_y => No $ lemma_funcexport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (FuncExport x)   (TableExport y)  = No lemma_funcexport_not_tableexport
  decEq (FuncExport x)   (MemExport y)    = No lemma_funcexport_not_memexport
  decEq (FuncExport x)   (GlobalExport y) = No lemma_funcexport_not_globalexport
  decEq (TableExport x)  (FuncExport y)   = No lemma_tableexport_not_funcexport
  decEq (TableExport x)  (TableExport y)  = case decEq x y of
    No x_not_y => No $ lemma_tableexport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (TableExport x)  (MemExport y)    = No lemma_tableexport_not_memexport
  decEq (TableExport x)  (GlobalExport y) = No lemma_tableexport_not_globalexport
  decEq (MemExport x)    (FuncExport y)   = No lemma_memexport_not_funcxport
  decEq (MemExport x)    (TableExport y)  = No lemma_memexport_not_tableexport
  decEq (MemExport x)    (MemExport y)    = case decEq x y of
    No x_not_y => No $ lemma_memexport__injective x_not_y
    Yes Refl   => Yes Refl
  decEq (MemExport x)    (GlobalExport y) = No lemma_memexport_not_globalexport
  decEq (GlobalExport x) (FuncExport y)   = No lemma_globalexport_not_funcxport
  decEq (GlobalExport x) (TableExport y)  = No lemma_globalexport_not_tableexport
  decEq (GlobalExport x) (MemExport y)    = No lemma_globalexport_not_memexport
  decEq (GlobalExport x) (GlobalExport y) = case decEq x y of
    No x_not_y => No $ lemma_globalexport__injective x_not_y
    Yes Refl   => Yes Refl

public export
implementation DecEq Export where
  decEq (MkExport n1 d1) (MkExport n2 d2) = case decEq n1 n2 of
    No n1_not_n2 => No $ lemma_export__name_injective n1_not_n2
    Yes Refl     => case decEq d1 d2 of
      No d1_not_d2 => No $ lemma_export__desc_injective d1_not_d2
      Yes Refl     => Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Flexidisc.Header.Sub

import Flexidisc.Header.Label
import Flexidisc.Header.Row
import Flexidisc.Header.Type
import Flexidisc.OrdList

%default total
%access public export

data Sub : (xs, ys : Header' k a) -> Type where
  S : {xs : OrdList k o a} -> {ys : OrdList k o a} ->
      Sub xs ys -> Sub (H xs) (H ys)

%hint
public export
rowFromSub : Sub xs ys -> Row key ty xs -> Row key ty ys
rowFromSub (S sub) (R lbl) = R (rowFromSub sub lbl)

%hint
public export
labelFromSub : Sub xs ys -> Label x xs -> Label x ys
labelFromSub (S sub) (L lbl) = L (labelFromSub sub lbl)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Prelude.Interfaces

import Builtin
import Prelude.Basics
import Prelude.EqOrd
import Prelude.Num
import Prelude.Ops

%default total

-------------
-- ALGEBRA --
-------------

||| Sets equipped with a single binary operation that is associative.  Must
||| satisfy the following laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
public export
interface Semigroup ty where
  (<+>) : ty -> ty -> ty

||| Sets equipped with a single binary operation that is associative, along with
||| a neutral element for that binary operation.  Must satisfy the following
||| laws:
|||
||| + Associativity of `<+>`:
|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
||| + Neutral for `<+>`:
|||     forall a, a <+> neutral == a
|||     forall a, neutral <+> a == a
public export
interface Semigroup ty => Monoid ty where
  neutral : ty

public export
Semigroup () where
  _ <+> _ = ()

public export
Monoid () where
  neutral = ()

public export
Semigroup Ordering where
  LT <+> _ = LT
  GT <+> _ = GT
  EQ <+> o =  o

public export
Monoid Ordering where
  neutral = EQ

public export
Semigroup b => Semigroup (a -> b) where
  (f <+> g) x = f x <+> g x

public export
Monoid b => Monoid (a -> b) where
  neutral _ = neutral

export
shiftL : Int -> Int -> Int
shiftL = prim__shl_Int

export
shiftR : Int -> Int -> Int
shiftR = prim__shr_Int

----------------------------------------------
-- FUNCTOR, APPLICATIVE, ALTERNATIVE, MONAD --
----------------------------------------------

||| Functors allow a uniform action over a parameterised type.
||| @ f a parameterised type
public export
interface Functor f where
  ||| Apply a function across everything of type 'a' in a parameterised type
  ||| @ f the parameterised type
  ||| @ func the function to apply
  map : (func : a -> b) -> f a -> f b

||| An infix alias for `map`, applying a function across everything of type 'a'
||| in a parameterised type.
||| @ f the parameterised type
||| @ func the function to apply
public export
(<$>) : Functor f => (func : a -> b) -> f a -> f b
(<$>) func x = map func x

||| Run something for effects, replacing the return value with a given parameter.
public export
(<$) : Functor f => b -> f a -> f b
(<$) b = map (const b)

||| Flipped version of `<$`.
public export
($>) : Functor f => f a -> b -> f b
($>) fa b = map (const b) fa

||| Run something for effects, throwing away the return value.
public export
ignore : Functor f => f a -> f ()
ignore = map (const ())

public export
interface Functor f => Applicative f where
  pure : a -> f a
  (<*>) : f (a -> b) -> f a -> f b

public export
(<*) : Applicative f => f a -> f b -> f a
a <* b = map const a <*> b

public export
(*>) : Applicative f => f a -> f b -> f b
a *> b = map (const id) a <*> b

%allow_overloads pure
%allow_overloads (<*)
%allow_overloads (*>)

public export
interface Applicative f => Alternative f where
  empty : f a
  (<|>) : f a -> f a -> f a

public export
interface Applicative m => Monad m where
  ||| Also called `bind`.
  (>>=) : m a -> (a -> m b) -> m b

  ||| Also called `flatten` or mu.
  join : m (m a) -> m a

  -- default implementations
  (>>=) x f = join (f <$> x)
  join x = x >>= id

%allow_overloads (>>=)

||| `guard a` is `pure ()` if `a` is `True` and `empty` if `a` is `False`.
public export
guard : Alternative f => Bool -> f ()
guard x = if x then pure () else empty

||| Conditionally execute an applicative expression.
public export
when : Applicative f => Bool -> Lazy (f ()) -> f ()
when True f = f
when False f = pure ()

---------------------------
-- FOLDABLE, TRAVERSABLE --
---------------------------

||| The `Foldable` interface describes how you can iterate over the elements in
||| a parameterised type and combine the elements together, using a provided
||| function, into a single result.
||| @ t The type of the 'Foldable' parameterised type.
public export
interface Foldable (t : Type -> Type) where
  ||| Successively combine the elements in a parameterised type using the
  ||| provided function, starting with the element that is in the final position
  ||| i.e. the right-most position.
  ||| @ func  The function used to 'fold' an element into the accumulated result
  ||| @ init  The starting value the results are being combined into
  ||| @ input The parameterised type
  foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc

  ||| The same as `foldr` but begins the folding from the element at the initial
  ||| position in the data structure i.e. the left-most position.
  ||| @ func  The function used to 'fold' an element into the accumulated result
  ||| @ init  The starting value the results are being combined into
  ||| @ input The parameterised type
  foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl f z t = foldr (flip (.) . flip f) id t z

||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
||| Consequently, the final value is wrapped in the same `Monad`.
public export
foldlM : (Foldable t, Monad m) => (funcM: a -> b -> m a) -> (init: a) -> (input: t b) -> m a
foldlM fm a0 = foldl (\ma,b => ma >>= flip fm b) (pure a0)

||| Combine each element of a structure into a monoid.
public export
concat : (Foldable t, Monoid a) => t a -> a
concat = foldr (<+>) neutral

||| Combine into a monoid the collective results of applying a function to each
||| element of a structure.
public export
concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
concatMap f = foldr ((<+>) . f) neutral

||| The conjunction of all elements of a structure containing lazy boolean
||| values.  `and` short-circuits from left to right, evaluating until either an
||| element is `False` or no elements remain.
public export
and : Foldable t => t (Lazy Bool) -> Bool
and = foldl (&&) True

||| The disjunction of all elements of a structure containing lazy boolean
||| values.  `or` short-circuits from left to right, evaluating either until an
||| element is `True` or no elements remain.
public export
or : Foldable t => t (Lazy Bool) -> Bool
or = foldl (||) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `any` short-circuits from left to right.
public export
any : Foldable t => (a -> Bool) -> t a -> Bool
any p = foldl (\x,y => x || p y) False

||| The disjunction of the collective results of applying a predicate to all
||| elements of a structure.  `all` short-circuits from left to right.
public export
all : Foldable t => (a -> Bool) -> t a -> Bool
all p = foldl (\x,y => x && p y)  True

||| Add together all the elements of a structure.
public export
sum : (Foldable t, Num a) => t a -> a
sum = foldr (+) 0

||| Add together all the elements of a structure.
||| Same as `sum` but tail recursive.
export
sum' : (Foldable t, Num a) => t a -> a
sum' = foldl (+) 0

||| Multiply together all elements of a structure.
public export
product : (Foldable t, Num a) => t a -> a
product = foldr (*) 1

||| Multiply together all elements of a structure.
||| Same as `product` but tail recursive.
export
product' : (Foldable t, Num a) => t a -> a
product' = foldl (*) 1

||| Map each element of a structure to a computation, evaluate those
||| computations and discard the results.
public export
traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()
traverse_ f = foldr ((*>) . f) (pure ())

||| Evaluate each computation in a structure and discard the results.
public export
sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
sequence_ = foldr (*>) (pure ())

||| Like `traverse_` but with the arguments flipped.
public export
for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
for_ = flip traverse_

||| Fold using Alternative.
|||
||| If you have a left-biased alternative operator `<|>`, then `choice` performs
||| left-biased choice from a list of alternatives, which means that it
||| evaluates to the left-most non-`empty` alternative.
|||
||| If the list is empty, or all values in it are `empty`, then it evaluates to
||| `empty`.
|||
||| Example:
|||
||| ```
||| -- given a parser expression like:
||| expr = literal <|> keyword <|> funcall
|||
||| -- choice lets you write this as:
||| expr = choice [literal, keyword, funcall]
||| ```
|||
||| Note: In Haskell, `choice` is called `asum`.
public export
choice : (Foldable t, Alternative f) => t (f a) -> f a
choice = foldr (<|>) empty

||| A fused version of `choice` and `map`.
public export
choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
choiceMap f = foldr (\e, a => f e <|> a) empty

public export
interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
  ||| Map each element of a structure to a computation, evaluate those
  ||| computations and combine the results.
  traverse : Applicative f => (a -> f b) -> t a -> f (t b)

||| Evaluate each computation in a structure and collect the results.
public export
sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)
sequence = traverse id

||| Like `traverse` but with the arguments flipped.
public export
for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
for = flip traverse


text:
import Data.List
import Data.List1
import Data.String

import System.File

fuel : List Int -> Int -> Int
fuel [] y = 0
fuel (x :: xs) y = abs (x - y) + fuel xs y

run : String -> IO ()
run s = do let l = catMaybes $ parseInteger {a=Int} <$> (forget $ split (== ',') s)
           let u = (\(c ::: _) => c) <$> (group $ sort $ l)
           let fs = head' $ sort $ fuel l <$> u
           putStrLn $ show fs

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
printLength : IO ()
printLength =
  putStr "Input: " >>= \_ =>
  getLine >>= \input =>
   let len = length input in
             putStrLn (show len)

printLength' : IO ()
printLength' = do
  putStr "Input: "
  input <- getLine
  let len = length input
  putStrLn (show len)

longest : IO ()
longest = do
  putStr "1: "
  in1 <- getLine
  putStr "2: "
  in2 <- getLine
  let len1 = length in1
  let len2 = length in2
  let longest = if len2 > len1 then in1 else in2
  putStrLn ("Longest: " ++ longest)

readNum : IO (Maybe Nat)
readNum = do
  input <- getLine
  let output =  if all isDigit (unpack input)
    then (Just (cast input))
    else Nothing
  pure output

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module IdrisNet.TCP.TCPServer
import Effects
import IdrisNet.Packet
import IdrisNet.PacketLang
import Network.Socket
import IdrisNet.TCP.TCPCommon

%access public

-- Closed -> Listening

{- Server States -}
data ServerBound : Type where
  SB : Socket -> ServerBound

data ServerListening : Type where
  SL : Socket -> ServerListening

data ServerError : Type where
  SE : Socket -> ServerError

data ClientConnected : Type where
  CC : Socket -> SocketAddress -> ClientConnected

data ClientError : Type where
  CE : Socket -> ClientError

{- Transition Functions -}
interpOperationRes : SocketOperationRes a -> Type
interpOperationRes (OperationSuccess _) = ServerListening
interpOperationRes (FatalError _) = ServerError
interpOperationRes (RecoverableError _) = ServerListening
interpOperationRes (ConnectionClosed) = ()

interpClientOperationRes : SocketOperationRes a -> Type
interpClientOperationRes (OperationSuccess _) = ClientConnected
interpClientOperationRes (FatalError _) = ClientError
interpClientOperationRes (RecoverableError _) = ClientConnected
interpClientOperationRes (ConnectionClosed) = ()

interpListenRes : SocketOperationRes a -> Type
interpListenRes (OperationSuccess _) = ServerListening
interpListenRes ConnectionClosed = ()
interpListenRes (RecoverableError _) = ServerBound
interpListenRes (FatalError _) = ServerError

interpTCPServerBindRes : SocketOperationRes a -> Type
interpTCPServerBindRes (OperationSuccess _) = ServerBound
interpTCPServerBindRes _ = ()

{- This is an effect that deals with an accepted client. We're allowed to
   read from, write to, and close this socket.
   An effectual program of type TCPSERVERCLIENT will be runInit, initially in the
   ClientConnected state, upon acceptance of a client. This will be given in the
   form of an argument to Accept. The effectual program must end by closing the socket. -}
data TCPServerClient : Effect where
  WriteString : String -> { ClientConnected ==> {result} interpClientOperationRes result}
                          TCPServerClient (SocketOperationRes ByteLength)
  ReadString : ByteLength -> { ClientConnected ==> {result} interpClientOperationRes result }
                             TCPServerClient (SocketOperationRes (String, ByteLength))
  CloseClient : { ClientConnected ==> () } TCPServerClient ()
  FinaliseClient : { ClientError ==> () }  TCPServerClient ()
  WritePacket  : (pl : PacketLang) ->
                 (mkTy pl) ->
                 { ClientConnected ==> {result} interpClientOperationRes result }
                 TCPServerClient (SocketOperationRes ByteLength)

  ReadPacket   : (pl : PacketLang) ->
                 Length -> -- I really dislike this sod being here
                 { ClientConnected ==> {result} interpClientOperationRes result }
                 TCPServerClient (SocketOperationRes (Maybe (mkTy pl, ByteLength)))

TCPSERVERCLIENT : Type -> EFFECT
TCPSERVERCLIENT t = MkEff t TCPServerClient

-- Send a string to the accepted client
tcpSend : String -> { [TCPSERVERCLIENT (ClientConnected)] ==> {result}
                      [TCPSERVERCLIENT (interpClientOperationRes result)] }
                    Eff (SocketOperationRes ByteLength)
tcpSend s = call (WriteString s)

-- Receive a string from the accepted client
tcpRecv : ByteLength -> { [TCPSERVERCLIENT (ClientConnected)] ==> {result}
                          [TCPSERVERCLIENT (interpClientOperationRes result)] }
                        Eff (SocketOperationRes (String, ByteLength))
tcpRecv bl = call (ReadString bl)

-- Close the connectoin
tcpClose : { [TCPSERVERCLIENT (ClientConnected)] ==> [TCPSERVERCLIENT ()] } Eff ()
tcpClose = call CloseClient

-- Finalise an erroneous connection
tcpFinalise : { [TCPSERVERCLIENT (ClientError)] ==> [TCPSERVERCLIENT ()] } Eff ()
tcpFinalise = call FinaliseClient

-- Write a PacketLang packet
tcpWritePacket : (pl : PacketLang) ->
                 (mkTy pl) ->
                 { [TCPSERVERCLIENT ClientConnected] ==> {result}
                   [TCPSERVERCLIENT (interpClientOperationRes result)] }
                 Eff (SocketOperationRes ByteLength)
tcpWritePacket pl dat = call (WritePacket pl dat)

-- Read a PacketLang packet
tcpReadPacket : (pl : PacketLang) ->
                Length -> -- TODO: Ideally we won't need this parameter
                { [TCPSERVERCLIENT ClientConnected] ==> {result}
                  [TCPSERVERCLIENT (interpClientOperationRes result)] }
                Eff (SocketOperationRes (Maybe (mkTy pl, ByteLength)))
tcpReadPacket pl len = call (ReadPacket pl len)

-- The type of client programs. Starts in ClientConnected, but must end unconnected.
ClientProgram : (effl: List EFFECT) -> Type -> Type
ClientProgram effl t = {TCPSERVERCLIENT (ClientConnected) :: effl ==>
                        TCPSERVERCLIENT () :: effl} Eff t

instance Handler TCPServerClient IO where
  handle (CC sock addr) (WriteString str) k = do
    send_res <- send sock str
    case send_res of
      Left err =>
        if (err == EAGAIN) then
          k (RecoverableError err) (CC sock addr)
        else
          k (FatalError err) (CE sock)
      Right bl => k (OperationSuccess bl) (CC sock addr)

  handle (CC sock addr) (ReadString bl) k = do
    recv_res <- recv sock bl
    case recv_res of
      Left err =>
        if err == EAGAIN then
          k (RecoverableError err) (CC sock addr)
        else if err == 0 then do -- Socket closed
          close sock
          k (ConnectionClosed) ()
        else k (FatalError err) (CE sock)
      Right (str, bl) => k (OperationSuccess (str, bl)) (CC sock addr)

  handle (CC sock addr) (CloseClient) k = do
    close sock *> k () ()
  handle (CE sock) (FinaliseClient) k =
    close sock *> k () ()

  handle (CC sock addr) (WritePacket pl dat) k = do
    (pckt, len) <- marshal pl dat
    send_res <- sendBuf sock pckt len
    case send_res of
         Left err =>
          if err == EAGAIN then
            k (RecoverableError err) (CC sock addr)
          else
            k (FatalError err) (CE sock)
         Right bl => k (OperationSuccess bl) (CC sock addr)

  handle (CC sock addr) (ReadPacket pl len) k = do
    ptr <- sock_alloc len
    recv_res <- recvBuf sock ptr len
    case recv_res of
         Left err =>
           if err == EAGAIN then
             k (RecoverableError err) (CC sock addr)
           else if err == 0 then do
             close sock
             k (ConnectionClosed) ()
           else
             k (FatalError err) (CE sock)
         Right bl => do
           res <- unmarshal pl ptr bl
           sock_free ptr
           -- The OperationSuccess depends on the actual network-y
           -- part, not the unmarshalling. If the unmarshalling fails,
           -- we still keep the connection open.
           k (OperationSuccess res) (CC sock addr)

data TCPServer : Effect where
  -- TCPServerBind a socket to a given address and port
  TCPServerBind : (Maybe SocketAddress) ->
                  Port ->
                  { () ==> {result} interpTCPServerBindRes result }
                   TCPServer (SocketOperationRes ())
  -- Listen
  Listen : { ServerBound ==> {result} interpListenRes result }
           TCPServer (SocketOperationRes ())
  -- Accept
  Accept :  ClientProgram effl t -> (Env IO effl) ->
            { ServerListening ==> {result} interpOperationRes result }
            TCPServer (SocketOperationRes t)
  ForkAccept : ClientProgram effl () -> (Env IO effl) ->
               { ServerListening ==> {result} interpOperationRes result }
               TCPServer (SocketOperationRes ())
  -- Need separate ones for each. It'd be nice to condense these into 1...
  CloseBound : { ServerBound ==> () } TCPServer ()
  CloseListening : { ServerListening ==> () } TCPServer ()
  Finalise : { ServerError ==> () } TCPServer ()

TCPSERVER : Type -> EFFECT
TCPSERVER t = MkEff t TCPServer

{- TCP Accessor Functions -}

-- Binds to a socket address, if given, and a port
bind : (Maybe SocketAddress) ->
       Port -> { [TCPSERVER ()] ==> {result}
                 [TCPSERVER (interpTCPServerBindRes result)] }
                Eff (SocketOperationRes ())
bind sa p = call (TCPServerBind sa p)

-- Listens on a bound socket
listen : { [TCPSERVER (ServerBound)] ==> {result}
           [TCPSERVER (interpListenRes result)] }
         Eff (SocketOperationRes ())
listen = call Listen

-- Accepts a new client, and runs the given client program
accept : (ClientProgram effl t) -> (Env IO effl) ->
       { [TCPSERVER (ServerListening)] ==> {result}
         [TCPSERVER (interpOperationRes result)]}
       Eff (SocketOperationRes t)
accept prog env = call (Accept prog env)

-- Accepts in a different thread
forkAccept : (ClientProgram effl ()) -> (Env IO effl) ->
         { [TCPSERVER (ServerListening)] ==> {result}
           [TCPSERVER (interpOperationRes result)]}
         Eff (SocketOperationRes ())
forkAccept prog env = call (ForkAccept prog env)

-- Close a bound server socket
closeBound : { [TCPSERVER (ServerBound)] ==> [TCPSERVER ()] } Eff ()
closeBound = call CloseBound

-- Close a listening server socket
closeListening : { [TCPSERVER (ServerListening)] ==> [TCPSERVER ()] } Eff ()
closeListening = call CloseListening

-- Finalise a server socket that has errored
finaliseServer : { [TCPSERVER (ServerError)] ==> [TCPSERVER ()] } Eff ()
finaliseServer = call Finalise

{- Handler Functions -}
instance Handler TCPServer IO where
  handle () (TCPServerBind sa p) k = do
    sock_res <- socket AF_INET Stream 0
    case sock_res of
      Left err => k (FatalError err) ()
      Right sock => do
        bind_res <- bind sock sa p
        if bind_res == 0 then
          -- Binding succeeded \o/
          k (OperationSuccess ()) (SB sock)
        else do
          close sock
          k (FatalError bind_res) ()

  handle (SB sock) (Listen) k = do
    listen_res <- listen sock
    if listen_res == 0 then
      -- Success
      k (OperationSuccess ()) (SL sock)
    else
      k (FatalError listen_res) (SE sock)

  handle (SL sock) (Accept prog env) k = do
    accept_res <- accept sock
    case accept_res of
         Left err => do
           if err == EAGAIN then
             k (RecoverableError err) (SL sock)
           else
             k (FatalError err) (SE sock)
         Right (client_sock, addr) => do
           res <- runInit ((CC client_sock addr) :: env) prog
           k (OperationSuccess res) (SL sock)

  handle (SL sock) (ForkAccept prog env) k = do
    accept_res <- accept sock
    case accept_res of
         Left err => do
           if err == EAGAIN then
             k (RecoverableError err) (SL sock)
           else
             k (FatalError err) (SE sock)
         Right (client_sock, addr) => do
           fork (runInit ((CC client_sock addr) :: env) prog *> return ())
           k (OperationSuccess ()) (SL sock)

  handle (SB sock) (CloseBound) k =
    close sock *> k () ()

  handle (SL sock) (CloseListening) k =
    close sock *> k () ()

  handle (SE sock) (Finalise) k =
    close sock *> k () ()


text:
-- Direct translation of AES specification
-- Kept as a reference

module Crypto.AES.Small

import Utils.ConstantTable
import Crypto.AES.Common
import Data.Bits
import Data.DPair
import Data.Fin
import Data.List
import Data.Nat
import Data.Stream
import Data.Vect
import Utils.Misc
import Utils.Bytes

gbox_9 : ConstantTable 256 Bits8
gbox_9 = from_vect
  [ 0x00, 0x09, 0x12, 0x1b, 0x24, 0x2d, 0x36, 0x3f, 0x48, 0x41, 0x5a, 0x53, 0x6c, 0x65, 0x7e, 0x77
  , 0x90, 0x99, 0x82, 0x8b, 0xb4, 0xbd, 0xa6, 0xaf, 0xd8, 0xd1, 0xca, 0xc3, 0xfc, 0xf5, 0xee, 0xe7
  , 0x3b, 0x32, 0x29, 0x20, 0x1f, 0x16, 0x0d, 0x04, 0x73, 0x7a, 0x61, 0x68, 0x57, 0x5e, 0x45, 0x4c
  , 0xab, 0xa2, 0xb9, 0xb0, 0x8f, 0x86, 0x9d, 0x94, 0xe3, 0xea, 0xf1, 0xf8, 0xc7, 0xce, 0xd5, 0xdc
  , 0x76, 0x7f, 0x64, 0x6d, 0x52, 0x5b, 0x40, 0x49, 0x3e, 0x37, 0x2c, 0x25, 0x1a, 0x13, 0x08, 0x01
  , 0xe6, 0xef, 0xf4, 0xfd, 0xc2, 0xcb, 0xd0, 0xd9, 0xae, 0xa7, 0xbc, 0xb5, 0x8a, 0x83, 0x98, 0x91
  , 0x4d, 0x44, 0x5f, 0x56, 0x69, 0x60, 0x7b, 0x72, 0x05, 0x0c, 0x17, 0x1e, 0x21, 0x28, 0x33, 0x3a
  , 0xdd, 0xd4, 0xcf, 0xc6, 0xf9, 0xf0, 0xeb, 0xe2, 0x95, 0x9c, 0x87, 0x8e, 0xb1, 0xb8, 0xa3, 0xaa
  , 0xec, 0xe5, 0xfe, 0xf7, 0xc8, 0xc1, 0xda, 0xd3, 0xa4, 0xad, 0xb6, 0xbf, 0x80, 0x89, 0x92, 0x9b
  , 0x7c, 0x75, 0x6e, 0x67, 0x58, 0x51, 0x4a, 0x43, 0x34, 0x3d, 0x26, 0x2f, 0x10, 0x19, 0x02, 0x0b
  , 0xd7, 0xde, 0xc5, 0xcc, 0xf3, 0xfa, 0xe1, 0xe8, 0x9f, 0x96, 0x8d, 0x84, 0xbb, 0xb2, 0xa9, 0xa0
  , 0x47, 0x4e, 0x55, 0x5c, 0x63, 0x6a, 0x71, 0x78, 0x0f, 0x06, 0x1d, 0x14, 0x2b, 0x22, 0x39, 0x30
  , 0x9a, 0x93, 0x88, 0x81, 0xbe, 0xb7, 0xac, 0xa5, 0xd2, 0xdb, 0xc0, 0xc9, 0xf6, 0xff, 0xe4, 0xed
  , 0x0a, 0x03, 0x18, 0x11, 0x2e, 0x27, 0x3c, 0x35, 0x42, 0x4b, 0x50, 0x59, 0x66, 0x6f, 0x74, 0x7d
  , 0xa1, 0xa8, 0xb3, 0xba, 0x85, 0x8c, 0x97, 0x9e, 0xe9, 0xe0, 0xfb, 0xf2, 0xcd, 0xc4, 0xdf, 0xd6
  , 0x31, 0x38, 0x23, 0x2a, 0x15, 0x1c, 0x07, 0x0e, 0x79, 0x70, 0x6b, 0x62, 0x5d, 0x54, 0x4f, 0x46
  ]

gbox_11 : ConstantTable 256 Bits8
gbox_11 = from_vect
  [ 0x00, 0x0b, 0x16, 0x1d, 0x2c, 0x27, 0x3a, 0x31, 0x58, 0x53, 0x4e, 0x45, 0x74, 0x7f, 0x62, 0x69
  , 0xb0, 0xbb, 0xa6, 0xad, 0x9c, 0x97, 0x8a, 0x81, 0xe8, 0xe3, 0xfe, 0xf5, 0xc4, 0xcf, 0xd2, 0xd9
  , 0x7b, 0x70, 0x6d, 0x66, 0x57, 0x5c, 0x41, 0x4a, 0x23, 0x28, 0x35, 0x3e, 0x0f, 0x04, 0x19, 0x12
  , 0xcb, 0xc0, 0xdd, 0xd6, 0xe7, 0xec, 0xf1, 0xfa, 0x93, 0x98, 0x85, 0x8e, 0xbf, 0xb4, 0xa9, 0xa2
  , 0xf6, 0xfd, 0xe0, 0xeb, 0xda, 0xd1, 0xcc, 0xc7, 0xae, 0xa5, 0xb8, 0xb3, 0x82, 0x89, 0x94, 0x9f
  , 0x46, 0x4d, 0x50, 0x5b, 0x6a, 0x61, 0x7c, 0x77, 0x1e, 0x15, 0x08, 0x03, 0x32, 0x39, 0x24, 0x2f
  , 0x8d, 0x86, 0x9b, 0x90, 0xa1, 0xaa, 0xb7, 0xbc, 0xd5, 0xde, 0xc3, 0xc8, 0xf9, 0xf2, 0xef, 0xe4
  , 0x3d, 0x36, 0x2b, 0x20, 0x11, 0x1a, 0x07, 0x0c, 0x65, 0x6e, 0x73, 0x78, 0x49, 0x42, 0x5f, 0x54
  , 0xf7, 0xfc, 0xe1, 0xea, 0xdb, 0xd0, 0xcd, 0xc6, 0xaf, 0xa4, 0xb9, 0xb2, 0x83, 0x88, 0x95, 0x9e
  , 0x47, 0x4c, 0x51, 0x5a, 0x6b, 0x60, 0x7d, 0x76, 0x1f, 0x14, 0x09, 0x02, 0x33, 0x38, 0x25, 0x2e
  , 0x8c, 0x87, 0x9a, 0x91, 0xa0, 0xab, 0xb6, 0xbd, 0xd4, 0xdf, 0xc2, 0xc9, 0xf8, 0xf3, 0xee, 0xe5
  , 0x3c, 0x37, 0x2a, 0x21, 0x10, 0x1b, 0x06, 0x0d, 0x64, 0x6f, 0x72, 0x79, 0x48, 0x43, 0x5e, 0x55
  , 0x01, 0x0a, 0x17, 0x1c, 0x2d, 0x26, 0x3b, 0x30, 0x59, 0x52, 0x4f, 0x44, 0x75, 0x7e, 0x63, 0x68
  , 0xb1, 0xba, 0xa7, 0xac, 0x9d, 0x96, 0x8b, 0x80, 0xe9, 0xe2, 0xff, 0xf4, 0xc5, 0xce, 0xd3, 0xd8
  , 0x7a, 0x71, 0x6c, 0x67, 0x56, 0x5d, 0x40, 0x4b, 0x22, 0x29, 0x34, 0x3f, 0x0e, 0x05, 0x18, 0x13
  , 0xca, 0xc1, 0xdc, 0xd7, 0xe6, 0xed, 0xf0, 0xfb, 0x92, 0x99, 0x84, 0x8f, 0xbe, 0xb5, 0xa8, 0xa3
  ]

gbox_13 : ConstantTable 256 Bits8
gbox_13 = from_vect
  [ 0x00, 0x0d, 0x1a, 0x17, 0x34, 0x39, 0x2e, 0x23, 0x68, 0x65, 0x72, 0x7f, 0x5c, 0x51, 0x46, 0x4b
  , 0xd0, 0xdd, 0xca, 0xc7, 0xe4, 0xe9, 0xfe, 0xf3, 0xb8, 0xb5, 0xa2, 0xaf, 0x8c, 0x81, 0x96, 0x9b
  , 0xbb, 0xb6, 0xa1, 0xac, 0x8f, 0x82, 0x95, 0x98, 0xd3, 0xde, 0xc9, 0xc4, 0xe7, 0xea, 0xfd, 0xf0
  , 0x6b, 0x66, 0x71, 0x7c, 0x5f, 0x52, 0x45, 0x48, 0x03, 0x0e, 0x19, 0x14, 0x37, 0x3a, 0x2d, 0x20
  , 0x6d, 0x60, 0x77, 0x7a, 0x59, 0x54, 0x43, 0x4e, 0x05, 0x08, 0x1f, 0x12, 0x31, 0x3c, 0x2b, 0x26
  , 0xbd, 0xb0, 0xa7, 0xaa, 0x89, 0x84, 0x93, 0x9e, 0xd5, 0xd8, 0xcf, 0xc2, 0xe1, 0xec, 0xfb, 0xf6
  , 0xd6, 0xdb, 0xcc, 0xc1, 0xe2, 0xef, 0xf8, 0xf5, 0xbe, 0xb3, 0xa4, 0xa9, 0x8a, 0x87, 0x90, 0x9d
  , 0x06, 0x0b, 0x1c, 0x11, 0x32, 0x3f, 0x28, 0x25, 0x6e, 0x63, 0x74, 0x79, 0x5a, 0x57, 0x40, 0x4d
  , 0xda, 0xd7, 0xc0, 0xcd, 0xee, 0xe3, 0xf4, 0xf9, 0xb2, 0xbf, 0xa8, 0xa5, 0x86, 0x8b, 0x9c, 0x91
  , 0x0a, 0x07, 0x10, 0x1d, 0x3e, 0x33, 0x24, 0x29, 0x62, 0x6f, 0x78, 0x75, 0x56, 0x5b, 0x4c, 0x41
  , 0x61, 0x6c, 0x7b, 0x76, 0x55, 0x58, 0x4f, 0x42, 0x09, 0x04, 0x13, 0x1e, 0x3d, 0x30, 0x27, 0x2a
  , 0xb1, 0xbc, 0xab, 0xa6, 0x85, 0x88, 0x9f, 0x92, 0xd9, 0xd4, 0xc3, 0xce, 0xed, 0xe0, 0xf7, 0xfa
  , 0xb7, 0xba, 0xad, 0xa0, 0x83, 0x8e, 0x99, 0x94, 0xdf, 0xd2, 0xc5, 0xc8, 0xeb, 0xe6, 0xf1, 0xfc
  , 0x67, 0x6a, 0x7d, 0x70, 0x53, 0x5e, 0x49, 0x44, 0x0f, 0x02, 0x15, 0x18, 0x3b, 0x36, 0x21, 0x2c
  , 0x0c, 0x01, 0x16, 0x1b, 0x38, 0x35, 0x22, 0x2f, 0x64, 0x69, 0x7e, 0x73, 0x50, 0x5d, 0x4a, 0x47
  , 0xdc, 0xd1, 0xc6, 0xcb, 0xe8, 0xe5, 0xf2, 0xff, 0xb4, 0xb9, 0xae, 0xa3, 0x80, 0x8d, 0x9a, 0x97
  ]

gbox_14 : ConstantTable 256 Bits8
gbox_14 = from_vect
  [ 0x00, 0x0e, 0x1c, 0x12, 0x38, 0x36, 0x24, 0x2a, 0x70, 0x7e, 0x6c, 0x62, 0x48, 0x46, 0x54, 0x5a
  , 0xe0, 0xee, 0xfc, 0xf2, 0xd8, 0xd6, 0xc4, 0xca, 0x90, 0x9e, 0x8c, 0x82, 0xa8, 0xa6, 0xb4, 0xba
  , 0xdb, 0xd5, 0xc7, 0xc9, 0xe3, 0xed, 0xff, 0xf1, 0xab, 0xa5, 0xb7, 0xb9, 0x93, 0x9d, 0x8f, 0x81
  , 0x3b, 0x35, 0x27, 0x29, 0x03, 0x0d, 0x1f, 0x11, 0x4b, 0x45, 0x57, 0x59, 0x73, 0x7d, 0x6f, 0x61
  , 0xad, 0xa3, 0xb1, 0xbf, 0x95, 0x9b, 0x89, 0x87, 0xdd, 0xd3, 0xc1, 0xcf, 0xe5, 0xeb, 0xf9, 0xf7
  , 0x4d, 0x43, 0x51, 0x5f, 0x75, 0x7b, 0x69, 0x67, 0x3d, 0x33, 0x21, 0x2f, 0x05, 0x0b, 0x19, 0x17
  , 0x76, 0x78, 0x6a, 0x64, 0x4e, 0x40, 0x52, 0x5c, 0x06, 0x08, 0x1a, 0x14, 0x3e, 0x30, 0x22, 0x2c
  , 0x96, 0x98, 0x8a, 0x84, 0xae, 0xa0, 0xb2, 0xbc, 0xe6, 0xe8, 0xfa, 0xf4, 0xde, 0xd0, 0xc2, 0xcc
  , 0x41, 0x4f, 0x5d, 0x53, 0x79, 0x77, 0x65, 0x6b, 0x31, 0x3f, 0x2d, 0x23, 0x09, 0x07, 0x15, 0x1b
  , 0xa1, 0xaf, 0xbd, 0xb3, 0x99, 0x97, 0x85, 0x8b, 0xd1, 0xdf, 0xcd, 0xc3, 0xe9, 0xe7, 0xf5, 0xfb
  , 0x9a, 0x94, 0x86, 0x88, 0xa2, 0xac, 0xbe, 0xb0, 0xea, 0xe4, 0xf6, 0xf8, 0xd2, 0xdc, 0xce, 0xc0
  , 0x7a, 0x74, 0x66, 0x68, 0x42, 0x4c, 0x5e, 0x50, 0x0a, 0x04, 0x16, 0x18, 0x32, 0x3c, 0x2e, 0x20
  , 0xec, 0xe2, 0xf0, 0xfe, 0xd4, 0xda, 0xc8, 0xc6, 0x9c, 0x92, 0x80, 0x8e, 0xa4, 0xaa, 0xb8, 0xb6
  , 0x0c, 0x02, 0x10, 0x1e, 0x34, 0x3a, 0x28, 0x26, 0x7c, 0x72, 0x60, 0x6e, 0x44, 0x4a, 0x58, 0x56
  , 0x37, 0x39, 0x2b, 0x25, 0x0f, 0x01, 0x13, 0x1d, 0x47, 0x49, 0x5b, 0x55, 0x7f, 0x71, 0x63, 0x6d
  , 0xd7, 0xd9, 0xcb, 0xc5, 0xef, 0xe1, 0xf3, 0xfd, 0xa7, 0xa9, 0xbb, 0xb5, 0x9f, 0x91, 0x83, 0x8d
  ]

data G : Type where
  G1 : G
  G2 : G
  G3 : G

data G' : Type where
  G9 : G'
  G11 : G'
  G13 : G'
  G14 : G'

mix_columns_mat : Vect 4 (Vect 4 G)
mix_columns_mat = [[G2, G1, G1, G3], [G3, G2, G1, G1], [G1, G3, G2, G1], [G1, G1, G3, G2]]

inv_mix_columns_mat : Vect 4 (Vect 4 G')
inv_mix_columns_mat = [[G14, G9, G13, G11], [G11, G14, G9, G13], [G13, G11, G14, G9], [G9, G13, G11, G14]]

gmod : Bits8 -> G -> Bits8
gmod x G1 = x
gmod x G2 = (if x < 128 then id else (xor 0x1b)) $ shiftL x 1
gmod x G3 = xor (gmod x G2) x

inv_gmod : Bits8 -> G' -> Bits8
inv_gmod x g =
  index_bits8 x $ case g of
    G9 => gbox_9
    G11 => gbox_11
    G13 => gbox_13
    G14 => gbox_14

mix_columns : Vect n (Vect 4 Bits8) -> Vect n (Vect 4 Bits8)
mix_columns xs = matmul (\a, b => foldl xor 0 $ zipWith gmod a b) xs mix_columns_mat

inv_mix_columns : Vect n (Vect 4 Bits8) -> Vect n (Vect 4 Bits8)
inv_mix_columns xs = matmul (\a, b => foldl xor 0 $ zipWith inv_gmod a b) xs inv_mix_columns_mat

mk_round_keys : {n_k, n_b : _} -> {auto 0 ok : NonZero n_b} -> {auto 0 ok2 : NonZero n_k} -> (n_main_rounds : Nat) -> (key : Vect n_k (Vect n_b Bits8)) -> (Vect 4 (Vect n_b Bits8), Vect n_main_rounds (Vect 4 (Vect n_b Bits8)), Vect 4 (Vect n_b Bits8))
mk_round_keys n_main_rounds k =
  let
    (rk_init :: rks) = Stream.take (S (S n_main_rounds)) $ chunk _ $ prepend (toList k) $ expand_key k
  in
    (rk_init, unsnoc rks)

shift_rows' : {m : _} -> Nat -> Vect n (Vect (S m) Bits8) -> Vect n (Vect (S m) Bits8)
shift_rows' n [] = []
shift_rows' n (x :: xs) = rot_word n x :: shift_rows' (S n) xs

shift_rows : {n, m : Nat} -> Vect (S n) (Vect m Bits8) -> Vect (S n) (Vect m Bits8)
shift_rows = transpose . shift_rows' Z . transpose

inv_shift_rows' : {m : _} -> Nat -> Vect n (Vect (S m) Bits8) -> Vect n (Vect (S m) Bits8)
inv_shift_rows' n [] = []
inv_shift_rows' n (x :: xs) = inv_rot_word n x :: inv_shift_rows' (S n) xs

inv_shift_rows : {n, m : Nat} -> Vect (S n) (Vect m Bits8) -> Vect (S n) (Vect m Bits8)
inv_shift_rows = transpose . inv_shift_rows' Z . transpose

encrypt_block' : {n_k : _} -> {auto 0 ok : NonZero n_k} -> (n_main_rounds : Nat) -> (key : Vect n_k (Vect 4 Bits8)) -> (state : Vect 4 (Vect 4 Bits8)) -> Vect 4 (Vect 4 Bits8)
encrypt_block' n_main_rounds k x =
  let
    (init_rk, main_rks, final_rk) = mk_round_keys n_main_rounds k
    -- initial round
    x = matxor x init_rk
    -- main rounds
    x = foldl (flip $ \rk => matxor rk . mix_columns . shift_rows . sub_bytes) x main_rks
    -- final round
    x = matxor final_rk $ shift_rows $ sub_bytes x
  in
    x

export
encrypt_block : (mode : Mode) -> (key : Vect ((get_n_k mode) * 4) Bits8) -> (state : Vect 16 Bits8) -> Vect 16 Bits8
encrypt_block mode k s = concat $ encrypt_block' {ok = n_k_never_Z mode} (get_main_rounds mode) (group _ _ k) (group _ _ s)

decrypt_block' : {n_k : _} -> {auto 0 ok : NonZero n_k} -> (n_main_rounds : Nat) -> (key : Vect n_k (Vect 4 Bits8)) -> (state : Vect 4 (Vect 4 Bits8)) -> Vect 4 (Vect 4 Bits8)
decrypt_block' n_main_rounds k x =
  let
    (init_rk, main_rks, final_rk) = mk_round_keys n_main_rounds k
    -- initial round
    x = matxor x init_rk
    -- main rounds
    x = foldl (flip $ \rk => inv_mix_columns . matxor rk . inv_sub_bytes . inv_shift_rows) x main_rks
    -- final round
    x = matxor final_rk $ inv_sub_bytes $ inv_shift_rows x
  in
    x

export
decrypt_block : (mode : Mode) -> (key : Vect ((get_n_k mode) * 4) Bits8) -> (state : Vect 16 Bits8) -> Vect 16 Bits8
decrypt_block mode k x = concat $ decrypt_block' {ok = n_k_never_Z mode} (get_main_rounds mode) (group _ _ k) (group _ _ x)


text:
module IdrisJvm.Core.Common

import Data.SortedMap
import IdrisJvm.Core.Asm
import IdrisJvm.IR.Types
import IdrisJvm.IO
import Java.Lang

%access public export

jtrace : Show a => a -> b -> b
jtrace x val = unsafePerformIO {ffi=FFI_JVM} (do printLn x; pure val)

jerror : String -> a
jerror msg = believe_me . unsafePerformIO $ invokeStatic RuntimeClass "error" (Object -> JVM_IO Object) (believe_me msg)

sep : String -> List String -> String
sep x xs = cast $ intercalate (cast x) $ map cast xs

IdrisToJavaNameConverterClass : JVM_NativeTy
IdrisToJavaNameConverterClass = Class "IdrisJvm/Core/IdrisToJavaNameConverter"

jname : String -> JMethodName
jname s =
  let [cname, mname] = split (== ',') . unsafePerformIO $ invokeStatic IdrisToJavaNameConverterClass "idrisClassMethodName" (String -> JVM_IO String) s
  in MkJMethodName cname mname

locIndex : LVar -> Int
locIndex (Loc i) = i
locIndex _       = jerror "Unexpected global variable"

classSig : String -> String
classSig className = "L" ++ className ++ ";"

rtFuncSig : String
rtFuncSig = classSig $ rtClass "Function"

rtThunkSig : String
rtThunkSig = classSig thunkClass

utilClass : String
utilClass = rtClass "Util"

intRange : Int -> Int -> List Int
intRange from to = if from < to then [from .. to] else []

boxDouble : Asm ()
boxDouble = InvokeMethod InvokeStatic "java/lang/Double" "valueOf" "(D)Ljava/lang/Double;" False

boxFloat : Asm ()
boxFloat = InvokeMethod InvokeStatic "java/lang/Float" "valueOf" "(F)Ljava/lang/Float;" False

boxBool : Asm ()
boxBool = InvokeMethod InvokeStatic "java/lang/Boolean" "valueOf" "(Z)Ljava/lang/Boolean;" False

boxByte : Asm ()
boxByte = InvokeMethod InvokeStatic "java/lang/Byte" "valueOf" "(B)Ljava/lang/Byte;" False

boxChar : Asm ()
boxChar = InvokeMethod InvokeStatic "java/lang/Character" "valueOf" "(C)Ljava/lang/Character;" False

boxInt : Asm ()
boxInt = InvokeMethod InvokeStatic "java/lang/Integer" "valueOf" "(I)Ljava/lang/Integer;" False

boxShort : Asm ()
boxShort = InvokeMethod InvokeStatic "java/lang/Short" "valueOf" "(S)Ljava/lang/Short;" False

boxLong : Asm ()
boxLong = InvokeMethod InvokeStatic "java/lang/Long" "valueOf" "(J)Ljava/lang/Long;" False

unboxBool : Asm ()
unboxBool = InvokeMethod InvokeVirtual "java/lang/Boolean" "booleanValue" "()Z" False

unboxByte : Asm ()
unboxByte = InvokeMethod InvokeVirtual "java/lang/Byte" "byteValue" "()B" False

unboxInt : Asm ()
unboxInt = InvokeMethod InvokeVirtual "java/lang/Integer" "intValue" "()I" False

unboxChar : Asm ()
unboxChar = InvokeMethod InvokeVirtual "java/lang/Character" "charValue" "()C" False

unboxShort : Asm ()
unboxShort = InvokeMethod InvokeVirtual "java/lang/Short" "shortValue" "()S" False

unboxLong : Asm ()
unboxLong = InvokeMethod InvokeVirtual "java/lang/Long" "longValue" "()J" False

unboxDouble : Asm ()
unboxDouble = InvokeMethod InvokeVirtual "java/lang/Double" "doubleValue" "()D" False

unboxFloat : Asm ()
unboxFloat = InvokeMethod InvokeVirtual "java/lang/Float" "floatValue" "()F" False

repeatString : Nat -> String -> String
repeatString n s = concat (replicate n s)

repeatObjectDesc : Nat -> String
repeatObjectDesc n = repeatString n "Ljava/lang/Object;"

sig : Nat -> String
sig nArgs = "(" ++ repeatObjectDesc nArgs ++  ")Ljava/lang/Object;"

metafactoryDesc : Descriptor
metafactoryDesc =
  concat [ "("
         , "Ljava/lang/invoke/MethodHandles$Lookup;"
         , "Ljava/lang/String;Ljava/lang/invoke/MethodType;"
         , "Ljava/lang/invoke/MethodType;"
         , "Ljava/lang/invoke/MethodHandle;"
         , "Ljava/lang/invoke/MethodType;"
         , ")"
         , "Ljava/lang/invoke/CallSite;"
         ]

unrolledConstructorPropsCount : Nat
unrolledConstructorPropsCount = 10

inferredTypeToFieldTypeDesc : InferredType -> FieldTypeDescriptor
inferredTypeToFieldTypeDesc IBool = FieldTyDescBoolean
inferredTypeToFieldTypeDesc IByte = FieldTyDescByte
inferredTypeToFieldTypeDesc IChar = FieldTyDescChar
inferredTypeToFieldTypeDesc IShort = FieldTyDescShort
inferredTypeToFieldTypeDesc IInt = FieldTyDescInt
inferredTypeToFieldTypeDesc ILong = FieldTyDescLong
inferredTypeToFieldTypeDesc IFloat = FieldTyDescFloat
inferredTypeToFieldTypeDesc IDouble = FieldTyDescDouble
inferredTypeToFieldTypeDesc (Ref refTy) = FieldTyDescReference (ClassDesc refTy)
inferredTypeToFieldTypeDesc IUnknown = FieldTyDescReference (ClassDesc "java/lang/Object")
inferredTypeToFieldTypeDesc (IArray elemTy) = FieldTyDescReference (ArrayDesc $ inferredTypeToFieldTypeDesc elemTy)

getInferredTyDesc : InferredType -> String
getInferredTyDesc = asmFieldTypeDesc . inferredTypeToFieldTypeDesc

toFrameLocalVarType : InferredType -> String
toFrameLocalVarType IBool = "INTEGER"
toFrameLocalVarType IByte = "INTEGER"
toFrameLocalVarType IChar = "INTEGER"
toFrameLocalVarType IShort = "INTEGER"
toFrameLocalVarType IInt = "INTEGER"
toFrameLocalVarType ILong = "LONG"
toFrameLocalVarType IFloat = "FLOAT"
toFrameLocalVarType IDouble = "DOUBLE"
toFrameLocalVarType (Ref clsName) = clsName
toFrameLocalVarType (IArray elemTy) = "[" ++ getInferredTyDesc elemTy
toFrameLocalVarType _ = "java/lang/Object"

toFrameLocalVarTypes : InferredTypeStore -> List String
toFrameLocalVarTypes types = toFrameLocalVarType <$> (values types)

fullFrame : Asm ()
fullFrame = do
  nlocalVars <- GetLocalVarCount
  locTypes <- GetFunctionLocTypes
  let frameLocTypes = toFrameLocalVarTypes locTypes
  Frame FFull nlocalVars frameLocTypes 0 []

addFrame : Asm ()
addFrame = do
  needFrame <- ShouldDescribeFrame
  if needFrame
    then do
      fullFrame
      UpdateShouldDescribeFrame False
    else Frame FSame 0 [] 0 []

defaultConstructor : ClassName -> ClassName -> Asm ()
defaultConstructor cname parent = do
  CreateMethod [Public] cname "<init>" "()V" Nothing Nothing [] []
  MethodCodeStart
  Aload 0
  InvokeMethod InvokeSpecial parent "<init>" "()V" False
  Return
  MaxStackAndLocal (-1) (-1) -- Let the asm calculate
  MethodCodeEnd

invokeError : String -> Asm ()
invokeError x = do
  Ldc $ StringConst x
  InvokeMethod InvokeStatic (rtClass "Runtime") "error" "(Ljava/lang/Object;)Ljava/lang/Object;" False

getPrimitiveClass : String -> Asm ()
getPrimitiveClass clazz = Field FGetStatic clazz "TYPE" "Ljava/lang/Class;"

getInferredFunDesc : List InferredType -> InferredType -> String
getInferredFunDesc [] retTy = "()" ++ getInferredTyDesc retTy
getInferredFunDesc argTypes retTy =
    let argDescs = getInferredTyDesc <$> argTypes
        retTyDesc = getInferredTyDesc retTy
    in "(" ++ (the String $ concat argDescs) ++ ")" ++ retTyDesc

box : InferredType -> Asm ()
box IBool   = boxInt
box IByte   = boxByte
box IChar   = boxChar
box IShort  = boxShort
box IInt    = boxInt
box ILong   = boxLong
box IFloat  = boxFloat
box IDouble = boxDouble
box _       = pure ()

getVarIndex : InferredTypeStore -> LVar -> Int
getVarIndex types (Loc index) = go 0 0 where
  go : Int -> Int -> Int
  go pos currVarIndex =
    if currVarIndex == index then
        pos
    else
        let currVarTy = getLocTy types (Loc currVarIndex)
            isTwoWordTy = currVarTy == IDouble || currVarTy == ILong
            nextPos = if isTwoWordTy then pos + 2 else succ pos
        in go nextPos (succ currVarIndex)

opWithWordSize : InferredTypeStore -> (Int -> Asm ()) -> LVar -> Asm ()
opWithWordSize types op var = do
    let newPos = getVarIndex types var
    op newPos

boolObjToBool : Asm ()
boolObjToBool = InvokeMethod InvokeStatic utilClass "toBoolean" "(Ljava/lang/Object;)Z" False

boolToInt : Asm ()
boolToInt = InvokeMethod InvokeStatic utilClass "boolToInt" "(Z)I" False

objToInt : Asm ()
objToInt = InvokeMethod InvokeStatic utilClass "toInt" "(Ljava/lang/Object;)I" False

objToByte : Asm ()
objToByte = InvokeMethod InvokeStatic utilClass "toByte" "(Ljava/lang/Object;)B" False

charObjToChar : Asm ()
charObjToChar = do Checkcast "java/lang/Character"; unboxChar

objToShort : Asm ()
objToShort = InvokeMethod InvokeStatic utilClass "toShort" "(Ljava/lang/Object;)S" False

longObjToLong : Asm ()
longObjToLong = do Checkcast "java/lang/Long"; unboxLong

objToFloat : Asm ()
objToFloat = InvokeMethod InvokeStatic utilClass "toFloat" "(Ljava/lang/Object;)F" False

objToDouble : Asm ()
objToDouble = InvokeMethod InvokeStatic utilClass "toDouble" "(Ljava/lang/Object;)D" False

checkcast : String -> Asm ()
checkcast "java/lang/Object" = pure ()
checkcast cname              = Checkcast cname

cgCast : InferredType -> InferredType -> Asm ()
cgCast IUnknown IBool = boolObjToBool
cgCast (Ref _) IBool = boolObjToBool

cgCast IUnknown IByte = objToByte
cgCast (Ref _) IByte = objToByte

cgCast IUnknown IChar = charObjToChar
cgCast (Ref _) IChar = charObjToChar

cgCast IUnknown IShort = objToShort
cgCast (Ref _) IShort = objToShort

cgCast IUnknown IInt = objToInt
cgCast (Ref _) IInt = objToInt

cgCast IUnknown ILong = longObjToLong
cgCast (Ref _) ILong = longObjToLong

cgCast IUnknown IFloat = objToFloat
cgCast (Ref _) IFloat = objToFloat

cgCast IUnknown IDouble = objToDouble
cgCast (Ref _) IDouble = objToDouble

cgCast IBool (Ref _) = boxBool
cgCast IBool IUnknown = boxBool

cgCast IByte (Ref _) = boxByte
cgCast IByte IUnknown = boxByte

cgCast IChar (Ref _) = boxChar
cgCast IChar IUnknown = boxChar

cgCast IShort (Ref _) = boxShort
cgCast IShort IUnknown = boxShort

cgCast IInt (Ref _) = boxInt
cgCast IInt IUnknown = boxInt

cgCast ILong (Ref _) = boxLong
cgCast ILong IUnknown = boxLong

cgCast IFloat (Ref _) = boxFloat
cgCast IFloat IUnknown = boxFloat

cgCast IDouble (Ref _) = boxDouble
cgCast IDouble IUnknown = boxDouble

cgCast IInt IByte = I2b
cgCast IInt IShort = I2s
cgCast IFloat IDouble = F2d
cgCast IDouble IFloat = D2f

cgCast IBool IInt = boolToInt

cgCast (Ref _) arr@(IArray _) = Checkcast $ getInferredTyDesc arr
cgCast IUnknown arr@(IArray _) = Checkcast $ getInferredTyDesc arr

cgCast IUnknown (Ref ty) = checkcast ty

cgCast (Ref ty1) (Ref ty2) = when (ty1 /= ty2) $ checkcast ty2

cgCast _ _ = pure ()

loadAndBox : (Int -> Asm ()) -> Asm () -> InferredTypeStore -> LVar -> Asm ()
loadAndBox loadOp boxOp sourceLocTys var = let op = \index => do loadOp index; boxOp
                                           in opWithWordSize sourceLocTys op var

loadAndBoxBool : InferredTypeStore -> LVar -> Asm ()
loadAndBoxBool = loadAndBox Iload boxBool

loadAndBoxByte : InferredTypeStore -> LVar -> Asm ()
loadAndBoxByte = loadAndBox Iload boxByte

loadAndBoxChar : InferredTypeStore -> LVar -> Asm ()
loadAndBoxChar = loadAndBox Iload boxChar

loadAndBoxShort : InferredTypeStore -> LVar -> Asm ()
loadAndBoxShort = loadAndBox Iload boxShort

loadAndBoxInt : InferredTypeStore -> LVar -> Asm ()
loadAndBoxInt = loadAndBox Iload boxInt

loadAndBoxLong : InferredTypeStore -> LVar -> Asm ()
loadAndBoxLong = loadAndBox Lload boxLong

loadAndBoxFloat : InferredTypeStore -> LVar -> Asm ()
loadAndBoxFloat = loadAndBox Fload boxFloat

loadAndBoxDouble : InferredTypeStore -> LVar -> Asm ()
loadAndBoxDouble = loadAndBox Dload boxDouble

loadVar : InferredTypeStore -> (srcTy: InferredType) -> (targetTy: InferredType) -> LVar -> Asm ()
loadVar sourceLocTys IBool IBool var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IByte IByte var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IChar IChar var  = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IShort IShort var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IByte IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IChar IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IShort IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IInt IInt  var = opWithWordSize sourceLocTys Iload var
loadVar sourceLocTys IInt IByte  var = opWithWordSize sourceLocTys (\var => do Iload var; I2b) var
loadVar sourceLocTys IInt IShort  var = opWithWordSize sourceLocTys (\var => do Iload var; I2s) var
loadVar sourceLocTys ILong ILong  var = opWithWordSize sourceLocTys Lload var
loadVar sourceLocTys IFloat IFloat var = opWithWordSize sourceLocTys Fload var
loadVar sourceLocTys IFloat IDouble var = opWithWordSize sourceLocTys (\var => do Fload var; F2d) var
loadVar sourceLocTys IDouble IDouble var = opWithWordSize sourceLocTys Dload var
loadVar sourceLocTys IDouble IFloat var = opWithWordSize sourceLocTys (\var => do Dload var; D2f)  var

loadVar sourceLocTys IBool IUnknown  var = loadAndBoxBool sourceLocTys var
loadVar sourceLocTys IBool (Ref _) var = loadAndBoxBool sourceLocTys var

loadVar sourceLocTys IByte IUnknown  var = loadAndBoxByte sourceLocTys var
loadVar sourceLocTys IByte (Ref _) var = loadAndBoxByte sourceLocTys var

loadVar sourceLocTys IChar IUnknown var = loadAndBoxChar sourceLocTys var
loadVar sourceLocTys IChar (Ref _) var = loadAndBoxChar sourceLocTys var

loadVar sourceLocTys IShort IUnknown var  = loadAndBoxShort sourceLocTys var
loadVar sourceLocTys IShort (Ref _) var = loadAndBoxShort sourceLocTys var

loadVar sourceLocTys IInt IUnknown var  = loadAndBoxInt sourceLocTys var
loadVar sourceLocTys IInt (Ref _) var = loadAndBoxInt sourceLocTys var

loadVar sourceLocTys ILong IUnknown var = loadAndBoxLong sourceLocTys var
loadVar sourceLocTys ILong (Ref _) var = loadAndBoxLong sourceLocTys var

loadVar sourceLocTys IFloat IUnknown var = loadAndBoxFloat sourceLocTys var
loadVar sourceLocTys IFloat (Ref _) var = loadAndBoxFloat sourceLocTys var

loadVar sourceLocTys IDouble IUnknown var = loadAndBoxDouble sourceLocTys var
loadVar sourceLocTys IDouble (Ref _) var = loadAndBoxDouble sourceLocTys var

loadVar sourceLocTys IUnknown IBool var =
    let loadInstr = \index => do Aload index; boolObjToBool
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IBool var =
    let loadInstr = \index => do Aload index; boolObjToBool
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IByte var =
    let loadInstr = \index => do Aload index; objToByte
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IByte var =
    let loadInstr = \index => do Aload index; objToByte
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IChar var =
    let loadInstr = \index => do Aload index; charObjToChar
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IChar var =
    let loadInstr = \index => do Aload index; charObjToChar
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IShort var =
    let loadInstr = \index => do Aload index; objToShort
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IShort var =
    let loadInstr = \index => do Aload index; objToShort
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IInt var =
    let loadInstr = \index => do Aload index; objToInt
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IBool IInt var =
    let loadInstr = \index => do Iload index; boolToInt
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys (Ref _) IInt var =
    let loadInstr = \index => do Aload index; objToInt
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown ILong var =
    let loadInstr = \index => do Aload index; longObjToLong
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) ILong var =
    let loadInstr = \index => do Aload index; longObjToLong
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IFloat var =
    let loadInstr = \index => do Aload index; objToFloat
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IFloat var =
    let loadInstr = \index => do Aload index; objToFloat
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown IDouble var =
    let loadInstr = \index => do Aload index; objToDouble
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) IDouble var =
    let loadInstr = \index => do Aload index; objToDouble
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown arr@(IArray _) var =
    let loadInstr = \index => do Aload index; Checkcast $ getInferredTyDesc arr
    in opWithWordSize sourceLocTys loadInstr var
loadVar sourceLocTys (Ref _) arr@(IArray _) var =
    let loadInstr = \index => do Aload index; Checkcast $ getInferredTyDesc arr
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys IUnknown (Ref ty2) var =
    let loadInstr = \index => do Aload index; checkcast ty2
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys (Ref ty1) (Ref ty2) var =
    let loadInstr = \index => do Aload index; when (ty1 /= ty2) $ checkcast ty2
    in opWithWordSize sourceLocTys loadInstr var

loadVar sourceLocTys _ _ var = opWithWordSize sourceLocTys Aload var

loadVars : InferredTypeStore -> InferredTypeStore -> List LVar -> Asm ()
loadVars _ _ []  = pure ()
loadVars sourceLocTys targetLocTys vars  = do
    let nVars = the Int $ cast $ length vars
    let targetVarTys = if nVars > 0 then getLocTy targetLocTys <$> (Loc <$> [0 .. pred nVars]) else []
    let sourceVarTys = getLocTy sourceLocTys <$> vars
    let varsWithSourceTargetTys = List.zip vars $ List.zip sourceVarTys targetVarTys
    go varsWithSourceTargetTys
  where
    go : List (LVar, InferredType, InferredType) -> Asm ()
    go [] = pure ()
    go ((var, srcTy, targetTy) :: vs) = do
      loadVar sourceLocTys srcTy targetTy var
      go vs

storeVarWithWordSize : (Int -> Asm ()) -> LVar -> Asm ()
storeVarWithWordSize storeOp var = do
    types <- GetFunctionLocTypes
    opWithWordSize types storeOp var

boxStore : Asm () -> LVar -> Asm ()
boxStore boxOp var = storeVarWithWordSize (\index => do boxOp; Astore index) var

storeVar : (srcTy: InferredType) -> (targetTy: InferredType) -> LVar -> Asm ()
storeVar IBool IBool     var = do types <- GetFunctionLocTypes; opWithWordSize types Istore var
storeVar IByte IByte     var = do types <- GetFunctionLocTypes; opWithWordSize types Istore var
storeVar IChar IChar     var = do types <- GetFunctionLocTypes; opWithWordSize types Istore var
storeVar IShort IShort   var = do types <- GetFunctionLocTypes; opWithWordSize types Istore var
storeVar IInt IInt       var = do types <- GetFunctionLocTypes; opWithWordSize types Istore var
storeVar ILong ILong     var = do types <- GetFunctionLocTypes; opWithWordSize types Lstore var
storeVar IFloat IFloat   var = do types <- GetFunctionLocTypes; opWithWordSize types Fstore var
storeVar IDouble IDouble var = do types <- GetFunctionLocTypes; opWithWordSize types Dstore var

storeVar IBool IUnknown var = boxStore boxBool var
storeVar IBool (Ref _) var = boxStore boxBool var

storeVar IByte IUnknown var = boxStore boxByte var
storeVar IByte (Ref _) var = boxStore boxByte var

storeVar IChar IUnknown var = boxStore boxChar var
storeVar IChar (Ref _) var = boxStore boxChar var

storeVar IShort IUnknown var = boxStore boxShort var
storeVar IShort (Ref _) var = boxStore boxShort var

storeVar IInt IUnknown var = boxStore boxInt var
storeVar IInt (Ref _) var = boxStore boxInt var

storeVar ILong IUnknown var = boxStore boxLong var
storeVar ILong (Ref _) var = boxStore boxLong var

storeVar IFloat IUnknown var = boxStore boxFloat var
storeVar IFloat (Ref _) var = boxStore boxFloat var

storeVar IDouble IUnknown var = boxStore boxDouble var
storeVar IDouble (Ref _) var = boxStore boxDouble var

storeVar IUnknown IBool var = storeVarWithWordSize (\index => do cgCast IUnknown IBool; Istore index) var
storeVar srcTy@(Ref _) IBool var = storeVarWithWordSize (\index => do cgCast srcTy IBool; Istore index) var

storeVar IUnknown IByte var = storeVarWithWordSize (\index => do cgCast IUnknown IByte; Istore index) var
storeVar srcTy@(Ref _) IByte var = storeVarWithWordSize (\index => do cgCast srcTy IByte; Istore index) var

storeVar IUnknown IChar var = storeVarWithWordSize (\index => do cgCast IUnknown IChar; Istore index) var
storeVar srcTy@(Ref _) IChar var = storeVarWithWordSize (\index => do cgCast srcTy IChar; Istore index) var

storeVar IUnknown IShort var = storeVarWithWordSize (\index => do cgCast IUnknown IShort; Istore index) var
storeVar srcTy@(Ref _) IShort var = storeVarWithWordSize (\index => do cgCast srcTy IShort; Istore index) var

storeVar IUnknown IInt var = storeVarWithWordSize (\index => do cgCast IUnknown IInt; Istore index) var
storeVar srcTy@(Ref _) IInt var = storeVarWithWordSize (\index => do cgCast srcTy IInt; Istore index) var

storeVar IUnknown ILong var = storeVarWithWordSize (\index => do cgCast IUnknown ILong; Lstore index) var
storeVar srcTy@(Ref _) ILong var = storeVarWithWordSize (\index => do cgCast srcTy ILong; Lstore index) var

storeVar IUnknown IFloat var = storeVarWithWordSize (\index => do cgCast IUnknown IFloat; Fstore index) var
storeVar srcTy@(Ref _) IFloat var = storeVarWithWordSize (\index => do cgCast srcTy IFloat; Fstore index) var

storeVar IUnknown IDouble var = storeVarWithWordSize (\index => do cgCast IUnknown IDouble; Dstore index) var
storeVar srcTy@(Ref _) IDouble var = storeVarWithWordSize (\index => do cgCast srcTy IDouble; Dstore index) var

storeVar IUnknown arr@(IArray elemTy) var =
    storeVarWithWordSize (\index => do Checkcast $ getInferredTyDesc arr; Astore index) var
storeVar (Ref _) arr@(IArray elemTy) var =
    storeVarWithWordSize (\index => do Checkcast $ getInferredTyDesc arr; Astore index) var

storeVar IUnknown targetTy@(Ref _) var = do
    types <- GetFunctionLocTypes
    cgCast IUnknown targetTy
    opWithWordSize types Astore var

storeVar srcTy@(Ref _) targetTy@(Ref _) var = do
    types <- GetFunctionLocTypes
    cgCast srcTy targetTy
    opWithWordSize types Astore var

storeVar _ _ var = do types <- GetFunctionLocTypes; opWithWordSize types Astore var

idrisObjectProperty : Int -> Int -> Asm ()
idrisObjectProperty object propertyIndex = do
  locTypes <- GetFunctionLocTypes
  loadVar locTypes inferredObjectType inferredObjectType (Loc object)
  Iconst propertyIndex
  InvokeMethod InvokeStatic idrisObjectType "getProperty" "(Ljava/lang/Object;I)Ljava/lang/Object;" False

assign : (lhs: List LVar) -> (rhs: List LVar) -> Asm ()
assign lhs rhs = do
    locTypes <- GetFunctionLocTypes
    go locTypes lhs rhs
  where
    go : InferredTypeStore -> (lhs: List LVar) -> (rhs: List LVar) -> Asm ()
    go types [] [] = pure ()
    go types [] _  = pure ()
    go types _  [] = pure ()
    go types (lhs :: lhsRest) (rhs :: rhsRest) = do
      let lhsTy = getLocTy types lhs
      let rhsTy = getLocTy types rhs
      loadVar types rhsTy lhsTy rhs
      storeVar lhsTy lhsTy lhs
      go types lhsRest rhsRest

aload : Int -> Asm ()
aload index = do
  types <- GetFunctionLocTypes
  opWithWordSize types Aload (Loc index)


text:
module Simplification

plusZN : (n : Nat) -> 0 + n = n
plusZN n = Refl

plusNZ : (n : Nat) -> n = 0 + n
plusNZ n = Refl

plus1l : (n : Nat) -> 1 + n = S n
plus1l n =  Refl

mult0l : (n : Nat) -> 0 * n = 0
mult0l n = Refl


text:
-- ------------------------------------------------------------- [ Metrics.idr ]
-- Module    : Metrics.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Readability Metrics
|||
||| http://www.editcentral.com/gwt1/EditCentral.html
module Readability.Metrics

%access export

public export
data RMetricTy = FLESCH | ARI | KINCAID | COLEMAN | FOG | SMOG

||| Flesch reading ease score
|||
||| ```java
||| 206.835 - (1.015 * wordCount) / sentenceCount - (84.6 * syllableCount) / wordCount;
||| ```
||| @wcount Number of words
||| @scount Number of sentences.
||| @sycount Number of syllables.
flesch : (wcount : Double) -> (scount : Double) -> (sycount : Double) -> Double
flesch ws ss sys = 206.835 - (1.015 * ws) / ss - (84.6 * sys) / ws

||| Automated readability index
|||
||| ```java
||| (4.71 * letterNumberCount) / wordCount + (0.5 * wordCount) / sentenceCount -21.43;
||| ```
||| @ccount Number of Characters
||| @wcount Number of words.
||| @scount Number of sentences.
ari : (ccount : Double) -> (wcount : Double) -> (scount : Double) -> Double
ari as ws ss = (4.71 * as) / ws + (0.5 * ws) / ss - 21.43

||| Flesch-Kincaid grade level
|||
||| ```java
||| (0.39 * wordCount) / sentenceCount + (11.8 * syllableCount) / wordCount - 15.59;
||| ```
||| @wcount The number of words
||| @scount Number of sentences
||| @sycount Number of syllables.
kincaid : (wcount : Double) -> (scount : Double) -> (sycount : Double) -> Double
kincaid ws ss sys = (0.39 * ws) / ss + (11.8 * sys) / ws - 15.59

||| Coleman-Liau index
|||
||| ```java
||| (5.89 * letterNumberCount) / wordCount - (30.0 * sentenceCount) / wordCount - 15.8;
||| ```
||| @ccount Number of letters and digits.
||| @wcount The number of words.
||| @scount The number of sentences.
coleman : (ccount : Double) -> (wcount : Double) -> (scount : Double) -> Double
coleman as ws ss = (5.89 * as) / ws - (30.0 * ss) / ws - 15.8

||| Gunning fog index
|||
||| ```java
|||  0.4 * ( (double)wordCount / sentenceCount + (100.0 * complexCount) / wordCount );
||| ```
||| @wcount Number of Words
||| @scount Number of sentences
||| @bwcount Number of words with three plus syllables.
fog : (wcount : Double) -> (scount : Double) -> (bwcount : Double) -> Double
fog ws ss bs = 0.4 * ( ws / ss + (100.0 * bs) / ws)

||| SMOG index
|||
||| ```java
||| Math.sqrt( complexCount * 30.0 / sentenceCount ) + 3.0;
||| ```
||| @bwcount The number of word with three plus syllables.
||| @scount The number of sentences.
smog : (bwcount : Double) -> (scount : Double) -> Double
smog bs ss = 3.0 + sqrt (bs * (30 / ss))

Show RMetricTy where
  show FLESCH  = "FLESCH"
  show ARI     = "ARI"
  show KINCAID = "KINCAID"
  show COLEMAN = "COLEMAN"
  show FOG     = "FOG"
  show SMOG    = "SMOG"

Eq RMetricTy where
  (==) FLESCH  FLESCH  = True
  (==) ARI     ARI     = True
  (==) KINCAID KINCAID = True
  (==) COLEMAN COLEMAN = True
  (==) FOG     FOG     = True
  (==) SMOG    SMOG    = True
  (==) _        _      = False

readRMetricTy : String -> Maybe RMetricTy
readRMetricTy s =
  case toLower s of
    "flesch"  => Just FLESCH
    "ari"     => Just ARI
    "kincaid" => Just KINCAID
    "coleman" => Just COLEMAN
    "fog"     => Just FOG
    "smog"    => Just SMOG
    otherwise  => Nothing

public export
record ReadResult where
  constructor MkReadResult
  flesch  : Double
  ari     : Double
  kincaid : Double
  coleman : Double
  fog     : Double
  smog    : Double

toList : ReadResult -> List (RMetricTy, Double)
toList (MkReadResult a b c d e f) =
    [ (FLESCH,  a)
    , (ARI,     b)
    , (KINCAID, c)
    , (COLEMAN, d)
    , (FOG,     e)
    , (SMOG,    f)]

Show ReadResult where
  show rslt = show (Metrics.toList rslt)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
data Expr = Val Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mult Expr Expr

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mult x y) = evaluate x * evaluate y

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
%default total

test : (f : () -> Bool) -> f === (\x => True) -> f () = True
test (\x => True) Refl = Refl


text:
module System.Directory.Extra

import Data.String
import Data.String.Extra
import System
import System.Directory
import System.Path

export
createDirIfNeeded : HasIO io => (path : String) -> io Bool
createDirIfNeeded path =
  pure $
    case !(createDir path) of
         Right ()        => True
         Left FileExists => True
         _               => False

||| Expand path as shells tend to. Limited support so far.
|||
||| e.g. ~/ becomes absolute path of HOME directory.
export
pathExpansion : HasIO io => (path : String) -> io (Maybe String)
pathExpansion path with (strM path)
  pathExpansion ""  | StrNil           = pure $ Just ""
  pathExpansion _   | (StrCons '~' path) = do
    Just home <- getEnv "HOME"
      | Nothing => pure Nothing
    pure . Just $ home </> (drop 1 path)
  pathExpansion str | _                = pure $ Just str

export
inDir : HasIO io => (path : String) -> io a -> io (Maybe a)
inDir path ops = do
  Just cwd <- currentDir
    | Nothing => pure Nothing
  Just dir <- pathExpansion path
    | Nothing => pure Nothing
  True <- changeDir dir
    | False => pure Nothing
  res <- ops
  ignore $ changeDir cwd
  pure (Just res)

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


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

Show a => Show (Vect n a) where
  show xs = "[" ++ showV xs ++ "]"
    where
      showV : forall n . Vect n a -> String
      showV [] = ""
      showV [x] = show x
      showV (x :: xs) = show x ++ ", " ++ showV xs

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter pred [] = (_ ** [])
filter pred (x :: xs)
    = let (n ** xs') = filter pred xs in
          if pred x
             then (_ ** x :: xs')
             else (_ ** xs')

test : (x ** Vect x Nat)
test = (_ ** [1,2])

foo : String
foo = show test

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

main : IO ()
main = printLn (filter even [S Z,2,3,4,5,6])

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
||| Implementation of ordering relations for `Nat`ural numbers
module Data.Nat.Order

import Data.Nat
import Data.Fun
import Data.Rel
import Decidable.Decidable

%default total

public export
zeroNeverGreater : Not (LTE (S n) Z)
zeroNeverGreater LTEZero     impossible
zeroNeverGreater (LTESucc _) impossible

public export
zeroAlwaysSmaller : {n : Nat} -> LTE Z n
zeroAlwaysSmaller = LTEZero

public export
ltesuccinjective : {0 n, m : Nat} -> Not (LTE n m) -> Not (LTE (S n) (S m))
ltesuccinjective disprf (LTESucc nLTEm) = void (disprf nLTEm)
ltesuccinjective disprf LTEZero         impossible

-- Remove any time after release of 0.6.0
||| Deprecated. Use `Nat.isLTE`.
public export
decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)
decideLTE = isLTE

public export
Decidable 2 [Nat,Nat] LTE where
  decide = decideLTE

public export
Decidable 2 [Nat,Nat] LT where
  decide m = decideLTE (S m)

public export
lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n

public export
shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)
shift m n mLTEn = LTESucc mLTEn


text:
module Demo

import public Demo.Utils
import public Demo.Other

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
module ExVectDecEq

import Decidable.Equality

%default total

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

{-
  interface DecEq ty where
    decEq : (val1 : ty) -> (val2 : ty) -> Dec (val1 = val2)

  data Dec : (prop : Type) -> Type where
    Yes : (prf : prop) -> Dec prop
    No : (contra ; prop -> Void) -> Dec prop
-}

headUnequal : DecEq a => { xs: Vect n a } -> { ys : Vect n a } ->
                       (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => { xs : Vect n a } -> { ys : Vect n a } ->
                         (contra : (xs = ys) -> Void) -> ((x :: xs) = (y:: ys)) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq [] _ = No ?nilNotEqualToCons
  decEq _ [] = No ?consNotEqualToNil
  decEq (x :: xs) (y :: ys) = case decEq x y of
                                   No contra => No (headUnequal contra)
                                   Yes Refl => case decEq xs ys of
                                                    No contra => No (tailUnequal contra)
                                                    Yes Refl => Yes Refl

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
namespace X

  export
  f : Int -> Int

namespace Y

  g : Int -> Int -> Int
  g x y = x + f g

namespace X

  f 5 = 6
  f x = x - 1

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module STLC

import Pruviloj
import Pruviloj.Derive.DecEq

%hide Abs
%hide lookup

%language ElabReflection
%default total
%access public export

data Typ
    = Base
    | Arrow Typ Typ

Show Typ where
    show Base = "A"
    show (Arrow ty1 ty2) = (show ty1) ++ "->" ++ (show ty2)

Uninhabited (Base = Arrow _ _) where
    uninhabited Refl impossible

decEqTyp : (ty1, ty2 : Typ) -> Dec (ty1 = ty2)
%runElab (deriveDecEq `{decEqTyp})

DecEq Typ where
    decEq = decEqTyp

data Term
    = Var String
    | Abs String Typ Term
    | App Term Term

Show Term where
    show (Var x) = x
    show (Abs x ty t) = "\\" ++ x ++ " : " ++ (show ty) ++ ". " ++ (show t)
    show (App t1 t2) = (helper t1) ++ " " ++ (helper t2)
        where
            helper (Var x) = x
            helper t = "(" ++ show t ++ ")"
data Value : Term -> Type where
    AbsVal : Value (Abs _ _ _)

Uninhabited (Value (Var _)) where
    uninhabited _ impossible

Uninhabited (Value (App _ _)) where
    uninhabited _ impossible

Ctx : Type
Ctx = List (String, Typ)

data In : (String, Typ) -> Ctx -> Type where
    Here : In (x, ty) ((x, ty)::ctx)
    There : (x = y -> Void) -> In (y, ty1) ctx -> In (y, ty1) ((x, ty2)::ctx)

Uninhabited (In x []) where
    uninhabited _ impossible

inDrop : (x = y -> Void) -> In (x, tt1) ((y, tt2)::ctx) -> In (x, tt1) ctx
inDrop p Here = absurd (p Refl)
inDrop _ (There _ pi) = pi

lookup : (x : String) -> (ctx : Ctx) -> Dec (ty ** In (x, ty) ctx)
lookup _ [] = No (\ (_ ** pi) => uninhabited pi)
lookup x ((y, ty1) :: ctx) with (decEq x y)
    lookup x ((x, ty1) :: ctx) | (Yes Refl) = Yes (ty1 ** Here)
    | (No contra1) with (lookup x ctx)
        | (Yes (ty ** pi)) = Yes (ty ** There (contra1 . sym) pi)
        | (No contra2) = No (\(ty1 ** pi1) =>
            contra2 (ty1 ** inDrop contra1 pi1))

Subset : {z : (String, Typ)} -> (ctx1, ctx2 : Ctx) -> Type
Subset {z = z} ctx1 ctx2 = In z ctx1 -> In z ctx2

subsetNil : Subset [] ctx
subsetNil _ impossible

subsetCons : ({z : (String, Typ)} -> Subset {z = z} ctx1 ctx2) -> Subset ((x, ty)::ctx1) ((x, ty)::ctx2)
subsetCons _ Here = Here
subsetCons ps (There p pi) =
    There p (ps pi)

subsetDrop : Subset ((x, ty1)::(x, ty2)::ctx) ((x, ty1)::ctx)
subsetDrop Here = Here
subsetDrop (There p Here) = absurd (p Refl)
subsetDrop (There p (There _ pi)) = There p pi

subsetSwap : (x = y -> Void) -> Subset ((y, ty1)::(x, ty2)::ctx) ((x, ty2)::(y, ty1)::ctx)
subsetSwap p Here = There p Here
subsetSwap _ (There _ Here) = Here
subsetSwap _ (There p1 (There p2 pi)) = There p2 (There p1 pi)

inUniqueType : In (x, ty1) ctx -> In (x, ty2) ctx -> ty1 = ty2
inUniqueType Here Here = Refl
inUniqueType Here (There p _) = absurd (p Refl)
inUniqueType (There p _) Here = absurd (p Refl)
inUniqueType (There _ pi1) (There _ pi2) = inUniqueType pi1 pi2

data Typed : Ctx -> Term -> Typ -> Type where
    TVar : In (x, ty) ctx -> Typed ctx (Var x) ty
    TAbs : Typed ((x, ty1) :: ctx) t2 ty2 -> Typed ctx (Abs x ty1 t2) (Arrow ty1 ty2)
    TApp : Typed ctx t1 (Arrow ty1 ty2) -> Typed ctx t2 ty1 -> Typed ctx (App t1 t2) ty2

Uninhabited (Typed [] (Var _) _) where
    uninhabited (TVar _) impossible

typedChange : Typed ctx1 t ty -> ({z : (String, Typ)} -> Subset {z = z} ctx1 ctx2) -> Typed ctx2 t ty
typedChange (TVar pi) ps = TVar (ps pi)
typedChange (TAbs pt) ps = TAbs (typedChange pt (subsetCons ps))
typedChange (TApp pt1 pt2) ps =
    let ih1 = typedChange pt1 ps in
    let ih2 = typedChange pt2 ps in
    TApp ih1 ih2

typedWeaken : Typed [] t ty -> Typed ctx t ty
typedWeaken pt = typedChange pt subsetNil

typedDrop : Typed ((x, ty1)::(x, ty2)::ctx) t ty -> Typed ((x, ty1)::ctx) t ty
typedDrop pt = typedChange pt subsetDrop

typedSwap : (x = y -> Void) -> Typed ((y, ty1)::(x, ty2)::ctx) t ty -> Typed ((x, ty2)::(y, ty1)::ctx) t ty
typedSwap pe pt = typedChange pt (subsetSwap pe)

typedUniqueType : (Typed ctx t ty1) -> (Typed ctx t ty2) -> ty1 = ty2
typedUniqueType (TVar pi1) (TVar pi2) = inUniqueType pi1 pi2
typedUniqueType (TAbs pt1) (TAbs pt2) with (typedUniqueType pt1 pt2)
    | Refl = Refl
typedUniqueType (TApp pt1 _) (TApp pt2 _) with (typedUniqueType pt1 pt2)
    | Refl = Refl

subst : String -> Term -> Term -> Term
subst x s (Var y) with (decEq x y)
    | (Yes _) = s
    | (No _) = Var y
subst x s (Abs y ty t) with (decEq x y)
    | (Yes _) = Abs x ty t
    | (No _) = Abs y ty (subst x s t)
subst x s (App t1 t2) = App (subst x s t1) (subst x s t2)

data Eval : Term -> Term -> Type where
    EApp1 : Eval t1 t1' -> Eval (App t1 t2) (App t1' t2)
    EApp2 : Value v1 -> Eval t2 t2' -> Eval (App v1 t2) (App v1 t2')
    EAppAbs : Value v2 -> t1' = subst x v2 t1 -> Eval (App (Abs x ty t1) v2) t1'

progress : (t : Term) -> Typed [] t ty -> Either (Value t) (t' ** Eval t t')
progress (Var _) (TVar _) impossible
progress (Abs _ _ _) (TAbs _) = Left AbsVal
progress (App t1 t2) (TApp pt1 pt2) with (progress t1 pt1)
    | (Right (t1' ** pe)) = Right ((App t1' t2) ** EApp1 pe)
    | (Left pv1) with (progress t2 pt2)
        | (Right (t2' ** pe)) = Right ((App t1 t2') ** EApp2 pv1 pe)
        | (Left pv2) with (pv1)
            progress (App (Abs x _ t) t2) _ | _ | (Left pv2) | AbsVal =
                Right (subst x t2 t ** EAppAbs pv2 Refl)

substyyped : {x : String} -> {s : Term} -> (t : Term) -> Typed [] s ty1 -> Typed ((x, ty1) :: ctx) t ty2 -> Typed ctx (subst x s t) ty2
substyyped {x=x} (Var y) pt1 pt2 with (decEq x y)
    substyyped _ pt1 (TVar Here) | (Yes Refl) = typedWeaken pt1
    substyyped _ _ (TVar (There peq _)) | (Yes Refl) = absurd (peq Refl)
    substyyped _ _ (TVar Here) | (No contra) = absurd (contra Refl)
    substyyped _ _ (TVar (There _ pi)) | (No contra) = TVar pi
substyyped {x=x} (Abs y _ t) pt1 (TAbs pt2) with (decEq x y)
    substyyped _ _ (TAbs pt2) | (Yes Refl) = TAbs (typedDrop pt2)
    substyyped (Abs _ _ t) pt1 (TAbs pt2) | (No pe) =
        let ih = substyyped t pt1 (typedSwap pe pt2) in
        TAbs ih
substyyped (App t1 t2) pt1 (TApp pt2 pt3) =
    let ih1 = substyyped t1 pt1 pt2 in
    let ih2 = substyyped t2 pt1 pt3 in
    TApp ih1 ih2

preservation : (t : Term) -> Typed [] t ty -> Eval t t' -> Typed [] t' ty
preservation (App t1 _) (TApp pt1 pt2) (EApp1 pe) =
    TApp (preservation t1 pt1 pe) pt2
preservation (App (Abs _ _ _) t2) (TApp pt1 pt2) (EApp2 AbsVal pe) =
    TApp pt1 (preservation t2 pt2 pe)
preservation (App (Abs _ _ t1) _) (TApp (TAbs pt1) pt2) (EAppAbs _ peq) =
    rewrite peq in
    substyyped t1 pt2 pt1

data LongEval : Term -> Term -> Type where
    LValue : Value v -> LongEval v v
    LEval : Eval t1 t2 -> LongEval t2 t3 -> LongEval t1 t3

partial
eval' : (t : Term) -> Typed [] t ty -> (t' ** LongEval t t')
eval' t pt with (progress t pt)
    | (Left vt) = (t ** LValue vt)
    | (Right (t' ** pe)) =
        let (t2 ** ple) = eval' t' (preservation t pt pe) in
        (t2 ** LEval pe ple)

typecheckLemma : Typed ctx (App t1 t2) ty -> Typed ctx t1 (Arrow ty1 ty2) -> Typed ctx t2 ty3 -> ty1 = ty3
typecheckLemma (TApp pt1 pt2) pt3 pt4 with (typedUniqueType pt1 pt3)
    | Refl with (typedUniqueType pt2 pt4)
        | Refl = Refl

typecheck : (t : Term) -> (ctx : Ctx) -> Dec (ty ** Typed ctx t ty)
typecheck (Var x) ctx with (lookup x ctx)
    | (Yes (ty ** pi)) = Yes (ty ** TVar pi)
    | (No contra) = No (\(ty ** TVar pi) => contra (ty ** pi))
typecheck (Abs x ty1 t) ctx with (typecheck t ((x, ty1)::ctx))
    | (Yes (ty2 ** pt)) = Yes (Arrow ty1 ty2 ** TAbs pt)
    | (No contra) = No (\(Arrow _ ty4 ** TAbs pt) => contra (ty4 ** pt))
typecheck (App t1 t2) ctx with (typecheck t1 ctx)
    | (No contra) = No (\(ty ** TApp pt1 _) => contra (Arrow _ ty ** pt1))
    | (Yes (Base ** pt)) =
        No (\(_ ** TApp pt1 _) => uninhabited (typedUniqueType pt pt1))
    | (Yes (Arrow ty1 ty2 ** pt1)) with (typecheck t2 ctx)
        | (No contra) = No (\(_ ** TApp _ pt2) => contra (_ ** pt2))
        | (Yes (ty3 ** pt2)) with (decEq ty1 ty3)
            | (No contra) = No (\(ty ** pt3) =>
                contra (typecheckLemma pt3 pt1 pt2))
            | (Yes p) = Yes (ty2 ** TApp pt1 (rewrite p in pt2))
partial
eval : (t : Term) -> Either ((ty ** Typed [] t ty), (t' ** LongEval t t')) ((ty ** Typed [] t ty) -> Void)
eval t with (typecheck t [])
    | (Yes (ty ** pt)) = Left ((ty ** pt), (eval' t pt))
    | (No contra) = Right contra

partial
evalForget : Term-> Maybe Term
evalForget t with (eval t)
    | Left ((_ ** _), (t' ** _)) = Just t'
    | Right _ = Nothing


text:
||| http://okmij.org/ftp/Computation/free-monad.html
||| https://pdfs.semanticscholar.org/e291/5b546b9039a8cf8f28e0b814f6502630239f.pdf
module Freer

%default total
%access public export

data Freer : (s : Type) -> (s -> Type) -> Type -> Type where
  Pure   : x -> Freer s t x
  Impure : (a : s) -> (t a -> Freer s t x) -> Freer s t x

||| Catamorphism
fold : (x -> y) -> ((a : s) -> (t a -> y) -> y) -> Freer s t x -> y
fold r _ (Pure x) = r x
fold r c (Impure s k) = c s $ \t => fold r c (k t)

bind : (x -> Freer s t y) -> Freer s t x -> Freer s t y
bind k = fold k Impure

call : (a : s) -> Freer s t (t a)
call a = Impure a Pure

Functor (Freer s t) where
  map f = bind (Pure . f)

Applicative (Freer s t) where
  pure = Pure
  (Pure f) <*> x = map f x
  (Impure y f) <*> x = ?hole_2

Monad (Freer s t) where
  x >>= f = bind f x

||| Generalized algebraic data type to encode a request
data Request : Type -> Type where
  FileExists : String -> Request Bool
  ReadText : String -> Request String
  GetCwd : Request String

Response : {a : Type} -> Request a -> Type

silly : Freer (Request String) (Response)
silly = do
  cwd <- call GetCwd
  let path = cwd ++ "/hello-world.txt"
  exists <- call $ FileExists path
  if exists
  then call $ ReadText path
  else pure "Hello, World!"

service : Request a -> IO a
-- TODO how to implement this properly in Idris?
service (FileExists _) = pure True
service (ReadText path) = do
  -- `idris_crash` here is obviously lousy, but this is just a simple example
  -- program
  Right x <- readFile path | Left e => idris_crash (show e)
  pure x
service GetCwd = currentDir

main : IO ()
main = do
  msg <- unfree service silly
  putStrLn msg


text:
module Example.Pil.AsC

import Example.Pil

export
Show Name where
  show (MkName n) = n

public export
0 allShows : Expression ctx a -> Type
allShows (C _) = Show a
allShows (V n) = ()
allShows (U _ e) = allShows e
allShows (B _ e1 e2) = (allShows e1, allShows e2)

export
show : (ex : Expression ctx a) -> (shows : allShows ex) => String
show (C x) = show x
show (V n) = show n
show (U f e) = "?(" ++ show e ++ ")"
show (B f e1 e2) = with Example.Pil.AsC.show "(" ++ show e1 {shows = fst shows} ++ ") ?? (" ++ show e2 {shows = snd shows} ++ ")"

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Average

average : (str1: String) -> Double
average str =  let
  numWords = Prelude.List.length (words str)
  totalLength = sum (map Prelude.Strings.length (words str))
  in
  cast totalLength / cast numWords

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module ITree
import Control.Monad.State

-- Based on https://arxiv.org/pdf/1906.00046.pdf

data ITree : (e : Type -> Type) -> (r : Type) -> Type where
  Ret : r -> ITree e r
  Tau : Inf (ITree e r) -> ITree e r
  Vis : e a -> (a -> Inf (ITree e r)) -> ITree e r

implementation Functor (ITree e) where
  map f (Ret x) = Ret $ f x
  map f (Tau tr) = Tau $ map f tr
  map f (Vis e k) = Vis e (\x => map f (k x))

implementation Applicative (ITree e) where
  pure a = Ret a

  (Ret f) <*> tra = map f tra
  (Tau trf) <*> tra = Tau $ trf <*> tra
  (Vis e k) <*> tra = Vis e (\x => k x <*> tra)

implementation Monad (ITree e) where
  (Ret r) >>= f = f r
  (Tau tr) >>= f = Tau $ tr >>= f
  (Vis e f') >>= f = Vis e (\x => f' x >>= f)

interface Monad m => MonadIter (m : Type -> Type) where
  iter : (a -> m (Either a b)) -> a -> m b

implementation MonadIter (ITree e) where
  iter body a = do {
                  ab <- body a;
                  case ab of
                    Left a => Tau $ iter body a
                    Right b => Ret b
                }

implementation MonadIter m => MonadIter (StateT s m) where
  iter body a = ST $ \s => iter (\(a, s) =>
    do {
      (ab, s) <- runStateT (body a) s
      pure $ case ab of
              Left a => Left (a, s)
              Right b => Right (b, s)
    }) (a, s)

interp : MonadIter m => ({r : Type} -> e r -> m r) -> {r : Type} -> ITree e r -> m r
interp h = iter (\tr => case tr of
                          Ret r => pure $ Right r
                          Tau tr => pure $ Left tr
                          Vis e k => h e >>= (\x => pure $ Left (k x)))

data IO' : Type -> Type where
  Input : IO' Nat
  Output : Nat -> IO' ()

spin : ITree IO' ()
spin = Tau spin

kill9 : ITree IO' ()
kill9 = Vis Input (\x => if x == 9 then Ret () else kill9)

data StateE : (s : Type) -> Type -> Type where
  Get : StateE s s
  Put : s -> StateE s ()

handlerState : StateE s r -> StateT s (ITree e) r
handlerState Get = ST $ \s => Ret (s, s)
handlerState (Put s') = ST $ \s => Ret ((), s')

interpState : MonadIter m => ({r : Type} -> e r -> StateT s m r) -> ITree e r -> StateT s m r
interpState h = interp h

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Flutter

import public Dart.FFI.Constructors
import public Flutter.FFI
import public Flutter.Widgets.Functions
import public Flutter.Widgets.Stateful
import public Flutter.Widgets.Stateless
import public Flutter.Widgets.Painter