text:
import Data.List.Views

rev : List a -> List a
rev xs with (snocList xs)
  rev [] | Empty = []
  rev (ys ++ [x]) | (Snoc y) = x :: rev ys | y

-- Show all the splits for all the recursive calls, to demonstrate they really
-- are split in half
showDivisions : (xs : List a) -> List (List a)
showDivisions xs with (splitRec xs)
  showDivisions [] | SplitRecNil = []
  showDivisions [x] | SplitRecOne = [[x]]
  showDivisions (ys ++ zs) | (SplitRecPair ysrec zsrec) =
    (ys ++ zs) :: showDivisions ys | ysrec ++ showDivisions zs | zsrec

total
mergeSort : Ord a => List a -> List a
mergeSort xs with (splitRec xs)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (ys ++ zs) | SplitRecPair ysrec zsrec
      = merge (mergeSort ys | ysrec)
              (mergeSort zs | zsrec)

testList : Int -> Int -> List Int -> List Int
testList 0 seed acc = acc
-- Need to explicitly mod since different back ends overflow differently
testList x seed acc = let seed' = (seed * 12345 + 768) `mod` 65536 in
                          testList (x - 1) seed'
                               ((seed' `mod` 100) :: acc)

myhead : List a -> a
myhead (x :: xs) = x

main : IO ()
main = do let list = testList 100 12345 []
          putStrLn "Sorting list"
          let list' = mergeSort list
          printLn list'
          printLn (rev list')

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
> module List.Operations

> import Data.List
> import Data.List.Quantifiers
> import Syntax.PreorderReasoning

> import Sigma.Sigma
> import Fun.Operations
> -- import NumRefinements
> import Rel.TotalPreorder
> import Rel.TotalPreorderOperations

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

* |List| is a functor:

> ||| fmap
> fmap : {A, B : Type} -> (A -> B) -> List A -> List B
> fmap = map

* |List| is a monad:

> ||| ret
> ret : {A : Type} -> A -> List A
> ret = pure

> ||| bind
> bind : {A, B : Type} -> List A -> (A -> List B) -> List B
> bind = (>>=)

* |List| is a container monad:

> |||
> NonEmpty    : {A : Type} -> List A -> Type
> NonEmpty  Nil      = Void
> NonEmpty (a :: as) = Unit

> idThere : {A : Type} ->
>           (a : A) -> (as : List A) ->
>           Sigma A (\ x => x `Elem` as) -> Sigma A (\ x => x `Elem` (a :: as))
> idThere a as (MkSigma x p) = MkSigma x (There p)

> ||| Tagging
> tagElem  :  {A : Type} -> (as : List A) -> List (Sigma A (\ a => a `Elem` as))
> tagElem Nil = Nil
> tagElem {A} (x :: xs) = (MkSigma x Here) :: (map (idThere x xs) (tagElem xs))

* Show

> implementation Show (Elem a as) where
>   show = show' where
>     show' : {A : Type} -> {a : A} -> {as : List A} -> Elem a as -> String
>     show'  Here     = "Here"
>     show' (There p) = "There" ++ show' p

> showlong : Show a => List a -> String
> showlong xs = "  [" ++ show' "" xs ++ "]" where
>   show' acc []        = acc
>   show' acc [x]       = acc ++ show x
>   show' acc (x :: xs) = show' (acc ++ show x ++ ",\n" ++ "   ") xs

* Reduction operators

> |||
> max : {A : Type} -> {R : A -> A -> Type} ->
>       TotalPreorder R -> (as : List A) -> List.Operations.NonEmpty as -> A
> max tp       Nil        p = absurd p
> max tp (a :: Nil)       _ = a
> max tp (a :: a' :: abs) _ with (max tp (a' :: abs) ())
>   | m with (totalPre tp a m)
>     | (Left _)  = m
>     | (Right _) = a

> |||
> argmaxMax : {A, B : Type} -> {R : B -> B -> Type} ->
>             TotalPreorder R -> (abs : List (A, B)) -> List.Operations.NonEmpty abs -> (A, B)
> argmaxMax tp       Nil                   p = absurd p
> argmaxMax tp ((a, b) :: Nil)             _ = (a, b)
> argmaxMax tp ((a, b) :: (a', b') :: abs) _ with (argmaxMax tp ((a', b') :: abs) ())
>   | (argmax, max) with (totalPre tp b max)
>     | (Left _)  = (argmax, max)
>     | (Right _) = (a, b)

> |||
> min : {A : Type} -> {R : A -> A -> Type} ->
>       TotalPreorder R -> (as : List A) -> List.Operations.NonEmpty as -> A
> {-
> min tp       Nil        p = absurd p
> min tp (a :: Nil)       _ = a
> min tp (a :: a' :: abs) _ with (min tp (a' :: abs) ())
>   | m with (totalPre tp a m)
>     | (Left _)  = a
>     | (Right _) = m
> -}
> min tp       Nil        p = absurd p
> min tp (a :: Nil)       _ = a
> min tp (a :: a' :: abs) _ with (totalPre tp a a')
>   | (Left  _) = assert_total (min tp (a  :: abs) ())
>   | (Right _) = assert_total (min tp (a' :: abs) ())

> |||
> argminMin : {A, B : Type} -> {R : B -> B -> Type} ->
>             TotalPreorder R -> (abs : List (A, B)) -> List.Operations.NonEmpty abs -> (A, B)
> argminMin tp       Nil                   p = absurd p
> argminMin tp ((a, b) :: Nil)             _ = (a, b)
> argminMin tp ((a, b) :: (a', b') :: abs) _ with (argminMin tp ((a', b') :: abs) ())
>   | (argmin, min) with (totalPre tp b min)
>     | (Left _)  = (a, b)
>     | (Right _) = (argmin, min)

> {-

> |||
> argmaxMax : {A, B : Type} -> TotalPreorder B -> (abs : List (A, B)) -> List.Operations.NonEmpty abs -> (A, B)
> argmaxMax tp       Nil                   p = absurd p
> argmaxMax tp ((a, b) :: Nil)             _ = (a, b)
> argmaxMax tp ((a, b) :: (a', b') :: abs) _ with (argmaxMax tp ((a', b') :: abs) ())
>   | (argmax, max) with (totalPre tp b max)
>     | (Left _)  = (argmax, max)
>     | (Right _) = (a, b)

> |||
> argminMin : {A, B : Type} -> TotalPreorder B -> (abs : List (A, B)) -> List.Operations.NonEmpty abs -> (A, B)
> argminMin tp       Nil                   p = absurd p
> argminMin tp ((a, b) :: Nil)             _ = (a, b)
> argminMin tp ((a, b) :: (a', b') :: abs) _ with (argminMin tp ((a', b') :: abs) ())
>   | (argmin, min) with (totalPre tp b min)
>     | (Left _)  = (a, b)
>     | (Right _) = (argmin, min)

> -}

> |||
> sumMapSnd : {A, B : Type} -> (Num B) => List (A, B) -> B
> sumMapSnd abs = sum (map snd abs)

> |||
> mapIdRightMult : {A, B : Type} -> (Num B) => (List (A, B), B) -> List (A, B)
> mapIdRightMult (abs, b) = map (cross id (* b)) abs

> |||
> mvMult : {A, A', B : Type} -> (Num B) => List (A, B) -> (A -> List (A', B)) -> List (A', B)
> mvMult abs f = concat (map (mapIdRightMult . (cross f id)) abs)
> -- mvMult            Nil  f = Nil
> -- mvMult ((a, b) :: abs) f = mapIdRightMult (f a, b) ++ mvMult abs f

> |||
> prods : {B : Type} -> (Num B) => List (B, B) -> List B
> prods = map (uncurry (*))

> |||
> sumProds : {B : Type} -> (Num B) => List (B, B) -> B
> sumProds Nil = 0
> sumProds ((b,b') :: bbs) = b * b' + sumProds bbs

* Filtering

> ||| Filters a list on a decidable property and pairs elements with proofs
> filterTagSigma : {A : Type} ->
>                  {P : A -> Type} ->
>                  ((a : A) -> Dec (P a)) ->
>                  List A ->
>                  List (Sigma A P)
> filterTagSigma d1P Nil = Nil
> filterTagSigma d1P (a :: as) with (filterTagSigma d1P as)
>   | tail with (d1P a)
>     | (Yes p) = (MkSigma a p) :: tail
>     | (No  _) = tail

> ||| Filters a list on a decidable property and pairs elements with proofs
> filterTagSubset : {A : Type} ->
>                   {P : A -> Type} ->
>                   ((a : A) -> Dec (P a)) ->
>                   List A ->
>                   List (Subset A P)
> filterTagSubset d1P Nil = Nil
> filterTagSubset d1P (a :: as) with (filterTagSubset d1P as)
>   | tail with (d1P a)
>     | (Yes p) = (Element a p) :: tail
>     | (No  _) = tail

* Ad-hoc filtering

> |||
> discardZeroes : {B : Type} -> (Num B, DecEq B) => List B -> List B
> discardZeroes  Nil      = Nil
> discardZeroes (b :: bs) with (decEq b 0)
>   | (Yes _) = discardZeroes bs
>   | (No _)  = b :: discardZeroes bs

> |||
> discardBySndZero : {A, B : Type} -> (Num B, DecEq B) => List (A, B) -> List (A, B)
> discardBySndZero  Nil      = Nil
> discardBySndZero (ab :: abs) with (decEq (snd ab) 0)
>   | (Yes _) = discardBySndZero abs
>   | (No _)  = ab :: discardBySndZero abs

> |||
> discardBySndZeroEq : {A, B : Type} -> (Num B, Eq B) => List (A, B) -> List (A, B)
> discardBySndZeroEq  Nil      = Nil
> discardBySndZeroEq (ab :: abs) with ((snd ab) == 0)
>   |  True = discardBySndZeroEq abs
>   | False = ab :: discardBySndZeroEq abs

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module printtest

printLength : IO ()
printLength = getLine >>= (\x => putStrLn (show (Strings.length x)))

printLarger: IO ()
printLarger =
  do
    first <- getLine
    second <- getLine
    let larger:Nat = case compare (length first) (length second) of
             GT => length first
             EQ => length first
             LT => length second
    putStrLn (show larger)

printLarger2: IO ()
printLarger2 = getLine >>= \first =>
               getLine >>= \second =>
                           let larger:Nat = case compare (length first) (length second) of
                                     GT => length first
                                     EQ => length first
                                     LT => length second in
                            putStrLn (show larger)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Main

%default total

%logging declare.data.parameters 20
%logging eval.eta 10

-- explicit
data Value : (value : Nat -> Type) -> Type where
  EmptyV : {0 value : Nat -> Type} -> Value (\ n => value n)

data TValue : Nat -> Type where
  MkTupleV : Value (\n => TValue n) -> TValue n


text:
> module FastSimpleProb.MonadicPostulates

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.Functor
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import Functor.Predicates

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

* On |fmap| and |rescale|:

> postulate
> fmapRescaleLemma : {A : Type} ->
>                    (f : A -> NonNegDouble) ->
>                    (p : NonNegDouble) -> (pp : Positive (toDouble p)) ->
>                    (sp : SimpleProb A) ->
>                    rescale p pp (fmap f sp) = fmap f (rescale p pp sp)

> postulate
> naturalRescale : (p : NonNegDouble) -> (pp : Positive (toDouble p)) ->
>                  Natural (rescale p pp)

* On |fmap| and |normalize|:

> postulate
> fmapNormalizeLemma : {A, B : Type} ->
>                      (f : A -> B) ->
>                      (sp : SimpleProb A) ->
>                      normalize (fmap f sp) = fmap f (normalize sp)

> postulate
> naturalNormalize : Natural normalize


text:
import NewEden.Natural
import NewEden.Implementations.Int64

{- Int64

   At present, this is pretty much completely worthless, as Idris doesn't have
   unboxed primitives, which means you're not gaining any practically significant
   performance by using this over GMP integers.

   But hopefully in the future they'll be available. Along with unboxed arrays.

-}

x : Natural Int64
x = 1024

y : Natural Int64
y = 12345

z : Natural Int64
z = x * y + y * x

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module Data.Bytes.Strict.API

import public Data.Bytes.Strict.Internal
import public Data.Bytes.Prim
import        Data.Bytes.Util

import Data.Word.Word8

import Data.List -- List.drop

moduleName : String
moduleName = "Data.Bytes.Strict.API"

%hide Prelude.empty

%default total

---------------------------------------------------------------------
-- Documentation
---------------------------------------------------------------------
{-

Pretty standard (strict) ByteString kind of stuff. Some operations have `'`
(prime) versions with slightly different behavior for convenience. In
particular operations which require `NonEmpty` proof have their `'` versions
give runtime errors on bad inputs instead. And things like replicate' use Int
instead of Nat.

This is to support what I consider the Idris community spirit: be provably safe
when it can be made convenient, but don't force anyone to jump through hoops.
I'm sure there's better wording for that though.

Included are some intended complexity values. They might be a lie since I don't
understand complexity very well. Hopefully they're in the ballpark, which is
all big-o is anyway.

Open Design Questions:

Is there a reason to allow negative position values in a Bytes? If we were
using pointers there might be some cute things we could do with that but
overall it doesn't really seem useful.
If we can get Nat or Fin to compile to Int, instead of the Integer that Nat
compiles to, then Nat for both fields of Bytes makes sense.

https://hackage.haskell.org/package/bytestring-0.10.10.0/docs/src/Data.ByteString.Internal.html#concat
Should helpers take all their arguments explicitly to avoid capturing as much
in closures? Does this even happen in idris?

Should things like replicate and unfoldrN simply cast their Nat and then call
to replicate'/unfoldrN' ? If that's the case is there any advantage to
providing them, aside from reducing cast noise for users?

Should functions that return List return lazy Lists?

If you feel something is missing from the API it might not be! Internal modules
implement common interfaces, be sure to check there first. e.g. <+>
-}

-- All of this will get fancier as Idris2 gains support for documentation
-- generation.

---------------------------------------------------------------------
-- API
---------------------------------------------------------------------

-------------------------------------------------
-- Barebones basic Bytes
-------------------------------------------------

-- Intended complexity: O(1)
export
empty : Bytes
empty = neutral

-- Intended complexity: O(1)
-- Provides NonEmpty
export
singleton : Word8 -> Bytes
singleton w = unsafeCreateBytes 1 $ \p => setByte p 0 w

private
packLenBytes : Int -> List Word8 -> Bytes
packLenBytes len xs0
    = unsafeCreateBytes len $ \b => go 0 b xs0
  where
    go : Int -> MutBlock -> List Word8 -> IO ()
    go p buf [] = pure ()
    go p buf (x::xs) = setByte buf p x *> go (p+1) buf xs

-- Intended complexity: O(n)
export
pack : List Word8 -> Bytes
pack xs = packLenBytes (cast (length xs)) xs

-- Intended complexity: O(n)
export
unpack : Bytes -> List Word8
unpack (MkB fp pos len) =
  take (intToNat len) . drop (intToNat pos)
                      . unsafePerformIO . blockData $ fp

-------------------------------------------------
-- Basic interface
-------------------------------------------------

-- Intended complexity: O(1)
total
length : Bytes -> Int
length (MkB _ _ len) = len

-- Intended complexity: O(1)
export
total
null : Bytes -> Bool
null buf = 0 >= length buf

-- Intended complexity: O(1)
export
cons : Word8 -> Bytes -> Bytes
cons x (MkB p0 pos len)
    = do unsafeCreateBytes (1 + len) $ \p => do
         setByte p 0 x
         copyBlock p0 pos len p 1

-- Intended complexity: O(1)
export
snoc : Bytes -> Word8 -> Bytes
snoc (MkB p0 pos len) x
  = unsafeCreateBytes (1 + len) $ \p => do
      copyBlock p0 pos len p 0
      setByte p len x

-- Intended complexity: O(1)
export
head : (b : Bytes) -> NonEmpty b => Word8
head (MkB b pos _) = unsafePerformIO (getByte b pos)

export
partial
head' : (b : Bytes) -> Word8
head' (MkB b pos len) = if 0 >= len
  then errorCall moduleName "head'" "block empty"
  else unsafePerformIO (getByte b pos)

-- Intended complexity: O(1)
export
tail : (b : Bytes) -> NonEmpty b => Bytes
tail (MkB p pos len) = MkB p (1 + pos) (len - 1)

export
partial
tail' : Bytes -> Bytes
tail' (MkB p pos len) = if len > 0
                          then MkB p (1 + pos) (len - 1)
                          else errorCall moduleName "tail'" "block empty"

-- Intended complexity: O(1)
export
uncons : (b : Bytes) -> NonEmpty b => (Word8, Bytes)
uncons bs = (head bs, tail bs)

export
uncons' : Bytes -> Maybe (Word8, Bytes)
uncons' bs@(MkB _ _ len) = if len > 0
                             then Just ( assert_total $ head' bs
                                       , assert_total $ tail' bs)
                             else Nothing

export
partial
uncons'' : Bytes -> (Word8, Bytes)
uncons'' bs@(MkB _ _ len)
  = if len > 0
      then (head' bs, tail' bs)
      else errorCall moduleName "uncons''" "block empty"

-- Intended complexity: O(1)
export
last : (b : Bytes) -> NonEmpty b => Word8
last (MkB p pos len) = unsafePerformIO (getByte p (len + pos - 1))

export
partial
last' : Bytes -> Word8
last' (MkB p pos len) = if len > 0
                          then unsafePerformIO (getByte p (len + pos - 1))
                          else errorCall moduleName "last'" "block empty"

-- Intended complexity: O(1)
export
init : (b: Bytes) -> NonEmpty b => Bytes
init (MkB p pos len) = MkB p pos (len - 1)

export
partial
init' : Bytes -> Bytes
init' (MkB p pos len) = if len > 0
                        then MkB p pos (len - 1)
                        else errorCall moduleName "init'" "block empty"

-- Intended complexity: O(1)
export
unsnoc : (b : Bytes) -> NonEmpty b => (Bytes, Word8)
unsnoc bs = (init bs, last bs)

export
unsnoc' : Bytes -> Maybe (Bytes, Word8)
unsnoc' bs@(MkB _ _ len) = if len > 0
                             then Just ( assert_total $ init' bs
                                       , assert_total $ last' bs)
                             else Nothing

export
partial
unsnoc'' : Bytes -> (Bytes, Word8)
unsnoc'' bs@(MkB _ _ len) = if len > 0
                              then (init' bs, last' bs)
                              else errorCall moduleName "unsnoc''" "block empty"

-------------------------------------------------
-- Transforms
-------------------------------------------------

-- Intended complexity: O(n)
export
reverse : Bytes -> Bytes
reverse b@(MkB buf pos len) = unsafeCreateBytes len $ \new =>
    rev_ 0 (len - 1) new
  where
    rev_ : Int -> Int -> MutBlock -> IO ()
    rev_ p q new = if 0 > q
      then pure ()
      else do
        x <- getByte buf (pos + p)
        setByte new q x
        assert_total $ rev_ (p+1) (q-1) new

sort : Bytes -> Bytes

intersperse : Word8 -> Bytes -> Bytes

intercalate : Bytes -> List Bytes -> Bytes

transpose : List Bytes -> List Bytes

export
stringToBytes : String -> Int -> (Bytes,Int)
stringToBytes str len = unsafeCreateNBytes' len $ \b => do
    (_,r) <- fef b (unpack str) 0
    pure (r,r)
  where
    fef : MutBlock -> List Char -> Int -> IO (MutBlock, Int)
    fef bs [] pos = pure (bs,pos)
    fef bs (c :: cs) pos = if len > pos
      then setByte bs pos (cast (cast {to=Int} c)) *> fef bs cs (pos+1)
      else pure (bs, pos)

-------------------------------------------------
-- Folding
-------------------------------------------------

-- Intended complexity: O(n)
export
foldl : (a -> Word8 -> a) -> a -> Bytes -> a
foldl f v (MkB b pos len)
    = unsafePerformIO $ go v pos (len + pos)
  where
    go : a -> (start : Int) -> (end : Int) -> IO a
    go z p q
      = if p >= q then pure z
                  else assert_total $ go (f z !(getByte b p)) (p+1) q

-- TODO: consider foldl', foldl with a lazy accumulator

foldl1 : (Word8 -> Word8 -> Word8) -> (b : Bytes) -> NonEmpty b => Word8
foldl1 f b = foldl f (head b) (tail b)

partial
foldl1' : (Word8 -> Word8 -> Word8) -> (b : Bytes) -> Word8
foldl1' f b = foldl f (head' b) (tail'
 b)

-- Intended complexity: O(n)
export
foldr : (Word8 -> a -> a) -> a -> Bytes -> a
foldr f v (MkB bs pos len)
    = unsafePerformIO $ go v pos (len + pos - 1)
  where
    go : a -> (start : Int) -> (end : Int) -> IO a
    go z p q
      = if p > q then pure z
                 else assert_total $ go (f !(getByte bs q) z) p (q-1)

-- TODO: consider foldr', foldr with a lazy accumulator

foldr1 : (Word8 -> Word8 -> Word8) -> (b : Bytes) -> NonEmpty b => Word8
foldr1 f b = foldr f (last b) (init b)

partial
foldr1' : (Word8 -> Word8 -> Word8) -> Bytes -> Word8
foldr1' f b = foldr f (last' b) (init' b)

concat : List Bytes -> Bytes

concatMap : (Word8 -> Bytes) -> Bytes -> Bytes

-------------------------------------------------
-- Mapping
-------------------------------------------------

-- Intended complexity: O(n)
export
map : (Word8 -> Word8) -> Bytes -> Bytes
map f (MkB b0 pos len)
    = unsafeCreateBytes len $ \new => map_ 0 len new
  where
    map_ : (pos1 : Int) -> (pos2 : Int) -> MutBlock -> IO ()
    map_ p q buf = if p >= q then pure ()
                             else do
                               x <- getByte b0 (pos + p)
                               setByte buf p (f x)
                               assert_total $ map_ (p+1) q buf

-- foldl with a state passed along
mapAccumL : (s -> Word8 -> (s, Word8)) -> s -> Bytes -> (s, Bytes)

-- foldr with a state passed along
mapAccumR : (s -> Word8 -> (s, Word8)) -> s -> Bytes -> (s, Bytes)

-------------------------------------------------
-- Scans
-------------------------------------------------

scanl : (Word8 -> Word8 -> Word8) -> Word8 -> Bytes -> Bytes
scanl1 : (Word8 -> Word8 -> Word8) -> (b : Bytes) -> NonEmpty b => Bytes
scanl1' : (Word8 -> Word8 -> Word8) -> Bytes -> Bytes

scanr : (Word8 -> Word8 -> Word8) -> Word8 -> Bytes -> Bytes
scanr1 : (Word8 -> Word8 -> Word8) -> (b : Bytes) -> NonEmpty b => Bytes
scanr1' : (Word8 -> Word8 -> Word8) -> Bytes -> Bytes

-------------------------------------------------
-- Generate Bytes
-------------------------------------------------

-- This can be written faster with a primitive like memset, should backends be
-- inclined to provide one?
-- Like replicate for List and elsewhere negative values are treated as 0.
replicate' : Int -> Word8 -> Bytes
replicate' n w = if n > 0
                   then map (const w) $ unsafeCreateBytes n $ (\_ => pure ())
                   else neutral

-- Why does a Nat version exist you ask? To make safety painless. People are
-- hopefully going to be using Nat all over their programs for safety reasons
-- so we want to support that easily. The user littering their code with casts
-- can get tedious so we'll support that for them here. That being said,
-- replicate' exists for when you're using Int anyway and especially if that's
-- due to performance, note that Nat compiles to Integer which (depending on
-- the backend) can be slower than Int.
-- TODO: should this case on Nat or is a cast fine? What does casing gain us?
replicate : Nat -> Word8 -> Bytes
replicate n w = replicate' (cast n) w

unfoldr : (a -> Maybe (Word8, a)) -> a -> Bytes

unfoldrN : Nat -> (a -> Maybe (Word8, a)) -> a -> (Bytes, Maybe a)

unfoldrN' : Int -> (a -> Maybe (Word8, a)) -> a -> (Bytes, Maybe a)

-------------------------------------------------
-- Splitting Bytes
-------------------------------------------------

take' : Int -> Bytes -> Bytes
take  : Nat -> Bytes -> Bytes

drop' : Int -> Bytes -> Bytes
drop  : Nat -> Bytes -> Bytes

splitAt' : Int -> Bytes -> (Bytes, Bytes)
splitAt  : Nat -> Bytes -> (Bytes, Bytes)

takeWhile : (Word8 -> Bool) -> Bytes -> Bytes
dropWhile : (Word8 -> Bool) -> Bytes -> Bytes

span  : (Word8 -> Bool) -> Bytes -> (Bytes, Bytes)
spanEnd  : (Word8 -> Bool) -> Bytes -> (Bytes, Bytes) -- starts from end

-- Should I really provide break when a person can just write not?
-- Might as well, for the same reason that we provide Nat and Int versions.
break : (Word8 -> Bool) -> Bytes -> (Bytes, Bytes)
breakEnd  : (Word8 -> Bool) -> Bytes -> (Bytes, Bytes) -- starts from end

-- potentially faster than groupBy (==), depends how we write this
group : Bytes -> List Bytes

groupBy : (Word8 -> Word8 -> Bool) -> Bytes -> List Bytes

inits : Bytes -> List Bytes
tails : Bytes -> List Bytes

-- TODO: Is this really common enough a need to include?
-- returns 2nd Bytes stripped of 1st Bytes iff 1st is a prefix of 2nd
stripPrefix : Bytes -> Bytes -> Maybe Bytes

-- Same, but from the other end.
stripSuffix : Bytes -> Bytes -> Maybe Bytes

-- split on, and consume, each occurence of Word8
split : Word8 -> Bytes -> List Bytes

-- same as above with predicate to determine delimiter
splitWith : (Word8 -> Bool) -> Bytes -> List Bytes

-------------------------------------------------
-- Predicates
-------------------------------------------------

any : (Word8 -> Bool) -> Bytes -> Bool
all : (Word8 -> Bool) -> Bytes -> Bool

isPrefixOf : Bytes -> Bytes -> Bool
isSuffixOf : Bytes -> Bytes -> Bool
isInfixOf  : Bytes -> Bytes -> Bool

-------------------------------------------------
-- Searches
-------------------------------------------------

-- TODO: needs more fitting name, even though yes we have a string of bytes in
-- memory.
-- Like break but we're breaking on a Bytes instead of a Word8. Examples:
{-
breakSubstring [3,4]     [1,2,3,4,5] ~ ([1,2],[3,4,5])
breakSubstring [3]       [1,2,3,4,5] ~ ([1,2],[3,4,5])
breakSubstring [3,4,5,6] [1,2,3,4,5] ~ ([1,2,3,4,5],[]) -- NB
breakSubstring [6]       [1,2,3,4,5] ~ ([1,2,3,4,5],[])
-}
-- This is likely to be a big player when you go to write parsers for Bytes
breakSubstring : Bytes -> Bytes -> (Bytes, Bytes)

elem : Word8 -> Bytes -> Bool

-- notElem is a common enough need to provide it for users so they don't have
-- to compose `not`
notElem : Word8 -> Bytes -> Bool

maximum :  Bytes -> Word8
minimum :  Bytes -> Word8

find : (Word8 -> Bool) -> Bytes -> Maybe Word8

filter : (Word8 -> Bool) -> Bytes -> Bytes

partition : (Word8 -> Bool) -> Bytes -> (Bytes, Bytes)

-------------------------------------------------
-- Indexing
-------------------------------------------------

-- NB: Best to avoid the Nat returning options until we have a primitive cast
-- for it to Int.

index : Bytes -> Nat -> Word8

index' : Bytes -> Int -> Word8

elemIndex  : Word8 -> Bytes -> Maybe Nat
elemIndex' : Word8 -> Bytes -> Maybe Int

elemIndices  : Word8 -> Bytes -> List Nat
elemIndices' : Word8 -> Bytes -> List Int

elemIndexEnd  : Word8 -> Bytes -> Maybe Nat
elemIndexEnd' : Word8 -> Bytes -> Maybe Int

findIndex  : (Word8 -> Bool) -> Bytes -> Maybe Nat
findIndex' : (Word8 -> Bool) -> Bytes -> Maybe Int

count  : Word8 -> Bytes -> Nat
count' : Word8 -> Bytes -> Int

-------------------------------------------------
-- Zips
-------------------------------------------------

-- analogous to zip for List
zip : Bytes -> Bytes -> List (Word8, Word8)

zipWith : (Word8 -> Word8 -> a) -> Bytes -> Bytes -> List a

unzip : List (Word8, Word8) -> (Bytes, Bytes)


text:
import Data.List
import Data.Stream

-- the built in sort function is an implementation of merge sort (for now at least)

lincong : Integral a => a -> Stream a
lincong = tail . (iterate (\n => (1103515245 * n + 12345) `mod` 2147483648))

randishInts : Nat -> Integer -> List Integer
randishInts size seed = take size $ lincong seed

mylast : List a -> Maybe a
mylast [] = Nothing
mylast [x] = Just x
mylast (x::xs) = mylast xs

doSort : Nat -> IO ()
doSort Z     = putStrLn "Done"
doSort (S k) = do let xs = sort $ randishInts 12000 $ natToInteger k
                  -- get last elem to make sure compiler doesn't optimise away the sort
                  putStrLn $ show $ mylast xs
                  doSort k

main : IO ()
main = do max <- getLine
          doSort (integerToNat (cast max))


text:
-- File containing all types used in form processing, and associated instances
module IdrisWeb.Form.FormTypes
import Decidable.Equality
import SQLite
import Parser
%access public

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module      : UML.Deployment.Model
-- Description : Model for textual UML deployment diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Deployment.Model

%access public

||| The different types of device type supported.
data DeviceTy = GenericDev | Server | Workstation | Mobile | Embedded

-- ReThink
||| The different types of execution environments supported.
data EnvTy = OS | Engine | Container | AppServer | App

||| The different types of artifacts supported.
data ArtifactTy = Document | Source | Library | Executable | Script

||| Key value pair.
Attribute : Type
Attribute = (String, String)

||| Key value pairs.
Attributes : Type
Attributes = List Attribute

data ElemTy = SPEC | ARTIFACT | ENV | DEVICE | RELA | MODEL

-- ------------------------------------------------------------------- [ Model ]

||| A model for UML Deployment Diagrams.
data DeploymentModel : ElemTy -> Type where
  ||| Description of a named deployment specification for artifacts.
  |||
  ||| @ident The name of the deployment specification,
  ||| @as The specification as KV pairs.
  Spec : (ident : String)
         -> (as : Attributes) -> DeploymentModel SPEC

  ||| Resources that are to be deployed in execution environments on devices.
  |||
  ||| @ty The type of artifact.
  ||| @ident The identify of the artifact.
  ||| @spec A possible specification schema that describes deployment.
  Artifact : (ty : ArtifactTy)
             -> (ident : String)
             -> (spec : Maybe (DeploymentModel SPEC))
             -> DeploymentModel ARTIFACT

  ||| A execution environment in which artifacts are run or hosted.
  |||
  ||| @ty The type of environment.
  ||| @ident The identity of the environment.
  ||| @as The artifacts being executed/hosted within the environment.
  ||| @ps A possible set of properties for the environment.
  Env : (ty : EnvTy)
      -> (ident : String)
      -> (as : List $ DeploymentModel ARTIFACT)
      -> (ps : Maybe Attributes)
      -> DeploymentModel ENV

  ||| A physical device in the deployment diagram.
  |||
  ||| @ty The type of the device.
  ||| @ident The identity of the device.
  ||| @es The execution environments hosted on the device.
  ||| @as A possible list of tags describing details over the device.
  Device : (ty : DeviceTy)
         -> (ident : String)
         -> (es : List $ DeploymentModel ENV)
         -> (as : Maybe Attributes)
         -> DeploymentModel DEVICE

  ||| Describes how different devices, and different execution environments, talk to each other.relation between two nodes.
  |||
  ||| @nodeA A device.
  ||| @nodeB The other device being communicated with.
  ||| @protocol The protocol being used for communication.
  Relation : (nodeA : String)
            -> (nodeB : String)
            -> (protocol : String)
            -> DeploymentModel RELA

  ||| A model for UML Deployment Diagrams.
  |||
  ||| @ds The physical devices.
  ||| @rs The relations between the devices.
  MkDeployment : (ds : List $ DeploymentModel DEVICE)
               -> (rs : List $ DeploymentModel $ RELA)
               -> DeploymentModel MODEL

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

instance Eq DeviceTy where
  (==) GenericDev   GenericDev  = True
  (==) Server       Server      = True
  (==) Workstation  Workstation = True
  (==) Mobile       Mobile      = True
  (==) Embedded     Embedded    = True
  (==) _            _           = False

instance Eq EnvTy where
  (==) OS         OS        = True
  (==) Engine     Engine    = True
  (==) Container  Container = True
  (==) AppServer  AppServer = True
  (==) App        App       = True
  (==) _          _         = False

instance Eq ArtifactTy where
  (==) Document     Document   = True
  (==) Source       Source     = True
  (==) Library      Library    = True
  (==) Executable   Executable = True
  (==) Script       Script     = True
  (==) _            _          = False

mutual

  %assert_total
  eqDepModel : (DeploymentModel x) -> (DeploymentModel x) -> Bool
  eqDepModel (MkDeployment xds xrs) (MkDeployment yds yrs) = xds == yds && xrs == yrs
  eqDepModel (Spec x xs)            (Spec y ys)            = x == y && xs == ys
  eqDepModel (Artifact xTy x xs)    (Artifact yTy y ys)    = xTy == yTy && x == y && xs == ys
  eqDepModel (Env xTy x xs xxs)     (Env yTy y ys yys)     = xTy == yTy && x == y && xs == ys && xxs == yys
  eqDepModel (Device xTy x xs xxs)  (Device yTy y ys yys)  = xTy == yTy && x == y && xs == ys && xxs == yys
  eqDepModel (Relation xa xb xp)    (Relation ya yb yp)    = xa == ya && xb == yb && xp == yp
  eqDepModel _                      _                      = False

  instance Eq (DeploymentModel x) where
    (==) = eqDepModel
-- -------------------------------------------------------------------- [ Show ]

instance Show DeviceTy where
  show GenericDev  = "Generic"
  show Server      = "Server"
  show Workstation = "Workstation"
  show Mobile      = "Mobile"
  show Embedded    = "Embedded"

instance Show EnvTy where
  show OS        = "OS"
  show Engine    = "Engine"
  show Container = "Container"
  show AppServer = "AppServer"
  show App       = "App"

instance Show ArtifactTy where
  show Document   = "Document"
  show Source     = "Source"
  show Library    = "Library"
  show Executable = "Executable"
  show Script     = "Script"

instance Show (DeploymentModel x) where
  show (MkDeployment ds rs)     = unwords ["[DeployModel", show ds, show rs, "]"]
  show (Spec id as)             = unwords ["[Specification", show id, show as, "]"]
  show (Artifact ty id spec)    = unwords ["[Artifact", show ty, show id, show spec, "]"]
  show (Env ty id as ps)        = unwords ["[Env", show ty, show id, show as, show ps, "]"]
  show (Device ty id es as)     = unwords ["[Device", show ty, show id, show es, show as, "]"]
  show (Relation xID yID proto) = "[Relation " ++ xID ++ " " ++ yID ++ " " ++ proto ++ "]"

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
-- ----------------------------------------------------------- [ Serialise.idr ]
||| Module    : Serialise.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
||| How to serialise objects between two different types. A slightly
||| more sane version of `Cast`.
|||
||| We could call this class marshall but I am fond of the
||| connotations associated with Java's serializable interface.
module Commons.Data.Serialise

%access public export

-- ------------------------------------------------------------------ [ Errors ]

data SerialiseError : Type where
  EmptyString    : SerialiseError
  MalformedData  : (msg : String) -> (raw : String) -> SerialiseError
  IncompleteData : (msg : String) -> (raw : String) -> SerialiseError
  ReadingError   : (msg : String) -> (raw : String) -> SerialiseError

Show SerialiseError where
    show EmptyString              = "Given an empty string."
    show (MalformedData msg raw)  = unlines ["Malformed Data Error:",  msg, "Raw String:", raw]
    show (IncompleteData msg raw) = unlines ["Incomplete Data Error:", msg, "Raw String:", raw]
    show (ReadingError msg raw)   = unlines ["Reading Error:",         msg, "Raw String:", raw]

-- -------------------------------------------------------------- [ Definition ]

||| Serialise data of type `a` to data of type `b`.
interface Serialise a b where
  writeData : a -> b
  readData  : b -> Either SerialiseError a

-- ---------------------------------------------------------- [ Some instances ]

Serialise a a where
    writeData x = x
    readData  x = Right x

Serialise Int String where
  writeData x = show x
  readData  x = Right $ cast x

Serialise Nat String where
  writeData x = show x
  readData  x = Right $ cast x

Serialise Double String where
  writeData x = show x
  readData  x = Right $ cast x

Serialise Integer String where
  writeData x = show x
  readData  x = Right $ cast x

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
||| Functions for the processing of received request and
||| notifications.
|||
||| (C) The Idris Community, 2021
module Server.ProcessMessage

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.OneOf
import Data.SortedSet
import Idris.ModTree
import Idris.Package
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.IDEMode.Holes
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.AddClause
import Language.LSP.CodeAction.CaseSplit
import Language.LSP.CodeAction.ExprSearch
import Language.LSP.CodeAction.RefineHole
import Language.LSP.CodeAction.GenerateDef
import Language.LSP.CodeAction.MakeCase
import Language.LSP.CodeAction.MakeLemma
import Language.LSP.CodeAction.MakeWith
import Language.LSP.Definition
import Language.LSP.DocumentSymbol
import Language.LSP.SignatureHelp
import Language.LSP.Message
import Libraries.Data.PosMap
import Libraries.Utils.Path
import Server.Capabilities
import Server.Configuration
import Server.Log
import Server.QuickFix
import Server.SemanticTokens
import Server.Response
import Server.Utils
import System
import System.Clock
import System.Directory
import System.File
import Data.List1
import Libraries.Data.List.Extra

displayType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayType defs (n, i, gdef)
    = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
                pure (pretty !(aliasName (fullname gdef)) <++> colon <++> prettyTerm tm))
            (\num => reAnnotate Syntax <$> prettyHole defs [] n num (type gdef))
            (isHole gdef)

displayTerm : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> ClosedTerm ->
              Core (Doc IdrisAnn)
displayTerm defs tm
    = do ptm <- resugar [] !(normaliseHoles defs [] tm)
         pure (prettyTerm ptm)

isDirty : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool
isDirty uri = gets LSPConf (contains uri . dirtyFiles)

isError : Ref LSPConf LSPConfiguration => DocumentURI -> Core Bool
isError uri = gets LSPConf (contains uri . errorFiles)

loadURI : Ref LSPConf LSPConfiguration
       => Ref Ctxt Defs
       => Ref UST UState
       => Ref Syn SyntaxInfo
       => Ref MD Metadata
       => Ref ROpts REPLOpts
       => InitializeParams -> URI -> Maybe Int -> Core (Either String ())
loadURI conf uri version = do
  modify LSPConf (record {openFile = Just (uri, fromMaybe 0 version)})
  resetContext (Virtual Interactive)
  let fpath = uri.path
  let Just (startFolder, startFile) = splitParent fpath
    | Nothing => do let msg = "Cannot find the parent folder for \{show uri}"
                    logString Error msg
                    pure $ Left msg
  True <- coreLift $ changeDir startFolder
    | False => do let msg = "Cannot change current directory to \{show startFolder}, folder of \{show startFile}"
                  logString Error msg
                  pure $ Left msg
  Just fname <- findIpkg (Just fpath)
    | Nothing => do let msg = "Cannot find ipkg file for \{show uri}"
                    logString Error msg
                    pure $ Left msg
  Right res <- coreLift $ File.readFile fname
    | Left err => do let msg = "Cannot read file at \{show uri}"
                     logString Error msg
                     pure $ Left msg
  setSource res
  errs <- catch
            (buildDeps fname)
            (\err => do
              logString Debug "loadURI: caught error which shouldn't be leaked: \{show err}"
              pure [err])
  -- FIXME: the compiler always dumps the errors on stdout, requires
  --        a compiler change.
  -- NOTE on catch: It seems the compiler sometimes throws errors instead
  -- of accumulating them in the buildDeps.
  case errs of
    [] => pure ()
    (_::_) => modify LSPConf (record { errorFiles $= insert uri })
  resetProofState
  let caps = (publishDiagnostics <=< textDocument) . capabilities $ conf
  modify LSPConf (record { quickfixes = [], cachedActions = empty, cachedHovers = empty })
  traverse_ (findQuickfix caps uri) errs
  sendDiagnostics caps uri version errs
  pure $ Right ()

loadIfNeeded : Ref LSPConf LSPConfiguration
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref MD Metadata
            => Ref ROpts REPLOpts
            => InitializeParams -> URI -> Maybe Int -> Core (Either String ())
loadIfNeeded conf uri version = do
  Just (oldUri, oldVersion) <- gets LSPConf openFile
    | Nothing => loadURI conf uri version
  if (oldUri == uri && (isNothing version || (Just oldVersion) == version))
     then pure $ Right ()
     else loadURI conf uri version

withURI : Ref LSPConf LSPConfiguration
       => Ref Ctxt Defs
       => Ref UST UState
       => Ref Syn SyntaxInfo
       => Ref MD Metadata
       => Ref ROpts REPLOpts
       => InitializeParams
       -> URI -> Maybe Int -> Core (Either ResponseError a) -> Core (Either ResponseError a) -> Core (Either ResponseError a)
withURI conf uri version d k = do
  False <- isError uri | _ => d
  case !(loadIfNeeded conf uri version) of
       Right () => k
       Left err =>
         pure $ Left (MkResponseError (Custom 3) err JNull)

||| Guard for requests that requires a successful initialization before being allowed.
whenInitializedRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a)
whenInitializedRequest k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => pure $ Left $ serverNotInitialized

||| Guard for requests that cannot be sent after the shutdown protocol.
whenNotShutdownRequest : Ref LSPConf LSPConfiguration => Core (Either ResponseError a) -> Core (Either ResponseError a)
whenNotShutdownRequest k =
  if !(gets LSPConf isShutdown)
     then pure $ Left $ (invalidRequest "Server has been shutdown")
     else k

||| whenInitializedRequest + whenNotShutdownRequest
whenActiveRequest : Ref LSPConf LSPConfiguration => (InitializeParams -> Core (Either ResponseError a)) -> Core (Either ResponseError a)
whenActiveRequest = whenNotShutdownRequest . whenInitializedRequest

||| Guard for notifications that requires a successful initialization before being allowed.
whenInitializedNotification : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenInitializedNotification k =
  case !(gets LSPConf initialized) of
       Just conf => k conf
       Nothing => sendUnknownResponseMessage $ serverNotInitialized

||| Guard for notifications that cannot be sent after the shutdown protocol.
whenNotShutdownNotification : Ref LSPConf LSPConfiguration => Core () -> Core ()
whenNotShutdownNotification k =
  if !(gets LSPConf isShutdown)
     then sendUnknownResponseMessage $ (invalidRequest "Server has been shutdown")
     else k

||| whenInitializedNotification + whenNotShutdownNotification
whenActiveNotification : Ref LSPConf LSPConfiguration => (InitializeParams -> Core ()) -> Core ()
whenActiveNotification = whenNotShutdownNotification . whenInitializedNotification

export
handleRequest :
       Ref LSPConf LSPConfiguration
    => Ref Ctxt Defs
    => Ref UST UState
    => Ref Syn SyntaxInfo
    => Ref MD Metadata
    => Ref ROpts REPLOpts
    => (method : Method Client Request)
    -> (params : MessageParams method)
    -> Core (Either ResponseError (ResponseResult method))

handleRequest Initialize params = do
  -- TODO: Here we should analyze the client capabilities.

  case params.initializationOptions of
       Just (JObject xs) => do
         case lookup "logFile" xs of
              Just (JString fname) => changeLogFile fname
              Just _ => logString Error "Incorrect type for log file location, expected string"
              Nothing => pure ()
         case lookup "longActionTimeout" xs of
              Just (JNumber v) => setSearchTimeout $ cast v
              Just _ => logString Error "Incorrect type for long action timeout, expected number"
              Nothing => pure ()
         case lookup "maxCodeActionResults" xs of
              Just (JNumber v) => modify LSPConf (record { searchLimit = integerToNat $ cast v })
              Just _ => logString Error "Incorrect type for max code action results, expected number"
              Nothing => pure ()
       Just _ => logString Error "Incorrect type for initialization options"
       Nothing => pure ()

  modify LSPConf (record {initialized = Just params})
  pure $ pure $ MkInitializeResult serverCapabilities (Just serverInfo)

handleRequest Shutdown params = do
  -- In a future multithreaded model, we must guarantee that all pending request are still executed.
  update LSPConf (record {isShutdown = True})
  pure $ pure $ (the (Maybe Null) Nothing)

handleRequest TextDocumentHover params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ pure $ make $ MkNull
    withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
      Nothing <- gets LSPConf (map snd . head' . searchPos (cast params.position) . cachedHovers)
        | Just hover => do logString Debug "hover: found cached action"
                           pure $ pure $ make hover

      defs <- get Ctxt
      nameLocs <- gets MD nameLocMap

      let Just (loc, name) = findPointInTreeLoc (params.position.line, params.position.character) nameLocs
        | Nothing => pure $ pure $ (make $ MkHover (make $ MkMarkupContent PlainText "") Nothing)
      -- Lookup the name globally
      globals <- lookupCtxtName name (gamma defs)
      globalResult <- the (Core $ Maybe $ Doc IdrisAnn) $ case globals of
        [] => pure Nothing
        ts => do tys <- traverse (displayType defs) ts
                 pure $ Just (vsep tys)
      localResult <- findTypeAt $ anyWithName name $ within (params.position.line, params.position.character)
      line <- case (globalResult, localResult) of
        -- Give precedence to the local name, as it shadows the others
        (_, Just (n, _, type)) => pure $ renderString $ unAnnotateS $ layoutUnbounded $ pretty (nameRoot n) <++> colon <++> !(displayTerm defs type)
        (Just globalDoc, Nothing) => pure $ renderString $ unAnnotateS $ layoutUnbounded globalDoc
        (Nothing, Nothing) => pure ""
      let supportsMarkup = maybe False (Markdown `elem`) $ conf.capabilities.textDocument >>= .hover >>= .contentFormat
      let markupContent = the MarkupContent $ if supportsMarkup then MkMarkupContent Markdown $ "```idris\n" ++ line ++ "\n```" else MkMarkupContent PlainText line
      let hover = MkHover (make markupContent) Nothing
      modify LSPConf (record { cachedHovers $= insert (cast loc, hover) })
      pure $ pure (make hover)

handleRequest TextDocumentDefinition params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ pure $ make $ MkNull
    withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
      Just link <- gotoDefinition params | Nothing => pure $ pure $ make MkNull
      pure $ pure $ make link

handleRequest TextDocumentCodeAction params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ pure $ make $ MkNull
    withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
      quickfixActions <- map Just <$> gets LSPConf quickfixes
      exprSearchAction <- map Just <$> exprSearch params
      splitAction <- caseSplit params
      lemmaAction <- makeLemma params
      withAction <- makeWith params
      clauseAction <- addClause params
      makeCaseAction <- handleMakeCase params
      generateDefAction <- map Just <$> generateDef params
      refineHoleAction <- map Just <$> refineHole params
      let resp = flatten $ quickfixActions ++ refineHoleAction
                             ++ [splitAction, lemmaAction, withAction, clauseAction, makeCaseAction]
                             ++ generateDefAction ++ exprSearchAction
      pure $ pure $ make resp
      where
        flatten : List (Maybe CodeAction) -> List (OneOf [Command, CodeAction])
        flatten [] = []
        flatten (Nothing :: xs) = flatten xs
        flatten ((Just x) :: xs) = make x :: flatten xs

handleRequest TextDocumentSignatureHelp params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ pure $ make $ MkNull
    withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
      Just signatureHelpData <- signatureHelp params | Nothing => pure $ pure $ make MkNull
      pure $ pure $ make signatureHelpData

handleRequest TextDocumentDocumentSymbol params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ pure $ make $ MkNull
    withURI conf params.textDocument.uri Nothing (pure $ pure $ make $ MkNull) $ do
      documentSymbolData <- documentSymbol params
      pure $ pure $ make documentSymbolData

handleRequest TextDocumentCodeLens params = whenActiveRequest $ \conf =>
    pure $ pure $ make MkNull

handleRequest TextDocumentCompletion params = whenActiveRequest $ \conf =>
    pure $ pure $ make MkNull

handleRequest TextDocumentDocumentLink params = whenActiveRequest $ \conf =>
    pure $ pure $ make MkNull

handleRequest TextDocumentSemanticTokensFull params = whenActiveRequest $ \conf => do
    False <- isDirty params.textDocument.uri
      | True => pure $ Left (MkResponseError RequestCancelled "Document Dirty" JNull)
    False <- gets LSPConf (contains params.textDocument.uri . semanticTokensSentFiles)
      | True => pure $ Left (MkResponseError RequestCancelled "Semantic tokens already sent" JNull)
    withURI conf params.textDocument.uri Nothing (pure $ Left (MkResponseError RequestCancelled "Document Errors" JNull)) $ do
      md <- get MD
      src <- getSource
      let srcLines = forget $ lines src
      let getLineLength = \lineNum => maybe 0 (cast . length) $ elemAt srcLines (integerToNat (cast lineNum))
      let tokens = getSemanticTokens md getLineLength
      modify LSPConf (record { semanticTokensSentFiles $= insert params.textDocument.uri })
      pure $ pure $ (make $ tokens)

handleRequest method params = whenActiveRequest $ \conf => do
    logString Warning $ "received a not supported \{show (toJSON method)} request"
    pure $ Left methodNotFound

export
handleNotification :
       Ref LSPConf LSPConfiguration
    => Ref Ctxt Defs
    => Ref UST UState
    => Ref Syn SyntaxInfo
    => Ref MD Metadata
    => Ref ROpts REPLOpts
    => (method : Method Client Notification)
    -> (params : MessageParams method)
    -> Core ()

handleNotification Exit params = do
  let status = if !(gets LSPConf isShutdown) then ExitSuccess else ExitFailure 1
  coreLift $ exitWith status

handleNotification TextDocumentDidOpen params = whenActiveNotification $ \conf =>
    ignore $ loadURI conf params.textDocument.uri (Just params.textDocument.version)

handleNotification TextDocumentDidSave params = whenActiveNotification $ \conf => do
    modify LSPConf (record
      { dirtyFiles $= delete params.textDocument.uri
      , errorFiles $= delete params.textDocument.uri
      , semanticTokensSentFiles $= delete params.textDocument.uri
      })
    ignore $ loadURI conf params.textDocument.uri Nothing
    when (fromMaybe False $ conf.capabilities.workspace >>= semanticTokens >>= refreshSupport) $
      sendRequestMessage_ WorkspaceSemanticTokensRefresh Nothing

handleNotification TextDocumentDidChange params = whenActiveNotification $ \conf => do
    modify LSPConf (record { dirtyFiles $= insert params.textDocument.uri })

handleNotification TextDocumentDidClose params = whenActiveNotification $ \conf => do
    modify LSPConf (record { openFile = Nothing
                           , quickfixes = []
                           , cachedActions = empty
                           , cachedHovers = empty
                           , dirtyFiles $= delete params.textDocument.uri
                           , errorFiles $= delete params.textDocument.uri
                           , semanticTokensSentFiles $= delete params.textDocument.uri
                           })
    logString Info $ "File \{params.textDocument.uri.path} closed"

handleNotification method params = whenActiveNotification $ \conf =>
  logString Warning "unhandled notification"


text:
crew : List String
crew = ["Lister", "Rimmer", "Kryten", "Cat"]

main : IO ()
main = do putStr "Display Crew? "
          x <- getLine
          when (x == "yes") $
               do traverse putStrLn crew
                  pure ()
          putStrLn "Done"


text:
module Types

public export
data IsIt = Z | O

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module System.File.Virtual

import System.File.Support
import public System.File.Types
import System.FFI

%default total

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_stdin"
         "node:lambda:x=>({fd:0, buffer: Buffer.alloc(0), name:'<stdin>', eof: false})"
         jvm runtimeClass "getStdin"
prim__stdin : FilePtr

%foreign support "idris2_stdout"
         "node:lambda:x=>({fd:1, buffer: Buffer.alloc(0), name:'<stdout>', eof: false})"
         jvm runtimeClass "getStdout"
prim__stdout : FilePtr

%foreign support "idris2_stderr"
         "node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
         jvm runtimeClass "getStderr"
prim__stderr : FilePtr

export
stdin : File
stdin = FHandle prim__stdin

export
stdout : File
stdout = FHandle prim__stdout

export
stderr : File
stderr = FHandle prim__stderr


text:
-- Previously this gave an 'unreachable case warning' and evaluated
-- to the first case! Should give foo : Nat -> Nat
foo : (x : Nat) -> case S x of
                        Z => Nat -> Nat
                        (S k) => Nat


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.Vect

reverseProof : Vect (k + 1) e -> Vect (S k) e
reverseProof {k} result = rewrite plusCommutative 1 k in result

myReverse : Vect n e -> Vect n e
myReverse [] = []
myReverse {n = S k} (x :: xs) = reverseProof (myReverse xs ++ [x])

appNilProof : Vect m e -> Vect (plus m 0) e
appNilProof {m} result = rewrite plusZeroRightNeutral m in result

appConsProof : Vect (S (m + k)) e -> Vect (plus m (S k)) e
appConsProof {m} {k} result =
  rewrite (sym (plusSuccRightSucc m k))
  in result

app : Vect n e -> Vect m e -> Vect (m + n) e
app [] ys = appNilProof ys
app (x :: xs) ys = appConsProof (x :: app xs ys)

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m     = sym (plusZeroRightNeutral m)
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in plusSuccRightSucc m k

reverseProofNil : Vect n a -> Vect (plus n 0) a
reverseProofNil {n} xs = rewrite plusZeroRightNeutral n in xs

reverseProofCons : Vect ((S n) + l) a -> Vect (plus n (S l)) a
reverseProofCons {n} {l} res =
  rewrite sym (plusSuccRightSucc n l) in
  res

myReverse2 : Vect n a -> Vect n a
myReverse2 xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n + m) a
    reverse' acc [] = reverseProofNil acc
    reverse' acc (x :: xs) = reverseProofCons (reverse' (x :: acc) xs)

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

zeroNotSucc : (0 = S k) -> Void
zeroNotSucc Refl impossible

succNotZero : (S k = 0) -> Void
succNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSucc
checkEqNat (S k) Z = No succNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
  Yes prf => Yes (cong prf)
  No contra => No (noRec contra)

isYes : Dec (a = b) -> Bool
isYes (Yes prf) = True
isYes (No contra) = False

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case decEq m len of
  Yes Refl => Just input
  No contra => Nothing

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

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

decEqVect : (DecEq a) => (xs : Vect n a) -> (ys : Vect n a) -> Dec (xs = ys)
decEqVect [] [] = Yes Refl
decEqVect (x :: xs) (y :: ys) = case decEq x y of
  (No contra) => No $ headEqual contra
  (Yes Refl) => case decEqVect xs ys of
    (Yes Refl) => Yes Refl
    (No contra) => No $ tailEqual contra

main : IO ()
main = do
  printLn $ myReverse [1,2,3,4]
  printLn $ app [1,2,3] [4,5,6,7]
  printLn $ myReverse2 [1,2,3,4,5]
  printLn $ isYes $ checkEqNat 100 99
  printLn $ Main.exactLength 2 [1,2,3]
  printLn $ isYes $ decEqVect [1,2,3] [1,2,3]

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
-- Credits to Guillaume Allais for the idea

module GenerFunctor

import Control.Category

import Control.Monad.Reader
import Control.Monad.Trans

%default total

------------------
--- Definition ---
------------------

interface
  Category {obj=objC} arrC =>
  Category {obj=objD} arrD =>
  GenFunctor objC objD arrC arrD f | f where
  --GenFunctor objC objD (0 arrC : objC -> objC -> Type) (0 arrD : objD -> objD -> Type) (0 f : objC -> objD) | f where
    gmap : {0 a, b : objC} -> arrC a b -> arrD (f a) (f b)

  -- Didn't manage to get rid of explicit `objC`, `objD`, `arrC` and `arrD` parameters.

-----------------------------
--- Auxiliary definitions ---
-----------------------------

%inline
Fun : Type -> Type -> Type
Fun = \a, b => a -> b

%inline
WrFun : (Type -> Type) -> Type -> Type -> Type
WrFun f = \a, b => f a -> f b

{0 m : Type -> Type} -> Category (WrFun m) where
  id = id
  (.) = (.)

------------------------------------
--- `GenFunctor` is more general ---
------------------------------------

--interface Functor f where
--  map : (a -> b) -> f a -> f b

Functor m => GenFunctor Type Type Fun Fun m where
  gmap = map

Functor m => GenFunctor Type Type Fun (WrFun m) Prelude.id where
  gmap = map

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

interface MonadLiftMap (0 t : (Type -> Type) -> Type -> Type) where
  liftMap : Monad m => (m a -> m b) -> t m a -> t m b

MonadLiftMap t => Monad m => GenFunctor Type Type (WrFun m) Fun (t m) where
  gmap = liftMap

MonadLiftMap t => Monad m => GenFunctor Type Type (WrFun m) (WrFun $ t m) Prelude.id where
  gmap = liftMap

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

interface PrevGenFunctor n (0 m : Type -> Type) | m where
  pgmap : (n a -> n b) -> m a -> m b

PrevGenFunctor n m => GenFunctor Type Type (WrFun n) Fun m where
  gmap = pgmap

PrevGenFunctor n m => GenFunctor Type Type (WrFun n) (WrFun m) Prelude.id where
  gmap = pgmap

-------------
--- Usage ---
-------------

-- All those `gmap {f=...}` work only when we have `GenFunctor ... f | f where` functional dependency

ns2is : List Nat -> List Int
ns2is = gmap {f=List} cast

[Trans] MonadReader r m => MonadTrans t => GenFunctor Type Type (WrFun m) Fun (t m) => Monad (t m) => MonadReader r (t m) where
  ask   = lift ask
  local = gmap {f=t m} . local

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Algebra.Solver.Semiring.SolvableSemiring

import Algebra.Semiring

%default total

||| When normalizing arithmetic expressions, we must
||| make sure that factors that evaluate to zero must
||| be removed from the sum of products.
|||
||| For instance, the following example only works,
||| if the term `0 * x * y` gets removed before comparing
||| the normalized sums:
|||
||| ```idris example
||| 0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
||| binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)
||| ```
|||
||| Because we cannot directly use a (primitive) pattern match
||| without having a concrete type, we need this interface.
||| (We *could* use `DecEq`, but this is not publicly exported
||| for the primitives; probably for good reasons since it is
||| implemented using `believe_me`).
public export
interface Semiring a => SolvableSemiring a where

  ||| Checks if a value is propositionally equal to zero.
  isZero : (v : a) -> Maybe (v === 0)

public export
SolvableSemiring Nat where
  isZero Z = Just Refl
  isZero _ = Nothing


text:
module Data.Time.Clock.POSIX

import Data.Fixed

import Data.Time.Clock.DiffTime
import Data.Time.Clock.UTCTime
import Data.Time.Calendar

%default total

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

public export POSIXTime : Type
POSIXTime = NominalDiffTime

public export posixDayLength : POSIXTime
posixDayLength = nominalDay

public export posixEpochDay : Day
posixEpochDay = ModifiedJulianDay 40587

public export
Cast POSIXTime UTCTime where
  cast i =
    let d = i.seconds `div'` posixDayLength.seconds
        t = i.seconds `mod'` posixDayLength.seconds
        in MkUTCTime (addDays d posixEpochDay) (secondsToDiffTime t)

public export
Cast UTCTime POSIXTime where
  cast (MkUTCTime d t) =
    let MkFixed l = posixDayLength.seconds
        ds = posixDayLength.seconds
     in secondsToDiffTime $ (scale (diffDays d posixEpochDay) ds) + (min ds t.seconds)


text:
module Minecraft.Core.Entity

import Minecraft.Core

%default total

public export
record Entity (self : Type) where
  constructor MkEntity

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Linear.Backprop

import Backprop
import Control.Optics
import Linear.V
import Linear.Math
import Linear.Optics

export
{n : _} -> CanBack a => CanBack (V n a) where
  zero = pure zero
  one = pure one
  add [] [] = []
  add (x :: xs) (y :: ys) = add x y :: add xs ys

export
(::) : {a, n : _} -> CanBack a => Node s a -> Node s (V n a) -> Node s (V (S n) a)
(::) = op2 $ \[x, xs] => (x :: xs, \(d :: ds) => [d, ds])

export
{n : _} -> NodeTraversable (V n) where
  sequence x = map (\i => x ^. at i) Fin.range

export
{n : _} -> NodeDistributive (V n) where
  collect [] = const []
  collect (node :: nodes) = node :: collect nodes

export
konst : {a, n : _} -> Num a => CanBack a => Node i a -> Node i (V n a)
konst = op1 $ \[x] => (pure x, \d => [sum d])

export
dot : {a : _} -> (Num a, CanBack a, Foldable f, Zippable f, NodeFunctor f)
  => Node i (f a) -> Node i (f a) -> Node i a
dot x y = V.dot (Node.sequence x) (Node.sequence y)

infixl 7 <.>
export
(<.>) : {a, n : _} -> Num a => CanBack a => Node i (V n a) -> Node i (V n a) -> Node i a
(<.>) = op2 $ \[x, y] => (x `dot` y, \d => let d' = pure d in [d' * y, x * d'])

export
outer : {n, m, a : _} -> (Num a, CanBack a) => Node i (T [n] a) -> Node i (T [m] a) -> Node i (T [n, m] a)
outer = op2 $ \[x, y] => (x `outer` y, \d => [d !* y, transpose d !* x])

export
(#>) : {m, n, a : _} -> Num a => CanBack a => Node i (T [m, n] a) -> Node i (T [n] a) -> Node i (T [m] a)
(#>) = op2 $ \[x, y] => (x !* y, \d => [d `outer` y, transpose x !* d])

-- export
-- (<#) : {m, n, a : _} -> Num a => CanBack a => Node i (T [m] a) -> Node i (T [m, n] a) -> Node i (T [n] a)

export
(*^) : {a : _} -> CanBack a => Num a => NodeFunctor f => Node i a -> Node i (f a) -> Node i (f a)
(*^) a = Node.map (a *)

export
(^*) : {a : _} -> CanBack a => NodeFunctor f => Num a => Node i (f a) -> Node i a -> Node i (f a)
x ^* y = y *^ x

-- export
-- (*!) : {a, f : _} -> (CanBack a, Num a, CanBack (f a), NodeTraversable t, NodeTraversable f, Functor t)
--   => Node i (t a) -> Node i (t (f a)) -> Node i (f a)

infixr 7 <>
export
(<>) : {n, p, m, a : _} -> (Num a, CanBack a) => Node i (T [m, n] a) -> Node i (T [n, p] a) -> Node i (T [m, p] a)
(<>) = op2 $ \[x, y] => (x !*! y, \d => [d !*! transpose y, transpose x !*! d])

export
asum : {a, n : _} -> Num a => CanBack a => Node i (V n a) -> Node i a
asum = op1 $ \[x] => (sum x, \d => [pure d])


text:
module Main

%default total

codata Stream' a = Nil | (::) a (Stream' a)

countFrom : Int -> Stream' Int
countFrom x = x :: countFrom (x + 1)

take : Nat -> Stream' a -> List a
take Z _ = []
take (S n) (x :: xs) = x :: take n xs
take n [] = []

main : IO ()
main = do printLn (take 10 (Main.countFrom 10))


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

> %name Vect xs, ys, zs

> transposeHelper : Vect m a -> (1 xs_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)


text:
module Language.LSP.Message.URI

import Data.Either
import Data.String.Parser
import public Data.URI
import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils

%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#uri
public export
DocumentURI : Type
DocumentURI = URI

export
ToJSON URI where
  toJSON = JString . show

export covering
FromJSON URI where
  fromJSON (JString str) = eitherToMaybe (fst <$> parse (uriParser <* eos) str)
  fromJSON _ = neutral

export
ToJSON v => ToJSON (SortedMap URI v) where
  toJSON m = JObject (map (mapFst show) $ toList $ toJSON <$> m)

export covering
FromJSON v => FromJSON (SortedMap URI v) where
  fromJSON (JObject xs) = fromList <$> traverse (\(k, v) => (,) <$> fromJSON (JString k) <*> fromJSON v) xs
  fromJSON _ = neutral


text:
module Main

import Syntax.Lexer
import Syntax.Tokens
import Error
import Loc

main : IO ()
main = case lex "(test \"test something\" 10 [1 2 3] {a b c d} (inside test \"kek\")) ;simple comment" of
          Right res => putStr (concatMap ((++ "\n") . show) res)
          Left _ => putStrLn "Error"

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
-- ------------------------------------------------------- [ NotWellFormed.idr ]
-- Module    : NotWellFormed.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Tests taken from [here](http://www.jclark.com/xml/).
module XML.Test.NotWellFormed

import Test.Unit

import Commons.Data.Location
import Commons.Text.Parser.Test

import XML.Lexer
import XML.Parser
import XML.DOM
import XML.Serialise

showParseError : Run.ParseError Token -> String
showParseError (FError e) = show e
showParseError (PError e) = unlines [maybe "" show (location e), error e]
showParseError (LError (MkLexFail l i)) = unlines [show l, show i]

export
runTests : IO ()
runTests = do
  putStrLn "=> Not WellFormed"

  runTests [
       runParseTest showParseError $ parseFail "Not Well Formed 1" (parseXMLDoc) "<?xml VERSION=\"1.0\"?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 2" (parseXMLDoc) "<?xml encoding=\"UTF-8\" version=\"1.0\"?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 3" (parseXMLDoc) "<?xml version=\"1.0\" encoding=\"UTF-8\" ?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 4" (parseXMLDoc) "<?xml version=\"1.0' encoding=\"UTF-8\" ?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 5" (parseXMLDoc) "<?xml version=\"1.0\" version=\"1.0\"?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 6" (parseXMLDoc) "<?xml version=\"1.0\" valid=\"no\" ?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 7" (parseXMLDoc) "<?xml version=\"1.0\" standalone=\"YES\" ?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 8" (parseXMLDoc) "<?xml version=\"1.0\" encoding=\" UTF-8\"?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 9" (parseXMLDoc) "<?xml version=\"1.0 \" ?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 10" (parseXMLDoc) "<?xml version=\"1.0\"?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 11" (parseXMLDoc) "<?xml encoding=\"UTF-8\"?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 12" (parseXMLDoc) "<?XML version=\"1.0\"?> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 13" (parseXMLDoc) "<?xmL version=\"1.0\"?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 14" (parseXMLSnippet) "<doc> <doc ? <a </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 15" (parseXMLSnippet) "<doc> <.doc></.doc> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 16" (parseXMLSnippet) "<doc><? ?></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 17" (parseXMLSnippet) "<doc><?target some data></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 18" (parseXMLSnippet) "<doc><?target some data?</doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 19" (parseXMLSnippet) "<doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 20" (parseXMLSnippet) "<doc>&amp no refc</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 21" (parseXMLSnippet) "<doc>&.entity;</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 22" (parseXMLSnippet) "<doc>&#RE;</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 23" (parseXMLSnippet) "<doc>A & B</doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 24" (parseXMLSnippet) "<doc a1></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 25" (parseXMLSnippet) "<doc a1=v1></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 26" (parseXMLSnippet) "<doc a1=\"v1'></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 27" (parseXMLSnippet) "<doc a1=\"<foo>\"></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 28" (parseXMLSnippet) "<doc a1=></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 29" (parseXMLSnippet) "<doc a1=\"v1\" \"v2\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 30" (parseXMLSnippet) "<doc><![CDATA[</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 31" (parseXMLSnippet) "<doc><![CDATA [ stuff]]></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 32" (parseXMLSnippet) "<doc></>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 33" (parseXMLSnippet) "<doc a1=\"A & B\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 34" (parseXMLSnippet) "<doc a1=\"a&b\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 35" (parseXMLSnippet) "<doc a1=\"&#123:\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 36" (parseXMLSnippet) "<doc 12=\"34\"></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 37" (parseXMLSnippet) "<doc> <123></123> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 38" (parseXMLSnippet) "<doc>]]></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 39" (parseXMLSnippet) "<doc>]]]></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 40" (parseXMLSnippet) "<doc>  <![CDATA[]]> <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 59" (parseXMLSnippet) "   <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 60" (parseXMLSnippet) "<doc></DOC>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 61" (parseXMLSnippet) " <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 62" (parseXMLSnippet) "<doc>&foo;</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 63" (parseXMLSnippet) "<doc a=\"&foo;\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 64" (parseXMLSnippet) "<doc>X</doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 65" (parseXMLSnippet) "<?pi stuff?> <![CDATA[]]> <doc> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 66" (parseXMLSnippet) "<?pi data?>  <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 67" (parseXMLSnippet) "<doc> <![CDATA [ ]]> </doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 68" (parseXMLSnippet) "<doc> <![cdata[data]]> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 69" (parseXMLSnippet) " <?xml version=\"1.0\"?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 70" (parseXMLSnippet) "<doc> <?xml version=\"1.0\"?> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 71" (parseXMLSnippet) "<doc> </doc> <?xml version=\"1.0\"?>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 72" (parseXMLSnippet) "<doc> <?xMl version=\"1.0\"?> </doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 73" (parseXMLSnippet) "<doc> <?xmL?> </doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 74" (parseXMLSnippet) "<doc>/doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 75" (parseXMLSnippet) " <doc></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 76" (parseXMLSnippet) "<?pas ?> <doc></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 77" (parseXMLSnippet) "<doc a=\"a\"></doc>"
    ,  runParseTest showParseError $ parseFail "Not Well Formed 78" (parseXMLSnippet) "<doc><![CDATA[]]></doc>"

    ,  runParseTest showParseError $ parseFail "Not Well Formed 79" (parseXMLSnippet) "<!DOCTYPE a [ <!ELEMENT a EMPTY> <!ATTLIST a b CDATA #IMPLIED d CDATA #IMPLIED> ]> "
    ]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Ch03.Relations

%default total
%access public export

||| Type representing the reflexive transitive closure of a relation
|||
||| Given a relational type `rel : ty -> ty -> Type`, `ReflSymmClos rel` is its reflexive and
||| transitive closure.
data ReflSymmClos : (rel : ty -> ty -> Type) -> ty -> ty -> Type where
  Refl : ReflSymmClos rel x x
  --Snoc : ReflSymmClos rel t t' -> (rel t' t'') -> ReflSymmClos rel t t''
  Cons : (rel t t') -> ReflSymmClos rel t' t'' -> ReflSymmClos rel t t''

||| Appends two (appendable) elements of the reflexive-transitive closure of `rel` together,
||| thus realizing the transitivity of said closure
(++) : ReflSymmClos rel t t' ->
       ReflSymmClos rel t' t'' ->
       ReflSymmClos rel t t''
(++) Refl y = y
(++) (Cons x z) y = Cons x (z ++ y)

||| Given `rel t1 t2`, returns the associated relation in the reflexive transitive closure,
||| thus realizing the "closure part" of said closure
weaken : rel t1 t2 -> ReflSymmClos rel t1 t2
weaken x = Cons x Refl

||| Dual version of the `Cons` constructor for convenience.
snoc : ReflSymmClos rel t t' -> (rel t' t'') -> ReflSymmClos rel t t''
snoc p p' = p ++ (weaken p')

||| Given a function `f` defined on relations of type `rel`, applies that to a relation in the
||| reflexive-transitive closure of `rel`
map : {func : ty -> ty} -> (f : {t1 : ty} -> {t2 : ty} -> rel t1 t2 -> rel (func t1) (func t2)) ->
      (ReflSymmClos rel t1 t2) ->
      (ReflSymmClos rel (func t1) (func t2))
map {func} f Refl = Refl
map {func} f (Cons x y) = Cons (f x) (map f y)

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module ArgParse.Lexer

import public Text.Lexer

%default total
%access export

public export
data Token = SFlag   String
           | LFlag   String
           | Equals String
           | Quoted String
           | WS String
           | Arg String
           | Unknown String

Show Token where
  show (LFlag    x) = unwords ["LFlag",   show x]
  show (SFlag    x) = unwords ["SFlag",   show x]
  show (Equals   x) = unwords ["Equals", show x]
  show (Quoted  x) = unwords ["Quoted", show x]
  show (WS      x) = unwords ["WS",     show x]
  show (Arg    x) = unwords ["Arg",     show x]
  show (Unknown x) = unwords ["BAD TOKEN", show x]

--doubleLit : Lexer
--doubleLit = (is '-' <|> empty)
--        <+> digits
--        <+> (is '.' <+> (digits <|> empty) <|> empty)

ch : Lexer
ch = pred (isAlphaNum)

str : Lexer
str = some (pred isAlphaNum)

shortFlag : Lexer
shortFlag = is '-' <+> ch

longFlag : Lexer
longFlag = is '-' <+> is '-' <+> str

equals : Lexer
equals = is '='

arg : Lexer
arg = any <+> manyTill any space

rawTokens : TokenMap Token
rawTokens =
  [ (space, WS)
  , (stringLit, Quoted)
  , (longFlag, LFlag)
  , (shortFlag, SFlag)
  , (equals, Equals)
  , (arg, Arg)
  , (symbol, Unknown)
  ]

export
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex str
    = case Lexer.lex rawTokens str of
           (tok, (_, _, "")) => Right (filter notComment tok)
           (_, fail) => Left fail
    where
      notComment : TokenData Token -> Bool
      notComment t = case tok t of
                          WS _ => False
                          _ => True

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

max_stars_repo_name: jfdm/idris-argparse

max_issues_repo_name: jfdm/idris-argparse

max_forks_repo_name: jfdm/idris-argparse


text:
module CH08

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

data ThreeEq : a -> b -> c -> Type where
  ThreeSame : ThreeEq x x x

cong2 : { f : x -> y -> z} -> a = b -> c = d -> f a c = f b d
cong2 Refl Refl = Refl

same_cons : {xs : List a} -> {ys : List a}
          -> xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

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

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x ThreeSame = ThreeSame

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 plusSuccRightSucc m k

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs
  where
    reverse' : Vect k a -> Vect m a -> Vect (k + m) a
    reverse' {k} acc []                  = rewrite (plusZeroRightNeutral k) in acc
    reverse' {k} {m = S m} acc (x :: xs) = rewrite sym (plusSuccRightSucc k m)
                                           in (reverse' (x :: acc) xs)

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

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

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


text:
module Circuits.Idealised.Check

import Decidable.Equality

import Data.Nat
import Data.String
import Data.List.Elem
import Data.List.Quantifiers
import Data.DPair

import Toolkit.Decidable.Informative
import Toolkit.Decidable.Equality.Views

import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Data.DList

import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

import Circuits.Split
import Circuits.Idealised.Core
import Circuits.Idealised.Types
import Circuits.Idealised.Terms
import Circuits.Idealised.AST

%default total

public export
Context : List (Ty, Usage) -> Type
Context = Context (Ty,Usage)

namespace FreeVar

  public export
  data IsFree : (item : (Ty, Usage)) -> Type
    where
      FVar : (prf : u = FREE)
                 -> IsFree (type, u)

  Uninhabited (IsFree (ty,USED)) where
    uninhabited (FVar Refl) impossible

  isFree : (item : (Ty, Usage))
                -> DecInfo ()
                           (IsFree item)
  isFree (ty, USED)
    = No () absurd

  isFree (ty, FREE)
    = Yes (FVar Refl)

  public export
  FreeVar : {types : List (Ty, Usage)}
         -> (key   : String)
         -> (ctxt  : Context types)
                  -> Type
  FreeVar str ctxt
   = Exists (Ty,Usage)
            IsFree
            str
            ctxt

  export
  lookup : {types : List (Ty, Usage)}
        -> (str  : String)
        -> (ctxt : Context types)
                -> DecInfo (Exists.Error ())
                           (FreeVar str ctxt)
  lookup = exists isFree

use : (ctxt : Context curr)
   -> (use  : Use curr prf next)
           -> Context next
use (I k (ty,FREE) :: rest) H
  = I k (ty, USED) :: rest

use (head :: tail) (T later)
  = head :: use tail later

isUsed : (ctxt : Context types)
              -> Dec (All Used types)
isUsed []
  = Yes []

isUsed ((I name x) :: tail) with (used x)
  isUsed ((I name x) :: tail) | (Yes pH) with (isUsed tail)
    isUsed ((I name x) :: tail) | (Yes pH) | (Yes pT)
      = Yes (pH :: pT)

    isUsed ((I name x) :: tail) | (Yes pH) | (No contra)
      = No (\(a::as) => contra as)

  isUsed ((I name x) :: tail) | (No contra)
    = No (\(a::as) => contra a)

withLocThrow : FileContext -> Check.Error -> Idealised a
withLocThrow fc e = throw (TyCheck $ Err fc e)

throw : Check.Error -> Idealised a
throw = (throw . TyCheck)

public export
allEqual : FileContext
        -> (a,b,c : DType)
                 -> Idealised (AllEqual a b c)
allEqual fc a b c with (Views.allEqual a b c)
  allEqual fc c c c | (Yes AE)
    = pure AE
  allEqual fc a b c | (No AB prfWhyNot)
    = withLocThrow fc (MismatchGate a b)
  allEqual fc a b c | (No AC prfWhyNot)
    = withLocThrow fc (MismatchGate a c)

data Result : (curr : List (Ty,Usage))
           -> Type
  where
    R : {cout : _}
     -> (type : Ty)
     -> (new  : Context cout)
     -> (term : Term cin type cout)
             -> Result cin

check : {cin  : List (Ty,Usage)}
     -> (curr : Context cin)
     -> (ast  : AST)
             -> Idealised (Result cin)

check curr (Var x) with (FreeVar.lookup (get x) curr)
  check curr (Var x) | (Yes (E type item prf locC locN)) with (prf)
    check curr (Var x) | (Yes (E (type, u) item prf locC locN)) | (FVar prf1) with (prf1)
      check curr (Var x) | (Yes (E (type, FREE) item prf locC locN)) | (FVar prf1) | Refl with (use (V _ locN))
        check curr (Var x) | (Yes (E (type, FREE) item prf locC locN)) | (FVar prf1) | Refl | (MkDPair next pU) with (use curr pU)
          check curr (Var x) | (Yes (E (type, FREE) item prf locC locN)) | (FVar prf1) | Refl | (MkDPair next pU) | new
            = pure (R type new (Var (V _ locN) pU))

  check curr (Var x) | (No msg _)
    = withLocThrow (span x) (ElemFail (get x) msg)

check curr (Input fc x y name body)

  = do R TyUnit Nil body <- check (I (get name) ((TyPort (MkPair x y)),FREE) :: curr)
                                    body
           | R ty Nil _ => throw (Mismatch TyUnit ty)
           | R _  xs  _ => withLocThrow fc (LinearityError xs)

       pure (R TyUnit Nil (NewSignal x y body))

check curr (Wire fc type a b body)

  = do R TyUnit Nil term <- check (I (get a) ((TyPort (MkPair OUTPUT type)), FREE) ::
                                   I (get b) ((TyPort (MkPair INPUT  type)), FREE) :: curr)
                                  body
           | R ty Nil _ => throw (Mismatch TyUnit ty)
           | R ty xs  _ => withLocThrow fc (LinearityError xs)

       pure (R TyUnit Nil (Wire type term))

check curr (Seq x y)
  = do R TyGate ex x <- check curr x
         | R ty _ _ => throw (Mismatch TyGate ty)

       R TyUnit Nil y <- check ex y
         | R ty Nil _ => throw (Mismatch TyUnit ty)
         | R ty xs  _ => throw (LinearityError xs)

       pure (R TyUnit Nil (Seq x y))

check curr (Mux fc o c a b)
  = do R (TyPort (OUTPUT,dtypeA)) cO o <- check curr o
         | _ => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,LOGIC)) cC c <- check cO c
         | R ty _ _ => withLocThrow fc (Mismatch (TyPort (INPUT,LOGIC)) ty)

       R (TyPort (INPUT,dtypeB)) cA a <- check cC a
         | _ => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,dtypeC)) cB b <- check cA b
         | _ => withLocThrow fc (PortExpected OUTPUT)

       AE <- allEqual fc dtypeA dtypeB dtypeC

       pure (R TyGate cB (Mux o c a b))

check curr (Dup fc a b i)
  = do R (TyPort (OUTPUT,dtypeA)) cA a <- check curr a
         | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (OUTPUT,dtypeB)) cB b <- check cA b
         | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,dtypeC)) cI i <- check cB i
         | ty => withLocThrow fc (PortExpected INPUT)

       AE <- allEqual fc dtypeA dtypeB dtypeC

       pure (R TyGate cI (Dup a b i))

