text:
-- Tests bitwise ops for the different data types
--
-- The tests in `idris2/basic055`, `chez/chez032` and `node/node024` are the
-- same and should all have the same output.

import Data.Stream

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

shl1 : Int -> Int
shl1 = prim__shl_Int 1

b8max : Bits8
b8max = 0xff

b16max : Bits16
b16max = 0xffff

b32max : Bits32
b32max = 0xffffffff

b64max : Bits64
b64max = 18446744073709551615

-- the only way to create -2^31
intmin : Int
intmin = shl1 31

intmax : Int
intmax = 0x7fffffff

powsOf2 : Num a => Nat -> List a
powsOf2 n = take n (iterate (*2) 1)

--------------------------------------------------------------------------------
--          shiftR
--------------------------------------------------------------------------------

shiftRBits8 : List Bits8
shiftRBits8 = map (`prim__shr_Bits8` 1) (powsOf2 8 ++ [b8max])

shiftRBits16 : List Bits16
shiftRBits16 = map (`prim__shr_Bits16` 1) (powsOf2 16 ++ [b16max])

shiftRBits32 : List Bits32
shiftRBits32 = map (`prim__shr_Bits32` 1) (powsOf2 32 ++ [b32max])

shiftRBits64 : List Bits64
shiftRBits64 = map (`prim__shr_Bits64` 1) (powsOf2 64 ++ [b64max])

shiftRInteger : List Integer
shiftRInteger = map (`prim__shr_Integer` 1) (powsOf2 128)

shiftRInt : List Int
shiftRInt = map (`prim__shr_Int` 1) (powsOf2 31 ++ [intmax])

shiftRNegativeInt : List Int
shiftRNegativeInt = map (`prim__shr_Int` 1) (map negate (powsOf2 31) ++ [intmin])

--------------------------------------------------------------------------------
--          shiftL
--------------------------------------------------------------------------------

shiftLBits8 : List Bits8
shiftLBits8 = map (`prim__shl_Bits8` 1) (0 :: powsOf2 7)

shiftLBits16 : List Bits16
shiftLBits16 = map (`prim__shl_Bits16` 1) (0 :: powsOf2 15)

shiftLBits32 : List Bits32
shiftLBits32 = map (`prim__shl_Bits32` 1) (0 :: powsOf2 31)

shiftLBits64 : List Bits64
shiftLBits64 = map (`prim__shl_Bits64` 1) (0 :: powsOf2 63)

shiftLInteger : List Integer
shiftLInteger = map (`prim__shl_Integer` 1) (0 :: powsOf2 127)

shiftLInt : List Int
shiftLInt = map (`prim__shl_Int` 1) (0 :: powsOf2 30)

shiftLNegativeInt : List Int
shiftLNegativeInt = map (`prim__shl_Int` 1) (map negate (powsOf2 30))

--------------------------------------------------------------------------------
--          Bitwise AND
--------------------------------------------------------------------------------

andBits8 : List Bits8
andBits8 = [ prim__and_Bits8 11 b8max
           , prim__and_Bits8 11 0
           , prim__and_Bits8 11 1
           , prim__and_Bits8 11 2
           , prim__and_Bits8 11 4
           , prim__and_Bits8 11 11
           ]

andBits16 : List Bits16
andBits16 = [ prim__and_Bits16 11 b16max
            , prim__and_Bits16 11 0
            , prim__and_Bits16 11 1
            , prim__and_Bits16 11 2
            , prim__and_Bits16 11 4
            , prim__and_Bits16 11 11
            ]

andBits32 : List Bits32
andBits32 = [ prim__and_Bits32 11 b32max
            , prim__and_Bits32 11 0
            , prim__and_Bits32 11 1
            , prim__and_Bits32 11 2
            , prim__and_Bits32 11 4
            , prim__and_Bits32 11 11
            ]

andBits64 : List Bits64
andBits64 = [ prim__and_Bits64 11 b64max
            , prim__and_Bits64 11 0
            , prim__and_Bits64 11 1
            , prim__and_Bits64 11 2
            , prim__and_Bits64 11 4
            , prim__and_Bits64 11 11
            ]

andInteger : List Integer
andInteger = [ prim__and_Integer 11 (prim__shl_Integer 1 128 - 1)
             , prim__and_Integer 11 0
             , prim__and_Integer 11 1
             , prim__and_Integer 11 2
             , prim__and_Integer 11 4
             , prim__and_Integer 11 11
             ]

andInt : List Int
andInt = [ prim__and_Int 11 intmax
         , prim__and_Int 11 0
         , prim__and_Int 11 1
         , prim__and_Int 11 2
         , prim__and_Int 11 4
         , prim__and_Int 11 11
         ]

andNegativeInt : List Int
andNegativeInt = [ prim__and_Int (-11) intmax
                 , prim__and_Int (-11) 0
                 , prim__and_Int (-11) 1
                 , prim__and_Int (-11) 2
                 , prim__and_Int (-11) 4
                 , prim__and_Int (-11) 11
                 , prim__and_Int (-11) intmin
                 , prim__and_Int (-11) (-1)
                 , prim__and_Int (-11) (-2)
                 , prim__and_Int (-11) (-4)
                 , prim__and_Int (-11) (-11)
                 ]

--------------------------------------------------------------------------------
--          Bitwise OR
--------------------------------------------------------------------------------

orBits8 : List Bits8
orBits8 = [ prim__or_Bits8 11 b8max
          , prim__or_Bits8 11 0
          , prim__or_Bits8 11 1
          , prim__or_Bits8 11 2
          , prim__or_Bits8 11 4
          , prim__or_Bits8 11 11
          ]

orBits16 : List Bits16
orBits16 = [ prim__or_Bits16 11 b16max
           , prim__or_Bits16 11 0
           , prim__or_Bits16 11 1
           , prim__or_Bits16 11 2
           , prim__or_Bits16 11 4
           , prim__or_Bits16 11 11
           ]

orBits32 : List Bits32
orBits32 = [ prim__or_Bits32 11 b32max
           , prim__or_Bits32 11 0
           , prim__or_Bits32 11 1
           , prim__or_Bits32 11 2
           , prim__or_Bits32 11 4
           , prim__or_Bits32 11 11
           ]

orBits64 : List Bits64
orBits64 = [ prim__or_Bits64 11 b64max
           , prim__or_Bits64 11 0
           , prim__or_Bits64 11 1
           , prim__or_Bits64 11 2
           , prim__or_Bits64 11 4
           , prim__or_Bits64 11 11
           ]

orInteger : List Integer
orInteger = [ prim__or_Integer 11 (prim__shl_Integer 1 128 - 1)
            , prim__or_Integer 11 0
            , prim__or_Integer 11 1
            , prim__or_Integer 11 2
            , prim__or_Integer 11 4
            , prim__or_Integer 11 11
            ]

orInt : List Int
orInt = [ prim__or_Int 11 intmax
        , prim__or_Int 11 0
        , prim__or_Int 11 1
        , prim__or_Int 11 2
        , prim__or_Int 11 4
        , prim__or_Int 11 11
        ]

orNegativeInt : List Int
orNegativeInt = [ prim__or_Int (-11) intmax
                , prim__or_Int (-11) 0
                , prim__or_Int (-11) 1
                , prim__or_Int (-11) 2
                , prim__or_Int (-11) 4
                , prim__or_Int (-11) 11
                , prim__or_Int (-11) intmin
                , prim__or_Int (-11) (-1)
                , prim__or_Int (-11) (-2)
                , prim__or_Int (-11) (-4)
                , prim__or_Int (-11) (-11)
                ]

--------------------------------------------------------------------------------
--          Bitwise XOR
--------------------------------------------------------------------------------

xorBits8 : List Bits8
xorBits8 = [ prim__xor_Bits8 11 b8max
           , prim__xor_Bits8 11 0
           , prim__xor_Bits8 11 1
           , prim__xor_Bits8 11 2
           , prim__xor_Bits8 11 4
           , prim__xor_Bits8 11 11
           ]

xorBits16 : List Bits16
xorBits16 = [ prim__xor_Bits16 11 b16max
            , prim__xor_Bits16 11 0
            , prim__xor_Bits16 11 1
            , prim__xor_Bits16 11 2
            , prim__xor_Bits16 11 4
            , prim__xor_Bits16 11 11
            ]

xorBits32 : List Bits32
xorBits32 = [ prim__xor_Bits32 11 b32max
            , prim__xor_Bits32 11 0
            , prim__xor_Bits32 11 1
            , prim__xor_Bits32 11 2
            , prim__xor_Bits32 11 4
            , prim__xor_Bits32 11 11
            ]

xorBits64 : List Bits64
xorBits64 = [ prim__xor_Bits64 11 b64max
            , prim__xor_Bits64 11 0
            , prim__xor_Bits64 11 1
            , prim__xor_Bits64 11 2
            , prim__xor_Bits64 11 4
            , prim__xor_Bits64 11 11
            ]

xorInteger : List Integer
xorInteger = [ prim__xor_Integer 11 (prim__shl_Integer 1 128 - 1)
             , prim__xor_Integer 11 0
             , prim__xor_Integer 11 1
             , prim__xor_Integer 11 2
             , prim__xor_Integer 11 4
             , prim__xor_Integer 11 11
             ]

xorInt : List Int
xorInt = [ prim__xor_Int 11 intmax
         , prim__xor_Int 11 0
         , prim__xor_Int 11 1
         , prim__xor_Int 11 2
         , prim__xor_Int 11 4
         , prim__xor_Int 11 11
         ]

xorNegativeInt : List Int
xorNegativeInt = [ prim__xor_Int (-11) intmax
                 , prim__xor_Int (-11) 0
                 , prim__xor_Int (-11) 1
                 , prim__xor_Int (-11) 2
                 , prim__xor_Int (-11) 4
                 , prim__xor_Int (-11) 11
                 , prim__xor_Int (-11) intmin
                 , prim__xor_Int (-11) (-1)
                 , prim__xor_Int (-11) (-2)
                 , prim__xor_Int (-11) (-4)
                 , prim__xor_Int (-11) (-11)
                 ]

--------------------------------------------------------------------------------
--          Running Tests
--------------------------------------------------------------------------------

main : IO ()
main = do printLn intmin

          putStrLn ""

          printLn shiftRBits8
          printLn shiftRBits16
          printLn shiftRBits32
          printLn shiftRBits64
          printLn shiftRInteger
          printLn shiftRInt
          printLn shiftRNegativeInt

          putStrLn ""

          printLn shiftLBits8
          printLn shiftLBits16
          printLn shiftLBits32
          printLn shiftLBits64
          printLn shiftLInteger
          printLn shiftLInt
          printLn shiftLNegativeInt

          putStrLn ""

          printLn andBits8
          printLn andBits16
          printLn andBits32
          printLn andBits64
          printLn andInteger
          printLn andInt
          printLn andNegativeInt

          putStrLn ""

          printLn orBits8
          printLn orBits16
          printLn orBits32
          printLn orBits64
          printLn orInteger
          printLn orInt
          printLn orNegativeInt

          putStrLn ""

          printLn xorBits8
          printLn xorBits16
          printLn xorBits32
          printLn xorBits64
          printLn xorInteger
          printLn xorInt
          printLn xorNegativeInt


text:
module ProveVoid

import Data.Vect

%default total

data In : (f : Type -> Type) -> Type where
  MkIn : In f

-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In x = In y -> x = y
injIn Refl = Refl

P : Type -> Type
P x = (a : (Type -> Type) ** (In a = x, a x -> Void))

func1 : P (In P) -> Void
func1 (a ** (InAEqInP, AAppInPImpVoid)) =
  let lem2 : (P (In P) -> Void) = replace {P=\ x => x (In P) -> Void} (injIn InAEqInP) AAppInPImpVoid
  in lem2 (P ** (Refl, lem2))

total -- for extra oumph!
lem2 : Void
lem2 =
  let foo : P (In P) = (P ** (Refl, func1))
  in func1 foo

ext: idr


text:
module Main

main : IO ()
main = printLn . map val . unpack $ "\x0a\x80\xC9\xFF\n3\n4"
  where
    -- make the values positive if the backend has signed chars
    val : Char -> Int
    val = flip mod 256 . (+256) . ord

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 Funktionen

hallo : String -> String
hallo name = "Hallo " ++ name

addieren : Int -> Int -> Int
addieren a b = a + b

addieren' : Int -> (Int -> Int)
addieren' a = \b => a + b

add10 : Int -> Int
add10 = addieren 10

identität : { ty : Type } -> ty -> ty
identität { ty = typ } val = val


text:
data ListLast : List a -> Type where
     Empty : ListLast []
     NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
                          Empty => NonEmpty [] x
                          NonEmpty xs y => NonEmpty (x :: xs) y

describeHelper : (input : List Int) -> ListLast input -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x)
        = "Non-empty, initial portion = " ++ show xs

describeListEnd : List Int -> String
describeListEnd xs = describeHelper xs (listLast xs)

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
AdderType : (numType : Type) -> (argc : Nat) -> Type
AdderType numType Z = numType
AdderType numType (S k) = (next : numType) -> AdderType numType k

adder : Num numType =>
  (argc : Nat) -> (acc : numType) -> AdderType numType argc
adder Z acc = acc
adder (S k) acc = \next => adder k (acc + next)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Toolkit.Data.Nat

%default total

public export
toNat : Int -> Nat
toNat = (integerToNat . cast)

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Specifications.OrderedGroup

import public Specifications.TranslationInvariance

%default total
%access public export

||| composed specification
data OrderedGroupSpec : Binop s -> s -> (s -> s) -> Binrel s -> Type where
  MkOrderedGroup :
    PartiallyOrderedGroupSpec op inv e leq ->
    isTotalOrder leq ->
    OrderedGroupSpec op inv e leq

||| forget
partiallyOrderedGroup : OrderedGroupSpec add zero neg leq ->
  PartiallyOrderedGroupSpec add zero neg leq
partiallyOrderedGroup (MkOrderedGroup p _) = p

||| forget
totalOrder : OrderedGroupSpec _ _ _ leq -> TotalOrderSpec leq
totalOrder (MkOrderedGroup p t) =
  MkTotalOrder (order (invariantOrder p)) t

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
> module Basic.Operations

> %default total

> %access public export

* Extensions of |replace|, |cong|

> |||
> replace2 : {a : _} -> {a1 : _} -> {a2 : _} ->
>            {b : _} -> {b1 : _} -> {b2 : _} ->
>            {P : a -> b -> Type} ->
>            (a1 = a2) -> (b1 = b2) -> P a1 b1 -> P a2 b2
> replace2 Refl Refl p = p

> |||
> cong2 : {alpha : Type} ->
>         {beta : Type} ->
>         {gamma : Type} ->
>         {a1 : alpha} ->
>         {a2 : alpha} ->
>         {b1 : beta} ->
>         {b2 : beta} ->
>         {f : alpha -> beta -> gamma} ->
>         (a1 = a2) ->
>         (b1 = b2) ->
>         f a1 b1 = f a2 b2
> cong2 Refl Refl = Refl

> |||
> depCong1 : {alpha : Type} ->
>            {P : alpha -> Type} ->
>            {a1 : alpha} ->
>            {a2 : alpha} ->
>            {f : (a : alpha) -> P a} ->
>            (a1 = a2) ->
>            f a1 = f a2
> depCong1 Refl = Refl

> |||
> depCong2 : {alpha : Type} ->
>            {P : alpha -> Type} ->
>            {gamma : Type} ->
>            {a1 : alpha} ->
>            {a2 : alpha} ->
>            {Pa1 : P a1} ->
>            {Pa2 : P a2} ->
>            {f : (a : alpha) -> P a -> gamma} ->
>            (a1 = a2) ->
>            (Pa1 = Pa2) ->
>            f a1 Pa1 = f a2 Pa2
> depCong2 Refl Refl = Refl

> |||
> depCong2' : {alpha : Type} ->
>             {P : alpha -> Type} ->
>             {Q : (a : alpha) -> P a -> Type} ->
>             {a1 : alpha} ->
>             {a2 : alpha} ->
>             {Pa1 : P a1} ->
>             {Pa2 : P a2} ->
>             {f : (a : alpha) -> (pa : P a) -> Q a pa} ->
>             (a1 = a2) ->
>             (Pa1 = Pa2) ->
>             f a1 Pa1 = f a2 Pa2
> depCong2' Refl Refl = Refl

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.RandomAccessList

import Data.Fin

%default total

-- TODO: Use idris-quickcheck to verify that the chosen implementation matches the
-- behavior of an implementation that uses induction (see comments)
select : (size1 : Nat) -> {size2 : Nat} -> Fin (size1 + size2) -> Either (Fin size1) (Fin size2)
-- select Z {size2} idx = Right idx
-- select (S size1) FZ = Left FZ
-- select (S size1) {size2} (FS idx)
--   = case select size1 idx of
--     Left n => Left $ FS n
--     Right n => Right n
select size1 {size2 = Z} idx = Left $ rewrite sym $ plusZeroRightNeutral size1 in idx
select size1 {size2 = S _} idx
  = let idxInt = finToInteger idx in
    case integerToFin idxInt size1 of
    Just idx' => Left idx'
    Nothing => Right $ restrict _ (idxInt - cast size1)

data Tree : (size : Nat) -> (ty : Type) -> Type where
  Singleton : (value : ty) -> Tree (S Z) ty
  Merged : .{halfSize : Nat} -> (left : Tree halfSize ty) -> (right : Tree halfSize ty) -> Tree (halfSize + halfSize) ty

