text:
> module List.Properties

> import Data.List
> import Data.List.Quantifiers
> import Data.Fin
> import Control.Isomorphism
> import Syntax.PreorderReasoning

> import List.Operations
> import Fun.Operations
> import Fun.Properties
> import Unique.Predicates
> import Finite.Predicates
> import Finite.Operations
> import Sigma.Sigma
> import Pairs.Operations
> import Basic.Operations
> -- import Isomorphism.Operations
> import Fin.Properties
> import Void.Properties
> import Unit.Properties
> import Num.Refinements
> import Pair.Properties

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

* |List| is a functor:

> -- functorSpec1 : fmap . id = id

> -- functorSpec2 : fmap (f . g) = (fmap f) . (fmap g)

* |List| is a monad:

> -- monadSpec1 : (fmap f) . ret = ret . f

> -- monadSpec21 : bind (ret a) f = f a

> -- monadSpec22 : bind ma ret = ma

> -- monadSpec23 : {A, B, C : Type} -> {f : A -> M B} -> {g : B -> M C} ->
> --                bind (bind ma f) g = bind ma (\ a => bind (f a) g)

* |List| is a container monad:

> |||
> elemNonEmptySpec0 : {A : Type} ->
>                     (a : A) -> (as : List A) ->
>                     a `Elem` as -> List.Operations.NonEmpty as
> elemNonEmptySpec0 _  Nil      p = absurd p
> elemNonEmptySpec0 _ (a :: as) _ = ()

> |||
> elemNonEmptySpec1 : {A : Type} ->
>                     (as : List A) ->
>                     List.Operations.NonEmpty as -> Sigma A (\ a => a `Elem` as)
> elemNonEmptySpec1  Nil      c = void c
> elemNonEmptySpec1 (a :: as) _ = MkSigma a Here

> |||
> containerMonadSpec1 : {A : Type} -> {a : A} -> a `Elem` (ret a)
> containerMonadSpec1 {A} {a} = Here

> -- containerMonadSpec2 : {A : Type} -> (a : A) -> (ma : M A) -> (mma : M (M A)) ->
> --                       a `Elem` ma -> ma `Elem` mma -> a `Elem` (join mma)

> containerMonadSpec3 : {A : Type} -> {P : A -> Type} -> (a : A) -> (as : List A) ->
>                       All P as -> a `Elem` as -> P a
> containerMonadSpec3 a'  Nil       _           eprf        = absurd eprf
> containerMonadSpec3 a' (a :: as)  Nil         _           impossible
> containerMonadSpec3 a  (a :: as) (pa :: pas)  Here        = pa
> containerMonadSpec3 a' (a :: as) (pa :: pas) (There eprf) = containerMonadSpec3 a' as pas eprf

> -- containerMonadSpec4 : {A : Type} -> (ma : M A) -> fmap outl (tagElem ma) = ma

> -- containerMonadSpec5 : {A : Type} -> {P : A -> Type} ->
> --                       (as : List A) -> ((a : A) -> a `Elem` as -> P a) -> All P as

* Specific container monad properties

