text:
> module SequentialDecisionProblems.TabBackwardsInduction1

> import Data.Vect
> import Control.Isomorphism
> -- import Debug.Trace

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import Nat.Operations
> import Nat.OperationsProperties
> import Nat.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Decidable.Properties
> import Sigma.Sigma
> import Sigma.Operations
> import Pairs.Operations
> import Vect.Operations
> import Vect.Properties
> import Decidable.Predicates
> import Fin.Operations

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

* Tabulation

If the state space is finite

> finiteState : (t : Nat) -> Finite (State t)

, we can compute the number of values of type |State t| and collect them
in a vector

> cardState : (t : Nat) -> Nat
> cardState t = card (finiteState t)

> vectState : (t : Nat) -> Vect (cardState t) (State t)
> vectState t = toVect (finiteState t)

If |Reachable| and |Viable n| are also decidable

> decidableReachable : {t' : Nat} -> (x' : State t') -> Dec (Reachable x')

< decidableViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (Viable n x)

then their conjunction

> ReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Type
> ReachableAndViable n x = (Reachable x , Viable n x)

is decidable

> decidableReachableAndViable : {t : Nat} -> (n : Nat) -> (x : State t) -> Dec (ReachableAndViable n x)
> decidableReachableAndViable n x = decPair (decidableReachable x) (decidableViable n x)

and we can collect all states which are reachable and viable in a vector:

> cardReachableAndViableState : (t : Nat) -> (n : Nat) -> Nat
> cardReachableAndViableState t n = outl (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

> vectReachableAndViableState : (t : Nat) -> (n : Nat) ->
>                               Vect (cardReachableAndViableState t n) (Sigma (State t) (ReachableAndViable n))
> vectReachableAndViableState t n = outr (f t n) where
>   f : (t : Nat) -> (n : Nat) -> Sigma Nat (\ m => Vect m (Sigma (State t) (ReachableAndViable n)))
>   f t n = filterTagSigma (decidableReachableAndViable n) (vectState t)

In this case, we can implement a "tabulated" versions of |bi| which is
linear in the number of decidion steps. Remember that |optExt| takes a
policy sequence for |n| steps and computes a policy sequence for |n + 1|
steps:

< optExt : {t, n : Nat} ->
<          (ps : PolicySeq (S t) n) -> Policy t (S n)

The idea is to replace the |ps| argument of |optExt| with a "value
table" |vt : Vect (cardReachableAndViableState t n) Val| storing the
value, for every state in |vectReachableAndViableState (S t) n|, of
taking |n| decision steps with |ps| starting from that state. Also ...

> |||
> PolicyTable : (t : Nat) -> (n : Nat) -> Type
> PolicyTable t  Z    = Unit
> PolicyTable t (S m) = Vect
>                       (cardReachableAndViableState t (S m))
>                       (Sigma (State t) (\x => (ReachableAndViable (S m) x, GoodCtrl t x m)))

> |||
> data PolicyTableSeq : (t : Nat) -> (n : Nat) -> Type where
>   Nil   :  {t : Nat} ->
>            PolicyTableSeq t Z
>   (::)  :  {t, n : Nat} ->
>            PolicyTable t (S n) -> PolicyTableSeq (S t) n -> PolicyTableSeq t (S n)

> |||
> ValueTable : Nat -> Nat -> Type
> ValueTable t n = Vect (cardReachableAndViableState t n) Val

> |||
> tabOptExt : {t, n : Nat} ->
>             (vt : ValueTable (S t) n) ->
>             -- (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>             PolicyTable t (S n)

We implement |tabOptExt| on the basis of the implementation of |optExt|
of the core theory. We start with a tabulated version of |sval|:

> tabSval : {t,n : Nat} ->
>         (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>         (gy  : GoodCtrl t x n) ->
>         (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>         PossibleNextState x (ctrl gy) -> Val
> tabSval {t} {n} x r v gy vt (MkSigma x' x'emx') =
>   let y    : Ctrl t x
>            = ctrl gy in
>   let mx'  : M (State (S t))
>            = nexts t x y in
>   let ar'  : All Reachable mx'
>            = reachableSpec1 x r y in
>   let av'  : All (Viable n) mx'
>            = allViable gy in
>   let r'   : Reachable x'
>            = allElemSpec0 x' mx' ar' x'emx' in
>   let v'   : Viable n x'
>            = allElemSpec0 x' mx' av' x'emx' in
>   let rvxs : Vect (cardReachableAndViableState (S t) n) (State (S t))
>            = map outl (vectReachableAndViableState (S t) n) in
>   let dRV  : ((x' : State (S t)) -> Dec (ReachableAndViable n x'))
>            = decidableReachableAndViable n in
>   let prf  : Elem x' (vectState (S t))
>            = toVectComplete (finiteState (S t)) x' in
>   let prf' : Elem x' rvxs
>            = filterTagSigmaLemma {P = ReachableAndViable n} dRV x' (vectState (S t)) prf (r',v') in
>   let k    : Fin (cardReachableAndViableState (S t) n)
>            -- = trace ("Lookup " ++ show n) (lookup x' rvxs prf') in
>            = lookup x' rvxs prf' in
>   reward t x y x' `plus` index k vt

Next, we implement a tabulated version of |cval|:

> tabCval : {t, n : Nat} ->
>         (x  : State t) -> .(r  : Reachable x) -> .(v  : Viable (S n) x) ->
>         (vt : Vect (cardReachableAndViableState (S t) n) Val) ->
>         GoodCtrl t x n -> Val
> tabCval {t} x r v vt gy = let y    : Ctrl t x
>                                  = ctrl gy in
>                         let mx'  : M (State (S t))
>                                  = nexts t x y in
>                         meas (fmap (tabSval x r v gy vt) (tagElem mx'))

And finally

> tabCvalargmax : {t, n : Nat} ->
>               (x  : State t) -> .(r : Reachable x) -> .(v : Viable (S n) x) ->
>               (vt : Vect (cardReachableAndViableState (S t) n) Val) -> GoodCtrl t x n

> {-
> tabOptExt {t} {n} vt = pt where
>   pt : PolicyTable t (S n)
>   pt = toVect ptf where
>     ptf : Fin (cardReachableAndViableState t (S n)) -> (Sigma (State t) (\x => (ReachableAndViable (S n) x, GoodCtrl t x n)))
>     ptf k = MkSigma x (rv, gy) where
>       xrv : Sigma (State t) (ReachableAndViable (S n))
>       xrv = index k (vectReachableAndViableState t (S n))
>       x   : State t
>       x   = outl xrv
>       rv  : ReachableAndViable (S n) x
>       rv  = outr xrv
>       gy  : GoodCtrl t x n
>       gy  = tabCvalargmax x (fst rv) (snd rv) vt
> -}
> tabOptExt {t} {n} vt =
>   let xrv -- : ((k : Fin (cardReachableAndViableState t (S n))) -> Sigma (State t) (ReachableAndViable (S n)))
>           = \ k => index k (vectReachableAndViableState t (S n)) in
>   let x   : ((k : Fin (cardReachableAndViableState t (S n))) -> State t)
>           = \ k => outl (xrv k) in
>   let rv  -- : ((k : Fin (cardReachableAndViableState t (S n))) -> ReachableAndViable (S n) (x k))
>           = \ k => outr (xrv k) in
>   let gy  -- : ((k : Fin (cardReachableAndViableState t (S n))) -> GoodCtrl t (x k) n)
>           = \ k => tabCvalargmax (x k) (fst (rv k)) (snd (rv k)) vt in
>   let ptf -- : ((k : Fin (cardReachableAndViableState t (S n))) -> (Sigma (State t) (\ x => (ReachableAndViable (S n) x, GoodCtrl t x n))))
>           = \ k => MkSigma (x k) (rv k, gy k) in
>   let pt  : PolicyTable t (S n)
>           = toVect ptf in
>   pt

* Tabulated tail-recursive backwards induction

With |tabOptExt| in place, it is easy to implement a tabulated version of
|trbi|:

> |||
> PolicySeqAndTab : Nat -> Nat -> Type
> PolicySeqAndTab t n = (PolicySeq t n, ValueTable t n)

> |||
> zeroVec : (n : Nat) -> Vect n Val
> zeroVec Z     = Nil
> zeroVec (S n) = zero :: zeroVec n

> ||| Tabulated tail-recursive backwards induction iteration
> ttrbii : (t : Nat) -> (n : Nat) -> (c : Nat) -> (LTE c n) ->
>          PolicyTableSeq (c + t) (n - c) ->
>          (vt : Vect (cardReachableAndViableState (c + t) (n - c)) Val) ->
>          PolicyTableSeq t n
>
> ttrbii t n  Z     prf pts vt = replace {P = \ z => PolicyTableSeq t z} (minusZeroRight n) pts
> {-
> ttrbii t n (S c') prf pts vt = ttrbii t n c' prf' pts' vt'' where
>   bic  : S (n - S c') = n - c'
>   bic  = minusLemma4 prf
>   prf' : LTE c' n
>   prf' = lteLemma1 c' n prf
>   pt   : PolicyTable (c' + t) (S (n - S c'))
>   pt   = tabOptExt vt
>   pts' : PolicyTableSeq (c' + t) (n - c')
>   pts' = replace {P = \ z => PolicyTableSeq (c' + t) z} bic (pt :: pts)
>   vt'  : Vect (cardReachableAndViableState (c' + t) (S (n - S c'))) Val
>   vt'  = toVect vt'f where
>     vt'f : Fin (cardReachableAndViableState (c' + t) (S (n - S c'))) -> Val
>     vt'f k = tabCval x r v vt gy where
>       xrvgy : Sigma (State (c' + t)) (\ x => (ReachableAndViable (S (n - S c')) x, GoodCtrl (c' + t) x (n - S c')))
>       xrvgy = index k pt
>       x     : State (c' + t)
>       x     = outl xrvgy
>       rv    : ReachableAndViable (S (n - S c')) x
>       rv    = fst (outr xrvgy)
>       r     : Reachable x
>       r     = fst rv
>       v     : Viable (S (n - S c')) x
>       v     = snd rv
>       gy    : GoodCtrl (c' + t) x (n - S c')
>       gy    = snd (outr xrvgy)
>   vt''  : Vect (cardReachableAndViableState (c' + t) (n - c')) Val
>   vt''  = replace {P = \z => Vect (cardReachableAndViableState (c' + t) z) Val} bic vt'
> -}
> ttrbii t n (S c') prf pts vt =
>   let bic   : (S (n - S c') = n - c')
>             = minusLemma4 prf in
>   let prf'  : LTE c' n
>             = lteLemma1 c' n prf in
>   let pt    : PolicyTable (c' + t) (S (n - S c'))
>             = tabOptExt vt in
>   let pts'  : PolicyTableSeq (c' + t) (n - c')
>             = replace {P = \ z => PolicyTableSeq (c' + t) z} bic (pt :: pts) in
>   let xrvgy -- : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) ->
>             --    Sigma (State (c' + t)) (\ x => (ReachableAndViable (S (n - S c')) x, GoodCtrl (c' + t) x (n - S c'))))
>             = \ k => index k pt in
>   let x     : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> State (c' + t))
>             = \ k => outl (xrvgy k) in
>   let rv    -- : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> ReachableAndViable (S (n - S c')) (x k))
>             = \ k => fst (outr (xrvgy k)) in
>   let r     : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Reachable {t' = c' + t} (x k))
>             = \ k => fst (rv k) in
>   let v     : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Viable {t = c' + t} (S (n - S c')) (x k))
>             = \ k => snd (rv k) in
>   let gy    : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> GoodCtrl (c' + t) (x k) (n - S c'))
>             = \ k => snd (outr (xrvgy k)) in
>   let vt'f  : ((k : Fin (cardReachableAndViableState (c' + t) (S (n - S c')))) -> Val)
>             = \ k => tabCval (x k) (r k) (v k) vt (gy k) in
>   let vt'   : Vect (cardReachableAndViableState (c' + t) (S (n - S c'))) Val
>             = toVect vt'f in
>   let vt''  : Vect (cardReachableAndViableState (c' + t) (n - c')) Val
>             = replace {P = \z => Vect (cardReachableAndViableState (c' + t) z) Val} bic vt' in
>   ttrbii t n c' prf' pts' vt''

> ||| Tabulated tail-recursive backwards induction
> tabTailRecursiveBackwardsInduction1 : (t : Nat) -> (n : Nat) -> PolicyTableSeq t n
> tabTailRecursiveBackwardsInduction1 t n = ttrbii t n n (reflexiveLTE n) zps (zeroVec _) where
>   zps : PolicyTableSeq (n + t) (n - n)
>   zps = replace {P = \ z => PolicyTableSeq (n + t) z} (minusZeroN n) Nil

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module SnocList

-- data SnocList ty = Nil | Snoc (SnocList ty) ty

public export
data SnocList : List a -> Type where
  Empty : SnocList []
  Snoc : (rec : SnocList xs) -> SnocList (xs ++ [x])

public export
snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs
  where
    snocListHelp : SnocList input -> (xs : List a) -> SnocList (input ++ xs)
    snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
    snocListHelp {input} snoc (x :: xs)
      = rewrite appendAssociative input [x] xs in
                (snocListHelp (Snoc snoc {x}) xs)

my_reverse_help' : (input : List a) -> SnocList input -> List a
my_reverse_help' [] Empty = []
my_reverse_help' (xs ++ [x]) (Snoc rec) = x :: my_reverse_help' xs rec

total
my_reverse' : List a -> List a
my_reverse' xs = my_reverse_help' xs (snocList xs)

total
my_reverse : List a -> List a
my_reverse input with (snocList input)
  my_reverse [] | Empty = []
  my_reverse (xs ++ [x]) | (Snoc rec) = x :: my_reverse xs | rec

-- reverse_snoc : SnocList ty -> List ty
-- reverse_snoc [] = []
-- reverse_snoc (Snoc xs x) = x :: reverse_snoc xs

ext: idr

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:
%default total

ohNo : Void
ohNo = let (? ** x) = the (a ** a) (Int ** 5) in x


text:
module Main

mkList : Int -> Int -> List Int
mkList seed 0 = []
mkList seed n =
  let seed' = (seed * 1664525) + 1013904223 in
  seed `mod` 1000 :: mkList seed' (n - 1)

insert : Int -> List Int -> List Int
insert x [] = [x]
insert x (y :: ys) =
  if x < y
    then x :: y :: ys
    else y :: insert x ys

sort : List Int -> List Int
sort [] = []
sort (x :: xs) = insert x (sort xs)

main : IO ()
main = printLn (sort (mkList 1234567890 10000))


text:
-- Some tests to see if it would run into race conditions

module QueueTest

import Utils.Queue
import System.Future
import System

spawn_worker : Queue String -> String -> IO ()
spawn_worker channel name = do
  thing <- recv channel
  putStrLn "\{name} got \{thing}"
  usleep 100
  spawn_worker channel name

send_stuff : Queue String -> IO ()
send_stuff queue = do
  t <- time
  signal queue "toby \{show t}"
  usleep 100
  send_stuff queue

brod_stuff : Queue String -> IO ()
brod_stuff queue = do
  t <- time
  broadcast queue "toby \{show t}"
  usleep 100
  send_stuff queue

main : (Queue String -> IO ()) -> IO ()
main f = do
  queue <- mk_queue
  putStrLn "spawning workers"
  _ <- forkIO $ spawn_worker queue "1"
  _ <- forkIO $ spawn_worker queue "2"
  _ <- forkIO $ spawn_worker queue "3"
  _ <- forkIO $ spawn_worker queue "4"

  putStrLn "signalling"
  f queue


text:
module Command

import Fuel

public export
data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String
  ReadFile : String -> Command String
  WriteFile : String -> String -> Command ()
  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

public export
data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace CommandDo
  public export
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

namespace ConsoleDo
  public export
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

public export
runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (ReadFile file) =
  (either (const "") id) <$> (readFile file)
runCommand (WriteFile file content) =
  (either (const ()) id) <$> (writeFile file content)
runCommand (Pure x) = pure x
runCommand (Bind c f) = do
  res  <- runCommand c
  runCommand (f res)

public export
run : Fuel -> ConsoleIO a -> IO (Maybe a)
run _ (Quit value) = pure (Just value)
run (More fuel) (Do k f) = do
  res <- runCommand k
  run fuel (f res)
run Dry _ = pure Nothing


text:
module Dummy

import System.Directory

dirExists : String -> IO Bool
dirExists dir = do
  Right d <- openDir dir
    | Left _ => pure False
  closeDir d
  pure True

main : IO ()
main = do
  True <- dirExists "custom_build"
    | False => putStrLn "Could not find build directory"
  putStrLn "Found build directory"


text:
module NQueensSMT

import Data.Vect
import src.SMTLib
import src.Tensor

N : Nat
N = 8

columns : Tensor [N] String
columns = toTensor $ tabulate (\i => "c_" ++ show (finToNat i))

rows : Tensor [N] String
rows = toTensor $ tabulate (\i => "r_" ++ show (finToNat i))

constrs : Vect n (Expr (NumT IntT)) -> Expr BoolT
constrs {n} xs = and [x >= (int 0) && x < (int (toIntNat n)) | x <- xs]

diags : Vect n (Expr (NumT IntT)) -> Vect n (Expr (NumT IntT)) -> Expr BoolT
diags [] [] = bool True
diags (col :: cols) (row :: rows) = let cs = map (\col' => abs $ col - col') cols in
                                    let rs = map (\row' => abs $ row - row') rows in
                                    let neqs = map (\(c, r) => not $ c == r) $ zip cs rs in
                                    and (diags cols rows :: neqs)
  where
    abs : Expr (NumT IntT) -> Expr (NumT IntT)
    abs x = ite (x >= (int 0)) x (x * (int (-1)))

solver : Smt ()
solver = do cols <- declareVars columns (NumT IntT)
            rows <- declareVars rows (NumT IntT)
            let cols = toVect cols
            let rows = toVect rows
            assert $ distinct cols
            assert $ distinct rows
            assert $ constrs cols
            assert $ constrs rows
            assert $ diags cols rows
            checkSat
            getModel
            end

test : IO ()
test = print solver

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Instances.OrderZZ

import public Data.Vect
import public Data.Rel
import public Decidable.Decidable
import Data.ZZ

%default total
%access export

||| LTE for ZZ, build on top of LTE for Nat.
public export
data LTEZ : ZZ -> ZZ -> Type where
  LtePosPos : LTE n m -> LTEZ (Pos n) (Pos m)
  LteNegNeg : LTE n m -> LTEZ (NegS m) (NegS n)
  LteNegPos : LTEZ (NegS _) (Pos _)

||| Because a positive number is always greater than a negative one.
public export
implementation Uninhabited (Pos _ `LTEZ` NegS _) where
  uninhabited _ impossible

public export
unwrapLtePosPos : LTEZ (Pos n) (Pos m) -> LTE n m
unwrapLtePosPos (LtePosPos prf) = prf

public export
unwrapLteNegNeg : LTEZ (NegS n) (NegS m) -> LTE m n
unwrapLteNegNeg (LteNegNeg prf) = prf

||| TODO. Consider import from Decidable.Order
lteAntisymmetric : LTE n m -> LTE m n -> n = m
lteAntisymmetric LTEZero LTEZero = Refl
lteAntisymmetric (LTESucc p) (LTESucc q) = cong $ lteAntisymmetric p q

||| Not yet in the base libraries.
public export
interface Bifunctor (f : Type -> Type -> Type) where
  bimap : (a -> b) -> (c -> d) -> f a c -> f b d

||| Not yet in the base libraries.
public export
implementation Bifunctor Either where
  bimap f _ (Left a) = Left (f a)
  bimap _ g (Right b) = Right (g b)

||| TODO. Consider import from Decidable.Order
lteTotal : (n,m : Nat) -> Either (LTE n m) (LTE m n)
lteTotal Z _ = Left LTEZero
lteTotal _ Z = Right LTEZero
lteTotal (S n) (S m) = bimap LTESucc LTESucc (lteTotal n m)

lteReflZ : (x : ZZ) -> LTEZ x x
lteReflZ (Pos _) = LtePosPos lteRefl
lteReflZ (NegS _) = LteNegNeg lteRefl

lteTransitiveZ : (x,y,z : ZZ) -> LTEZ x y -> LTEZ y z -> LTEZ x z
lteTransitiveZ _ _ _ (LtePosPos p) (LtePosPos q) = LtePosPos (lteTransitive p q)
lteTransitiveZ _ _ _ (LteNegNeg p) (LteNegNeg q) = LteNegNeg (lteTransitive q p)
lteTransitiveZ _ _ _ (LteNegNeg _) LteNegPos = LteNegPos
lteTransitiveZ _ _ _ LteNegPos (LtePosPos _) = LteNegPos

lteAntisymmetricZ : (x,y : ZZ) -> LTEZ x y -> LTEZ y x -> x = y
lteAntisymmetricZ _ _ (LtePosPos p) (LtePosPos q) = cong $ lteAntisymmetric p q
lteAntisymmetricZ _ _ (LteNegNeg p) (LteNegNeg q) = cong $ lteAntisymmetric q p

lteTotalZ : (x,y : ZZ) -> Either (LTEZ x y) (LTEZ y x)
lteTotalZ (Pos _) (NegS _) = Right LteNegPos
lteTotalZ (NegS _) (Pos _) = Left LteNegPos
lteTotalZ (Pos n) (Pos m) = bimap LtePosPos LtePosPos (lteTotal n m)
lteTotalZ (NegS n) (NegS m) = bimap LteNegNeg LteNegNeg (lteTotal m n)

||| The difficulty here, is to hop over the split at zero.
lteSuccZ : (x,y : ZZ) -> LTEZ x y -> LTEZ (Pos 1 + x) (Pos 1 + y)
lteSuccZ _ _ (LtePosPos p) = LtePosPos (LTESucc p)
lteSuccZ (NegS (S _)) (NegS (S _)) (LteNegNeg p) = LteNegNeg (fromLteSucc p)
lteSuccZ (NegS (S _)) (NegS Z) _ = LteNegPos
lteSuccZ (NegS (S _)) (Pos _) _ = LteNegPos
lteSuccZ (NegS Z) (Pos _) _ = LtePosPos LTEZero
lteSuccZ (NegS Z) (NegS Z) _ = LtePosPos lteRefl
lteSuccZ (NegS Z) (NegS (S _)) (LteNegNeg _) impossible
lteSuccZ (Pos _) (NegS _) p = absurd p

||| The difficulty here, is to hop over the split at zero.
ltePredZ : (x,y : ZZ) -> LTEZ x y -> LTEZ (NegS Z + x) (NegS Z + y)
ltePredZ (Pos (S _)) (Pos (S _)) (LtePosPos p) = LtePosPos (fromLteSucc p)
ltePredZ (Pos Z) (Pos (S _)) _ = LteNegPos
ltePredZ (Pos Z) (Pos Z) _ = LteNegNeg lteRefl
ltePredZ (NegS _) (Pos (S _)) _ = LteNegPos
ltePredZ (NegS _) (Pos Z) _ = LteNegNeg LTEZero
ltePredZ (NegS n) (NegS m) (LteNegNeg p) = LteNegNeg (LTESucc p)
ltePredZ (Pos (S _)) (Pos Z) (LtePosPos _) impossible
ltePredZ (Pos _) (NegS _) p = absurd p

||| Lemma
private
lteLeftTranslationInvariantPosZ : (x,y : ZZ) -> (n : Nat) ->
  LTEZ x y -> LTEZ (Pos n + x) (Pos n + y)
lteLeftTranslationInvariantPosZ x y Z prf =
  rewrite plusZeroLeftNeutralZ x in
  rewrite plusZeroLeftNeutralZ y in prf
lteLeftTranslationInvariantPosZ x y (S n) prf =
  rewrite sym $ plusAssociativeZ (Pos 1) (Pos n) x in
  rewrite sym $ plusAssociativeZ (Pos 1) (Pos n) y in
  lteSuccZ _ _ (lteLeftTranslationInvariantPosZ x y n prf)

||| Lemma
private
lteLeftTranslationInvariantNegZ : (x,y : ZZ) -> (n : Nat) ->
  LTEZ x y -> LTEZ (NegS n + x) (NegS n + y)
lteLeftTranslationInvariantNegZ x y Z prf = ltePredZ x y prf
lteLeftTranslationInvariantNegZ x y (S n) prf =
  rewrite sym $ plusAssociativeZ (NegS Z) (NegS n) x in
  rewrite sym $ plusAssociativeZ (NegS Z) (NegS n) y in
  ltePredZ _ _ (lteLeftTranslationInvariantNegZ x y n prf)

||| This order is translation invariant.
lteLeftTranslationInvariantZ : (x,y,a : ZZ) ->
  LTEZ x y -> plusZ a x `LTEZ` plusZ a y
lteLeftTranslationInvariantZ x y (Pos n) =
  lteLeftTranslationInvariantPosZ x y n
lteLeftTranslationInvariantZ x y (NegS n) =
  lteLeftTranslationInvariantNegZ x y n

||| Make ZZ into a discrete ordered group.
lteDiscreteZ : (x : ZZ) ->
  Not (x = Pos Z) -> LTEZ x (Pos Z) -> LTEZ (Pos 1 + x) (Pos Z)
lteDiscreteZ (Pos (S _)) _ (LtePosPos p) = absurd (succNotLTEzero p)
lteDiscreteZ (Pos Z) notZ _ = absurd (notZ Refl)
lteDiscreteZ (NegS Z) _ LteNegPos = LtePosPos LTEZero
lteDiscreteZ (NegS (S _)) _ LteNegPos = LteNegPos

||| Lift a decision from Nat to ZZ.
public export
toLtePosPos : Dec (LTE n m) -> Dec (LTEZ (Pos n) (Pos m))
toLtePosPos (Yes prf) = Yes (LtePosPos prf)
toLtePosPos (No contra) = No (contra . unwrapLtePosPos)

||| Lift a decision from Nat to ZZ.
public export
toLteNegNeg : Dec (LTE n m) -> Dec (LTEZ (NegS m) (NegS n))
toLteNegNeg (Yes prf) = Yes (LteNegNeg prf)
toLteNegNeg (No contra) = No (contra . unwrapLteNegNeg)

public export
isLTEZ : (x,y : ZZ) -> Dec (LTEZ x y)
isLTEZ (Pos n) (Pos m) = toLtePosPos (isLTE n m)
isLTEZ (NegS n) (NegS m) = toLteNegNeg (isLTE m n)
isLTEZ (NegS _) (Pos _) = Yes LteNegPos
isLTEZ (Pos _) (NegS _) = No absurd

public export
implementation Decidable [ZZ, ZZ] LTEZ where
  decide = isLTEZ

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Data.Time.Calendar.Days

import Generics.Derive

%default total
%language ElabReflection

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

public export
record Day where
  constructor ModifiedJulianDay
  modifiedJulianDay : Integer

%runElab derive "Day" [Generic, Meta, Eq, Ord, DecEq]

export addDays : Integer -> Day -> Day
addDays n x = { modifiedJulianDay $= (+n) } x

export diffDays : Day -> Day -> Integer
diffDays x y = x.modifiedJulianDay - y.modifiedJulianDay

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


text:
module Lambdapants.Colors

%default total

public export
data Color
  = Black
  | Red
  | Green
  | Yellow
  | Blue
  | Purple
  | Cyan
  | White

public export
data AnsiColor
  = Regular Color
  | Intense Color

public export
data Style
  = Normal
  | Bold
  | Underline
  | Italic
  | Reverse
  | Strikethrough

color : Color -> String
color Black  = "0"
color Red    = "1"
color Green  = "2"
color Yellow = "3"
color Blue   = "4"
color Purple = "5"
color Cyan   = "6"
color White  = "7"

foreground : AnsiColor -> String
foreground (Regular code) =  "3" ++ color code
foreground (Intense code) =  "9" ++ color code

background : AnsiColor -> String
background (Regular code) =  "4" ++ color code
background (Intense code) = "10" ++ color code

font : Style -> String
font Normal        = "0"
font Bold          = "1"
font Italic        = "3"
font Underline     = "4"
font Reverse       = "7"
font Strikethrough = "9"

export
decorated : Style -> Maybe AnsiColor -> Maybe AnsiColor -> String -> String
decorated style fg bg str = "\ESC[" ++ body ++ "m" ++ str ++ "\ESC[0m" where
  codes : List String
  codes = catMaybes [ Just (font style), background <$> bg, foreground <$> fg ]
  body : String
  body = foldr (++) "" (intersperse ";" codes)

export
error : String -> String
error = decorated Bold (Just (Intense Red)) Nothing

export
okay : String -> String
okay = decorated Normal (Just (Regular Green)) Nothing

max_stars_repo_name: laserpants/redex-reflex

max_issues_repo_name: laserpants/lambdapants

max_forks_repo_name: laserpants/lambdapants


text:
module IdrisJvm.Core.Foreign

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.IR.Types
import Data.SortedMap

%access public export

data JForeign = JStatic String String
              | JGetStaticField String String
              | JSetStaticField String String
              | JVirtual String String
              | JGetInstanceField String String
              | JSetInstanceField String String
              | JInterface String String
              | JNew String
              | JNewArray
              | JMultiNewArray
              | JSetArray
              | JGetArray
              | JArrayLength
              | JClassLiteral String
              | JLambda String String
              | JInstanceOf String

javaReturn : TypeDescriptor -> Asm ()
javaReturn VoidDescriptor                       = Return
javaReturn (FieldDescriptor FieldTyDescBoolean) = Ireturn
javaReturn (FieldDescriptor FieldTyDescByte)    = Ireturn
javaReturn (FieldDescriptor FieldTyDescShort)   = Ireturn
javaReturn (FieldDescriptor FieldTyDescInt)     = Ireturn
javaReturn (FieldDescriptor FieldTyDescChar)    = Ireturn
javaReturn (FieldDescriptor FieldTyDescLong)    = Lreturn
javaReturn (FieldDescriptor FieldTyDescFloat)   = Freturn
javaReturn (FieldDescriptor FieldTyDescDouble)  = Dreturn
javaReturn _                                    = Areturn

mutual
  fdescFieldDescriptor : FDesc -> FieldTypeDescriptor
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntNative"]) = FieldTyDescInt
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntChar"]) = FieldTyDescChar
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntBits8"]) = FieldTyDescByte
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntBits16"]) = FieldTyDescShort
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntBits32"]) = FieldTyDescInt
  fdescFieldDescriptor (FApp "JVM_IntT" [_, FCon "JVM_IntBits64"]) = FieldTyDescLong
  fdescFieldDescriptor (FCon "JVM_Float") = FieldTyDescFloat
  fdescFieldDescriptor (FCon "JVM_Double") = FieldTyDescDouble
  fdescFieldDescriptor (FCon "JVM_Bool") = FieldTyDescBoolean

  fdescFieldDescriptor (FCon "JVM_Str") = FieldTyDescReference $ ClassDesc "java/lang/String"
  fdescFieldDescriptor (FCon "JVM_BigInteger") = FieldTyDescReference $ ClassDesc "java/math/BigInteger"
  fdescFieldDescriptor fdesc = FieldTyDescReference $ fdescRefDescriptor fdesc

  fdescRefDescriptor : FDesc -> ReferenceTypeDescriptor
  fdescRefDescriptor desc@(FApp "JVM_NativeT" [FApp "Class" [FStr typeName]]) = ClassDesc typeName
  fdescRefDescriptor desc@(FApp "JVM_NativeT" [FApp "Interface" [FStr typeName]]) = InterfaceDesc typeName

  fdescRefDescriptor desc@(FApp "JVM_ArrayT" [_, elemDesc]) = ArrayDesc $ fdescFieldDescriptor elemDesc

  fdescRefDescriptor (FCon "JVM_Str") = ClassDesc "java/lang/String"
  fdescRefDescriptor (FCon "JVM_BigInteger") = ClassDesc "java/math/BigInteger"
  fdescRefDescriptor (FStr exportedType) = IdrisExportDesc exportedType
  fdescRefDescriptor desc = jerror $ "Invalid reference type descriptor: " ++ show desc

fdescTypeDescriptor : FDesc -> TypeDescriptor
fdescTypeDescriptor (FCon "JVM_Unit") = VoidDescriptor
fdescTypeDescriptor (FIO t) = fdescTypeDescriptor t
fdescTypeDescriptor (FApp "JVM_ThrowableT" [_, desc]) = ThrowableDescriptor $ fdescTypeDescriptor desc
fdescTypeDescriptor fdesc = FieldDescriptor $ fdescFieldDescriptor fdesc

isExportIO : FDesc -> Bool
isExportIO (FIO _) = True
isExportIO _       = False

parseExportedClassName : String -> (ClassName, ClassName, List ClassName)
parseExportedClassName desc
= let parts = filter ((/=) "") . map trim . Strings.split (\c => c == ' ' || c == ',') $ desc
  in case parts of
       [c] => (c, "java/lang/Object", [])
       [c, "extends", p] => (c, p, [])
       (c :: "implements" :: intfs) => (c, "java/lang/Object", intfs)
       (c :: "extends" :: p :: "implements" :: intfs) => (c, p, intfs)
       _ => jerror $ "invalid class descriptor in export: " ++ desc

fieldTypeDescriptorToInferredType : FieldTypeDescriptor -> InferredType
fieldTypeDescriptorToInferredType FieldTyDescByte             = IByte
fieldTypeDescriptorToInferredType FieldTyDescChar             = IChar
fieldTypeDescriptorToInferredType FieldTyDescShort            = IShort
fieldTypeDescriptorToInferredType FieldTyDescBoolean          = IBool
fieldTypeDescriptorToInferredType FieldTyDescDouble           = IDouble
fieldTypeDescriptorToInferredType FieldTyDescFloat            = IFloat
fieldTypeDescriptorToInferredType FieldTyDescInt              = IInt
fieldTypeDescriptorToInferredType FieldTyDescLong             = ILong
fieldTypeDescriptorToInferredType (FieldTyDescReference (ArrayDesc elemTy))
    = IArray $ fieldTypeDescriptorToInferredType elemTy
fieldTypeDescriptorToInferredType (FieldTyDescReference refTy) = Ref (refTyClassName refTy)

typeDescriptorToInferredType : TypeDescriptor -> InferredType
typeDescriptorToInferredType (ThrowableDescriptor _) = inferredObjectType
typeDescriptorToInferredType VoidDescriptor          = IUnknown
typeDescriptorToInferredType (FieldDescriptor fieldTyDesc) = fieldTypeDescriptorToInferredType fieldTyDesc

idrisToJava : List (FieldTypeDescriptor, LVar) -> Asm ()
idrisToJava vars = do
    locTypes <- GetFunctionLocTypes
    sequence_ $ map (f locTypes) vars
  where
    f :  InferredTypeStore -> (FieldTypeDescriptor, LVar) -> Asm ()
    f locTypes (ty, v) = do
      let vTy = getLocTy locTypes v
      loadVar locTypes vTy (fieldTypeDescriptorToInferredType ty) v

idrisToJavaLoadArray : List (FieldTypeDescriptor, LVar) -> Asm ()
idrisToJavaLoadArray = sequence_ . intersperse Aaload . map f where
  f : (FieldTypeDescriptor, LVar) -> Asm ()
  f (ty, v) = do
    locTypes <- GetFunctionLocTypes
    let vTy = getLocTy locTypes v
    loadVar locTypes vTy (fieldTypeDescriptorToInferredType ty) v

parseDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
parseDescriptor returns ffi argsDesc = tryParseStaticMethodDescriptor returns ffi argsDesc where

  unsupportedDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  unsupportedDescriptor returns ffiDesc args =
      jerror $ "Unsupported descriptor: " ++ show ffiDesc ++ ", returns: " ++ show returns ++ ", args: " ++ show args

  tryParseInstanceOfDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseInstanceOfDescriptor returns (FApp "InstanceOf" [FStr cname]) argsDesc = JInstanceOf cname
  tryParseInstanceOfDescriptor returns ffi argsDesc = unsupportedDescriptor returns ffi argsDesc

  tryParseLambdaDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseLambdaDescriptor returns ffiDesc@(FApp ffi [FApp nativeTy [FStr cname], FStr interfaceMethodName]) argsDesc
    = if ffi == "Lambda" && nativeTy == "Interface"
        then JLambda cname interfaceMethodName
        else tryParseInstanceOfDescriptor returns ffiDesc argsDesc
  tryParseLambdaDescriptor returns ffi argsDesc = tryParseInstanceOfDescriptor returns ffi argsDesc

  tryParseClassLiteralDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseClassLiteralDescriptor returns ffiDesc@(FApp ffi [FStr cname]) argsDesc
    = if ffi == "ClassLiteral"
        then JClassLiteral cname
        else tryParseLambdaDescriptor returns ffiDesc argsDesc
  tryParseClassLiteralDescriptor returns ffi argsDesc = tryParseLambdaDescriptor returns ffi argsDesc

  tryParseArrayLengthDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseArrayLengthDescriptor returns (FCon "ArrayLength") argsDesc = JArrayLength
  tryParseArrayLengthDescriptor returns ffi argsDesc = tryParseClassLiteralDescriptor returns ffi argsDesc

  tryParseGetArrayDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseGetArrayDescriptor returns (FCon "GetArray") argsDesc = JGetArray
  tryParseGetArrayDescriptor returns ffi argsDesc = tryParseArrayLengthDescriptor returns ffi argsDesc

  tryParseSetArrayDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseSetArrayDescriptor returns (FCon "SetArray") argsDesc = JSetArray
  tryParseSetArrayDescriptor returns ffi argsDesc = tryParseGetArrayDescriptor returns ffi argsDesc

  tryParseMultiNewArrayDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseMultiNewArrayDescriptor returns (FCon "MultiNewArray") argsDesc = JMultiNewArray
  tryParseMultiNewArrayDescriptor returns ffi argsDesc = tryParseSetArrayDescriptor returns ffi argsDesc

  tryParseNewArrayDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseNewArrayDescriptor returns (FCon "NewArray") argsDesc = JNewArray
  tryParseNewArrayDescriptor returns ffi argsDesc = tryParseMultiNewArrayDescriptor returns ffi argsDesc

  tryParseConstructorDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseConstructorDescriptor returns ffiDesc@(FCon ffi) argsDesc
    = if ffi == "New" then
        case fdescTypeDescriptor returns of
            (FieldDescriptor (FieldTyDescReference (ClassDesc cname)))    => JNew cname
            (ThrowableDescriptor (FieldDescriptor (FieldTyDescReference (ClassDesc cname)))) => JNew cname
            (FieldDescriptor (FieldTyDescReference (InterfaceDesc _)))    =>
                jerror $ "Invalid FFI descriptor for constructor. A constructor can't return an interface type. "
            (FieldDescriptor (FieldTyDescReference (ArrayDesc _)))        => jerror "No constructors for array types"
            (FieldDescriptor (FieldTyDescReference (IdrisExportDesc _)))  =>
                jerror "Cannot invoke constructor of Idris exported type"
        else
            tryParseNewArrayDescriptor returns ffiDesc argsDesc
  tryParseConstructorDescriptor returns ffi argsDesc = tryParseNewArrayDescriptor returns ffi argsDesc

  tryParseSetInstanceFieldDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseSetInstanceFieldDescriptor returns ffiDesc@(FApp ffi [FStr fieldName]) argsDesc@((declClass, _)::_)
    = if ffi == "SetInstanceField"
        then case fdescRefDescriptor declClass of
                ClassDesc cname => JSetInstanceField cname fieldName
                _               => jerror "Fields can be set only from classes"
      else tryParseConstructorDescriptor returns ffiDesc argsDesc
  tryParseSetInstanceFieldDescriptor returns ffi argsDesc = tryParseConstructorDescriptor returns ffi argsDesc

  tryParseGetInstanceFieldDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseGetInstanceFieldDescriptor returns ffiDesc@(FApp ffi [FStr fieldName]) argsDesc@((declClass, _)::_)
    = if ffi == "GetInstanceField"
        then case fdescRefDescriptor declClass of
                ClassDesc cname => JGetInstanceField cname fieldName
                _               => jerror "Fields can be accessed only from classes"
        else tryParseSetInstanceFieldDescriptor returns ffiDesc argsDesc
  tryParseGetInstanceFieldDescriptor returns ffi argsDesc = tryParseSetInstanceFieldDescriptor returns ffi argsDesc

  tryParseInstanceMethodDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseInstanceMethodDescriptor returns ffiDesc@(FApp ffi [FStr fn]) argsDesc@((declClass, _)::_)
    = if ffi == "Instance"
        then case fdescRefDescriptor declClass of
                ClassDesc cname     => JVirtual cname fn
                InterfaceDesc cname => JInterface cname fn
                ArrayDesc _         => jerror "No instance methods on an array"
                IdrisExportDesc _   => jerror "No instance methods on an Idris exported type"
        else tryParseGetInstanceFieldDescriptor returns ffiDesc argsDesc
  tryParseInstanceMethodDescriptor returns ffi argsDesc = tryParseGetInstanceFieldDescriptor returns ffi argsDesc

  tryParseInstanceMethodNoArgDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseInstanceMethodNoArgDescriptor returns ffiDesc@(FApp ffi [FStr _]) []
    = if ffi == "Instance"
        then jerror "Instance methods should have atleast one argument"
        else tryParseInstanceMethodDescriptor returns ffiDesc []
  tryParseInstanceMethodNoArgDescriptor returns ffi argsDesc = tryParseInstanceMethodDescriptor returns ffi argsDesc

  tryParseSetStaticFieldDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseSetStaticFieldDescriptor returns ffiDesc@(FApp ffi [FApp nativeTy [FStr cname], FStr fieldName]) argsDesc
    = if ffi == "SetStaticField" && nativeTy == "Class"
        then JSetStaticField cname fieldName
        else tryParseInstanceMethodNoArgDescriptor returns ffiDesc argsDesc
  tryParseSetStaticFieldDescriptor returns ffi argsDesc = tryParseInstanceMethodNoArgDescriptor returns ffi argsDesc

  tryParseStaticFieldDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseStaticFieldDescriptor returns ffiDesc@(FApp ffi [FApp nativeTy [FStr cname], FStr fieldName]) argsDesc
    = if ffi == "GetStaticField" && nativeTy == "Class"
        then JGetStaticField cname fieldName
        else tryParseSetStaticFieldDescriptor returns ffiDesc argsDesc
  tryParseStaticFieldDescriptor returns ffi argsDesc = tryParseSetStaticFieldDescriptor returns ffi argsDesc

  tryParseStaticMethodDescriptor : FDesc -> FDesc -> List (FDesc, LVar) -> JForeign
  tryParseStaticMethodDescriptor returns ffiDesc@(FApp ffi [FApp nativeTy [FStr cname], FStr fn]) argsDesc
    = if ffi == "Static"
        then JStatic cname fn
        else tryParseStaticFieldDescriptor returns ffiDesc argsDesc
  tryParseStaticMethodDescriptor returns ffi argsDesc = tryParseStaticFieldDescriptor returns ffi argsDesc

fdescFunctionArgDescriptor : FDesc -> List FieldTypeDescriptor
fdescFunctionArgDescriptor (FApp "JVM_FnBase" [_,ty]) = []
fdescFunctionArgDescriptor (FApp "JVM_FnIO" [_,ty]) = []
fdescFunctionArgDescriptor (FApp "JVM_FnT" [_,ty]) = fdescFunctionArgDescriptor ty
fdescFunctionArgDescriptor (FApp c [_,_, FCon "JVM_Unit",fn]) = []
fdescFunctionArgDescriptor (FApp "JVM_Fn" [_,_, ty,fn]) = fdescFieldDescriptor ty :: fdescFunctionArgDescriptor fn
fdescFunctionArgDescriptor _ = []

fdescFunctionRetDescriptor : FDesc -> TypeDescriptor
fdescFunctionRetDescriptor (FApp "JVM_FnBase" [_,ty]) = fdescTypeDescriptor ty
fdescFunctionRetDescriptor (FApp "JVM_FnIO" [_,ty]) = fdescTypeDescriptor ty
fdescFunctionRetDescriptor (FApp "JVM_FnT" [_,ty]) = fdescFunctionRetDescriptor ty
fdescFunctionRetDescriptor (FApp "JVM_Fn" [_,_,ty,fn]) = fdescFunctionRetDescriptor fn
fdescFunctionRetDescriptor desc = fdescTypeDescriptor desc

anewarray : FieldTypeDescriptor -> Asm ()
anewarray FieldTyDescByte          = Anewbytearray
anewarray FieldTyDescChar          = Anewchararray
anewarray FieldTyDescShort         = Anewshortarray
anewarray FieldTyDescBoolean       = Anewbooleanarray
anewarray FieldTyDescDouble        = Anewdoublearray
anewarray FieldTyDescFloat         = Anewfloatarray
anewarray FieldTyDescInt           = Anewintarray
anewarray FieldTyDescLong          = Anewlongarray
anewarray (FieldTyDescReference f) = Anewarray $ refTyClassName f

arrayStore : FieldTypeDescriptor -> Asm ()
arrayStore FieldTyDescByte = Bastore
arrayStore FieldTyDescChar = Castore
arrayStore FieldTyDescShort = Sastore
arrayStore FieldTyDescBoolean = Bastore
arrayStore FieldTyDescDouble = Dastore
arrayStore FieldTyDescFloat = Fastore
arrayStore FieldTyDescInt = Iastore
arrayStore FieldTyDescLong = Lastore
arrayStore (FieldTyDescReference ReferenceTypeDescriptor) = Aastore

arrayLoad : FieldTypeDescriptor -> Asm ()
arrayLoad FieldTyDescByte                                = Baload
arrayLoad FieldTyDescChar                                = Caload
arrayLoad FieldTyDescShort                               = Saload
arrayLoad FieldTyDescBoolean                             = Baload
arrayLoad FieldTyDescDouble                              = Daload
arrayLoad FieldTyDescFloat                               = Faload
arrayLoad FieldTyDescInt                                 = Iaload
arrayLoad FieldTyDescLong                                = Laload
arrayLoad (FieldTyDescReference ReferenceTypeDescriptor) = Aaload

typeDescToarrayElemDesc : TypeDescriptor -> FieldTypeDescriptor
typeDescToarrayElemDesc VoidDescriptor = jerror $ "An array cannot have 'void' elements"
typeDescToarrayElemDesc (FieldDescriptor desc) = desc

arrayDesc : String -> Nat -> String
arrayDesc cname dimensions =
  let arrayPrefix = cast $ replicate dimensions '['
  in arrayPrefix ++ cname

invokeDynamic : ClassName -> MethodName -> MethodName -> String -> String -> String -> String -> Asm ()
invokeDynamic implClassName implMethodName interfaceMethodName invokeDynamicDesc samDesc implMethodDesc instantiatedMethodDesc =
  let metafactoryHandle = MkHandle HInvokeStatic "java/lang/invoke/LambdaMetafactory" "metafactory" metafactoryDesc False
      implMethodHandle = MkHandle HInvokeStatic implClassName implMethodName implMethodDesc False
      metafactoryArgs = [ BsmArgGetType samDesc
                        , BsmArgHandle implMethodHandle
                        , BsmArgGetType instantiatedMethodDesc
                        ]
  in InvokeDynamic interfaceMethodName invokeDynamicDesc metafactoryHandle metafactoryArgs

createLambdaForThunk : JMethodName -> JMethodName -> List LVar -> (MethodName -> Asm ()) -> Asm ()
createLambdaForThunk caller targetFname args lambdaCode = do
  let nArgs = length args
  locTypes <- GetFunctionLocTypes
  (_, targetLocTys) <- getFunctionType targetFname
  let cname = jmethClsName caller
  lambdaIndex <- FreshLambdaIndex cname
  let implMethodName = sep "$" ["lambda", jmethName caller, show lambdaIndex]
  loadVars locTypes targetLocTys args
  let targetArgTys = if nArgs > 0 then getLocTy targetLocTys <$> (Loc . cast <$> [ 0 .. Nat.pred nArgs]) else []
  let invokeDynamicDesc = getInferredFunDesc targetArgTys (Ref thunkClass)
  let implMethodDesc = getInferredFunDesc targetArgTys (Ref "java/lang/Object")
  let samDesc = "()" ++ classSig "java/lang/Object"
  let instantiatedMethodDesc = samDesc
  invokeDynamic cname implMethodName "call" invokeDynamicDesc samDesc implMethodDesc instantiatedMethodDesc
  lambdaCode implMethodName

createLambdaForJavaFunction : JMethodName
                           -> JMethodName
                           -> List FieldTypeDescriptor
                           -> TypeDescriptor
                           -> List FieldTypeDescriptor
                           -> TypeDescriptor
                           -> (MethodName -> Asm ())
                           -> Asm ()
createLambdaForJavaFunction caller (MkJMethodName interfaceName interfaceMethodName) interfaceMethodArgs interfaceMethodReturns implMethodArgs implMethodReturns lambdaCode = do
  let cname = jmethClsName caller
  lambdaIndex <- FreshLambdaIndex cname
  let implMethodName = sep "$" ["lambda", jmethName caller, show lambdaIndex]
  -- takes idris function as input, returns an instance of Java interface
  let invokeDynamicDesc = "(Ljava/lang/Object;)" ++ classSig interfaceName
  let samDesc = asmMethodDesc $ MkMethodDescriptor interfaceMethodArgs interfaceMethodReturns
  let objectDesc = FieldTyDescReference $ ClassDesc "java/lang/Object"
  let implMethodDesc = asmMethodDesc $
    -- first objectDesc is for idris function capture
    MkMethodDescriptor (objectDesc :: implMethodArgs) implMethodReturns
  let instantiatedMethodDesc = asmMethodDesc $ MkMethodDescriptor implMethodArgs implMethodReturns
  invokeDynamic cname implMethodName interfaceMethodName invokeDynamicDesc samDesc implMethodDesc instantiatedMethodDesc
  lambdaCode implMethodName

createWrapperForThunkLambda : JMethodName -> ClassName -> MethodName -> List LVar -> Asm ()
createWrapperForThunkLambda fname@(MkJMethodName cname mname) callerCname lambdaMethodName args = do
  (targetRetTy, targetLocTys) <- getFunctionType fname
  let nArgs = the Int $ cast $ length args
  let argNums = if nArgs > 0 then [ 0 .. pred nArgs] else []
  let syntheticMethodArgs = Loc <$> argNums
  let targetArgTys = getLocTy targetLocTys <$> syntheticMethodArgs
  let syntheticMethodArgTys = SortedMap.fromList $ List.zip argNums targetArgTys
  let implMethodDesc = getInferredFunDesc targetArgTys (Ref "java/lang/Object")
  let targetMethodDesc = getInferredFunDesc targetArgTys targetRetTy
  CreateMethod [Private, Static, Synthetic] callerCname lambdaMethodName implMethodDesc Nothing Nothing [] []
  MethodCodeStart
  loadVars syntheticMethodArgTys targetLocTys syntheticMethodArgs
  InvokeMethod InvokeStatic cname mname targetMethodDesc False
  box targetRetTy
  Areturn
  MaxStackAndLocal (-1) (-1)
  MethodCodeEnd

createExceptionLambdaWrapper : ClassName -> MethodName -> Nat -> Asm () -> Asm ()
createExceptionLambdaWrapper callerCname lambdaMethodName nArgs body = do
  let desc = sig nArgs
  CreateMethod [Private, Static, Synthetic] callerCname lambdaMethodName desc Nothing Nothing [] []
  MethodCodeStart
  body
  Areturn
  MaxStackAndLocal (-1) (-1)
  MethodCodeEnd

createWrapperForJavaLambda : ClassName -> MethodName -> List FieldTypeDescriptor -> TypeDescriptor -> Asm ()
createWrapperForJavaLambda callerCname lambdaMethodName argDescs returnDesc = do
    let descriptor = asmMethodDesc $ MkMethodDescriptor locDescs returnDesc
    CreateMethod [Private, Static, Synthetic] callerCname lambdaMethodName descriptor Nothing Nothing [] []
    MethodCodeStart
    when (isNil argDescs) $ do
      Aconstnull
      Dup
    (applyRetTy, applyLocTys) <- applyFnType
    let applyArgTys = take 2 (values applyLocTys)
    let (applyArg0 :: _ :: _) = applyArgTys
    loadVar locTys inferredObjectType applyArg0 (Loc 0)
    applyArgs 1 argDescs
    if (isThunk applyRetTy || isObject applyRetTy) then do
        InvokeMethod InvokeStatic (rtClass "Runtime") "unwrap" (sig 1) False
        cgCast inferredObjectType (typeDescriptorToInferredType returnDesc)
    else
        cgCast applyRetTy (typeDescriptorToInferredType returnDesc)
    javaReturn returnDesc
    MaxStackAndLocal (-1) (-1)
    MethodCodeEnd
  where
    idrisApplyMethod : JMethodName
    idrisApplyMethod = jname "{APPLY_0}"

    locDescs : List FieldTypeDescriptor
    locDescs = (FieldTyDescReference $ ClassDesc "java/lang/Object") :: argDescs

    locTys : InferredTypeStore
    locTys = SortedMap.fromList $ List.zip argVars $ fieldTypeDescriptorToInferredType <$> locDescs where
        argVars : List Int
        argVars = [0 .. (pred . cast $ length locDescs)]

    applyFnClassName : String
    applyFnClassName = jmethClsName idrisApplyMethod

    applyFnMethodName : String
    applyFnMethodName = jmethName idrisApplyMethod

    applyFnType : Asm (InferredType, InferredTypeStore)
    applyFnType = getFunctionType idrisApplyMethod

    callIoType : Asm (InferredType, InferredTypeStore)
    callIoType = getFunctionType (jname "call__IO")

    applyArgs : Nat -> List FieldTypeDescriptor -> Asm ()
    applyArgs (S Z) [] = do
        (callIoRetTy, callIoLocTys) <- callIoType
        let callIoArgTys = take 3 $ (values callIoLocTys)
        let callIoDesc = getInferredFunDesc callIoArgTys callIoRetTy
        InvokeMethod InvokeStatic "main/Main" "call__IO" callIoDesc False
    applyArgs index (argDesc :: argDescs) = do
      (applyRetTy, applyArgVarAndTys) <- applyFnType
      let applyLocTys = SortedMap.values applyArgVarAndTys
      let applyArgTys = take 2 applyLocTys
      let (_ :: applyArg1 :: _) = applyArgTys
      loadVar locTys (fieldTypeDescriptorToInferredType argDesc) applyArg1 (Loc $ cast index)
      let applyFnDesc = getInferredFunDesc applyArgTys applyRetTy
      InvokeMethod InvokeStatic applyFnClassName applyFnMethodName applyFnDesc False
      applyArgs (index + 1) argDescs
    applyArgs _ _ = pure ()

createThunk : JMethodName -> JMethodName -> List LVar -> Asm ()
createThunk caller@(MkJMethodName callerCname _) fname args = do
  let lambdaCode =
    \lambdaMethodName =>
      Subroutine $ createWrapperForThunkLambda fname callerCname lambdaMethodName args
  createLambdaForThunk caller fname args lambdaCode

createExceptionHandlerThunk : JMethodName -> JMethodName -> List LVar -> Asm () -> Asm ()
createExceptionHandlerThunk caller@(MkJMethodName callerCname _) targetFname args body = do
  let nArgs = List.length args
  let lambdaCode = \lambdaMethodName => Subroutine $ createExceptionLambdaWrapper callerCname lambdaMethodName nArgs body
  createLambdaForThunk caller targetFname args lambdaCode

createJvmFunctionalObject : LVar -> JMethodName -> JMethodName -> FDesc -> FDesc -> Asm ()
createJvmFunctionalObject idrisFunction caller@(MkJMethodName callerCname _) interfaceMethod interfaceFnTy lambdaTy  = do
  let implMethodArgDescs = fdescFunctionArgDescriptor lambdaTy
  let interfaceMethodArgDescs = fdescFunctionArgDescriptor interfaceFnTy
  let implMethodReturnDesc = fdescFunctionRetDescriptor lambdaTy
  let interfaceMethodReturnDesc = fdescFunctionRetDescriptor interfaceFnTy
  let lambdaCode = \implMethodName => Subroutine $ createWrapperForJavaLambda callerCname implMethodName implMethodArgDescs implMethodReturnDesc
  aload $ locIndex idrisFunction
  createLambdaForJavaFunction caller interfaceMethod interfaceMethodArgDescs interfaceMethodReturnDesc implMethodArgDescs implMethodReturnDesc lambdaCode

createWrapperForThunkParLambda : JMethodName -> ClassName -> MethodName -> Nat -> Asm ()
createWrapperForThunkParLambda fname@(MkJMethodName cname mname) callerCname lambdaMethodName nArgs = do
  (targetRetTy, targetLocTys) <- getFunctionType fname

  let argNums = the (List Int) $ if nArgs > 0 then [0 .. Prelude.pred $ cast nArgs] else []
  let syntheticMethodArgs = Loc <$> argNums
  let targetArgTys = getLocTy targetLocTys <$> syntheticMethodArgs
  let syntheticMethodArgTys = SortedMap.fromList $ List.zip argNums targetArgTys
  let implMethodDesc = getInferredFunDesc targetArgTys (Ref "java/lang/Object")
  let targetMethodDesc = getInferredFunDesc targetArgTys targetRetTy
  CreateMethod [Private, Static, Synthetic] callerCname lambdaMethodName implMethodDesc Nothing Nothing [] []
  MethodCodeStart
  loadVars syntheticMethodArgTys targetLocTys syntheticMethodArgs
  InvokeMethod InvokeStatic cname mname targetMethodDesc False -- invoke the target method
  box targetRetTy
  Astore 1
  Aload 1
  InstanceOf idrisObjectType
  CreateLabel "elseLabel"
  Ifeq "elseLabel"
  Aload 1
  cgCast targetRetTy inferredIdrisObjectType
  InvokeMethod InvokeStatic cname mname targetMethodDesc False
  box targetRetTy
  Areturn
  LabelStart "elseLabel"
  Frame FAppend 1 ["java/lang/Object"] 0 []
  Aload 1
  Areturn
  MaxStackAndLocal (-1) (-1)
  MethodCodeEnd

createParThunk : JMethodName -> JMethodName -> List LVar -> Asm ()
createParThunk caller@(MkJMethodName callerCname _) fname args = do
  let nArgs = List.length args
  let lambdaCode = \lambdaMethodName => Subroutine $ createWrapperForThunkParLambda fname callerCname lambdaMethodName nArgs
  createLambdaForThunk caller fname args lambdaCode


text:
module Cic

import Bits
import Synchronous
import Unsigned

import Data.Bits

%access export
%default total

-- See Hogenauer's 1981 paper "An Economical Class of Digital Filters for
-- Decimation and Interpolation". All the equations are referenced against this
-- paper

--------------------------------------------------------------------------------
-- CIC subcircuits
--------------------------------------------------------------------------------

||| Prune an `Unsigned n` down to a smaller `Unsigned m`
prune : Unsigned n -> Unsigned m
prune {n} {m} x = saturate . cast $
  shiftR (cast . cast {to=Double} $ cast x {to=Integer}) -- Horrible!
         (cast $ n `minus` m)

||| Extend an `Unsigned n` up to a larger `Unsigned m`
extend : Unsigned n -> Unsigned m
extend = saturate . cast

||| Integrator circuit
partial
integrate : Stream (Unsigned n) -> Stream (Unsigned n)
integrate xs = liftA2 (addWrap) xs (delay 0 $ integrate xs)

||| Boolean true every Rth cycle, starting at first cycle
everyR : (r: Nat) -> Stream Bool
everyR   Z    = pure False
everyR (S j) = map (\a=>modNatNZ a (S j) SIsNotZ == 0) $ counterFrom 0

||| Downsampler circuit
downsample : (r: Nat) -> Stream a -> Stream (Maybe a)
downsample r = zipWith (\e, x=>if e then Just x else Nothing) (everyR r)

||| Comb filter circuit
comb : (m : Nat) -> Stream (Maybe (Unsigned n)) -> Stream (Maybe (Unsigned n))
comb _ xs = map (\(a,b)=>map (`minusWrap` b) a) $
            zip xs (regMaybe 0 xs) -- TODO Delay by m... and get

--------------------------------------------------------------------------------
-- Wordlength calculations
--------------------------------------------------------------------------------

||| Recursive definition of a binomial coefficient
nChooseK : (n: Nat) -> (k: Nat) -> Nat
nChooseK n Z = 1
nChooseK Z (S k) = 0
nChooseK (S n) (S k) = if k>n then 0 else
                       nChooseK n k + nChooseK n (S k)

||| Helper to divide two `Nat`s safely, returning zero for division by zero
||| (fight me, mathematicians)
divNatOrZero : Nat -> Nat -> Nat
divNatOrZero k Z = Z
divNatOrZero k (S j) = divNatNZ k (S j) SIsNotZ

parameters (r, n, m : Nat)

  ||| Partial system function, $h_j(k)$ (Eq. 9b)
  hjk : (j, k : Nat) -> Integer
  hjk j k = case j <= n of
    True  => sum $ map (\l => pow (-1) l * cast (
                                (nChooseK n l) *
                                (nChooseK ((n `minus` j)+(k `minus` r*m*l)) (k `minus` r*m*l)))
                       ) [0..(divNatOrZero k (r*m))]
    False => pow (-1) k * cast (nChooseK (minus (2*n+1) j) k)

  ||| Variance error gain for stage j, $F(j)$ (Eq. 16b)
  fj : (j : Nat) -> Double
  fj j = case j == (2*n+1) of
      True  => 1.0
      False => sqrt . cast . sum $ map (\k=>pow (hjk j k) 2) [0..((r*m `minus` 1) * n + j `minus` 1)]

  ||| Max unpruned wordlength, $B_{max}$ (Eq 12)
  bmax : (bin : Nat) -> Nat
  bmax bin = bin + clog2 (pow (r*m) n)

  ||| Error at output due to final rounding/truncation, $E_{2N+1}$ (Eq. 12)
  eT2n1 : (bin, bout : Nat) -> Integer
  eT2n1 bin bout = pow 2 $ bmax bin `minus` bout

  ||| Variance at output due to final rounding/truncation, $\sigma_T_{2N+1}$ (Eq. 14)
  sigmaT2n1 : (bin, bout : Nat) -> Double
  sigmaT2n1 bin bout = sqrt $ cast (pow  (eT2n1 bin bout) 2) / 12.0

  ||| Bits to prune at stage j, $B_j$ (Eq. 21).
  ||| We use log laws to avoid errors with an integer implementation of log2
  bj : (bin, bout, j : Nat) -> Nat
  bj bin bout j = flog2Approx $ (sigmaT2n1 bin bout) * (sqrt $ 6.0 / (cast n)) / fj j

  ||| Bits to keep at stage j
  cicAccPruned : (bin, bout, j : Nat) -> Nat
  cicAccPruned bin bout j = if j==0 then bmax bin else
                                  if j>=(2*n+1) then bout else
                                  bmax bin `minus` bj bin bout j

--------------------------------------------------------------------------------
-- CIC decimator
--------------------------------------------------------------------------------

  ||| Recursive integrator chain
  partial --Because of integrate
  cicDecimateRecI : (bin, bout, j : Nat)
    -> Stream (Unsigned (cicAccPruned bin bout 0))
    -> Stream (Unsigned (cicAccPruned bin bout j))
  cicDecimateRecI bin bout  Z    = id
  cicDecimateRecI bin bout (S j) = map prune . integrate .
                                   cicDecimateRecI bin bout j

  ||| Recursive comb filter chain
  cicDecimateRecC : (bin, bout, j : Nat)
    -> Stream (Maybe (Unsigned (cicAccPruned bin bout n)))
    -> Stream (Maybe (Unsigned (cicAccPruned bin bout (j+n))))
  cicDecimateRecC bin bout  Z    = id
  cicDecimateRecC bin bout (S j) = map (map prune) . comb m .
                                   cicDecimateRecC bin bout j
  ||| CIC decimator circuit
  partial --Because of integrate
  cicDecimate : Stream (Unsigned bin) -> Stream (Maybe (Unsigned bout))
  cicDecimate {bin} {bout} =
    map (map prune) .                        -- Final truncation, after
    cicDecimateRecC bin bout n .             -- Recursive comb steps, after
    downsample r .                           -- Downsample, after
    cicDecimateRecI bin bout n .             -- Recursive integrate steps, after
    map (extend {m=cicAccPruned bin bout 0}) -- Input extend

-- TODO Is it worth proving that cicAccPruned bin bout (2*n+1)) == bout?

||| Example of calculating pruning for Hogenauer's design example (Section IV. D)
mainBj : IO ()
mainBj = print $ map (bj 25 4 1 16 16) [1..8]

||| Example of simulating `cicDecimate`
partial
mainSim : IO ()
mainSim = do let dut = cicDecimate {bin=8} {bout=8} 3 3 1
             let inp = map (\t=> saturate {n=8} . cast $
                                 sin (t*2*pi/10.0) * 127 + 127 )
                       $ counterFrom 0 {ty=Double}
             let out = take 40 $ simulate dut inp
             putStrLn . show $ zip (take 40 inp) out


text:
||| Default configurations for the LSP server implementation capabilities.
|||
||| (C) The Idris Community, 2021
module Server.Capabilities

import Language.JSON
import Language.LSP.Message

%default total

syncOptions : TextDocumentSyncOptions
syncOptions = MkTextDocumentSyncOptions { openClose = Just True
                                        , change = Just Incremental
                                        , willSave = Nothing
                                        , willSaveWaitUntil = Nothing
                                        , save = Just (make (MkSaveOptions (Just True)))
                                        }

semanticTokensLegend : SemanticTokensLegend
semanticTokensLegend = MkSemanticTokensLegend
  -- ``type``: type constructors       ==> ``type``
  -- ``function``: defined functions   ==> ``function``
  -- ``data``: data constructors       ==> ``enumMember``
  -- ``bound``: bound variables, or    ==> ``variable``
  -- ``keyword``                       ==> ``keyword``
  ["type", "function", "enumMember", "variable", "keyword"]
  []

semanticTokensOptions : SemanticTokensOptions
semanticTokensOptions = MkSemanticTokensOptions
  semanticTokensLegend
  (Just (make False))
  (Just (make True))

||| Default server capabilities to be sent to clients during the initialization protocol.
export
serverCapabilities : ServerCapabilities
serverCapabilities =
  MkServerCapabilities { textDocumentSync                 = Just (make syncOptions)
                       , completionProvider               = Just (MkCompletionOptions Nothing (Just []) (Just []) Nothing)
                       , hoverProvider                    = Just (make True)
                       , signatureHelpProvider            = Just (MkSignatureHelpOptions Nothing Nothing Nothing)
                       , definitionProvider               = Just (make (MkDefinitionOptions
                                                                          (Just False)))
                       , declarationProvider              = Just (make False)
                       , typeDefinitionProvider           = Just (make False)
                       , implementationProvider           = Just (make False)
                       , referencesProvider               = Just (make False)
                       , documentHighlightProvider        = Just (make False)
                       , documentSymbolProvider           = Just (make (MkDocumentSymbolOptions
                                                                          Nothing
                                                                          Nothing))
                       , codeActionProvider               = Just (make (MkCodeActionOptions
                                                                          Nothing
                                                                          Nothing
                                                                          (Just False)))
                       , codeLensProvider                 = Just (MkCodeLensOptions Nothing Nothing)
                       , documentLinkProvider             = Just (MkDocumentLinkOptions Nothing Nothing)
                       , colorProvider                    = Just (make False)
                       , documentFormattingProvider       = Just (make False)
                       , documentRangeFormattingProvider  = Just (make False)
                       , documentOnTypeFormattingProvider = Nothing
                       , renameProvider                   = Just (make False)
                       , foldingRangeProvider             = Just (make False)
                       , executeCommandProvider           = Just (MkExecuteCommandOptions Nothing [])
                       , selectionRangeProvider           = Just (make False)
                       , linkedEditingRangeProvider       = Just (make False)
                       , callHierarchyProvider            = Just (make False)
                       , semanticTokensProvider           = Just (make semanticTokensOptions)
                       , monikerProvider                  = Just (make False)
                       , workspaceSymbolProvider          = Just (make False)
                       , workspace                        = Just (MkWorkspaceServerCapabilities
                                                                 (Just (MkWorkspaceFoldersServerCapabilities (Just False) Nothing))
                                                                 (Just (MkFileOperationsServerCapabilities Nothing Nothing Nothing Nothing Nothing Nothing)))
                       , experimental                     = Nothing
                       }

||| Server information to be sent to clients during the initialization protocol.
export
serverInfo : ServerInfo
serverInfo = MkServerInfo { name = "idris2-lsp", version = Just "0.1" }


text:
module HtmlStyle

import public Js.VirtualDom
import Js.Html

%access export

private
listStyleToStyle : List Style -> Style
listStyleToStyle [] = Nil
listStyleToStyle (x::xs) = x :: listStyleToStyle xs

private
pixels : Double -> String
pixels x = show x ++ "px"

height : Double -> Style
height x = mkStyle "height" (pixels x)

width: Double -> Style
width x = mkStyle "width" (pixels x)

margin : Double -> Style
margin x = mkStyle "margin" (pixels x)

fill : String -> Style
fill x = mkStyle "fill" x

data Transform = MkTransform String

Show Transform where
  show (MkTransform s) = s

Semigroup Transform where
  (<+>) (MkTransform a) (MkTransform b) = MkTransform (a ++ b)

Monoid Transform where
  neutral = MkTransform ""

translate : Double -> Double -> Transform
translate x y =
  MkTransform $ "translate(" ++ pixels x ++ "," ++ pixels y ++ ")"

scale : Double -> Double -> Transform
scale x y =
  MkTransform $ "scale(" ++ show x ++ "," ++ show y ++ ")"

transform : Transform -> Style
transform (MkTransform x) = mkStyle "transform" x

public export
data FlexDirection = Row | Column

flexDirectionToString : FlexDirection -> String
flexDirectionToString Row = "row"
flexDirectionToString Column = "column"

export
data FlexOption = MkFlexOption Style

export
direction : FlexDirection -> FlexOption
direction x = MkFlexOption $  mkStyle "flex-direction" (flexDirectionToString x)

wrap : FlexOption
wrap = MkFlexOption $ mkStyle "flex-wrap" "wrap"

flex : List FlexOption -> Style
flex opts =
  [mkStyle "display" "flex", listStyleToStyle $ map (\(MkFlexOption x) => x) opts]

public export
data Position = Static | Fixed Double Double

position : Position -> Style
position Static = mkStyle "position" "static"
position (Fixed x y) = [mkStyle "position" "fixed", mkStyle "left" (pixels x), mkStyle "top" (pixels y)]

zIndex : Double -> Style
zIndex x = mkStyle "z-index" (show x)

backgroundColor : String -> Style
backgroundColor = mkStyle "background-color"

namespace UserSelect

  public export
  data UserSelectType = Auto | None | Text | All

  userSelect : UserSelectType -> Style
  userSelect Auto = mkStyle "user-select" "auto"
  userSelect None = mkStyle "user-select" "none"
  userSelect Text = mkStyle "user-select" "text"
  userSelect All = mkStyle "user-select" "all"
{-

padding : Double -> Attribute a f g
padding x = CSSAttribute "padding" (DynConst $ pixels x)

paddingTop : Double -> Attribute a f g
paddingTop x = CSSAttribute "paddingTop" (DynConst $ pixels x)

paddingTopF : (a -> Double) -> Attribute a b
paddingTopF f = CSSAttribute "paddingTop" (DynA $ \(_**x) => pixels $ f x)

data BoxShadowOption : (a:Type) -> (a->Type) -> (a->Type) -> Type where
  Blur : Dyn (DPair a f) Double -> BoxShadowOption a f g
  HShadow : Dyn (DPair a f) Double -> BoxShadowOption a f g
  VShadow : Dyn (DPair a f) Double -> BoxShadowOption a f g

blur : Double -> BoxShadowOption a f g
blur x = Blur $ DynConst x

hShadow : Double -> BoxShadowOption a f g
hShadow x = HShadow $ DynConst x

vShadow : Double -> BoxShadowOption a f g
vShadow x = VShadow $ DynConst x

private
record BoxShadowArguments (a:Type) (f : a->Type) where
  constructor MkBoxShadowArguments
  hShadow : Dyn (DPair a f) Double
  vShadow : Dyn (DPair a f) Double
  blur : Dyn (DPair a f) Double
  spread : Dyn (DPair a f) Double
  color : Dyn (DPair a f) String

private
boxShadowOptionsToArgs : List (BoxShadowOption a f g) -> BoxShadowArguments a f
boxShadowOptionsToArgs x =
  foldl opt (MkBoxShadowArguments (pure 0) (pure 0) (pure 0) (pure 0) (pure "black")) x
  where
    opt : BoxShadowArguments a f -> BoxShadowOption a f g -> BoxShadowArguments a f
    opt y (Blur x) = record{blur = x} y
    opt y (HShadow x) = record{hShadow = x} y
    opt y (VShadow x) = record{vShadow = x} y

private
boxShadowArgsToString : Double -> Double -> Double -> Double -> String -> String
boxShadowArgsToString hsh vsh blr spr clr =
  unwords
      [pixels hsh, pixels vsh, pixels blr, pixels spr, clr]

boxShadow :  List (BoxShadowOption a f g) -> Attribute a f g
boxShadow {a} {f} x =
  CSSAttribute "box-shadow" (boxShadowArgsToString <$> hShadow args <*> vShadow args <*> blur args <*> spread args <*> color args)
  where
    args : BoxShadowArguments a f
    args = boxShadowOptionsToArgs x

  -}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
||| THIS WORKS
data MyNat = A | Next MyNat

cycABC: MyNat -> MyNat
cycABC A                    = Next A
cycABC (Next A)             = Next (Next A)
cycABC (Next(Next A))       = A
cycABC (Next(Next(Next x))) = Next(Next(Next x))

cycACB: MyNat -> MyNat
cycACB A                    = Next(Next A)
cycACB (Next A)             = A
cycACB (Next(Next A))       = Next A
cycACB (Next(Next(Next x))) = Next(Next(Next x))

invPrfMyNat : (x:MyNat) -> cycABC ( cycACB x ) = x
invPrfMyNat A = Refl

||| THIS WORKS
cyc012: Nat -> Nat
cyc012 Z                    = S Z
cyc012 (S Z)                = S (S Z)
cyc012 (S(S Z))             = Z
cyc012 (S(S(S x)))          = S(S(S x))

cyc021: Nat -> Nat
cyc021 Z                    = S(S Z)
cyc021 (S Z)                = Z
cyc021 (S(S Z))             = S Z
cyc021 (S(S(S x)))          = S(S(S x))

invPrfNat : (x:Nat) -> cyc012 ( cyc021 x ) = x
invPrfNat Z = Refl

||| Map between

abc120: MyNat -> Nat
abc120 A                    = S Z
abc120 (Next A)             = S (S Z)
abc120 (Next(Next A))       = Z
abc120 (Next(Next(Next x))) = S(S(S (abc120 x)))

iabc120: Nat -> MyNat
iabc120 Z                    = Next(Next A)
iabc120 (S Z)                = A
iabc120 (S(S Z))             = Next A
iabc120 (S(S(S x)))          = Next(Next(Next (iabc120 x)))

invPrfNat : (x:MyNat) -> iabc120 ( abc120 x ) = x
invPrfNat A = Refl

||| THIS DOES WORK, how unexpected.
cyc01: Nat -> Nat
cyc01 Z                    = S Z
cyc01 (S Z)                = Z
cyc01 (S(S x))             = S(S(x))

invPrfNat2 : (x:Nat) -> cyc01 ( cyc01 x ) = x
invPrfNat2 Z = Refl

max_stars_repo_name: algeboy/BlackBoxType

max_issues_repo_name: algeboy/BlackBoxType

max_forks_repo_name: algeboy/BlackBoxType


text:
data Elem : a -> List a -> Type where
  Here : Elem x (x :: xs)
  There : Elem x xs -> Elem x (y :: xs)

data Last : List a -> a -> Type where
  LastOne : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

not_in_nil : Last [] value -> Void
not_in_nil LastOne impossible
not_in_nil (LastCons _) impossible

not_last_one : (contra : (value = x) -> Void) -> Last [x] value -> Void
not_last_one contra LastOne = contra Refl
not_last_one _ (LastCons LastOne) impossible
not_last_one _ (LastCons (LastCons _)) impossible

not_last_cons : (contra : Last (x :: xs) value -> Void) ->
                   Last (y :: (x :: xs)) value -> Void
not_last_cons contra (LastCons prf) = contra prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No not_in_nil
isLast [x] value = case decEq value x of
                        (Yes Refl) => Yes LastOne
                        (No contra) => No (not_last_one contra)
isLast (y :: (x :: xs)) value = case isLast (x :: xs) value of
                                     (Yes prf) => Yes (LastCons prf)
                                     (No contra) => No (not_last_cons contra)


text:
module Lambdapants.Term.Parser

import Lambdapants.Term
import Lightyear
import Lightyear.Char
import Lightyear.Strings

export
symbol : Parser String
symbol = pack <$> some (alphaNum <|> char '_')

export
lambda : (body : Parser Term) -> Parser Term
lambda term = do
  char '\\'
  var  <- symbol
  char '.'
  body <- term
  pure (Lam var body)

mutual
  export appl : Parser Term
  appl = do
    terms <- some (spaces *> expr)
    pure (foldl1 App terms)
  expr : Parser Term
  expr = map Var symbol  -- x
    <|>| lambda appl     -- \x.M
    <|>| parens appl     -- (M)

export
term : Parser Term
term = appl <* spaces <* eof


text:
module Erlang.Show

import Erlang.Conversion
import Erlang.IO
import Erlang.Types

%default total

showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

export
Show ErlTerm where
  show _ = "<Erlang Term>"

export
Show ErlPid where
  show x =
    let MkCharlist str = erlUnsafeCall ErlCharlist "erlang" "pid_to_list" [x]
    in "#Pid" ++ str

export
Show ErlReference where
  show x =
    let MkCharlist str = erlUnsafeCall ErlCharlist "erlang" "ref_to_list" [x]
    in str

export
Show ErlPort where
  show x =
    let MkCharlist str = erlUnsafeCall ErlCharlist "erlang" "port_to_list" [x]
    in str

export
Show ErlAtom where
  show (MkAtom x) = "'" ++ x ++ "'"

export
Show ErlCharlist where
  show xs = show (erlUnsafeCast (List Int) xs)

export
Show ErlNil where
  show [] = "[]"

export
(Show a, Show b) => Show (ErlCons a b) where
  show (x :: y) = "[" ++ show x ++ " | " ++ show y ++ "]"

export
Show (ErlList []) where
  show [] = "[]"

export
(Show x, Show (ErlList xs)) => Show (ErlList (x :: xs)) where
  show (x :: xs) = "[" ++ show x ++ " | " ++ show xs ++ "]"

export
Show ErlTuple0 where
  show MkTuple0 = "{}"

export
Show a => Show (ErlTuple1 a) where
  show (MkTuple1 x1) =
    "{" ++ showSep ", " [show x1] ++ "}"

export
(Show a, Show b) => Show (ErlTuple2 a b) where
  show (MkTuple2 x1 x2) =
    "{" ++ showSep ", " [show x1, show x2] ++ "}"

export
(Show a, Show b, Show c) => Show (ErlTuple3 a b c) where
  show (MkTuple3 x1 x2 x3) =
    "{" ++ showSep ", " [show x1, show x2, show x3] ++ "}"

export
(Show a, Show b, Show c, Show d) => Show (ErlTuple4 a b c d) where
  show (MkTuple4 x1 x2 x3 x4) =
    "{" ++ showSep ", " [show x1, show x2, show x3, show x4] ++ "}"

export
(Show a, Show b, Show c, Show d, Show e) => Show (ErlTuple5 a b c d e) where
  show (MkTuple5 x1 x2 x3 x4 x5) =
    "{" ++ showSep ", " [show x1, show x2, show x3, show x4, show x5] ++ "}"

export
Show (ErlMapSubset xs) where
  show _ = "<Erlang Map>" -- TODO: Implement


text:
module Verified.Functor.Either

import Verified.Functor

instance VerifiedFunctor (Either e) where
  functorIdentity (Left _) = Refl
  functorIdentity (Right _) = Refl
  functorComposition (Left _) g1 g2 = Refl
  functorComposition (Right _) g1 g2 = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Chapter6

import Data.Vect

%default total

-- type synonyms

Position : Type
Position = (Double, Double)

tri : Vect 3 Position
tri = [(0.0, 0.0), (1.0, 2.0), (-23.22, -11.089)]

-- type-level functions
-- type-level functions are merely functions that return a Type

-- defining functions with a variable number of arguments

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:
module Main

import NonDTRealizedFunction

-- Realized incrementer
incrementer : Int -> Int
incrementer = (+1)
incrementer_attrs : NonDTRealizedAttributes
incrementer_attrs = MkNonDTRealizedAttributes (MkCosts 1 1 1) 1
rlz_incrementer : NonDTRealizedFunction (Int -> Int)
rlz_incrementer = MkNonDTRealizedFunction incrementer incrementer_attrs

-- Realized twicer
twicer : Int -> Int
twicer = (*2)
twicer_attrs : NonDTRealizedAttributes
twicer_attrs = MkNonDTRealizedAttributes (MkCosts 2 2 2) 0.9
rlz_twicer : NonDTRealizedFunction (Int -> Int)
rlz_twicer = MkNonDTRealizedFunction twicer twicer_attrs

-- Realized (twicer . incrementer)
rlz_composition : NonDTRealizedFunction (Int -> Int)
rlz_composition = compose rlz_twicer rlz_incrementer

-- Simple test, result should be (3+1)*2 = 8
rslt : Int
rslt = apply rlz_composition 3

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
||| How to replace things.
|||
||| Module    : Substitution.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.DeBruijn.Substitution

import Decidable.Equality

import Data.DPair

import Toolkit.Decidable.Informative

import Toolkit.Data.List.AtIndex
import Toolkit.Data.DList
import Toolkit.Data.DList.AtIndex

import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

%default total

namespace General
  public export
  interface Rename type term
         => Substitute (type : Type)
                       (term : List type -> type -> Type)
                             | term
    where

      subst : {old, new : List type}
           -> (f : {ty  : type}
                       -> IsVar old ty
                       -> term  new ty)
           -> ({ty : type}
                  -> term old ty
                  -> term new ty)

namespace Single
  %inline
  apply : {type : Type}
       -> {term : List type -> type -> Type}
       -> Rename type term
       => {ctxt   : List type}
       -> {typeA  : type}
       -> {typeB  : type}
       -> (this   : term   ctxt    typeB)
       -> (idx    : IsVar (ctxt += typeB) typeA)
                 -> term   ctxt           typeA
  apply this (V Z Here) = this
  apply this (V (S pos) (There later)) = embed (V pos later)

  export
  subst : {type : Type}
       -> {term : List type -> type -> Type}
       -> Rename type term
       => Substitute type term
       => {ctxt          : List type}
       -> {typeA         : type}
       -> {typeB         : type}
       -> (this          : term  ctxt           typeB)
       -> (inThis        : term (ctxt += typeB) typeA)
                        -> term  ctxt           typeA
  subst {ctxt} {typeA} {typeB} this inThis
    = General.subst (apply this) inThis

namespace Double

  %inline
  public export
  apply : {type : Type}
       -> {term : List type -> type -> Type}
       -> Rename type term
       => {ctxt          : List type}
       -> {typeA, typeB, typeC : type}
       -> (this    : term    ctxt                     typeA)
       -> (andThis : term    ctxt                     typeB)
       -> (idx     : IsVar ((ctxt += typeA) += typeB) typeC)
                  -> term    ctxt                     typeC
  apply this andThis pos = ?todo -- I know

  public export
  subst : {type : Type}
       -> {term : List type -> type -> Type}
       -> Rename type term
       => Substitute type term
       => {ctxt          : List type}
       -> {typeA, typeB, typeC : type}
       -> (this    : term  ctxt                     typeA)
       -> (andThis : term  ctxt                     typeB)
       -> (inThis  : term ((ctxt += typeA) += typeB) typeC)
                  -> term   ctxt                     typeC
  subst {ctxt} {typeA} {typeB} {typeC} this andThis inThis
    = General.subst (apply this andThis) inThis

-- [ 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 Test.MarkdownTest

import IdrTest.Test
import IdrTest.Expectation

import Markdown.Data
import Markdown

parserSpecs : List (String, String, Maybe Markdown)
parserSpecs =
  [ ( "Parse Header", "# test", Just $ Doc [Header 1 [Text " test"]] )
  , ( "Parse Short Paragraph", "test", Just $ Doc [Paragraph [Text "test"]] )
  , ( "Parse Paragraph", "test\n\n", Just $ Doc [Paragraph [Text "test"]] )
  , ( "Parse Two Paragraphs", "test\n\ntest2", Just $ Doc [Paragraph [Text "test"], Paragraph [Text "test2"]] )
  , ( "Parse Both", "# text\nand more\n\n", Just $ Doc [Header 1 [Text " text"], Paragraph [Text "and more"]] )
  , ( "Parse Bold then Italic", "## Well **hello** _there_", Just $ Doc [Header 2 [Text " Well ", Bold [Text "hello"], Text " ", Italics [Text "there"]]] )
  , ( "Parse a Link", "[here](http://example.com)", Just $ Doc [Paragraph [Link "here" "http://example.com"]] )
  , ( "Parse an Image", "![desc](http://example.com/img.svg)", Just $ Doc [Paragraph [Image "desc" "http://example.com/img.svg"]] )
  , ( "Parse HTML", "This is Super!", Just $ Doc [Paragraph [Text "This is ", Html "sup" [Text "Super"], Text "!"]] )
  , ( "Parse Non-HTML Brackets", "A  C <D E> >F< << >>", Just $ Doc [Paragraph [Text "A  C <D E> >F< << >>"]] )
  , ( "Parse Preformatted Text", "# Hello `john`\n```how\nare\nyou```", Just $ Doc [Header 1 [Text " Hello ", Pre "john"], Paragraph [CodeBlock "are\nyou" (Just "how")]] )
  , ( "Parse Spaced Start", "\n\n# test\n\n\n\n", Just $ Doc [Header 1 [Text " test"]] )
  ]

export
suite : Test
suite =
  let
    parserTests =
      map (\(name, text, result) =>
        test name (\_ => assertEq (parse text) result)
      ) parserSpecs
  in
  describe "Markdown"
    [ describe "Parser Specs" parserTests ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- --------------------------------------------------------------- [ GLang.idr ]
-- Module    : GLang.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| The original unadulterated version of the GRL.
module GRL.Lang.GLang

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty
import public GRL.Lang.GLang.Pretty

%access export
%default total

||| The original unadulterated version of the GRL.
data GLang : GTy -> Type where
    ||| Make a Goal node.
    MkGoal : String -> Maybe SValue -> GLang ELEM
    ||| Make a Soft Goal node.
    MkSoft : String -> Maybe SValue -> GLang ELEM
    ||| Make a Task node.
    MkTask : String -> Maybe SValue -> GLang ELEM
    ||| Make a resource node.
    MkRes  : String -> Maybe SValue -> GLang ELEM

    ||| Declare an impact relation.
    MkImpacts : CValue -> GLang ELEM -> GLang ELEM -> GLang INTENT

    ||| Declare a side-effect relation.
    MkEffects : CValue -> GLang ELEM -> GLang ELEM -> GLang INTENT

    ||| And decomposition relation.
    MkAnd : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT
    ||| XOR decomposition relation.
    MkXor : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT
    ||| IOR decomposition relation.
    MkIor : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT

-- --------------------------------------------------------------- [ Accessors ]

||| Obtain the node's title.
getElemTitle : GLang ELEM -> String
getElemTitle (MkGoal t _) = t
getElemTitle (MkSoft t _) = t
getElemTitle (MkTask t _) = t
getElemTitle (MkRes  t _) = t

-- ------------------------------------------------------------ [ Constructors ]

mkGoal : String -> GLang ELEM
mkGoal t = MkGoal t Nothing

mkSoft : String -> GLang ELEM
mkSoft t = MkSoft t Nothing

mkTask : String -> GLang ELEM
mkTask t = MkTask t Nothing

mkRes : String -> GLang ELEM
mkRes t = MkRes t Nothing

mkSatGoal : String -> SValue -> GLang ELEM
mkSatGoal t s = MkGoal t (Just s)

mkSatSoft : String -> SValue -> GLang ELEM
mkSatSoft t s = MkSoft t (Just s)

mkSatTask : String -> SValue -> GLang ELEM
mkSatTask t s = MkTask t (Just s)

mkSatRes : String -> SValue -> GLang ELEM
mkSatRes t s = MkRes t (Just s)

mkImpacts : CValue -> GLang ELEM -> GLang ELEM -> GLang INTENT
mkImpacts = MkImpacts

mkEffects : CValue -> GLang ELEM -> GLang ELEM -> GLang INTENT
mkEffects = MkEffects

mkAnd : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT
mkAnd = MkAnd

mkIor : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT
mkIor = MkIor

mkXor : GLang ELEM -> List (GLang ELEM) -> GLang STRUCT
mkXor = MkXor

-- --------------------------------------------------------------------- [ GRL ]

GRL GLang where
    mkElem (MkGoal s v) = Elem GOALty s v
    mkElem (MkSoft s v) = Elem SOFTty s v
    mkElem (MkTask s v) = Elem TASKty s v
    mkElem (MkRes  s v) = Elem RESty  s v

    mkIntent (MkImpacts c a b) = ILink IMPACTSty c (mkElem a) (mkElem b)
    mkIntent (MkEffects c a b) = ILink AFFECTSty c (mkElem a) (mkElem b)

    mkStruct (MkAnd a bs) = SLink ANDty (mkElem a) (map mkElem bs)
    mkStruct (MkXor a bs) = SLink XORty (mkElem a) (map mkElem bs)
    mkStruct (MkIor a bs) = SLink IORty (mkElem a) (map mkElem bs)

-- -------------------------------------------------------------------- [ Sort ]
private
record DeclGroups where
  constructor DGroup
  elems : List (GLang ELEM)
  intes : List (GLang INTENT)
  strus : List (GLang STRUCT)

private
getGroups : DList GTy GLang gs -> DeclGroups
getGroups xs = DList.foldr doGrouping (DGroup Nil Nil Nil) xs
  where
    doGrouping : GLang ty -> DeclGroups -> DeclGroups
    doGrouping {ty=ELEM}   x g = record {elems = x :: (elems g)} g
    doGrouping {ty=INTENT} x g = record {intes = x :: (intes g)} g
    doGrouping {ty=STRUCT} x g = record {strus = x :: (strus g)} g

private
recoverList : DeclGroups -> (xs ** DList GTy GLang xs)
recoverList (DGroup es is ss) =
       (_ ** (snd es')
          ++ (snd is')
          ++ (snd ss'))
  where
    es' : (xs ** DList GTy GLang xs)
    es' = fromList es

    is' : (ys ** DList GTy GLang ys)
    is' = fromList is

    ss' : (zs ** DList GTy GLang zs)
    ss' = fromList ss

groupDecls : DList GTy GLang gs -> (gs' ** DList GTy GLang gs')
groupDecls xs = recoverList $ getGroups xs

insertDecls : DList GTy GLang gs -> GModel -> GModel
insertDecls ds m = doInsert (getGroups ds) m
  where
    doInsert' : List (GLang ELEM)
             -> List (GLang STRUCT)
             -> List (GLang INTENT)
             -> GModel
             -> GModel
    doInsert' es ss is m = insertGroup es ss is m

    doInsert : DeclGroups -> GModel -> GModel
    doInsert (DGroup es is ss) m = doInsert' es ss is m

-- -------------------------------------------------------------------- [ Show ]

private
showElem : GLang ELEM -> String
showElem (MkGoal t s) = with List unwords ["[Goal", t, show s, "]"]
showElem (MkSoft t s) = with List unwords ["[Soft", t, show s, "]"]
showElem (MkTask t s) = with List unwords ["[Task", t, show s, "]"]
showElem (MkRes  t s) = with List unwords ["[Res" , t, show s, "]"]

private
showIntent : GLang INTENT -> String
showIntent (MkImpacts c a b) = "[Impacts " ++ show c ++ " " ++ showElem a ++ " " ++ showElem b ++ "]"
showIntent (MkEffects c a b) = "[Effects " ++ show c ++ " " ++ showElem a ++ " " ++ showElem b ++ "]"

private
showElems : List (GLang ELEM) -> String
showElems ys = "[" ++ (unwords $ intersperse "," (map showElem ys)) ++ "]"

private
showStruct : GLang STRUCT -> String
showStruct (MkAnd a bs) = "[And " ++ showElem a ++ " " ++ showElems bs ++ "]"
showStruct (MkXor a bs) = "[And " ++ showElem a ++ " " ++ showElems bs ++ "]"
showStruct (MkIor a bs) = "[And " ++ showElem a ++ " " ++ showElems bs ++ "]"

private
showLang : {ty : GTy} -> GLang ty -> String
showLang {ty=ELEM}   x = showElem x
showLang {ty=INTENT} x = showIntent x
showLang {ty=STRUCT} x = showStruct x

Show (GLang ty) where
    show x = showLang x

-- ---------------------------------------------------------------------- [ Eq ]

private
eqGLangE : GLang ELEM -> GLang ELEM -> Bool
eqGLangE (MkGoal x t) (MkGoal y u) = x == y && t == u
eqGLangE (MkSoft x t) (MkSoft y u) = x == y && t == u
eqGLangE (MkTask x t) (MkTask y u) = x == y && t == u
eqGLangE (MkRes  x t) (MkRes  y u) = x == y && t == u
eqGLangE _            _            = False

private
eqGLangI : GLang INTENT -> GLang INTENT -> Bool
eqGLangI (MkImpacts c a b) (MkImpacts d x y) = c == d && eqGLangE a x && eqGLangE b y
eqGLangI (MkEffects c a b) (MkEffects d x y) = c == d && eqGLangE a x && eqGLangE b y
eqGLangI _                 _                 = False

mutual
  private
  eqGLangS : GLang STRUCT -> GLang STRUCT -> Bool
  eqGLangS (MkAnd a as) (MkAnd b bs) = eqGLangE a b && eqGLangList as bs
  eqGLangS (MkXor a as) (MkXor b bs) = eqGLangE a b && eqGLangList as bs
  eqGLangS (MkIor a as) (MkIor b bs) = eqGLangE a b && eqGLangList as bs
  eqGLangS _            _            = False

  private
  eqGLangList : List (GLang ELEM) -> List (GLang ELEM) -> Bool
  eqGLangList Nil     Nil     = True
  eqGLangList (x::xs) (y::ys) =
      if eqGLangE x y
        then eqGLangList xs ys
        else False
  eqGLangList _       _       = False

private
eqGLang : GLang a -> GLang b -> Bool
eqGLang {a=ELEM}   {b=ELEM}   x y = eqGLangE x y
eqGLang {a=INTENT} {b=INTENT} x y = eqGLangI x y
eqGLang {a=STRUCT} {b=STRUCT} x y = eqGLangS x y
eqGLang _          _              = False

Eq (GLang ty) where
  (==) = eqGLang

-- -------------------------------------------------------------- [ Comparable ]

cmpGLang : GLang x -> GLang y -> Ordering
cmpGLang {x} {y} _ _ = compare x y

Ord (GLang ty) where
  compare x y = cmpGLang x y

-- ---------------------------------------------------------------- [ Synonyms ]
public export
GOAL : Type
GOAL = GLang ELEM

public export
SOFT : Type
SOFT = GLang ELEM

public export
TASK : Type
TASK = GLang ELEM

public export
RES : Type
RES = GLang ELEM

-- ----------------------------------------------------------- [ Pretty Syntax ]

syntax [a] "==>" [b] "|" [c] = mkImpacts c a b
syntax [a] "~~>" [b] "|" [c] = mkEffects c a b
syntax [a] "&=" [b] = mkAnd a b
syntax [a] "X=" [b] = mkXor a b
syntax [a] "|=" [b] = mkIor a b

-- ---------------------------------------------------------------- [ toString ]

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
import Data.Vect

PIN : Type
PIN = Vect 4 Char

data ATMState = Ready | CardInserted | Session

data PINCheck = CorrectPIN | IncorrectPIN

data HasCard : ATMState -> Type where
    HasCI : HasCard CardInserted
    HasSession : HasCard Session

data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where
    InsertCard : ATMCmd () Ready (const CardInserted)
    EjectCard : {auto prf : HasCard state} -> ATMCmd () state (const Ready)
    GetPIN : ATMCmd PIN CardInserted (const CardInserted)

    CheckPIN : PIN -> ATMCmd PINCheck CardInserted
                        (\check =>
                            case check of
                                CorrectPIN => Session
                                IncorrectPIN => CardInserted)
    GetAmount : ATMCmd Nat state (const state)

    Dispense : (amount : Nat) -> ATMCmd () Session (const Session)

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

atm : ATMCmd () Ready (const Ready)
atm =
    do
        InsertCard
        pin <- GetPIN
        cash <- GetAmount
        pinOK <- CheckPIN pin
        case pinOK of
            CorrectPIN =>
                do
                    Dispense cash
                    EjectCard
                    Message "Please remove your card and cash"
            IncorrectPIN =>
                do
                    Message "Incorrect PIN"
                    EjectCard

-- badATM : ATMCmd () state (const Ready)
-- badATM = EjectCard

testPIN : PIN
testPIN = ['1', '2', '3', '4']

readVect : (n : Nat) -> IO (Vect n Char)
readVect Z =
    do
        discard <- getLine
        pure []
readVect (S k) =
    do
        ch <- getChar
        chs <- readVect k
        pure (ch :: chs)

runATM : ATMCmd res inState outStateFn -> IO res
runATM InsertCard =
    do
        putStrLn "Please insert your card (press enter)"
        x <- getLine
        pure ()
runATM EjectCard  = putStrLn "Card ejected"
runATM GetPIN =
    do
        putStr "Enter PIN: "
        readVect 4
runATM (CheckPIN pin) =
    if pin == testPIN
        then pure CorrectPIN
        else pure IncorrectPIN
runATM GetAmount =
    do
        putStr "How much would you like? "
        x <- getLine
        pure (cast x)
runATM (Dispense amount) = putStrLn ("Here is " ++ show amount)
runATM (Message msg) = putStrLn msg
runATM (Pure res) = pure res
runATM (x >>= f) =
    do
        x' <- runATM x
        runATM (f x')


text:
-- printf "Hallo" : String
-- printf "Hallo %s" : String -> String
-- printf "%s = %d" : String -> Int -> String

data Format = Lit String Format
            | Str Format
            | Num Format
            | End

%name Format fmt

PrintfType : Format -> Type
PrintfType (Lit x fmt) = PrintfType fmt
PrintfType (Str fmt) = String -> PrintfType fmt
PrintfType (Num fmt) = Int -> PrintfType fmt
PrintfType End = String

parseFormat1 : List Char -> Format
parseFormat1 [] = End
parseFormat1 ('%' :: 's' :: xs) = Str (parseFormat1 xs)
parseFormat1 ('%' :: 'd' :: xs) = Num (parseFormat1 xs)
parseFormat1 (x :: xs) = case parseFormat1 xs of
                            Lit lit fmt => Lit (strCons x lit) fmt
                            fmt         => Lit (strCons x "")  fmt

parseFormat : String -> Format
parseFormat x = ?parseFormat2 (unpack x)

printf : (s : String) -> PrintfType (parseFormat s)

--data Format = Lit String Format
--            | Str Format
            --| Num Format
            --| End

--%name Format fmt

--PrintfType : Format -> Type
--PrintfType (Lit x fmt) = PrintfType fmt
--PrintfType (Str fmt) = ?PrintfType_rhs_6
--PrintfType (Num fmt) = ?PrintfType_rhs_7
--PrintfType End = String

max_stars_repo_name: fthomas/tdd-talk

max_issues_repo_name: fthomas/tdd-talk

max_forks_repo_name: fthomas/tdd-talk