check curr (Not fc a b)
  = do R (TyPort (OUTPUT,LOGIC)) cA a <- check curr a
         | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,LOGIC)) cB b <- check cA b
         | ty => withLocThrow fc (PortExpected INPUT)

       pure (R TyGate cB (Not a b))

check curr (Gate fc k a b c)
  = do R (TyPort (OUTPUT,LOGIC)) cA a <- check curr a
         | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,LOGIC)) cB b <- check cA b
         | ty => withLocThrow fc (PortExpected INPUT)

       R (TyPort (INPUT,LOGIC)) cC c <- check cB c
         | ty => withLocThrow fc (PortExpected INPUT)

       pure (R TyGate cC (Gate k a b c))

check curr (IndexS fc o i)
  = do R (TyPort (OUTPUT,dtypeO)) cO termO <- check curr o
         | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,BVECT (W (S Z) ItIsSucc) dtypeI)) cI termI <- check cO i
         | R (TyPort (INPUT, BVECT s type)) _ _
             => withLocThrow fc (Mismatch (TyPort (INPUT, BVECT (W (S Z) ItIsSucc) type))
                                          (TyPort (INPUT, BVECT s type)))
         | ty => withLocThrow fc (PortExpected INPUT)

       Refl <- embed (TyCheck $ Err fc (MismatchGate dtypeO  dtypeI))
                     (decEq dtypeO dtypeI)

       pure (R TyGate cI (IndexSingleton termO termI))