treeLookup : {size : Nat} -> Fin size -> Tree size ty -> ty
treeLookup FZ (Singleton x) = x
treeLookup {size = halfSize + halfSize} idx (Merged left right) with (select halfSize idx)
  | (Left idx') = treeLookup idx' left
  | (Right idx') = treeLookup idx' right

treeUpdate : {size : Nat} -> Fin size -> Tree size ty -> (ty -> ty) -> Tree size ty
treeUpdate FZ (Singleton x) f = Singleton $ f x
treeUpdate {size = halfSize + halfSize} idx (Merged left right) f with (select halfSize idx)
  | (Left idx') = Merged (treeUpdate idx' left f) right
  | (Right idx') = Merged left (treeUpdate idx' right f)

pow2 : Nat -> Nat
pow2 n = power 2 n

data TreeList : (pos : Nat) -> (size : Nat) -> (ty : Type) -> Type where
  Nil : TreeList _ Z _
  (::) : {nextPos : Nat} -> .{auto posPrf : LT pos nextPos}
         -> .{size : Nat} -> .{auto smaller : LTE (pow2 pos) size}
         -> Tree (pow2 pos) ty -> TreeList nextPos (size - (pow2 pos)) ty
         -> TreeList pos size ty

minusLeftPlusRight : {x, y, z : Nat} -> {auto smaller : LTE y x}
                  -> x - y = z -> x = y + z
minusLeftPlusRight {x} {y = Z} {z} prf = rewrite sym $ minusZeroRight x in prf
minusLeftPlusRight {x = Z} {y = S _} _ impossible
minusLeftPlusRight {x = S x'} {y = S y'} {z} {smaller} prf
  = let smaller' = fromLteSucc smaller
        prf' = replace {P = \var => var = z} (minusSuccSucc x' y') prf
        ind = minusLeftPlusRight prf' in
    cong {f = S} ind

treeSizeComponents : (pos, size : Nat) -> {auto smaller : LTE (pow2 pos) size}
                     -> size = pow2 pos + (size - pow2 pos)
treeSizeComponents pos size {smaller} = minusLeftPlusRight Refl

treeListLookup : {pos, size : Nat} -> Fin size -> TreeList pos size ty -> ty
treeListLookup {pos} {size} idx (t :: ts)
  with (let eqPrf = treeSizeComponents pos size
            idx' = (replace {P = \x => Fin x} eqPrf idx) in
        select (pow2 pos) idx')
  | (Left idx') = treeLookup idx' t
  | (Right idx') = treeListLookup idx' ts

treeListUpdate : {pos, size : Nat} -> Fin size -> TreeList pos size ty -> (ty -> ty) -> TreeList pos size ty
treeListUpdate {pos} {size} idx (t :: ts) f
  with (let eqPrf = treeSizeComponents pos size
            idx' = (replace {P = \x => Fin x} eqPrf idx) in
        select (pow2 pos) idx')
  | (Left idx') = treeUpdate idx' t f :: ts
  | (Right idx') = t :: treeListUpdate idx' ts f

pow2Lemma : (x : Nat) -> (pow2 x + pow2 x) = pow2 (S x)
pow2Lemma Z = Refl
pow2Lemma (S x)
  = let hyp = pow2Lemma x in
    rewrite sym hyp in
    rewrite plusZeroRightNeutral (pow2 x + pow2 x) in
    Refl

lteAddLeft : (m, n : Nat) -> LTE n (m + n)
lteAddLeft m n = rewrite plusCommutative m n in lteAddRight {m} n

ltAddRight : (n : Nat) -> {m : Nat} -> LT n (n + (S m))
ltAddRight n {m} = rewrite sym $ plusSuccRightSucc n m in lteAddRight {m} (S n)

lteAddBoth : {x, y, x', y' : Nat} -> LTE x y -> LTE x' y' -> LTE (x + x') (y + y')
lteAddBoth {x' = S _} {y' = Z} _ _ impossible
lteAddBoth {x} {y} {x' = Z} {y'} smaller _
  = rewrite plusZeroRightNeutral x in
    lteTransitive smaller (lteAddRight y)
lteAddBoth {x} {y} {x' = S x''} {y' = S y''} smaller smaller'
  = let ind = lteAddBoth smaller (fromLteSucc smaller') in
    rewrite sym $ plusSuccRightSucc x x'' in
    rewrite sym $ plusSuccRightSucc y y'' in
    LTESucc ind

pow2Monotone : {n, m : Nat} -> LTE n m -> LTE (pow2 n) (pow2 m)
pow2Monotone {n = Z} {m = Z} _ = LTESucc LTEZero
pow2Monotone {n = Z} {m = S m'} _
  = let prf = pow2Monotone {n = Z} {m = m'} LTEZero in
    lteTransitive prf (lteAddRight (pow2 m') {m = (pow2 m' + 0)})
pow2Monotone {n = S _} {m = Z} _ impossible
pow2Monotone {n = S n'} {m = S m'} smaller
  = let prf = pow2Monotone {n = n'} {m = m'} (fromLteSucc smaller)
        prf' = lteAddBoth prf (lteRefl {n = Z}) in
    lteAddBoth prf prf'

minusPlusNeutral : (x, y : Nat) -> LTE y x -> (x - y) + y = x
minusPlusNeutral x Z _
  = replace {P = \var => var = x}
            (sym $ plusZeroRightNeutral (x `minus` Z))
            (minusZeroRight x)
minusPlusNeutral Z (S _) _ impossible
minusPlusNeutral (S x) (S y) prf
  = let ind = minusPlusNeutral x y (fromLteSucc prf)
        succPrf = plusSuccRightSucc (x `minus` y) y in
    rewrite sym succPrf in
    cong {f = S} ind

plusMinusAssociative : (a, b, c : Nat) -> {auto smaller : LTE c b} -> a + (b `minus` c) = (a + b) `minus` c
plusMinusAssociative a b Z
  = rewrite minusZeroRight b in
    rewrite minusZeroRight (a + b) in
    Refl
plusMinusAssociative a Z (S _) impossible
plusMinusAssociative a (S b) (S c) {smaller}
  = let ind = plusMinusAssociative {smaller = fromLteSucc smaller} a b c
        succPrf = sym $ minusSuccSucc (a + b) c
        p = \x => (a + b) `minus` c = x `minus` (S c)
        succPrf' = replace {P = p} (plusSuccRightSucc a b) succPrf in
    replace {P = \x => a + (b `minus` c) = x} succPrf' ind

lteReflAddLeftContra : LTE (x + S y) x -> Void
lteReflAddLeftContra {x = S _} LTEZero impossible
lteReflAddLeftContra (LTESucc {left = Z + S y} {right = Z} prf) impossible
lteReflAddLeftContra (LTESucc {left = S x + S y} {right = S x} prf) = absurd $ lteReflAddLeftContra prf

treeListCons : {tPos, pos : Nat} -> Tree (pow2 tPos) ty -> TreeList pos size ty -> .{auto fits : LTE tPos pos}
               -> (newPos : Nat ** TreeList newPos (size + (pow2 tPos)) ty)
treeListCons {ty} {tPos} t Nil = rewrite plusCommutative Z (pow2 tPos) in
                                 rewrite plusZeroRightNeutral (pow2 tPos) in
                                 let nil = replace {P = \x => TreeList (S tPos) x ty}
                                                   (minusZeroN (pow2 tPos))
                                                   RandomAccessList.Nil
                                     ts' = (::) {nextPos = S tPos} {posPrf = lteRefl} {smaller = lteRefl} t nil in
                                 (tPos ** ts')
treeListCons {tPos} {pos} {size} t' ((::) {smaller} t ts) {fits} {ty}
  = case cmp tPos pos of
    CmpEQ => let merged = Merged t' t
                 merged' = replace {P = \x => Tree x ty} (pow2Lemma tPos) merged
                 (newPos ** ts') = treeListCons {tPos = S tPos} merged' ts in
             rewrite sym $ plusZeroRightNeutral (pow2 tPos) in
             rewrite sym $ minusPlusNeutral size (pow2 tPos) $
                     lteTransitive (pow2Monotone fits) smaller in
             rewrite sym $ plusAssociative (size `minus` pow2 tPos) (pow2 tPos) (pow2 tPos + Z) in
             (newPos ** ts')
    CmpLT diff => let p = plusZeroRightNeutral size
                      p' = minusZeroN $ pow2 tPos
                      p'' = replace {P = \x => size + x = size} p' p
                      p''' = replace {P = \x => x = size} (plusMinusAssociative {smaller = lteRefl} size (pow2 tPos) (pow2 tPos)) p''
                      ts' = (::) {smaller} t ts
                      ts'' = replace {P = \s => TreeList (tPos + (S diff)) s ty} (sym p''') ts'
                      ts''' = RandomAccessList.(::) {posPrf = ltAddRight tPos} {smaller = lteAddLeft size (pow2 tPos)} t' ts'' in
                  (tPos ** ts''')
    CmpGT diff => absurd $ lteReflAddLeftContra fits

pow2StrictlyPositive : (n : Nat) -> LTE 1 (pow2 n)
pow2StrictlyPositive Z = lteRefl
pow2StrictlyPositive (S n)
  = let ind = pow2StrictlyPositive n in
    lteTransitive ind (lteAddRight {m = pow2 n + Z} (pow2 n))

equalsNotLT : {n, m : Nat} -> n = m -> LT n m -> Void
equalsNotLT {n = Z} {m = Z} _ lt impossible
equalsNotLT {n = Z} {m = S _} Refl _ impossible
equalsNotLT {n = S _} {m = Z} Refl _ impossible
equalsNotLT {n = S n'} {m = S m'} eq (LTESucc lt')
  = equalsNotLT (cong {f = Nat.pred} eq) lt'

treeListTailHelper : {tPos, tsPos, size : Nat}
                  -> Tree (pow2 tPos) ty
                  -> TreeList tsPos size ty
                  -> {posPrf : LTE tPos tsPos}
                  -> let smaller = lteTransitive (pow2StrictlyPositive tPos)
                                                 (lteAddRight {m = size} (pow2 tPos)) in
                     (pos' ** TreeList pos' ((-) {smaller} (pow2 tPos + size) (S Z)) ty)
treeListTailHelper {size} {tPos = Z} _ ts = rewrite minusZeroRight size in (_ ** ts)
treeListTailHelper {ty} {size} {tPos = S pos'} t {tsPos} {posPrf} ts
  = let (_ ** (t', eqPrf)) = eraseSize t in
    case t' of
      Singleton _ => void $ notSingleton eqPrf
      Merged {halfSize} l r =>
        let eqPrf' = replace {P = \y => halfSize + halfSize = pow2 pos' + y} (plusZeroRightNeutral $ pow2 pos') eqPrf
            l' = replace {P = \x => Tree x ty} (halve eqPrf') l
            r' = replace {P = \x => Tree x ty} (halve eqPrf') r
            p = plusZeroRightNeutral size
            p' = minusZeroN $ pow2 pos'
            p'' = replace {P = \x => size + x = size} p' p
            p''' = replace {P = \x => x = size} (plusMinusAssociative {smaller = lteRefl} size (pow2 pos') (pow2 pos')) p''
            ts' = replace {P = \x => TreeList tsPos x ty} (sym p''') ts
            ts'' = RandomAccessList.(::) {posPrf} {smaller = lteAddLeft size (pow2 pos')} r' ts' in
        rewrite plusZeroRightNeutral (pow2 pos') in
        rewrite sym $ plusAssociative (pow2 pos') (pow2 pos') size in
        rewrite plusCommutative (pow2 pos') size in
        treeListTailHelper {posPrf = lteRefl} l' ts''
    where eraseSize : {n : Nat} -> Tree n ty -> (n' : Nat ** (Tree n' ty, n' = n))
          eraseSize t = (_ ** (t, Refl))
          halve : {x, y : Nat} -> x + x = y + y -> x = y
          halve {x = Z} {y = S _} Refl impossible
          halve {x = S _} {y = Z} Refl impossible
          halve {x = Z} {y = Z} _ = Refl
          halve {x = S x'} {y = S y'} prf = cong {f = S} $ halve prev
            where prev : x' + x' = y' + y'
                  prev = let prf' = replace {P = \var => var = S (S y' + y')}
                                            (sym $ plusSuccRightSucc (S x') x') $
                                    replace {P = \var => S x' + S x' = var}
                                            (sym $ plusSuccRightSucc (S y') y')
                                            prf in
                         cong {f = Nat.pred . Nat.pred} prf'
          notSingleton : {n : Nat} -> 1 = (pow2 n) + (pow2 n + Z) -> Void
          notSingleton {n} eq
            = let eq' = replace {P = \var => 1 = pow2 n + var}
                                (plusZeroRightNeutral $ pow2 n)
                                eq
                  lte = pow2StrictlyPositive n
                  lte' = lteAddBoth lte lte in
              void $ equalsNotLT eq' lte'

treeListTail : {pos, size : Nat} -> TreeList pos (S size) ty -> (newPos : Nat ** TreeList newPos size ty)
treeListTail {ty} {pos} {size} ((::) {posPrf} t ts)
  = let (newPos ** newList) = treeListTailHelper {posPrf = lteSuccLeft posPrf} t ts
        p = plusMinusAssociative (pow2 pos) (S size) (pow2 pos)
        newList' = replace {P = \x => TreeList newPos (x `minus` 1) ty} p newList
        p' = plusCommutative (pow2 pos) (S size)
        newList'' = replace {P = \x => TreeList newPos ((x `minus` pow2 pos) `minus` 1) ty} p' newList'
        p'' = sym $ plusMinusAssociative {smaller = lteRefl} (S size) (pow2 pos) (pow2 pos)
        newList''' = replace {P = \x => TreeList newPos (x `minus` 1) ty} p'' newList'' in
    rewrite sym $ plusZeroRightNeutral size in
    rewrite minusZeroN $ pow2 pos in
    rewrite sym $ minusZeroRight (size + (pow2 pos `minus` pow2 pos)) in
    (newPos ** newList''')

namespace RandomAccessList
  export
  RandomAccessList : Nat -> Type -> Type
  RandomAccessList size ty = (pos : Nat ** TreeList pos size ty)

  export
  empty : RandomAccessList Z ty
  empty = (Z ** Nil)

  export
  cons : ty -> RandomAccessList size ty -> RandomAccessList (S size) ty
  cons {size} x (pos ** l)
    = let (pos' ** l') = treeListCons (Singleton x) l in
      rewrite plusCommutative (S Z) size in
      (pos' ** l')

  export
  tail : {size : Nat} -> RandomAccessList (S size) ty -> RandomAccessList size ty
  tail (pos ** l) = treeListTail l

  export
  index : {size : Nat} -> Fin size -> RandomAccessList size ty -> ty
  index idx (pos ** l) = treeListLookup idx l

  export
  update : {size : Nat} -> Fin size -> RandomAccessList size ty -> (ty -> ty) -> RandomAccessList size ty
  update idx (pos ** l) f = (pos ** treeListUpdate idx l f)

namespace CountedRandomAccessList
  export
  CountedRandomAccessList : Type -> Type
  CountedRandomAccessList ty = (len : Nat ** RandomAccessList len ty)

  export
  empty : CountedRandomAccessList ty
  empty = (Z ** RandomAccessList.empty)

  export
  cons : ty -> CountedRandomAccessList ty -> CountedRandomAccessList ty
  cons x (size ** arr) = (S size ** cons x arr)

  export
  tail : CountedRandomAccessList ty -> CountedRandomAccessList ty
  tail (Z ** arr) = (Z ** arr)
  tail (S size ** arr) = (size ** tail arr)

  export
  size : CountedRandomAccessList ty -> Nat
  size (size ** _) = size

  export
  index : (idx : Nat) -> (carr : CountedRandomAccessList ty) -> Maybe ty
  index idx (size ** arr)
    = do finIdx <- natToFin idx size
         pure $ index finIdx arr

  export
  update : (idx : Nat) -> (carr : CountedRandomAccessList ty) -> (ty -> ty) -> CountedRandomAccessList ty
  update idx (size ** arr) f
    = maybe (size ** arr)
            (\finIdx => (size ** update finIdx arr f))
            (natToFin idx size)

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
module Replica.TestConfig.Parser

import public Text.Parser

import System.File

import Replica.TestConfig.Core
import Replica.TestConfig.Lexer

public export
Rule : Type -> Type
Rule = Grammar (TokenData Token) True

export
key : String -> Rule ()
key k = terminal ("Expected key " ++ k)
  \x => case tok x of
             Word y      => guard $ k == y
             StringLit y => guard $ k == y
             _ => Nothing

export
ident : Rule String
ident = terminal "Expected ident"
  \x => case tok x of
             Word y      => Just y
             _ => Nothing

export
equals : Rule ()
equals = terminal "Expected equals"
  \x => case tok x of
             Equals => Just ()
             _ => Nothing

export
stringLit : Rule String
stringLit = terminal "Expected String literal"
  \x => case tok x of
             StringLit str => Just str
             _ => Nothing

export
string : Rule String
string = terminal "Expected string"
  \x => case tok x of
             Word y      => Just y
             StringLit y => Just y
             _ => Nothing

export
separator : Rule ()
separator = terminal "Expected String literal"
  \x => case tok x of
             Separator str => Just ()
             _ => Nothing

export
identPath : Rule Path
identPath = sepBy1' separator ident

export
path : Rule Path
path = identPath <|> fail "A Path is expected"

export
Value : Type
Value = Either Path String

export
test : Rule Path
test = (key "test" *> path) <|>fail "No test preamble"

export
keyValue : Rule (String, Value)
keyValue =  MkPair <$> ident <*> (equals *> (map Left path <|> map Right string))

export
testConfig : Rule $ DPair (List (String, Value)) NonEmpty
testConfig = do
  x <- map (MkPair "test" . Left) test
  xs <- many keyValue
  pure ((x :: xs) ** IsNonEmpty)

foldBuilder : DPair (List (String, Value)) NonEmpty -> BuildTestConfig
foldBuilder = concatMap (uncurry toBuilder) . fst
  where
    pathToString : Path -> String
    pathToString (MkDPair path snd) = foldr1 (\x, y => x ++ "/" ++ y) path

    valueToString : Value -> String
    valueToString = either pathToString id

    toBuilder : String -> Value -> BuildTestConfig
    toBuilder "test" (Left y) = record {path = [y]} emptyBuilder
    toBuilder "exec" y = record {exec = [valueToString y]} emptyBuilder
    toBuilder "params" y = record {params = [valueToString y]} emptyBuilder
    toBuilder "input" y = record {inputFile = [Just $ valueToString y]} emptyBuilder
    toBuilder "inputFile" y = record {inputFile = [Just $ valueToString y]} emptyBuilder
    toBuilder "output" y = record {outputFile = [valueToString y]} emptyBuilder
    toBuilder "outputFile" y = record {outputFile = [valueToString y]} emptyBuilder
    toBuilder x y = emptyBuilder

public export
data ParsingError err
  = FileNotFound FileError
  | LexerFailed (Int, Int, String)
  | ParserFailed (ParseError (TokenData Token))
  | TargetError err

export
displayParsingError : (err -> String) -> ParsingError err -> String
displayParsingError _ (FileNotFound x)
  = show x
displayParsingError _ (LexerFailed (l,c,msg))
  = "Syntax error: line " ++ show l ++ "; column: " ++ show c ++"; " ++ msg
displayParsingError _ (ParserFailed (Error msg xs))
  = "Cannot parse file: " ++ msg
displayParsingError f (TargetError x)
  = "Cannot build expected value: " ++ f x

export
parseTestConfig : (filename : String) -> IO (Either (ParsingError BuildError) TestConfig)
parseTestConfig filename = do
  Right str <- readFile filename
    | Left err => pure $ Left $ FileNotFound err
  pure $ runParser str

  where

    mapError : (a -> b) -> Either a c -> Either b c
    mapError f (Left x) = Left (f x)
    mapError f (Right x) = Right x

    runParser : String -> Either (ParsingError BuildError) TestConfig
    runParser  str = do
      tokens <- mapError LexerFailed $ lex str
      (cfg, []) <- mapError ParserFailed $ parse testConfig tokens
        | (_, err) => Left $ ParserFailed (Error "Cannot parse tokens"  err)
      mapError TargetError $ build $ foldBuilder cfg

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
module FLK_ast

import Data.SortedMap

Ident : Type
Ident = String

data OpTy = Arith | Rel | Gen | Bool

data Op1 = Not

instance Show Op1 where
  show Not = "Not"

data Op2 : OpTy -> Type where
  Plus   : Op2 Arith
  Minus  : Op2 Arith
  LThan  : Op2 Rel
  LEThan : Op2 Rel
  GThan  : Op2 Rel
  GEThan : Op2 Rel
  EQ     : Op2 Gen
  NEQ    : Op2 Gen

instance Show (Op2 a) where
  show Plus = "+"
  show Minus = "-"
  show LThan = "<"
  show LEThan = "<="
  show GThan = ">"
  show GEThan = ">="
  show EQ = "="
  show NEQ = "!="

data Status = Inter | Done | Lam | RecLam

total
arithOp : Op2 Arith -> Nat -> Nat -> Nat
arithOp Plus  = (+)
arithOp Minus = (-)

total
relop : Op2 Rel -> Nat -> Nat -> Bool
relop LThan  = (<)
relop LEThan = (<=)
relop GThan  = (>)
relop GEThan = (>=)

-- Basic ADT for FLK
-- Status phantom type is used to tag useful subsets of the grammar

mutual
  Env : Type
  Env = SortedMap Ident (Exp Done `Either` Exp RecLam)

  data Exp : Status -> Type where
    App   : Exp a   -> Exp b          -> Exp Inter
    Abs   : Ident   -> Exp a          -> Exp Lam
    Rec   : Ident   -> Exp a          -> Exp RecLam
    If    : Exp a   -> Exp b -> Exp c -> Exp Inter
    Prim1 : Op1     -> Exp a          -> Exp Inter
    Prim2 : Op2 y   -> Exp a -> Exp b -> Exp Inter
    N     : Nat                       -> Exp Done
    B     : Bool                      -> Exp Done
    Clos  : Env     -> Exp Lam        -> Exp Done
    Id    : Ident                     -> Exp Inter

syntax "((" [exp] [e1] [e2] "))" = "("++exp++" "++(show e1)++" "++(show e2)++")";

instance Show (Exp a) where
  show (App x y) = (("" x y))
  show (Abs x y) = (("lambda" x y))
  show (Rec x y) = (("rec" x y))
  show (If x y z) = ((("if "++(show x)) y z))
  show (Prim1 x y) = (("" x y))
  show (Prim2 x z w) = (((show x) z w))
  show (N k) = (show k)
  show (B x) = (show x)
  show (Clos x y) = (("Clos" (map fst $ SortedMap.toList x) y))
  show (Id x) = (show x)

genOp : Op2 Gen -> Exp Done -> Exp Done -> Exp Done
genOp EQ (N k) (N j) = B (j == k)
genOp NEQ (N k) (N j) = B $ not (j == k)
genOp EQ (B y) (B x2) = B (y == x2)
genOp NEQ (B y) (B x2) = B $ not (y == x2)
genOp EQ a b = B False
genOp NEQ a b = B True

emptyEnv : Env
emptyEnv = empty
infixr 7 >-
data CF : Status -> Type where
  (>-) : {s : Status} -> (Exp s) -> Env -> (CF s)

instance Show (CF a) where
  show (x >- z) = "<" ++ show x ++ ", "++ (show $ map fst $ SortedMap.toList z)++ ">"

-- grab value from type
total
getTag : {b : Status} -> (state : Exp b) -> Status
getTag {b=b} _ = b

-- grab value from type
total
getOpT : {b : OpTy} -> Op2 b -> OpTy
getOpT {b=b} _ = b
-- construct proof of containment with dependent pattern matching
idSteps :  (ident : Ident)
        -> (env : Env)
        -> Maybe (Sigma (Exp Done) (\v => lookup ident env = (Just (Left v))))
idSteps ident env with (lookup ident env)
  idSteps ident env | Nothing = Nothing
  idSteps ident env | (Just x) = h1 x ident env
where h1 : (x : Either (Exp Done) (Exp RecLam))
        -> String -> Env -> Maybe (Sigma (Exp Done) (\v => Just x = Just (Left v)))
      h1 (Left x) x1 x2 = Just (x ** Refl)
      h1 (Right x) x1 x2 = Nothing

-- construct proof of containment with dependent pattern matching
idRecSteps : (ident : Ident)
        -> (env : Env)
        -> Maybe (Sigma (Exp RecLam) (\v => lookup ident env = (Just (Right v))))
idRecSteps ident env with (lookup ident env)
  idRecSteps ident env | Nothing = Nothing
  idRecSteps ident env | (Just x) = h1 x ident env
where h1 : (x : Either (Exp Done) (Exp RecLam))
        -> String -> Env -> Maybe (Sigma (Exp RecLam) (\v => Just x = Just (Right v)))
      h1 (Left x) x1 x2 = Nothing
      h1 (Right x) x1 x2 = Just (x ** Refl)

yexpr : (Exp Inter)
yexpr = (App (App (Abs "f" (App (Abs "x" (App (Id "x") (Id "x"))) (Abs "g" (App (Id "f") (Abs "x" (App (App (Id "g") (Id "g")) (Id "x"))))))) (Abs "f" (Abs "n" (If (Prim2 EQ (Id "n") (N 0)) (N 0) (Prim2 Plus (Id "n") (App (Id "f") (Prim2 Minus (Id "n") (N 1)))))))) (N 4))

ycomb : (s ** CF s)
ycomb = (Inter ** yexpr >- emptyEnv)

max_stars_repo_name: ezrosent/FLK-Semantics

max_issues_repo_name: ezrosent/FLK-Semantics

max_forks_repo_name: ezrosent/FLK-Semantics


text:
module HintFunctionGen

export
record Gen a where
  constructor MkGen
  cont : List a

export
Functor Gen where
  map f (MkGen xs) = MkGen $ f <$> xs

export
Applicative Gen where
  pure = MkGen . pure
  MkGen xs <*> MkGen ys = MkGen $ xs <*> ys

export
Alternative Gen where
  empty = MkGen empty
  MkGen xs <|> mys = MkGen $ xs <|> mys.cont

export
Monad Gen where
  MkGen xs >>= f = MkGen $ xs >>= cont . f

export
Show a => Show (Gen a) where
  show = ("gen " ++) . show . cont

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Hangman

import Data.Vect

data WordState : (guesses: Nat) -> (letters: Nat) -> Type where
  MkWordState : (word: String) -> (missing: Vect letters Char) -> WordState guesses_remaining letters

-- data Finished: Type where
--   Lost: (game: WordState 0 (S letters)) -> Finished
--   Won: (game: WordState (S guesses) 0) -> Finished

letters: String -> List Char
letters str = nub (map toUpper (unpack str))

data GameState : Type where
  NotRunning: GameState
  Running: (guesses: Nat) -> (letters: Nat) -> GameState

data GuessResult = Correct | Incorrect

data GameCmd : (ty: Type) -> GameState -> (ty -> GameState) -> Type where

  NewGame: (word: String) -> GameCmd () NotRunning (const (Running 6 (List.length (letters word))))

  Won : GameCmd () (Running (S guesses) 0) (const NotRunning)

  Lost: GameCmd () (Running 0 (S guesses)) (const NotRunning)

  Pure: (res: ty) -> GameCmd ty (state_fn res) (state_fn)

  (>>=): GameCmd a state1 state2_fn -> ((res: a) -> GameCmd b (state2_fn res) state3) -> GameCmd b state1 state3_fn

  ShowState: GameCmd () state (const state)

  Guess: (c: Char) ->
         GameCmd GuessResult (Running (S guesses) (S letters))
                             (\res => case res of
                                           Correct => Running (S guesses) letters
                                           Incorrect => Running guesses (S letters))

  Message: String -> GameCmd () state (const state)

  ReadGuess: GameCmd Char state (const state)

namespace Loop
  data GameLoop: (ty: Type) -> GameState -> (ty -> GameState) -> Type where
    (>>=):  GameCmd a state1 state2_fn -> ((res: a) -> Inf (GameLoop b (state2_fn res) state3_fn)) -> GameLoop b state1 state3_fn
    Exit: GameLoop () NotRunning (const NotRunning)

gameLoop : GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
gameLoop {guesses} {letters} = do
  ShowState
  g <- ReadGuess
  ok <- Guess g
  case ok of
    Correct => case letters of
                    Z => do Won
                            ShowState
                            Exit
                    S k => do Message "Correct"
                              gameLoop
    Incorrect => case guesses of
              Z => do Lost
                      ShowState
                      Exit
              S k => do Message "Incorrect"
                        gameLoop

hangman: GameLoop () NotRunning (const NotRunning)
hangman = do NewGame "testing"
             gameLoop

data Game: GameState -> Type where
  GameStart: Game NotRunning
  GameWon: (word: String) -> Game NotRunning
  GameLost: (word: String) -> Game NotRunning
  InProgress: (word: String) -> (guesses: Nat) -> (missing: Vect letters Char)

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Test.Int16

import Data.Prim.Int16
import Data.SOP
import Hedgehog
import Test.RingLaws

allInt16 : Gen Int16
allInt16 = int16 (linear (-0x8000) 0xffff)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allInt16
  (b8 <= MaxInt16) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allInt16
  (b8 >= MinInt16) === True

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allInt16, allInt16]
  toOrdering (comp m n) === compare m n

export
props : Group
props = MkGroup "Int16" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  ] ++ ringProps allInt16


text:
-- ----------------------------------------------------------------- [ Lib.idr ]
-- Module    : Lib.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A library of Patterns
module Sif.Library

import Effect.Default

import Sif.Types
import Sif.Pattern

import public Data.DList
import public Data.AVL.Dict

-- -------------------------------------------------------------- [ Directives ]
%access export

-- --------------------------------------------------------- [ Data Structures ]
public export
record LibEntry (impl : SifTy -> SifDomain -> Type) where
  constructor MkEntry
  idx   : Nat
  entry : PATTERN impl d

public export
record SifLib where
  constructor MkSLib
  counter : Nat
  patts   : DList (SifTy -> SifDomain -> Type) LibEntry is

emptyLib : SifLib
emptyLib = MkSLib Z Nil

addToLibrary : PATTERN impl d -> SifLib -> SifLib
addToLibrary p (MkSLib c ps) = MkSLib (S c) (MkEntry c p::ps)

addToLibraryM : List (PATTERN impl d) -> SifLib -> SifLib
addToLibraryM xs lib = foldl (flip $ addToLibrary) lib xs

defaultLib : SifLib
defaultLib = emptyLib

Default SifLib where
  default = defaultLib

getLibraryIndex : SifLib -> Dict Nat String
getLibraryIndex lib = Dict.fromList idx
  where
    f : LibEntry impl -> (Nat, String)
    f (MkEntry n p) = (n, unwords ["Pattern:", SifExpr.getTitle p])

    idx : List (Nat, String)
    idx = mapDList f (patts lib)

getPatternByIndex : Nat -> SifLib -> Maybe (d ** (impl ** PATTERN impl d))
getPatternByIndex n lib =
  case index (minus (length (patts lib)) (n + 1)) (patts lib) of
    Nothing       => Nothing
    Just (_ ** p) => Just (_ ** (_ ** entry p))

indexToString : Dict Nat String -> String
indexToString idx = unlines res
  where
    itemToString : (Nat, String) -> List String -> List String
    itemToString (i,t) rs = (unwords [show i, "<--", t]) :: rs

    res : List String
    res = foldr (itemToString) Nil $ Dict.toList idx

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Graphics.DOT.Lexer

import Text.Lexer
import Data.String
import Data.List

%default total

public export
data DOTToken : Type where
  ||| A keyword
  Keyword : (kw : String) -> DOTToken

  ||| An identifier as a name
  NameID : (name : String) -> DOTToken
  ||| An identifier as a numeral
  NumeralID : (numeral : String) -> DOTToken
  ||| An identifier as a double-quoted string
  StringID : (str : String) -> DOTToken
  ||| An identifier as a HTML string
  HTML_ID : (html : String) -> DOTToken

  ||| An edge operation in a directed graph
  DiGrEdgeOp : DOTToken
  ||| An edge operation in a graph
  GrEdgeOp : DOTToken
  ||| A compass point (used in combination with ports)
  CompassPt : (pt : String) -> DOTToken
  ||| A comment
  Comment : DOTToken
  ||| A multiline indicator
  MultilineBackslash : DOTToken
  ||| A double-quoted-string concatenation operator ('+')
  StrConcat : DOTToken

  ||| Any amount of whitespace
  Whitespace : DOTToken

  ||| [
  LBracket : DOTToken
  ||| ]
  RBracket : DOTToken
  ||| {
  LBrace : DOTToken
  ||| }
  RBrace : DOTToken
  ||| ,
  Comma : DOTToken
  ||| ;
  Semicolon : DOTToken
  ||| :
  Colon : DOTToken
  ||| =
  Equal : DOTToken

export
Show DOTToken where
  show (Keyword kw) = "(KW " ++ kw ++ ")"
  show (NameID name) = "(NameID " ++ name ++ ")"
  show (NumeralID numeral) = "(NumeralID " ++ numeral ++ ")"
  show (StringID str) = "(StringID " ++ str ++ ")"
  show (HTML_ID html) = "(HTML_ID " ++ html ++ ")"
  show DiGrEdgeOp = "DiEO"
  show GrEdgeOp = "GrEO"
  show (CompassPt pt) = "(CPt " ++ pt ++ ")"
  show Comment = "COMMENT"
  show MultilineBackslash = "MLB"
  show StrConcat = "STR++"
  show Whitespace = "WS"
  show LBracket = "LBracket"
  show RBracket = "RBracket"
  show LBrace = "LBrace"
  show RBrace = "RBrace"
  show Comma = "Comma"
  show Semicolon = "Semicolon"
  show Colon = "Colon"
  show Equal = "EQ"

-- Keywords --

-- DOT keywords are case-insensitive

nodeKW : Lexer
nodeKW = approx "node"

edgeKW : Lexer
edgeKW = approx "edge"

graphKW : Lexer
graphKW = approx "graph"

digraphKW : Lexer
digraphKW = approx "digraph"

subgraphKW : Lexer
subgraphKW = approx "subgraph"

strictKW : Lexer
strictKW = approx "strict"

||| Keywords are "node", "edge", "graph", "digraph", "subgraph", and "strict"
||| (without the quotes)
keyword : Lexer
keyword =  nodeKW
       <|> edgeKW
       <|> graphKW
       <|> digraphKW
       <|> subgraphKW
       <|> strictKW

-- Identifiers --

underscore : Lexer
underscore = is '_'

nameIDHead : Lexer
nameIDHead =  alpha
          <|> underscore

nameIDRest : Lexer
nameIDRest =  alphaNum
          <|> underscore

||| Any string of alphabetic characters, underscores, or digits, not beginning
||| with a digit.
nameID : Lexer
nameID = nameIDHead <+> many nameIDRest

minus : Lexer
minus = is '-'

fullStop : Lexer
fullStop = is '.'

-- \.[0-9]+
dotNum : Lexer
dotNum = fullStop <+> digits

-- \.[0-9]*
decimalNumRest : Lexer
decimalNumRest = fullStop <+> many digit

-- [0-9]+(\.[0-9]*)?
decimalNum : Lexer
decimalNum = digits <+> opt decimalNumRest

-- \.[0-9]+|[0-9]+(\.[0-9]*)?
numeral_helper : Lexer
numeral_helper =  dotNum
              <|> decimalNum

||| A numeral:
||| [-]?(\.[0-9]+|[0-9]+(\.[0-9]*)?)
numeralID : Lexer
numeralID = opt minus <+> numeral_helper

||| Any double-quoted string possibly containing escaped quotes.
stringID : Lexer
stringID = stringLit

--  v  this is probably a library on its own...
||| An HTML string
htmlID : Lexer
htmlID = ?todo_htmlIDs_are_not_implemented_atm

-- Edge operations --

digraphEdgeOp : Lexer
digraphEdgeOp = exact "->"

graphEdgeOp : Lexer
graphEdgeOp = exact "--"

-- Compass Points --

northCPt : Lexer
northCPt =        is 'n'

northEastCPt : Lexer
northEastCPt = exact "ne"

eastCPt : Lexer
eastCPt =         is 'e'

southEastCPt : Lexer
southEastCPt = exact "se"

southCPt : Lexer
southCPt =        is 'e'

southWestCPt : Lexer
southWestCPt = exact "sw"

westCPt : Lexer
westCPt =         is 'w'

northWestCPt : Lexer
northWestCPt = exact "nw"

centerCPt : Lexer
centerCPt =       is 'c'

-- The compass point "_" specifies that an appropriate side of the port adjacent
-- to the exterioior of the node should be used, if such exists. Otherwise, the
-- center is used. If no compass point is used with a portname, the default
-- value is "_".
underCPt : Lexer
underCPt =        is '_'

-- (n | ne | e | se | s | sw | w | nw | c | _)
compassPt : Lexer
compassPt = northCPt
         <|> northEastCPt
         <|> eastCPt
         <|> southEastCPt
         <|> southCPt
         <|> southWestCPt
         <|> westCPt
         <|> northWestCPt
         <|> centerCPt
         <|> underCPt

-- Comments --

-- "a line beginning with a '#' character is considered a line output from a C
-- preprocessor and discarded"
cPreProcessorOutput : Lexer
cPreProcessorOutput = lineComment (is '#')

cppLineComment : Lexer
cppLineComment = lineComment (exact "//")

cppBlockComment : Lexer
cppBlockComment = blockComment (exact "/*") (exact "*/")

||| The language supports C++-style comments `/* */` and `//`. Line starting
||| with a '#' are considered pre-processer output and ignored.
comment : Lexer
comment =  cppLineComment
       <|> cppBlockComment
       <|> cPreProcessorOutput

-- Misc --

-- DOT allows double-quoted strings to span multiple physical lines using the
-- standard C convention of a backslash immediately preceding a newline
-- character
multilineBackslash : Lexer
multilineBackslash = (is '\\') <+> newline

-- double-quoted strings can be concatenated using a '+' operator
strConcat : Lexer
strConcat = is '+'

-- "any amount of whitespace may be inserted [...]"
whitespace : Lexer
whitespace = spaces

lBracket : Lexer
lBracket = is '['

rBracket : Lexer
rBracket = is ']'

lBrace : Lexer
lBrace = is '{'

rBrace : Lexer
rBrace = is '}'

comma : Lexer
comma = is ','

semicolon : Lexer
semicolon = is ';'

colon : Lexer
colon = is ':'

equal : Lexer
equal = is '='

---------------
-- TOKEN MAP --
---------------

||| A mapping from the @Lexer@s to a function of type String -> @DOTToken@
dotTokenMap : TokenMap DOTToken
dotTokenMap = [ (keyword,             \str => Keyword (toLower str))
              , (nameID,              \name => NameID name)
              , (numeralID,           \numeral => NumeralID numeral)
              , (stringID,            \str => StringID str)
--              , (htmlID,              \html => HTML_ID html)
              , (digraphEdgeOp,       const DiGrEdgeOp)
              , (graphEdgeOp,         const GrEdgeOp)
              , (compassPt,           \pt  => CompassPt pt)
              , (comment,             const Comment)
              , (multilineBackslash,  const MultilineBackslash)
              , (strConcat,           const StrConcat)
              , (whitespace,          const Whitespace)
              , (lBracket,            const LBracket)
              , (rBracket,            const RBracket)
              , (lBrace,              const LBrace)
              , (rBrace,              const RBrace)
              , (comma,               const Comma)
              , (semicolon,           const Semicolon)
              , (colon,               const Colon)
              , (equal,               const Equal)
              ]

-- comments and whitespace are irrelevant to the program
relevant : WithBounds DOTToken -> Bool
relevant (MkBounded Comment _ _)    = False
relevant (MkBounded Whitespace _ _) = False
relevant _                          = True

-- removes the irrelevant tokens
clean :  (List (WithBounds DOTToken), (Int, (Int, String)))
      -> (List (WithBounds DOTToken), (Int, (Int, String)))
clean (tokens, inputRemainder) = (filter relevant tokens, inputRemainder)

||| Given a source file, return the token stream
export
lex : String -> (List (WithBounds DOTToken), (Int, (Int, String)))
lex fStr = clean $ lex dotTokenMap fStr


text:
parameters (n:Nat)
  namespace X
    export
    foo : Bool
    foo = True

  U : Bool
  U = foo


text:
printLonger : IO ()
printLonger = do putStr "First string: "
                 first <- getLine
                 putStr "Second string: "
                 second <- getLine
                 let lenFirst = length first
                     lenSecond = length second
                 putStrLn (show (max lenFirst lenSecond))

printLonger2 : IO ()
printLonger2 = putStr "First string: " >>= \_ =>
               getLine >>= \first =>
               putStr "Second string: " >>= \_ =>
               getLine >>= \second =>
               let lenFirst = length first
                   lenSecond = length second in
               putStrLn (show (max lenFirst lenSecond))


text:
module Ch05.Exercise_5_2_8

import Ch05.LambdaCalculus

%default total

-- Lists are represented by their corresponding fold function. That is, a list
-- [x, y, z] is identified with the function
--
--    f |-> ( c |-> f x (f y (f z c))) )
--
-- Where f is any 2-ary function (since the untyped lambda calculus is untyped, of
-- course we can't talk about arities).

||| The term representing the empty list
nil : Term
nil = Abs 0 (Abs 1 (Var 1))--?nil_rhs

||| The term representing the cons combinator
cons : Term
cons = let car = Var 0 -- not to be confused with the car combinator below
           cdr = Var 1 -- --------------------------- cdr ----------------
           f = Var 2
           c = Var 3 in
           Abs 0 (Abs 1 (Abs 2 (Abs 3 (f . car . (cdr . f . c)))))

||| Checks whether a list is nil
isnil : Term
isnil = let l = Var 0
            f = Abs 1 (Abs 2 fls) in
            Abs 0 (l . f . tru)

||| The term representing the "car" combinator
head : Term
head = let l = Var 0 in
           Abs 0 l . fst . nil

||| The term representing the "cdr" combinator
tail : Term
tail = let l = Var 0
           x = Var 1
           y = Var 2
           f = Abs 1 (Abs 2 pair . (snd . y) . (cons . x . (snd . y)))
           c = pair . nil . nil in
           Abs 0 (fst . (l . f . c))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Chapter4

import Data.Vect as V

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double
%name Shape shape, shape1, shape2

-- Both of these are the same
-- This second syntax is more flexible for defining dependent types
-- data Shape : Type where
--      Triangle : Double -> Double -> Shape
--      Rectangle : Double -> Double -> Shape
--      Circle : Double -> Shape

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture
%name Picture pic, pic1, pic2, pic3

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

test_picture : Picture
test_picture = Combine (Translate 5 5 rectangle)
               (Combine (Translate 35 5 circle)
               (Translate 15 25 triangle))

picture_area : Picture -> Double
picture_area (Primitive x) = area x
picture_area (Combine x y) = picture_area x + picture_area y
picture_area (Rotate _ y) = picture_area y
picture_area (Translate _ _ z) = picture_area z

data Biggest = NoTriangle
             | Size Double

biggest : Biggest -> Biggest -> Biggest
biggest NoTriangle y = y
biggest x NoTriangle = x
biggest (Size x) (Size y) = if x > y then Size x else Size y

biggest_triangle : Picture -> Biggest
biggest_triangle (Primitive (Rectangle x y)) = NoTriangle
biggest_triangle (Primitive (Circle x)) = NoTriangle
biggest_triangle (Primitive pic) = Size (area pic)
biggest_triangle (Combine pic pic1) = biggest (biggest_triangle pic) (biggest_triangle pic1)
biggest_triangle (Rotate x pic) = biggest_triangle pic
biggest_triangle (Translate x y pic) = biggest_triangle pic

data Expr = ENum Int
          | EAdd Expr Expr
          | ESub Expr Expr
          | EMul Expr Expr
%name Expr expr, expr1, expr2

evalExpr : Expr -> Int
evalExpr (ENum x)          = x
evalExpr (EAdd expr expr1) = evalExpr expr + evalExpr expr1
evalExpr (ESub expr expr1) = evalExpr expr - evalExpr expr1
evalExpr (EMul expr expr1) = evalExpr expr * evalExpr expr1

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing y = y
maxMaybe x Nothing = x
maxMaybe xval@(Just x) yval@(Just y) = if x > y then xval else yval

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         (Just x) => Just $ V.index x xs

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = case integerToFin pos n of
                                Nothing => Nothing
                                (Just x) => Just $ (V.index x xs) + (V.index x ys)

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs sum istr = let i = cast istr in
                         if i < 0 then Nothing
                         else let newSum = sum + i in
                                  Just ("Subtotal: " ++ show newSum ++ "\n", newSum)

main : IO ()
main = replWith 0 "Enter a value: " sumInputs

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Data.InSet.List

import Data.Bool
import Data.InSet
import Data.List

import Syntax.WithProof

%default total

public export
elems : Equality a => List a -> InSet a
elems []      = []
elems (x::xs) = x :: elems xs

export
elems_of_concat : Equality a => (xs, ys : List a) -> elems (xs ++ ys) == elems xs + elems ys
elems_of_concat [] _ _ = Refl
elems_of_concat (x::xs) ys n = case @@(n =?= x) of
  (True  ** prf) => rewrite prf in Refl
  (False ** prf) => rewrite prf in elems_of_concat xs ys n

-- This is better to be placed in `Data.List`.
reverseOfConc : (x : a) -> (xs : List a) -> reverse (x::xs) = reverse xs ++ [x]
reverseOfConc x []      = Refl
reverseOfConc x (y::ys) = rewrite reverseOfConc y ys in
                          rewrite sym $ appendAssociative (reverse ys) [y] [x] in
                          rewrite revAppend [x, y] ys in
                          Refl

export
reverse_preserves_elems : Equality a => (xs : List a) -> elems (reverse xs) == elems xs
reverse_preserves_elems []      n = Refl
reverse_preserves_elems (x::xs) n = rewrite reverseOfConc x xs in
                                    rewrite elems_of_concat (reverse xs) [x] n in
                                    case @@(n =?= x) of
                                      (True ** prf) => rewrite x_in_same_etc n x [] prf in
                                                       rewrite prf in
                                                       rewrite orTrueTrue $ n `isin` elems (reverse xs) in
                                                       Refl
                                      (False ** prf) => rewrite prf in
                                                        rewrite reverse_preserves_elems xs n in
                                                        rewrite orFalseNeutral $ n `isin` elems xs in
                                                        Refl

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
module TypeFuns

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety Four"
getStringOrInt True = 94

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False x = trim x
valToString True x = cast x


text:
module Main

import System

%default total
%access public export

Foldable (Either a) where
  foldr _ z (Left _) = z
  foldr f z (Right y) = f y z

Traversable (Either a) where
  traverse _ (Left x) = pure (Left x)
  traverse f (Right y) = Right <$> f y

mapi : (Nat -> a -> b) -> List a -> List b
mapi = mapi' Z where
  mapi' : Nat -> (Nat -> a -> b) -> List a -> List b
  mapi' _ _ [] = []
  mapi' k f (x :: xs) = f k x :: mapi' (S k) f xs

lineTooLong : Nat -> Nat -> String -> Maybe (Nat, Nat)
lineTooLong limit lineN s =
  let len = length s
  in if len > limit
  then Just (lineN, len)
  else Nothing

linesInViolation : Nat -> List String -> List (Nat, Nat)
linesInViolation limit = catMaybes . mapi (lineTooLong limit)

formatViolation : Nat -> String -> (Nat, Nat) -> String
formatViolation limit filepath (lineN, len) =
  filepath ++ ":" ++ cast lineN ++ ": " ++ cast len ++ " > " ++ cast limit

printViolations : Nat -> String -> List (Nat, Nat) -> IO Nat
printViolations limit filepath =
  map length . traverse (fPutStrLn stderr . formatViolation limit filepath)

processFile' : Nat -> String -> String -> IO Nat
processFile' limit filepath =
  printViolations limit filepath . linesInViolation limit . lines

-- Idris does not have bifunctor in its prelude
mapLeft : (a -> c) -> Either a b -> Either c b
mapLeft f (Left l) = Left (f l)
mapLeft _ (Right r) = Right r

processFile : Nat -> String -> IO (Either (String, FileError) Nat)
processFile limit filepath = do
  result <- readFile filepath
  traverse (processFile' limit filepath) $ mapLeft (MkPair filepath) result

formatTotalMsg : Nat -> Nat -> String
formatTotalMsg limit Z = "All lines <" ++ cast limit ++ "."
formatTotalMsg limit (S k) = cast (S k) ++ " total lines >" ++ cast limit ++ "."

handleResult : Nat -> Either (String, FileError) (List Nat) -> IO Int
handleResult _ (Left (filepath, err)) = do
  fPutStrLn stderr ("Failed to read " ++ filepath ++ ": " ++ show err)
  pure 2
handleResult limit (Right violations) = do
  let n = sum violations
  putStrLn $ formatTotalMsg limit n
  pure (if n == 0 then 0 else 1)

main_ : Nat -> List String -> IO Int
main_ limit args = do
  result <- traverse (processFile limit) args
  handleResult limit $ traverse id result

partial
main : IO ()
main = exit !(main_ 80 !getArgs)


text:
module Data.Vect.Structural

-- For structural lemmas about (Vect) modules
import Control.Algebra
import Control.Algebra.VectorSpace -- definition of module
import Classes.Verified -- definition of verified algebras other than modules
import Control.Algebra.DiamondInstances
import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20

%default total

{-
Theorem (vecHeadtailsEq) for proving equality of (Vect)s by proving equality of their heads and tails. Often used after (headtails).

Theorem (vecIndexwiseEq) for proving equality of (Vect)s by proving indexwise equality of their entries.
-}

vecHeadtailsEq : {xs,ys : Vect _ _} -> ( headeq : x = y ) -> ( taileq : xs = ys ) -> x::xs = y::ys
vecHeadtailsEq {x} {xs} {ys} headeq taileq = trans (vectConsCong x xs ys taileq) $ cong {f=(::ys)} headeq
-- Also a solid proof:
-- vecHeadtailsEq {x} {xs} {ys} headeq taileq = trans (cong {f=(::xs)} headeq) $ replace {P=\l => l::xs = l::ys} headeq $ vectConsCong x xs ys taileq

vecIndexwiseEq : ((i : Fin _) -> index i xs = index i ys) -> xs = ys
vecIndexwiseEq fn {xs=[]} {ys=[]} = Refl
vecIndexwiseEq fn {xs=x::xs} {ys=y::ys} = vecHeadtailsEq (fn FZ) $ vecIndexwiseEq {xs=xs} {ys=ys} (\i => fn $ FS i)

{-
* Theorems characterizing (Vect)s of degenerate qualities.
* Theorems characterizing the index or head of a list created with a certain operation.
* The theorem (weakenedInd) about comparing an index of a list to an index of its (init).
* The theorem (extensionalEqToMapEq) extending an extensional equality between functions to one between their (map)s over (Vect)s.
-}

total
zeroVecEq : {a : Vect 0 r} -> {b : Vect 0 r} -> a = b
zeroVecEq {a=[]} {b=[]} = Refl

total
vecSingletonReplicateEq : ((u : a) -> v=u) -> (xs : Vect n a) -> (xs = replicate n v)
vecSingletonReplicateEq f [] = Refl
vecSingletonReplicateEq f (x::xs) {v} = rewrite sym (f x) in cong {f=(v::)} (vecSingletonReplicateEq f xs)

total
zeroVecVecId : (xs : Vect n (Vect 0 a)) -> (xs = replicate n [])
zeroVecVecId = vecSingletonReplicateEq (\b => zeroVecEq {a=[]} {b=b})

total
headMapChariz : {xs : Vect (S n) _} -> head $ map f xs = f $ head xs
headMapChariz {xs=x::xs} = Refl

mapheadrec : with Data.Vect ( map head (v::vs) = (head v) :: (map head vs) )
mapheadrec = Refl

headtails : (v : Vect (S predk) _) -> v = (head v) :: (tail v)
headtails (vv::vvs) = Refl

-- The theorem below this one should not be a necessary weakening, since the functions have equivalent definitions.
-- indexFZIshead : index FZ = Data.Vect.head

total
indexFZIsheadValued : index FZ xs = head xs
indexFZIsheadValued {xs=x :: xs} = Refl

indexReplicateChariz : Data.Vect.index k $ replicate n a = a
indexReplicateChariz {n=Z} {k} = FinZElim k
indexReplicateChariz {n=S predn} {k=FZ} = Refl
indexReplicateChariz {n=S predn} {k=FS prelk} = indexReplicateChariz {k=prelk}

uniformValImpliesReplicate : (a : ty) -> (x : Vect n ty) -> ((i : _) -> index i x = a) -> x = replicate n a
uniformValImpliesReplicate a [] fn = Refl
uniformValImpliesReplicate a (x::xs) fn = vecHeadtailsEq (fn FZ) $ uniformValImpliesReplicate a xs (\i => fn $ FS i)

indexMapChariz : Data.Vect.index k $ map f xs = f $ index k xs
indexMapChariz {xs=[]} {k} = FinZElim k
-- indexMapChariz {xs} {f} {k=FZ} = trans indexFZIsheadValued $ trans headMapChariz $ sym $ cong indexFZIsheadValued
indexMapChariz {xs=x::xs} {f} {k=FZ} = Refl
indexMapChariz {xs=x::xs} {f} {k=FS k} = indexMapChariz {xs=xs} {f=f} {k=k}

indexUpdateAtChariz : index i $ updateAt i f xs = f $ index i xs
indexUpdateAtChariz {xs=[]} {i} = FinZElim i
indexUpdateAtChariz {xs=(x::xs)} {f} {i=FZ} = Refl
indexUpdateAtChariz {xs=x::xs} {f} {i=FS i} = indexUpdateAtChariz {xs=xs} {f=f} {i=i}

indexUpdateAtChariz2 : Not (i = j) -> index i $ updateAt j f xs = index i xs
indexUpdateAtChariz2 prneq {i=FZ} {j=FZ} = void $ prneq Refl
indexUpdateAtChariz2 prneq {i=FS k} {j=FZ} {xs=x::xs} = Refl
indexUpdateAtChariz2 prneq {i=FZ} {j=FS k} {xs=x::xs} = Refl
indexUpdateAtChariz2 prneq {i=FS ki} {j=FS kj} {xs=x::xs} = indexUpdateAtChariz2 {xs=xs}
	$ prneq . (cong {f=FS})

updateDeleteAtChariz : deleteAt i $ updateAt i f xs = deleteAt i xs
updateDeleteAtChariz {i=FZ} {xs=x::xs} = Refl
updateDeleteAtChariz {i=FS k} {xs=x::[]} = FinZElim k
updateDeleteAtChariz {i=FS k} {xs=x::x2::xs} = cong {f=(x::)}
	$ updateDeleteAtChariz {i=k} {xs=x2::xs}

updateAtIndIsMapAtInd : index i $ updateAt i f xs = index i $ map f xs
updateAtIndIsMapAtInd = trans indexUpdateAtChariz $ sym indexMapChariz

deleteSuccRowVanishesUnderHead : head $ deleteRow (FS k) xs = head xs
deleteSuccRowVanishesUnderHead {xs=x::xs} = Refl

updateAtSuccRowVanishesUnderHead : head $ updateAt (FS k) f xs = head xs
updateAtSuccRowVanishesUnderHead {xs=x::xs} = Refl

zipWithEntryChariz : index i $ Vect.zipWith m x y = m (index i x) (index i y)
zipWithEntryChariz {x=[]} {y=[]} {i} = FinZElim i
zipWithEntryChariz {x=(x::xs)} {y=(y::ys)} {i=FZ} = Refl
zipWithEntryChariz {x=(x::xs)} {y=(y::ys)} {i=FS preli} = zipWithEntryChariz {x=xs} {y=ys} {i=preli}

plusOneVectIsSuccVect : Vect (n+1) a = Vect (S n) a
plusOneVectIsSuccVect {a} {n} = sym $ cong {f=\k => Vect k a} $ trans (cong {f=S} $ sym $ plusZeroRightNeutral n) $ plusSuccRightSucc n Z

{-
appendedSingletonAsSuccVect : (xs : Vect n a) -> (v : a) -> Vect (S n) a
appendedSingletonAsSuccVect {a} {n} xs v = rewrite sym $ plusOneVectIsSuccVect {a=a} {n=n} in (xs++[v])
-}
appendedSingletonAsSuccVect : (xs : Vect n a) -> (v : a) -> Vect (S n) a
appendedSingletonAsSuccVect [] v = [v]
appendedSingletonAsSuccVect (x::xs) v = x::appendedSingletonAsSuccVect xs v

-- With the old implementation of (appendedSingletonAsSuccVect) this seemed impossible to prove.
consAppendedSingleton : {xs : Vect n a} -> appendedSingletonAsSuccVect (x::xs) v = x::appendedSingletonAsSuccVect xs v
consAppendedSingleton {x} {xs} {v} {a} {n} = Refl

{-
-- Too many problems with this, rewriting the types to handle Nat addition.
lastInd : {xs : Vect n a} -> Data.Vect.index Data.Fin.last (rewrite sym $ plusOneVectIsSuccVect {a=a} {n=n} in (xs++[v])) = v
-}

{-
-- Stopped typechecking once the implementation of (appendedSingletonAsSuccVect) changed.
lastInd : {xs : Vect n a} -> index Data.Fin.last $ appendedSingletonAsSuccVect xs v = v
lastInd {xs=[]} = Refl
lastInd {xs=x::xs} {v} = rewrite consAppendedSingleton {x=x} {xs=xs} {v=v} in (lastInd {xs=xs} {v=v})

-----

"ERROR ON INTROS" BUG, CASE, SOLUTION

---

> lastInd {xs=x::xs} = ?lastInd_rhs_2

> :prove lastInd_rhs_2
lastInd_rhs_2> intro

Type mismatch between
        Vect k a = Vect k a
and
        Vect (S (S k)) a = Vect (S (plus k 1)) a

which I think means the type signature for (lastInd) is being reanalyzed in the presence of (x::xs), as if inlined, in such a way that the sucessor to rewrite is the one inside rather than outside, or something.

This works fine:

> lastInd {xs=x::xs} {v} = the ( (index Data.Fin.last $ appendedSingletonAsSuccVect (x::xs) v) = v ) ?lastInd_rhs_2

and spells out

> lastInd {xs=x::xs} {v} = the ( (index Data.Fin.last $ appendedSingletonAsSuccVect (x::xs) v) = v ) ( rewrite consAppendedSingleton {x=x} {xs=xs} {v=v} in lastInd {xs=xs} {v=v} )

-}

-- Could this be done with the reversal isomorphism of each Fin?
lastInd : {xs : Vect n a} -> index Data.Fin.last $ appendedSingletonAsSuccVect xs v = v
lastInd {xs=[]} = Refl
lastInd {xs=x::xs} {v} = lastInd {xs=xs} {v=v}

{-
-- Stopped typechecking once the implementation of (appendedSingletonAsSuccVect) changed.
total
weakenedInd : {xs : Vect n a} -> index (weaken k) $ appendedSingletonAsSuccVect xs v = index k xs
weakenedInd {xs=[]} {k} = absurd k
weakenedInd {xs=x::xs} {k=FZ} {v} = rewrite consAppendedSingleton {x=x} {xs=xs} {v=v} in Refl
weakenedInd {xs=x::xs} {k=FS j} {v} = rewrite consAppendedSingleton {x=x} {xs=xs} {v=v} in weakenedInd {xs=xs} {k=j} {v}
-}

{-
Could this be done with the reversal isomorphism of each Fin and a proof that weaken becomes FS under it?
-}
total
weakenedInd : {xs : Vect n a} -> index (weaken k) $ appendedSingletonAsSuccVect xs v = index k xs
weakenedInd {xs=[]} {k} = absurd k
weakenedInd {xs=x::xs} {k=FZ} {v} = Refl
weakenedInd {xs=x::xs} {k=FS j} {v} = weakenedInd {xs=xs} {k=j} {v}

extensionalEqToMapEq : (exteq : (a : ty) -> (f a = g a)) -> (xs : Vect n ty) -> (map f xs = map g xs)
extensionalEqToMapEq exteq [] = Refl
extensionalEqToMapEq exteq (x::xs) = vecHeadtailsEq (exteq x) $ extensionalEqToMapEq exteq xs

-- Functorial nature of (map).
composeUnderMap : (v : Vect n a)
	-> (g : b -> c)
	-> (f : a -> b)
	-> map g $ map f v = map (g . f) v
composeUnderMap [] g f = Refl
composeUnderMap (v::vs) g f = vecHeadtailsEq Refl $ composeUnderMap vs g f

{-
Theorems about the module (Vect n a) over a ring (a):
* Compatibility between the operations of the ring (a) and of (Vect n a) as a module under (index).
-}

indexNeutralIsNeutral1D : Ring a => (k : Fin n) -> index k $ Algebra.neutral {a=Vect n a} = Algebra.neutral
indexNeutralIsNeutral1D FZ = Refl
indexNeutralIsNeutral1D (FS k) = indexNeutralIsNeutral1D k

-- For completeness's sake, these should have (index FZ) as (head) forms proved.

indexCompatInverse : VerifiedRingWithUnity a => (xs : Vect n a) -> (i : Fin n) -> index i $ inverse xs = inverse $ index i xs
indexCompatInverse [] i = FinZElim i
indexCompatInverse (x::xs) FZ = Refl
indexCompatInverse (x::xs) (FS preli) = indexCompatInverse xs preli

indexCompatAdd : VerifiedRingWithUnity a => (xs, ys : Vect n a) -> (i : Fin n) -> index i $ xs <+> ys = index i xs <+> index i ys
indexCompatAdd xs ys i = zipWithEntryChariz {x=xs} {y=ys} {i=i} {m=(<+>)}

indexCompatSub : VerifiedRingWithUnity a
	=> {auto ok :
		((<+>) @{vrwuSemigroupByGrp $ the (VerifiedRingWithUnity a) %instance})
		= ((<+>) @{vrwuSemigroupByVMon $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (xs, ys : Vect n a)
	-> (i : Fin n)
	-> index i $ xs <-> ys = index i xs <-> index i ys
indexCompatSub {ok} xs ys i = rewrite ok in
	trans (indexCompatAdd xs (inverse ys) i)
	$ cong {f=((index i xs)<+>)}
	$ indexCompatInverse ys i

indexCompatScaling : VerifiedRingWithUnity a
	=> {auto ok :
		((<.>) @{vrwuRingByRWU $ the (VerifiedRingWithUnity a) %instance})
		= ((<.>) @{vrwuRingByVR $ the (VerifiedRingWithUnity a) %instance})
		}
	-> (r : a) -> (xs : Vect n a) -> (i : Fin n)
	-> index i $ r <#> xs = r <.> index i xs
indexCompatScaling r [] i = FinZElim i
indexCompatScaling r (x::xs) FZ {ok} = cong {f=\t => t r x} ok
indexCompatScaling r (x::xs) (FS preli) = indexCompatScaling r xs preli

{-
* The recursive equation for (foldr) over (Vect)s.
* The recursive equation for sums in (Monoid)s over a (Vect _).
-}

foldrImplRec : (f : t -> acc -> acc) -> (e : acc) -> (go : acc -> acc) -> (x : t) -> (xs : Vect n t) -> (foldrImpl f e go (x::xs) = go $ f x $ foldrImpl f e Basics.id xs)
foldrImplRec f e go x [] = Refl
foldrImplRec f e go x (xx::xxs) = trans (foldrImplRec f e (go . (f x)) xx xxs) $ cong {f=go . (f x)} $ sym $ foldrImplRec f e id xx xxs

monoidrec : Monoid a => (v : a) -> (vs : Vect n a) -> sum' (v::vs) = v <+> sum' vs
monoidrec = foldrImplRec (<+>) Algebra.neutral id


text:
module MinesweeperSMT

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

puzzle : Vect 3 (Vect 3 Int)
puzzle = [ [1, 2, 3],
           [4, 5, 6],
           [7, 8, 9] ]

shiftLeft : a -> Vect n a -> Vect n a
shiftLeft e [] = []
shiftLeft {n = S n} e (x :: xs) = replace {P = (\x => Vect x a)} (plusCommutative n 1) (xs ++ [e])

shiftRight : a -> Vect n a -> Vect n a
shiftRight e xs = reverse $ shiftLeft e $ reverse xs

index : Fin n -> Fin m -> Vect n (Vect m a) -> a
index n m xss = index m (index n xss)

collect : Fin n -> Fin m -> Vect n (Vect m Int) -> Expr BoolT
collect n m xss = let r = (index n m (map (shiftLeft 0) xss)) in
                  let l = (index n m (map (shiftRight 0) xss)) in
                  (int l) == (int r)

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
module Error.Format

import Syntax.Lexer
import Data.String.Extra
import Data.String
import Data.List
import Data.List1
import Error.ANSI
import Error.Data

public export
insertInList : Nat -> a -> List a -> List a
insertInList index line lines =
  take index lines ++ [line] ++ (drop index lines)

public export
insertInLines : (Int, Int) -> Int -> String -> List String -> List String
insertInLines (start, end) mainLine text =
  insertInList (cast (mainLine - (cast start))) text

public export
getRange : ErrorType -> Maybe Range
getRange (LexicalError  r _) = Just r
getRange (ReadingError  r _) = Just r
getRange (ParsingError  r _) = Just r
getRange _                   = Nothing

space : Nat -> String
space n = replicate n ' '

public export
lineJump : Nat -> String
lineJump n = replicate n '\n'

breakText : (Int, Int) -> String -> (String, String, String)
breakText (startColumn, endColumn) text =
    let start  = strSubstr 0 (cast startColumn) text
        middle = strSubstr (cast startColumn) (cast $ endColumn - startColumn) text
        end    = strSubstr (cast endColumn)   (cast $ (cast $ length text) - endColumn) text in
        (start, middle, end)

public export
getIndex : Nat -> List a -> a -> a
getIndex idx ls alt =
  case (drop idx ls) of
    h::tl => h
    _ => alt

-- Simple Syntax Highlight based on the lexer

keywords : List String
keywords = ["data", "defn", "doc", "case", "if", "else"]

specialWords : List String
specialWords = ["->", "IO", "List"]

-- TODO: Move to another folder
getTknColor : Tkn -> String
getTknColor (TknNum     _) = "\x1b[32m"
getTknColor (TknStr     _) = "\x1b[33m"
getTknColor (TknComment _) = "\x1b[90m"
getTknColor (TknId n) =
  case find (== n) keywords of
    Just _ => "\x1b[31m"
    _ => case find (== n) specialWords of
      Just _ => "\x1b[35m"
      _ => ""

getTknColor TknRSquare = "\x1b[34m"
getTknColor TknLSquare = "\x1b[34m"
getTknColor _ = ""

syntaxHighlight : String -> String -> String
syntaxHighlight style text =
  case lex text of
    Right tokens =>
      snd $ foldl
              (\cur => syntaxHighlightSingle (fst cur) (snd cur))
              (0, text)
              tokens
    Left _ => text
  where
    syntaxHighlightSingle : Int -> String -> (Range, Tkn) -> (Int, String)
    syntaxHighlightSingle accPos text (MkRange start end, tkn) =
      let lineEnd = if (Loc.line start) /= (Loc.line end) then length text else (cast $ Loc.line end)
          pos = ((Loc.column start) + accPos, (Loc.column end) + accPos)
          (start, middle, end) = breakText pos text
          color = getTknColor tkn
          newPos = (length color) + (length style) + 4 in
      ((cast newPos) + accPos, concat [start, color, style, middle, Deco.reset, end, Deco.reset])

-- Formats the code

public export
getErrorLineRange : (List String) -> Range -> (Int, Int)
getErrorLineRange lines (MkRange (MkLoc _ startLine) (MkLoc _ endLine)) =
  (if startLine - 2 < 0                    then 0           else startLine - 2,
   if endLine + 3 < (cast $ length lines)  then endLine + 3 else (cast $ length lines))

formatLineNumber : String -> Int -> String
formatLineNumber text num =
  concat [ justifyRight 6 ' ' (cast $ num + 1)
         , " | "]

formatCommonCodeLine : String -> String -> Int -> String
formatCommonCodeLine style text lineNum =
  concat [ style
         , formatLineNumber text lineNum
         , syntaxHighlight style text
         , Deco.reset]

public export
createMarkLine : String -> Int -> Range -> String
createMarkLine style textEnd (MkRange startLoc endLoc) =
  let start = Loc.column startLoc
      end = if (Loc.line startLoc) == (Loc.line endLoc)
              then Loc.column endLoc
              else textEnd
  in
  concat [ Deco.bold, style, space (cast start + 9), replicate (cast $ end - start) '^', Deco.reset ]

public export
formatHighlightedCodeLine : Range -> String -> String -> Int -> String
formatHighlightedCodeLine (MkRange start end) style text lineNum =
  let (start, middle, end) = breakText ((Loc.column start), (Loc.column end)) text in
  concat [ formatLineNumber text lineNum
         , syntaxHighlight "" start
         , Deco.bold
         , style
         , middle
         , Deco.reset
         , syntaxHighlight "" end
         , Deco.reset ]

public export
formatLines : Range -> (Int,Int) -> Int -> (List String) -> List String
formatLines range (start, end) mainLine =
      map  formatLine
    . zip  [start..end]
    . take (cast (end - start))
    . drop (cast start)
  where
    formatLine : (Int, String) -> String
    formatLine (line, text) =
      if mainLine /= line
        then formatCommonCodeLine Deco.dim text line
        else formatHighlightedCodeLine range Fg.red text line

-- Formats the header messages

public export
formatHeader : String -> String
formatHeader header =
    case lines header of
        (title :: tl) => concat ["\n", errorTag, " ", title, "\n", unlines $ map ((space 10) ++) tl, if (length tl > 0) then "\n" else ""]
        _ => concat ["\n", errorTag, "Empty error"]
    where
      errorTag : String
      errorTag = concat [space 2, Bg.red, " ERROR ", Deco.reset]

public export
fileHeader : Range -> String -> String
fileHeader (MkRange (MkLoc col line) (MkLoc colEnd lineEnd)) file =
  let text =
    concat ["on ./"
           , file, ":"
           , (cast (line+1))
           , ":"
           , (cast (col + 1))
           , "~"
           , (cast (lineEnd+1))
           , ":"
           , (cast (colEnd + 1))] in
  concat [ space 4
         , Deco.dim
         , Fg.cyan
         , text
         , Deco.reset
         , "\n"]

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Control.Monad.Either

-------------------------------------------------
-- The monad transformer `EitherT e m a` equips a monad with the ability to
-- return a choice of two values.

-- Sequenced actions of `Either e m a` produce a value `a` only if none of the
-- actions in the sequence returned `e`. Because returning `e` exits the
-- computation early, this can be seen as equipping a monad with the ability to
-- throw an exception.

-- This is more powerful than MaybeT which instead equips a monad with the
-- ability to not return a result.
-------------------------------------------------

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

public export
data EitherT : (e : Type) -> (m : Type -> Type) -> (a : Type) -> Type where
  MkEitherT : (1 _ : m (Either e a)) -> EitherT e m a

export
%inline
runEitherT : EitherT e m a -> m (Either e a)
runEitherT (MkEitherT x) = x

export
eitherT : Monad m => (a -> m c) -> (b -> m c) -> EitherT a m b -> m c
eitherT f g x = runEitherT x >>= either f g

||| map the underlying computation
||| The basic 'unwrap, apply, rewrap' of this transformer.
export
%inline
mapEitherT : (m (Either e a) -> n (Either e' a')) -> EitherT e m a -> EitherT e' n a'
mapEitherT f = MkEitherT . f . runEitherT

export
bimapEitherT : Functor m => (a -> c) -> (b -> d)
            -> EitherT a m b -> EitherT c m d
bimapEitherT f g x = mapEitherT (map (either (Left . f) (Right . g))) x

||| Analogous to Left, aka throwE
export
%inline
left : Applicative m => e -> EitherT e m a
left = MkEitherT . pure . Left

||| Analogous to Right, aka pure for EitherT
export
%inline
right : Applicative m => a -> EitherT e m a
right = MkEitherT . pure . Right

export
swapEitherT : Functor m => EitherT e m a -> EitherT a m e
swapEitherT = mapEitherT (map (either Right Left))

-------------------------------------------------
-- Methods of the 'exception' theme
-------------------------------------------------

||| aka `left`
export
%inline
throwE : Applicative m => e -> EitherT e m a
throwE = MkEitherT . pure . Left

export
catchE : Monad m => EitherT e m a -> (e -> EitherT e' m a) -> EitherT e' m a
catchE et f
  = MkEitherT $ runEitherT et >>= either (runEitherT . f) (pure . Right)

-------------------------------------------------
-- Interface Implementations
-------------------------------------------------

on : (b -> b -> c) -> (a -> b) -> a -> a -> c
on f g x y = g x `f` g y

public export
Eq (m (Either e a)) => Eq (EitherT e m a) where
 (==) = (==) `on` runEitherT

public export
Ord (m (Either e a)) => Ord (EitherT e m a) where
 compare = compare `on` runEitherT

public export
Show (m (Either e a)) => Show (EitherT e m a) where
  showPrec d (MkEitherT x) = showCon d "MkEitherT" $ showArg x

-- I'm not actually confident about having this instance but it is a sane
-- default and since idris has named implementations it can be swapped out at
-- the use site.
public export
Monad m => Semigroup (EitherT e m a) where
  MkEitherT x <+> MkEitherT y = MkEitherT $ do
    r@(Right _) <- x
      | Left _ => y
    pure r

public export
Functor m => Functor (EitherT e m) where
  map f e = MkEitherT $ map f <$> runEitherT e

public export
Foldable m => Foldable (EitherT e m) where
  foldr f acc (MkEitherT e)
    = foldr (\x,xs => either (const acc) (`f` xs) x) acc e

public export
Traversable m => Traversable (EitherT e m) where
  traverse f (MkEitherT x)
    = MkEitherT <$> traverse (either (pure . Left) (map Right . f)) x

public export
Applicative m => Applicative (EitherT e m) where
  pure = MkEitherT . pure . Right
  f <*> x = MkEitherT [| runEitherT f <*> runEitherT x |]

public export
Monad m => Monad (EitherT e m) where
  x >>= k = MkEitherT $ runEitherT x >>= either (pure . Left) (runEitherT . k)

||| Alternative instance that collects left results, allowing you to try
||| multiple possibilities and combine failures.
public export
(Monad m, Monoid e) => Alternative (EitherT e m) where
  empty = left neutral
  MkEitherT x <|> MkEitherT y = MkEitherT $ do
    Left l <- x
      | Right r => pure (Right r)
    Left l' <- y
      | Right r => pure (Right r)
    pure (Left (l <+> l'))

public export
MonadTrans (EitherT e) where
  lift = MkEitherT . map Right

public export
HasIO m => HasIO (EitherT e m) where
  liftIO act = MkEitherT $ liftIO (io_bind act (pure . Right))

public export
MonadReader r m => MonadReader r (EitherT e m) where
  ask = lift ask
  local f (MkEitherT x) = MkEitherT (local f x)

public export
MonadState s m => MonadState s (EitherT e m) where
  get = lift get
  put = lift . put


text:
module TyTTP.Adapter.Node.HTTP

import Data.Buffer
import Data.Buffer.Ext
import public Node.Error
import Node.HTTP.Server
import TyTTP
import public TyTTP.Adapter.Node.Error
import TyTTP.HTTP as HTTP

public export
RawHttpRequest : Type
RawHttpRequest = HttpRequest String StringHeaders $ Publisher IO NodeError Buffer

public export
RawHttpResponse : Type
RawHttpResponse = Response Status StringHeaders $ Publisher IO NodeError Buffer

toNodeResponse : RawHttpResponse -> Node.HTTP.Server.ServerResponse -> IO ()
toNodeResponse res nodeRes = do
  let status = res.status.code
  headers <- mapHeaders res.headers

  nodeRes.writeHead status headers
  res.body.subscribe $ MkSubscriber
        { onNext = \a => nodeRes.write a }
        { onFailed = \e => pure () }
        { onSucceded = \_ => nodeRes.end }
  where
    mapHeaders : StringHeaders -> IO Node.HTTP.Headers.Headers
    mapHeaders h = do
      newHeaders <- empty
      foldlM (\hs, (k,v) => hs.setHeader k v) newHeaders h

fromPromiseToNodeResponse : Error e
  => (e -> RawHttpResponse)
  -> Promise e IO (Context Method String StringHeaders Status StringHeaders b $ Publisher IO NodeError Buffer)
  -> ServerResponse
  -> IO ()
fromPromiseToNodeResponse errorHandler (MkPromise cont) nodeRes =
  let callbacks = MkCallbacks
        { onSucceded = \a => toNodeResponse a.response nodeRes }
        { onFailed = \e => toNodeResponse (errorHandler e) nodeRes }
  in
    cont callbacks

fromNodeRequest : Node.HTTP.Server.IncomingMessage -> RawHttpRequest
fromNodeRequest nodeReq =
  let method = parseMethod nodeReq.method
      path = nodeReq.url
      headers = nodeReq.headers.asList
  in HTTP.mkRequest method path headers $ MkPublisher $ \s => do
        nodeReq.onData s.onNext
        nodeReq.onError s.onFailed
        nodeReq.onEnd s.onSucceded

public export
record ListenOptions e where
  constructor MkListenOptions
  port : Int
  errorHandler : (e -> RawHttpResponse)

export
defaultListenOptions : Error e => ListenOptions e
defaultListenOptions = MkListenOptions
  { port = 3000
  , errorHandler = \e => MkResponse
    { status = INTERNAL_SERVER_ERROR
    , headers =
      [ ("Content-Type", "text/plain")
      , ("Content-Length", show $ length $ message e)
      ]
    , body = singleton $ fromString $ message e
    }
  }

export
listen : HasIO io
   => Error e
   => HTTP
   -> ListenOptions e
   -> (
    Context Method String StringHeaders Status StringHeaders (Publisher IO NodeError Buffer) ()
     -> Promise e IO $ Context Method String StringHeaders Status StringHeaders b (Publisher IO NodeError Buffer)
  )
   -> io Server
listen http options handler = do
  server <- http.createServer

  server.onRequest $ \req => \res => do
    let handlerReq = fromNodeRequest req
        initialRes = MkResponse OK [] () {h = StringHeaders}
        result = handler $ MkContext handlerReq initialRes

    fromPromiseToNodeResponse options.errorHandler result res

  server.listen options.port
  pure server

export
listen' : HasIO io
   => Error e
   => { auto http : HTTP }
   -> { default defaultListenOptions options : ListenOptions e }
   -> (
    Context Method String StringHeaders Status StringHeaders (Publisher IO NodeError Buffer) ()
     -> Promise e IO $ Context Method String StringHeaders Status StringHeaders b (Publisher IO NodeError Buffer)
  )
   -> io Server
listen' {http} {options} handler = listen http options handler

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
||| TODO docs
module RegExp.String

import Decidable.Equality
import RegExp as RE
import public RegExp.Types as RET

infixr 2 .|.
infixr 3 .&.
infixr 5 .+.
infixr 6 ...

-----------
-- TYPES --
-----------

||| A regular expression specification.
public export
RegExp : Type
RegExp = RET.RegExp Char

||| The property of a regular expression matching an input string.
public export
Matches : RegExp -> String -> Type
Matches r s = RET.Matches r (unpack s)

---------------
-- OPERATORS --
---------------

||| Builds a `RegExp` matching a single character.
export
lit : Char -> RegExp
lit = Lit

||| Builds a `RegExp` as the concatenation of two other `RegExp`.
export
(.+.) : RegExp -> RegExp -> RegExp
(.+.) = Cat

||| Builds a `RegExp` as the disjunction of two other `RegExp`.
export
(.|.) : RegExp -> RegExp -> RegExp
(.|.) = Disj

||| Builds a `RegExp` as the conjunction of two other `RegExp`.
export
(.&.) : RegExp -> RegExp -> RegExp
(.&.) = Conj

||| Builds a `RegExp` which optionally matches another `RegExp`.
export
one : RegExp -> RegExp
one r = Star r .|. Empty

||| Builds a `RegExp` which matches zero or more of another `RegExp`.
export
star : RegExp -> RegExp
star = Star

||| Builds a `RegExp` which matches one or more of another `RegExp`.
export
plus : RegExp -> RegExp
plus r = Cat r $ Star r

||| Builds a `RegExp` which matches a range of characters.
export
(...) : Char -> Char -> RegExp
(...) x y = let x' = min x y
                y' = max x y in
                to (ord x') ((ord y') - 1) (Lit y') where
  to : Int -> Int -> RegExp -> RegExp
  to min n r = if n < min
               then r
               else to min (n - 1) (Disj (Lit (chr n)) r)

||| Builds a `RegExp` which matches any one of the provided characters.
export
any : (Foldable a, Functor a) => (xs : a Char) -> RegExp
any = foldr (.|.) Null . map Lit

----------------
-- SHORTHANDS --
----------------

||| Matches a lowercase ASCII character.
export
lowercase : RegExp
lowercase = 'a'...'z'

||| Matches an uppercase ASCII character.
export
uppercase : RegExp
uppercase = 'A'...'Z'

||| Matches an alphabetical ASCII character.
export
alpha : RegExp
alpha = lowercase .|. uppercase

||| Matches a numeric digit ASCII character.
export
digit : RegExp
digit = '0'...'9'

||| Matches an alphanumeric ASCII character.
export
alphaNumeric : RegExp
alphaNumeric = alpha .|. digit

||| Matches an alphanumeric or underscore ASCII character.
export
word : RegExp
word = alphaNumeric .|. lit '_'

||| Matches a whitespace ASCII character.
export
whitespace : RegExp
whitespace = any [' ', '\t', '\r', '\n', '\v', '\f']

--------------
-- MATCHING --
--------------

||| Decides whether the provided string matches a regular expression.
export
matches : (r : RegExp) -> (s : String) -> Dec (Matches r s)
matches r s = RE.matches r (unpack s)

-----------
-- TESTS --
-----------

test_range_single : 'x'...'x' = Lit 'x'
test_range_single = Refl

test_to_asc : 'a'...'c' = (Disj (Lit 'a') (Disj (Lit 'b') (Lit 'c')))
test_to_asc = Refl

test_to_desc : '3'...'1' = (Disj (Lit '1') (Disj (Lit '2') (Lit '3')))
test_to_desc = Refl

max_stars_repo_name: polendri/idris-regex

max_issues_repo_name: polendri/idris-regex

max_forks_repo_name: polendri/idris-regexp


text:
module Issue835

baz : (x : Nat) -> {P2 : Nat -> Type} -> P2 x
baz x = ?rhs3

foo : {P : Nat -> Type}  -> Dec (P 0)
foo = ?rhs1 where

  bar : {P2 : Nat -> Type} ->
          (x : Nat)
          -> P2 x
  bar x with (S x)
     bar x | x1 =  ?rhs2


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 7

-- check that all functions are total
%default total

--
-- Shapes and pictures
--

||| Represents shapes
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
             Rectangle Double Double
           | ||| A circle with its radius
             Circle Double
%name Shape shape, shape1, shape2

||| Area of a shape
area : Shape -> Double
area (Triangle x y) = 0.5 * x * y
area (Rectangle x y) = x * y
area (Circle x) = pi * x * x

Eq Shape where
  (==) (Triangle x z) (Triangle x' z') = x == x' && z == z'
  (==) (Rectangle x z) (Rectangle x' z') = x == x' && z == z'
  (==) (Circle x) (Circle x') = x == x'
  (==) _ _ = False

Ord Shape where
  compare x y = compare (area x) (area y)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]

||| Represents pictures
data Picture = ||| A primitive shape
               Primitive Shape
             | ||| The combination of two pictures
               Combine Picture Picture
             | ||| The rotation of a picture, given the angle and the picture
               Rotate Double Picture
             | ||| The translation of a picture, given dx, dy, and the picture
               Translate Double Double Picture
%name Picture pic, pic1, pic2

rectangle : Picture
rectangle = Primitive $ Rectangle 20 10

circle : Picture
circle = Primitive $ Circle 5

triangle : Picture
triangle = Primitive $ Triangle 10 10

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
                      (Combine (Translate 35 5 circle)
                               (Translate 15 25 triangle))

||| Area of a picture
pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic pic1) = pictureArea pic + pictureArea pic1
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

||| Computes the largest of two inputs or Nothing if both are Nothing
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe (Just x) Nothing = Just x
maxMaybe Nothing (Just y) = Just y
maxMaybe (Just x) (Just y) = Just (max x y)

||| Biggest triangle
biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive tri@(Triangle x y)) = Just (area tri)
biggestTriangle (Primitive (Rectangle x y)) = Nothing
biggestTriangle (Primitive (Circle x)) = Nothing
biggestTriangle (Combine pic1 pic2)
  = maxMaybe (biggestTriangle pic1) (biggestTriangle pic2)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3)) (Primitive (Triangle 2 4))

testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3)) (Primitive (Circle 4))

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module India.Language.Core.Lexer

import Text.Lexer

import India.Union

%default total

public export
IndianToken : List Type -> Type
IndianToken = TokenData . Token . Union Prelude.id

public export
data Space = SP

export
TokenKind Space where
  TokType = const String
  tokValue = flip const

export
Eq Space where
  (==) = const $ const True

export
Show Space where
  show = const "Space"

public export
data Newline = NL

export
TokenKind Newline where
  TokType = const Unit
  tokValue = const $ const ()

export
Eq Newline where
  (==) = const $ const True

export
Show Newline where
  show p = "Newline"

public export
data Escaped = ESC Char

export
Eq Escaped where
  (==) = (==) `on` (\(ESC c) => c)

export
Show Escaped where
  show (ESC x) = "Escaped \{pack [x]}"

export
TokenKind Escaped where
  TokType = const Char
  tokValue (ESC x) = const x

public export
data Word = W

export
Eq Word where
  (==) = const $ const $ True

export
Show Word where
  show =  const "Word"

export
TokenKind Word where
  TokType = const String
  tokValue = flip const

export
word : List Lexer -> Lexer
word stops = (reject stop <+> any) <+> manyUntil stop any
  where
    stop : Lexer
    stop = some (choice stops)

export
escaped : Lexer
escaped = is '\\' <+> any

export
record LexerEntry (ts : List Type) where
  constructor Entry
  lexer : Lexer
  tok : t
  {auto member : Member t ts}

export
record IndianLexer (ts : List Type) where
  constructor MkIndianLexer
  stop   : List $ LexerEntry ts
  exact  : List $ LexerEntry ts

export
indianLexer : (Member Word ts) => IndianLexer ts -> TokenMap $ Token $ Union Prelude.id ts
indianLexer (MkIndianLexer  stop exact)
  = let stops = map lexer stop
  in toTokenMap $ (map (\x => (x.lexer, inj @{x.member} x.tok)) $ exact ++ stop)
                 ++ [(word stops, inj W)]

export
CoreLexer : Member Space ts =>
            Member Newline ts =>
            IndianLexer ts
CoreLexer = MkIndianLexer
  [Entry newlines NL, Entry spaces SP]
  []

export
coreLexer : TokenMap $ Token $ Union Prelude.id [Word, Space, Newline]
coreLexer = indianLexer CoreLexer

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india