> |||
> uniqueAllLemma : {A : Type} -> {P : A -> Type} ->
>                  Unique1 P -> (as : List A) -> Unique (All P as)
> uniqueAllLemma u1P  Nil      Nil Nil = Refl
> uniqueAllLemma u1P (a :: as) (pa :: pas) (pa' :: pas') =
>     ( pa :: pas )
>   ={ replace {P = \ ZUZU => pa :: pas = ZUZU :: pas} (u1P a pa pa') Refl }=
>     ( pa' :: pas )
>   ={ replace {P = \ ZUZU => pa' :: pas = pa' :: ZUZU} (uniqueAllLemma u1P as pas pas') Refl }=
>     ( pa' :: pas' )
>   QED

> |||
> finiteAllLemma0 : {A : Type} -> {P : A -> Type} ->
>                   Finite1 P -> Iso (All P Nil) Unit
> finiteAllLemma0 f1P = MkIso to from toFrom fromTo where
>   to : All P Nil -> Unit
>   to Nil = ()
>   from : Unit -> All P Nil
>   from () = Nil
>   toFrom : (k : Unit) -> to (from k) = k
>   toFrom () = Refl
>   fromTo : (nil : All P Nil) -> from (to nil) = nil
>   fromTo Nil = Refl

> |||
> finiteAllLemma1 : {A : Type} -> {P : A -> Type} ->
>                   Finite1 P -> (a : A) -> (as : List A) ->
>                   Iso (All P (a :: as)) (P a, All P as)
> finiteAllLemma1 {P} f1P a as = MkIso to from toFrom fromTo where
>   to : All P (a :: as) -> (P a, All P as)
>   to (pa :: pas) = (pa, pas)
>   from : (P a, All P as) -> All P (a :: as)
>   from (pa, pas) = pa :: pas
>   toFrom : (papas : (P a, All P as)) -> to (from papas) = papas
>   toFrom (pa, pas) = Refl
>   fromTo : (papas : All P (a :: as)) -> from (to papas) = papas
>   fromTo (pa :: pas) = Refl

> |||
> finiteAllLemma : {A : Type} -> {P : A -> Type} ->
>                  Finite1 P -> (as : List A) -> Finite (All P as)
> finiteAllLemma {P} f1P Nil = MkSigma (S Z) iso where
>   iso : Iso (All P Nil) (Fin (S Z))
>   iso = isoTrans (finiteAllLemma0 f1P) (isoSym isoFin1Unit)
> finiteAllLemma {P} f1P (a :: as) = MkSigma n iso where
>   fH : Finite (P a)
>   fH = f1P a
>   mH : Nat
>   mH = getWitness fH
>   isoH : Iso (P a) (Fin mH)
>   isoH = getProof fH
>   fT : Finite (All P as)
>   fT = finiteAllLemma f1P as
>   mT : Nat
>   mT = getWitness fT
>   isoT : Iso (All P as) (Fin mT)
>   isoT = getProof fT
>   n  : Nat
>   n  = mH * mT
>   iso1 : Iso (All P (a :: as)) (P a, All P as)
>   iso1 = finiteAllLemma1 f1P a as
>   iso2 : Iso (P a, All P as) (Fin mH, Fin mT)
>   iso2 = pairCong isoH isoT
>   iso3 : Iso (Fin mH, Fin mT) (Fin (mH * mT))
>   iso3 = finPairTimes
>   iso  : Iso (All P (a :: as)) (Fin n)
>   iso  = isoTrans iso1 (isoTrans iso2 iso3)

> |||
> finiteAll : {A : Type} -> {P : A -> Type} ->
>             Finite1 P -> (as : List A) -> Finite (All P as)
> finiteAll = finiteAllLemma

> ||| All is decidable
> decidableAll : {A : Type} -> {P : A -> Type} ->
>                (dec : (a : A) -> Dec (P a)) -> (as : List A) -> Dec (All P as)
> decidableAll = all

> ||| NotEmpty is finite
> finiteNonEmpty : {A : Type} -> (as : List A) -> Finite (List.Operations.NonEmpty as)
> finiteNonEmpty  Nil      = finiteVoid
> finiteNonEmpty (a :: as) = finiteUnit

> ||| NonEmpty is decidable
> decidableNonEmpty : {A : Type} -> (as : List A) -> Dec (List.Operations.NonEmpty as)
> decidableNonEmpty {A} Nil       = No absurd
> decidableNonEmpty {A} (a :: as) = Yes ()

> ||| tagElem preserves length
> tagElemPreservesLength : {A : Type} -> (as : List A) -> length (tagElem as) = length as
> tagElemPreservesLength  Nil      = Refl
> tagElemPreservesLength (a :: as) = ( length (tagElem (a :: as)) )
>                                  ={ Refl }=
>                                    ( length ((MkSigma a Here) :: (map (idThere a as) (tagElem as))) )
>                                  ={ Refl }=
>                                    ( S (length (map (idThere a as) (tagElem as))) )
>                                  ={ cong (mapPreservesLength (idThere a as) (tagElem as)) }=
>                                    ( S (length (tagElem as)) )
>                                  ={ cong (tagElemPreservesLength as) }=
>                                    ( S (length as) )
>                                  ={ Refl }=
>                                    ( length (a :: as) )
>                                  QED

* |nub| preserves non-emptiness:

> nubPreservesNonEmpty : {A : Type} -> (Eq A) =>
>                        (as : List A) ->
>                        List.Operations.NonEmpty as ->
>                        List.Operations.NonEmpty (nub as)
> nubPreservesNonEmpty Nil ne = absurd ne
> nubPreservesNonEmpty (a :: as) ne = ()

* |fmap| preserves shape:

> mapPreservesNonEmpty : {A, B : Type} ->
>                        (f : A -> B) -> (as : List A) ->
>                        List.Operations.NonEmpty as ->
>                        List.Operations.NonEmpty (map f as)
> mapPreservesNonEmpty f Nil ne = absurd ne
> mapPreservesNonEmpty f (a :: as) ne = ()

* Fusion-related properties:

> |||
> mapSndMapCrossAnyIdLemma : {A, B, C : Type} ->
>                            (f : A -> C) ->
>                            (abs : List (A, B)) ->
>                            map snd (map (cross f id) abs) = map snd abs
> mapSndMapCrossAnyIdLemma _ Nil = Refl
> mapSndMapCrossAnyIdLemma f ((a, b) :: abs) =
>     ( map snd (map (cross f id) ((a, b) :: abs)) )
>   ={ Refl }=
>     ( map snd ((f a, b) :: map (cross f id) abs) )
>   ={ Refl }=
>     ( b :: map snd (map (cross f id) abs) )
>   ={ cong (mapSndMapCrossAnyIdLemma f abs) }=
>     ( b :: map snd abs )
>   ={ Refl }=
>     ( map snd ((a, b) :: abs) )
>   QED

* Properties of |length|:

> |||
> lengthLemma : {A, B, C : Type} ->
>               (as : List A) -> (f : A -> B) -> (g : A -> C) ->
>               length (map f as) = length (map g as)
> lengthLemma  Nil      f g = Refl
> lengthLemma (a :: as) f g = ( length (map f (a :: as)) )
>                           ={ Refl }=
>                             ( length (f a :: map f as) )
>                           ={ Refl }=
>                             ( S (length (map f as)) )
>                           ={ cong (lengthLemma as f g) }=
>                             ( S (length (map g as)) )
>                           ={ Refl }=
>                             ( length (g a :: map g as) )
>                           ={ Refl }=
>                             ( length (map g (a :: as)) )
>                           QED

> |||
> lengthConsLemma : {A, B : Type} ->
>                   (a : A) -> (b : B) -> (as : List A) -> (bs : List B) ->
>                   length (a :: as) = length (b :: bs) -> length as = length bs
> lengthConsLemma a b as bs prf = succInjective (length as) (length bs) s2 where
>   s1 : length (a :: as) = length (b :: bs)
>   s1 = prf
>   s2 : S (length as) = S (length bs)
>   s2 = replace2 {P = \ X => \ Y => X = Y} Refl Refl s1

> |||
> lengthReplicateLemma : {A : Type} ->
>                        (n : Nat) -> (a : A) ->
>                        length (replicate n a) = n
> lengthReplicateLemma  Z    _ = Refl
> lengthReplicateLemma (S m) a = ( length (replicate (S m) a) )
>                              ={ Refl }=
>                                ( length (a :: replicate m a) )
>                              ={ Refl }=
>                                ( S (length (replicate m a)) )
>                              ={ cong (lengthReplicateLemma m a) }=
>                                ( S m )
>                              QED

* Properties of |zip| and |unzip|:

> |||
> unzipConsLemma : {A, B : Type} ->
>                  (ab : (A, B)) -> (abs : List (A, B)) ->
>                  unzip (ab :: abs) = (fst ab :: fst (unzip abs), snd ab :: snd (unzip abs))
> unzipConsLemma (a, b) abs with (unzip abs)
>   | (_, _) = Refl

> |||
> fstUnzipConsLemma : {A, B : Type} ->
>                     (ab : (A, B)) -> (abs : List (A, B)) ->
>                     fst (unzip (ab :: abs)) = fst ab :: fst (unzip abs)
> fstUnzipConsLemma ab abs = cong {f = fst} (unzipConsLemma ab abs)

> |||
> sndUnzipConsLemma : {A, B : Type} ->
>                     (ab : (A, B)) -> (abs : List (A, B)) ->
>                     snd (unzip (ab :: abs)) = snd ab :: snd (unzip abs)
> sndUnzipConsLemma ab abs = cong {f = snd} (unzipConsLemma ab abs)

> |||
> unzipZipLemma : {A, B : Type} ->
>                 (as : List A) -> (bs : List B) -> length as = length bs ->
>                 unzip (zip as bs) = (as, bs)
> unzipZipLemma  Nil       Nil      _   = Refl
> unzipZipLemma  Nil      (b :: bs) prf = absurd prf
> unzipZipLemma (a :: as)  Nil      prf = absurd (sym prf)
> unzipZipLemma (a :: as) (b :: bs) prf with (unzip (zip as bs)) proof p
>   | (left, right) = s4 where
>       s1 : length as = length bs
>       s1 = lengthConsLemma a b as bs prf
>       s2 : unzip (zip as bs) = (as, bs)
>       s2 = unzipZipLemma as bs s1
>       s3 : (left, right) = (as, bs)
>       s3 = trans p s2
>       s4 : (a :: left, b :: right) = (a :: as, b :: bs)
>       s4 = replace2 {P = \ X => \ Y => (a :: left, b :: right) = (a :: X, b :: Y)}
>                     (cong {f = fst} s3) (cong {f = snd} s3) Refl

> |||
> sumMapSndUnzipLemma : {A, B : Type} -> (Num B) =>
>                       (abs : List (A, B)) -> sumMapSnd abs = sum (snd (unzip abs))
> sumMapSndUnzipLemma  Nil        = Refl
> sumMapSndUnzipLemma (ab :: abs) =
>     ( sumMapSnd (ab :: abs) )
>   ={ Refl }=
>     ( sum (map snd (ab :: abs)) )
>   ={ Refl }=
>     ( sum (snd ab :: map snd abs) )
>   ={ Refl }=
>     ( snd ab + sum (map snd abs) )
>   ={ Refl }=
>     ( snd ab + sumMapSnd abs )
>   ={ cong (sumMapSndUnzipLemma abs) }=
>     ( snd ab + sum (snd (unzip abs)) )
>   ={ Refl }=
>     ( sum (snd ab :: snd (unzip abs)) )
>   ={ cong (sym (sndUnzipConsLemma ab abs)) }=
>     ( sum (snd (unzip (ab :: abs))) )
>   QED

* Properties of |fold|:

> foldrListLemma : {A, B : Type} ->
>                  (f : A -> B -> B) -> (e : B) ->
>                  (a : A) -> (as : List A) ->
>                  foldr f e (a :: as) = f a (foldr f e as)
> foldrListLemma f e a as = Refl

* Properties of |sum| (for lists of types which are refinements of |Num|):

> |||
> sumSingletonLemma : {A : Type} -> (NumPlusZeroNeutral A) => (x : A) -> sum [x] = x
> sumSingletonLemma x = ( x + 0 )
>                     ={ plusZeroRightNeutral x }=
>                       ( x )
>                     QED

> |||
> sumPlusAppendLemma : {B : Type} -> (NumPlusAssociative B) =>
>                      (xs : List B) -> (ys : List B) ->
>                      (sum xs + sum ys) = sum (xs ++ ys)
> sumPlusAppendLemma Nil       ys = plusZeroLeftNeutral (sum ys)
> sumPlusAppendLemma (x :: xs) ys =
>     ( sum (x :: xs) + sum ys )
>   ={ Refl }=
>     ( (x + sum xs) + sum ys )
>   ={ sym (plusAssociative x (sum xs) (sum ys)) }=
>     ( x + (sum xs + sum ys) )
>   ={ cong (sumPlusAppendLemma xs ys) }=
>     ( x + sum (xs ++ ys) )
>   ={ Refl }=
>     ( sum (x :: (xs ++ ys)) )
>   ={ Refl }=
>     ( sum ((x :: xs) ++ ys) )
>   QED

> |||
> sumConcatLemma : {B : Type} -> (NumPlusAssociative B) =>
>                  (bss : List (List B)) ->
>                  sum (map sum bss) = sum (concat bss)
> sumConcatLemma  Nil        = Refl
> sumConcatLemma (bs :: bss) =
>     ( sum (map sum (bs :: bss)) )
>   ={ Refl }=
>     ( sum (sum bs :: map sum bss) )
>   ={ Refl }=
>     ( sum bs + sum (map sum bss) )
>   ={ cong (sumConcatLemma bss) }=
>     ( sum bs + sum (concat bss) )
>   ={ sumPlusAppendLemma bs (concat bss) }=
>     ( sum (bs ++ concat bss) )
>   ={ Refl }=
>     ( sum (concat (bs :: bss)) )
>   QED

> |||
> sumMapSndNilLemma : {A, B : Type} -> (Num B) => sumMapSnd {A} {B} Prelude.List.Nil = fromInteger 0
> sumMapSndNilLemma = Refl

> |||
> sumMapSndSingletonLemma : {A, B : Type} -> (NumPlusZeroNeutral B) =>
>                           (a : A) -> (b : B) -> sumMapSnd [(a, b)] = b
> sumMapSndSingletonLemma a b = ( sumMapSnd [(a, b)] )
>                             ={ Refl }=
>                               ( sum (map snd [(a, b)]) )
>                             ={ Refl }=
>                               ( sum [b] )
>                             ={ sumSingletonLemma b }=
>                               ( b )
>                             QED

> |||
> sumMapSndConcatLemma : {A, B : Type} -> (NumPlusAssociative B) =>
>                        (abss : List (List (A, B))) ->
>                        sum (map sumMapSnd abss) = sumMapSnd (concat abss)
> sumMapSndConcatLemma  Nil          = Refl
> sumMapSndConcatLemma (abs :: abss) =
>     ( sum (map sumMapSnd (abs :: abss)) )
>   ={ Refl }=
>     ( sum (sumMapSnd abs :: map sumMapSnd abss) )
>   ={ Refl }=
>     ( sum (sum (map snd abs) :: map sumMapSnd abss) )
>   ={ Refl }=
>     ( sum (map snd abs) + sum (map sumMapSnd abss) )
>   ={ cong (sumMapSndConcatLemma abss) }=
>     ( sum (map snd abs) + sumMapSnd (concat abss) )
>   ={ Refl }=
>     ( sum (map snd abs) + sum (map snd (concat abss)) )
>   ={ sumPlusAppendLemma (map snd abs) (map snd (concat abss)) }=
>     ( sum (map snd abs ++ map snd (concat abss)) )
>   ={ cong (sym (mapDistributesOverAppend snd abs (concat abss))) }=
>     ( sum (map snd (abs ++ concat abss)) )
>   ={ Refl }=
>     ( sum (map snd (concat (abs :: abss))) )
>   ={ Refl }=
>     ( sumMapSnd (concat (abs :: abss)) )
>   QED

> |||
> sumMapSndMapIdRightMultLemma : {A, B : Type} -> (Num B) =>
>                                (b : B) -> (ab : (A, B)) -> (abs : List (A, B)) ->
>                                (snd ab) * b + sumMapSnd (mapIdRightMult (abs, b))
>                                =
>                                sumMapSnd (mapIdRightMult ((ab :: abs), b))
> sumMapSndMapIdRightMultLemma b ab abs =
>     ( (snd ab) * b + sumMapSnd (mapIdRightMult (abs, b)) )
>   ={ Refl }=
>     ( (snd ab) * b + sum (map snd (mapIdRightMult (abs, b))) )
>   ={ Refl }=
>     ( sum ((snd ab) * b :: (map snd (mapIdRightMult (abs, b)))) )
>   ={ Refl }=
>     ( sum (snd (fst ab, (snd ab) * b) :: (map snd (mapIdRightMult (abs, b)))) )
>   ={ Refl }=
>     ( sum (snd ((cross id (* b)) (fst ab, snd ab)) :: (map snd (mapIdRightMult (abs, b)))) )
>   ={ cong {f = \ ZUZU => sum (snd ((cross id (* b)) ZUZU) :: (map snd (mapIdRightMult (abs, b))))}
>           (sym (pairLemma ab)) }=
>     ( sum (snd ((cross id (* b)) ab) :: (map snd (mapIdRightMult (abs, b)))) )
>   ={ Refl }=
>     ( sum (snd ((cross id (* b)) ab) :: (map snd (map (cross id (* b)) abs))) )
>   ={ Refl }=
>     ( sum (map snd (((cross id (* b)) ab) :: map (cross id (* b)) abs)) )
>   ={ Refl }=
>     ( sum (map snd (map (cross id (* b)) (ab :: abs))) )
>   ={ Refl }=
>     ( sum (map snd (mapIdRightMult ((ab :: abs), b))) )
>   ={ Refl }=
>     ( sumMapSnd (mapIdRightMult ((ab :: abs), b)) )
>   QED

> |||
> mapIdRightMultLemma : {A, B : Type} -> (NumMultDistributesOverPlus B) =>
>                       (absb : (List (A, B), B)) ->
>                       sumMapSnd (mapIdRightMult absb)
>                       =
>                       (sumMapSnd (fst absb)) * (snd absb)
> mapIdRightMultLemma {A} {B} (Nil, b) =
>     ( sumMapSnd {A} (mapIdRightMult (Nil, b)) )
>   ={ Refl }=
>     ( sumMapSnd {A} (map (cross id (* b)) Nil) )
>   ={ Refl }=
>     ( sumMapSnd {A} Nil )
>   ={ Refl }=
>     ( 0 )
>   ={ sym (multZeroLeftZero b) }=
>     ( 0 * b )
>   ={ Refl }=
>     ( (sumMapSnd {A} Nil) * b )
>   ={ Refl }=
>     ( (sumMapSnd {A} (fst (Nil, b))) * (snd {a = List (A, B)} (Nil, b)) )
>   QED
> mapIdRightMultLemma ((ab :: abs), b) = assert_total (
>     ( sumMapSnd (mapIdRightMult ((ab :: abs), b)) )
>   ={ sym (sumMapSndMapIdRightMultLemma b ab abs) }=
>     ( (snd ab) * b + sumMapSnd (mapIdRightMult (abs, b)) )
>   ={ cong (mapIdRightMultLemma (abs, b)) }=
>     ( (snd ab) * b + (sumMapSnd (fst (abs, b))) * (snd (abs, b)) )
>   ={ Refl }=
>     ( (snd ab) * b + (sumMapSnd abs) * b )
>   ={ sym (multDistributesOverPlusLeft (snd ab) (sumMapSnd abs) b) }=
>     ( (snd ab + sumMapSnd abs) * b )
>   ={ Refl }=
>     ( (snd ab + sum (map snd abs)) * b )
>   ={ Refl }=
>     ( (sumMapSnd (ab :: abs)) * b )
>   ={ Refl }=
>     ( (sumMapSnd (fst ((ab :: abs), b))) * (snd ((ab :: abs), b)) )
>   QED
>   )

> |||
> mvMultLemma : {A, A', B : Type} -> (NumMultDistributesOverPlus B) =>
>               (abs : List (A, B)) -> (f : A -> List (A', B)) -> ((a : A) -> sumMapSnd (f a) = 1) ->
>               sumMapSnd (mvMult abs f) = sumMapSnd abs
> mvMultLemma  Nil        _ _   = Refl
> mvMultLemma (ab :: abs) f prf =
>   let a = fst ab in
>   let b = snd ab in
>   let fid = cross f id in
>   let h = mapIdRightMult . fid in
>     ( sumMapSnd (mvMult (ab :: abs) f) )
>   ={ Refl }=
>     ( sumMapSnd (concat (map h (ab :: abs))) )
>   ={ sym (sumMapSndConcatLemma (map h (ab :: abs))) }=
>     ( sum (map sumMapSnd (map h (ab :: abs))) )
>   ={ Refl }=
>     ( sum (map sumMapSnd (h ab :: map h abs)) )
>   ={ Refl }=
>     ( sum (sumMapSnd (h ab) :: map sumMapSnd (map h abs)) )
>   ={ cong {f = \ ZUZU => sum (ZUZU :: map sumMapSnd (map h abs))} (mapIdRightMultLemma ((cross f id) ab)) }=
>     ( sum ((sumMapSnd (fst (fid ab))) * (snd (fid ab)) :: map sumMapSnd (map h abs)) )
>   ={ cong {f = \ ZUZU => sum ((sumMapSnd (fst (fid ab))) * ZUZU :: map sumMapSnd (map h abs))}
>           (crossAnyIdSndLemma' {ab} {f}) }=
>     ( sum ((sumMapSnd (fst (fid ab))) * (snd ab) :: map sumMapSnd (map h abs)) )
>   ={ cong {f = \ ZUZU => sum ((sumMapSnd ZUZU) * (snd ab) :: map sumMapSnd (map h abs))}
>           (crossAnyIdFstLemma' {ab} {f}) }=
>     ( sum ((sumMapSnd (f a)) * b :: map sumMapSnd (map h abs)) )
>   ={ cong {f = \ ZUZU => sum (ZUZU * b :: map sumMapSnd (map h abs))} (prf a) }=
>     ( sum (1 * b :: map sumMapSnd (map h abs)) )
>   ={ cong {f = \ ZUZU => sum (ZUZU :: map sumMapSnd (map h abs))} (multOneLeftNeutral b) }=
>     ( sum (b :: map sumMapSnd (map h abs)) )
>   ={ Refl }=
>     ( b + sum (map sumMapSnd (map h abs)) )
>   ={ cong (sumMapSndConcatLemma (map h abs)) }=
>     ( b + sumMapSnd (concat (map h abs)) )
>   ={ Refl }=
>     ( b + sumMapSnd (mvMult abs f) )
>   ={ cong (mvMultLemma abs f prf) }=
>     ( b + sumMapSnd abs )
>   ={ Refl }=
>     ( b + sum (map snd abs) )
>   ={ Refl }=
>     ( sum (b :: map snd abs) )
>   ={ Refl }=
>     ( sum (map snd (ab :: abs)) )
>   ={ Refl }=
>     ( sumMapSnd (ab :: abs) )
>   QED

* Ad-hoc filtering

> |||
> discardZeroesLemma : {B : Type} -> (NumPlusZeroNeutral B, DecEq B) =>
>                    (bs : List B) -> sum (discardZeroes bs) = sum bs
> discardZeroesLemma  Nil      = Refl
> discardZeroesLemma (b :: bs) with (decEq b 0)
>   | (Yes p) = ( sum (discardZeroes bs) )
>             ={ discardZeroesLemma bs }=
>               ( sum bs )
>             ={ sym (plusZeroLeftNeutral (sum bs)) }=
>               ( 0 + sum bs )
>             ={ cong {f = \ ZUZU => ZUZU + sum bs} (sym p) }=
>               ( b + sum bs )
>             ={ Refl }=
>               ( sum (b :: bs) )
>             QED
>   | (No _)  = ( sum (b :: discardZeroes bs) )
>             ={ Refl }=
>               ( b + sum (discardZeroes bs) )
>             ={ cong (discardZeroesLemma bs) }=
>               ( b + sum bs )
>             ={ Refl }=
>               ( sum (b :: bs) )
>             QED

> |||
> discardBySndZeroLemma : {A, B : Type} -> (NumPlusZeroNeutral B, DecEq B) =>
>                         (abs : List (A, B)) -> sumMapSnd (discardBySndZero abs) = sumMapSnd abs
> discardBySndZeroLemma  Nil      = Refl
> discardBySndZeroLemma (ab :: abs) with (decEq (snd ab) 0)
>   | (Yes p) = ( sumMapSnd (discardBySndZero abs) )
>             ={ discardBySndZeroLemma abs }=
>               ( sumMapSnd abs )
>             ={ sym (plusZeroLeftNeutral (sumMapSnd abs)) }=
>               ( 0 + sumMapSnd abs )
>             ={ cong {f = \ ZUZU => ZUZU + sumMapSnd abs} (sym p) }=
>               ( (snd ab) + sumMapSnd abs )
>             ={ Refl }=
>               ( sumMapSnd (ab :: abs) )
>             QED
>   | (No _)  = ( sumMapSnd (ab :: discardBySndZero abs) )
>             ={ Refl }=
>               ( (snd ab) + sumMapSnd (discardBySndZero abs) )
>             ={ cong (discardBySndZeroLemma abs) }=
>               ( (snd ab) + sumMapSnd abs )
>             ={ Refl }=
>               ( sumMapSnd (ab :: abs) )
>             QED

> |||
> postulate discardBySndZeroLemmaEq : {A, B : Type} -> (Num B, Eq B) =>
>                                     (abs : List (A, B)) -> sumMapSnd (discardBySndZeroEq abs) = sumMapSnd abs

> |||
> discardBySndZeroLemma1 : {A, B : Type} -> (Num B, DecEq B) =>
>                          (a : A) -> (b : B) -> Not (b = 0) ->
>                          discardBySndZero ((a, b) :: Nil) = (a, b) :: Nil
> discardBySndZeroLemma1 a b contra with (decEq b 0)
>   | (Yes prf) = void (contra prf)
>   | (No _)  = Refl


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 11, section 2

import Data.Primitives.Views
import System

-- check that all functions are total
%default total

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

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

data InfIO : Type where
  Do : IO a
       -> (a -> Inf InfIO)
       -> InfIO

loopPrint : String -> InfIO
loopPrint msg = Do (putStrLn msg)
                   (\_ => loopPrint msg)

partial
run : InfIO -> IO ()
run (Do action cont) = do res <- action
                          run (cont res)

data Fuel = Dry | More Fuel

tank : Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

runOnFuel : Fuel -> InfIO -> IO ()
runOnFuel (More fuel) (Do act gen) = do res <- act
                                        runOnFuel fuel (gen res)
runOnFuel Dry ios = putStrLn "Out of fuel"

data LazyFuel = LDry | LMore (Lazy LazyFuel)

partial
forever : LazyFuel
forever = LMore forever

runOnLazyFuel : LazyFuel -> InfIO -> IO ()
runOnLazyFuel (LMore fuel) (Do act gen) = do res <- act
                                             runOnLazyFuel fuel (gen res)
runOnLazyFuel LDry ios = putStrLn "Out of fuel"

(>>=) : IO a -> (a -> Inf InfIO)  -> InfIO
(>>=) = Do

loopPrint' : String -> InfIO
loopPrint' msg = do putStrLn msg
                    loopPrint' msg

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

partial
main : IO ()
main = do seed <- time
          runOnLazyFuel forever (quiz' (arithInputs (fromInteger seed)) 0)

ext: idr

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Data.Vect
import Data.String
import System

-- Page 110: 1 - 5

-- Exercise 1
-- Extend the Vehicle data type so that it supports
-- unicycles and motorcycles, and update wheels and refuel accordingly.

-- Exercise 2
-- Extend the PowerSource and Vehicle data types to support electric vehicles
-- (such as trams or electric cars).

data PowerSource = Petrol | Pedal | Electric
data Vehicle : PowerSource -> Type where
  Unicycle : Vehicle Pedal
  Bicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : Vehicle Electric

wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Unicycle = 1
wheels (Motorcycle fuel) = 2
wheels Tram = 0

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Motorcycle fuel) = Motorcycle 50

-- Exercise 3
-- The take function, on List, has type Nat -> List a -> List a. What’s an
-- appropriate type for the corresponding vectTake function on Vect?
-- Hint: How do the lengths of the input and output relate? It shouldn’t be
-- valid to take more elements than there are in the Vect. Also, remember that
-- you can have any expression in a type.

-- The answer is
-- take : (n : Nat) -> Vect (n + m) elem -> Vect n elem
-- which in fact can be obtained just by doing
-- :t Vect.take on a terminal

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

-- Exercise 5
sumEntriesFin : Num a => Maybe (Fin n) -> (xs : Vect n a) -> (ys : Vect n a) -> Maybe a
sumEntriesFin Nothing xs ys = Nothing
sumEntriesFin (Just i) xs ys = Just $ index i xs + index i ys

sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = sumEntriesFin (integerToFin pos n) xs ys

-- Page 131: 1 - 2
-- Exercise 1
printLonger : IO()
printLonger = do
                x <- getLine
                y <- getLine
                let xl = length x
                let yl = length y
                let m = max xl yl
                putStrLn (show m)

-- Exercise 2
printLonger' : IO()
printLonger' = getLine >>= \x =>
               getLine >>= \y =>
               let xl = length x in
               let yl = length y in
               let m = max xl yl in
               putStrLn (show m)

-- Page 138: 1 - 4
-- Exercise 1

makeMessage: (guess : Maybe Integer) -> (target : Integer) -> (String, Bool)
makeMessage Nothing target = ("Please input a number", True)
makeMessage (Just g) target =
  if g == target then ("Correct!", False) else
  if g < target then ("Too low", True)
    else ("Too high", True)

guess : (target : Integer) -> IO ()
guess target = do
  putStrLn "Choose a number"
  l <- getLine
  let i = parseInteger l
  let (message, continue) = makeMessage i target
  putStrLn message
  if continue then (guess target) else pure()

-- Exercise 2

main : IO()
main = do
    putStrLn "Welcome to the guessing show!"
    putStrLn ""
    number <- time
    guess number

-- Exercise 3
guess' : (target : Integer) -> (guesses : Nat) -> IO ()
guess' target guesses = do
  putStrLn $ "You have tried " ++ show guesses ++ " times"
  putStrLn "Choose a number"
  l <- getLine
  let i = parseInteger l
  let (message, continue) = makeMessage i target
  putStrLn message
  if continue then (guess' target (S guesses)) else pure()

-- Exercise 4
--repl' : String -> (String -> String) -> IO ()
--repl' x f = do
--  putStrLn (f x)
--  repl' x f

--replWith' : (state : a) -> (prompt : String) ->
--            (onInput : a -> String -> Maybe (String, a)) -> IO ()
-- replWith' state prompt onInput = ?replWith'_rhs

-- Page 145: 1 - 3
-- Exercise 1

-- Source: https://gist.github.com/PeterHajdu/0a4a0de909660921e5da1034e8b17360#file-readtoblank-idr-L5
readToBlank : IO (List String)
readToBlank = do
  line <- getLine
  if line == "" then pure [] else (line ::) <$> readToBlank
  -- Not really sure how to implement the last part!

-- Exercise 2
readAndSave : IO ()
readAndSave = do
  lines <- readToBlank
  let content = concat lines
  filename <- getLine
  Right () <- writeFile filename content
    | Left err => putStrLn (show err)
  pure ()

-- Exercise 3
-- readVectFile : (filename : String) -> IO (n ** Vect n String)
-- readVectFile filename = do
--  Right file <- openFile filename Read
--    | Left err => do
--      putStrLn "Error while reading file"
--      pure (0 ** [])
--  let content = ...

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module With

f : (n : Nat) -> (m : Nat ** n : Nat ** m = n + n)
f n with (n + n) proof eq
  f n | Z     = (Z ** n ** sym eq)
  f n | (S m) = (S m ** n ** sym eq)

g : List a -> Nat
g [] = Z
g (a :: as) with (as ++ as)
  g (b :: bs) | asas = Z

nested : Nat -> Nat
nested m with (m)
  nested m | Z with (m + m)
    nested m | Z | 0 = 1
    nested m | Z | S k with (k + k)
      nested m | Z | S k | Z = 2
      nested m | Z | S k | S l with (l + l)
        nested m | Z | S k | S l | Z = 3
        nested m | Z | S k | S l | S p = 4
  nested m | S k = 5

data ANat : Nat -> Type where
  MkANat : (n : Nat) -> ANat n

someNats : Nat -> Nat
someNats n with (MkANat n)
  someNats n | m@(MkANat n) with (MkANat n)
    someNats n | p@(MkANat n) | MkANat n = Z


text:
module Data.AVL

import Data.List

-- Boring basic AVL weight balanced BST
-- ordered on keys to be more versatile

Height : Type
Height = Int

export
data Tree : Type -> Type -> Type where
  Leaf : Tree k a
  Node : (h : Int) -> (key : k) -> (v : a) -> (l : Tree k a) -> (r : Tree k a) -> Tree k a

-- a               a    a
--  \             /  ->  \
--   b   ->  b   b        b
--    \     / \
--     c   a   c
rotateL : Tree k a -> Tree k a
rotateL (Node hA kA vA lA (Node hB kB vB lB c)) = Node hB kB vB (Node hA kA vA lA lB) c
rotateL t = t

roLtest1 : rotateL (Node 0 1 'a' Leaf (Node 0 2 'b' Leaf (Node 0 3 'c' Leaf Leaf))) = Node 0 2 'b' (Node 0 1 'a' Leaf Leaf) (Node 0 3 'c' Leaf Leaf)
roLtest1 = Refl

rotateR : Tree k a -> Tree k a
rotateR (Node hA kA vA (Node hB kB vB c rB) rA) = Node hB kB vB c (Node hA kA vA rB rA)
rotateR t = t

roRtest1 : rotateR (Node 0 1 'a' (Node 0 2 'b' (Node 0 3 'c' Leaf Leaf) Leaf) Leaf) = Node 0 2 'b' (Node 0 3 'c' Leaf Leaf) (Node 0 1 'a' Leaf Leaf)
roRtest1 = Refl

--     c       c
--    /       /
--   a   ->  b   -> b
--    \     /      / \
--     b   a      a   c
rotateRL : Tree k a -> Tree k a
rotateRL Leaf = Leaf
rotateRL (Node x k v l r) = rotateR (Node x k v (rotateL l) r)

foobles2 : rotateRL (Node 0 3 'c' (Node 0 1 'a' Leaf (Node 0 2 'b' Leaf Leaf)) Leaf) = Node 0 2 'b' (Node 0 1 'a' Leaf Leaf) (Node 0 3 'c' Leaf Leaf)
foobles2 = Refl

rotateLR : Tree k a -> Tree k a
rotateLR Leaf = Leaf
rotateLR (Node x k v l r) = rotateL (Node x k v l (rotateR r))

foobles3 : rotateLR (Node 0 1 'a' Leaf (Node 0 3 'c' (Node 0 2 'b' Leaf Leaf) Leaf)) = Node 0 2 'b' (Node 0 1 'a' Leaf Leaf) (Node 0 3 'c' Leaf Leaf)
foobles3 = Refl

public export
data NonEmpty : Tree k a -> Type where
  IsNonEmpty : NonEmpty (Node h k v l r)

export
height : Tree k a -> Int
height Leaf = 0
height (Node h k v l r) = h

checkBalance : (t : Tree k a) -> Int
checkBalance Leaf = 0
checkBalance (Node x k v l r) = height r - height l

data Balance = LeftHeavy | LeftLean | Neutral | RightLean | RightHeavy

checkBalance' : Tree k a -> Balance
checkBalance' Leaf = Neutral
checkBalance' t = let i = checkBalance t
               in   if i > 1 then RightHeavy
               else if i == 1 then  RightLean
               else if i == -1 then LeftLean
               else if i < -1 then LeftHeavy
               else Neutral

isLeftHeavy : Tree k a -> Bool
isLeftHeavy t with (checkBalance' t)
  isLeftHeavy t | LeftHeavy = True
  isLeftHeavy t | _ = False

isRightHeavy : Tree k a -> Bool
isRightHeavy t with (checkBalance' t)
  isRightHeavy t | RightHeavy = True
  isRightHeavy t | _ = False

balance : Tree k a -> Tree k a
balance Leaf = Leaf
balance n@(Node h k v l r) = case checkBalance' n of
    LeftHeavy => if isRightHeavy l then rotateRL n else rotateR n
    LeftLean => n
    Neutral => n
    RightLean => n
    RightHeavy => if isLeftHeavy r then rotateLR n else rotateL n

export
insert : Ord k => k -> a -> Tree k a -> Tree k a
insert i x Leaf = Node 1 i x Leaf Leaf
insert i x n@(Node h k v l r) = case compare i k of
    EQ => n
    LT => balance $ Node h k v (insert i x l) r
    GT => balance $ Node h k v l (insert i x r)

export
lookup : Ord k => k -> Tree k a -> Maybe a
lookup i Leaf = Nothing
lookup i n@(Node h k v l r) = case compare i k of
    EQ => Just v
    LT => lookup i l
    GT => lookup i r

export
fromList : Ord k => List (k,a) -> Tree k a
fromList = foldr (uncurry insert) Leaf

bt : Tree Int Char
bt = Node 3 1 '1' Leaf (Node 2 2 '2' (Node 1 3 '3' Leaf Leaf) Leaf)

bt2 : Tree Int Char
bt2 = Node 3 1 '1' (Node 2 2 '2' (Node 1 3 '3' Leaf Leaf) Leaf) Leaf

bt3 : Tree Int Char
bt3 = fromList [(1,'1'),(2,'2'),(3,'3')]

foobles4 : balance (Node 3 1 'a' Leaf (Node 2 3 'c' (Node 1 2 'b' Leaf Leaf) Leaf)) = Node 2 2 'b' (Node 1 1 'a' Leaf Leaf) (Node 1 3 'c' Leaf Leaf)
foobles4 = ?dsfdfs


text:
module Compiler.Opts.InlineHeuristics

import Compiler.CompileExpr
import Core.Context
import Core.Context.Log
import Data.Vect

parameters (fn : Name)
    isVar : CExp vars -> Bool
    isVar (CLocal _ _) = True
    isVar (CRef _ _) = True
    isVar (CForce _ _ x) = isVar x
    isVar (CDelay _ _ x) = isVar x
    isVar _ = False

    simple : CExp vars -> Bool
    simple (CLocal _ _) = True
    simple (CRef _ _) = True
    simple (CLam _ _ _) = False
    simple (CLet _ _ _ _ _) = False
    simple (CApp _ (CRef _ fn') xs) = not (fn == fn') && all isVar xs
    simple (CApp _ fn xs) = isVar fn && all isVar xs
    simple (CCon _ _ _ _ xs) = all isVar xs
    simple (COp _ _ xs) = all isVar xs
    simple (CExtPrim _ _ xs) = all isVar xs
    simple (CForce _ _ y) = simple y
    simple (CDelay _ _ y) = simple y
    simple (CConCase _ _ _ _) = False
    simple (CConstCase _ _ _ _) = False
    simple (CPrimVal _ _) = True
    simple (CErased _) = True
    simple (CCrash _ _) = False

    inlineCDef : CDef -> Bool
    inlineCDef (MkFun args exp) =
        simple exp
    inlineCDef _ = False

export
inlineHeuristics : Ref Ctxt Defs => Name -> Core ()
inlineHeuristics fn = do
    defs <- get Ctxt
    Just (fnIdx, gdef) <- lookupCtxtExactI fn defs.gamma
        | Nothing => pure ()
    let Just cdef = gdef.compexpr
        | Nothing => pure ()
    let True = inlineCDef fn cdef
        | False => pure ()
    log "compiler.inline.heuristic" 25 $ "inlining heuristic decided to inline: " ++ show fn
    unless (NoInline `elem` gdef.flags) $ setFlag EmptyFC (Resolved fnIdx) Inline


text:
||| Low-Level C Sockets bindings for Idris. Used by higher-level, cleverer things.
||| Type-unsafe parts. Use Network.Socket for a safe variant.
|||
||| Original (C) SimonJF, MIT Licensed, 2014
||| Modified (C) The Idris Community, 2015, 2016
module Network.Socket.Raw

import public Network.Socket.Data

import Network.FFI

-- ---------------------------------------------------------------- [ Pointers ]

public export
data RecvStructPtr     = RSPtr AnyPtr

public export
data RecvfromStructPtr = RFPtr AnyPtr

public export
data BufPtr = BPtr AnyPtr

public export
data SockaddrPtr = SAPtr AnyPtr

-- ---------------------------------------------------------- [ Socket Utilies ]

||| Put a value in a buffer
export
sock_poke : HasIO io => BufPtr -> Int -> Int -> io ()
sock_poke (BPtr ptr) offset val = primIO $ prim__idrnet_poke ptr offset val

||| Take a value from a buffer
export
sock_peek : HasIO io => BufPtr -> Int -> io Int
sock_peek (BPtr ptr) offset = primIO $ prim__idrnet_peek ptr offset

||| Frees a given pointer
export
sock_free : HasIO io => BufPtr -> io ()
sock_free (BPtr ptr) = primIO $ prim__idrnet_free ptr

export
sockaddr_free : HasIO io => SockaddrPtr -> io ()
sockaddr_free (SAPtr ptr) = primIO $ prim__idrnet_free ptr

||| Allocates an amount of memory given by the ByteLength parameter.
|||
||| Used to allocate a mutable pointer to be given to the Recv functions.
export
sock_alloc : HasIO io => ByteLength -> io BufPtr
sock_alloc bl = map BPtr $ primIO $ prim__idrnet_malloc bl

||| Retrieves the port the given socket is bound to
export
getSockPort : HasIO io => Socket -> io Port
getSockPort sock = primIO $ prim__idrnet_sockaddr_port $ descriptor sock

||| Retrieves a socket address from a sockaddr pointer
export
getSockAddr : HasIO io => SockaddrPtr -> io SocketAddress
getSockAddr (SAPtr ptr) = do
  addr_family_int <- primIO $ prim__idrnet_sockaddr_family ptr

  -- ASSUMPTION: Foreign call returns a valid int
  assert_total (case getSocketFamily addr_family_int of
    Just AF_INET => do
      ipv4_addr <- primIO $ prim__idrnet_sockaddr_ipv4 ptr

      pure $ parseIPv4 ipv4_addr
    Just AF_INET6 => pure IPv6Addr
    Just AF_UNSPEC => pure InvalidAddress)

export
freeRecvStruct : HasIO io => RecvStructPtr -> io ()
freeRecvStruct (RSPtr p) = primIO $ prim__idrnet_free_recv_struct p

||| Utility to extract data.
export
freeRecvfromStruct : HasIO io => RecvfromStructPtr -> io ()
freeRecvfromStruct (RFPtr p) = primIO $ prim__idrnet_free_recvfrom_struct p

||| Sends the data in a given memory location
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @ptr  The location containing the data to send.
||| @len  How much of the data to send.
export
sendBuf : HasIO io
       => (sock : Socket)
       -> (ptr  : BufPtr)
       -> (len  : ByteLength)
       -> io (Either SocketError ResultCode)
sendBuf sock (BPtr ptr) len = do
  send_res <- primIO $ prim__idrnet_send_buf (descriptor sock) ptr len

  if send_res == (-1)
   then map Left getErrno
   else pure $ Right send_res

||| Receive data from a given memory location.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to receive the message.
||| @ptr  The location containing the data to receive.
||| @len  How much of the data to receive.
export
recvBuf : HasIO io
       => (sock : Socket)
       -> (ptr  : BufPtr)
       -> (len  : ByteLength)
       -> io (Either SocketError ResultCode)
recvBuf sock (BPtr ptr) len = do
  recv_res <- primIO $ prim__idrnet_recv_buf (descriptor sock) ptr len

  if (recv_res == (-1))
    then map Left getErrno
    else pure $ Right recv_res

||| Send a message stored in some buffer.
|||
||| Returns on failure a `SocketError`
||| Returns on success the `ResultCode`
|||
||| @sock The socket on which to send the message.
||| @addr Address of the recipient.
||| @port The port on which to send the message.
||| @ptr  A Pointer to the buffer containing the message.
||| @len  The size of the message.
export
sendToBuf : HasIO io
         => (sock : Socket)
         -> (addr : SocketAddress)
         -> (port : Port)
         -> (ptr  : BufPtr)
         -> (len  : ByteLength)
         -> io (Either SocketError ResultCode)
sendToBuf sock addr p (BPtr dat) len = do
  sendto_res <- primIO $ prim__idrnet_sendto_buf
                (descriptor sock) dat len (show addr) p (toCode $ family sock)

  if sendto_res == (-1)
    then map Left getErrno
    else pure $ Right sendto_res

||| Utility function to get the payload of the sent message as a `String`.
export
foreignGetRecvfromPayload : HasIO io => RecvfromStructPtr -> io String
foreignGetRecvfromPayload (RFPtr p) = primIO $ prim__idrnet_get_recvfrom_payload p

||| Utility function to return senders socket address.
export
foreignGetRecvfromAddr : HasIO io => RecvfromStructPtr -> io SocketAddress
foreignGetRecvfromAddr (RFPtr p) = do
  sockaddr_ptr <- map SAPtr $ primIO $ prim__idrnet_get_recvfrom_sockaddr p
  getSockAddr sockaddr_ptr

||| Utility function to return sender's IPV4 port.
export
foreignGetRecvfromPort : HasIO io => RecvfromStructPtr -> io Port
foreignGetRecvfromPort (RFPtr p) = do
  sockaddr_ptr <- primIO $ prim__idrnet_get_recvfrom_sockaddr p
  port         <- primIO $ prim__idrnet_sockaddr_ipv4_port sockaddr_ptr
  pure port

||| Receive a message placed on a 'known' buffer.
|||
||| Returns on failure a `SocketError`.
||| Returns on success a pair of
||| + `UDPAddrInfo` :: The address of the sender.
||| + `Int`         :: Result value from underlying function.
|||
||| @sock The channel on which to receive.
||| @ptr  Pointer to the buffer to place the message.
||| @len  Size of the expected message.
|||
export
recvFromBuf : HasIO io
           => (sock : Socket)
           -> (ptr  : BufPtr)
           -> (len  : ByteLength)
           -> io (Either SocketError (UDPAddrInfo, ResultCode))
recvFromBuf sock (BPtr ptr) bl = do
  recv_ptr <- primIO $ prim__idrnet_recvfrom_buf (descriptor sock) ptr bl

  let recv_ptr' = RFPtr recv_ptr

  isnull <- nullPtr recv_ptr

  if isnull
    then map Left getErrno
    else do
      result <- primIO $ prim__idrnet_get_recvfrom_res recv_ptr
      if result == -1
        then do
          freeRecvfromStruct recv_ptr'
          map Left getErrno
        else do
          port <- foreignGetRecvfromPort recv_ptr'
          addr <- foreignGetRecvfromAddr recv_ptr'
          freeRecvfromStruct recv_ptr'
          pure $ Right (MkUDPAddrInfo addr port, result + 1)


text:
import DataStore

import Data.Vect

{- 1 -}

testStore : DataStore (SString .+. SInt)
testStore = addToStore ("First", 1) $
            addToStore ("Second", 2) $
            empty

getValues : DataStore (SString .+. val_schema) ->
            List (SchemaType val_schema)
getValues input with (storeView input)
  getValues empty | SNil = []
  getValues (addToStore (key, value) store) | (SAdd rec)
       = value :: getValues store | rec

{- 2 -}

export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

export
triangle : Double -> Double -> Shape
triangle = Triangle

export
rectangle : Double -> Double -> Shape
rectangle = Rectangle

export
circle : Double -> Shape
circle = Circle

data ShapeView : Shape -> Type where
     STriangle : ShapeView (triangle base height)
     SRectangle : ShapeView (rectangle width height)
     SCircle : ShapeView (circle radius)

shapeView : (s : Shape) -> ShapeView s
shapeView (Triangle x y) = STriangle
shapeView (Rectangle x y) = SRectangle
shapeView (Circle x) = SCircle

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = pi * radius * radius

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Control.Monad.Ref

import public Control.Monad.Identity
import public Control.Monad.Trans
import public Data.IORef
import public Data.Universe

%default total
%access public export

%hide Language.Reflection.Ref
%hide Language.Reflection.Universe

-- Interface -------------------------------------------------------------------

interface ( Monad m, Universe t ) => MonadRef (t : Type) (l : t -> Type) (m : Type -> Type) | m where
  ref    : (typeOf a) -> m (l a)
  deref  : l a -> m (typeOf a)
  assign : l a -> (typeOf a) -> m ()

infix 4 :=
(:=) : MonadRef t l m => l a -> (typeOf a) -> m ()
(:=) = assign

-- Instances -------------------------------------------------------------------

||| Note:
||| - We can't make an instance of MonadRef for IO because of the type clash between
|||   `l : t -> Type` and `IORef : Type -> Type`
-- MonadRef t IORef IO where
--   ref    = newIORef
--   deref  = readIORef
--   assign = writeIORef

-- Helpers ---------------------------------------------------------------------

modify : MonadRef t l m => l a -> (typeOf a -> typeOf a) -> m ()
modify l f = do
  x <- deref l
  l := f x

{- Tests -----------------------------------------------------------------------

test0 : IO Int
test0 = do
  r <- newIORef 5
  writeIORef r 10
  x <- readIORef r
  pure x

test : MonadRef IORef IO => IO Int
test = do
  r <- ref (the Int 5)
  r := (the Int 10)
  x <- deref r
  pure x

-------------------------------------------------------------------------------}

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Idris.REPL.FuzzySearch

import Core.AutoSearch
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Env
import Core.InitPrimitives
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.Termination
import Core.TT
import Core.Unify

import Idris.Desugar
import Idris.Doc.String
import Idris.Error
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands
import Idris.IDEMode.MakeClause
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Parser
import Idris.Pretty
import Idris.ProcessIdr
import Idris.Resugar
import Idris.Syntax
import Idris.Version

import public Idris.REPL.Common

import Data.List
import Data.List1
import Data.Maybe
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Stream
import Data.String
import Data.DPair
import Libraries.Data.String.Extra
import Libraries.Data.List.Extra
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Path
import Libraries.System.Directory.Tree

import System
import System.File
import System.Directory

%default covering

export
fuzzySearch : {auto c : Ref Ctxt Defs}
           -> {auto u : Ref UST UState}
           -> {auto s : Ref Syn SyntaxInfo}
           -> {auto m : Ref MD Metadata}
           -> {auto o : Ref ROpts REPLOpts}
           -> PTerm
           -> Core REPLResult
fuzzySearch expr = do
  let Just (neg, pos) = parseExpr expr
    | _ => pure (REPLError (pretty "Bad expression, expected"
                       <++> code (pretty "B")
                       <++> pretty "or"
                       <++> code (pretty "_ -> B")
                       <++> pretty "or"
                       <++> code (pretty "A -> B")
                       <+> pretty ", where"
                       <++> code (pretty "A")
                       <++> pretty "and"
                       <++> code (pretty "B")
                       <++> pretty "are spines of global names"))
  defs <- branch
  let curr = currentNS defs
  let ctxt = gamma defs
  filteredDefs <-
    do names   <- allNames ctxt
       defs    <- traverse (flip lookupCtxtExact ctxt) names
       let defs = flip mapMaybe defs $ \ md =>
                      do d <- md
                         guard (visibleIn curr (fullname d) (visibility d))
                         guard (isJust $ userNameRoot (fullname d))
                         pure d
       allDefs <- traverse (resolved ctxt) defs
       filterM (\def => fuzzyMatch neg pos def.type) allDefs
  put Ctxt defs
  doc <- traverse (docsOrSignature EmptyFC) $ fullname <$> filteredDefs
  pure $ PrintedDoc $ vsep doc
 where

  data NameOrConst = AName Name
                   | AInt
                   | AInteger
                   | ABits8
                   | ABits16
                   | ABits32
                   | ABits64
                   | AString
                   | AChar
                   | ADouble
                   | AWorld
                   | AType

  eqConst : (x, y : NameOrConst) -> Bool
  eqConst AInt     AInt     = True
  eqConst AInteger AInteger = True
  eqConst ABits8   ABits8   = True
  eqConst ABits16  ABits16  = True
  eqConst ABits32  ABits32  = True
  eqConst ABits64  ABits64  = True
  eqConst AString  AString  = True
  eqConst AChar    AChar    = True
  eqConst ADouble  ADouble  = True
  eqConst AWorld   AWorld   = True
  eqConst AType    AType    = True
  eqConst _        _        = False

  parseNameOrConst : PTerm -> Maybe NameOrConst
  parseNameOrConst (PRef _ n)               = Just (AName n)
  parseNameOrConst (PPrimVal _ IntType)     = Just AInt
  parseNameOrConst (PPrimVal _ IntegerType) = Just AInteger
  parseNameOrConst (PPrimVal _ Bits8Type)   = Just ABits8
  parseNameOrConst (PPrimVal _ Bits16Type)  = Just ABits16
  parseNameOrConst (PPrimVal _ Bits32Type)  = Just ABits32
  parseNameOrConst (PPrimVal _ Bits64Type)  = Just ABits64
  parseNameOrConst (PPrimVal _ StringType)  = Just AString
  parseNameOrConst (PPrimVal _ CharType)    = Just AChar
  parseNameOrConst (PPrimVal _ DoubleType)  = Just ADouble
  parseNameOrConst (PPrimVal _ WorldType)   = Just AWorld
  parseNameOrConst (PType _)                = Just AType
  parseNameOrConst _                        = Nothing

  parseExpr' : PTerm -> Maybe (List NameOrConst)
  parseExpr' (PApp _ f x) =
    [| parseNameOrConst x :: parseExpr' f |]
  parseExpr' x = (:: []) <$> parseNameOrConst x

  parseExpr : PTerm -> Maybe (List NameOrConst, List NameOrConst)
  parseExpr (PPi _ _ _ _ a (PImplicit _)) = do
    a' <- parseExpr' a
    pure (a', [])
  parseExpr (PPi _ _ _ _ a b) = do
    a' <- parseExpr' a
    b' <- parseExpr' b
    pure (a', b')
  parseExpr b = do
    b' <- parseExpr' b
    pure ([], b')

  isApproximationOf : (given : Name)
                   -> (candidate : Name)
                   -> Bool
  isApproximationOf (NS ns n) (NS ns' n') =
    n == n' && Namespace.isApproximationOf ns ns'
  isApproximationOf (UN n) (NS ns' (UN n')) =
    n == n'
  isApproximationOf (NS ns n) _ =
    False
  isApproximationOf (UN n) (UN n') =
    n == n'
  isApproximationOf _ _ =
    False

  isApproximationOf' : (given : NameOrConst)
                    -> (candidate : NameOrConst)
                    -> Bool
  isApproximationOf' (AName x) (AName y) =
    isApproximationOf x y
  isApproximationOf' a b = eqConst a b

  ||| Find all name and type literal occurrences.
  export
  doFind : List NameOrConst -> Term vars -> List NameOrConst
  doFind ns (Local fc x idx y) = ns
  doFind ns (Ref fc x name) = AName name :: ns
  doFind ns (Meta fc n i xs)
      = foldl doFind ns xs
  doFind ns (Bind fc x (Let _ c val ty) scope)
      = doFind (doFind (doFind ns val) ty) scope
  doFind ns (Bind fc x b scope)
      = doFind (doFind ns (binderType b)) scope
  doFind ns (App fc fn arg)
      = doFind (doFind ns fn) arg
  doFind ns (As fc s as tm) = doFind ns tm
  doFind ns (TDelayed fc x y) = doFind ns y
  doFind ns (TDelay fc x t y)
      = doFind (doFind ns t) y
  doFind ns (TForce fc r x) = doFind ns x
  doFind ns (PrimVal fc c) =
    fromMaybe [] ((:: []) <$> parseNameOrConst (PPrimVal fc c)) ++ ns
  doFind ns (Erased fc i) = ns
  doFind ns (TType fc) = AType :: ns

  toFullNames' : NameOrConst -> Core NameOrConst
  toFullNames' (AName x) = AName <$> toFullNames x
  toFullNames' x = pure x

  fuzzyMatch : (neg : List NameOrConst)
            -> (pos : List NameOrConst)
            -> Term vars
            -> Core Bool
  fuzzyMatch neg pos (Bind _ _ b sc) = do
    let refsB = doFind [] (binderType b)
    refsB <- traverse toFullNames' refsB
    let neg' = diffBy isApproximationOf' neg refsB
    fuzzyMatch neg' pos sc
  fuzzyMatch (_ :: _) pos tm = pure False
  fuzzyMatch [] pos tm = do
    let refsB = doFind [] tm
    refsB <- traverse toFullNames' refsB
    pure (isNil $ diffBy isApproximationOf' pos refsB)


text:
module BootstrappedQueue

import Queue

%default total
%access private

export
data BootstrappedQueue a =
  E | Q Int (List a) (BootstrappedQueue (Lazy (List a))) Int (List a)

mutual
  checkF : Int -> List a -> BootstrappedQueue (Lazy (List a)) -> Int -> List a
        -> BootstrappedQueue a
  checkF lenfm [] E lenr r = E
  checkF lenfm [] m lenr r = Q lenfm (Force $ head m) (tail m) lenr r
  checkF lenfm f  m lenr r = Q lenfm f m lenr r

  checkQ : Int -> List a -> BootstrappedQueue (Lazy (List a)) -> Int -> List a
        -> BootstrappedQueue a
  checkQ lenfm f m lenr r =
    if lenr <= lenfm then checkF lenfm f m lenr r
    else checkF (lenfm + lenr) f (snoc m (reverse r)) 0 []

  export
  Queue BootstrappedQueue where
    empty = E -- Incorrect in original: Q 0 [] E 0 []
    isEmpty E = True
    isEmpty _ = False

    snoc E x = Q 1 [x] E 0 [] -- Incorrect in original: q 1 [x] E 0 []
    snoc (Q lenfm f m lenr r) x = checkQ lenfm f m (lenr + 1) (x :: r)

    head E                            = idris_crash "empty queue"
    head (Q lenfm (x :: f') m lenr r) = x
    head (Q _     []        _ _    _) = assert_unreachable

    tail E                            = idris_crash "empty queue"
    tail (Q lenfm (x :: f') m lenr r) = assert_total $ checkQ (lenfm - 1) f' m lenr r
    tail (Q _     []        _ _    _) = assert_unreachable


text:
module LightClick.DSL.Parser.API

import        Data.Vect
import        Data.List
import        Data.List1
import        Data.String
import        Data.Maybe

import public Text.Lexer
import public Text.Parser

import public Toolkit.Data.Location
import public Toolkit.Text.Lexer.Run
import public Toolkit.Text.Parser.Support
import        Toolkit.Text.Parser.Location
import public Toolkit.Text.Parser.Run

import        Language.SystemVerilog.Gates

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

import        LightClick.DSL.AST

import public LightClick.DSL.Lexer

namespace LightClick
  public export
  Rule : Type -> Type
  Rule = Rule () Token

  public export
  RuleEmpty : Type -> Type
  RuleEmpty = RuleEmpty () Token

  export
  eoi : RuleEmpty ()
  eoi = eoi isEOI
    where
      isEOI : Token -> Bool
      isEOI EndInput = True
      isEOI _ = False

export
symbol : String -> Rule ()
symbol str
  = terminal ("Expected Symbol '" ++ str ++ "'")
             (\x => case x of
                           Symbol s => if s == str then Just ()
                                                   else Nothing
                           _ => Nothing)

export
keyword : String -> Rule ()
keyword str
  = terminal ("Expected Keyword '" ++ str ++ "'")
               (\x => case x of
                           Keyword s => if s == str then Just ()
                                                    else Nothing
                           _ => Nothing)

export
natLit : Rule Nat
natLit = terminal "Expected nat literal"
             (\x => case x of
                         LitNat i => Just i
                         _ => Nothing)

export
strLit : Rule String
strLit = terminal "Expected string literal"
             (\x => case x of
                         LitStr s => Just s
                         _ => Nothing)

export
identifier : Rule String
identifier
  = terminal "Expected Identifier"
             (\x => case x of
                                ID str => Just str
                                _ => Nothing)

export
doc : Rule (List1 String)
doc = some docString
  where
    docString : Rule String
    docString = terminal "Documentation String"
                         (\x => case x of
                                     Documentation doc => Just doc
                                     _ => Nothing)

export
name : Rule String
name = identifier

export
arrow : Rule ()
arrow = symbol "->"

export
braces : Rule a
      -> Rule a
braces p
  = do symbol "["
       a <- p
       symbol "]"
       pure a

export
brackets : (Rule a)
        -> Rule a
brackets = between (symbol "{") (symbol "}")

export
parens : (Rule a)
      -> Rule a
parens = between (symbol "(") (symbol ")")

export
sepBy1V : (sep : Rule b)
       -> (p : Rule a)
       -> Rule (n ** Vect (S n) a)
sepBy1V sep p = do {x <- p; xs <- many (sep *> p); pure (_ ** fromList $ x::xs)}

export
sepBy2V : (sep : Rule ())
       -> (p : Rule a)
       -> Rule (n ** Vect (S (S n)) a)
sepBy2V sep p
  = do x <- p
       sep
       y <- p
       rest <- many (sep *> p)
       pure (_ ** fromList $ x::y::rest)

export
commaSepBy1V : (p : Rule a) -> Rule (n ** Vect (S n) a)
commaSepBy1V = sepBy1V (symbol ",")

export
commaSepBy2V : (p : Rule a) -> Rule (n ** Vect (S (S n)) a)
commaSepBy2V = sepBy2V (symbol ",")

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) ->
              (items : Vect size String) ->
              DataStore

size : DataStore -> Nat
size (MkData size items) = size

items : (store : DataStore) -> Vect (size store) String
items (MkData size items) = items

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newItem = MkData _ (addToData items)
  where
    addToData : Vect old String -> Vect (S old) String
    addToData [] = [newItem]
    addToData (item :: items2) = item :: addToData items2

data Command = Add String
             | Get Integer
             | Search String
             | Size
             | Quit

parseCommand : String -> String -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                         False => Nothing
                         True => Just (Get (cast val))
parseCommand "search" pat = Just (Search pat)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
                             case integerToFin pos (size store) of
                                  Nothing => Just ("Out of range\n", store)
                                  Just id => Just (index id store_items ++ "\n", store)

findAllMatches : String -> Integer -> Vect n String -> List (Integer, String)
findAllMatches pat idx [] = []
findAllMatches pat idx (x :: xs) = if isInfixOf pat x then (idx, x) :: findAllMatches pat (idx + 1) xs
                                                  else findAllMatches pat (idx + 1) xs

search : String -> DataStore -> List (Integer, String)
search pat (MkData size items) = findAllMatches pat 0 items

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp
   = case parse inp of
          Nothing => Just ("Invalid command\n", store)
          Just (Add item) => Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
          Just (Get pos) => getEntry pos store
          Just (Search pat) => Just ("Found: " ++ show (search pat store) ++ "\n", store)
          Just Size => Just ("Size of store: " ++ show (size store) ++ "\n", store)
          Just Quit => Nothing

main : IO ()
main = replWith (MkData _ []) "Command: " processInput


text:
> module Real.Sequence

> import Real.Postulates
> import Real.Properties

> %default total
> %access public export

> ||| Sequences as functions
> Sequence : Type
> Sequence = Nat -> Real

> using implementation NegReal
>   hasLimit : Sequence -> Real -> Type
>   hasLimit f x = (eps : Real) -> eps `GT` zero -> Exists (\ N => P f x eps N) where
>     P         : Sequence -> Real -> Real -> Nat -> Type
>     P f x eps N = (n : Nat) -> n `GT` N -> abs (f n - x) `LTE` eps

> limit : (s : Sequence) -> Exists (hasLimit s) -> Real
> limit s = getWitness

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


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

import GRL.Lang.GLang

import Edda
import Edda.Refine
import Edda.Writer.Org

import Freyja

%access private

-- ------------------------------------------------------------------- [ Utils ]

sectionTemplate : Nat -> Maybe String -> EddaString -> Edda PRIME BLOCK
sectionTemplate n l t = Section PRIME n l t Nil

section : Maybe String -> EddaString -> Edda PRIME BLOCK
section l t = sectionTemplate 0 l t

subsection : Maybe String -> EddaString -> Edda PRIME BLOCK
subsection l t = sectionTemplate 1 l t

subsubsection : Maybe String -> EddaString -> Edda PRIME BLOCK
subsubsection l t = sectionTemplate 2 l t

subsubsubsection : Maybe String -> EddaString -> Edda PRIME BLOCK
subsubsubsection l t = sectionTemplate 3 l t

-- ----------------------------------------------------------------- [ Affects ]

convertAffect : Affect -> EddaBody
convertAffect (MkAffect c r d) =
      [subsubsubsection Nothing
        ((Emph [Text $ show c]) :: Space :: name r ) ]
   ++ fromMaybe Nil d

-- ------------------------------------------------------------------ [ Traits ]

convertTrait : Trait ty -> EddaBody
convertTrait (MkTrait ty n d s as) =
      [subsubsection Nothing (Text (show ty) :: Colon :: Space :: n)]
   ++ d
   ++ [DList PRIME
         [MkPair [Text "Satisfaction"] [Text (show s)]]]
   ++ concatMap convertAffect as

convertTraits : DList TTy Trait ts -> EddaBody
convertTraits Nil     = Nil
convertTraits (m::ms) = convertTrait m ++ convertTraits ms

-- -------------------------------------------------------------- [ Properties ]

convertProperty : Property -> EddaBody
convertProperty (MkProperty n d ts) =
      [subsection Nothing (Text "Property" :: Colon :: Space :: n)]
   ++ d
   ++ convertTraits ts

-- ------------------------------------------------------------------ [ Models ]

convertModel : Model ty -> EddaBody
convertModel (MkModel n ty d m) =
      [subsection Nothing (Text (show ty) :: Colon :: Space :: n)]
   ++ [Listing
         Nothing
         (Text (show ty) :: Colon :: Space :: n)
         Nothing
         Nothing
         Nil
         m]
   ++ d

convertModels : DList MTy Model ms -> EddaBody
convertModels Nil     = Nil
convertModels (m::ms) = convertModel m ++ convertModels ms

-- ---------------------------------------------------------------- [ Solution ]

export
convertSolution : Solution -> EddaBody
convertSolution (MkSolution n d ms ps) =
       [section Nothing (Text "Solution" :: Colon :: Space :: n)]
    ++ d
    ++ convertModels ms
    ++ concatMap convertProperty ps

-- ------------------------------------------------------------ [ Requirements ]

convertReq : Requirement ty -> EddaBody
convertReq (MkReq ty n d) =
    [ subsection Nothing
        (Text (show ty) :: Colon :: Space :: n)]
    ++ d

convertReqs : DList RTy Requirement ms -> EddaBody
convertReqs Nil     = Nil
convertReqs (m::ms) = convertReq m ++ convertReqs ms

-- ----------------------------------------------------------------- [ Problem ]

export
convertProblem : Problem -> EddaBody
convertProblem (MkProblem n d rs) =
    [section Nothing (Text "Problem" :: Colon :: Space :: n)]
    ++
    d
    ++
    [subsection Nothing [Text "Requirements"]]
    ++ convertReqs rs

-- ----------------------------------------------------------------- [ Context ]

export
convertDomain : Context -> EddaBody
convertDomain (MkContext t d) = tblock :: d
  where
    tblock : Edda PRIME BLOCK
    tblock = section Nothing (Text "Context" :: Colon :: Space :: t)

-- ---------------------------------------------------------------- [ MetaData ]

export
convertMetadata : Metadata -> EddaBody
convertMetadata mdata =
       [section Nothing [Text "Metadata"]]
    ++ [subsection Nothing [Text "Aliases"]]
    ++ [BList (aliases mdata)]
    ++ [subsection Nothing [Text "Tags"]]
    ++ [BList (tags mdata)]
    ++ [subsection Nothing [Text "Authors"]]
    ++ [BList (authors mdata)]
    ++ [subsection Nothing [Text "Auditors"]]
    ++ [BList (auditors mdata)]
    ++ [subsection Nothing [Text "Times"]]
    ++ [DList PRIME
          [ MkPair [Text "Created"]  [Text (created mdata)]
          , MkPair [Text "Modified"] [Text (modified mdata)]
          , MkPair [Text "Evaluted"] [Text (evaluated mdata)]
          , MkPair [Text "ID"]       [Text (ident mdata)]]
       ]

-- ---------------------------------------------------------------- [ Evidence ]
export
convertEvidence : EddaBody -> EddaBody
convertEvidence d = [section Nothing [Text "Evidence"]] ++ d

-- ----------------------------------------------------------------- [ Studies ]
export
convertStudies : List Study -> EddaBody
convertStudies ss = [section Nothing [Text "Case Studies"]]
    ++ concatMap convertStudy ss
  where
    convertStudy : Study -> EddaBody
    convertStudy (MkStudy n b a) =
        [subsection Nothing (Text "Study" :: Colon :: Space :: n)]
     ++ [subsubsection Nothing [Text "Before"]]
     ++ b
     ++ [subsection Nothing [Text "Study"]]
     ++ a

-- --------------------------------------------------------------- [ Relations ]

convertRelations : DList LTy Relation ls -> EddaBody
convertRelations _ = Nil -- @TODO

-- ----------------------------------------------------------------- [ Pattern ]
export
convertPattern : PatternDoc -> Edda PRIME MODEL
convertPattern p = MkEdda as (intersperse (Empty PRIME) body)
  where
    as : List (String, String)
    as = [MkPair "TITLE" (inlines $ name p)]

    body : EddaBody
    body = summary p
        ++ (convertDomain $ context p)
        ++ (convertProblem $ problem p)
        ++ (convertSolution $ solution p)
        ++ (convertEvidence $ evidence p)
        ++ (convertStudies $ studies p)
        ++ (convertRelations $ relations p)
        ++ (convertMetadata $ mdata p)

namespace Freyja
  export
  toEdda : PatternDoc -> Edda PRIME MODEL
  toEdda pdoc = (convertPattern pdoc)

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


text:
module Crypto.ChaCha

import Control.Monad.State
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.Nat.Order.Properties
import Data.Vect
import Utils.Bytes
import Utils.Misc

public export
Key : Type
Key = Vect 8 Bits32 -- 32 * 8 = 256

public export
ChaChaState : Type
ChaChaState = Vect 16 Bits32

-- The first four words (0-3) are constants
public export
constants : Vect 4 Bits32
constants = [0x61707865, 0x3320646e, 0x79622d32, 0x6b206574] -- ['expa', 'nd 3', '2-by', 'te k']

public export
quarter_rotate : Fin 16 -> Fin 16 -> Fin 16 -> Fin 16 -> State ChaChaState ()
quarter_rotate a b c d = do
  modify (\s => updateAt a (+ index b s) s)
  modify (\s => updateAt d (`xor` index a s) s)
  modify (\s => updateAt d (rotl 16) s)

  modify (\s => updateAt c (+ index d s) s)
  modify (\s => updateAt b (`xor` index c s) s)
  modify (\s => updateAt b (rotl 12) s)

  modify (\s => updateAt a (+ index b s) s)
  modify (\s => updateAt d (`xor` index a s) s)
  modify (\s => updateAt d (rotl 8) s)

  modify (\s => updateAt c (+ index d s) s)
  modify (\s => updateAt b (`xor` index c s) s)
  modify (\s => updateAt b (rotl 7) s)

public export
double_rotate : State ChaChaState ()
double_rotate = do
  quarter_rotate 0 4  8 12
  quarter_rotate 1 5  9 13
  quarter_rotate 2 6 10 14
  quarter_rotate 3 7 11 15
  ------------------------
  quarter_rotate 0 5 10 15
  quarter_rotate 1 6 11 12
  quarter_rotate 2 7  8 13
  quarter_rotate 3 4  9 14

public export
run2x : (n_double_rounds : Nat) -> ChaChaState -> ChaChaState
run2x n_double_rounds s =
  execState s $ do
    original <- get
    go last
    modify (zipWith (+) original)
  where
  go : Fin (S n_double_rounds) -> State ChaChaState ()
  go FZ = pure ()
  go (FS wit) = double_rotate *> go (weaken wit)

||| ChaCha construction with 4 octets counter and 12 octets nonce as per RFC8439
public export
chacha_rfc8439_block : Nat -> (counter : Bits32) -> Key -> Vect 3 Bits32 -> Vect 64 Bits8
chacha_rfc8439_block rounds counter key nonce = concat $ map (to_le {n = 4}) $ run2x rounds $ constants ++ key ++ [counter] ++ nonce

||| ChaCha construction with 8 octets counter and 8 octets nonce as per the original ChaCha specification
public export
chacha_original_block : Nat -> (counter : Bits64) -> Key -> Vect 2 Bits32 -> Vect 64 Bits8
chacha_original_block rounds counter key nonce = concat $ map (to_le {n = 4}) $ run2x rounds $ constants ++ key ++ split_word counter ++ nonce
  where
    split_word : Bits64 -> Vect 2 Bits32
    split_word a = [ cast a, cast (shiftR a 32) ]


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

import GRL.Common
import GRL.Model

%access export
-- ------------------------------------------------------------- [ Eval Result ]

namespace EvalResult
  public export
  data EvalResult : Type where
    Result   : List GoalNode  -> EvalResult
    BadModel : EvalResult

  public export
  implementation Show EvalResult where
    show BadModel    = "Bad Model"
    show (Result xs) = unlines $ map (mkPretty) xs
       where
         mkPretty : GoalNode -> String
         mkPretty x = unwords [getNodeTitle x, show (fromMaybe NONE (getSValue x)), "\n"]

  toString : EvalResult -> (GoalNode -> String) -> Maybe String
  toString BadModel    _ = Nothing
  toString (Result xs) f = Just $ unlines (mkString xs)
    where
      mkString : List GoalNode -> List String
      mkString Nil     = Nil
      mkString (x::xs) = f x :: mkString xs

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Main

import Data.Vect

infixr 5 .+.

data Schema = SString
            | SInt
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

-- data DataStore : Type where
--      MkData : (schema : Schema) -> (size : Nat) -> (items : Vect size (SchemaType schema)) -> DataStore

record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

-- data Command = Add String
--              | Search String
--              | Get Integer
--              | Size
--              | Quit

data Command : Schema -> Type where
     Add : SchemaType schema -> Command schema
     Get : Integer -> Command schema
     SetSchema : (newschema : Schema) -> Command schema
     Quit : Command schema

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size store) y = MkData schema _ (addToData store)
  where
    addToData : Vect old (SchemaType schema) -> Vect (S old) (SchemaType schema)
    addToData [] = [y]
    addToData (x :: xs) = x :: addToData xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs tot inp = let val = cast inp in
          if val < 0
             then Nothing
             else let newVal = tot + val in
                      Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString inp = getQuoted (unpack inp)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs) = case span (/= '"') xs of
                                 (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                                 _ => Nothing
    getQuoted _ = Nothing
parsePrefix SInt inp = case span isDigit inp of
                            ("", rest) => Nothing
                            (num, rest) => Just (cast num, ltrim rest)
parsePrefix (x .+. y) inp = do l <- parsePrefix x inp
                               r <- parsePrefix y $ snd l
                               pure ((fst l, fst r), snd r)
-- parsePrefix (x .+. y) inp = case parsePrefix x inp of
--                                   Nothing => Nothing
--                                   Just (lval, inp') => case parsePrefix y inp' of
--                                                            Nothing => Nothing
--                                                            Just (rval, inp'') => Just ((lval, rval), inp'')

parseBySchema : (schema : Schema) -> (str : String) -> Maybe $ SchemaType schema
parseBySchema schema inp = case parsePrefix schema inp of
                                -- Just (res,  "") => Just res
                                Just _ => Nothing
                                Nothing => Nothing

parseCommand : (schema : Schema) -> (cmd : String) -> (args : String) -> Maybe (Command schema)
parseCommand schema "add" str = case parseBySchema schema str of
                                     Nothing => Nothing
                                     Just r => Just (Add r)
parseCommand schema "get" val = if all isDigit (unpack val) then Just (Get (cast val)) else Nothing
parseCommand schema "quit" "" = Just Quit
parseCommand schema _ args = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                   (cmd, args) => parseCommand schema cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (x .+. y)} (a, b) = display a ++ ", " ++ display b

getEntry : (ind : Integer) -> (ds : DataStore) -> Maybe (String, DataStore)
getEntry ind ds = let storeItems = items ds in
                      (case (integerToFin ind (size ds)) of
                            Nothing => Just ("Out of bounds \n", ds)
                            (Just id) => Just (display (index id storeItems) ++ "\n", ds))

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput ds inp = case parse (schema ds) inp of
                           Nothing => Just ("Invalid command inputed\n", ds)
                           (Just x) => (case x of
                                             (Add item) => Just ("ID " ++ show (size ds) ++ "\n", addToStore ds item)
                                             (Get ind) => getEntry ind ds
                                             -- (Search str) => searchForEntry str ds
                                             -- Size => Just ("Size Of Datastore: " ++ show (size ds) ++ "\n", ds)
                                             Quit => Nothing)

main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput


text:
import Control.Function

Injective Prelude.id where
  injective = id

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module EquivExercises

import Equiv
import Expr
import Imp
import Inequiv
import Logic
import Maps

%access public export

%default total

noninterfering_update : Not (l1 = l2) ->
                        VarNotUsedInAExp l1 a2 ->
                        VarNotUsedInAExp l2 a1 ->
                        aeval st a1 = n1 ->
                        ((aeval (t_update l1 n1 st) a2 = n2) ↔ aeval st a2 = n2)
noninterfering_update _ (VNUNum _) _ _ = (id, id)
noninterfering_update _ (VNUId y contra) _ _ =
  rewrite snd (beq_id_false_iff {x=l1} {y=y}) contra
  in (id, id)
noninterfering_update {st} contra (VNUPlus _ _ l1nua3 l1nua4) l2nua1 prf1 =
  let ih1 = noninterfering_update {st=st} contra l1nua3 l2nua1 prf1
      ih2 = noninterfering_update {st=st} contra l1nua4 l2nua1 prf1
  in ( \prf2 => rewrite fst ih1 Refl
                in rewrite fst ih2 Refl
                in prf2
     , \prf2 => rewrite sym $ fst ih1 Refl
                in rewrite sym $ fst ih2 Refl
                in prf2 )
noninterfering_update {st} contra (VNUMinus _ _ l1nua3 l1nua4) l2nua1 prf1 =
  let ih1 = noninterfering_update {st=st} contra l1nua3 l2nua1 prf1
      ih2 = noninterfering_update {st=st} contra l1nua4 l2nua1 prf1
  in ( \prf2 => rewrite fst ih1 Refl
                in rewrite fst ih2 Refl
                in prf2
     , \prf2 => rewrite sym $ fst ih1 Refl
                in rewrite sym $ fst ih2 Refl
                in prf2 )
noninterfering_update {st} contra (VNUMult _ _ l1nua3 l1nua4) l2nua1 prf1 =
  let ih1 = noninterfering_update {st=st} contra l1nua3 l2nua1 prf1
      ih2 = noninterfering_update {st=st} contra l1nua4 l2nua1 prf1
  in ( \prf2 => rewrite fst ih1 Refl
                in rewrite fst ih2 Refl
                in prf2
     , \prf2 => rewrite sym $ fst ih1 Refl
                in rewrite sym $ fst ih2 Refl
                in prf2 )

swap_noninterfering_assignments : Not (l1 = l2) ->
                                  VarNotUsedInAExp l1 a2 ->
                                  VarNotUsedInAExp l2 a1 ->
                                  CEquiv (do l1 ::= a1; l2 ::= a2)
                                         (do l2 ::= a2; l1 ::= a1)
swap_noninterfering_assignments {l1} {l2} {a1} {a2} contra l1nua2 l2nua1 st st' =
  (forward, backward)
where forward : ((do l1 ::= a1; l2 ::= a2) / st \\ st') ->
                ((do l2 ::= a2; l1 ::= a1) / st \\ st')
      forward rel = case rel of
        E_Seq (E_Ass {n=n1} prf1) (E_Ass {n=n2} prf2) =>
          let pf1 = fst (noninterfering_update {st=st} contra l1nua2 l2nua1 prf1)
                        prf2
              pf2 = snd (noninterfering_update {st=st}
                                               (neqSym contra) l2nua1 l1nua2 pf1)
                        prf1
          in rewrite t_update_permute contra {v1=n2} {v2=n1} {m=st}
          in E_Seq (E_Ass pf1) (E_Ass pf2)
      backward : ((do l2 ::= a2; l1 ::= a1) / st \\ st') ->
                 ((do l1 ::= a1; l2 ::= a2) / st \\ st')
      backward rel = case rel of
        E_Seq (E_Ass {n=n1} prf1) (E_Ass {n=n2} prf2) =>
          let pf1 = fst (noninterfering_update
                           {st=st} (neqSym contra) l2nua1 l1nua2 prf1)
                        prf2
              pf2 = snd (noninterfering_update {st=st} contra l1nua2 l2nua1 pf1)
                        prf1
          in rewrite sym $ t_update_permute contra {v1=n1} {v2=n2} {m=st}
          in E_Seq (E_Ass pf1) (E_Ass pf2)

CApprox : (c1, c2 : Com) -> Type
CApprox c1 c2 = (st, st' : State) -> (c1 / st \\ st') -> (c2 / st \\ st')

c1 : Com
c1 = WHILE (not (X == 1)) $
       X ::= X - 1

c2 : Com
c2 = X ::= 1

c3 : Com
c3 = c2

c4 : Com
c4 = X ::= 2

c3_c4_different : ( Not (CApprox EquivExercises.c3 EquivExercises.c4)
                  , Not (CApprox EquivExercises.c4 EquivExercises.c3) )
c3_c4_different = (forward, backward)
where forward : Not ((st, st' : State) ->
                     (EquivExercises.c3 / st \\ st') ->
                     (EquivExercises.c4 / st \\ st'))
      forward f = case f empty_state (t_update X 1 empty_state) (E_Ass Refl) of
        E_Skip impossible
        (E_Ass _) impossible
        (E_Seq _ _) impossible
        (E_IfTrue _ _) impossible
        (E_IfFalse _ _) impossible
        (E_WhileEnd _) impossible
        (E_WhileLoop _ _ _) impossible
      backward : Not ((st, st' : State) ->
                      (EquivExercises.c4 / st \\ st') ->
                      (EquivExercises.c3 / st \\ st'))
      backward f = case f empty_state (t_update X 2 empty_state) (E_Ass Refl) of
        E_Skip impossible
        (E_Ass _) impossible
        (E_Seq _ _) impossible
        (E_IfTrue _ _) impossible
        (E_IfFalse _ _) impossible
        (E_WhileEnd _) impossible
        (E_WhileLoop _ _ _) impossible

cmin : Com
cmin = WHILE BTrue SKIP

cmin_minimal : (c : Com) -> CApprox EquivExercises.cmin c
cmin_minimal _ _ _ rel = absurd $ while_true_nonterm btrue_is_true rel


text:
-- | ISO 8601 Ordinal Date format
module Data.Time.Calendar.OrdinalDate

import Data.Time.Calendar.Days
import Data.Time.Calendar.Private

||| Is this year a leap year according to the proleptic Gregorian calendar?
export
isLeapYear : Integer -> Bool
isLeapYear year = (mod year 4 == 0) && ((mod year 400 == 0) || not (mod year 100 == 0))

-- | Convert to ISO 8601 Ordinal Date format. First element of result is year (proleptic Gregoran calendar),
-- second is the day of the year, with 1 for Jan 1, and 365 (or 366 in leap years) for Dec 31.
export
toOrdinalDate : Day -> (Integer, Int)
toOrdinalDate (MkModifiedJulianDay mjd) =
  let
    a = mjd + 678575
    quadcent = div a 146097
    b = mod a 146097
    cent = min (div b 36524) 3
    c = b - (cent * 36524)
    quad = div c 1461
    d = mod c 1461
    y = min (div d 365) 3
    yd = fromInteger (d - (y * 365) + 1)
    year = quadcent * 400 + cent * 100 + quad * 4 + y + 1
  in
    (year, yd)

-- | Convert from ISO 8601 Ordinal Date format.
-- Invalid day numbers will be clipped to the correct range (1 to 365 or 366).
export
fromOrdinalDate : Integer -> Int -> Day
fromOrdinalDate year day =
  let
    y = year - 1
    clipped_day = (clip
                  1
                  (if isLeapYear year
                    then 366
                    else 365)
            (cast day))
    a = (365 * y)
    b = (div y (the Integer 4))
    c = (div y (the Integer 100))
    d = (div y (the Integer 400))
    e = (the Integer 678576)
    mjd = (fromInteger clipped_day) + a  + b - c + d - e
  in
    MkModifiedJulianDay mjd

||| Convert from ISO 8601 Ordinal Date format.
||| Invalid day numbers return 'Nothing'
export
fromOrdinalDateValid: Integer -> Int -> Maybe Day
fromOrdinalDateValid year day = do
    day' <-
        clipValid
            1
            (if isLeapYear year
                 then 366
                 else 365)
            day
    let y = year - 1
    let mjd = (cast day') + (365 * y) + (div y 4) - (div y 100) + (div y 400) - 678576
    pure (MkModifiedJulianDay mjd)

||| Show in ISO 8601 Ordinal Date format (yyyy-ddd)
export
showOrdinalDate : Day -> String
showOrdinalDate date =
  let (y, d) = toOrdinalDate date
  in
    (show y) ++ "-" ++ (show d)

||| Get the number of the Monday-starting week in the year and the day of the week.
||| The first Monday is the first day of week 1, any earlier days in the year are week 0 (as @%W@ in 'Data.Time.Format.formatTime').
|||Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
export
mondayStartWeek : Day -> (Int, Int)
mondayStartWeek date@(MkModifiedJulianDay dateint) =
  let
    yd = snd (toOrdinalDate date)
    d = dateint + 2
    k = d - (cast yd)
  in
    (fromInteger ((div d 7) - (div k 7)), fromInteger (mod d 7) + 1)

||| Get the number of the Sunday-starting week in the year and the day of the week.
||| The first Sunday is the first day of week 1, any earlier days in the year are week 0 (as @%U@ in 'Data.Time.Format.formatTime').
||| Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
export
sundayStartWeek : Day -> (Int, Int)
sundayStartWeek date@(MkModifiedJulianDay dateint) =
  let
    yd = snd (toOrdinalDate date)
    d = dateint + 3
    k = d - (cast yd)
  in
    (fromInteger ((div d 7) - (div k 7)), fromInteger (mod d 7))

||| The inverse of 'mondayStartWeek'. Get a 'Day' given the year,
||| the number of the Monday-starting week, and the day of the week.
||| The first Monday is the first day of week 1, any earlier days in the year
||| are week 0 (as @%W@ in 'Data.Time.Format.formatTime').
export
fromMondayStartWeek:
       Integer -- ^ Year.
    -> Int -- ^ Monday-starting week number (as @%W@ in 'Data.Time.Format.formatTime').
    -> Int -- ^ Day of week.
-- Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
    -> Day
fromMondayStartWeek year w d = let
    -- first day of the year
    firstDay = fromOrdinalDate year 1
    -- 0-based year day of first monday of the year
    zbFirstMonday = (5 - toInteger firstDay) `mod` 7
    -- 0-based week of year
    zbWeek = w - 1
    -- 0-based day of week
    zbDay = d - 1
    -- 0-based day in year
    zbYearDay = zbFirstMonday + 7 * cast zbWeek + cast zbDay
    in
      addDays zbYearDay firstDay

export
fromMondayStartWeekValid :
       Integer -- ^ Year.
    -> Int -- ^ Monday-starting week number (as @%W@ in 'Data.Time.Format.formatTime').
    -> Int -- ^ Day of week.
                               -- Monday is 1, Sunday is 7 (as @%u@ in 'Data.Time.Format.formatTime').
    -> Maybe Day
fromMondayStartWeekValid year w d = do
    d' <- clipValid 1 7 d
  -- first day of the year
    let    firstDay = fromOrdinalDate year 1
    -- 0-based week of year
    let    zbFirstMonday = (5 - toInteger firstDay) `mod` 7
    -- 0-based week number
    let    zbWeek = w - 1
    -- 0-based day of week
    let    zbDay = d' - 1
     -- 0-based day in year
    let    zbYearDay = zbFirstMonday + 7 * cast zbWeek + cast zbDay
    zbYearDay' <-
        clipValid
            0
            (if isLeapYear year
                 then 365
                 else 364)
            zbYearDay
    pure $ addDays zbYearDay' firstDay

||| The inverse of 'sundayStartWeek'. Get a 'Day' given the year and
||| the number of the day of a Sunday-starting week.
||| The first Sunday is the first day of week 1, any earlier days in the
||| year are week 0 (as @%U@ in 'Data.Time.Format.formatTime').
export
fromSundayStartWeek:
       Integer -- ^ Year.
    -> Int -- ^ Sunday-starting week number (as @%U@ in 'Data.Time.Format.formatTime').
    -> Int -- ^ Day of week
-- Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
    -> Day
fromSundayStartWeek year w d = let
    -- first day of the year
    firstDay = fromOrdinalDate year 1
    -- 0-based year day of first monday of the year
    zbFirstSunday = (4 - toInteger firstDay) `mod` 7
    -- 0-based week of year
    zbWeek = w - 1
    -- 0-based day of week
    zbDay = d
    -- 0-based day in year
    zbYearDay = zbFirstSunday + 7 * cast zbWeek + cast zbDay
    in addDays zbYearDay firstDay

export
fromSundayStartWeekValid:
  Integer -- ^ Year.
  -> Int -- ^ Sunday-starting week number (as @%U@ in 'Data.Time.Format.formatTime').
  -> Int -- ^ Day of week.
-- Sunday is 0, Saturday is 6 (as @%w@ in 'Data.Time.Format.formatTime').
  -> Maybe Day
fromSundayStartWeekValid year w d = do
    d' <- clipValid 0 6 d
    -- first day of the year
    let firstDay = fromOrdinalDate year 1
    -- 0-based week of year
    let zbFirstSunday = (4 - toInteger firstDay) `mod` 7
    -- 0-based week number
    let zbWeek = w - 1
    -- 0-based day of week
    let zbDay = d'
    -- 0-based day in year
    let zbYearDay = zbFirstSunday + 7 * cast zbWeek + cast zbDay
    zbYearDay' <-
        clipValid
            0
            (if isLeapYear year
                 then 365
                 else 364)
            zbYearDay
    pure $ addDays zbYearDay' firstDay

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub
  abs = Abs

(Integral ty, Neg ty, Eq ty ) => Eq (Expr ty) where
  (==) x y = eval x == eval y

Show ty => Show (Expr ty) where
 show (Val x) = show x
 show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
 show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
 show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
 show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
 show (Abs x) = "|" ++ show x ++ "|"

--https://github.com/idris-lang/Idris-dev/issues/3479
Cast ty ty where
      cast = id

(Integral ty, Neg ty, Cast ty num) => Cast (Expr ty) num where
  cast expr = cast (eval expr)

Functor Expr where
  map func (Val x) = Val (func x)
  map func (Add x y) = Add (map func x) (map func y)
  map func (Sub x y) = Sub (map func x) (map func y)
  map func (Mul x y) = Mul (map func x) (map func y)
  map func (Div x y) = Div (map func x) (map func y)
  map func (Abs x) = Abs (map func x)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


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

(++) : Vect n a -> Vect m a -> Vect (n + m) a
(++) Nil       ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

data Fin : Nat -> Type where
   FZ : Fin (S k)
   FS : Fin k -> Fin (S k)

index : Fin n -> Vect n a -> a
index FZ     (x :: xs) = x
index (FS k) (x :: xs) = index k xs

filter : (a -> Bool) -> Vect n a -> (p ** Vect p a)
filter p Nil = (_ ** [])
filter p (x :: xs)
    = case filter p xs of
           (_ ** xs') => if p x then (_ ** x :: xs')
                                else (_ ** xs')

cons : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons val xs
    = record { fst = S (fst xs),
               snd = (val :: snd xs) } xs

cons' : t -> (x : Nat ** Vect x t) -> (x : Nat ** Vect x t)
cons' val
    = record { fst $= S,
               snd $= (val ::) }

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


text:
module Generics.SOP

import Decidable.Equality

import public Data.List.Elem
import public Data.SOP

%default total

||| Interface for converting a data type from and to
||| its generic representation as a sum of products.
|||
||| Additional Idris coolness: This comes with proofs
||| that `from . to = id` and `to . from = id` and
||| thus, that `t` and `SOP code` are indeed isomorphic.
public export
interface Generic (0 t : Type) (0 code : List $ List Type) | t where
  constructor MkGeneric
  ||| Converts the data type to its generic representation.
  from : (v : t) -> SOP I code

  ||| Converts the generic representation back to the original
  ||| value.
  to   : (v : SOP I code) -> t

  ||| Proof that `to . from = id`.
  fromToId : (v : t) -> to (from v) = v

  ||| Proof that `from . to = id`.
  toFromId : (v : SOP I code) -> from (to v) = v

export
fromInjective : Generic t code =>
                (0 x : t) -> (0 y : t) -> (from x = from y) -> x = y
fromInjective x y prf = rewrite sym $ fromToId y in lemma2
  where lemma1 : to {t = t} (from x) = to {t = t} (from y)
        lemma1 = cong to prf

        lemma2 : x = to {t = t} (from y)
        lemma2 = rewrite sym $ fromToId x in lemma1

public export
0 Code : (t : Type) -> Generic t code => List $ List Type
Code _ = code

||| Tries to extract the arguments of a single constructor
||| from a value's generic representation.
public export
genExtract :  (0 ts : List Type)
           -> (v : t)
           -> Generic t code
           => {auto prf : Elem ts code}
           -> Maybe (NP I ts)
genExtract ts v = extractSOP ts $ from v

||| Tries to extract the value of a single one argument
||| constructor from a value's generic representation.
public export
genExtract1 :  (0 t' : Type)
            -> (v : t)
            -> Generic t code
            => {auto prf : Elem [t'] code}
            -> Maybe t'
genExtract1 t' v = hd <$> genExtract [t'] v

||| Returns all value from a generic enum type
||| (all nullary constructors) wrapped in homogeneous n-ary product.
public export
valuesNP : Generic t code => (et : EnumType code) =>
           NP_ (List Type) (K t) code
valuesNP = hmap (to . MkSOP) (run et)
  where run :  EnumType kss -> NP_ (List k) (K (NS_ (List k) (NP f) kss)) kss
        run EZ     = []
        run (ES x) = Z [] :: mapNP (\ns => S ns) (run x)

||| Returns all value from a generic enum type
||| (all nullary constructors) wrapped in a list.
public export %inline
values : Generic t code => (et : EnumType code) => List t
values = collapseNP valuesNP

||| Like `valuesNP` but takes the erased value type as an
||| explicit argument to help with type inference.
public export %inline
valuesForNP : (0 t: Type) -> Generic t code => (et : EnumType code) =>
              NP_ (List Type) (K t) code
valuesForNP _ = valuesNP

||| Like `values` but takes the erased value type as an
||| explicit argument to help with type inference.
public export %inline
valuesFor : (0 t : Type) -> Generic t code => (et : EnumType code) => List t
valuesFor _ = values

--------------------------------------------------------------------------------
--          Generic Implementation Functions
--------------------------------------------------------------------------------

||| Default `(==)` implementation for data types with a `Generic`
||| instance.
public export
genEq : Generic t code => POP Eq code => t -> t -> Bool
genEq x y = from x == from y

||| Default `compare` implementation for data types with a `Generic`
||| instance.
public export
genCompare : Generic t code => POP Ord code => t -> t -> Ordering
genCompare x y = compare (from x) (from y)

||| Default `decEq` implementation for data types with a `Generic`
||| instance.
public export
genDecEq :  Generic t code => POP DecEq code
         => (x : t) -> (y : t) -> Dec (x = y)
genDecEq x y = case decEq (from x) (from y) of
                    (Yes prf)   => Yes $ fromInjective x y prf
                    (No contra) => No $ \h => contra (cong from h)

||| Default `(<+>)` implementation for data types with a `Generic`
||| instance.
public export
genAppend :  Generic t [ts]
          => POP Semigroup [ts]
          => t -> t -> t
genAppend x y = to $ from x <+> from y

||| Default `neutral` implementation for data types with a `Generic`
||| instance.
public export
genNeutral :  Generic t [ts] => POP Monoid [ts] => t
genNeutral = to neutral

--------------------------------------------------------------------------------
--          Prelude Implementations
--------------------------------------------------------------------------------

-- I wrote the implementations below manually to get a feel for
-- their general structure before starting with deriving
-- them via elaborator reflection.

public export
Generic () [[]] where
  from () = MkSOP $ Z []

  to (MkSOP $ Z []) = ()
  to (MkSOP $ S _) impossible

  fromToId () = Refl

  toFromId (MkSOP $ Z []) = Refl

public export
Generic (a,b) [[a,b]] where
  from (a,b) = MkSOP $ Z [a,b]

  to (MkSOP $ Z [a,b]) = (a,b)
  to (MkSOP $ S _) impossible

  fromToId (a,b) = Refl

  toFromId (MkSOP $ Z [a,b]) = Refl

public export
Generic (LPair a b) [[a,b]] where
  from (a # b) = MkSOP $ Z [a,b]

  to (MkSOP $ Z [a,b]) = (a # b)
  to (MkSOP $ S _) impossible

  fromToId (a # b) = Refl

  toFromId (MkSOP $ Z [a, b]) = Refl

public export
Generic Void [] where
  from v impossible

  to (MkSOP v) impossible

  fromToId v impossible

  toFromId (MkSOP v) impossible

public export
Generic (Stream a) [[a, Inf (Stream a)]] where
  from (h :: t) = MkSOP $ Z [h,t]

  to (MkSOP $ Z [h,t])  = h :: t

  fromToId (h :: t) = Refl

  toFromId (MkSOP $ Z [h,t]) = Refl