check curr (IndexE fc k a b i)

  = do R (TyPort (OUTPUT,dtypeA)) cA termA <- check curr a
                  | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (OUTPUT,BVECT free dtypeB)) cB termB <- check cA b
                  | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,BVECT size dtypeC)) cI termI <- check cB i
                  | ty => withLocThrow fc (PortExpected INPUT)

       AE <- allEqual fc dtypeA dtypeB dtypeC

       let p = case k of { F => minus (toNat size) 1; L => 0}

       (s ** prf) <- embed (const $ TyCheck $ Err fc (NotEdgeCase (InvalidEdge (toNat size) (S Z) (toNat free))))
                           (EdgeCase.index size p)

       Refl <- embed (TyCheck $ Err fc (NotEdgeCase (InvalidEdge (toNat size) (S Z) (toNat free))))
                     (decEq free s)

       pure (R TyGate cI (IndexEdge p prf termA termB termI))

check curr (IndexP fc p a b c i)
  = do R (TyPort (OUTPUT,dtypeA)) cA termA <- check curr a
                  | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (OUTPUT,BVECT freeB dtypeB)) cB termB <- check cA b
                  | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (OUTPUT,BVECT freeC dtypeC)) cC termC <- check cB c
                  | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT,BVECT size dtypeD)) cI termI <- check cC i
                  | ty => withLocThrow fc (PortExpected INPUT)

       Refl <- embed (TyCheck $ Err fc (MismatchGate dtypeA (BVECT freeB dtypeB)))
                     (decEq dtypeA dtypeB)

       Refl <- embed (TyCheck $ Err fc (MismatchGate (BVECT freeB dtypeB) (BVECT freeC dtypeC)))
                     (decEq dtypeB dtypeC)

       Refl <- embed (TyCheck $ Err fc (MismatchGate (BVECT freeC dtypeC) (BVECT size dtypeD)))
                     (decEq dtypeC dtypeD)

       (a ** b ** prf) <- embed (const $ TyCheck $ Err fc (NotEdgeCase (InvalidSplit p (toNat size) (toNat freeB) (toNat freeC))))
                                (Pivot.index p size)

       Refl <- embed (TyCheck $ Err fc (MismatchGate (BVECT a     dtypeB)
                                                     (BVECT freeB dtypeB)))
                     (decEq freeB a)

       Refl <- embed (TyCheck $ Err fc (MismatchGate (BVECT b     dtypeB)
                                                     (BVECT freeC dtypeB)))
                     (decEq freeC b)

       pure (R TyGate cI (IndexSplit p prf termA termB termC termI))

