text:
module Collections.BSTree.Map.Elem

import Collections.BSTree.Map.Core
import Collections.Util.Bnd
import Decidable.Equality
import Decidable.Order.Strict

namespace Key
  ||| Proof that a key is contained in a `BSTree`.
  |||
  ||| @ k The key whose presence is being asserted
  ||| @ t The tree in which `k` is present
  public export
  data Elem : {0 rel : kTy -> kTy -> Type} ->
              {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              (k : kTy) ->
              (t : BST pre tot vTy mn mx) ->
              Type where
    [search k]
    ||| Proof that `k` is at the root of the tree.
    Here    : {0 l : BST pre tot vTy mn (Mid k)} ->
              {0 r : BST pre tot vTy (Mid k) mx} ->
              Elem k (Node k v l r)
    ||| Proof that `k` is in the left subtree.
    |||
    ||| @ bnds  Ordering witnesses on `k`. These are not erased.
    ||| @ elemL Proof that `k` is in a tree `l`.
    InLeft  : {0 rel : kTy -> kTy -> Type} ->
              {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              {0 l : BST pre tot vTy mn (Mid x)} ->
              {0 r : BST pre tot vTy (Mid x) mx} ->
              (bnds : (BndLT rel mn (Mid k), BndLT rel (Mid k) (Mid x))) ->
              (elemL : Elem k l) ->
              Elem k (Node x v l r)
    ||| Proof that `k` is in the right subtree.
    |||
    ||| @ bnds  Ordering witnesses on `k`. These are not erased.
    ||| @ elemL Proof that `k` is in a tree `r`.
    InRight : {0 rel : kTy -> kTy -> Type} ->
              {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              {0 l : BST pre tot vTy mn (Mid x)} ->
              {0 r : BST pre tot vTy (Mid x) mx} ->
              (bnds : (BndLT rel (Mid x) (Mid k), BndLT rel (Mid k) mx)) ->
              (elemR : Elem k r) ->
              Elem k (Node x v l r)

  export
  Uninhabited (Elem {pre} {tot} k (Empty prf)) where
    uninhabited Here        impossible
    uninhabited (InLeft _ _)  impossible
    uninhabited (InRight _ _) impossible

  ||| Proof that if `k` is an element of a tree and `k` precedes its root node, then `k` is an
  ||| element of its left subtree.
  elemInLeft : {0 rel : kTy -> kTy -> Type} ->
               {pre : StrictPreorder kTy rel} ->
               {tot : StrictOrdered kTy rel} ->
               {k,x : kTy} ->
               {l : BST pre tot vTy mn (Mid x)} ->
               {r : BST pre tot vTy (Mid x) mx} ->
               BndLT rel (Mid k) (Mid x) ->
               Elem k (Node x v l r) ->
               Elem k l
  elemInLeft {pre} {k} kx Here                    = absurd $ irreflexive {x=Mid k} kx
  elemInLeft           _  (InLeft _ elemL)        = elemL
  elemInLeft {pre}     kx (InRight (xk, _) elemR) =
    absurd $ asymmetric @{SPA} {x=Mid k} {y=Mid x} kx xk

  ||| Proof that if `x` is an element of a tree and `x` follows its root node, then `x` is an element
  ||| of its right subtree.
  elemInRight : {0 rel : kTy -> kTy -> Type} ->
                {pre : StrictPreorder kTy rel} ->
                {tot : StrictOrdered kTy rel} ->
                {k,x : kTy} ->
                {l : BST pre tot vTy mn (Mid x)} ->
                {r : BST pre tot vTy (Mid x) mx} ->
                BndLT rel (Mid x) (Mid k) ->
                Elem k (Node x v l r) ->
                Elem k r
  elemInRight {pre} {k} xk Here                   = absurd $ irreflexive {x=Mid k} xk
  elemInRight {pre}     xk (InLeft (_, kx) elemL) =
    absurd $ asymmetric @{SPA} {x=Mid k} {y=Mid x} kx xk
  elemInRight           _  (InRight _ elemR)      = elemR

  isElem' : {0 rel : kTy -> kTy -> Type} ->
            {pre : StrictPreorder kTy rel} ->
            {tot : StrictOrdered kTy rel} ->
            (k : kTy) ->
            (BndLT rel mn (Mid k), BndLT rel (Mid k) mx) ->
            (t : BST pre tot vTy mn mx) ->
            Dec (Elem k t)
  isElem' _ _ (Empty _) = No absurd
  isElem' {tot} k (lk, ku) (Node x v l r) =
    case order (Mid k) (Mid x) of
        DecLT kx   => case isElem' k (lk, kx) l of
                            Yes prf => Yes $ InLeft (lk, kx) prf
                            No ctra => No $ ctra . (elemInLeft kx)
        DecEQ Refl => Yes Here
        DecGT xk   => case isElem' k (xk, ku) r of
                            Yes prf => Yes $ InRight (xk, ku) prf
                            No ctra => No $ ctra . (elemInRight xk)

  ||| Decide whether `k` is a key in the tree `t`.
  export
  isElem : {0 rel : kTy -> kTy -> Type} ->
           {pre : StrictPreorder kTy rel} ->
           {tot : StrictOrdered kTy rel} ->
           (k : kTy) ->
           (t : BSTree rel {pre} {tot} vTy) ->
           Dec (Elem k t)
  isElem k t = isElem' k (BotLTMid, MidLTTop) t

namespace Value
  ||| Proof that a value is contained in a `BSTree`.
  |||
  ||| @ v The key whose presence is being asserted
  ||| @ t The tree in which `v` is present
  public export
  data Elem : {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              (v : vTy) ->
              (t : BST pre tot vTy mn mx) ->
              Type where
    [search v]
    ||| Proof that `v` is at the root of the tree.
    Here    : Elem v (Node k v l r)
    ||| Proof that `v` is in the left subtree.
    |||
    ||| @ elemL Proof that `v` is in a tree `l`.
    InLeft  : {l : BST pre tot vTy mn (Mid k)} ->
              {r : BST pre tot vTy (Mid k) mx} ->
              (elemL : Value.Elem {pre} {tot} v l) ->
              Elem v (Node k x l r)
    ||| Proof that `v` is in the right subtree.
    |||
    ||| @ elemL Proof that `v` is in a tree `r`.
    InRight : {l : BST pre tot vTy mn (Mid k)} ->
              {r : BST pre tot vTy (Mid k) mx} ->
              (elemR : Value.Elem {pre} {tot} v r) ->
              Elem v (Node k x l r)

  export
  Uninhabited (Value.Elem v (Empty {pre} {tot} prf)) where
    uninhabited Here        impossible
    uninhabited (InLeft _)  impossible
    uninhabited (InRight _) impossible

  ||| Decide whether `v` is a value in the tree `t`.
  |||
  ||| Note that since the tree is structured by key, not by value, this is necessarily implemented
  ||| via an inefficient search.
  export
  isElem : DecEq vTy =>
           {pre : StrictPreorder kTy rel} ->
           {tot : StrictOrdered kTy rel} ->
           (v : vTy) ->
           (t : BSTree rel vTy) ->
           Dec (Value.Elem v t)
  isElem = isElem' where
    isElem' : (v : vTy) ->
              (t : BST pre tot vTy mn mx) ->
              Dec (Value.Elem v t)
    isElem' _ (Empty _) = No absurd
    isElem' v (Node _ x l r) =
      case decEq v x of
           Yes Refl => Yes Here
           No  neq  => case isElem' v l of
                            Yes prf => Yes $ InLeft prf
                            No notL => case isElem' v r of
                                            Yes prf => Yes $ InRight prf
                                            No notR => No $ \case
                                                                  InLeft  prf => absurd $ notL prf
                                                                  Here        => absurd $ neq Refl
                                                                  InRight prf => absurd $ notR prf

insertElem' : {0 rel : kTy -> kTy -> Type} ->
              {pre : StrictPreorder kTy rel} ->
              {tot : StrictOrdered kTy rel} ->
              {0 min,max : Bnd kTy} ->
              (k : kTy) ->
              (v : vTy) ->
              (bnds : (BndLT rel min (Mid k), BndLT rel (Mid k) max)) ->
              (t : BST pre tot vTy min max) ->
              (t : BST pre tot vTy min max ** (Key.Elem k t, Value.Elem v t))
insertElem' x vX (lx, xu) (Empty _) =
  ((Node x vX (Empty lx) (Empty xu)) ** (Here, Here))
insertElem' {tot} x vX (lx, xu) (Node y vY l r) =
  case order (Mid x) (Mid y) of
      DecLT xy   => let bnd = (lx, xy)
                        (l' ** (pk, pv)) = insertElem' x vX bnd l in
                        (Node y vY l' r ** (InLeft bnd pk, InLeft pv))
      DecEQ Refl => (Node x vX l r ** (Here, Here))
      DecGT yx   => let bnd = (yx, xu)
                        (r' ** (pk, pv)) = insertElem' x vX bnd r in
                        (Node y vY l r' ** (InRight bnd pk, InRight pv))

||| Insert a new key `k` and value `v` in the tree, and produce membership proofs for `k` and `v` in
||| the updated tree. If the key is already present in the tree, the associated value is replaced
||| with the supplied value.
export
insertElem : {0 rel : kTy -> kTy -> Type} ->
             {pre : StrictPreorder kTy rel} ->
             {tot : StrictOrdered kTy rel} ->
             (k : kTy) ->
             (v : vTy) ->
             BSTree {pre} {tot} rel vTy ->
             (t : BSTree {pre} {tot} rel vTy ** (Key.Elem k t, Value.Elem v t))
insertElem k v t = insertElem' k v (BotLTMid, MidLTTop) t

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
module Inigo.Async.Promise

export
data Promise : Type -> Type where
  MkPromise : ((a -> IO ()) -> (String -> IO ()) -> IO ()) -> Promise a

export
Functor Promise where
  map f (MkPromise cmd) = MkPromise (\succ => \err => cmd (\x => succ (f x)) err)

mutual
  export
  Applicative Promise where
    pure x = MkPromise (\succ => \err => succ x)
    x <*> y = x >>= (\f => f <$> y)

  export
  Monad Promise where
    (MkPromise cmd) >>= f = MkPromise (\succ =>
                                        \err =>
                                                cmd (\x =>
                                                          let (MkPromise cmd_) = (f x)
                                                          in cmd_ succ err
                                                    ) err
                                      )

export
resolve : Promise a -> (a -> IO ()) -> (String -> IO ()) -> IO ()
resolve (MkPromise cmd) ok err =
  cmd ok err

export
run : Promise a -> IO ()
run p =
  resolve p (\_ => pure ()) (\err => putStrLn ("Error: " ++ err))

-- I can fold these, but that's a bit of an issue since
-- they will end up running sequentially, which is really
-- not the intent here, but for now...
export
all : List (Promise a) -> Promise (List a)
all promises =
  doAll promises
  where
    doAll : List (Promise a) -> Promise (List a)
    doAll (p :: ps) =
      do
        x <- p
        rest <- doAll ps
        pure (x :: rest)
    doAll [] = pure []

export
lift : a -> Promise a
lift x = MkPromise (\ok => \err => ok x)

export
liftIO : IO a -> Promise a
liftIO x = MkPromise (\ok => \err => x >>= ok)

export
parallel : Promise a -> Promise a -> Promise a
parallel (MkPromise s1) (MkPromise s2) = MkPromise $ \err => \cb => do
  s1 err cb
  s2 err cb

public export
promise : Type -> Type
promise a = (a -> IO ()) -> (String -> IO ()) -> PrimIO ()

export
promisify : promise a -> Promise a
promisify prim =
  MkPromise (\ok, err => primIO $ prim ok err)

export
boolToInt : Bool -> Int
boolToInt False = 0
boolToInt True = 1

ext: idr

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Physics

import World

%access export

inspectWorld : Host -> String
inspectWorld w = foldWorld w $ \_, i, k, e =>
  "(id: " ++ show k ++ ", health: " ++ show (health i e) ++ ");"

attack' : Int -> Key -> Host -> Host
attack' d k w = fst $ withEntity w k $ \_, i, e => (attack i d e, ())


text:
import Aoc
import Data.List
import Data.Vect
import Data.SortedSet as S

Point : Nat -> Type
Point n = Vect n Int

replicateM : Monad m => (n : Nat) -> m a -> m (Vect n a)
replicateM Z _ = pure []
replicateM (S k) m = (::) <$> m <*> replicateM k m

neighbors : {n : Nat} -> Point n -> List (Point n)
neighbors v =
  [zipWith (+) v d | d <- replicateM n [-1..1], any (/=0) d]

step : {n : Nat} -> SortedSet (Point n) -> SortedSet (Point n)
step ps =
  let ps' = S.toList ps
  in S.fromList [p | p <- nub $ ps' ++ concatMap neighbors ps',
                 let k = count (flip S.contains ps) (neighbors p),
                 k == 3 || k == 2 && S.contains p ps]

main : IO ()
main = do
  ls <- readLines
  let initial = [(x,y) | (y,line) <- enumerate ls, (x,c) <- enumerate (unpack line), c == '#']
  let initial3 = S.fromList [[the Int $ cast x,cast y,0] | (x,y) <- initial]
  let initial4 = S.fromList [[the Int $ cast x,cast y,0,0] | (x,y) <- initial]
  putStr "*   "; printLn $ length $ S.toList $ times 6 step initial3
  putStr "**  "; printLn $ length $ S.toList $ times 6 step initial4


text:
import Data.Primitives.Views

quiz : Stream Int -> (score : Nat) -> IO ()
quiz (num1 :: num2 :: nums) score =
    do
        putStrLn ("Score so far: " ++ show score)
        putStr (show num1 ++ " * " ++ show num2 ++ "? ")
        answer <- getLine
        if cast answer == num1 * num2
            then do
                putStrLn "Correct!"
                quiz nums (score + 1)
            else do
                putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
                quiz nums score

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

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
    where
        bound : Int -> Int
        bound num with (divides num 12)
            bound ((12 * div) + rem) | DivBy prf = rem + 1

data Face = Heads | Tails

total
getFace : Int -> Face
getFace x with (divides x 2)
  getFace ((2 * div) + rem) | (DivBy prf) =
    case rem of
        0 => Heads
        _ => Tails

coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips count xs = take count (map getFace xs)


text:
module Main

import Test.Golden

main : IO ()
main = runner [!(testsInDir "examples" (const True) "description..." [] Nothing)]

max_stars_repo_name: gemmaro/hello-idris-test

max_issues_repo_name: gemmaro/hello-idris-test

max_forks_repo_name: gemmaro/hello-idris-test


text:
import Data.Vect

-- Page 219
-- Exercise 1
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

-- Exercise 2
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

-- Exercise 3
data ThreeEq : a -> b -> c -> Type where
  Same : ThreeEq x x x

-- Exercise 4
allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x (Same) = Same

-- Page 227
-- Exercise 1
myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in
                         rewrite plusSuccRightSucc m k in Refl

reverseProof_xs : Vect (S (n + len)) a -> Vect (n + (S len)) a
reverseProof_xs xs {n} {len} = rewrite sym(plusSuccRightSucc n len) in xs

-- Exercise 2
reverse' : Vect n a -> Vect m a -> Vect (n + m) a
reverse' acc [] {n} = rewrite plusZeroRightNeutral n in acc
reverse' acc (x :: xs) =
        reverseProof_xs (reverse' (x::acc) xs)

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs

-- Page 234
-- See file `week7_2_234.idr`

-- Page 249
-- Exercise 2

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

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

notLastOne : (contra : (x = value) -> Void) -> Last [x] value -> Void
notLastOne contra LastOne = contra Refl
notLastOne contra (LastCons prf) = noLastEmpty prf

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

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

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module Lib
import Types
import Data.List

public export
calculateDeltas : (Double,Double) -> (Double, Double) -> Double
calculateDeltas (t0, t1) (x, y) = t0 + t1 * x-y

avg : List Double -> Double
avg [] = 0.0
avg xs = do
  let x = length xs
  let y = natToInteger x
  let z = fromInteger y
  (sum xs) / z

getmult: List Double -> List Double -> List Double
getmult [] [] = []
getmult (x::xs) [] = (x::getmult xs [])
getmult [] (y::ys) = (y::getmult [] ys)
getmult (x::xs) (y::ys) = (x * y :: getmult xs ys)

public export
adjustDeltas : List Double -> List (Double,Double) -> List Double
adjustDeltas deltas examples =
  let xs = map fst examples
--      zipped = zip deltas xs
--  in getmult deltas  xs
  in  zipWith (*) deltas xs

public export
newthetas : (Double, Double) -> Double -> List (Double, Double) ->  (Double, Double)
newthetas thetas alpha examples =
  let deltas = (map (calculateDeltas thetas) examples)
      adjusted = adjustDeltas deltas examples
      t0 = fst thetas
      t1 = snd thetas
      newt0 = t0 - alpha * avg deltas
      newt1 = t1 - alpha * avg adjusted
  in (newt0, newt1)

public export
linearRegression : (Double, Double) -> Double ->List (Double, Double) -> Int -> (Double, Double)
linearRegression coefficients alpha dataset iterations =
 case iterations == 0 of
      True => coefficients
      False => let thetas = newthetas coefficients alpha dataset in linearRegression thetas alpha dataset (iterations -1)


text:
module Main -- where

import Compiler.ANF
import Compiler.Common
import Compiler.LambdaLift
import Compiler.VMCode
import Core.CompileExpr
import Core.Context
import Idris.Driver
import Language.JSON.Data
import System
import System.File
import System.Path
import Text.PrettyPrint.Prettyprinter.Doc
import Text.PrettyPrint.Prettyprinter.Render.Terminal

import Idris.Codegen.ExtSTG.ANFToSTG
import Idris.Codegen.ExtSTG.ExternalTopIds
import Idris.Codegen.ExtSTG.JSON
import Idris.Codegen.ExtSTG.STG
import Idris.Codegen.ExtSTG.StringTable

compile
  :  Ref Ctxt Defs
  -> (tmpDir : String)
  -> (outputDir : String)
  -> ClosedTerm
  -> (outfile : String)
  -> Core (Maybe String)
compile defs tmpDir outputDir term outfile = do
  coreLift $ putStrLn "Compile closed program term..."
  cdata <- getCompileData (True {-lazy annotations-}) ANF term
  cntr  <- mkCounter
  unqs  <- mkUniques
  dts   <- mkDataTypes
  ebs   <- mkExternalBinders
  st    <- newStringTableRef
  stgs  <- compileModule $ anf cdata
  let res = show $ toJSON stgs
  let out = outputDir </> outfile
  Right () <- coreLift $ writeFile out res
    | Left err => throw $ FileErr out err
  pure (Just out)

execute
  :  Ref Ctxt Defs
  -> (tmpDir : String)
  -> ClosedTerm
  -> Core ()
execute defs tmpDir term = do
  coreLift $ putStrLn "Maybe in an hour."

stgCodegen : Codegen
stgCodegen = MkCG compile execute

main : IO ()
main = mainWithCodegens [("stg", stgCodegen)]

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
main : IO ()
main = do sline <- getLine
          let arr = [ the Nat (cast v) | v <- words sline ]
          printLn (arr)


text:
module Data.MergeList

import Decidable.Order
import Data.OrderedVect

%default total

export
data MergeList : (rank : Nat) -> (cnt : Nat) -> (constraint : Ordered ty to) -> Type where
  Nil : MergeList _ Z _
  Skip : (next : MergeList (n + n) cnt constraint)
      -> MergeList n cnt constraint
  (::) : OrderedVect n constraint
      -> .{cnt : Nat}
      -> (next : MergeList (n + n) cnt constraint)
      -> MergeList n (n + cnt) constraint

%name MergeList xs,ys,zs

insertVect : {constraint : Ordered ty to}
          -> {n : Nat}
          -> {cnt : Nat}
          -> MergeList n cnt constraint
          -> OrderedVect n constraint
          -> MergeList n (cnt + n) constraint
insertVect {n} {constraint} {cnt=Z} Nil v
  = rewrite rewriteType in v :: Nil
      where rewriteType : MergeList n n constraint = MergeList n (n + 0) constraint
            rewriteType = rewrite sym $ plusZeroRightNeutral n in Refl
insertVect {n} {cnt} (Skip next) v = rewrite plusCommutative cnt n in
                                     v :: next
insertVect {n} ((::) v next {cnt}) v'
  = rewrite sym $ plusCommutative cnt n in
    rewrite sym $ plusAssociative cnt n n in
    Skip $ insertVect next (merge n v n v')

export
empty : .{auto constraint : Ordered ty to} -> MergeList 1 0 constraint
empty = []

export
insert : .{constraint : Ordered ty to}
      -> {cnt : Nat}
      -> MergeList 1 cnt constraint
      -> ty
      -> MergeList 1 (cnt + 1) constraint
insert l x = insertVect l [x]

export
mergeListToOrderedVect : .{constraint : Ordered ty _}
                      -> (n : Nat)
                      -> (cnt : Nat)
                      -> MergeList n cnt constraint
                      -> OrderedVect cnt constraint
mergeListToOrderedVect _ _ Nil = []
mergeListToOrderedVect n cnt (Skip next) = mergeListToOrderedVect (n + n) cnt next
mergeListToOrderedVect n (n + nextCnt) (v :: next)
  = merge n v nextCnt $ mergeListToOrderedVect (n + n) nextCnt next

namespace CountedMergeList
  public export
  CountedMergeList : (n : Nat) -> (constraint: Ordered to rel) -> Type
  CountedMergeList n constraint = (cnt : Nat ** Lazy $ MergeList n cnt constraint)

  export
  empty : CountedMergeList 1 constraint
  empty = (Z ** empty)

  export
  insert : .{constraint : Ordered ty to} -> CountedMergeList 1 constraint -> ty -> CountedMergeList 1 constraint
  insert (cnt ** xs) x = (cnt + 1 ** insert xs x)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
module Control.Linear.Network

-- An experimental linear type based API to sockets

import Control.Linear.LIO

import public Network.Socket.Data
import Network.Socket

public export
data SocketState = Ready | Bound | Listening | Open | Closed

export
data Socket : SocketState -> Type where
     MkSocket : Socket.Data.Socket -> Socket st

export
newSocket : LinearIO io
      => (fam  : SocketFamily)
      -> (ty   : SocketType)
      -> (pnum : ProtocolNumber)
      -> (success : (1 _ : Socket Ready) -> L io ())
      -> (fail : SocketError -> L io ())
      -> L io ()
newSocket fam ty pnum success fail
    = do Right rawsock <- socket fam ty pnum
               | Left err => fail err
         success (MkSocket rawsock)

export
close : LinearIO io => (1 _ : Socket st) -> L io {use=1} (Socket Closed)
close (MkSocket sock)
    = do Socket.close sock
         pure1 (MkSocket sock)

export
done : LinearIO io => (1 _ : Socket Closed) -> L io ()
done (MkSocket sock) = pure ()

export
bind : LinearIO io =>
       (1 _ : Socket Ready) ->
       (addr : Maybe SocketAddress) ->
       (port : Port) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Bound)))
bind (MkSocket sock) addr port
    = do ok <- Socket.bind sock addr port
         pure1 $ ok == 0 # MkSocket sock

export
connect : LinearIO io =>
          (sock : Socket) ->
          (addr : SocketAddress) ->
          (port : Port) ->
          L io {use=1} (Res Bool (\res => Socket (case res of
                                                       False => Closed
                                                       True => Open)))
connect sock addr port
    = do ok <- Socket.connect sock addr port
         pure1 $ ok == 0 # MkSocket sock

export
listen : LinearIO io =>
         (1 _ : Socket Bound) ->
         L io {use=1} (Res Bool (\res => Socket (case res of
                                                      False => Closed
                                                      True => Listening)))
listen (MkSocket sock)
    = do ok <- Socket.listen sock
         pure1 $ ok == 0 # MkSocket sock

export
accept : LinearIO io =>
         (1 _ : Socket Listening) ->
         L io {use=1} (Res Bool (\case
                                    False => Socket Listening
                                    True => (Socket Listening, Socket Open)))
accept (MkSocket sock)
    = do Right (sock', sockaddr) <- Socket.accept sock
             | Left err => pure1 (False # MkSocket sock)
         pure1 (True # (MkSocket sock, MkSocket sock'))

export
send : LinearIO io =>
       (1 _ : Socket Open) ->
       (msg : String) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Open)))
send (MkSocket sock) msg
    = do Right c <- Socket.send sock msg
             | Left err => pure1 (False # MkSocket sock)
         pure1 (True # MkSocket sock)

export
recv : LinearIO io =>
       (1 _ : Socket Open) ->
       (len : ByteLength) ->
       L io {use=1} (Res (Maybe (String, ResultCode))
                         (\res => Socket (case res of
                                               Nothing => Closed
                                               Just msg => Open)))
recv (MkSocket sock) len
    = do Right msg <- Socket.recv sock len
             | Left err => pure1 (Nothing # MkSocket sock)
         pure1 (Just msg # MkSocket sock)

export
recvAll : LinearIO io =>
          (1 _ : Socket Open) ->
          L io {use=1} (Res (Maybe String)
                            (\res => Socket (case res of
                                                  Nothing => Closed
                                                  Just msg => Open)))
recvAll (MkSocket sock)
    = do Right msg <- Socket.recvAll sock
             | Left err => pure1 (Nothing # MkSocket sock)
         pure1 (Just msg # MkSocket sock)


text:
module Primitives.Externals

import Primitives.Common
import Primitives.Felt
import Primitives.Primitives
import CairoCode.CairoCode
import Core.Context
import CairoCode.CairoCodeUtils
import CodeGen.CodeGenHelper
import Data.SortedMap
import Data.SortedSet

interface External where
  apStable : Bool
  tupleSig : Maybe TupleStructure
  implicits : List LinearImplicit
  imports : SortedSet Import
  genCode : List CairoReg -> LinearImplicitArgs -> List CairoReg -> String
  eval: (numRes:Nat) -> List ValueInfo -> Maybe (List EvalRes)

%spec f
associate : (rec:External) => (f:(External -> a)) -> a
associate fun = fun rec

 -- Definitions
[pedersen_hash] External where
    apStable = True
    tupleSig = Nothing
    implicits = [pedersen_builtin]
    imports = empty
    eval _ _ = Nothing -- Todo: add pedersen_hash impl in idris2
    -- tupled
    genCode [r] impls [a,b] = """
        #cairopedersenhash
        assert [\{ ptrName }] = \{ compileReg a }
        assert [\{ ptrName } + 1] = \{ compileReg b }
        \{ compileRegDecl r } = [\{ ptrName } + 2]
        \{ compileRegDecl (snd ptr) } = \{ ptrName } + 3

        """
        where ptr: (CairoReg, CairoReg)
              ptr = fromMaybe (assert_total $ idris_crash "pedersen_ptr is missing") (lookup pedersen_builtin impls)
              ptrName : String
              ptrName = compileReg (fst ptr)
    genCode _ _ _ = assert_total $ idris_crash "unsupported signature for cairopedersenhash"

[cairo_output] External where
    apStable = True
    tupleSig = Nothing
    implicits = [] -- Will use a Monadic implementation for the builtin
    imports = empty
    eval _ _ = Nothing -- output can not be constant folded
    genCode [r] impls [ptr,val] = """
        #cairooutput
        assert [\{ compileReg ptr }] = \{ compileReg val }
        \{ compileRegDecl r } = \{ compileReg ptr } + 1

        """
    genCode _ _ _ = assert_total $ idris_crash "unsupported signature for cairooutput"

 -- Dispatch
%inline
dispatch : (name:Name) -> ((External => a) -> a)
dispatch (NS _ (UN $ Basic "cairopedersenhash")) = associate @{pedersen_hash}
dispatch (NS _ (UN $ Basic "cairooutput")) = associate @{cairo_output}
dispatch n = (\f => assert_total $ idris_crash ("No implementation for external " ++ show n ++ " available"))

 -- Accessors
export
externalApStable : Name -> Bool
externalApStable name = dispatch name apStable

export
externalLinearImplicits : Name -> List LinearImplicit
externalLinearImplicits name = dispatch name implicits

export
externalImports : Name -> SortedSet Import
externalImports name = dispatch name imports

export
externalCodeGen : Name -> List CairoReg -> LinearImplicitArgs -> List CairoReg -> String
externalCodeGen name res impls args = dispatch name genCode res checkedImpls args
    where expectedImpls : List LinearImplicit
          expectedImpls = externalLinearImplicits name
          checkedImpls : LinearImplicitArgs
          checkedImpls = if (length (keys impls)) == (length expectedImpls) && all (\i => isJust $ lookup i impls) expectedImpls
            then impls
            else assert_total $ idris_crash ("implicits are not correct for " ++ (show name))

export
externalTupleSig : Name -> Maybe TupleStructure
externalTupleSig name = dispatch name tupleSig

export
externalEval : Name -> (numRes:Nat) -> List ValueInfo -> Maybe (List EvalRes)
externalEval name numRets args = dispatch name eval numRets args

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module RecRule

recNat : (x : Type) -> x -> (Nat -> x -> x) -> (Nat -> x)
recNat x base step Z = base
recNat x base step (S k) = step k (recNat x base step k)

fctl : Nat -> Nat
fctl = recNat Nat (S Z) step where
  step = \n: Nat => \y : Nat => (S n) * y

recListNat : (x: Type) -> x -> (Nat -> List Nat -> x -> x) -> (List Nat -> x)
recListNat x base step [] = base
recListNat x base step (y :: xs) = step y xs previous where
  previous = recListNat x base step xs

lsum : List Nat -> Nat
lsum = recListNat Nat base step where
  base = Z
  step = \h : Nat => \t : List Nat => \accum : Nat => h + accum


text:
module Control.Applicative.Concurrent

%default total

public export
interface ConcurrentApplicative m where
  Concurrent : Applicative m


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

import XML.DOM
import XML.Reader

import Freyja
import Freyja.Convert
import Freyja.Extract

import Readability

import Frigg.Effs
import Frigg.Options
import Frigg.Error
import Frigg.Eval
import Frigg.API
import Frigg.Commands

-- ------------------------------------------------------------------- [ Begin ]

friggBanner : String
friggBanner = """
    ______     _                ______            __
   / ____/____(_)___ _____ _   /_  __/___  ____  / /
  / /_  / ___/ / __ `/ __ `/    / / / __ \/ __ \/ /
 / __/ / /  / / /_/ / /_/ /    / / / /_/ / /_/ / /
/_/   /_/  /_/\__, /\__, /    /_/  \____/\____/_/
             /____//____/

http://www.github.com/jfdm/frigg-tool
Type :? for help

Frigg is free software with ABSOLUTELY NO WARRANTY.
"""

||| Fetch and parse commands
fetchCMD : Frigg FriggCMD
fetchCMD = do
    putStr "frigg> "
    rawCmd <- getStr
    case parseCMD rawCmd of
      Left err => do
        printLn NoSuchCommand
        fetchCMD
      Right cmd => pure cmd

doCommand : FriggCMD -> Frigg ()
doCommand Quit             = pure ()
doCommand Help             = putStrLn showHelp
doCommand (Display part)   = doDisplay part
doCommand (Convert outfmt) = doConvertShow outfmt
doCommand (Query qStr)     = doQuery qStr
doCommand (Eval  what)     = doEvalAndReport what

runREPL : Frigg ()
runREPL = do
    cmd <- fetchCMD
    case cmd of
      Quit => pure ()
      x    => do
        doCommand x
        runREPL

||| A Viewer to view a library of patterns.
export
friggREPL : Frigg ()
friggREPL =
  case banner !(getOptions) of
    True => do
      putStrLn friggBanner
      runREPL
    False => runREPL

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Solutions.Traverse

import Control.Applicative.Const
import Control.Monad.Identity
import Data.HList
import Data.List1
import Data.Singleton
import Data.String
import Data.Validated
import Data.Vect
import Text.CSV

%default total

record State state a where
  constructor ST
  runST : state -> (state,a)

get : State state state
get = ST $ \s => (s,s)

put : state -> State state ()
put v = ST $ \_ => (v,())

modify : (state -> state) -> State state ()
modify f = ST $ \v => (f v,())

runState : state -> State state a -> (state, a)
runState = flip runST

evalState : state -> State state a -> a
evalState s = snd . runState s

execState : state -> State state a -> state
execState s = fst . runState s

Functor (State state) where
  map f (ST run) = ST $ \s => let (s2,va) = run s in (s2, f va)

Applicative (State state) where
  pure v = ST $ \s => (s,v)
  ST fun <*> ST val = ST $ \s =>
    let (s2, f)  = fun s
        (s3, va) = val s2
     in (s3, f va)

Monad (State state) where
  ST val >>= f = ST $ \s =>
    let (s2, va) = val s
     in runST (f va) s2

--------------------------------------------------------------------------------
--          Reading CSV Tables
--------------------------------------------------------------------------------

-- 1

mapFromTraverse : Traversable t => (a -> b) -> t a -> t b
mapFromTraverse f = runIdentity . traverse (Id . f)

-- 2

-- Since Idris can't infer the type of `b` the call to `MkConst`, we have
-- to pass a value (which we can choose freely) explicitly.
foldMapFromTraverse : Traversable t => Monoid m => (a -> m) -> t a -> m
foldMapFromTraverse f = runConst . traverse (MkConst {b = ()}. f)

-- 3

interface Functor t => Foldable t => Traversable' t where
  traverse' : Applicative f => (a -> f b) -> t a -> f (t b)

Traversable' List where
  traverse' f Nil       = pure Nil
  traverse' f (x :: xs) = [| f x :: traverse' f xs |]

Traversable' List1 where
  traverse' f (h ::: t) = [| f h ::: traverse' f t |]

Traversable' (Either e) where
  traverse' f (Left ve)  = pure $ Left ve
  traverse' f (Right va) = Right <$> f va

Traversable' Maybe where
  traverse' f Nothing   = pure Nothing
  traverse' f (Just va) = Just <$> f va

-- 4

data List01 : (nonEmpty : Bool) -> Type -> Type where
  Nil  : List01 False a
  (::) : a -> List01 False a -> List01 ne a

Functor (List01 ne) where
  map f Nil       = Nil
  map f (x :: xs) = f x :: map f xs

Foldable (List01 ne) where
  foldr acc st []        = st
  foldr acc st (x :: xs) = acc x (foldr acc st xs)

Traversable (List01 ne) where
  traverse _ Nil       = pure Nil
  traverse f (x :: xs) = [| f x :: traverse f xs |]

-- 5

record Tree a where
  constructor Node
  value  : a
  forest : List (Tree a)

Forest : Type -> Type
Forest = List . Tree

treeMap : (a -> b) -> Tree a -> Tree b
treeMap f (Node value forest) = Node (f value) (go forest)
  where go : Forest a -> Forest b
        go []        = []
        go (x :: xs) = treeMap f x :: go xs

Functor Tree where map = treeMap

mutual
  foldrTree : (el -> st -> st) -> st -> Tree el -> st
  foldrTree f v (Node value forest) = f value (foldrForest f v forest)

  foldrForest : (el -> st -> st) -> st -> Forest el -> st
  foldrForest _ v []        = v
  foldrForest f v (x :: xs) = foldrTree f (foldrForest f v xs) x

Foldable Tree where
  foldr   = foldrTree

mutual
  traverseTree : Applicative f => (a -> f b) -> Tree a -> f (Tree b)
  traverseTree g (Node v fo) = [| Node (g v) (traverseForest g fo) |]

  traverseForest : Applicative f => (a -> f b) -> Forest a -> f (Forest b)
  traverseForest g []        = pure []
  traverseForest g (x :: xs) = [| traverseTree g x :: traverseForest g xs |]

Traversable Tree where
  traverse = traverseTree

-- 6

data Crud : (i : Type) -> (a : Type) -> Type where
  Create : (value : a) -> Crud i a
  Update : (id : i) -> (value : a) -> Crud i a
  Read   : (id : i) -> Crud i a
  Delete : (id : i) -> Crud i a

Functor (Crud i) where
  map f (Create value)    = Create $ f value
  map f (Update id value) = Update id $ f value
  map f (Read id)         = Read id
  map f (Delete id)       = Delete id

Foldable (Crud i) where
  foldr acc st (Create value)   = acc value st
  foldr acc st (Update _ value) = acc value st
  foldr _   st (Read _)         = st
  foldr _   st (Delete _)       = st

Traversable (Crud i) where
  traverse f (Create value)    = Create <$> f value
  traverse f (Update id value) = Update id <$> f value
  traverse f (Read id)         = pure $ Read id
  traverse f (Delete id)       = pure $ Delete id

-- 7

data Response : (e, i, a : Type) -> Type where
  Created : (id : i) -> (value : a) -> Response e i a
  Updated : (id : i) -> (value : a) -> Response e i a
  Found   : (values : List a) -> Response e i a
  Deleted : (id : i) -> Response e i a
  Error   : (err : e) -> Response e i a

Functor (Response e i) where
  map f (Created id value) = Created id $ f value
  map f (Updated id value) = Updated id $ f value
  map f (Found values)     = Found $ map f values
  map _ (Deleted id)       = Deleted id
  map _ (Error err)        = Error err

Foldable (Response e i) where
  foldr acc st (Created _ value) = acc value st
  foldr acc st (Updated _ value) = acc value st
  foldr acc st (Found values)    = foldr acc st values
  foldr _   st (Deleted _)       = st
  foldr _   st (Error _)         = st

Traversable (Response e i) where
  traverse f (Created id value) = Created id <$> f value
  traverse f (Updated id value) = Updated id <$> f value
  traverse f (Found values)     = Found <$> traverse f values
  traverse _ (Deleted id)       = pure $ Deleted id
  traverse _ (Error err)        = pure $ Error err

-- 8

record Comp (f,g : Type -> Type) (a : Type) where
  constructor MkComp
  unComp  : f (g a)

Functor f => Functor g => Functor (Comp f g) where
  map fun = MkComp . (map . map) fun . unComp

Foldable f => Foldable g => Foldable (Comp f g) where
  foldr f st (MkComp v)  = foldr (flip $ foldr f) st v

Traversable f => Traversable g => Traversable (Comp f g) where
  traverse fun = map MkComp . (traverse . traverse) fun . unComp

record Product (f,g : Type -> Type) (a : Type) where
  constructor MkProduct
  fst : f a
  snd : g a

Functor f => Functor g => Functor (Product f g) where
  map fun (MkProduct fa ga) = MkProduct (map fun fa) (map fun ga)

Foldable f => Foldable g => Foldable (Product f g) where
  foldr f st (MkProduct v w)  = foldr f (foldr f st w) v

Traversable f => Traversable g => Traversable (Product f g) where
  traverse fun (MkProduct fa ga) =
    [| MkProduct (traverse fun fa) (traverse fun ga) |]

--------------------------------------------------------------------------------
--          Programming with State
--------------------------------------------------------------------------------

-- 1

rnd : Bits64 -> Bits64
rnd seed = fromInteger
         $ (437799614237992725 * cast seed) `mod` 2305843009213693951

Gen : Type -> Type
Gen = State Bits64

-- 1.1

bits64 : Gen Bits64
bits64 = get <* modify rnd

-- 1.2

range64 : (upper : Bits64) -> Gen Bits64
range64 18446744073709551615 = bits64
range64 n                    = (`mod` (n + 1)) <$> bits64

interval64 : (a,b : Bits64) -> Gen Bits64
interval64 a b =
  let mi = min a b
      ma = max a b
   in (mi +) <$> range64 (ma - mi)

interval : Num n => Cast n Bits64 => (a,b : n) -> Gen n
interval a b = fromInteger . cast <$> interval64 (cast a) (cast b)

-- 1.3

bool : Gen Bool
bool = (== 0) <$> range64 1

-- 1.4

fin : {n : _} -> Gen (Fin $ S n)
fin = (\x => fromMaybe FZ $ natToFin x _) <$> interval 0 n

-- 1.5

element : {n : _} -> Vect (S n) a -> Gen a
element vs = (`index` vs) <$> fin

-- 1.6

vect : {n : _} -> Gen a -> Gen (Vect n a)
vect = sequence . replicate n

list : Gen Nat -> Gen a -> Gen (List a)
list gnat ga = gnat >>= \n => toList <$> vect {n} ga

testGen : Bits64 -> Gen a -> Vect 10 a
testGen seed = evalState seed . vect

-- 1.7

choice : {n : _} -> Vect (S n) (Gen a) -> Gen a
choice gens = element gens >>= id

-- 1.8

either : Gen a -> Gen b -> Gen (Either a b)
either ga gb = choice [Left <$> ga, Right <$> gb]

-- 1.9

printableAscii : Gen Char
printableAscii = chr <$> interval 32 126

-- 1.10

string : Gen Nat -> Gen Char -> Gen String
string gn = map pack . list gn

-- 1.11

namespace HListF

  public export
  data HListF : (f : Type -> Type) -> (ts : List Type) -> Type where
    Nil  : HListF f []
    (::) : (x : f t) -> (xs : HListF f ts) -> HListF f (t :: ts)

hlist : HListF Gen ts -> Gen (HList ts)
hlist Nil        = pure Nil
hlist (gh :: gt) = [| gh :: hlist gt |]

-- 1.12

hlistT : Applicative f => HListF f ts -> f (HList ts)
hlistT Nil        = pure Nil
hlistT (fh :: ft) = [| fh :: hlistT ft |]

-- 2

-- 2.1

record IxState s t a where
  constructor IxST
  runIxST : s -> (t,a)

-- 2.2

Functor (IxState s t) where
  map f (IxST run) = IxST $ \vs => let (vt,va) = run vs in (vt, f va)

-- 2.3

pure : a -> IxState s s a
pure va = IxST $ \vs => (vs,va)

(<*>) : IxState r s (a -> b) -> IxState s t a -> IxState r t b
IxST ff <*> IxST fa = IxST $ \vr =>
  let (vs,f)  = ff vr
      (vt,va) = fa vs
   in (vt, f va)

-- 2.4

(>>=) : IxState r s a -> (a -> IxState s t b) -> IxState r t b
IxST fa >>= f = IxST $ \vr =>
  let (vs,va) = fa vr in runIxST (f va) vs

(>>) : IxState r s () -> IxState s t a -> IxState r t a
IxST fu >> IxST fb = IxST $ fb . fst . fu

-- 2.5

namespace IxMonad
  interface Functor (m s t) =>
            IxApplicative (0 m : Type -> Type -> Type -> Type) where
    pure : a -> m s s a
    (<*>) : m r s (a -> b) -> m s t a -> m r t b

  interface IxApplicative m => IxMonad m where
    (>>=) : m r s a -> (a -> m s t b) -> m r t b

  IxApplicative IxState where
    pure = Traverse.pure
    (<*>) = Traverse.(<*>)

  IxMonad IxState where
    (>>=) = Traverse.(>>=)

-- 2.6

namespace IxState
  get : IxState s s s
  get = IxST $ \vs => (vs,vs)

  put : t -> IxState s t ()
  put vt = IxST $ \_ => (vt,())

  modify : (s -> t) -> IxState s t ()
  modify f = IxST $ \vs => (f vs, ())

  runState : s -> IxState s t a -> (t,a)
  runState = flip runIxST

  evalState : s -> IxState s t a -> a
  evalState vs = snd . runState vs

  execState : s -> IxState s t a -> t
  execState vs = fst . runState vs

-- 2.7

Applicative (IxState s s) where
  pure = Traverse.pure
  (<*>) = Traverse.(<*>)

Monad (IxState s s) where
  (>>=) = Traverse.(>>=)
  join = (>>= id)

--------------------------------------------------------------------------------
--          The Power of Composition
--------------------------------------------------------------------------------

-- 1

data Tagged : (tag, val : Type) -> Type where
  Tag  : tag -> val -> Tagged tag val
  Pure : val -> Tagged tag val

Functor (Tagged tag) where
  map f (Tag x y) = Tag x (f y)
  map f (Pure x)  = Pure (f x)

Foldable (Tagged tag) where
  foldr f acc (Tag _ x) = f x acc
  foldr f acc (Pure x)  = f x acc

Traversable (Tagged tag) where
  traverse f (Tag x y) = Tag x <$> f y
  traverse f (Pure x)  = Pure <$> f x

Bifunctor Tagged where
  bimap f g (Tag x y) = Tag (f x) (g y)
  bimap _ g (Pure x)  = Pure (g x)

  mapFst f (Tag x y) = Tag (f x) y
  mapFst _ (Pure x)  = Pure x

  mapSnd g (Tag x y) = Tag x (g y)
  mapSnd g (Pure x)  = Pure (g x)

Bifoldable Tagged where
  bifoldr f g acc (Tag x y) = f x (g y acc)
  bifoldr f g acc (Pure x)  = g x acc

  bifoldl f g acc (Tag x y) = g (f acc x) y
  bifoldl _ g acc (Pure x)  = g acc x

  binull _ = False

Bitraversable Tagged where
  bitraverse f g (Tag x y) = [| Tag (f x) (g y) |]
  bitraverse _ g (Pure x)  = Pure <$> g x

-- 2

record Biff (p : Type -> Type -> Type) (f,g : Type -> Type) (a,b : Type) where
  constructor MkBiff
  runBiff : p (f a) (g b)

Bifunctor p => Functor f => Functor g => Bifunctor (Biff p f g) where
  bimap ff fg = MkBiff .  bimap (map ff) (map fg) . runBiff

Bifoldable p => Foldable f => Foldable g => Bifoldable (Biff p f g) where
  bifoldr ff fg acc = bifoldr (flip $ foldr ff) (flip $ foldr fg) acc . runBiff

Bitraversable p => Traversable f => Traversable g =>
  Bitraversable (Biff p f g) where
    bitraverse ff fg =
      map MkBiff . bitraverse (traverse ff) (traverse fg) . runBiff

-- 3

record Tannen (f : Type -> Type) (p : Type -> Type -> Type) (a,b : Type) where
  constructor MkTannen
  runTannen : f (p a b)

Bifunctor p => Functor f => Bifunctor (Tannen f p) where
  bimap ff fg = MkTannen .  map (bimap ff fg) . runTannen

Bifoldable p => Foldable f => Bifoldable (Tannen f p) where
  bifoldr ff fg acc = foldr (flip $ bifoldr ff fg) acc . runTannen

Bitraversable p => Traversable f => Bitraversable (Tannen f p) where
  bitraverse ff fg = map MkTannen . traverse (bitraverse ff fg) . runTannen

-- 4

data TagError : Type where
  CE         : CSVError -> TagError
  InvalidTag : (line : Nat) -> (tag : String) -> TagError
  Append     : TagError -> TagError -> TagError

Semigroup TagError where (<+>) = Append

pairWithIndex : a -> State Nat (Nat,a)
pairWithIndex v = ST $ \index => (S index, (index, v))

data Color = Red | Green | Blue

readColor : String -> State Nat (Validated TagError Color)
readColor s = uncurry decodeTag . (`MkPair` s) <$> get
  where decodeTag : Nat -> String -> Validated TagError Color
        decodeTag k "red"   = pure Red
        decodeTag k "green" = pure Green
        decodeTag k "blue"  = pure Blue
        decodeTag k s       = Invalid $ InvalidTag k s

readTaggedLine : String -> Tagged String String
readTaggedLine s = case split ('#' ==) s of
  h ::: [t] => Tag t h
  _         => Pure s

tagAndDecodeTE :  (0 ts : List Type)
               -> CSVLine (HList ts)
               => String
               -> State Nat (Validated TagError (HList ts))
tagAndDecodeTE ts s = mapFst CE . uncurry (hdecode ts) <$> pairWithIndex s

readTagged :  (0 ts : List Type)
           -> CSVLine (HList ts)
           => String
           -> Validated TagError (List $ Tagged Color $ HList ts)
readTagged ts = map runTannen
              . evalState 1
              . bitraverse @{%search} @{Compose} readColor (tagAndDecodeTE ts)
              . MkTannen {f = List} {p = Tagged}
              . map readTaggedLine
              . lines

validInput : String
validInput = """
  f,12,-13.01#green
  t,100,0.0017
  t,1,100.8#blue
  f,255,0.0
  f,24,1.12e17
  """

invalidInput : String
invalidInput = """
  o,12,-13.01#yellow
  t,100,0.0017
  t,1,abc
  f,256,0.0
  f,24,1.12e17
  """


text:
module Mmhelloworld.IdrisSpringBoot.Http.Converter.Json

import IdrisJvm.IO

%access public export

Jackson2ObjectMapperBuilder : Type
Jackson2ObjectMapperBuilder = JVM_Native (Class "org/springframework/http/converter/json/Jackson2ObjectMapperBuilder")

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
module Text.WebIDL.Codegen.Rules

import Data.List
import Data.List1
import Data.List.Elem
import Data.SortedSet
import Text.WebIDL.Codegen.Util

--------------------------------------------------------------------------------
--          Environment
--------------------------------------------------------------------------------

parents : Domain -> List Identifier
parents d =  mapMaybe inherits d.interfaces
          ++ mapMaybe inherits d.dictionaries

kinds : List Domain -> SortedMap Identifier Kind
kinds ds =
  let ps = SortedSet.fromList $ ds >>= parents
   in SortedMap.fromList
        $  (ds >>= pairs name KEnum . enums)
        ++ (ds >>= pairs name KMixin . mixins)
        ++ (ds >>= pairs name (iface ps) . interfaces)
        ++ (ds >>= pairs name KDictionary . dictionaries)
        ++ (ds >>= pairs name KCallback . callbackInterfaces)
        ++ (ds >>= pairs name KCallback . callbacks)
        ++ (ds >>= pairs name KAlias . typedefs)
  where -- pairs list of identifiers with their kinds
        pairs :  (a -> Identifier)
              -> (Identifier -> Kind)
              -> List a
              -> List (Identifier,Kind)
        pairs name knd = map $ \v => (name v, knd $ name v)

        iface : SortedSet Identifier -> Identifier -> Kind
        iface ps i = KInterface (contains i ps) i

||| Calculate the environment from a list of domains.
export
env : Nat -> List Domain -> Env
env k ds = let ks = kinds ds
            in MkEnv k ks jsTypes (aliases ks $ ds >>= typedefs)
  where -- calculates the mapping from type aliases to the
        -- types they represent
        aliases :  SortedMap Identifier Kind
                -> List Typedef
                -> SortedMap Identifier (IdlTypeF ExtAttributeList Kind)
        aliases ks = SortedMap.fromList . map mkPair
          where kind : Identifier -> Kind
                kind i = fromMaybe (KOther i) $ lookup i ks

                mkPair : Typedef -> (Identifier,IdlTypeF ExtAttributeList Kind)
                mkPair (MkTypedef _ _ t n) = (n, map kind t)

        dictToType : Dictionary -> (Identifier,JSType)
        dictToType (MkDictionary _ n i _) = (n, MkJSType i Nil)

        interfaceToType : Interface -> (Identifier,JSType)
        interfaceToType (MkInterface _ n i _) = (n, MkJSType i Nil)

        mixin :  SortedMap Identifier JSType
              -> Includes
              -> SortedMap Identifier JSType
        mixin ts (MkIncludes _ n incl) =
          case lookup n ts of
               Nothing => ts
               Just js => let js2 = record {mixins $= (incl ::)} js
                           in insert n js2 ts

        jsTypes : SortedMap Identifier JSType
        jsTypes = let types =  (ds >>= map dictToType . dictionaries)
                            ++ (ds >>= map interfaceToType . interfaces)

                      includes = ds >>= includeStatements

                      initialMap = SortedMap.fromList types

                   in foldl mixin initialMap includes

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

buff : BufferRelatedType -> SimpleType
buff Uint8Array        = Unchangeable "UInt8Array"
buff Uint16Array       = Unchangeable "UInt8Array"
buff Uint32Array       = Unchangeable "UInt8Array"
buff Uint8ClampedArray = Unchangeable "UInt8ClampedArray"
buff x                 = Unchangeable $ show x

-- booleans are marshalled from Idris2 `Bool` to JS `Boolean`
-- and back
prim : PrimitiveType -> SimpleType
prim Boolean             = Boolean
prim (Unsigned Short)    = Primitive "Bits16"
prim (Unsigned Long)     = Primitive "Bits32"
prim (Unsigned LongLong) = Primitive "JSBits64"
prim (Signed Short)      = Primitive "Int16"
prim (Signed Long)       = Primitive "Int32"
prim (Signed LongLong)   = Primitive "JSInt64"
prim (Unrestricted x)    = Primitive "Double"
prim (Restricted x)      = Primitive "Double"
prim Undefined           = Undef
prim Byte                = Primitive "Int8"
prim Octet               = Primitive "Bits8"
prim BigInt              = Primitive "Integer"

string : StringType -> SimpleType
string ByteString = Unchangeable "ByteString"
string DOMString  = Primitive "String"
string USVString  = Primitive "String"

strTpe : StringType -> String
strTpe ByteString = "ByteString"
strTpe DOMString = "String"
strTpe USVString = "String"

parameters (e : Env, dom : Domain)

  -- Lookup the kind of an identifier from the environment
  kind : Identifier -> Kind
  kind i = fromMaybe (KOther i) $ lookup i e.kinds

  mutual
    -- the most interesting part when unaliasing a type:
    -- here the aliases may be wrapped in an `I` data
    -- constructor, in which case we try to convert it
    -- to a distinguishable type. If that's not possible,
    -- we return the corresponding type wrapped in a `Left`.
    -- Otherwise we keep the distinguishable type
    -- (but keep unaliasing inner types, if any)
    uaD : DistinguishableF ExtAttributeList Kind -> Codegen CGType
    uaD i@(I $ KAlias x) =
      case lookup x e.aliases of
           Nothing            => Left [UnresolvedAlias dom x]
           Just x             => unalias x
    uaD (I k)                 = Right $ fromKind k
    uaD (Sequence x y)        = simple . Array <$> unalias y
    uaD (FrozenArray x y)     = simple . Array <$> unalias y
    uaD (ObservableArray x y) = simple . Array <$> unalias y
    uaD (Record x _ z)        = simple . Record (strTpe x) <$> unalias z
    uaD (P p)                 = Right . simple $ prim p
    uaD (S s)                 = Right . simple $ string s
    uaD (B b)                 = Right . simple $ buff b
    uaD Object                = Right . simple . Interface True $
                                MkIdent "Object"
    uaD Symbol                = Right $ unchangeable "Symbol"

    uaU :  UnionTypeF ExtAttributeList Kind
        -> Codegen (Nullable $ List1 SimpleType)
    uaU (UT f s r) =
      do (hf ::: tf) <- uaM f
         rest        <- map join (traverse uaM (s ::: r))

         let nullables = hf ::: (tf ++ forget rest)
             simples   = map nullVal nullables

         if any isNullable nullables
            -- the result is nullable
            then pure $ MaybeNull simples
            -- the result is non-nullable
            else pure $ NotNull simples

    -- in case of a wrapped distinguishable type,
    -- we unalias it using `uaD` but keep the unaliased
    -- version only, if it is again distinguishable.
    uaM :  UnionMemberTypeF ExtAttributeList Kind
        -> Codegen (List1 $ Nullable SimpleType)
    uaM (MkUnionMember a t) =
      do t2 <- uaD t
         case t2 of
              Any       => Left [AnyInUnion dom]
              Promise x => Left [PromiseInUnion dom]
              Simple x  => Right $ singleton x
              (Union $ MaybeNull xs) => Right $ map MaybeNull xs
              (Union $ NotNull xs)   => Right $ map NotNull xs

    unalias : IdlTypeF ExtAttributeList Kind -> Codegen CGType
    unalias Any               = Right Any
    unalias (D $ NotNull d)   = uaD d
    unalias (U $ NotNull d)   = Union <$> uaU d
    unalias (U $ MaybeNull d) = Union . nullable <$> uaU d
    unalias (Promise x)       = Promise <$> unalias x
    unalias t@(D $ MaybeNull d) =
      do res <- uaD d
         case res of
              Any         => Left [NullableAny dom]
              (Simple x)  => pure . Simple $ nullable x
              (Union x)   => pure . Union $ nullable x
              (Promise x) => Left [NullablePromise dom]

  -- calculate the aliased type from a type coming
  -- from the WebIDL parser
  -- the unaliased version of the type is only kept (in a `Just`)
  -- if it differs from the original type.
  tpe : IdlType -> CodegenV CGType
  tpe t = let cgt = map kind t
           in fromEither $ unalias cgt

  -- convert an IDL type coming from the parser to
  -- a return type in the code generator
  rtpe : IdlType -> CodegenV ReturnType
  rtpe (D $ NotNull $ P Undefined)        = Valid Undefined
  rtpe (D $ NotNull $ I $ MkIdent "void") = Valid Undefined
  rtpe t = Def <$> tpe t

  constTpe : ConstType -> CodegenV CGConstType
  constTpe (CI i) =
    case uaD (I $ kind i) of
         Left x                                 => Invalid x
         Right (Simple $ NotNull $ Primitive s) => Valid $ MkConstType s
         Right _                                => Invalid [InvalidConstType dom]

  constTpe (CP p) =
    case prim p of
         Primitive s => Valid $ MkConstType s
         _           => Invalid [InvalidConstType dom]

  const : Const -> CodegenV CGConst
  const (MkConst t n v) = map (\t2 => MkConst t2 n v) (constTpe t)

--------------------------------------------------------------------------------
--          Arguments
--------------------------------------------------------------------------------

  -- create an optional argument named "value" from
  -- a type coming from the parser
  optArg : IdlType -> Default -> CodegenV CGArg
  optArg t d = [| Optional (pure $ MkArgName "value") (tpe t) (pure d) |]

  -- create an argument named "value" from
  -- a type coming from the parser
  valArg : IdlType -> CodegenV CGArg
  valArg t = Mandatory (MkArgName "value") <$> tpe t

  -- convert an argument coming from the parser
  -- to one to be used in the code generator
  arg : Arg -> CodegenV CGArg
  arg (MkArg _ t n) = Mandatory n <$> tpe t

  -- convert an argument coming from the parser
  -- to a vararg to be used in the code generator
  vararg : Arg -> CodegenV CGArg
  vararg (MkArg _ t n) = VarArg n <$> tpe t

  -- convert an argument coming from the parser
  -- to an optional arg to be used in the code generator
  opt : OptArg -> CodegenV CGArg
  opt (MkOptArg _ _ t n d) = [| Optional (pure n) (tpe t) (pure d) |]

  -- convert an argument list coming from the parser
  -- to a list of codegen args
  toArgs : ArgumentList -> CodegenV Args
  toArgs (VarArg as v)    = [| snoc (traverse arg as) (vararg v) |]
  toArgs (NoVarArg as os) = [| traverse arg as ++ traverse opt os |]

--------------------------------------------------------------------------------
--          Inheritance
--------------------------------------------------------------------------------

  objectOnly : Supertypes
  objectOnly = MkSupertypes [MkIdent "Object"] []

  ||| Calculates the supertypes and mixins for a given
  ||| identifier.
  |||
  |||  @maxIterations : Maximal number of iterations. Without this,
  |||                   the algorithm might loop forever in case of
  |||                   cyclic dependencies. This value corresponds
  |||                   to the maximal length of the inheritance chain.
  supertypes : Identifier -> Supertypes
  supertypes = run e.maxInheritance
    where run : Nat -> Identifier -> Supertypes
          run 0     i = objectOnly
          run (S k) i =
            case lookup i e.jsTypes of
                 Nothing                              => objectOnly

                 (Just $ MkJSType Nothing mixins)       =>
                   record { mixins = mixins } objectOnly

                 (Just $ MkJSType (Just parent) mixins) =>
                   let MkSupertypes parents mixins2 = run k parent
                    in MkSupertypes (parent :: parents) (mixins ++ mixins2)

--------------------------------------------------------------------------------
--          Functions
--------------------------------------------------------------------------------

  op : Identifier -> Op a -> CodegenV (List CGFunction)
  op n (MkOp _ _ Nothing _)   = Invalid [RegularOpWithoutName dom n]
  op n (MkOp _ t (Just o) as) =
    map pure [| Regular (pure o) (pure $ kind n) (toArgs as) (rtpe t) |]

  static : Identifier -> Op a -> CodegenV (List CGFunction)
  static n (MkOp _ _ Nothing _)   = Invalid [RegularOpWithoutName dom n]
  static n (MkOp _ t (Just o) a) =
    map pure [| Static (pure o) (pure $ kind n) (toArgs a) (rtpe t) |]

  constr : Identifier -> ArgumentList -> CodegenV (List CGFunction)
  constr name args = pure . Constructor (kind name) <$> toArgs args

  attrRO : Identifier -> Readonly Attribute -> CodegenV (List CGFunction)
  attrRO o (MkRO $ MkAttribute _ t n) =
    pure . AttributeGet n (kind o) <$> rtpe t

  attr : Identifier -> Attribute -> CodegenV (List CGFunction)
  attr obj (MkAttribute _ t n) =
     map pure [| Attribute (pure n) (pure $ kind obj) (valArg t) (rtpe t) |]

  str : Identifier -> Stringifier -> CodegenV (List CGFunction)
  str o (Z v)              = attr o v
  str o (S $ Z v)          = attrRO o v
  str o (S $ S $ Z v)      = op o v
  str o (S $ S $ S $ Z ()) =
    let name = Just $ MkOpName "toString"
     in op o (MkOp () domString name (NoVarArg [] []))

  staticAttrRO : Identifier -> Readonly Attribute -> CodegenV (List CGFunction)
  staticAttrRO o (MkRO $ MkAttribute _ t n) =
    pure . StaticAttributeGet n (kind o) <$> rtpe t

  staticAttr : Identifier -> Attribute -> CodegenV (List CGFunction)
  staticAttr obj (MkAttribute _ t n) =
    let ak  = kind obj
     in sequence [ StaticAttributeGet n ak <$> rtpe t
                 , StaticAttributeSet n ak <$> valArg t
                 ]

  dictCon : Kind -> List DictionaryMemberRest -> CodegenV CGFunction
  dictCon o = fromEither . go Nil Nil
    where go : Args -> Args -> List DictionaryMemberRest -> Codegen CGFunction
          go xs ys [] = pure $ DictConstructor o (reverse xs ++ reverse ys)
          go xs ys (Required _ t n :: zs) =
            do t2 <- toEither $ tpe t
               go (Mandatory (MkArgName n.value) t2 :: xs) ys zs
          go xs ys (Optional t n d :: zs) =
            do t2 <- toEither $ tpe t
               go xs (Optional (MkArgName n.value) t2 d :: ys) zs

  dictFuns : Dictionary -> CodegenV (List CGFunction)
  dictFuns d = [| dictCon (kind d.name) (map snd d.members) ::
                  (map join (traverse (fromMember . snd) d.members)) |]
    where fromMember : DictionaryMemberRest -> CodegenV (List CGFunction)
          fromMember (Required _ t n) =
            let an = Valid $ MkAttributeName n.value
             in map pure [| Attribute an (pure $ kind d.name)
                                      (valArg t) (rtpe t) |]

          fromMember (Optional t n def) =
            let an = Valid $ MkAttributeName n.value
                cgt = map (`UndefOr` Just def) (tpe t)
                ak  = Valid $ kind d.name
             in map pure [| Attribute an ak (optArg t def) cgt |]

  mixinFuns : Mixin -> CodegenV (List CGFunction)
  mixinFuns m = concat <$> traverse (fromMember . snd) m.members
    where fromMember : MixinMember -> CodegenV (List CGFunction)
          fromMember (MConst _)   = Valid Nil
          fromMember (MOp o)      = op m.name o
          fromMember (MStr s)     = str m.name s
          fromMember (MAttrRO ro) = attrRO m.name ro
          fromMember (MAttr at)   = attr m.name at

  ifaceFuns : Interface -> CodegenV (List CGFunction)
  ifaceFuns i = concat <$> traverse (fromMember . snd) i.members
    where getter : IdlType -> ArgumentList -> CodegenV (List CGFunction)
          getter t (NoVarArg [a] Nil) =
             fromEither $ do ag <- toEither $ arg a
                             rt <- toEither $ rtpe t
                             if isIndex (argType ag)
                                then Right [Getter (kind i.name) ag rt]
                                else Left [InvalidGetter dom i.name]

          getter _ _ = Invalid [InvalidGetter dom i.name]

          setter : IdlType -> ArgumentList -> CodegenV (List CGFunction)
          setter t (NoVarArg [a,r] Nil) =
            fromEither $ do ag <- toEither $ arg a
                            rt <- toEither $ rtpe t
                            rg <- toEither $ arg r
                            if isIndex (argType ag) && isUndefined rt
                               then Right [Setter (kind i.name) ag rg]
                               else Left [InvalidSetter dom i.name]

          setter _ _ = Invalid [InvalidSetter dom i.name]

          -- getters and setters without a name are treated as indexed
          -- versions (special syntax in the FFI), all others are treated
          -- as regular operations
          fromOp : Operation -> CodegenV (List CGFunction)
          fromOp (MkOp (Just Getter)  t Nothing as) = getter t as
          fromOp (MkOp (Just Setter)  t Nothing as) = setter t as
          fromOp (MkOp (Just Deleter) _ _       _ ) = Valid Nil
          fromOp x                                  = op i.name x

          fromPart : PartialInterfaceMember -> CodegenV (List CGFunction)
          fromPart (IOp x)                 = fromOp x
          fromPart (IStr x)                = str i.name x
          fromPart (IStatic $ Z x)         = staticAttr i.name x
          fromPart (IStatic $ S $ Z x)     = staticAttrRO i.name x
          fromPart (IStatic $ S $ S $ Z x) = static i.name x
          fromPart (IAttr x)               = attr i.name x
          fromPart (IAttrRO x)             = attrRO i.name x
          fromPart (IConst _)              = Valid Nil
          fromPart (IMap x)                = Valid Nil
          fromPart (ISet x)                = Valid Nil
          fromPart (IMapRO x)              = Valid Nil
          fromPart (ISetRO x)              = Valid Nil
          fromPart (IAttrInh x)            = Valid Nil
          fromPart (IIterable x y)         = Valid Nil
          fromPart (IAsync x y xs)         = Valid Nil

          fromMember : InterfaceMember -> CodegenV (List CGFunction)
          fromMember (Z $ MkConstructor as) = constr i.name as
          fromMember (S $ Z p)              = fromPart p
          fromMember (S $ S x) impossible

  ifaceConsts : Interface -> CodegenV (List CGConst)
  ifaceConsts (MkInterface _ _ _ ms) = join <$> traverse (fromMember . snd) ms
    where fromMember : InterfaceMember -> CodegenV (List CGConst)
          fromMember (S $ Z $ IConst x) = map pure $ const x
          fromMember _                  = Valid []

  mixinConsts : Mixin -> CodegenV (List CGConst)
  mixinConsts (MkMixin _ _ ms) = join <$> traverse (fromMember . snd) ms
    where fromMember : MixinMember -> CodegenV (List CGConst)
          fromMember (MConst x) = map pure $ const x
          fromMember _          = Valid []

  callbackConsts : CallbackInterface -> CodegenV (List CGConst)
  callbackConsts (MkCallbackInterface _ _ ms) =
    join <$> traverse (fromMember . snd) ms
    where fromMember : CallbackInterfaceMember -> CodegenV (List CGConst)
          fromMember v = case extract Const v of
                              Nothing => Valid []
                              Just x  => map pure $ const x

  export
  domain : CodegenV CGDomain
  domain = [| MkDomain (pure dom.domain)
                       callbacks
                       (traverse dict dom.dictionaries)
                       (pure dom.enums)
                       (traverse iface dom.interfaces)
                       (traverse mixin dom.mixins)
           |]

    where dict : Dictionary -> CodegenV CGDict
          dict v@(MkDictionary _ n i _) =
            MkDict n  (supertypes n) <$> dictFuns v

          iface : Interface -> CodegenV CGIface
          iface v@(MkInterface _ n i _) =
            [| MkIface (pure n) (pure $ supertypes n)
                       (ifaceConsts v) (ifaceFuns v) |]

          mixin : Mixin -> CodegenV CGMixin
          mixin m = [| MkMixin (pure m.name) (mixinConsts m) (mixinFuns m) |]

          callback : Callback -> CodegenV CGCallback
          callback c = [| MkCallback (pure c.name) (pure Nil)
                                     (rtpe c.type) (toArgs c.args) |]

          callbackIface : CallbackInterface -> CodegenV CGCallback
          callbackIface v@(MkCallbackInterface _ n ms) =
            case mapMaybe (\(_,m)   => extract RegularOperation m) ms of
                 [MkOp () t _ a] =>
                   [| MkCallback (pure n) (callbackConsts v) (rtpe t) (toArgs a) |]
                 xs => Invalid [CBInterfaceInvalidOps dom n (length xs)]

          callbacks : CodegenV (List CGCallback)
          callbacks = [| traverse callback dom.callbacks ++
                         traverse callbackIface dom.callbackInterfaces |]


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

%name Vect xs, ys, zs

{- 3 and 4-}

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

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
data MyList : (a: Type) -> Type where
  Nil: MyList a
  Cons: (x: a) -> MyList a -> MyList a

insertList: a -> MyList a -> MyList a
insertList = Cons

max_stars_repo_name: LucasTornai/pgc-ufabc

max_issues_repo_name: LucasTornai/pgc-ufabc

max_forks_repo_name: LucasTornai/pgc-ufabc


text:
module Flexidisc.OrdList.Permute

import Flexidisc.OrdList.Fresh
import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Nub
import Flexidisc.OrdList.Row
import Flexidisc.OrdList.Type

%default total
%access private

||| Proof that an `OrdList` is a permutation of another `OrdList`
public export
data Permute : (xs : OrdList k o1 v) ->
               (ys : OrdList k o2 v) ->
               Type where
  ||| The empty list is a permutation of an empty list
  Empty : Permute [] []
  Keep  : (e : OrdRow k ty ys) -> Permute xs (dropOrdRow ys e) ->
          Permute ((k, ty)::xs) ys

permuteRefl : (xs : OrdList k o v) -> Permute xs xs
permuteRefl [] = Empty
permuteRefl ((k, v)::xs) = Keep Here (permuteRefl xs)

insertConsPermute : (x : (k, v)) -> (xs : OrdList k o v) ->
                    Permute  (insert x xs) (x :: xs)
insertConsPermute (k, ty) [] = Keep Here Empty
insertConsPermute (k, ty) ((kx, tx) :: xs) with (k < kx)
  | True  = Keep Here (Keep Here (permuteRefl xs))
  | False = Keep (There Here) (insertConsPermute (k, ty) xs)

consInsertPermute : (x : (k, v)) -> (xs : OrdList k o v) ->
                    Permute  (x :: xs) (insert x xs)
consInsertPermute (l, ty) xs =
  Keep (findInsertOrdRow l xs)
       (rewrite dropInsertInv l ty xs in (permuteRefl xs))

permutePreservesFresh :  Permute ys xs -> Fresh k xs -> Fresh k ys
permutePreservesFresh Empty [] = []
permutePreservesFresh (Keep e perm) fresh =
  (\p => freshCantBeLabel fresh (rewrite p in labelFromOrdRow e)) ::
  permutePreservesFresh perm (dropPreservesFresh fresh)

isNubFromPermute : Permute xs ys -> Nub ys -> Nub xs
isNubFromPermute Empty [] = []
isNubFromPermute (Keep e perm) pf =
  permutePreservesFresh perm (removeFromNubIsFresh pf (labelFromOrdRow e))
    :: isNubFromPermute perm (dropPreservesNub pf (labelFromOrdRow e))

export
freshInsert : Fresh k' header -> Nub header ->
              Nub (insert (k', ty) header)
freshInsert fresh isnub {k'} {ty} {header} =
  isNubFromPermute (insertConsPermute (k', ty) header) (fresh :: isnub)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module TestIntegers

import Data.Bits
import Data.List.Quantifiers

put : Show a => a -> IO ()
put = putStrLn . show

castAllTo : (to : Type)
         -> {0 types : List Type}
         -> All (flip Cast to) types => HList types -> List to
castAllTo to = forget . imapProperty (flip Cast to) (cast {to})

interface Num a => Bits a => SomeBits a where
    one : Index {a}

SomeBits Bits8 where
    one = fromNat 1

SomeBits Bits16 where
    one = fromNat 1

SomeBits Bits32 where
    one = fromNat 1

SomeBits Bits64 where
    one = fromNat 1

SomeBits Int8 where
    one = fromNat 1

SomeBits Int16 where
    one = fromNat 1

SomeBits Int32 where
    one = fromNat 1

SomeBits Int64 where
    one = fromNat 1

SomeBits Int where
    one = fromNat 1

SomeBits Integer where
    one = 1

interface Num a => Ord a => NumOrd a where

Num a => Ord a => NumOrd a where

main : IO ()
main = do
    let ints = the (HList _) [
        the Bits8 0, -- Bits8 min
        the Bits8 50,
        the Bits8 255, -- Bits8 max
        the Bits16 0, -- Bits16 min
        the Bits16 10000,
        the Bits16 65535, -- Bits16 max
        the Bits32 0, -- Bits32 min
        the Bits32 1000000000,
        the Bits32 4294967295, -- Bits32 max
        the Bits64 0, -- Bits64 min
        the Bits64 5000000000000000000,
        the Bits64 18446744073709551615, -- Bits64 max
        the Int8 $ -128, -- Int8 min
        the Int8 50,
        the Int8 127, -- Int8 max
        the Int16 $ -32768, -- Int16 min
        the Int16 10000,
        the Int16 32767, -- Int16 max
        the Int32 $ -2147483648, -- Int32 min
        the Int32 500000000,
        the Int32 2147483647, -- Int32 max
        the Int64 $ -9223372036854775808, -- Int64 min
        the Int64 1000000000000000000,
        the Int64 9223372036854775807, -- Int64 max
        the Int $ -9223372036854775808, -- Int min
        the Int 1000000000000000000,
        the Int 9223372036854775807, -- Int max
        the Integer $ -9223372036854775809, -- Int min - 1
        the Integer 0,
        the Integer 9223372036854775808 -- Int max + 1
    ]

    putStrLn "Cast to String:"
    put ints

    putStrLn "Cast to Bits8:"
    put $ castAllTo Bits8 ints

    putStrLn "Cast to Bits16:"
    put $ castAllTo Bits16 ints

    putStrLn "Cast to Bits32:"
    put $ castAllTo Bits32 ints

    putStrLn "Cast to Bits64:"
    put $ castAllTo Bits64 ints

    putStrLn "Cast to Int:"
    put $ castAllTo Int ints

    putStrLn "Cast to Integer:"
    put $ castAllTo Integer ints

    putStrLn "Add:"
    put $ imapProperty Num (+ 1) ints

    putStrLn "Subtract:"
    put $ imapProperty Neg (flip (-) 1) ints

    putStrLn "Negate:"
    put $ imapProperty Neg negate ints

    putStrLn "Multiply:"
    put $ imapProperty Num (* 2) ints

--    putStrLn "Divide:"
--    put $ imapProperty Integral (`div` 3) ints
--    put $ imapProperty Integral (`div` -3) ints
--
--    putStrLn "Mod:"
--    put $ imapProperty Integral (`mod` 17) ints
--    put $ imapProperty Integral (`mod` -17) ints
--
--    putStrLn "Division Euclidean:"
--    put $ imapProperty Integral (\x => (x `div` 19) * 19 + (x `mod` 19)) ints
--    put $ imapProperty Integral (\x => (x `div` -19) * -19 + (x `mod` -19)) ints

    putStrLn "Shift:"
    put $ imapProperty SomeBits (`shiftL` one) ints
    put $ imapProperty SomeBits (`shiftR` one) ints

    putStrLn "Bit Ops:"
    put $ imapProperty SomeBits (.&. 0xAA) ints
    put $ imapProperty SomeBits (.|. 0xAA) ints
    put $ imapProperty SomeBits (`xor` 0xAA) ints

    putStrLn "Comparisons:"
    put $ imapProperty NumOrd (< 0) ints
    put $ imapProperty NumOrd (< 1) ints
    put $ imapProperty NumOrd (> 0) ints
    put $ imapProperty NumOrd (> 1) ints
    put $ imapProperty NumOrd (== 0) ints
    put $ imapProperty NumOrd (<= 0) ints
    put $ imapProperty NumOrd (<= 1) ints
    put $ imapProperty NumOrd (>= 0) ints
    put $ imapProperty NumOrd (>= 1) ints


text:
module LightClick.Types.Equality

import public Toolkit.Decidable.Equality.Indexed

import public Toolkit.Decidable.Informative

import Toolkit.Data.Rig

import Toolkit.Data.Vect.Extra

import LightClick.Types.Meta
import LightClick.Types.Direction
import LightClick.Types.Sensitivity
import LightClick.Types.WireType

import LightClick.Types

%default total

public export
Equals : {a,b : MTy}
      -> (x : Ty a)
      -> (y : Ty b)
      -> Type
Equals = Equals MTy Ty

-- [ No's for Logic vs X]
namespace Logic
  export
  logicNotStruct : (Equals TyLogic (TyStruct xs)) -> Void
  logicNotStruct (Same _ _) impossible

  export
  logicNotUnion : (Equals TyLogic (TyUnion xs)) -> Void
  logicNotUnion (Same _ _ ) impossible

  export
  logicNotArray : (Equals TyLogic (TyArray x k)) -> Void
  logicNotArray (Same _ _) impossible

-- [ No's for Array vs X]
namespace Array
  export
  arrayNotStruct : (Equals (TyArray x k) (TyStruct xs)) -> Void
  arrayNotStruct (Same _ _) impossible

  export
  arrayNotUnion  : (Equals (TyArray x k) (TyUnion xs)) -> Void
  arrayNotUnion (Same _ _) impossible

  export
  arrayDiffIndicies : {k,j : Nat}
                   -> (contra : (k = j) -> Void)
                   -> (Equals (TyArray x k) (TyArray y j))
                   -> Void
  arrayDiffIndicies contra (Same Refl Refl) {k = j} {j = j} = contra Refl

  export
  arrayDiffTypes : (contra : (x `Equals` y) -> Void)
                -> (Equals (TyArray x k) (TyArray y j))
                -> Void
  arrayDiffTypes contra (Same Refl Refl) = contra (Same Refl Refl)

-- [ No's for 'Bodies' vs X]
namespace Body

  namespace Length
    export
    structNotUnion : (TyStruct xs `Equals` TyUnion ys) -> Void
    structNotUnion (Same _ _) impossible

    export
    structDifferBody : {xs : Vect (S n) (Pair String (Ty DATA))}
                    -> {ys : Vect (S m) (Pair String (Ty DATA))}
                    -> (contra : (xs = ys) -> Void)
                    -> (TyStruct xs `Equals` TyStruct ys)
                    -> Void
    structDifferBody contra (Same Refl Refl) = contra Refl

    export
    unionDifferBody : {xs : Vect (S n) (Pair String (Ty DATA))}
                   -> {ys : Vect (S m) (Pair String (Ty DATA))}
                   -> (contra : (xs = ys) -> Void)
                   -> (TyUnion xs `Equals` TyUnion ys)
                   -> Void
    unionDifferBody contra (Same Refl Refl) = contra Refl

    export
    modDifferBody : {xs : DVect String (Ty . PORT) (S n) ns}
                 -> {ys : DVect String (Ty . PORT) (S m) ms}
                 -> (contra : (xs = ys) -> Void)
                 -> (TyModule xs `Equals` TyModule ys)
                 -> Void
    modDifferBody contra (Same Refl Refl) = contra Refl

-- [ No's for Ports]
namespace Ports
  export
  portDifferUsage : (contra : (ux = uy) -> Void)
                 -> (TyPort lx dy sy wx ty ux `Equals` TyPort lx dy sy wx ty uy)
                 -> Void
  portDifferUsage contra (Same Refl Refl) = contra Refl

  export
  portDifferType :  (contra : (tx `Equals` ty) -> Void)
                -> (TyPort lx dy sy wx tx ux `Equals` TyPort lx dy sy wy ty uy)
                -> Void
  portDifferType contra (Same Refl Refl) = contra (Same Refl Refl)

  export
  portDifferWire : (contra : (wx = wy) -> Void)
                -> (TyPort lx dy sy wx tx ux `Equals` TyPort lx dy sy wy ty uy)
                -> Void
  portDifferWire contra (Same Refl Refl) = contra Refl

  export
  portDifferSens : (contra : (sx = sy) -> Void)
                -> (TyPort lx dy sx wx tx ux `Equals` TyPort lx dy sy wy ty uy)
                -> Void
  portDifferSens contra (Same Refl Refl) = contra Refl

  export
  portsDifferDir : (contra : (dx = dy) -> Void)
                -> (TyPort a dx sx wx tx ux `Equals` TyPort a dy sy wy ty uy)
                -> Void
  portsDifferDir contra (Same Refl Refl) = contra Refl

  export
  portsDifferLabel : (contra : (lx = ly) -> Void)
                  -> (TyPort lx dx sx wx tx ux `Equals` TyPort ly dy sy wy ty uy)
                  -> Void
  portsDifferLabel contra (Same Refl Refl) = contra Refl

-- [ No's for Body ]
namespace Body
  namespace Length
    export
    dataBodyLengthsDiffer : {xs : Vect n (Pair String (Ty DATA))}
                         -> {ys : Vect m (Pair String (Ty DATA))}
                         -> (contra : (n = m) -> Void)
                         -> (xs = ys)
                         -> Void
    dataBodyLengthsDiffer contra Refl = contra Refl

    export
    dataBodyLengthsDiffer' : {xs : Vect (S n) (Pair String (Ty DATA))}
                          -> {ys : Vect (S m) (Pair String (Ty DATA))}
                          -> (contra : (xs = ys) -> Void)
                          -> (xs = ys)
                          -> Void
    dataBodyLengthsDiffer' contra Refl = contra Refl

  namespace Values

    namespace Names
      export
      modBodyDiffer : {n : Nat}
                   -> {names : Vect (S n) String}
                   -> {xs : DVect String (Ty . PORT) (S n) names}
                   -> {ys : DVect String (Ty . PORT) (S n) names}
                   -> (contra : (xs = ys) -> Void)
                   -> (TyModule xs `Equals` TyModule ys)
                   -> Void
      modBodyDiffer contra (Same Refl Refl) = contra Refl

    namespace Rest
      export
      restDataBodyDiffer : {xs : Vect n (Pair String (Ty DATA))}
                        -> {ys : Vect n (Pair String (Ty DATA))}
                        -> (contra : (xs = ys) -> Void)
                        -> (((ky, vy) :: xs) = ((ky, vy) :: ys))
                        -> Void
      restDataBodyDiffer contra Refl = contra Refl

      export
      dataBodyDiffer : {xs : Vect n (Pair String (Ty DATA))}
                    -> {ys : Vect n (Pair String (Ty DATA))}
                    -> (contra : (xs = ys) -> Void)
                    -> (xs = ys)
                    -> Void
      dataBodyDiffer contra Refl = contra Refl

      vRestDiffer : {xs : Vect n (Pair String (Ty DATA))}
                 -> {ys : Vect m (Pair String (Ty DATA))}
                 -> (contra : (xs = ys) -> Void)
                 -> (((ky, vy) :: xs) = ((ky, vy) :: ys))
                 -> Void
      vRestDiffer contra Refl = contra Refl

      export
      dVectElemDiffer : {n : Nat}
                     -> {ns : Vect n String}
                     -> {xrest : DVect String (Ty . PORT) n ns}
                     -> {yrest : DVect String (Ty . PORT) n ns}
                     -> {x : String}
                     -> {ex : Ty (PORT x)}
                     -> {ey : Ty (PORT x)}
                     -> (contra : (ex `Equals` ey) -> Void)
                     -> ((ex :: xrest) = (ey :: yrest))
                     -> Void
      dVectElemDiffer contra Refl = contra (Same Refl Refl)

      export
      dVectBodyDiffer : {xrest : DVect String (Ty . PORT) n ns}
                     -> {yrest : DVect String (Ty . PORT) n ns}
                     -> (contra : (xrest = yrest) -> Void)
                     -> ((ey :: xrest) = (ey :: yrest))
                     -> Void
      dVectBodyDiffer contra Refl = contra Refl

    namespace Head
      export
      elemDataBodyDiffer : {xs : Vect n (Pair String (Ty DATA))}
                        -> {ys : Vect n (Pair String (Ty DATA))}
                        -> {vx, vy : Ty DATA}
                        -> (contra : (vx `Equals` vy) -> Void)
                        -> (((ky, vx) :: xs) = ((ky, vy) :: ys))
                        -> Void
      elemDataBodyDiffer contra Refl = contra (Same Refl Refl)

      export
      elemDataKeyDiffer : {xs : Vect n (Pair String (Ty DATA))}
                       -> {ys : Vect n (Pair String (Ty DATA))}
                       -> {vx, vy : Ty DATA}
                       -> (contra : (kx = ky) -> Void)
                       -> (((kx, vx) :: xs) = ((ky, vy) :: ys))
                       -> Void
      elemDataKeyDiffer contra Refl = contra Refl

export
decEq : (x : Ty i)
     -> (y : Ty j)
     -> (prf : i = j)
     -> Dec (Equals MTy Ty x y)

namespace Fields

  differentLengthLeft : {y : String}
                     -> {z : Ty DATA}
                     -> (y, z) `Vect.(::)` (x `Vect.(::)` xs) = (y, z) `Vect.(::)` Nil -> Void
  differentLengthLeft _ impossible

  differentLengthRight : {y : String}
                      -> {z : Ty DATA}
                      -> (y, z) `Vect.(::)` Nil = (y, z) `Vect.(::)` (x `Vect.(::)` xs) -> Void
  differentLengthRight _ impossible

  headTypeDiff : {xs : Vect m (Pair String (Ty DATA))}
              -> {ys : Vect n (Pair String (Ty DATA))}
              -> {z,w : Ty DATA}
              -> (Equals MTy Ty z w -> Void)
              -> (y, z) `Vect.(::)` xs = (y, w) `Vect.(::)` ys
              -> Void
  headTypeDiff contra Refl = contra (Same Refl Refl)

  headLabelDiff : {xs : Vect m (Pair String (Ty DATA))}
               -> {ys : Vect n (Pair String (Ty DATA))}
               -> (x = y -> Void)
               -> {z,w : Ty DATA}
               -> (x, z) `Vect.(::)` xs = (y, w) `Vect.(::)` ys
               -> Void
  headLabelDiff contra Refl = contra Refl

  fieldsAreNotEqual : {xs : Vect m (Pair String (Ty DATA))}
                   -> {ys : Vect n (Pair String (Ty DATA))}
                   -> (x `Vect.(::)` xs = y' `Vect.(::)` ys -> Void)
                   -> (y, z) `Vect.(::)` (x `Vect.(::)` xs) = (y, z) `Vect.(::)` (y' `Vect.(::)` ys)
                   -> Void
  fieldsAreNotEqual contra Refl = contra Refl

  export
  decEq : (xs : Vect (S n) (Pair String (Ty DATA)))
       -> (ys : Vect (S m) (Pair String (Ty DATA)))
             -> Dec (xs = ys)
  decEq {n} xs {m} ys  with (shape xs ys)
    decEq {n = n} ((x, z) :: xs) {m = m} ((y, w) :: ys) | Both with (decEq x y)
      decEq {n = n} ((y, z) :: xs) {m = m} ((y, w) :: ys) | Both | (Yes Refl) with (Equality.decEq z w Refl)
        decEq {n = n} ((y, z) :: xs) {m = m} ((y, z) :: ys) | Both | (Yes Refl) | (Yes (Same Refl Refl)) with (shape xs ys)
          decEq {n = 0} ((y, z) :: []) {m = 0} ((y, z) :: []) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | Empty = Yes Refl

          decEq {n = (S len)} ((y, z) :: (x :: xs)) {m = 0} ((y, z) :: []) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | LH = No differentLengthLeft
          decEq {n = 0} ((y, z) :: []) {m = (S len)} ((y, z) :: (y' :: ys)) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | RH = No differentLengthRight

          decEq {n = (S len)} ((y, z) :: (x :: xs)) {m = (S len)} ((y, z) :: (y' :: ys)) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | Both with (Fields.decEq (x::xs) (y'::ys))
            decEq {n = (S len)} ((y, z) :: (x :: xs)) {m = (S len)} ((y, z) :: (x :: xs)) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | Both | (Yes Refl) = Yes Refl
            decEq {n = (S len)} ((y, z) :: (x :: xs)) {m = (S len)} ((y, z) :: (y' :: ys)) | Both | (Yes Refl) | (Yes (Same Refl Refl)) | Both | (No contra) = No (fieldsAreNotEqual contra)

        decEq {n = n} ((y, z) :: xs) {m = m} ((y, w) :: ys) | Both | (Yes Refl) | (No contra) = No (headTypeDiff contra)
      decEq {n = n} ((x, z) :: xs) {m = m} ((y, w) :: ys) | Both | (No contra) = No (headLabelDiff contra)

namespace Port

  export
  decEq : (x : Ty (PORT a))
       -> (y : Ty (PORT b))
       -> Dec (Equals x y)
  decEq (TyPort a dx sx wx tx ux) (TyPort b dy sy wy ty uy) with (decEq a b)
    decEq (TyPort a dx sx wx tx ux) (TyPort a dy sy wy ty uy) | (Yes Refl) with (decEq dx dy)
      decEq (TyPort a dx sx wx tx ux) (TyPort a dx sy wy ty uy) | (Yes Refl) | (Yes Refl) with (decEq sx sy)
        decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wy ty uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) with (decEq wx wy)
          decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wx ty uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes Refl) with (decEq tx ty Refl)
            decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wx tx uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes (Same Refl Refl)) with (decEq ux uy)
              decEq (TyPort a dx sx wx tx uy) (TyPort a dx sx wx tx uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes (Same Refl Refl)) | (Yes Refl) = Yes (Same Refl Refl)
              decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wx tx uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes (Same Refl Refl)) | (No contra) = No (portDifferUsage contra)
            decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wx ty uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (No contra) = No (portDifferType contra)

          decEq (TyPort a dx sx wx tx ux) (TyPort a dx sx wy ty uy) | (Yes Refl) | (Yes Refl) | (Yes Refl) | (No contra) = No (portDifferWire contra)
        decEq (TyPort a dx sx wx tx ux) (TyPort a dx sy wy ty uy) | (Yes Refl) | (Yes Refl) | (No contra) = No (portDifferSens contra)
      decEq (TyPort a dx sx wx tx ux) (TyPort a dy sy wy ty uy) | (Yes Refl) | (No contra) = No (portsDifferDir contra)
    decEq (TyPort a dx sx wx tx ux) (TyPort b dy sy wy ty uy) | (No contra) = No (portsDifferLabel contra)

namespace Ports

  export
  decEq : {n :Nat}
       -> {ns : _}
       -> (xs : DVect String (Ty . PORT) n ns)
       -> (ys : DVect String (Ty . PORT) n ns)
             -> Dec (xs = ys)
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) with (Port.decEq x y)
    decEq (x :: xs) (x :: ys) | (Yes (Same Refl Refl)) with (Ports.decEq xs ys)
      decEq (x :: xs) (x :: xs) | (Yes (Same Refl Refl)) | (Yes Refl) = Yes Refl
      decEq (x :: xs) (y :: ys) | (Yes (Same Refl Refl)) | (No contra) = No (dVectBodyDiffer contra)
    decEq (x :: xs) (y :: ys) | (No contra) = No (dVectElemDiffer contra)

-- [ Body ]

-- [ Logic Types]
decEq TyLogic TyLogic Refl = Yes (Same Refl Refl)
decEq TyLogic (TyArray x k) Refl = No logicNotArray
decEq TyLogic (TyStruct xs) Refl = No logicNotStruct
decEq TyLogic (TyUnion xs) Refl = No logicNotUnion

-- [ Array Types ]
decEq (TyArray x k) TyLogic Refl = No (negEqSym logicNotArray)

decEq (TyArray x i) (TyArray y j) Refl with (decEq i j)
  decEq (TyArray x i) (TyArray y i) Refl | (Yes Refl) with (decEq x y Refl)
    decEq (TyArray x i) (TyArray x i) Refl | (Yes Refl) | (Yes (Same Refl Refl))
      = Yes (Same Refl Refl)
    decEq (TyArray x i) (TyArray y i) Refl | (Yes Refl) | (No contra)
      = No (arrayDiffTypes contra)
  decEq (TyArray x i) (TyArray y j) Refl | (No contra)
    = No (arrayDiffIndicies contra)

decEq (TyArray x k) (TyStruct xs) Refl = No arrayNotStruct
decEq (TyArray x k) (TyUnion xs) Refl = No arrayNotUnion

-- [ Structs ]
decEq (TyStruct xs) TyLogic Refl = No (negEqSym logicNotStruct)
decEq (TyStruct xs) (TyArray type length) Refl = No (negEqSym arrayNotStruct)

decEq (TyStruct xs) (TyStruct ys) Refl with (Fields.decEq xs ys)
  decEq (TyStruct xs) (TyStruct xs) Refl | (Yes Refl)  = Yes (Same Refl Refl)
  decEq (TyStruct xs) (TyStruct ys) Refl | (No contra) = No (structDifferBody contra)

decEq (TyStruct xs) (TyUnion kvs) Refl = No structNotUnion

-- [ Unions ]
decEq (TyUnion xs) TyLogic Refl = No (negEqSym logicNotUnion)
decEq (TyUnion xs) (TyArray type length) Refl = No (negEqSym arrayNotUnion)
decEq (TyUnion xs) (TyStruct kvs) Refl = No (negEqSym structNotUnion)

decEq (TyUnion xs) (TyUnion ys) Refl with (Fields.decEq xs ys)
  decEq (TyUnion xs) (TyUnion xs) Refl | (Yes Refl)   = Yes (Same Refl Refl)
  decEq (TyUnion xs) (TyUnion ys) Refl | (No  contra) = No (unionDifferBody contra)

-- [ Unit ]
decEq TyUnit TyUnit Refl = Yes (Same Refl Refl)

-- [ Gates ]
decEq TyGate TyGate Refl = Yes (Same Refl Refl)

-- [ Connections ]

decEq TyConn TyConn Refl = Yes (Same Refl Refl)

-- [ Ports ]
decEq (TyPort l dx sx wx tx ux) (TyPort l dy sy wy ty uy) Refl = Port.decEq (TyPort l dx sx wx tx ux) (TyPort l dy sy wy ty uy)

decEq (TyModule xs) (TyModule ys) Refl with (Ports.decEq xs ys)
  decEq (TyModule xs) (TyModule xs) Refl | (Yes Refl) = Yes (Same Refl Refl)
  decEq (TyModule xs) (TyModule ys) Refl | (No contra) = No (modBodyDiffer contra)

DecEqIdx MTy Ty where
  decEq x y prf = Equality.decEq x y prf

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
-- --------------------------------------------------------------- [ Stack.idr ]
-- Module    : Stack.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Testing Stacks using silly stupid tests
module Data.Test.Stack

import Test.Unit

import Data.Stack

%access export

covering
test2 : IO Bool
test2 = genericTest (Just "Pushing") (pushSThings [1,2,3] mkStack) [1,2,3] (==)

covering
test3 : IO Bool
test3 = genericTest (Just "Pushing Many") (pushSThings [1,2,3] (pushS 1 Nil)) [1,2,3,1] (==)

covering
test4 : IO Bool
test4 = genericTest (Just "Popping") (snd (popS [1,2,3]), fst (popS [1,2,3])) ([2,3],1) (==)

covering
runTest : IO ()
runTest = do
  putStrLn "Testing Stack"
  putStrLn infoLine
  NonReporting.runTests [
    genericTest (Just "Nothing") (the (Stack Nat) mkStack) (the (Stack Nat) Nil) (==)
  , test2
  , test3
  , test4
  ]

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers