text:
-- -------------------------------------------------------------- [ Viewer.idr ]
-- Module    : Viewer.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A Pattern Viewer
module Sif.REPL

import System

import Sif.Types
import Sif.AbsSyntax
import Sif.Pattern
import Sif.Effs
import Sif.Error
import Sif.Library
import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution
import Sif.DSL.Parser
import Sif.DSL
import Sif.Options
import Sif.API

import Sif.Commands

%default partial

-- -------------------------------------------------------------------- [ Effs ]

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

http://www.github.com/jfdm/sif-lang
Type :? for help

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

||| Fetch and parse commands
fetchCMD : Eff SifCMD SifEffs
fetchCMD = do
    putStr "sif-viewer> "
    rawCmd <- getStr
    case parseCMD rawCmd of
      Left err => do
        printLn NoSuchCommand
        fetchCMD
      Right cmd => do
        case getCmdIndex cmd of
          Nothing => pure cmd
          Just n  => do
            lib <- getLibrary
            if n < (length $ patts lib)
              then pure cmd
              else do
               printLn IndexOutOfBounds
               fetchCMD

doCommand : SifCMD -> Eff () SifEffs
doCommand Quit = pure ()
doCommand Help = putStrLn showHelp

doCommand (ShowPattern n fmt fname) = do
  case fname of
    Nothing => do
      putStrLn "Show Pattern"
      getAndPrintPattern n fmt
    Just fn => do
      putStrLn $ "Saving Pattern to " ++ fn ++ " as " ++ show fmt
      printLn FeatureNotImpl

doCommand (ListLib) = do
  putStrLn "Listing Library"
  listLibrary

doCommand (PreludeLoad x) = do
  case x of
    Nothing => loadPrelude
    dirname => do
      updateOptions (\o => record {prelude = dirname} o)
      loadPrelude

doCommand (EvalPattern n) = do
  putStrLn "Eval Pattern"
  getAndEvalPattern n

doCommand (CheckExtPattern p s) = do
  putStrLn "Importing..."
  evalPatternFromFile (Just p) (Just s)

doCommand _ = printLn NoSuchCommand

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

||| A Viewer to view a library of patterns.
export
sifREPL : Eff () SifEffs
sifREPL =
  case banner !(getOptions) of
    True => do
      putStrLn sifBanner
      runREPL
    False => runREPL

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Tensor

-- Based on https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/aplicative.pdf
import src.GenericArity
import Data.Vect
import Data.HVect
import Data.Matrix.Numeric

%access public export

data Tensor : Vect n Nat -> Type -> Type where
  Scalar : a -> Tensor [] a
  Prism : Tensor ns (Vect n a) -> Tensor (n :: ns) a

toVectT : Vect n Nat -> Type -> Type
toVectT [] a = a
toVectT (x :: xs) a = toVectT xs (Vect x a)

toVectT' : Vect n Nat -> Type -> Type
toVectT' [] a = a
toVectT' (x :: xs) a = Vect x (toVectT' xs a)

toTensor : toVectT xs a -> Tensor xs a
toTensor {xs = []} v = Scalar v
toTensor {xs = (x :: xs)} v = Prism (toTensor v)

toVect : Tensor xs a -> toVectT xs a
toVect {xs = []} (Scalar v) = v
toVect {xs = (x :: xs)} (Prism v) = toVect v

finToInt : Fin n -> Int
finToInt FZ     = 0
finToInt (FS k) = 1 + finToInt k

index' : {xs : Vect n Nat} -> HVect (map (\n => Fin n) xs) -> toVectT' xs a -> a
index' {xs = []} [] x = x
index' {xs = (x :: xs)} (fin :: fins) vs = index' fins (Data.Vect.index fin vs)

index : Fin n -> Fin m -> Vect n (Vect m a) -> a
index {n} {m} fn fm xss = index' {xs = [n, m]} [fn, fm] xss

positions' : (n : Nat) -> Vect n (Fin n)
positions' Z = []
positions' (S n) = FZ :: map FS (positions' n)

tabulate' : {xs : Vect n Nat} -> (Arrows n (map (\n => Fin n) xs) a) -> toVectT' xs a
tabulate' {n = Z} {xs = []} x = x
tabulate' {n = S n} {xs = (x :: xs)} f = [tabulate' (f fn) | fn <- positions' x]

tabulate : (Fin n -> a) -> Vect n a
tabulate {n} f = tabulate' {xs = [n]} f

Functor (Tensor ns) where
  map f (Scalar x) = Scalar (f x)
  map f (Prism x) = Prism (map (map f) x)

Foldable (Tensor ns) where
  foldr {ns = []} f acc (Scalar x) = f x acc
  foldr {ns = (n :: ns)} f acc (Prism x) = foldr (\x, acc => foldr f acc x) acc x

Applicative (Tensor ns) where
  pure {ns = []} x = Scalar x
  pure {ns = (n :: ns)} x = Prism (pure (pure x))

  (<*>) {ns = []} (Scalar f) (Scalar x) = Scalar (f x)
  (<*>) {ns = (n :: ns)} (Prism f) (Prism x) = Prism ((<*>) <$> f <*> x)

Traversable (Tensor ns) where
  traverse {ns = []} f (Scalar x) = map Scalar (f x)
  traverse {ns = (n :: ns)} f (Prism x) = map Prism (traverse (traverse f) x)

Show a => Show (Tensor ns a) where
  show (Scalar x) = show x
  show (Prism x) = show x

Num a => Num (Tensor ns a) where
  (+) {ns = []} (Scalar x) (Scalar y) = Scalar (x + y)
  (+) {ns = (n :: ns)} (Prism x) (Prism y) = Prism (x + y)
  (*) {ns = []} (Scalar x) (Scalar y) = Scalar (x * y)
  (*) {ns = (n :: ns)} (Prism x) (Prism y) = Prism (x * y)
  fromInteger {ns = []} i = Scalar (fromInteger i)
  fromInteger {ns = (n :: ns)} i = Prism (fromInteger i)

example : Tensor [2, 2] Int
example = Prism (Prism (Scalar [[1, 2], [3, 4]]))

test : Tensor [2, 2] Int
test = map (\x => x * 2) example

ext: idr

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


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

||| Print pretty models.
module GRL.Pretty

import GRL.Model

%access export

||| Pretty models
prettyModel : GModel -> String
prettyModel g = (foldl (\res,x => show x ++ "\n" ++ res) "" (vertices g)) ++ "\n" ++
                (foldl (\res,x => show x ++ "\n" ++ res) "" (edges g))    ++ "\n"

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
import Aoc
import Data.Fin
import Data.List
import Data.Vect
%default total

data FB = F | B
parseFB : Char -> Maybe FB
parseFB 'F' = Just F
parseFB 'B' = Just B
parseFB _ = Nothing

data LR = L | R
parseLR : Char -> Maybe LR
parseLR 'L' = Just L
parseLR 'R' = Just R
parseLR _ = Nothing

data Seat = MkSeat (Vect 7 FB) (Vect 3 LR)
parseSeat : String -> Maybe Seat
parseSeat s =
  case unpack s of
    [a,b,c,d,e,f,g,x,y,z] =>
      MkSeat <$> traverse parseFB [a,b,c,d,e,f,g]
             <*> traverse parseLR [x,y,z]
    _ => Nothing

interface ToBit a where toBit : a -> Fin 2
ToBit FB where toBit F = 0; toBit B = 1
ToBit LR where toBit L = 0; toBit R = 1

fromBits : (ToBit a, Traversable t) => t a -> Nat
fromBits = foldl (\acc, a => 2*acc + finToNat (toBit a)) 0

seatID : Seat -> Nat
seatID (MkSeat row col) = fromBits {a=FB} row * 8 + fromBits {a=LR} col

||| Given a range [a..b] with one number deleted, find that number.
findGap : List Nat -> Maybe Nat
findGap [] = Nothing
findGap [x] = Nothing
findGap (x::y::xs) =
  -- The totality checker wants this "let", but I don't understand why ;v;
  let rest = findGap (y::xs) in if S x == y then rest else Just (S x)

partial
main : IO ()
main = do
  seats <- parseLines parseSeat
  case map seatID seats of
    [] => putStrLn "no seats!"
    ids@(_::_) => do
      -- ^ This @ pattern helps "foldl1" find a proof that "ids" is non-empty.
      putStr "*   "; printLn (foldl1 max ids)
      putStr "**  "; printLn (findGap $ sort ids)


text:
module Brainfeck.Type

import Data.Vect

%default total

public export
Label : Nat -> Type
Label = Fin

public export
data Token     : Type  where
  TLeft        : Token -- <
  TRight       : Token -- >
  TInc         : Token -- +
  TDec         : Token -- -
  TOut         : Token -- .
  TIn          : Token -- ,
  TJumpForward : Token -- [
  TJumpBack    : Token -- ]

public export
data Operation : Nat -> Type where
  OLeft        : Operation n -- <
  ORight       : Operation n -- >
  OInc         : Operation n -- +
  ODec         : Operation n -- -
  OOut         : Operation n -- .
  OIn          : Operation n -- ,
  OJumpZero    : Label f -> Operation f-- [
  OJumpNZero   : Label b -> Operation b -- ]

export
tokenToS : Token -> String
tokenToS TLeft = "<"
tokenToS TRight = ">"
tokenToS TInc = "+"
tokenToS TDec = "-"
tokenToS TOut = "."
tokenToS TIn = ","
tokenToS TJumpForward = "["
tokenToS TJumpBack = "]"

export
operationToS : Operation f -> String
operationToS OLeft          = "<"
operationToS ORight         = ">"
operationToS OInc           = "+"
operationToS ODec           = "-"
operationToS OOut           = "."
operationToS OIn            = ","
operationToS (OJumpZero  l) = "[ " ++ show (finToNat l)
operationToS (OJumpNZero l) = show (finToNat l) ++ " ]"

public export
data Location : Type where
  Loc : (line : Nat) -> (col : Nat) -> Location

export
locToS : Location -> String
locToS (Loc l c) = "Line: " ++ show l ++ " Column: " ++ show c

public export
Tokens   : Nat -> Type
Tokens n = Vect n (Location, Token)
%name Tokens tokens

-- TODO: Use a better datatype for this (Brainfeck.Instructions.Instructions?)
-- This hasn't been profiled, but it seems trivially true that doing "random" access indexing
-- with ineffecient Fin's is going to cause speed problems
-- Probably wait until its actually an issue first though
public export
Instructions   : Nat -> Type
Instructions n = Vect n (Operation n)
%name Instructions instructions

max_stars_repo_name: jhmcstanton/brainfeck

max_issues_repo_name: jhmcstanton/brainfeck

max_forks_repo_name: jhmcstanton/brainfeck


text:
module Main

import Uri

lul : List String
lul = [
    "https://www.youtube.com/watch?v=YgmFIVOR1-I&list=RD2By3feOVw20&index=9&ab_channel=%E3%81%9A%E3%81%A3%E3%81%A8%E7%9C%9F%E5%A4%9C%E4%B8%AD%E3%81%A7%E3%81%84%E3%81%84%E3%81%AE%E3%81%AB%E3%80%82ZUTOMAYO",
    "ftp://ftp.is.co.za/rfc/rfc1808.txt",
    "gopher://spinaltap.micro.umn.edu/00/Weather/California/Los%20Angeles",
    "http://www.math.uio.no/faq/compression-faq/part1.html",
    "mailto:mduerst@ifi.unizh.ch",
    "news:comp.infosystems.www.servers.unix",
    "telnet://melvyl.ucop.edu/",
    "http://192.168.0:8080",
    "//www.cwi.nl:80/%7Eguido/Python.html",
    "www.cwi.nl/%7Eguido/Python.html",
    "help/Python.html",
    "http://www.cwi.nl/%7Eguido/Python.html",
    "example.com",
    "user:password@example.com:8080",
    "http://user:password@example.com:8080"
]

main : IO ()
main =
    case (traverse decodeURI lul) of
        Right res =>
            for_ res (\x => putStrLn (show res))
        Left err => putStrLn "Err"

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
import System

import Command
import Arith
import Fuel

%default total

mutual
  correct : Stream Int -> (score : Nat) -> ConsoleIO Nat
  correct nums score
    = do PutStr "Correct!\n"
         quiz nums (score + 1)

  wrong : Stream Int -> Int -> (score : Nat) -> ConsoleIO Nat
  wrong nums answer score
    = do PutStr ("Wrong, the answer is " ++ show answer ++ "\n")
         quiz nums score

  quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat
  quiz (num1 :: num2 :: nums) score
    = do PutStr ("Score: " ++ show score ++ "\n")
         PutStr (show num1 ++ " * " ++ show num2 ++ " ")
         answer <- GetLine
         if toLower answer == "quit" then Quit score else
           if (cast answer == num1 * num2)
           then correct nums score
           else wrong nums (num1 * num2) score

partial
main : IO ()
main = do
  seed <- time
  Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)
       | Nothing => putStrLn "Out Of Fuel"
  putStrLn ("Final Score: " ++ show score)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Mmhelloworld.IdrisSpringBoot.Context

import IdrisJvm.IO

%access public export

ConfigurableApplicationContext : Type
ConfigurableApplicationContext = JVM_Native $ Class "org/springframework/context/ConfigurableApplicationContext"

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
-- Code based on the question in the Idris mailing list

import Data.Vect

%default total

public export
group : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect n (Vect m a)
group Z     _ _  = []
group (S n) m xs = let (l, r) = splitAt m xs in l :: group n m r

public export
group' : (n : Nat) -> (m : Nat) -> Vect (n * m) a -> Vect m (Vect n a)
group' n m xs = group m n $ rewrite multCommutative m n in xs

export
splitAtConcatRev : (n : Nat) -> (xs : Vect (n + m) a) -> {0 l : Vect n a} -> {0 r : Vect m a} -> (0 _ : splitAt n xs = (l, r)) -> l ++ r = xs
splitAtConcatRev Z _ Refl = Refl
splitAtConcatRev (S n) (x::xs) {l} prf with (splitAt n xs) proof sprf
  splitAtConcatRev (S n) (x::xs) {l=x::l} Refl | (l, r) = cong (x::) $ splitAtConcatRev n xs sprf

public export
concat_group_id : (n : Nat) -> (m : Nat) -> (v : Vect (n * m) a) -> concat (group n m v) = v
concat_group_id Z     _ [] = Refl
concat_group_id (S n) m xs with (splitAt m xs) proof prf
  _ | (l, r) = rewrite concat_group_id n m r in splitAtConcatRev m xs prf

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module ABMinus

mm : (a, b : Nat) -> a `minus` b = (S a `minus` b) `minus` 1
mm Z     Z     = Refl
mm Z     (S _) = Refl
mm (S a) Z     = Refl
mm (S a) (S b) = rewrite mm a b in Refl

ms : (a, b : Nat) -> a `minus` S b = (a `minus` b) `minus` 1
ms Z     b     = Refl
ms (S _) Z     = Refl
ms (S a) (S b) = rewrite ms a b in Refl

abm : (a, b : Nat) -> a `minus` (b + 1) = (a `minus` b) `minus` 1
abm Z     Z     = Refl
abm (S k) Z     = Refl
abm Z     (S _) = Refl
abm (S a) (S b) = rewrite abm a b in Refl


text:
= The First Tale

> module WhoStoleTheTarts.TheFirstTale
>
> %access  export
> %default total
>
> %hide Prelude.Pairs.DPair.fst

Someone stole the jam. Our job is to figure out who the thief was.

== Suspects

We know it was one of the

- March Hare,

> data MarchHare

- Mad Hatter, or

> data MadHatter

- Dormouse

> data Dormouse

... and that they worked alone.

> SomeoneStoleTheJam : Type
> SomeoneStoleTheJam = Either (    MarchHare, Not MadHatter, Not Dormouse)
>                    $ Either (Not MarchHare,     MadHatter, Not Dormouse)
>                             (Not MarchHare, Not MadHatter,     Dormouse)

== Statements

The March Hare claims,

I never stole the jam!

> MarchHareStatement : (truth : Bool) -> Type
> MarchHareStatement False =     MarchHare
> MarchHareStatement True  = Not MarchHare

According to the Mad Hatter,

One of us stole it, but it wasn't me!

> MadHatterStatement : (truth : Bool) -> Type
> MadHatterStatement False = (    MadHatter, Not    MarchHare, Not Dormouse)
> MadHatterStatement True  = (Not MadHatter, Either MarchHare      Dormouse)

As per the Dormouse,

At least one of them (spoke the truth).

> DormouseStatement : (truth : Bool) -> Type
> DormouseStatement False =     (MarchHareStatement False, MadHatterStatement False)
> DormouseStatement True  = Not (MarchHareStatement False, MadHatterStatement False)

== Revelation

We're also given a revelation:

> Revelation : Type

The March Hare and the Dormouse were not both speaking the truth, i.e. either

- ... the March Hare spoke the truth and the Dormouse did not

> Revelation = Either (MarchHareStatement True,  DormouseStatement False)

- ... or the March Hare did not speak the truth and the Dormouse did.

>                     (MarchHareStatement False, DormouseStatement True)

== Conclusion