check curr (MergeS fc o i)

  = do R (TyPort (OUTPUT,BVECT (W (S Z) ItIsSucc) dtypeO)) cO termO <- check curr o
           | R (TyPort (INPUT, BVECT s type)) _ _
                => withLocThrow fc (Mismatch (TyPort (OUTPUT, BVECT (W (S Z) ItIsSucc) type))
                                             (TyPort (INPUT,  BVECT s                  type)))
           | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT, dtypeI)) cI termI <- check cO i
           | ty => withLocThrow fc (PortExpected INPUT)

       Refl <- embed (TyCheck $ Err fc (MismatchGate dtypeO dtypeI))
                     (decEq dtypeO dtypeI)

       pure (R TyGate cI (MergeSingleton termO termI))

check curr (MergeV fc o a b)

  = do R (TyPort (OUTPUT, dtypeO)) cO termO <- check curr o
           | ty => withLocThrow fc (PortExpected OUTPUT)

       R (TyPort (INPUT, dtypeA)) cA termA <- check cO a
           | ty => withLocThrow fc (PortExpected INPUT)

       R (TyPort (INPUT, dtypeB)) cB termB <- check cA b
           | ty => withLocThrow fc (PortExpected INPUT)

       case Views.allEqual LOGIC dtypeA dtypeB of
         Yes AE
           => do Refl <- embed (TyCheck (Err fc (MismatchGate (BVECT (W (S (S Z)) ItIsSucc) LOGIC)
                                                              dtypeO)))
                               (decEq dtypeO (BVECT (W (S (S Z)) ItIsSucc) LOGIC))

                 pure (R TyGate cB (Merge2L2V termO termA termB))
         No msg prf
           => case dtypeO of
                LOGIC => withLocThrow fc VectorExpected
                BVECT sO tO
                  => case dtypeA of
                       LOGIC => withLocThrow fc VectorExpected
                       BVECT sA tA
                         => case dtypeB of
                              LOGIC => withLocThrow fc VectorExpected
                              BVECT sB tB
                                => do prfS <- embed (TyCheck (Err fc (VectorSizeMismatch sO sA sB)))
                                                    (isPlus sA sB sO)

                                      AE <- allEqual fc tO tA tB

                                      pure (R TyGate cB (Merge2V2V prfS termO termA termB))

check curr (Stop fc)
  = do prf <- embed (TyCheck (Err fc (LinearityError curr)))
                    (isUsed curr)

       pure (R TyUnit Nil (Stop prf))

namespace Design

  export
  check : (ast : AST)
              -> Idealised (Term Nil TyUnit Nil)
  check ast
    = do R TyUnit Nil term <- check Nil ast
           | R ty _ _ => throw (TyCheck (Mismatch TyUnit ty))
         pure term

-- [ 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:
||| Fixed point fractional number. - Ported from Haskell base.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Fixed

import Data.Maybe
import Data.String

import Generics.Derive

import Data.Rational

%default total
%language ElabReflection

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

namespace ResolutionV

  public export
  data ResolutionV : Nat -> Type where
    MkResV : (n:Nat) -> (res:Integer) -> (res > 0 = True) -> ResolutionV n

  export expToResolution : (n:Nat) -> ResolutionV n
  expToResolution n = go 1 Refl n where
    go : (ans:Integer) -> (ans > 0 = True) -> (m:Nat) -> ResolutionV n
    go ans prf Z = MkResV n ans prf
    go ans prf (S m) = go (ans * 10) (believe_me $ Refl {x=True}) m

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

public export
data Fixed : Nat -> Type where
  MkFixed : Integer -> Fixed n

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

public export
{n:Nat} -> Num (Fixed n) where
  (MkFixed x) + (MkFixed y) = MkFixed $ x + y
  (MkFixed x) * (MkFixed y) = let
    MkResV _ res _ = expToResolution n in MkFixed $ (x * y) `div` res
  fromInteger i = let
    MkResV _ res _ = expToResolution n in MkFixed $ i * res

public export
{n:Nat} -> Neg (Fixed n) where
  negate (MkFixed x) = MkFixed $ negate x
  (MkFixed x) - (MkFixed y) = MkFixed $ x - y

public export
{n:Nat} -> Abs (Fixed n) where abs (MkFixed x) = MkFixed $ abs x

partial public export
{n:Nat} -> Fractional (Fixed n) where
  (MkFixed x) / (MkFixed y) = let
    MkResV _ res _ = expToResolution n in MkFixed $ (x * res) `div` y
  recip (MkFixed x) = let
    MkResV _ res _ = expToResolution n in MkFixed $ (res * res) `div` x

public export
{n:Nat} -> Show (Fixed n) where
  show (MkFixed x) = if n == 0 then show x
                               else if x < 0 then "-" ++ go (negate x)
                               else go x where
    go : Integer -> String
    go x = let MkResV _ r _ = expToResolution n
               i = x `div` r
               d' = show $ x `mod` r
            in show i ++ "." ++ replicate (fromInteger $ cast $ cast n - strLength d') '0' ++ d'

-- --------------------------------------------------------------------------
-- Type cast

public export
{n:Nat} -> Cast Int (Fixed n) where
  cast i = let MkResV _ res _ = expToResolution n in MkFixed $ (cast i) * res
public export
{n:Nat} -> Cast Integer (Fixed n) where
  cast i = let MkResV _ res _ = expToResolution n in MkFixed $ i * res
public export
{n:Nat} -> Cast Rational (Maybe (Fixed n)) where
  cast x = let d = x.den
               MkResV _ res _ = expToResolution n
            in toMaybe (d == 0) $ MkFixed $ x.num * res `div` (natToInteger d)
public export
{n:Nat} -> Cast (Fixed n) Rational where
  cast (MkFixed x) = let
    MkResV _ res _ = expToResolution n in x %: res

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

public export resolution : {n:Nat} -> Fixed n -> Integer
resolution {n=n} _ = let MkResV _ res _ = expToResolution n in res

export div' : {n:Nat} -> Fixed n -> Fixed n -> Integer
div' {n=n} (MkFixed x) (MkFixed q) = x `div` q

export mod' : {n:Nat} -> Fixed n -> Fixed n -> Fixed n
mod' {n=n} (MkFixed x) (MkFixed q) = MkFixed $ x `mod` q

export scale : {n:Nat} -> Integer -> Fixed n -> Fixed n
scale {n=n} y (MkFixed x) = MkFixed $ x * y

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