Given the [statements](#statements) above and the [revelation](#revelation),

> Thief : SomeoneStoleTheJam -> Revelation

... we can conclude the March Hare stole the jam.

>      -> (MarchHare, Not MadHatter, Not Dormouse)

The first clause is a simple pattern match.

> Thief (Left  marchHare)         _                        = marchHare

From the revelation it follows that if the March Hare spoke the truth,
then the Dormouse lied. If the March Hare spoke the truth, then they
didn't steal the jam. But if the Dormouse lied, then so did the March Hare
and is guilty *BWOC*.

> Thief _                         (Left  (itWas,(them,_))) = absurd (itWas them)

If the March Hare lied, then they stole the jam.

> Thief (Left  (_,did,it))        (Right (marchHare,_))    = (marchHare,did,it)

If we assume the Mad Hatter stole jam and the March Hare lied,
then the March Hare did it *BWOC*.

> Thief (Right (Left  (itWas,_))) (Right (them,_))         = absurd (itWas them)

Assume the Dormouse did it and lied. If the Dormouse lied,
then the March Hare lied, and therefore stole the jam.

> Thief (Right (Right (itWas,_))) (Left  (_,(them,_)))     = absurd (itWas them)

Assume the Dormouse did it and the March Hare lied.
If the March Hare lied then they are guilty.

> Thief (Right (Right (itWas,_))) (Right (them,_))         = absurd (itWas them)

∎

ext: lidr

max_stars_repo_name: yurrriq/alice-in-puzzleland

max_issues_repo_name: yurrriq/alice-in-puzzleland

max_forks_repo_name: yurrriq/alice-in-puzzleland


text:
module Proofs.TranslationInvarianceTheory

import Common.Util
import Specifications.TranslationInvariance
import Proofs.GroupTheory
import Proofs.GroupCancelationLemmas
import Symmetry.Opposite

%default total
%access export

infixl 8 #

composeOrder : {(#) : Binop s} -> {(<=) : Binrel s} ->
  PartiallyOrderedMagmaSpec (#) (<=) -> (a,b,c,d : s) ->
    a <= b -> c <= d -> a # c <= b # d
composeOrder spec a b c d ab cd =
  let pp = translationInvariantR spec a b c ab
      qq = translationInvariantL spec c d b cd
  in transitive (order spec) (a # c) (b # c) (b # d) pp qq

orderInverseL : {(#) : Binop s} -> {(<=) : Binrel s} ->
  PartiallyOrderedGroupSpec (#) e inv (<=) -> (a,b,c : s) ->
    a # c <= b -> c <= inv a # b
orderInverseL spec a b c given = rewrite sym o2 in o1 where
  o1 : inv a # (a # c) <= inv a # b
  o1 = translationInvariantL (invariantOrder spec) (a # c) b _ given
  o2 : inv a # (a # c) = c
  o2 = groupCancel1bis (group spec) a c

orderInverseR : {(#) : Binop s} -> {(<=) : Binrel s} ->
  PartiallyOrderedGroupSpec (#) e inv (<=) -> (a,b,c : s) ->
    a # c <= b -> a <= b # inv c
orderInverseR spec a b c = orderInverseL (opposite spec) c b a

inverseReversesOrder : {(#) : Binop s} ->
  PartiallyOrderedGroupSpec (#) _ inv leq ->
    leq a b -> inv b `leq` inv a
inverseReversesOrder spec {a} {b} given = rewriteRelation leq o3 o4 o2 where
  o1 : inv a # a `leq` inv a # b
  o1 = translationInvariantL (invariantOrder spec) _ _ (inv a) given
  o2 : inv a # a # inv b `leq` inv a # b # inv b
  o2 = translationInvariantR (invariantOrder spec) (inv a # a) (inv a # b) _ o1
  o3 : inv a # a # inv b = inv b
  o3 = groupCancel1 (group spec) a _
  o4 : inv a # b # inv b = inv a
  o4 = groupCancel3bis (group spec) _ b

groupInverseAndOrder : {(#) : Binop s} ->
  PartiallyOrderedGroupSpec (#) e inv leq -> (a,b : s) ->
    a `leq` b -> a # inv b `leq` e
groupInverseAndOrder spec a b given = rewrite sym o2 in o1 where
  o1 : a # inv b `leq` b # inv b
  o1 = translationInvariantR (invariantOrder spec) a b _ given
  o2 : b # inv b = e
  o2 = inverseR (group spec) b

invertNegative : {(<=) : Binrel s} ->
  PartiallyOrderedGroupSpec _ zero neg (<=) -> (a : s) ->
    a <= zero -> zero <= neg a
invertNegative spec a negative = rewrite sym o2 in o1 where
  o1 : neg zero <= neg a
  o1 = inverseReversesOrder spec negative
  o2 : neg zero = zero
  o2 = groupInverseNeutral (group spec)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Lib2

import Data.List as L

D : Type
D = Double

LD : Type
LD = List D

LLD : Type
LLD = List LD

-- default value of base
b : D
b = 0.03

fullNNLayer : LLD -> LLD -> LLD
fullNNLayer [] _ = []
fullNNLayer _ [] = []
fullNNLayer (x::inps) (y::ws) = (softmax $ nnLayer x y ) :: fullNNLayer inps ws

nnLayer : LD -> LD -> LD
nnLayer xs ys = L.zipWith (\x,y => x * y + b) xs ys

softmax : LD -> LD
softmax xs = let softmax_denom = sum $ map exp $ xs
             in foldr (\x, acc => (exp x)/softmax_denom::acc) [] xs

ceLoss : LD -> LD -> LD
ceLoss  [] _ = []
ceLoss  _ [] = []
ceLoss  (x::xs) (y::ys) = -(y/x) + (1-y)/(1-x)::ceLoss xs ys

adam : LD -> LD -> D ->  D -> D -> D -> D -> D -> LD

adam [] _ _ _ _ _ _ _ = []
adam _ [] _ _ _ _ _ _ = []
adam (t::thetas) (gt::gts) alpha m_prev v_prev beta1 beta2 epsilon = do
  let m_current = (beta1 * m_prev + (1-beta1) * gt) /(1-beta1)
      v_current = (beta2 * v_prev + (1-beta2) * (pow gt 2))/ (1-pow beta2 2)
      mhat_current = m_current / (1-beta1)
      vhat_current = v_current / (1-beta2)
  (t - alpha * mhat_current / ((sqrt vhat_current) + epsilon)) :: adam thetas gts alpha m_current v_current beta1 beta2 epsilon

optimizer : (LD -> LD -> D -> D -> D -> D ->D -> D -> LD) ->
            LLD -> LLD -> D -> D -> D -> D -> D -> D -> LLD

optimizer f [] _ _ _ _ _ _ _ = []
optimizer f _ [] _ _ _ _ _ _ = []
optimizer f (ws::wss) (cs::costs) alpha m v beta1 beta2 epsilon =
  (f ws cs alpha m v beta1 beta2 epsilon) :: optimizer f wss costs alpha m v beta1 beta2 epsilon

record LossFx where
  constructor CreateFx
  fx : LD -> LD -> LD
--  preds, targets : LLD

record Optimizer {a : D} where
  constructor OptimFx
  fx : LD -> LD -> D -> D -> D -> D -> D -> D -> LD
  weights , costs : LLD
  alpha, m, v, beta1, beta2, epsilon : D

record Model where
  constructor Create
  weights, inputs, targets : LLD
  alpha, beta1, beta2, epsilon : D
  iter : Int

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Postgres.Data.Conn

||| Internal phantom type used to mark pointers related to
||| DB connections.
export
data PGconn : Type

public export
data Conn : Type where
  MkConn : Ptr PGconn -> Conn

%name Conn conn

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
import Data.Binary
import Data.Binary.Digit
import Data.List
import Data.Nat
import Data.String
import Data.String.Parser
import Data.Vect

import System.File

shexMap : List (Char, String)
shexMap = [
  ('0', "0000"),
  ('1', "0001"),
  ('2', "0010"),
  ('3', "0011"),
  ('4', "0100"),
  ('5', "0101"),
  ('6', "0110"),
  ('7', "0111"),
  ('8', "1000"),
  ('9', "1001"),
  ('A', "1010"),
  ('B', "1011"),
  ('C', "1100"),
  ('D', "1101"),
  ('E', "1110"),
  ('F', "1111")
  ]

Input : Type
Input = Bin

binToNat : Vect n Digit -> Nat
binToNat = toNat . reverse . toList

digitParser : Parser Digit
digitParser = char '0' $> O <|> char '1' $> I

numParser : Nat -> Parser Nat
numParser n = binToNat <$> ntimes n digitParser

litParser : Parser Bin
litParser = do d <- digitParser
               case d of
                    O => toList <$> ntimes 4 digitParser
                    I => do b <- toList <$> ntimes 4 digitParser
                            ((++) b) <$> litParser

doExp : Nat -> List Nat -> Maybe Nat
doExp 0 l = pure $ foldl (+) 0 l
doExp 1 l = pure $ foldl (*) 1 l
doExp 2 (x :: xs) = pure $ foldl min x xs
doExp 3 (x :: xs) = pure $ foldl max x xs
doExp 5 (x :: y :: []) = pure $ if x > y then 1 else 0
doExp 6 (x :: y :: []) = pure $ if x < y then 1 else 0
doExp 7 (x :: y :: []) = pure $ if x == y then 1 else 0
doExp _ _ = Nothing

expParser : Parser Nat
expParser = do version <- numParser 3
               type <- numParser 3
               if type == 4
                  then do lit <- toNat . reverse <$> litParser
                          pure $ lit
                  else do ltype <- numParser 1
                          if ltype == 1
                             then do num <- numParser 11
                                     vs <- ntimes num expParser
                                     maybe (fail "Unknown op") pure $ doExp type $ toList vs
                             else do len <- numParser 15
                                     sub <- pack . toList <$> ntimes len alphaNum
                                     Right (vs, _) <- pure $ parse (some expParser) sub
                                       | Left err => fail err
                                     maybe (fail "Unknown op") pure $ doExp type $ toList vs

part2 : String -> IO String
part2 a = do Right (v, _) <- pure $ parse expParser a
               | Left err => pure err
             pure $ show v
main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          let a = fastAppend $ catMaybes $ (flip lookup $ shexMap) <$> unpack input
          part2 a >>= putStrLn


text:
module Compiler.Optimize

import Control.Monad.State
import Data.List
import Data.String
import System
import System.File

import Compiler.Common
import Compiler.VMCode
import Core.Directory
import Core.CompileExpr
import Core.Name
import Libraries.Data.SortedMap
import Libraries.Utils.Path

record OptInfo where
  constructor MkOptInfo
  funcUsageCounter : Bool
  allFuncs : SortedMap Name VMDef

record TransformSt where
  constructor MkTransformSt
  nextLoc : Int
  instructions : List VMInst

Transform : Type -> Type
Transform = Control.Monad.State.State TransformSt

addInstructon : VMInst -> Transform ()
addInstructon i = modify (record { instructions $= (i ::)})

gatherInfo : List (Name, VMDef) -> OptInfo
gatherInfo defs = MkOptInfo True (fromList defs)

nextFreeLoc : Int -> List VMInst -> Int
nextFreeLoc i [] = i
nextFreeLoc i (DECLARE (Loc x)::rest) = nextFreeLoc (max i (x+1)) rest
nextFreeLoc i (START::_) = i
nextFreeLoc i (_::rest) = nextFreeLoc i rest

renumber : (off : Int) -> Reg -> Reg
renumber _ Discard = Discard
renumber off RVal = Loc off
renumber off (Loc n) = Loc (off + n + 1)

renumberInst : Int -> VMInst -> VMInst
renumberInst off (APPLY r f a) = APPLY (renumber off r) (renumber off f) (renumber off a)
renumberInst off (ASSIGN r src) = ASSIGN (renumber off r) (renumber off src)

renumberInst off START = START
renumberInst off x = ERROR $ "renumber not impl:" ++ show x

parameters (info : OptInfo)
  inlinable : Name -> Bool
  inlinable (NS _ (CaseBlock _ _)) = True
  inlinable n = False

  inlineFunc : Reg -> Name -> List Reg -> Transform ()
  inlineFunc r n args = do
    case lookup n info.allFuncs of
         (Just (MkVMFun iargs iis)) => do
           argShift <- (.nextLoc) <$> get
           let newVarCount = nextFreeLoc (cast $ length iargs) iis
           modify (record { nextLoc $= (newVarCount +)})
           let renumberedRval = (Loc argShift)
           let renumberedArgs = map (renumber argShift . Loc) iargs

           -- RVal from inlined function:
           addInstructon (DECLARE renumberedRval)
           -- function args:
           for_ renumberedArgs (\arg => addInstructon (DECLARE arg))

           for_ (zip renumberedArgs args) (\(t, f) => addInstructon (ASSIGN (t) (f)))
           for_ iis (\ins => addInstructon $ renumberInst argShift ins)
           --addInstructon (CALL r False n args)
           addInstructon (ASSIGN r renumberedRval)
           pure ()
         _ => addInstructon (CALL r False n args)

  doTransform : Name -> List Int -> VMInst -> Transform ()
  doTransform n args i = do
    case i of
         (CALL r tailpos fn args) => if inlinable n then inlineFunc r fn args else addInstructon i
         i => addInstructon i

  transformFun : Name -> List Int -> List VMInst -> VMDef
  transformFun n args is = MkVMFun args is

  transformDef : (Name, VMDef) -> (Name, VMDef)
  transformDef (n, (MkVMFun args is)) =
    let finSt = fst $ runState (MkTransformSt (nextFreeLoc (cast $ length args) is) []) (traverse_ (doTransform n args) is) in
    (n, MkVMFun args (reverse $ finSt.instructions))
  transformDef x = x

export
optimize : List (Name, VMDef) -> List (Name, VMDef)
optimize defs = let info = gatherInfo defs in
                    map (transformDef info) defs

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
record R (a : Type) where
  constructor MkR
  x : a

rmap : (a -> b) -> R a -> R b
rmap f = { x $= f }


text:
import Data.So

isLeap : Integer -> Bool
isLeap year = (mod year 400 == 0) ||
              ((mod year 4 == 0) && not (mod year 100 == 0))

numberOfDays : Integer -> Integer -> Integer
numberOfDays year 2 = if isLeap year then 29 else 28
numberOfDays _ 9 = 30
numberOfDays _ 4 = 30
numberOfDays _ 6 = 30
numberOfDays _ 11 = 30
numberOfDays _ _ = 31

validDate : Integer -> Integer -> Integer -> Bool
validDate year month day = (day >= 1) && (day <= numberOfDays year month) &&
                           (month >= 1) && (month <= 12)

data Date : Integer -> Integer -> Integer -> Type where
    makeDate : (y:Integer) -> (m:Integer) -> (d:Integer) -> So (validDate y m d) -> Date y m d

dateFromUnsafeInput : (y:Integer) -> (m:Integer) -> (d:Integer) -> Maybe (Date y m d)
dateFromUnsafeInput y m d = case choose (validDate y m d) of
                                 Left valid => Just (makeDate y m d valid)
                                 Right _ => Nothing

max_stars_repo_name: dkandalov/katas

max_issues_repo_name: dkandalov/katas

max_forks_repo_name: dkandalov/katas


text:
module Compile

import Syntax
import Machine

export
compile : Expr -> List Instr
compile (Var nm) = [IVar nm]
compile (EInt i) = [IInt i]
compile (EBool b) = [IBool b]
compile (Times e1 e2) = compile e1 ++ compile e2 ++ [IMult]
compile (Plus e1 e2) = compile e1 ++ compile e2 ++ [IAdd]
compile (Minus e1 e2) = compile e1 ++ compile e2 ++ [ISub]
compile (Equal e1 e2) = compile e1 ++ compile e2 ++ [IEqual]
compile (Less e1 e2) = compile e1 ++ compile e2 ++ [ILess]
compile (If e1 e2 e3) = compile e1 ++ [IBranch (compile e2) (compile e3)]
compile (Fun fnm nm _ _ body) = [IClosure fnm nm (compile body ++ [IPopEnv])]
compile (Apply e1 e2) = (compile e1) ++ (compile e2) ++ [ICall]

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module Text.CSS

import public Text.CSS.Color
import public Text.CSS.Dir
import public Text.CSS.Declaration
import public Text.CSS.Flexbox
import public Text.CSS.Grid
import public Text.CSS.Length
import public Text.CSS.ListStyleType
import public Text.CSS.Percentage
import public Text.CSS.Property
import public Text.CSS.Render
import public Text.CSS.Rule
import public Text.CSS.Selector


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

export
mapEither : (a -> Either e b) -> List a -> Either e (List b)
mapEither f Nil     = pure Nil
mapEither f (x::xs) = do
  x'  <- f x
  xs' <- mapEither f xs
  pure (x' :: xs')

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

max_stars_repo_name: jfdm/freyja-schema

max_issues_repo_name: jfdm/freyja-schema

max_forks_repo_name: jfdm/freyja-schema


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

import Data.Vect

-- check that all functions are total
%default total

--
-- section 4.1
-- see BSTree.idr
-- see Expr.idr
-- see Shape.idr
--

--
-- section 4.2
-- see Vehicle.idr
--

-- first version, does not output the same error than in the book
-- > vectTake1 3 [1,2,3,4,5,6,7]
-- [1, 2, 3] : Vect 3 Integer
-- > vectTake1 8 [1,2,3,4,5,6,7]
-- (input):1:11:When checking argument prf to function Data.Fin.fromInteger:
--         When using 8 as a literal for a Fin 8
--                 8 is not strictly less than 8
vectTake1 : (q : Fin (S n)) -> Vect n t -> Vect (finToNat q) t
vectTake1 FZ _ = []
vectTake1 (FS x) [] impossible
vectTake1 (FS x) (y :: ys) = y :: vectTake1 x ys

-- second version
-- > vectTake2 3 [1,2,3,4,5,6,7]
-- [1, 2, 3] : Vect 3 Integer
-- > vectTake2 8 [1,2,3,4,5,6,7]
-- (input):1:14:When checking argument xs to constructor Data.Vect.:::
--         Type mismatch between
--                 Vect 0 elem (Type of [])
--         and
--                 Vect (S k) t (Expected type)
--
--         Specifically:
--                 Type mismatch between
--                         0
--                 and
--                         S k
vectTake2 : (q : Nat) -> Vect (q+k) t -> Vect q t
vectTake2 Z _ = []
vectTake2 (S k) (x :: xs) = x :: vectTake2 k xs

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

--
-- section 4.3
-- see DataStore.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Example.Qtt.Range

import Data.Vect

fromMaybe' : a -> (1 _ : Maybe a) -> a
fromMaybe' _ (Just x) = x
fromMaybe' d Nothing  = d

f : a -> Vect n (Maybe a) -> Vect n a
f x = map (\y => fromMaybe' x y)

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
-- SPDX-FileCopyrightText: 2021 The test-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Tester.Runner

import Tester
import Data.List

import Control.ANSI
import Control.Monad.Either

||| Run the set of tests in `tests` and print out the test result.
|||
||| If a test failed the fail-message will be displayed.
|||
||| @ tests The tests to run
export
runTests : (tests : List Test) -> IO Bool
runTests tests = do
    let longestDesc = foldl (\acc,t => max acc (length t.description)) 0 tests
    let padding = \len =>
            let diff = longestDesc `minus` len
            in pack $ replicate diff ' '

    res <- for tests $ \t => do
        putStr $ t.description ++ padding (length t.description) ++ " ... "
        case !(runEitherT t.run) of
            Left err => do

                printLn $ colored Red "failed"
                putStrLn err
                pure False
            Right () => do
                printLn $ colored Green "passed"
                pure True
    pure $ all (==True) res

max_stars_repo_name: tiatomee/tester-idr

max_issues_repo_name: tiatomee/tester-idr

max_forks_repo_name: tiatomee/tester-idr


text:
module Algebraic

-- Example functions

or : Bool -> Bool -> Bool
or p q = p || q

xor : Bool -> Bool -> Bool
xor p q = (p || q) && not (p && q)

-- Idempotency

Idempotent : (a -> a) -> a -> Type
Idempotent f a = f (f a) = f a

-- Involution

notNotTrue : not (not True) = True
notNotTrue = Refl

notNotFalse : not (not False) = False
notNotFalse = Refl

notNot : (b : Bool) -> not (not b) = b
notNot False = Refl
notNot True = Refl

Involution : (a -> a) -> a -> Type
Involution f a = f (f a) = a

xorInvolution : (a : Bool) -> (b : Bool) -> xor a (xor a b) = b
xorInvolution False False = Refl
xorInvolution False True = Refl
xorInvolution True False = Refl
xorInvolution True True = Refl

-- Uninhabited

notNotIdempotent : (b : Bool) -> Idempotent not b -> Void
notNotIdempotent False Refl impossible
notNotIdempotent True Refl impossible

succNotIdempotent : (n : Nat) -> Idempotent S n -> Void
succNotIdempotent Z Refl impossible
succNotIdempotent (S k) prf =
  succNotIdempotent k (succInjective (S (S k)) (S k) prf)

-- Both

idempotentInvolution : Idempotent f a -> Involution f a -> f a = a
idempotentInvolution idem invo = ?idempotentInvolution

---------- Proofs ----------

Algebraic.idempotentInvolution1 = proof
  intros
  rewrite idem
  rewrite sym invo
  trivial


text:
t1 : Bits8
t1 = 2

t2 : Bits8
t2 = 255

t3 : Bits8
t3 = 100

tests8 : List String
tests8 = map show [t1 + t2,
                   t1 * t3,
                   the Bits8 (fromInteger (-8)),
                   the Bits8 257,
                   the Bits8 (fromInteger (-1)),
                   prim__shl_Bits8 t3 1,
                   prim__shl_Bits8 t2 1]

testsCmp : List String
testsCmp = map show [t1 < t2, t3 < (t2 + t1)]

testsMax : List String
testsMax = [show (the Bits8 (fromInteger (-1))),
            show (the Bits16 (fromInteger (-1))),
            show (the Bits32 (fromInteger (-1))),
            show (the Bits64 (fromInteger (-1)))]

main : IO ()
main
    = do printLn (t1 + t2)
         printLn (t1 * t3)
         printLn (t1 < t2)
         printLn (prim__shl_Bits8 t3 1)
         printLn (prim__shl_Bits8 t2 1)
         printLn (t3 < (t2 + t1))
         printLn (the Bits8 (fromInteger (-8)))
         printLn (the Bits8 257)
         printLn (the Bits64 1234567890)
         printLn (the Bits8 (fromInteger (-1)))
         printLn (the Bits16 (fromInteger (-1)))
         printLn (the Bits32 (fromInteger (-1)))
         printLn (the Bits64 (fromInteger (-1)))


text:
module Language.Elab.Types

import Language.Elab.Syntax

import Language.Reflection

import Util

%language ElabReflection

-- Helper types for deriving more cleanly

-- A argument to a constructor along with additional relation data like whether it's an index of the type
public export
record ArgInfo where
  constructor MkArgInfo
  count  : Count
  piInfo : PiInfo TTImp
  name   : Name
  type   : TTImp
  isIndex : Bool -- as in not a parameter
  -- An index has its name in the return type and is not a basic %type
  -- Nat is an index in MkFoo : Foo a Z
  -- (n : Nat) is an index in Foo a n
  --------------
  -- meta : Maybe MetaArgInfo
  -- position : Nat
  -- Do I need the position if I can establish it's an index anyway?

export
Show ArgInfo where
  show (MkArgInfo count piInfo name type ind)
    = "MkArgInfo " ++ show count ++ " " ++ show piInfo ++ " " ++ showPrec App name ++ " " ++ "tyttimp " ++ show ind

export
logArgInfo : Nat -> ArgInfo -> Elab ()
logArgInfo n (MkArgInfo count piInfo name type isIndex) = do
  logMsg "logArgInfo" n $ "MkArgInfo " ++ show count ++ " " ++ show piInfo ++ " " ++ showPrec App name
  logTerm "logArgInfo" n "argimp: " type

-- Fully qualified Name
-- `type` is our fully applied type, e.g. given args a,b,c: Foo a b c
public export
record Constructor where
  constructor MkConstructor
  name : Name
  args : List ArgInfo
  type : TTImp

-- Fully qualified Name
-- `type` is our fully applied type, e.g. given args a,b,c: Foo a b c
public export
record TypeInfo where
  constructor MkTypeInfo
  name : Name
  args : List ArgInfo
  cons : List Constructor
  type : TTImp

-- This seems to be fairly slow, not sure why
infix 8 `indexOf`
private
total
indexOf : Name -> TTImp -> Bool
indexOf n1 (IVar _ n2) = n1 == n2
indexOf l (IApp _ z w) = indexOf l z || indexOf l w
indexOf _ _ = False

-- workhorse of the module, though you'll tend to use it through makeTypeInfo
-- If an argument doesn't have a name we generate one for it, this simplifies
-- use of names. That being said idris (with PR 337) should have already
-- generated names for everything so this shouldn't come up often.
-- TODO: revisit this decision
export
getConType : Name -> Elab (List ArgInfo, TTImp)
getConType qn = go (snd !(lookupName qn))
  where
    go : TTImp -> Elab (List ArgInfo, TTImp)
    go (IPi _ c i n0 argTy retTy0) = do
      (xs,retTy1) <- go retTy0
      let n1 = maybe !(genSym "arg") id n0
      logMsg "getConType" 1 "compute"
      let b = maybe False (`indexOf`retTy1) n0
      pure $ (MkArgInfo c i n1 argTy b :: xs, retTy1)
    go retTy = pure ([],retTy)

-- makes them unique for now
export
genArgs : Name -> Elab (List ArgInfo)
genArgs qn = do (_,tyimp) <- lookupName qn
                go tyimp
  where
    go : TTImp -> Elab (List ArgInfo)
    go (IPi _ c i n argTy retTy)
      = let isIndex = not (isType argTy) -- && isExplicitPi i
        in [| pure (MkArgInfo c i !(readableGenSym "arg") argTy isIndex) :: go retTy |]
    go _ = pure []

-- TODO try making this explicitly to reduce quoting
-- Takes String so that you can process the names as you like
-- NB: Likely to change
export
appTyCon : List String -> Name -> TTImp
appTyCon ns n = foldl (\tt,v => `( ~(tt) ~(iBindVar v) )) (iVar n) ns

export
pullExplicits : TypeInfo -> List ArgInfo
pullExplicits x = filter (isExplicitPi . piInfo) (args x)

export
pullImplicits : TypeInfo -> List ArgInfo
pullImplicits x = filter (isImplicitPi . piInfo) (args x)

argnam : ArgInfo -> Name
argnam (MkArgInfo count piInfo name type isIndex) = name

-- not bad start, we might try not renaming here, make names at use-site?
export
makeTypeInfo : Name -> Elab TypeInfo
makeTypeInfo n = do
  logMsg "makeTypeInfo" 1 "bado"
  (tyname,tyimp) <- lookupName n
  args <- genArgs n
  connames <- getCons tyname
  conlist <- traverse getConType connames
  logMsg "makeTypeInfo" 1 "I'm being computed"
  let tyargs = filter (isExplicitPi . piInfo) args
      ty = appTyCon (map (\arg => extractNameStr  arg.name) tyargs) tyname
  pure $ MkTypeInfo tyname args
           (zipWith (\x,(y,z) => MkConstructor x y z) connames conlist) ty

-----------------------------
-- Testing Area
-----------------------------
-- {-
data MyNat' : Type where
  MZ' : MyNat'
  MS' : MyNat' -> MyNat'

-- Time making this is directly related to arg count
data Foo6'' : Type -> Type -> Type -> Nat -> Type where
  Zor6'' : a -> b -> Foo6'' a b c Z
  Gor6'' : b -> Foo6'' a b c (S k)
  Nor6A'' : a -> b -> c -> c -> c -> c -> (n : Nat) -> Foo6'' a b c n
  Nor6B'' : a -> (0 _ : b) -> c -> Foo6'' a b c n -- NB: 0 Use arg
  Bor6'' : Foo6'' a b c n
  Wah6'' : a -> (n : Nat) -> Foo6'' a b c n

{-
-- I need a minimal example of reflected OrderedSet failing
-}


text:
module lib.Library

import lib.sublib.Sublibrary

export
salute : String
salute = salutation ++ ", dependencies example of idris"


text:
-- -------------------------------------------------------------- [ Ranges.idr ]
||| Module    : Ranges.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
|||
module Commons.Data.Ranged

import Data.So

%access export
%default total

namespace Int

  data IntRange : (l,u : Int)
               -> (prf : So (l < u))
               -> Type where
    MkIntRange : (l,u : Int) -> (prf : So (l < u)) -> IntRange l u prf

  mkIntRange : (l,u : Int)
         -> {auto prf : So (l < u)}
         -> IntRange l u prf
  mkIntRange l u {prf} = MkIntRange l u prf

  data RangedInt : (lower : Int)
                -> (upper : Int)
                -> Type
    where
      MkRangedInt : (x     : Int)
                 -> (range : IntRange l u vrange)
                 -> (prf   : So (l <= x && x <= u))
                 -> RangedInt l u

  getValue : RangedInt l u -> Int
  getValue (MkRangedInt x _ _) = x

  getRange : RangedInt l u -> (Int, Int)
  getRange (MkRangedInt _ (MkIntRange l u _) _) = (l, u)

  inRange : (x : Int)
         -> (range : IntRange l u prf)
         -> Maybe (RangedInt l u)
  inRange x range with (choose $ l <= x && x <= u)
    inRange x range | (Left  okay) = Just $ MkRangedInt x range okay
    inRange x range | (Right nout) = Nothing

  Show (IntRange l u prf) where
    show (MkIntRange l u _) = unwords ["(", show l, ",", show u, ")"]

  Show (RangedInt l u) where
    show (MkRangedInt x (MkIntRange l u _) _) = unwords ["(", show l, "<=", show x, "<=", show u, ")"]

namespace Nat

  data NatRange : (l,u : Nat)
               -> (prf : LT l u)
               -> Type
    where
      MkNatRange : (l,u : Nat) -> (prf : LT l u) -> NatRange l u prf

  mkNatRange : (l,u : Nat) -> {auto prf : LT l u} -> NatRange l u prf
  mkNatRange l u {prf} = MkNatRange l u prf

  data RangedNat : (lower : Nat)
                -> (upper : Nat)
                -> Type where
    MkRangedNat : (x : Nat)
               -> (range : NatRange l u prfRange)
               -> (prfLower : LTE l x)
               -> (prfUpper : LTE x u)
               -> RangedNat l u

  getValue : RangedNat l u -> Nat
  getValue (MkRangedNat x _ _ _) = x

  getRange : RangedNat l u -> (Nat, Nat)
  getRange (MkRangedNat _ (MkNatRange l u _) _ _) = (l, u)

  inRange : (x : Nat)
         -> (range : NatRange l u prf)
         -> Maybe $ RangedNat l u
  inRange x (MkNatRange l u prf) with (isLTE l x)
    inRange x (MkNatRange l u prf) | (Yes y) with (isLTE x u)
      inRange x (MkNatRange l u prf) | (Yes y) | (Yes z) = Just (MkRangedNat x (MkNatRange l u prf) y z)
      inRange x (MkNatRange l u prf) | (Yes y) | (No contra) = Nothing
    inRange x (MkNatRange l u prf) | (No contra) = Nothing

  Show (NatRange l u prf) where
    show (MkNatRange l u prf) = unwords ["(", show l, ",", show u, ")"]

  Show (RangedNat l u) where
    show (MkRangedNat x (MkNatRange l u prf) _ _) = unwords ["(", show l, "<=", show x, "<=", show u, ")"]

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Data.List

import Data.Nat
import Data.List1

public export
isNil : List a -> Bool
isNil [] = True
isNil _  = False

public export
isCons : List a -> Bool
isCons [] = False
isCons _  = True

public export
snoc : List a -> a -> List a
snoc xs x = xs ++ [x]

public export
take : Nat -> List a -> List a
take (S k) (x :: xs) = x :: take k xs
take _ _ = []

public export
drop : (n : Nat) -> (xs : List a) -> List a
drop Z     xs      = xs
drop (S n) []      = []
drop (S n) (_::xs) = drop n xs

||| Satisfiable if `k` is a valid index into `xs`
|||
||| @ k the potential index
||| @ xs the list into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : List a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : InBounds Z (x :: xs)
    ||| Valid indices can be extended
    InLater : InBounds k xs -> InBounds (S k) (x :: xs)

public export
Uninhabited (InBounds k []) where
    uninhabited InFirst impossible
    uninhabited (InLater _) impossible

||| Decide whether `k` is a valid index into `xs`
public export
inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
inBounds _ [] = No uninhabited
inBounds Z (_ :: _) = Yes InFirst
inBounds (S k) (x :: xs) with (inBounds k xs)
  inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
  inBounds (S k) (x :: xs) | (No contra)
      = No $ \(InLater y) => contra y

||| Find a particular element of a list.
|||
||| @ ok a proof that the index is within bounds
public export
index : (n : Nat) -> (xs : List a) -> {auto ok : InBounds n xs} -> a
index Z (x :: xs) {ok = InFirst} = x
index (S k) (_ :: xs) {ok = InLater _} = index k xs

||| Generate a list by repeatedly applying a partial function until exhausted.
||| @ f the function to iterate
||| @ x the initial value that will be the head of the list
public export
iterate : (f : a -> Maybe a) -> (x : a) -> List a
iterate f x  = x :: case f x of
  Nothing => []
  Just y => iterate f y

public export
takeWhile : (p : a -> Bool) -> List a -> List a
takeWhile p []      = []
takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

public export
dropWhile : (p : a -> Bool) -> List a -> List a
dropWhile p []      = []
dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

public export
filter : (p : a -> Bool) -> List a -> List a
filter p [] = []
filter p (x :: xs)
   = if p x
        then x :: filter p xs
        else filter p xs

||| Find the first element of the list that satisfies the predicate.
public export
find : (p : a -> Bool) -> (xs : List a) -> Maybe a
find p [] = Nothing
find p (x::xs) = if p x then Just x else find p xs

||| Find associated information in a list using a custom comparison.
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e []      = Nothing
lookupBy p e ((l, r) :: xs) =
  if p e l then
    Just r
  else
    lookupBy p e xs

||| Find associated information in a list using Boolean equality.
public export
lookup : Eq a => a -> List (a, b) -> Maybe b
lookup = lookupBy (==)

||| Check if something is a member of a list using a custom comparison.
public export
elemBy : (a -> a -> Bool) -> a -> List a -> Bool
elemBy p e []      = False
elemBy p e (x::xs) = p e x || elemBy p e xs

public export
nubBy : (a -> a -> Bool) -> List a -> List a
nubBy = nubBy' []
  where
    nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
    nubBy' acc p []      = []
    nubBy' acc p (x::xs) =
      if elemBy p x acc then
        nubBy' acc p xs
      else
        x :: nubBy' (x::acc) p xs

||| O(n^2). The nub function removes duplicate elements from a list. In
||| particular, it keeps only the first occurrence of each element. It is a
||| special case of nubBy, which allows the programmer to supply their own
||| equality test.
|||
||| ```idris example
||| nub (the (List _) [1,2,1,3])
||| ```
public export
nub : Eq a => List a -> List a
nub = nubBy (==)

||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
public export
deleteBy : (a -> a -> Bool) -> a -> List a -> List a
deleteBy _  _ []      = []
deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

||| `delete x` removes the first occurrence of `x` from its list argument. For
||| example,
|||
|||````idris example
|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
|||````
|||
||| It is a special case of deleteBy, which allows the programmer to supply
||| their own equality test.
public export
delete : Eq a => a -> List a -> List a
delete = deleteBy (==)

||| The unionBy function returns the union of two lists by user-supplied equality predicate.
public export
unionBy : (a -> a -> Bool) -> List a -> List a -> List a
unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

||| Compute the union of two lists according to their `Eq` implementation.
|||
||| ```idris example
||| union ['d', 'o', 'g'] ['c', 'o', 'w']
||| ```
|||
public export
union : Eq a => List a -> List a -> List a
union = unionBy (==)

public export
span : (a -> Bool) -> List a -> (List a, List a)
span p []      = ([], [])
span p (x::xs) =
  if p x then
    let (ys, zs) = span p xs in
      (x::ys, zs)
  else
    ([], x::xs)

public export
break : (a -> Bool) -> List a -> (List a, List a)
break p xs = span (not . p) xs

public export
split : (a -> Bool) -> List a -> List1 (List a)
split p xs =
  case break p xs of
    (chunk, [])          => singleton chunk
    (chunk, (c :: rest)) => cons chunk (split p (assert_smaller xs rest))

public export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
splitAt Z xs = ([], xs)
splitAt (S k) [] = ([], [])
splitAt (S k) (x :: xs)
      = let (tk, dr) = splitAt k xs in
            (x :: tk, dr)

public export
partition : (a -> Bool) -> List a -> (List a, List a)
partition p []      = ([], [])
partition p (x::xs) =
  let (lefts, rights) = partition p xs in
    if p x then
      (x::lefts, rights)
    else
      (lefts, x::rights)

||| The inits function returns all initial segments of the argument, shortest
||| first. For example,
|||
||| ```idris example
||| inits [1,2,3]
||| ```
public export
inits : List a -> List (List a)
inits xs = [] :: case xs of
  []        => []
  x :: xs'  => map (x ::) (inits xs')

||| The tails function returns all final segments of the argument, longest
||| first. For example,
|||
||| ```idris example
||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
|||```
public export
tails : List a -> List (List a)
tails xs = xs :: case xs of
  []        => []
  _ :: xs'  => tails xs'

||| Split on the given element.
|||
||| ```idris example
||| splitOn 0 [1,0,2,0,0,3]
||| ```
|||
public export
splitOn : Eq a => a -> List a -> List1 (List a)
splitOn a = split (== a)

||| Replaces all occurences of the first argument with the second argument in a list.
|||
||| ```idris example
||| replaceOn '-' ',' ['1', '-', '2', '-', '3']
||| ```
|||
public export
replaceOn : Eq a => a -> a -> List a -> List a
replaceOn a b l = map (\c => if c == a then b else c) l

public export
reverseOnto : List a -> List a -> List a
reverseOnto acc [] = acc
reverseOnto acc (x::xs) = reverseOnto (x::acc) xs

public export
reverse : List a -> List a
reverse = reverseOnto []

||| Construct a list with `n` copies of `x`.
||| @ n how many copies
||| @ x the element to replicate
public export
replicate : (n : Nat) -> (x : a) -> List a
replicate Z     _ = []
replicate (S n) x = x :: replicate n x

||| Compute the intersect of two lists by user-supplied equality predicate.
export
intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]

||| Compute the intersect of two lists according to the `Eq` implementation for the elements.
export
intersect : Eq a => List a -> List a -> List a
intersect = intersectBy (==)

export
intersectAllBy : (a -> a -> Bool) -> List (List a) -> List a
intersectAllBy eq [] = []
intersectAllBy eq (xs :: xss) = filter (\x => all (elemBy eq x) xss) xs

export
intersectAll : Eq a => List (List a) -> List a
intersectAll = intersectAllBy (==)

||| Combine two lists elementwise using some function.
|||
||| If the lists are different lengths, the result is truncated to the
||| length of the shortest list.
export
zipWith : (a -> b -> c) -> List a -> List b -> List c
zipWith _ [] _ = []
zipWith _ _ [] = []
zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

||| Combine two lists elementwise into pairs.
|||
||| If the lists are different lengths, the result is truncated to the
||| length of the shortest list.
export
zip : List a -> List b -> List (a, b)
zip = zipWith \x, y => (x, y)

export
zipWith3 : (a -> b -> c -> d) -> List a -> List b -> List c -> List d
zipWith3 _ [] _ _ = []
zipWith3 _ _ [] _ = []
zipWith3 _ _ _ [] = []
zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

||| Combine three lists elementwise into tuples.
|||
||| If the lists are different lengths, the result is truncated to the
||| length of the shortest list.
export
zip3 : List a -> List b -> List c -> List (a, b, c)
zip3 = zipWith3 \x, y, z => (x, y, z)

public export
data NonEmpty : (xs : List a) -> Type where
    IsNonEmpty : NonEmpty (x :: xs)

export
Uninhabited (NonEmpty []) where
  uninhabited IsNonEmpty impossible

||| Get the head of a non-empty list.
||| @ ok proof the list is non-empty
public export
head : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
head [] impossible
head (x :: _) = x

||| Get the tail of a non-empty list.
||| @ ok proof the list is non-empty
public export
tail : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
tail [] impossible
tail (_ :: xs) = xs

||| Retrieve the last element of a non-empty list.
||| @ ok proof that the list is non-empty
public export
last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
last [] impossible
last [x] = x
last (_::x::xs) = List.last (x::xs)

||| Return all but the last element of a non-empty list.
||| @ ok proof the list is non-empty
public export
init : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
init [] impossible
init [_] = []
init (x::y::ys) = x :: init (y::ys)

||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
public export
head' : List a -> Maybe a
head' []      = Nothing
head' (x::_) = Just x

||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
export
tail' : List a -> Maybe (List a)
tail' []      = Nothing
tail' (_::xs) = Just xs

||| Attempt to retrieve the last element of a non-empty list.
|||
||| If the list is empty, return `Nothing`.
export
last' : List a -> Maybe a
last' [] = Nothing
last' xs@(_::_) = Just (last xs)

||| Attempt to return all but the last element of a non-empty list.
|||
||| If the list is empty, return `Nothing`.
export
init' : List a -> Maybe (List a)
init' [] = Nothing
init' xs@(_::_) = Just (init xs)

||| Convert any Foldable structure to a list.
export
toList : Foldable t => t a -> List a
toList = foldr (::) []

||| Prefix every element in the list with the given element
|||
||| ```idris example
||| with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
||| ```
|||
export
mergeReplicate : a -> List a -> List a
mergeReplicate sep []      = []
mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys

||| Insert some separator between the elements of a list.
|||
||| ````idris example
||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
||| ````
|||
export
intersperse : a -> List a -> List a
intersperse sep []      = []
intersperse sep (x::xs) = x :: mergeReplicate sep xs

||| Given a separator list and some more lists, produce a new list by
||| placing the separator between each of the lists.
|||
||| @ sep the separator
||| @ xss the lists between which the separator will be placed
|||
||| ```idris example
||| intercalate [0, 0, 0] [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
||| ```
export
intercalate : (sep : List a) -> (xss : List (List a)) -> List a
intercalate sep xss = concat $ intersperse sep xss

||| Apply a partial function to the elements of a list, keeping the ones at which
||| it is defined.
public export
mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe f []      = []
mapMaybe f (x::xs) =
  case f x of
    Nothing => mapMaybe f xs
    Just j  => j :: mapMaybe f xs

--------------------------------------------------------------------------------
-- Special folds
--------------------------------------------------------------------------------

||| Foldl a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldl1 : (a -> a -> a) -> (l : List a)  -> {auto 0 ok : NonEmpty l} -> a
foldl1 f [] impossible
foldl1 f (x::xs) = foldl f x xs

||| Foldr a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldr1 : (a -> a -> a) -> (l : List a)  -> {auto 0 ok : NonEmpty l} -> a
foldr1 f [] impossible
foldr1 f [x] = x
foldr1 f (x::y::ys) = f x (List.foldr1 f (y::ys))

||| Foldl without seeding the accumulator. If the list is empty, return `Nothing`.
public export
foldl1' : (a -> a -> a) -> List a -> Maybe a
foldl1' f [] = Nothing
foldl1' f xs@(_::_) = Just (List.foldl1 f xs)

||| Foldr without seeding the accumulator. If the list is empty, return `Nothing`.
public export
foldr1' : (a -> a -> a) -> List a -> Maybe a
foldr1' f [] = Nothing
foldr1' f xs@(_::_) = Just (List.foldr1 f xs)

--------------------------------------------------------------------------------
-- Sorting
--------------------------------------------------------------------------------

||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
export
sorted : Ord a => List a -> Bool
sorted (x :: xs @ (y :: _)) = x <= y && sorted xs
sorted _ = True

||| Merge two sorted lists using an arbitrary comparison
||| predicate. Note that the lists must have been sorted using this
||| predicate already.
export
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order []      right   = right
mergeBy order left    []      = left
mergeBy order (x::xs) (y::ys) =
  -- The code below will emit `y` before `x` whenever `x == y`.
  -- If you change this, `sortBy` will stop being stable, unless you fix `sortBy`, too.
  case order x y of
       LT => x :: mergeBy order xs (y::ys)
       _  => y :: mergeBy order (x::xs) ys

||| Merge two sorted lists using the default ordering for the type of their elements.
export
merge : Ord a => List a -> List a -> List a
merge left right = mergeBy compare left right

||| Sort a list using some arbitrary comparison predicate.
|||
||| @ cmp how to compare elements
||| @ xs the list to sort
export
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
sortBy cmp []  = []
sortBy cmp [x] = [x]
sortBy cmp xs  = let (x, y) = split xs in
    mergeBy cmp
          (sortBy cmp (assert_smaller xs x))
          (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
  where
    splitRec : List b -> List a -> (List a -> List a) -> (List a, List a)
    splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
    splitRec _          ys      zs = (ys, zs [])
    -- In the above base-case clause, we put `ys` on the LHS to get a stable sort.
    -- This is because `mergeBy` prefers taking elements from its RHS operand
    -- if both heads are equal, and all elements in `zs []` precede all elements of `ys`
    -- in the original list.

    split : List a -> (List a, List a)
    split xs = splitRec xs xs id

||| Sort a list using the default ordering for the type of its elements.
export
sort : Ord a => List a -> List a
sort = sortBy compare

export
isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
isPrefixOfBy p [] _            = True
isPrefixOfBy p _ []            = False
isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys

||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
export
isPrefixOf : Eq a => List a -> List a -> Bool
isPrefixOf = isPrefixOfBy (==)

export
isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
export
isSuffixOf : Eq a => List a -> List a -> Bool
isSuffixOf = isSuffixOfBy (==)

||| The isInfixOf function takes two lists and returns True iff the first list
||| is contained, wholly and intact, anywhere within the second.
|||
||| ```idris example
||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
||| ```
||| ```idris example
||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
||| ```
|||
export
isInfixOf : Eq a => List a -> List a -> Bool
isInfixOf n h = any (isPrefixOf n) (tails h)

||| Transposes rows and columns of a list of lists.
|||
||| ```idris example
||| with List transpose [[1, 2], [3, 4]]
||| ```
|||
||| This also works for non square scenarios, thus
||| involution does not always hold:
|||
|||     transpose [[], [1, 2]] = [[1], [2]]
|||     transpose (transpose [[], [1, 2]]) = [[1, 2]]
export
transpose : List (List a) -> List (List a)
transpose [] = []
transpose (heads :: tails) = spreadHeads heads (transpose tails) where
  spreadHeads : List a -> List (List a) -> List (List a)
  spreadHeads []              tails           = tails
  spreadHeads (head :: heads) []              = [head] :: spreadHeads heads []
  spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

export
Uninhabited ([] = Prelude.(::) x xs) where
  uninhabited Refl impossible

export
Uninhabited (Prelude.(::) x xs = []) where
  uninhabited Refl impossible

||| (::) is injective
export
consInjective : forall x, xs, y, ys .
                the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
consInjective Refl = (Refl, Refl)

||| The empty list is a right identity for append.
export
appendNilRightNeutral : (l : List a) -> l ++ [] = l
appendNilRightNeutral []      = Refl
appendNilRightNeutral (_::xs) = rewrite appendNilRightNeutral xs in Refl

||| Appending lists is associative.
export
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative []      c r = Refl
appendAssociative (_::xs) c r = rewrite appendAssociative xs c r in Refl

revOnto : (xs, vs : List a) -> reverseOnto xs vs = reverse vs ++ xs
revOnto _ [] = Refl
revOnto xs (v :: vs)
    = rewrite revOnto (v :: xs) vs in
        rewrite appendAssociative (reverse vs) [v] xs in
                                  rewrite revOnto [v] vs in Refl

export
revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl
revAppend (v :: vs) ns
    = rewrite revOnto [v] vs in
        rewrite revOnto [v] (vs ++ ns) in
          rewrite sym (revAppend vs ns) in
            rewrite appendAssociative (reverse ns) (reverse vs) [v] in
              Refl

export
dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
dropFusion  Z     m    l      = Refl
dropFusion (S n)  Z    l      = rewrite plusZeroRightNeutral n in Refl
dropFusion (S n) (S m) []     = Refl
dropFusion (S n) (S m) (x::l) = rewrite plusAssociative n 1 m in
                                rewrite plusCommutative n 1 in
                                dropFusion (S n) m l

export
lengthMap : (xs : List a) -> length (map f xs) = length xs
lengthMap [] = Refl
lengthMap (x :: xs) = cong S (lengthMap xs)


text:
module LazyFoldlM

import Data.List.Lazy

import Debug.Trace

foldlM : Monad m => (fm : b -> a -> m b) -> (init : b) -> LazyList a -> m b
foldlM fm init xs = foldrLazy (\x, k, z => fm z x >>= k) pure xs init

l : LazyList Nat
l = (\n => trace "gen \{show n}" n) <$> iterateN 10000 (+1) 0

x : Maybe Nat
x = LazyFoldlM.foldlM (\m, n => trace "nm: \{show n} \{show m}" $ if m <= 1 then Just n else Nothing) 0 l

y : Maybe Nat
y = Prelude.foldlM (\m, n => trace "nm: \{show n} \{show m}" $ if m <= 1 then Just n else Nothing) 0 l


text:
||| The content of this module is based on the paper
||| Applications of Applicative Proof Search
||| by Liam O'Connor

module Search.Properties

import Data.Fuel
import Data.List.Lazy
import Data.List.Lazy.Quantifiers
import Data.Nat
import Data.So
import Data.Stream
import Data.Colist
import Data.Colist1

import public Search.Negation
import public Search.HDecidable
import public Search.Generator

import Decidable.Equality

%default total

------------------------------------------------------------------------
-- Type

||| Take the product of a list of types
public export
Product : List Type -> Type
Product = foldr Pair ()

||| A property amenable to testing
||| @cs is the list of generators we need (inferrable)
||| @a  is the type we hope is inhabited
||| NB: the longer the list of generators, the bigger the search space!
public export
record Prop (cs : List Type) (a : Type) where
  constructor MkProp
  ||| The function trying to find an `a` provided generators for `cs`.
  ||| Made total by consuming some fuel along the way.
  runProp : Colist1 (Product cs) -> Fuel -> HDec a

------------------------------------------------------------------------
-- Prop-like structure

||| A type constructor satisfying the AProp interface is morally a Prop
||| It may not make use of all of the powers granted by Prop, hence the
||| associated `Constraints` list of types.
public export
interface AProp (0 t : Type -> Type) where
  0 Constraints : List Type
  toProp : t a -> Prop Constraints a

||| Props are trivially AProp
public export
AProp (Prop cs) where
  Constraints = cs
  toProp = id

||| Half deciders are AProps that do not need any constraints to be satisfied
public export
AProp HDec where
  Constraints = []
  toProp = MkProp . const . const

||| Deciders are AProps that do not need any constraints to be satisfied
public export
AProp Dec where
  Constraints = []
  toProp = MkProp . (const . const . toHDec)

||| We can run an AProp to try to generate a value of type a
public export
check : (gen : Generator (Product cs)) => (f : Fuel) -> (p : Prop cs a) ->
        {auto pr : So (isTrue (runProp p (generate @{gen}) f))} -> a
check @{gen} f p @{pr} = evidence (runProp p (generate @{gen}) f) pr

||| Provided that we know how to generate candidates of type `a`, we can look
||| for a witness satisfying a given predicate over `a`.
public export
exists : {0 p : a -> Type} -> (aPropt : AProp t) =>
         ((x : a) -> t (p x)) ->
         Prop (a :: Constraints @{aPropt}) (DPair a p)
exists test = MkProp $ \ acs, fuel =>
  let candidates : LazyList a = take fuel (map fst acs) in
  let cs = map snd acs in
  let find = any candidates (\ x => runProp (toProp (test x)) cs fuel) in
  map toDPair find

------------------------------------------------------------------------
-- Examples

namespace GT11

  example : Prop ? (DPair Nat (\ i => Not (i `LTE` 10)))
  example = exists (\ i => not (isLTE 11 i))

  lemma : DPair Nat (\ i => Not (i `LTE` 10))
  lemma = check (limit 1000) example

namespace Pythagoras

  formula : Type
  formula = DPair Nat $ \ m =>
            DPair Nat $ \ n =>
            DPair Nat $ \ p =>
            (0 `LT` m, 0 `LT` n, 0 `LT` p
            , (m * m + n * n) === (p * p))

  search : Prop ? Pythagoras.formula
  search = exists $ \ m =>
           exists $ \ n =>
           exists $ \ p =>
           (isLT 0 m && isLT 0 n && isLT 0 p
           && decEq (m * m + n * n) (p * p))

  -- This one is quite a bit slower so it's better to run
  -- the compiled version instead
  lemma : HDec Pythagoras.formula
  lemma = runProp search generate (limit 10)


text:
module Network.HTTP.Method

import Generics.Derive

%language ElabReflection

public export
data Method : Type where
  GET : Method
  HEAD : Method
  POST : Method
  PUT : Method
  DELETE : Method
  CONNECT : Method
  OPTIONS : Method
  PATCH : Method
  Custom : String -> Method

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

export
http_method_to_string : Method -> String
http_method_to_string (Custom x) = toUpper x
http_method_to_string x = show x

export
string_to_http_method : String -> Method
string_to_http_method x =
  case toUpper x of
    "GET" => GET
    "HEAD" => HEAD
    "POST" => POST
    "PUT" => PUT
    "DELETE" => DELETE
    "CONNECT" => CONNECT
    "OPTIONS" => OPTIONS
    "PATCH" => PATCH
    x => Custom x

export
FromString Method where
  fromString = string_to_http_method


text:
module TheHobbit

import Flexidisc
import Flexidisc.Validation

Record' : Header String -> Type
Record' = Record String

location : Record' ["city" ::: String, "region" ::: String, "smial" ::: String]
location = [ "region" := "Shire"
           , "city"   := "Hobbiton"
           , "smial"  := "Bag End"
           ]

gandalf : Record' [ "firstname" ::: String
                  , "nickname"  ::: String
                  ]
gandalf = [ "firstname" := "Gandalf" , "nickname"  := "The Grey" ]

magician : Record' [ "firstname" ::: String
                   , "nickname"  ::: String
                   , "class"     ::: String
                   ]
magician = "class" := "Magician" :: gandalf

backToGandalf : Record' [ "firstname" ::: String
                        , "nickname"  ::: String
                        ]
backToGandalf = drop "class" magician

keepArbitrary : Record' [ "class" ::: String ]
keepArbitrary = keep ["class"] magician

theGrey : String
theGrey = gandalf !! "nickname"

gandalfWho : Maybe String
gandalfWho = Read.lookup "lastname" gandalf -- Nothing

bilbo : Record' [ "firstname" ::: String
                , "lastname"  ::: String
                ]
bilbo = [ "firstname" := "Bilbo", "lastname" := "Baggins" ]

theHobbitCharacters : RecordList String
                                 [ [ "firstname" ::: String
                                   , "nickname"  ::: String ]
                                 , [ "firstname" ::: String
                                   , "lastname"  ::: String ]
                                 ]
theHobbitCharacters = [gandalf, bilbo]

theHobbitFirstnames : List (Record' ["firstname" ::: String])
theHobbitFirstnames = toList theHobbitCharacters

fullname : Record' header ->
           {auto fProof : Row "firstname" String header} ->
           {auto lProof : Row "lastname"  String header} ->
           String
fullname xs = unwords [xs !! "firstname", xs !! "lastname"]

longerFullname : RecordFunc [ "firstname" ::: String ]
                            [ "lastname"  ::: String
                            , "nickname"  ::: String ]
                            String
longerFullname = Func go
  where
    go req opt = unwords $ (req !! "firstname")
                         :: catMaybes [ opt !! "nickname"
                                      , opt !! "lastname" ]

charactersName : List String
charactersName = foldAll longerFullname theHobbitCharacters

gandalf' : Record' [ "firstname" ::: String
                   , "nickname"  ::: String
                   ]
gandalf' = [ "firstname" := "gandalf" , "nickname"  := "The grey" ]

secureFullname : RecordFunc [ "firstname" ::: String ]
                            [ "lastname"  ::: String
                            , "nickname"  ::: String ]
                            (Validation (List String) String)
secureFullname = Func go
  where
    uppercaseFirst : String -> Validation (List String) String
    uppercaseFirst =
      validateL (\str => "In \"" ++ str ++ "\" each word should start with an uppercase")
                (all (isUpper . strHead) . words)
    go req opt = map unwords $ sequence $ catMaybes
                   [ Just (uppercaseFirst (req !! "firstname"))
                   , map  uppercaseFirst (opt !! "nickname")
                   , map  uppercaseFirst (opt !! "lastname")
                   ]

checkedCharactersName : List (Validation (List String) String)
checkedCharactersName = foldAll secureFullname theHobbitCharacters

errorOnCharachtersName : List (Validation (List String) String)
errorOnCharachtersName = foldAll secureFullname [bilbo, gandalf']

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
||| Simple mutable hashtable.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.Hashtable

import Data.Container.Mutable.Array
import public Data.Container.Mutable.Interfaces
import Data.Hash

import Data.Maybe
import Data.Fin
import Data.So
import Data.List
import Data.IORef

%default total

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

export data IOHashtable k v
  = MkIOHashtable (IORef Nat) (IOArray (List (k, IORef v)))

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

export newIOHashtable : HasIO io
    => (capacity:Nat)
    -> {auto 0 capacity_isnt_zero: So (capacity /= 0)}
    -> io (IOHashtable k v)
newIOHashtable capacity@(S _)
  = pure $ MkIOHashtable !(newIORef 0) !(newIOArray capacity [])

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

export null : (HasIO io, Eq k, Hashable k) => IOHashtable k v -> io Bool
null (MkIOHashtable c _) = pure $ !(readIORef c) == 0

export length : (HasIO io, Eq k, Hashable k) => IOHashtable k v -> io Nat
length (MkIOHashtable c _) = readIORef c

export contains : (HasIO io, Eq k, Hashable k) => k -> IOHashtable k v -> io Bool
contains k (MkIOHashtable _ arr) = do
  let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
  xs <- readIOArray arr ix
  pure $ maybe False (const True) $ lookup k xs

export insert : (HasIO io, Eq k, Hashable k) => k -> v -> IOHashtable k v -> io Bool
insert k v (MkIOHashtable c arr) = do
  let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
  xs <- readIOArray arr ix
  case lookup k xs of
       Just refv => writeIORef refv v
       Nothing => do
         kv <- pure $ (k, !(newIORef v))
         writeIOArray arr ix (kv::xs)
         modifyIORef c S
  pure True

export lookup : (HasIO io, Eq k, Hashable k) => k -> IOHashtable k v -> io (Maybe v)
lookup k (MkIOHashtable _ arr) = do
  let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
  xs <- readIOArray arr ix
  maybe (pure Nothing) (\v' => pure $ Just !(readIORef v')) $ lookup k xs

export delete : (HasIO io, Eq k, Hashable k) => k -> IOHashtable k v -> io Bool
delete k (MkIOHashtable c arr) = do
  let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
  xs <- readIOArray arr ix
  let xs' = filter ((k /=) . fst) xs
      d = cast (length xs) - cast (length xs')
  writeIOArray arr ix xs'
  modifyIORef c (\c' => fromInteger $ cast c' - d)
  pure $ d /= 0

{-
export
(HasIO io, Eq k, Hashable k) => MutableMap io (IOHashtable k) where

  null (MkIOHashtable c _) = pure $ !(readIORef c) == 0
  length (MkIOHashtable c _) = readIORef c

  contains k (MkIOHashtable _ arr) = do
    let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
    xs <- readIOArray arr ix
    pure $ maybe False (const True) $ lookup k xs

  insert k v (MkIOHashtable c arr) = do
    let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
    xs <- readIOArray arr ix
    case lookup k xs of
         Just refv => writeIORef refv v >> pure True
         Nothing => do
           kv <- pure $ (k, !(newIORef v))
           writeIOArray arr ix (kv::xs)
           modifyIORef c S
           pure True

  lookup k (MkIOHashtable _ arr) = do
    let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
    xs <- readIOArray arr ix
    maybe (pure Nothing) (\v' => pure $ Just !(readIORef v')) $ lookup k xs

  delete k (MkIOHashtable c arr) = do
    let ix = restrict (ubound arr) (cast $ saltedHash 0xdeadbeef k)
    xs <- readIOArray arr ix
    let xs' = filter ((k /=) . fst) xs
        d = cast (length xs) - cast (length xs')
    writeIOArray arr ix xs'
    modifyIORef c (+ fromInteger d)
    pure $ d /= 0

-}

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


text:
module Data.JSON.Value

import Data.Scientific

public export
data JSONValue : Type where
  JSONNull : JSONValue
  JSONBool : Bool -> JSONValue
  JSONNumber : Scientific 10 -> JSONValue
  JSONString : String -> JSONValue
  JSONObject : List (String, JSONValue) -> JSONValue
  JSONArray : List JSONValue -> JSONValue

public export
Eq JSONValue where
  JSONNull == JSONNull = True
  (JSONBool x) == (JSONBool y) = x == y
  (JSONNumber x) == (JSONNumber y) = x == y
  (JSONString x) == (JSONString y) = x == y
  (JSONObject xs) == (JSONObject ys) = xs == ys
  (JSONArray xs) == (JSONArray ys) = xs == ys
  _ == _ = False

public export
Show JSONValue where
  show JSONNull = "JSONNull"
  show (JSONBool x) = "JSONBool " ++ show x
  show (JSONNumber x) = "JSONNumber " ++ prettyShowScientific x
  show (JSONString x) = "JSONString " ++ show x
  show (JSONObject xs) = "JSONObject " ++ show xs
  show (JSONArray xs) = "JSONArray " ++ show xs


text:
module Idrlisp.Signature

import Idrlisp.Sexp
import Idrlisp.Pattern

%default total

public export
data Signature a
  = Any String
  | Num String
  | Sym String
  | Str String
  | Bool String
  | Nil
  | (::) (Signature a) (Signature a)
  | List (Signature a)
  | Pat String
  | Pure String a
  | Or (Signature a) (Signature a)

namespace Args
  public export
  data ArgsSignature a
    = Nil
    | (::) (Signature a) (ArgsSignature a)
    | Rest (Signature a)

export
Cast (Signature a) (Sexp b) where
  cast (Any x) = Sym x
  cast (Num x) = Sym x
  cast (Sym x) = Sym x
  cast (Str x) = Sym x
  cast (Bool x) = Sym x
  cast Nil = Nil
  cast (x :: y) = cast x :: cast y
  cast (List x) = [cast x, Sym "..."]
  cast (Pat x) = Sym x
  cast (Pure x _) = Sym x
  cast (Or x y) = [Sym "or", cast x, cast y]

export
Cast (ArgsSignature a) (Sexp b) where
  cast Nil = Nil
  cast (x :: y) = cast x :: cast y
  cast (Rest x) = [cast x, Sym "..."]

export
covering
Show (Signature a) where
  show x = show (the (Sexp ()) (cast x))

export
covering
Show (ArgsSignature a) where
  show x = show (the (Sexp ()) (cast x))

public export
interface Match a s | a where
  SignatureType : a -> Type
  match : (sig : a) -> s -> Maybe (SignatureType sig)

public export
Match () () where
  SignatureType () = ()
  match () () = Just ()

public export
Match a b => Match (Signature a) (Sexp b) where
  SignatureType (Any _) = Sexp b
  SignatureType (Num _) = Double
  SignatureType (Sym _) = String
  SignatureType (Str _) = String
  SignatureType (Bool _) = Bool
  SignatureType Nil = ()
  SignatureType (a :: b) =
    case b of
      Nil => SignatureType a
      b' => (SignatureType a, SignatureType b')
  SignatureType (List a) = List (SignatureType a)
  SignatureType (Pat _) = Pattern
  SignatureType (Pure _ a) = SignatureType a
  SignatureType (Or a b) = Either (SignatureType a) (SignatureType b)

  match (Any _) x = Just x
  match (Num _) (Num x) = Just x
  match (Num _) _ = Nothing
  match (Sym _) (Sym x) = Just x
  match (Sym _) _ = Nothing
  match (Str _) (Str x) = Just x
  match (Str _) _ = Nothing
  match (Bool _) (Bool x) = Just x
  match (Bool _) _ = Nothing
  match Nil [] = Just ()
  match Nil _ = Nothing
  match (car :: cdr) (x :: y) = do
    x' <- match car x
    y' <- match cdr y
    Just $ case cdr of
      Nil => x'
      -- It seems that Idris type checker cannot specialize `SignatureType (car :: cdr)`.
      _ => believe_me (x', y')
  match (car :: cdr) _ = Nothing
  match (List s) xs with (cast {to = SList b} xs)
    | Proper xs' = traverse (match s) xs'
    | Improper x = Nothing
  match (Pat _) x =
    case Pattern.build x of
      Right p => Just p
      Left _ => Nothing
  match (Pure _ s) (Pure x) = match s x
  match (Pure _ s) _ = Nothing
  match (Or a b) x = (Left <$> match a x) <|> (Right <$> match b x)

public export
Match a b => Match (ArgsSignature a) (List (Sexp b)) where
  SignatureType Nil = ()
  SignatureType (x :: y) =
    case y of
      Nil => SignatureType x
      y' => (SignatureType x, SignatureType y')
  SignatureType (Rest x) = List (SignatureType x)

  match Nil [] = Just ()
  match Nil _ = Nothing
  match (car :: cdr) (x :: y) = do
    x' <- match car x
    y' <- match cdr y
    Just $ case cdr of
      Nil => x'
      -- Same as Match Signature, Idris type checker cannot specialize `SignatureType (car :: cdr)`.
      _ => believe_me (x', y')
  match (car :: cdr) _ = Nothing
  match (Rest s) xs = traverse (match s) xs

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Applicative

-- Attempt to write applicative from memory
interface Functor s => MyApplicative (s : Type -> Type) where
          myPure : a -> s a
          myApply : s (a -> b) -> s a -> s b