text:
module nabarundeka.Odds

import Evens

import Intro

data IsOdd : (n : Nat) -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n : Nat) -> IsOdd n -> IsOdd (S (S n))

threeOdd : IsOdd 3
threeOdd = SSOdd 1 OneOdd

twoNotOdd : IsOdd 2 -> Void
twoNotOdd OneOdd impossible
twoNotOdd (SSOdd Z OneOdd) impossible
twoNotOdd (SSOdd Z (SSOdd _ _)) impossible

nOddSnEven : (n : Nat) -> IsOdd n -> IsEven (S n)
nOddSnEven (S Z) OneOdd = SSEven 0 ZEven
nOddSnEven (S (S n)) (SSOdd n x) = SSEven (S n) (nOddSnEven n x)

nEvenSnOdd : (n : Nat) -> IsEven n -> IsOdd (S n)
nEvenSnOdd Z ZEven = OneOdd
nEvenSnOdd (S (S n)) (SSEven n x) = SSOdd (S n) (nEvenSnOdd n x)

nOddOrEven : (n : Nat) -> Either (IsEven n) (IsOdd n)
nOddOrEven Z = Left ZEven
nOddOrEven (S n) = case (nOddOrEven n) of
                      (Left l) => Right (nEvenSnOdd n l)
                      (Right r) => Left (nOddSnEven n r)

nNotOddEven : (n: Nat) -> (IsOdd n) -> (IsEven n) -> Void
nNotOddEven Z OneOdd ZEven impossible
nNotOddEven (S Z) OneOdd ZEven impossible
nNotOddEven (S (S n)) (SSOdd n x) (SSEven n y) = nNotOddEven n x y

nNotOddEvenBoth : (n : Nat) -> (IsOdd n, IsEven n) -> Void
nNotOddEvenBoth n (x,y) = nNotOddEven n x y

sumOddOdd : (n : Nat) -> (m : Nat) -> (IsOdd n) -> (IsOdd m) -> IsEven (add n m)
sumOddOdd (S Z) m OneOdd x = nOddSnEven m x
sumOddOdd (S (S n)) m (SSOdd n x) y = SSEven (add n m) (sumOddOdd n m x y)

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

succOddDivByTwo : (n : Nat) -> IsOdd n -> (k : Nat ** (S(double k)) = n)
succOddDivByTwo (S Z) OneOdd = (Z ** Refl)
succOddDivByTwo (S (S k)) (SSOdd k x) = step where
  step = case (succOddDivByTwo k x) of
              (m ** pf) => ((S m) ** apNat (\l=> S (S l)) (S(double m)) k pf)


text:
module Main

import Control.App
import Control.App.Console

import Test.Unit.Spec
import Control.App.Fresh

%default total

data FreshA : Type where
data FreshB : Type where

partial main : IO ()
main = run $ consoleRunSpecSimple $ do
  describe "Fresh number" $ do
    runFresh FreshA $ do
      tests "fresh" $ do
        (lift $ fresh FreshA) >>= assertEqual 1
        (lift $ fresh FreshA) >>= assertEqual 2
        (lift $ fresh FreshA) >>= assertEqual 3

ext: idr


text:
module sorting_with_proof

import Data.Vect
import Data.Fin
import permutation
import perm_cons
import Finite

%access public export

||| Type of proofs that a vector 'v' of length 'n' is sorted in increasing order.
||| It takes the following parameters : 'n'(length of the vector), 'v'(vector),
||| 'ind'(index). Check if v[ind - 1] <= v[ind]. Note that the predecessor
||| function takes care of the first index ( pred FZ = FZ ).
total
SortProof : (n : Nat) -> (NatVect n) -> (Fin n) -> Type
SortProof Z v a impossible
SortProof (S k) v l = LTE (Vect.index (pred l) v) (Vect.index l v)

||| If 'v' is a vector of length 'n' then an element of the Type
||| (IsSorted n v) is a function which given an index 'k' gives
||| a proof that v[k-1] <= v[k]. The special case for first
||| index is taken care of by the predecessor function
||| (pred FZ = FZ).
total
IsSorted : (n : Nat) -> (v : (NatVect n)) -> Type
IsSorted n v = (k : Fin n) -> (SortProof n v k)

||| An element of the type SortedVect n v is of the form (v_sorted, perm, pfPerm, pfSort)
||| where 'v_sorted' is 'v' with its element sorted in increasing order. 'perm' is a
||| permutation such that perm(v) = v_sorted. 'pfPerm' is a proof that perm(v) = v_sorted.
||| 'pfSort' is a proof that 'v_sorted' is sorted.
total
SortedVect : (n : Nat) -> (v : (NatVect n)) -> Type
SortedVect n v = (v_sorted : (NatVect n) **
                 (perm : (PermC n) ** (((applyPerm n Nat perm v) = v_sorted), (IsSorted n v))))


text:
import Language.Reflection

add : TTImp -> TTImp -> TTImp
add x y = `(~(x) + ~(y))

test : TTImp
test = add `(3) `(4)

bigger : TTImp -> TTImp
bigger val
    = `(let xfn : Int -> Int
            xfn var = var * 2 in
            xfn ~(val))

bigger' : Int -> TTImp
bigger' val
    = `(let xfn : Int -> Int
            xfn var = var * 2 in
            xfn ~(IPrimVal EmptyFC (I val)))

bad : Int -> TTImp
bad val
    = `(let xfn : Int -> Int
            xfn var = var * 2 in
            xfn ~(val))

names : List Name
names = [ `{{ names }}, `{{ Prelude.(+) }} ]


text:
import public Data.Vect

-- Write a type for an m×n matrix.

Matrix : Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

-- Write a function to mirror a matrix horizontally.

horizontallyMirrorMatrix: Matrix n m a -> Matrix n m a
horizontallyMirrorMatrix [] = []
horizontallyMirrorMatrix (row :: rows) = reverse row :: (horizontallyMirrorMatrix rows)

-- Write a function to transpose the matrix so that element m, n in the argument is element n, m in the result.
transposeMatrix : Matrix n m a -> Matrix m n a
transposeMatrix matrix = transpose matrix

max_stars_repo_name: hemslo/seven-in-seven

max_issues_repo_name: hemslo/seven-in-seven

max_forks_repo_name: hemslo/seven-in-seven


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

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

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

-- Covering function for the View
total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) = case listLast xs of
  Empty => NonEmpty [] x
  NonEmpty ys y => NonEmpty (x :: ys) y

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

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

myReverse : List a -> List a
myReverse input with (listLast input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs

data SplitList : List a -> Type where
  SplitNil : SplitList []
  SplitOne : SplitList [x]
  SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ rights)

total
splitList : (input : List a) -> SplitList input
splitList input = splitListHelp input input
  where
    splitListHelp : List a -> (input : List a) -> SplitList input
    splitListHelp _ [] = SplitNil
    splitListHelp _ [x] = SplitOne
    splitListHelp (_ :: _ :: counter) (item :: items) =
      case splitListHelp counter items of
        SplitNil => SplitOne
        SplitOne {x} => SplitPair [item] [x]
        SplitPair lfts rgts => SplitPair (item :: lfts) rgts
    splitListHelp _ items = SplitPair [] items

mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ rights) | (SplitPair lefts rights) = merge (mergeSort lefts) (mergeSort rights)

main : IO ()
main = do
  putStrLn $ describeListEnd []
  putStrLn $ describeListEnd [1]
  putStrLn $ describeListEnd [1,2,3]
  putStrLn $ describeListEndWith []
  putStrLn $ show $ myReverse [1,2,3,4,5]
  putStrLn $ show $ merge [1,3,5] [2,4,6]
  printLn $ mergeSort [3,2,1]
  printLn $ mergeSort [5,1,4,3,2,6,8,7,9]

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module MenoSlave

%default total

-- This proof is based on the dialog between Socrates and one of Meno's slaves
-- Source: Plato, Meno, 84c

{- Diagammatic view of the square

  J-H-G
  |/ \|
  D C E
  |\ /|
  A-B-F

-}

{- Axioms

A square is a regular quadrilateral with four equal sides and angles with properties
The angles of a square add up to 360 degrees

A triangle is a polygon with three edges and vertices
The angles of a triangle add up to 180 degrees
An isosceles triangle is a triangle with two sides (and therefore two angles) of equal length

-}

-- Construct a square

data Square   : Double -> Type where
     MkSquare : Double -> Square a

testSquareReflexivity : Square 4 = Square (2 + 2)
testSquareReflexivity = Refl

testSquareReflexivity' : Square 3 = Square (3 + 1) -> Void
testSquareReflexivity' Refl impossible

-- Square functions

length : Square a -> Double
length (MkSquare x) = x

testLength : length (MkSquare 4) = 4.0
testLength = Refl

circumference : Square a -> Double
circumference (MkSquare x) = x * 4

testCircumference : circumference (MkSquare 4) = 16.0
testCircumference = Refl

area : Square a -> Double
area (MkSquare x) = x * x

testArea : area (MkSquare 5) = 25.0
testArea = Refl

-- Construct a square from four smaller squares

makeSquare : Square a -> Square b -> Square c -> Square d -> Square e
makeSquare w x y z = MkSquare (area w + area x + area y + area z)

testMakeSquare : makeSquare (MkSquare 1) (MkSquare 2) (MkSquare 3) (MkSquare 4) = (MkSquare 30)
testMakeSquare = Refl

-- Construct four equal squares

-- SOCRATES: Tell me, boy, is not this our square of four feet? (ABCD.) You understand?
-- BOY: Yes.
abcd : Square 4
abcd = MkSquare 4

-- SOCRATES: Now we can add another equal to it like this? (BCEF.)
-- BOY: Yes.
bcef : Square 4
bcef = MkSquare 4

-- SOCRATES: And a third here, equal to each of the others? (CEGH.)
-- BOY: Yes.
cegh : Square 4
cegh = MkSquare 4

-- SOCRATES: And then we can fill in this one in the comer? (DCHJ.)
-- BOY: Yes.
dchj : Square 4
dchj = MkSquare 4

-- SOCRATES: Then here we have four equal squares?
-- BOY: Yes.
fourEqualSquares : MenoSlave.abcd = MenoSlave.bcef -> MenoSlave.bcef = MenoSlave.cegh -> MenoSlave.cegh = MenoSlave.dchj
fourEqualSquares Refl Refl = Refl

afgj : Square a
afgj = makeSquare abcd bcef cegh dchj

-- 4 * 4 = 16, and 16 * 4 = 64
testSizeAFGJ : MenoSlave.afgj = (MkSquare 64)
testSizeAFGJ = Refl

-- Diagonal bisection of a square
-- To bisect a square diagonally in equal parts, we need to split one of it's angles into two equal pieces:
bisect90deg : 90.0 / 2 = 45
bisect90deg = Refl

-- This will split the square into two triangles
-- Since we know two of the angles, we can infer the length of the third angle:
partial triangleAngles : 90 + 45 + c = 180
triangleAngles {c = 45} = Refl

-- Since the unknown angle is equal to the split angle, we know that it has formed an isosceles triangle where the
-- non-diagonal sides are equal, which means that a diagonal split along a square creates two equal pieces

-- Construct a triangle
data Triangle   : Double -> Double -> Type where
     MkTriangle : Double -> Double -> Triangle a b

areaTriangle : Triangle a b -> Double
areaTriangle (MkTriangle x y) = x * y / 2

-- SOCRATES: Now does this line going from corner to corner cut each of these squares in half? (BEHD.)
-- BOY: Yes.

-- Cuts ABCD across DB, BCEF across BE, CEGH across EH, DCHJ across HD

lenABCD : Double
lenABCD = length abcd

acbdHalved : areaTriangle (MkTriangle MenoSlave.lenABCD MenoSlave.lenABCD) +
             areaTriangle (MkTriangle MenoSlave.lenABCD MenoSlave.lenABCD) = area MenoSlave.abcd
acbdHalved = Refl

-- Same type of proof holds for all other squares due being cut along their diagonals and having the same size

-- SOCRATES: And how many such halves are there in this figure? (BEHD.)
-- BOY: Four.
-- SOCRATES: And how many in this one? (ABCD.)
-- BOY: Two.
-- SOCRATES: And what is the relation of four to two?
-- BOY: Double.
-- SOCRATES: How big is this figure then?
-- BOY: Eight feet.
-- SOCRATES: On what base?
-- BOY: This one.
-- SOCRATES: The line which goes from corner to corner of the square of four feet?
-- BOY: Yes.
-- SOCRATES: The technical name for it is 'diagonal'; so if we use that name, it is your personal opinion that the
--           square on the diagonal of the original square is double its area.
-- BOY: That is so, Socrates.

max_stars_repo_name: Risto-Stevcev/meno-slave

max_issues_repo_name: Risto-Stevcev/meno-slave

max_forks_repo_name: Risto-Stevcev/meno-slave


text:
example : String
example = ?example


text:
x : IO $ Either Bool $ Maybe Bool

f : IO ()
f = do
  Left b <- x
     | Right (Just b) => pure ()
     | Right Nothing => pure ()
  pure ()

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Data.List
import Data.HVect
import Helper

allowedChars : List Char
allowedChars = ['a'..'z'] ++ ['0'..'9'] ++ ['-']

data ValidLiteral : List Char -> Type where
  One : { auto prf : Elem value Main.allowedChars } -> ValidLiteral [value]
  Multi : { auto prf : Elem value Main.allowedChars } -> ValidLiteral xs -> ValidLiteral (value :: xs)

data LiteralRoute : String -> Type where
  Literal : (lit:String) ->
            -- RULE 1
            { auto prf : ValidLiteral (unpack lit) } ->
            LiteralRoute lit

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

maxLevel : Nat
maxLevel = 3

data Base = MkBase

-- shortRoute : Test Route
-- shortRoute = Check (Root / Literal "two" / Literal "three") -- must compile

-- longRoute : Test Route
-- longRoute = Check (Root / Literal "two" / Literal "three" / Literal "four") -- does not compile

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
-- Module      : Main
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

import Itea

||| Message sent upon user generated event
data Msg
  = Edited

data Reason
  = TooShort
  | DoNotMatch
  | Ok

||| Application model consisting of the applicaiton state
record Model where
  constructor MkModel
  password      : String
  passwordAgain : String

||| Initial state
init : (Model, Cmd Msg)
init = (MkModel "" "", ?nothing)

||| Update state upon event
update : Msg -> Model -> (Model, Cmd Msg)
update Edited model = (model, ?cmd)

||| Subscriptions to IO replated services
subscriptions : Model -> Sub Msg
subscriptions _ = ?none

||| Display the input boxes along with the result
prompt : Reason -> String -> Html Msg
prompt state ref =
    div [cssClass "passwordbox"]
      [ text "password: "
      , input [onchange Edited] []
      , text "again: "
      , input [onchange Edited] match
      , div reason [text ref]
      ]

  where

    ||| Change password box theme to reflect a difference
    match : List Attribute
    match = case state of
                 DoNotMatch => [cssClass "nomatch"]
                 _          => []

    ||| Display the status of the entry
    reason : List Attribute
    reason = [ case state of
                    DoNotMatch => cssClass "red"
                    TooShort   => cssClass "yellow"
                    Ok         => cssClass "green"
             ]

||| View which builds the page using the model
view : Model -> Html Msg
view (MkModel pass again) =
  case (pass == again, length pass > 8) of
       (_, True)  => prompt TooShort "Too short"
       (False, _) => prompt DoNotMatch "Passwords don't match"
       (True, _)  => prompt Ok "All ok"

||| Program entry
main : JS_IO ()
main = runProgram $ record
  { init = init
  , update = update
  , view = view
  , subscriptions = subscriptions
  } ?default

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
> module FastSimpleProb.MonadicPostulates

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

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

> postulate
> monotoneWorst : {A : Type} ->
>                 (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
>                 (p : (a : A) -> f a `LTE` g a) ->
>                 (sp : SimpleProb A) ->
>                 worst (fmap f sp) `LTE` worst (fmap g sp)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import Data.Vect

add : Int -> Int -> Int
add x y = x + y

xs : Vect 2 Int
xs = [10,20]

ys : Vect 0 Int
ys = []

ErrorOrValue : Bool -> Type
ErrorOrValue False = String
ErrorOrValue True = Double

div : (divisor:Nat) -> (dividend:Nat) -> ErrorOrValue (dividend /= Z)
div divisor Z = "Error: Dividend is zero"
div divisor dividend@(S k) = (cast divisor) / (cast dividend)
--div divisor (S k) = (cast divisor) / (cast (S k))

vtake : (n:Nat) -> Vect (n+m) a -> Vect n a
vtake Z xs = []
vtake (S k) (head::tail) = head :: vtake k tail

mylist : Vect 5 Int
mylist = [1,2,3,4,5]

main : IO ()
main = putStrLn (show (vtake 6 mylist))

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Main

import Data.Vect

StringOrInt: (x: Bool) -> Type
StringOrInt x = case x of
    True => Int
    False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
    True => 94
    False => "Ninety four"

average: (str: String) -> Double
average str = let numWords = wordCount str
                  totalLenght = sum(allLengths (words str)) in
                  cast totalLenght / cast numWords
    where
        wordCount :  String -> Nat
        wordCount str = length (words str)

        allLengths : List String -> List Nat
        allLengths strs = map length strs

double: Num input => input -> input
double input = input + input

twice: (f: a -> a) -> (x: a) -> a
twice f x = f (f x)

palindrome2: String -> Bool
palindrome2 x = toLower x == toLower (reverse x)

palindrome4: Nat -> String -> Bool
palindrome4 len str = if length str > len then palindrome2 str else False

palindrome3: String -> Bool
palindrome3 x = palindrome4 10 x

counts: String -> (Nat, Nat)
counts str = let numOfWords = length (words str)
                 numOfChars = length str in
                    (numOfWords, numOfChars)

top_ten: Ord a => List a -> List a
top_ten list = let sorted = reverse (sort list)
                   topTen = take 10 sorted in
                     topTen

over_length: Nat -> List String -> Nat
over_length len list = length (filter (\x => length(x) > len) list)

allLengths: Vect len String -> Vect len Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

insertList: Ord elem => elem -> (xsSorted : Vect len elem) -> Vect (S len) elem
insertList x [] = [x]
insertList x (y :: xs) = if x < y
    then x :: y :: xs
    else y :: insertList x xs

insSort: Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: tail) =
    let
        sortedTail = insSort tail
        in
            insertList x sortedTail

total my_length: List a -> Nat
my_length [] = 0
my_length (x :: xs) = 1 + my_length xs

total pushToEnd : a -> List a -> List a
pushToEnd x [] = [x]
pushToEnd x (y :: ys) = y :: pushToEnd x ys

total my_reverse: List a -> List a
my_reverse [] = []
my_reverse (x :: xs) =
    let reversed = my_reverse xs
    in pushToEnd x reversed

total my_map: (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs

total my_vect_map: (a -> b) -> Vect n a -> Vect n b
my_vect_map f [] = []
my_vect_map f (x :: xs) = f x :: my_vect_map f xs

total createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

total transposeHelper : (x : Vect n elem) -> (xsTrans : Vect n (Vect len elem)) -> Vect n (Vect (S len) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

total transposeMat: Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) =
    let xsTrans = transposeMat xs
    in transposeHelper x xsTrans

data Direction = North | East | South | West

turnClockwise: Direction -> Direction
turnClockwise North = East
turnClockwise East = South
turnClockwise South = West
turnClockwise West = North

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

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

data BSTree : Type -> Type where
    Leaf : Ord elem => BSTree elem
    Node : Ord elem => (left: BSTree elem) -> (val: elem) -> (right: BSTree elem) -> BSTree elem

total insertTree: elem -> BSTree elem -> BSTree elem
insertTree x Leaf = Node Leaf x Leaf
insertTree x orig@(Node left val right) =
    case compare x val of
        LT => Node (insertTree x left) val right
        EQ => orig
        GT => Node left val (insertTree x right)

listToTree: Ord a => List a -> BSTree a
listToTree [] = Leaf
listToTree (x :: xs) =
    let tailAsTree = listToTree xs
    in insertTree x tailAsTree

treeToList: BSTree a -> List a
treeToList Leaf = []
treeToList (Node left val right) =
    let leftPart = treeToList left
        rightPart = val :: treeToList right
    in leftPart ++ rightPart

data Expr = Val Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mult Expr Expr

total evaluate: Expr -> Int
evaluate (Val value) = value
evaluate (Add l r) = evaluate l + evaluate r
evaluate (Sub l r) = evaluate l - evaluate r
evaluate (Mult l r) = evaluate l * evaluate r

total maxMaybe: Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) =
    let max = if x > y then x else y
    in Just max

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

total biggestTriangle: Picture -> Maybe Double
biggestTriangle (Primitive shape@(Triangle x y)) = Just(area shape)
biggestTriangle (Primitive (Rectangle x y)) = Nothing
biggestTriangle (Primitive (Circle x)) = Nothing
biggestTriangle (Combine left right) =
    let maybeLeft  = biggestTriangle left
        maybeRight = biggestTriangle right
    in maxMaybe maybeLeft maybeRight
biggestTriangle (Rotate _ pic) = biggestTriangle pic
biggestTriangle (Translate _ _ pic) = biggestTriangle pic

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

wheels : Vehicle _ -> Nat
wheels Bicycle = 2
wheels Car = 4
wheels Bus = 4

refuel: Vehicle Petrol -> Vehicle Petrol
refuel (Car _) = Car 100
refuel (Bus _) = Bus 200
refuel Bicycle impossible

append_nil : Vect m elem -> Vect (plus m 0) elem
append_nil {m} xs = rewrite plusZeroRightNeutral m in xs

append_xs : Vect (S (m + len)) elem -> Vect (plus m (S len)) elem
append_xs {m} {len} xs = rewrite sym (plusSuccRightSucc m len) in xs

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)

total my_zip : Vect n a -> Vect n b -> Vect n (a, b)
my_zip [] [] = []
my_zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i vector =
    case integerToFin i n of
        Nothing => Nothing
        (Just idx) => Just (index idx vector)

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

total sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos left right =
    case integerToFin pos n of
        Nothing => Nothing
        (Just x) => let leftVal = index x left
                        rightVal = index x right
                    in Just (leftVal + rightVal)

main : IO ()
main = repl "\n> " reverse

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module BiNat.Properties.Plus

import BiNat

%access public export
%default total

succDashAppendsAcc : (n : BiNat) -> (acc : List Bit) -> succ' n acc = foldl (-:) (succ' n []) acc
succDashAppendsAcc J        acc = Refl
succDashAppendsAcc (n -: O) acc = Refl
succDashAppendsAcc (n -: I) acc =
  rewrite succDashAppendsAcc n (O :: acc) in
  rewrite succDashAppendsAcc n [O] in Refl

predDashAppendsAcc : (n : BiNat) -> (acc : List Bit) -> pred' n acc = foldl (-:) (pred' n []) acc
predDashAppendsAcc J              acc = Refl
predDashAppendsAcc (n -: I)       acc = Refl
predDashAppendsAcc (J -: O)       acc = Refl
predDashAppendsAcc (ns -: n -: O) acc =
  rewrite predDashAppendsAcc (ns -: n) (I :: acc) in
  rewrite predDashAppendsAcc (ns -: n) [I] in Refl

predOfSucc : (n : BiNat) -> pred (succ n) = n
predOfSucc J              = Refl
predOfSucc (n -: O)       = Refl
predOfSucc (J -: I)       = Refl
predOfSucc (ns -: O -: I) = Refl
predOfSucc (ns -: I -: I) =
  rewrite succDashAppendsAcc ns [O, O] in
  rewrite predDashAppendsAcc (succ' ns [] -: O) [I] in
  rewrite sym $ succDashAppendsAcc ns [O] in
  rewrite predOfSucc (ns -: I) in Refl

succOfPred : (n : BiNat) -> Not (n = J) -> succ (pred n) = n
succOfPred J              notJ = absurd (notJ Refl)
succOfPred (n -: I)       _    = Refl
succOfPred (J -: O)       _    = Refl
succOfPred (ns -: I -: O) _    = Refl
succOfPred (ns -: O -: O) _    =
  rewrite predDashAppendsAcc (ns -: O) [I] in
  rewrite succDashAppendsAcc (pred' (ns -: O) []) [O] in
  rewrite succOfPred (ns -: O) uninhabited in Refl

succInjective : (m, n : BiNat) -> succ m = succ n -> m = n
succInjective m n eq =
  rewrite sym $ predOfSucc m in
  rewrite eq in
  predOfSucc n

plusJIsSucc : (n : BiNat) -> plus n J = succ n
plusJIsSucc J         = Refl
plusJIsSucc (ns -: n) = Refl

jPlusIsSucc : (n : BiNat) -> plus J n = succ n
jPlusIsSucc J         = Refl
jPlusIsSucc (ns -: n) = Refl

nextCarrySymmetric : (a, b, c : Bit) -> nextCarry a b c = nextCarry b a c
nextCarrySymmetric O O O = Refl
nextCarrySymmetric O O I = Refl
nextCarrySymmetric O I O = Refl
nextCarrySymmetric O I I = Refl
nextCarrySymmetric I O O = Refl
nextCarrySymmetric I O I = Refl
nextCarrySymmetric I I O = Refl
nextCarrySymmetric I I I = Refl

nextAccSymmetric : (a, b, c : Bit) -> nextAcc a b c = nextAcc b a c
nextAccSymmetric O O O = Refl
nextAccSymmetric O O I = Refl
nextAccSymmetric O I O = Refl
nextAccSymmetric O I I = Refl
nextAccSymmetric I O O = Refl
nextAccSymmetric I O I = Refl
nextAccSymmetric I I O = Refl
nextAccSymmetric I I I = Refl

plusDashSymmetric : (m, n : BiNat) -> (carry : Bit) -> (acc : List Bit) ->
  plus' m n carry acc = plus' n m carry acc
plusDashSymmetric J         J         carry acc = Refl
plusDashSymmetric J         (ns -: n) O     acc = Refl
plusDashSymmetric J         (ns -: n) I     acc = Refl
plusDashSymmetric (ms -: m) J         O     acc = Refl
plusDashSymmetric (ms -: m) J         I     acc = Refl
plusDashSymmetric (ms -: m) (ns -: n) carry acc =
  rewrite nextCarrySymmetric n m carry in
  rewrite nextAccSymmetric n m carry in
  plusDashSymmetric ms ns (nextCarry m n carry) (nextAcc m n carry :: acc)

plusSymmetric : (m, n : BiNat) -> plus m n = plus n m
plusSymmetric m n = plusDashSymmetric m n O []

plusDashAppendsAcc : (m, n : BiNat) -> (carry : Bit) -> (acc : List Bit) ->
  plus' m n carry acc = foldl (-:) (plus' m n carry []) acc
plusDashAppendsAcc J         J         carry acc = Refl
plusDashAppendsAcc J         (ns -: n) O     acc = succDashAppendsAcc (ns -: n) acc
plusDashAppendsAcc J         (ns -: n) I     acc =
  rewrite succDashAppendsAcc ns [n] in
  rewrite succDashAppendsAcc ns (n :: acc) in Refl
plusDashAppendsAcc (ms -: m) J         O     acc = succDashAppendsAcc (ms -: m) acc
plusDashAppendsAcc (ms -: m) J         I     acc =
  rewrite succDashAppendsAcc ms [m] in
  rewrite succDashAppendsAcc ms (m :: acc) in Refl
plusDashAppendsAcc (ms -: m) (ns -: n) carry acc =
  rewrite plusDashAppendsAcc ms ns (nextCarry m n carry) (nextAcc m n carry :: acc) in
  rewrite plusDashAppendsAcc ms ns (nextCarry m n carry) [nextAcc m n carry] in Refl

succGoesToCarry : (m, n : BiNat) -> (acc : List Bit) ->
  succ' (plus' m n O []) acc = plus' m n I acc
succGoesToCarry J         J         acc = Refl
succGoesToCarry (ms -: O) J         acc = Refl
succGoesToCarry (ms -: I) J         acc =
  rewrite succDashAppendsAcc ms [O] in
  rewrite succDashAppendsAcc ms (I :: acc) in Refl
succGoesToCarry J         (ns -: O) acc = Refl
succGoesToCarry J         (ns -: I) acc =
  rewrite succDashAppendsAcc ns [O] in
  rewrite succDashAppendsAcc ns (I :: acc) in Refl
succGoesToCarry (ms -: O) (ns -: O) acc =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite plusDashAppendsAcc ms ns O (I :: acc) in Refl
succGoesToCarry (ms -: O) (ns -: I) acc =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite succGoesToCarry ms ns (O :: acc) in Refl
succGoesToCarry (ms -: I) (ns -: O) acc =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite succGoesToCarry ms ns (O :: acc) in Refl
succGoesToCarry (ms -: I) (ns -: I) acc =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite plusDashAppendsAcc ms ns I (I :: acc) in Refl

succDashCommutesToPlusDashSnd : (m, n : BiNat) -> (acc : List Bit) ->
  succ' (plus m n) acc = plus' m (succ n) O acc
succDashCommutesToPlusDashSnd J         J         acc = Refl
succDashCommutesToPlusDashSnd J         (ns -: O) acc = Refl
succDashCommutesToPlusDashSnd J         (ns -: I) acc =
  rewrite succDashAppendsAcc (succ' ns [O]) acc in
  rewrite plusDashAppendsAcc J (succ' ns [O]) O acc in
  rewrite jPlusIsSucc (succ' ns [O]) in Refl
succDashCommutesToPlusDashSnd (ms -: O) J         acc =
  rewrite succDashAppendsAcc ms (O :: acc) in
  rewrite plusDashAppendsAcc ms J O (O :: acc) in
  rewrite plusJIsSucc ms in Refl
succDashCommutesToPlusDashSnd (ms -: I) J         acc =
  rewrite succDashAppendsAcc ms [O] in
  rewrite sym $ plusJIsSucc ms in
  rewrite plusDashAppendsAcc ms J O (I :: acc) in Refl
succDashCommutesToPlusDashSnd (ms -: O) (ns -: O) acc =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite plusDashAppendsAcc ms ns O (I :: acc) in Refl
succDashCommutesToPlusDashSnd (ms -: O) (ns -: I) acc =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite succDashCommutesToPlusDashSnd ms ns (O :: acc) in
  rewrite succDashAppendsAcc ns [O] in Refl
succDashCommutesToPlusDashSnd (ms -: I) (ns -: O) acc =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite succGoesToCarry ms ns (O :: acc) in Refl
succDashCommutesToPlusDashSnd (ms -: I) (ns -: I) acc =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite sym $ succGoesToCarry ms ns [] in
  rewrite succDashAppendsAcc ns [O] in
  rewrite sym $ succDashCommutesToPlusDashSnd ms ns (I :: acc) in
  rewrite succDashAppendsAcc (plus' ms ns O []) (I :: acc) in Refl

succDashCommutesToPlusDashFst : (m, n : BiNat) -> (acc : List Bit) ->
  succ' (plus m n) acc = plus' (succ m) n O acc
succDashCommutesToPlusDashFst m n acc =
  rewrite plusSymmetric m n in
  rewrite succDashCommutesToPlusDashSnd n m acc in
  rewrite plusDashSymmetric n (succ m) O acc in Refl

plusAssociative : (l, m, n : BiNat) -> plus l (plus m n) = plus (plus l m) n
plusAssociative J         J         J         = Refl
plusAssociative J         J         (ns -: O) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite plusDashAppendsAcc J ns O [O] in
  rewrite jPlusIsSucc ns in Refl
plusAssociative J         J         (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite plusDashAppendsAcc J ns O [I] in
  rewrite jPlusIsSucc ns in Refl
plusAssociative J         (ms -: O) J         = Refl
plusAssociative J         (ms -: I) J         = plusDashSymmetric J (succ' ms [O]) O []
plusAssociative (ls -: O) J         J         =
  rewrite succDashAppendsAcc ls [O] in
  rewrite plusDashAppendsAcc ls J O [O] in
  rewrite plusJIsSucc ls in Refl
plusAssociative (ls -: I) J         J         =
  rewrite succDashAppendsAcc ls [O] in
  rewrite plusDashAppendsAcc ls J O [I] in
  rewrite plusJIsSucc ls in Refl
plusAssociative J         (ms -: O) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite plusDashAppendsAcc ms ns O [I] in Refl
plusAssociative J         (ms -: O) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite sym $ succGoesToCarry ms ns [O] in Refl
plusAssociative J         (ms -: I) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite succDashAppendsAcc (plus' ms ns O []) [O] in
  rewrite sym $ jPlusIsSucc (plus' ms ns O []) in
  rewrite succDashAppendsAcc ms [O] in
  rewrite plusDashAppendsAcc (succ' ms []) ns O [O] in
  rewrite sym $ jPlusIsSucc ms in
  rewrite plusAssociative J ms ns in Refl
plusAssociative J         (ms -: I) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite sym $ succGoesToCarry ms ns [] in
  rewrite succDashAppendsAcc ms [O] in
  rewrite plusDashAppendsAcc (succ' ms []) ns O [I] in
  rewrite sym $ jPlusIsSucc ms in
  rewrite sym $ jPlusIsSucc (plus' ms ns O []) in
  rewrite plusAssociative J ms ns in Refl
plusAssociative (ls -: O) J         (ns -: O) = Refl
plusAssociative (ls -: O) J         (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite plusDashAppendsAcc ls (succ' ns []) O [O] in
  rewrite sym $ plusJIsSucc ns in
  rewrite sym $ succGoesToCarry ls ns [O] in
  rewrite succDashAppendsAcc (plus' ls ns O []) [O] in
  rewrite sym $ plusJIsSucc (plus' ls ns O []) in
  rewrite plusAssociative ls ns J in Refl
plusAssociative (ls -: I) J         (ns -: O) =
  rewrite sym $ succGoesToCarry ls ns [O] in
  rewrite succDashAppendsAcc (plus' ls ns O []) [O] in
  rewrite sym $ jPlusIsSucc (plus' ls ns O []) in
  rewrite succDashAppendsAcc ls [O] in
  rewrite plusDashAppendsAcc (succ' ls []) ns O [O] in
  rewrite sym $ jPlusIsSucc ls in
  rewrite plusAssociative J ls ns in Refl
plusAssociative (ls -: I) J         (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite plusDashAppendsAcc ls (succ' ns []) O [I] in
  rewrite sym $ jPlusIsSucc ns in
  rewrite succDashAppendsAcc ls [O] in
  rewrite plusDashAppendsAcc (succ' ls []) ns O [I] in
  rewrite sym $ plusJIsSucc ls in
  rewrite plusAssociative ls J ns in Refl
plusAssociative (ls -: O) (ns -: O) J         =
  rewrite plusDashAppendsAcc ls ns O [O] in
  rewrite plusDashAppendsAcc ls ns O [I] in Refl
plusAssociative (ls -: O) (ns -: I) J         =
  rewrite succDashAppendsAcc ns [O] in
  rewrite sym $ plusJIsSucc ns in
  rewrite plusDashAppendsAcc ls (plus' ns J O []) O [O] in
  rewrite plusDashAppendsAcc ls ns O [I] in
  rewrite succDashAppendsAcc (plus' ls ns O []) [O] in
  rewrite sym $ plusJIsSucc (plus' ls ns O []) in
  rewrite plusAssociative ls ns J in Refl
plusAssociative (ls -: I) (ns -: O) J         =
  rewrite plusDashAppendsAcc ls ns I [O] in
  rewrite sym $ succGoesToCarry ls ns [] in
  rewrite sym $ plusJIsSucc (plus' ls ns O []) in
  rewrite plusDashAppendsAcc ls ns O [I] in
  rewrite succDashAppendsAcc (plus' ls ns O []) [O] in
  rewrite sym $ plusJIsSucc (plus' ls ns O []) in Refl
plusAssociative (ls -: I) (ns -: I) J         =
  rewrite succDashAppendsAcc ns [O] in
  rewrite plusDashAppendsAcc ls (succ' ns []) O [I] in
  rewrite sym $ plusJIsSucc ns in
  rewrite plusDashAppendsAcc ls ns I [O] in
  rewrite sym $ succGoesToCarry ls ns [] in
  rewrite sym $ plusJIsSucc (plus' ls ns O []) in
  rewrite plusAssociative ls ns J in Refl
plusAssociative (ls -: O) (ms -: O) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite plusDashAppendsAcc ls (plus' ms ns O []) O [O] in
  rewrite plusDashAppendsAcc ls ms O [O] in
  rewrite plusDashAppendsAcc (plus' ls ms O []) ns O [O] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: O) (ms -: O) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite plusDashAppendsAcc ls (plus' ms ns O []) O [I] in
  rewrite plusDashAppendsAcc ls ms O [O] in
  rewrite plusDashAppendsAcc (plus' ls ms O []) ns O [I] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: O) (ms -: I) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite plusDashAppendsAcc ls (plus' ms ns O []) O [I] in
  rewrite plusDashAppendsAcc ls ms O [I] in
  rewrite plusDashAppendsAcc (plus' ls ms O []) ns O [I] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: O) (ms -: I) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite sym $ succGoesToCarry ms ns [] in
  rewrite plusDashAppendsAcc ls ms O [I] in
  rewrite sym $ succGoesToCarry (plus' ls ms O []) ns [O] in
  rewrite sym $ plusAssociative ls ms ns in
  rewrite succDashCommutesToPlusDashSnd ls (plus' ms ns O []) [O] in Refl
plusAssociative (ls -: I) (ms -: O) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite plusDashAppendsAcc ls (plus' ms ns O []) O [I] in
  rewrite plusDashAppendsAcc ls ms O [I] in
  rewrite plusDashAppendsAcc (plus' ls ms O []) ns O [I] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: I) (ms -: O) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite sym $ succGoesToCarry ls (plus' ms ns O []) [O] in
  rewrite plusDashAppendsAcc ls ms O [I] in
  rewrite sym $ succGoesToCarry (plus' ls ms O []) ns [O] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: I) (ms -: I) (ns -: O) =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite sym $ succGoesToCarry ls (plus' ms ns O []) [O] in
  rewrite plusDashAppendsAcc ls ms I [O] in
  rewrite sym $ succGoesToCarry ls ms [] in
  rewrite sym $ succDashCommutesToPlusDashFst (plus' ls ms O []) ns [O] in
  rewrite plusAssociative ls ms ns in Refl
plusAssociative (ls -: I) (ms -: I) (ns -: I) =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite sym $ succGoesToCarry ms ns [] in
  rewrite sym $ succDashCommutesToPlusDashSnd ls (plus' ms ns O []) [I] in
  rewrite plusDashAppendsAcc ls ms I [O] in
  rewrite sym $ succGoesToCarry ls ms [] in
  rewrite sym $ succDashCommutesToPlusDashFst (plus' ls ms O []) ns [I] in
  rewrite plusAssociative ls ms ns in Refl

shiftLeftDoubles : (n : BiNat) -> n -: O = plus n n
shiftLeftDoubles J         = Refl
shiftLeftDoubles (ns -: O) =
  rewrite plusDashAppendsAcc ns ns O [O] in
  rewrite shiftLeftDoubles ns in Refl
shiftLeftDoubles (ns -: I) =
  rewrite plusDashAppendsAcc ns ns I [O] in
  rewrite sym $ succGoesToCarry ns ns [] in
  rewrite sym $ shiftLeftDoubles ns in Refl

succIsNotJ : (n : BiNat) -> Not (succ n = J)
succIsNotJ J         eq = uninhabited eq
succIsNotJ (ns -: O) eq = uninhabited eq
succIsNotJ (ns -: I) eq = uninhabited $ replace {P = \z => z = J} (succDashAppendsAcc ns [O]) eq

predOfDoubled : (n : BiNat) -> Not (n = J) -> pred (n -: O) = pred n -: I
predOfDoubled J notJ = absurd $ notJ Refl
predOfDoubled (ns -: O) _ = predDashAppendsAcc (ns -: O) [I]
predOfDoubled (ns -: I) _ = Refl

predCommutesToPlusSnd : (m, n : BiNat) -> Not (n = J) ->
  pred (plus m n) = plus m (pred n)
predCommutesToPlusSnd J         n notJ =
  rewrite jPlusIsSucc n in
  rewrite predOfSucc n in
  rewrite jPlusIsSucc (pred n) in
  rewrite succOfPred n notJ in Refl
predCommutesToPlusSnd (ms -: m) n notJ =
  rewrite sym $ succOfPred (ms -: m) uninhabited in
  rewrite sym $ jPlusIsSucc (pred (ms -: m)) in
  rewrite sym $ plusAssociative J (pred (ms -: m)) n in
  rewrite jPlusIsSucc (plus (pred (ms -: m)) n) in
  rewrite predOfSucc (plus (pred (ms -: m)) n) in
  rewrite plusSymmetric J (pred (ms -: m)) in
  rewrite sym $ plusAssociative (pred (ms -: m)) J (pred n) in
  rewrite jPlusIsSucc (pred n) in
  rewrite succOfPred n notJ in Refl

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
module Cordial.Model.Common.Widths

import public Data.List

import Data.Ranged
import Data.So
import Cordial.Model.Common.Essential
import Cordial.Model.Common.Whole
import Cordial.Model.Common.Hacks
import Cordial.Model.Common.WireTy

%default total
%access public export

data CanBeOne : WireTy -> Type where
  ClockIsOne     : CanBeOne (Clock a b c)
  ResetIsOne     : CanBeOne Reset
  InterruptIsOne : CanBeOne Interrupt
  ControlIsOne   : CanBeOne (Control)

data PortWidthDesc : PortShape -> Type where
  UserDefined : PortWidthDesc shape
  One   : PortWidthDesc WIRE
  Width : (w : Whole) -> IsGreaterThanOne w -> PortWidthDesc ARRAY

data HasWidth : PortWidthDesc shape -> Type where
  HasWidthOne : HasWidth One
  HasWidthW : HasWidth (Width w prf)

fromNat : (x : Nat)
       -> {auto prfN : IsSucc x}
       -> (ty ** PortWidthDesc ty)
fromNat x {prfN} with (prfN)
  fromNat (S n) {prfN = prfN} | ItIsSucc with (n)
    fromNat (S n) {prfN = prfN} | ItIsSucc | Z = (WIRE ** One)
    fromNat (S n) {prfN = prfN} | ItIsSucc | (S k) with (isGreaterThanOne $ W (S (S k)) ItIsSucc)
      fromNat (S n) {prfN = prfN} | ItIsSucc | (S k) | (Yes prf) = (ARRAY ** Width (W (S (S k)) ItIsSucc) prf)
      fromNat (S n) {prfN = prfN} | ItIsSucc | (S k) | (No contra) = (WIRE ** One)

namespace Array
  data ValidInt : Int -> Type where
    IsValid : (prfSucc : IsSucc (cast {to=Nat} i))
           -> (prfGT1  : IsGreaterThanOne (W (cast {to=Nat} i) prfSucc))
           -> ValidInt i

  fromInteger : (i : Int)
            -> {auto prf : ValidInt i}
            -> PortWidthDesc ARRAY
  fromInteger i {prf = (IsValid prfSucc prfGT1)} =
    Width (W (cast {to=Nat} i) prfSucc) prfGT1

  fromWhole : (w : Whole)
           -> (prf : IsGreaterThanOne w)
           -> (PortWidthDesc ARRAY)
  fromWhole w prf = Width w prf

  fromNat : (n : Nat)
         -> {auto prfSucc : IsSucc n}
         -> {auto prfGT1  : IsGreaterThanOne (W n prfSucc)}
         -> PortWidthDesc ARRAY
  fromNat n {prfSucc} {prfGT1} = Width (W n prfSucc) prfGT1

  fromDouble : (d : Double)
            -> {auto prfSucc : IsSucc (Hacks.fromDoubleToNat d)}
            -> {auto prfGT1  : IsGreaterThanOne (W (Hacks.fromDoubleToNat d) prfSucc)}
            -> PortWidthDesc ARRAY
  fromDouble d {prfSucc} {prfGT1} = Width (W (Hacks.fromDoubleToNat d) prfSucc) prfGT1

  namespace AtLeastTwo
    fromNat : (n : Nat)
           -> (prfSucc : IsSucc n)
           -> (prfG2 : LTE 2 n)
           -> PortWidthDesc ARRAY
    fromNat (S k) ItIsSucc prfG2 = Width (W (S k) ItIsSucc) (IsGT1 prfG2)

toNat : PortWidthDesc kind -> Nat
toNat UserDefined = 0
toNat One = 1
toNat (Width x _) = toNat x

Cast (PortWidthDesc kind) Nat where
  cast = toNat

Show (PortWidthDesc kind) where
  show UserDefined = show 0
  show One = show 1
  show (Width w x) = show w

namespace Value
  data PortWidth : (shape : PortShape)
                -> (spec  : PortWidthDesc shape)
                -> Type
    where
      One   : PortWidth WIRE One
      Width : (w : Whole)
            -> PortWidth ARRAY (Width w prf)
      UserDef : (w : Whole) -> PortWidth shape UserDefined

  fromNat : (n : Nat)
         -> {auto prfN : IsSucc n}
         -> (spec : PortWidthDesc shape)
         -> PortWidth shape spec
  fromNat n spec {prfN} with (spec)
    fromNat n spec {prfN = prfN} | UserDefined = UserDef (W n prfN)
    fromNat n spec {prfN = prfN} | One = One
    fromNat n spec {prfN = prfN} | (Width w x) = Width w

  fromWhole : (w : Whole)
           -> (spec : PortWidthDesc shape)
           -> PortWidth shape spec
  fromWhole w spec with (spec)
    fromWhole w spec | UserDefined = UserDef w
    fromWhole w spec | One = One
    fromWhole w spec | (Width x y) = Width x

namespace FromArraySpec
  data ValidArraySpec : (w : Nat)
                     -> (ws : List Nat)
                     -> Type
    where
      IsValid : (prfInSet   : Elem w ws)
             -> (prfNotZero : IsSucc w)
             -> (prfNotOne  : IsGreaterThanOne (W w prfNotZero))
             -> ValidArraySpec w ws

  fromNat : (n : Nat)
         -> (prf : ValidArraySpec n ns)
         -> PortWidthDesc ARRAY
  fromNat n {prf = (IsValid prfInSet prfNotZero prfNotOne)} =
     Width (W n prfNotZero) prfNotOne

  widthIsZero : (contra : IsSucc w -> Void) -> ValidArraySpec w ws -> Void
  widthIsZero contra (IsValid prfInSet prfNotZero prfNotOne) = contra prfNotZero

  widthNotInList : (contra : Elem w ws -> Void) -> ValidArraySpec w ws -> Void
  widthNotInList contra (IsValid prfInSet prfNotZero prfNotOne) = contra prfInSet

  widthIsOne : (contra : IsGreaterThanOne (W (S n) ItIsSucc) -> Void) -> ValidArraySpec (S n) ws -> Void
  widthIsOne contra (IsValid prfInSet ItIsSucc (IsGT1 x)) = contra (IsGT1 x)

  validArraySpec : (w : Nat) -> (ws : List Nat)
                -> Dec (ValidArraySpec w ws)
  validArraySpec w ws with (isItSucc w)
    validArraySpec w ws | (Yes prf) with (isGreaterThanOne (W w prf))
      validArraySpec w ws | (Yes prf) | (Yes x) with (isElem w ws)
        validArraySpec w ws | (Yes prf) | (Yes x) | (Yes y) = Yes (IsValid y prf x)
        validArraySpec w ws | (Yes prf) | (Yes x) | (No contra) = No (widthNotInList contra)

      validArraySpec (S n) ws | (Yes ItIsSucc) | (No contra) = No (widthIsOne contra)

    validArraySpec w ws | (No contra) = No (widthIsZero contra)

   namespace Hint
     %hint
     validArraySpec : (w : Nat) -> (ws : List Nat)
                   -> {auto prfElem : Elem w ws}
                   -> {auto prfSucc : IsSucc w}
                   -> {auto prfGT1  : IsGreaterThanOne (W w prfSucc)}
                   -> ValidArraySpec w ws
     validArraySpec w ws {prfElem} {prfSucc} {prfGT1} = IsValid prfElem prfSucc prfGT1

namespace FromDouble
   fromDouble : (d : Double)
             -> (shape ** PortWidthDesc shape)
   fromDouble d with (fromDoubleToNat d)
     fromDouble d | Z = (WIRE ** One)
     fromDouble d | (S k) = (WIRE ** One)
     fromDouble d | (S (S k)) = fromNat (S (S k)) {prfN=ItIsSucc}

{-
  fromDouble : (d : Double)
            -> {auto prfSucc : IsSucc (fromDoubleToNat d)}
            -> {auto prfGT1  : IsGreaterThanOne (W (fromDoubleToNat d) prfSucc)}
            -> PortWidthDesc ARRAY
  fromDouble d {prfSucc} {prfGT1} = Width (W (fromDoubleToNat d) prfSucc) prfGT1

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Test.TomlTest

import IdrTest.Test
import IdrTest.Expectation

import Toml

parseSpecs : List (String, Maybe Toml)
parseSpecs =
  [
    (
      "hello=\"world\"",
      Just [(["hello"], Str "world")]
    ),
    (
      "hello=\"wor\\nld\"",
      Just [(["hello"], Str "wor\nld")]
    ),
    (
      "count=55",
      Just [(["count"], Num 55)]
    ),
    (
      "count=[55, [66 ,\"dog\"]]",
      Just [(["count"], Lst [Num 55,Lst [Num 66, Str "dog"]])]
    ),
    (
      "count=[\n55, \n66 ,77\n]",
      Just [(["count"], Lst [Num 55, Num 66, Num 77])]
    ),
    (
      "[x]\ny=55",
      Just [(["x", "y"], Num 55)]
    ),
    (
      "[x-z]\ny=55",
      Just [(["x-z", "y"], Num 55)]
    ),
    (
      "5=55",
      Just [(["5"], Num 55)]
    ),
    (
      "[\"x.y\"]\n\"z.z\"=55",
      Just [(["x.y", "z.z"], Num 55)]
    ),
    (
      "[a]\nb=1\n[c]\nd=1\ne=1",
      Just [
        (["a", "b"], Num 1),
        (["c", "d"], Num 1),
        (["c", "e"], Num 1)
      ]
    ),
    (
      "[a]\nb=1\nc.d=2\n[e.f]\ng=3",
      Just [
        (["a", "b"], Num 1),
        (["a", "c", "d"], Num 2),
        (["e", "f", "g"], Num 3)
      ]
    ),
    (
      "[[a]]\nb=1\nc=2\nd.e=3\n[[a]]\nb=3\nc=4\n[a.d]\ne=5",
      Just [
        (["a"], ArrTab [
          [ (["b"], Num 1)
          , (["c"], Num 2)
          , (["d", "e"], Num 3)
          ],
          [ (["b"], Num 3)
          , (["c"], Num 4)
          , (["d", "e"], Num 5)
          ]
        ])
      ]
    ),
    (
      "[cool]
description=\"cool package\"
version=\"1.2.3\"
[funk]
description=\"funky package\"
version=\"10.0.0\"",
      Just [
        (["cool", "description"], Str "cool package"),
        (["cool", "version"], Str "1.2.3"),
        (["funk", "description"], Str "funky package"),
        (["funk", "version"], Str "10.0.0")
      ]
    )
  ]

encodeSpecs : List (Toml, String)
encodeSpecs =
  [
    (
      [(["hello"], Str "world")],
      "hello=\"world\""
    ),
    (
      [(["hello.world"], Str "cool")],
      "\"hello.world\"=\"cool\""
    ),
    (
      [(["hello=world"], Str "cool")],
      "\"hello=world\"=\"cool\""
    ),
    (
      [(["count"], Num 55)],
      "count=55"
    ),
    (
      [(["deep","count"], Num 55)],
      "deep.count=55"
    ),
    (
      [
        (["a"], ArrTab [
          [ (["b"], Num 1)
          , (["c"], Num 2)
          , (["d", "e"], Num 3)
          ],
          [ (["b"], Num 3)
          , (["c"], Num 4)
          , (["d", "e"], Num 5)
          ]
        ])
      ],
      "[[a]]\nb=1\nc=2\nd.e=3\n\n[[a]]\nb=3\nc=4\nd.e=5"
    )
  ]

getSpecs : List (Toml, List String, Maybe Value)
getSpecs =
  [
    (
      [(["hello"], Str "world")],
      ["hello"],
      Just (Str "world")
    ),
    (
      [(["count"], Num 55)],
      ["count"],
      Just (Num 55)
    ),
    (
      [(["count"], Num 55)],
      ["butter"],
      Nothing
    ),
    (
      [(["count"], Num 55)],
      ["count", "more"],
      Nothing
    ),
    (
      [(["count"], Num 55)],
      [],
      Nothing
    ),
    (
      [(["deep","count"], Num 55)],
      ["deep", "count"],
      Just (Num 55)
    )
  ]

export
suite : Test
suite =
  let
    parseTests =
      map (\(text, result) =>
        test text (\_ => assertEq (parseToml text) result)
      ) parseSpecs

    encodeTests =
      map (\(toml, exp) =>
        test exp (\_ => assertEq (encode toml) exp)
      ) encodeSpecs

    getTests =
      map (\(toml, keys, exp) =>
        test ("Getting " ++ show keys ++ " from " ++ show toml) (\_ => assertEq (get keys toml) exp)
      ) getSpecs
  in
    describe "Toml Tests"
      [ describe "Parser Specs" parseTests
      , describe "Encoder Specs" encodeTests
      , describe "Get Specs" getTests
      ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module UserApi

import Control.Monad.Freer
import Debug.Trace
import Control.Monad.Id

%access public export
%default total

data Tensor : Type where
  DoubleT : Double -> Tensor

implementation Show Tensor where
  show (DoubleT x) = show x

-- temporary
data Shape

data GraphData : Type -> Type where
  Mul : Tensor -> Tensor -> GraphData Tensor
  Placeholder : GraphData Tensor
  Constant : Double -> GraphData Tensor

FreeGraph : Type --type of computation graph ,freer graph
FreeGraph = Freer GraphData Tensor

implicit gt2fg : GraphData Tensor -> FreeGraph
gt2fg = liftF

newPlaceholder : FreeGraph
newPlaceholder = liftF Placeholder

exampleGraph : FreeGraph
exampleGraph = do
  t<-newPlaceholder
  a<-liftF Placeholder -- same
  b<-Placeholder -- same
  liftF (Mul t a)

const1 : GraphData Tensor
const1 = Constant 1

mulG : FreeGraph
mulG = do
  x<-liftF $ Constant 1
  y<-liftF $ Constant 3
  liftF $ Mul x y

numericGradId : {x : Type}->  GraphData Tensor->GraphData x -> Id x
numericGradId Placeholder (Mul x y) =  pure $ DoubleT  2.0
numericGradId (Constant z) (Mul (DoubleT x) (DoubleT y)) =
  let res : Double =(x*y + 0.1)/(z+0.1) in
  pure $ trace (show z ++ "," ++show x) $ DoubleT res
numericGradId (Mul x y) (Mul (DoubleT z) (DoubleT w)) = pure $ DoubleT 3.0
numericGradId _ (Constant x) = pure $ DoubleT 3.0
numericGradId _ Placeholder = pure $ DoubleT 4.0

mainGradId : Id String
mainGradId = do
  x <- (foldFreer ((trace "xxx" numericGradId) const1) mulG)
  --print x
  pure $ show x

max_stars_repo_name: justjoheinz/tensorflow-idris

max_issues_repo_name: justjoheinz/tensorflow-idris

max_forks_repo_name: justjoheinz/tensorflow-idris


text:
module Resumption

{-
data Res a = Done a | Pause (Res a)
-}

data Res : Type -> Type where
  Done  : a -> Res a
  Pause : (Res a) -> (Res a)

instance Functor Res where
  map f (Done a)  = Done (f a)
  map f (Pause r) = Pause (map f r)

instance Applicative Res where
  pure a            = Done a
  (Done f)  <$> res = map f res
  (Pause p) <$> res = p <$> res

instance Monad Res where
  (Done a)  >>= f = f a
  (Pause a) >>= f = a >>= f

{-
data React i o a = Done a | Pause o (i -> o)
-}

data React : Type -> Type -> Type -> Type where
  D : a -> React i o a
  P : o -> (i -> React i o a) -> React i o a

instance Functor (React i o) where
  map f (D a)   = D (f a)
  map f (P o r) = P o (\i => map f (r i))

instance Applicative (React i o) where
  pure a = D a
  (D f)   <$> res = map f res
  (P o f) <$> res = P o (\i => (f i) <$> res)

instance Monad (React i o) where
  (D a)   >>= f = f a
  (P o r) >>= f = P o (\i => (r i) >>= f)

par : React i o a -> React j n a -> React (i,j) (o,n) a
par (D a) _ = D a
par _ (D a) = D a
par (P o r1) (P n r2) = P (o,n) (\(i1,i2) => par (r1 i1) (r2 i2))

refold : (o1 -> o2) -> (i2 -> o1 -> i1) -> React i1 o1 a -> React i2 o2 a
refold _ _ (D a)      = D a
refold fo fi (P o ii) = P (fo o) (\i2 => refold fo fi (ii (fi i2 o)))

parvect : React (Vect k s) (Vect k' t) a ->
          React (Vect n s) (Vect n' t) a ->
          React (Vect (k+n) s) (Vect (k'+n') t) a
parvect (D a) _ = D a
parvect _ (D a) = D a
parvect {k} (P ol r1) (P or r2) = P (ol ++ or) (\i => let (i1,i2) = splitAt k i
                                                   in parvect (r1 i1) (r2 i2))

max_stars_repo_name: igraves/draconis-resumptions

max_issues_repo_name: igraves/draconis-resumptions

max_forks_repo_name: igraves/draconis-resumptions


text:
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

Name : Type
Name = String

showParen : String -> String
showParen x = "(" ++ x ++ ")"

data Tm
  = Var Name           -- x
  | Lam Name Tm        -- \x. t
  | App Tm Tm          -- t u
  | Let Name Tm Tm     -- let x = t in u
Show Tm where
  show (Var str) = str
  show (Lam x t) = showParen ("λ" ++ x ++ "." ++ show t)
  show (App t u) = showParen ("" ++ show t ++ " " ++ show u)
  show (Let str tm1 tm2) = showParen ("Let " ++ str ++ " = " ++ show tm1 ++ " in " ++ show tm2)

-- parsing

keyword : String -> Bool
keyword x = x == "λ" || x == "in" || x == "let"

pIdent' : Parser Name
pIdent' = do f <- satisfy (isAlphaNum)
             i <- many (satisfy isAlphaNum)
             pure (pack (f :: i)) <* spaces

pIdent : Parser Name
pIdent = do
  str <- pIdent'
  guard (not (keyword str))
  pure str

pBind : Parser Name
pBind = pIdent <|> (token "_" *> pure "_")

mutual
  pAtom : Parser Tm
  pAtom = (Var <$> pIdent) <|> parens pTm -- what's `<$>` doing here?

  pTm : Parser Tm
  pTm = pLet <|>| pLam <|>| pSpine

  pLam : Parser Tm
  pLam = do
    char 'λ' <|> char '\\'
    xs <- some pBind
    token "."
    t <- pTm
    pure (foldr Lam t xs)

  pLet : Parser Tm
  pLet = do
    token "let"
    x <- pBind
    token "="
    t <- pTm
    token "in"
    u <- pTm
    pure $ Let x t u

  pSpine : Parser Tm
  pSpine = foldl1 App <$> some pAtom

-- evaluation

data Val
  = VVar Name
  | VApp Val Val
  | VLam Name (Val -> Val)

Env : Type
Env = List (Name, Maybe Val)

fresh : Env -> Name -> Name
fresh env "_" = "_"
fresh env x = case lookup x env of
                   Nothing => x
                   (Just _) => fresh env (x ++ "'")

eval : Env -> Tm -> Val
eval env (Var x) = let findX = lookup x env in
                       (case findX of
                             Nothing => VVar x
                             (Just x') => (case x' of
                                                Nothing => VVar x
                                                (Just x'') => x''))
eval env (App t u) = let evalT = eval env t
                         evalU = eval env u
                         in
                         (case evalT of
                               (VLam _ f) => f evalU
                               _ => VApp evalT evalU)
eval env (Lam x t) = VLam x (\u => eval ((x, Just u)::env) t)
eval env (Let x t u) = let nextEnv = Just (eval env t) in
                           eval ((x, nextEnv)::env) u

quote : Env -> Val -> Tm
quote env (VVar x) = Var x
quote env (VApp t u) = App (quote env t) (quote env u)
quote env (VLam x t) = let freshX = fresh env x in
                           Lam freshX (quote ((x, Nothing)::env) (t (VVar x)))
nf : Env -> Tm -> Tm
nf env = let qe = quote env
             ee = eval env in
             qe . ee

test : Maybe Tm
test = let parsed = (Lightyear.Strings.parse (pTm) "let five = \\s z. s (s (s (s (s z)))) in let add = \\a b s z. a s (b s z) in let mul = \\a b s z. a (b s) z in let ten = add five five in let hundred = mul ten ten in let thousand = mul ten hundred in let tenthousand = mul ten thousand in tenthousand") in
           (case parsed of
                 (Left l) => Nothing
                 (Right r) => Just (nf [] r))

test2 : Maybe Tm
test2 = let parsed = (Lightyear.Strings.parse (pTm) "let true = (\\x y. x) in let false = (\\x y. y) in let and = (\\x y. (x (y true false) false)) in let or = (\\x y. (x true (y true false))) in or false true") in
           (case parsed of
                 (Left l) => Nothing
                 (Right r) => Just (nf [] r))

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
module Main

main : IO ()
main = do
  printLn $ prim_lenString "hallo"
  printLn $ prim_lenString "1"
  printLn $ prim_lenString ""

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
> module Fun.Operations

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

> |||
> pair : (a -> b, a -> c) -> a -> (b, c)
> pair (f, g) x = (f x, g x)

> |||
> cross : (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> cross f g (x, y) = (f x, g y)

> |||
> modifyFun : {a : Type} -> {b : Type} -> (Eq a) =>
>             (a -> b) -> a -> b -> (a -> b)
> modifyFun f a b a' = if a' == a then b else f a'


text:
main : JS_IO ()
main = putStr' $ show 66

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Test.Inigo.Package.PackageIndexTest

import IdrTest.Test
import IdrTest.Expectation

import Data.List
import Inigo.Async.Promise
import Inigo.Package.PackageIndex
import SemVar.Data
import Test.Inigo.Package.PackageTest
import Toml

exampleIndexToml : String
exampleIndexToml = """
[[pkg]]
ns=\"Example\"
package=\"Cool\"
description=\"cool package\"
version=\"1.2.3\"

[[pkg]]
ns=\"Example\"
package=\"Funk\"
description=\"funky package\"
version=\"10.0.0\"
"""

exampleIndex : PackageIndex
exampleIndex =
  [ MkPackageMeta "Example" "Cool" (Just "cool package") (MkVersion 1 2 3 Nothing Nothing)
  , MkPackageMeta "Example" "Funk" (Just "funky package") (MkVersion 10 0 0 Nothing Nothing)
  ]

exampleIndexExp : PackageIndex
exampleIndexExp =
  [ MkPackageMeta "Example" "Cool" (Just "cool package") (MkVersion 1 2 3 Nothing Nothing)
  , MkPackageMeta "Example" "Inigo" (Just "what pkg") (MkVersion 0 10 0 Nothing Nothing)
  , MkPackageMeta "Example" "Funk" (Just "funky package") (MkVersion 10 0 0 Nothing Nothing)
  ]

exampleInigoMeta : PackageMeta
exampleInigoMeta =
  MkPackageMeta "Example" "Inigo" (Just "My Description") (MkVersion 0 0 1 (Just "pre") Nothing)

toTomlTest : Test
toTomlTest =
  test "To Toml" (\_ => assertEq
    (toToml exampleIndex)
    [(["pkg"],
      ArrTab
        [
          [ (["ns"], Str "Example")
          , (["package"], Str "Cool")
          , (["description"], Str "cool package")
          , (["version"], Str "1.2.3")
          ],
          [ (["ns"], Str "Example")
          , (["package"], Str "Funk")
          , (["description"], Str "funky package")
          , (["version"], Str "10.0.0")
          ]
        ]
    )]
  )

encodePackageIndexTest : Test
encodePackageIndexTest =
  test "Encode package index" (\_ => assertEq
    (encodePackageIndex exampleIndex)
    exampleIndexToml
  )

toPackageMetaTest : Test
toPackageMetaTest =
  test "fromPackage" (\_ => assertEq
    (fromPackage examplePackage)
    exampleInigoMeta
  )

updatePackageMetaNewTest : Test
updatePackageMetaNewTest =
  test "updatePackageMeta New Package" (\_ => assertEq
    (
      updatePackageMeta
        exampleIndex
        examplePackage
    )
    (snoc exampleIndex exampleInigoMeta)
  )

updatePackageMetaExistingTest : Test
updatePackageMetaExistingTest =
  test "updatePackageMeta Existing Package" (\_ => assertEq
    (
      updatePackageMeta
        exampleIndexExp
        examplePackage
    )
    [ MkPackageMeta "Example" "Cool" (Just "cool package") (MkVersion 1 2 3 Nothing Nothing)
    , MkPackageMeta "Example" "Inigo" (Just "My Description") (MkVersion 0 0 1 (Just "pre") Nothing)
    , MkPackageMeta "Example" "Funk" (Just "funky package") (MkVersion 10 0 0 Nothing Nothing)
    ]
  )

export
suite : Test
suite =
  describe "Package Index"
    [ test "Parse Example Index" (\_ => assertEq
        (parsePackageIndex exampleIndexToml)
        (Right exampleIndex)
      )
    , test "Search Index" (\_ => assertEq
        (((map $ searchPackageIndex "fun") . parsePackageIndex) exampleIndexToml)
        (Right $
          [ MkPackageMeta "Example" "Funk" (Just "funky package") (MkVersion 10 0 0 Nothing Nothing)
          ]
        )
      )
    , toTomlTest
    , encodePackageIndexTest
    , toPackageMetaTest
    , updatePackageMetaNewTest
    , updatePackageMetaExistingTest
    ]


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

export
program : PrintString m => CanSleep m => Zippable m => m ()
program = do
  offset <- currentTime
  printTime offset "start"
  ignore $ zip
    (for 5 $ do
      printTime offset "proc 1, before 1000"
      sleepFor 1.seconds
      printTime offset "proc 1, before 2000"
      sleepFor 2.seconds)
    (for 10 $ do
      printTime offset "                     proc 2, before 350"
      sleepFor 350.millis
      printTime offset "                     proc 2, before 750"
      sleepFor 750.millis)
  printTime offset "end"


text:
module Genesis

NamePath : Type
NamePath = List String

data CoreCommand : Type where
  --this needs to be private so that only genesis can run it
  AlterCommand : {type : Type} -> (namePath : NamePath) -> (value : type) -> CoreCommand

Coins : Type
Coins = Integer

PubKey : Type
PubKey = Int

UpdateIndex : Type
UpdateIndex = Integer

--note that the address is the reference to the account, ex. 'timsAccount'
record Account where
  constructor MkAccount
  bal : Coins
  pubKey : PubKey
  updInd : UpdateIndex -- increments for every update

timsAccount : Account
timsAccount = MkAccount 100 123456789101112 0

ccsAccount : Account
ccsAccount = MkAccount 50 1122334455 0

--TODO we need to make a compiler time function that translates a name
-- to a reference
--a reference to an object
data Ref : Type -> Type where
  MkRef : NamePath -> (t: Type) -> Ref t

--TODO
--This should return the value of a given reference, for example 'timsAccount'
--If the type doesn't match, a compiler error will result
getRefValue : Ref type -> type

Signature : Type
Signature = Int

--This verifies a transfer funds signature is valid
--The signature should sign
-- * fromName
-- * toName
-- * amt
-- * from updInd
-- TODO 3 the updInd prevents a txn from being reused multiple times, but
--  it limits one txn per from account per block unless the miner can order
--  the txns (which is a fair amount of work)
verifySigTransferFunds : (sig : Signature) -> (from : Ref Account) -> (to : Ref account) -> (amt : Coins) -> Bool
verifySigTransferFunds _ _ _ _ = True -- TODO 2 implement

-- verifies no negative balance
verifySufficientFunds : Account -> Coins -> Bool
verifySufficientFunds acct amt = True -- (bal acct) >= amt

transferFunds : (from : Ref Account) -> (to : Ref Account) -> (amt : Coins) -> (sig : Signature) -> verifySigTransferFunds sig from to amt = True -> verifySufficientFunds (getRefValue from) amt = True -> List CoreCommand  --TODO 2 CoreCommand should probably be a monad
transferFunds from to amt _ _ _ =
  let
    fromAccount = getRefValue from
    toAccount = getRefValue to
    (MkRef fromName _) = from
    (MkRef toName _) = to
    newFromAccount = record { bal = (bal fromAccount) - amt, updInd $= (+1) } fromAccount
    newToAccount = record { bal = (bal toAccount) - amt, updInd $= (+1) } toAccount
    in
      [ AlterCommand fromName newFromAccount
        ,AlterCommand fromName newToAccount ]

--TODO 2 to create new accounts, transfer funds to them
--transferFundsToNewAccount : (from : Ref Account) -> (to : Ref Account) -> (amt : Coins) -> (sig : Signature) -> verifySigTransferFunds sig from to amt = True -> verifySufficientFunds (getRefValue from) amt = True -> List CoreCommand  --TODO 2 CoreCommand should probably be a monad
-- transferFunds from to amt _ _ _ =
--   let
--     fromAccount = getRefValue from
--     toAccount = getRefValue to
--     (MkRef fromName _) = from
--     (MkRef toName _) = to
--     newFromAccount = record { bal = (bal fromAccount) - amt, updInd $= (+1) } fromAccount
--     newToAccount = record { bal = (bal toAccount) - amt, updInd $= (+1) } toAccount
--     in
--       [ AlterCommand fromName newFromAccount
--         ,AlterCommand fromName newToAccount ]

-- --   [ AlterCommand fromName Account (MkAccount ((bal (getRefValue fromName)) - amt) (

--pretend block txn
lunchMoney : List CoreCommand
lunchMoney = transferFunds (MkRef [ "timsAccount" ] Account)
                           (MkRef [ "ccsAccount" ] Account)
                           10
                           0
                           Refl
                           Refl


text:
module Isomorphism

import TypesAndFunctions
import public Category

%default total

public export
IsInverse : {cat : Category} -> {a, b: Object cat} ->
    Morphism cat a b -> Morphism cat b a -> Type
IsInverse f g = (g .* f = catId a, f .* g = catId b)

public export
IsIsomorphism : {cat : Category} -> {a, b: Object cat} ->
  Morphism cat a b -> Type
IsIsomorphism f = DPair (Morphism cat b a) (Isomorphism.IsInverse f)

public export
Isomorphic : {cat : Category} -> (a, b: Object cat) -> Type
Isomorphic a b = DPair (Morphism cat a b) IsIsomorphism

public export
inversePostComposeIsPostComposeInverse :
  {cat : Category} -> {a, b, c : Object cat} ->
  (f : Morphism cat b c) ->
  (isIsomorphism : IsIsomorphism {cat} {a=b} {b=c} f) ->
  IsBijection (postCompose {cat} {a} {b} {c} f)
inversePostComposeIsPostComposeInverse f (fInv ** (isLeftInv, isRightInv)) =
  (postCompose fInv **
   (\g =>
     let
       assoc = Associativity cat fInv f g
       cancelInverse =
         replace {p=(\f' => After cat f' g = After cat fInv (After cat f g))}
           isLeftInv assoc
       cancelId =
         replace {p=(\g' => g' = After cat fInv (After cat f g))}
           (LeftIdentity cat g) cancelInverse
     in
     sym cancelId,
    \g =>
     let
       assoc = Associativity cat f fInv g
       cancelInverse =
         replace {p=(\f' => After cat f' g = After cat f (After cat fInv g))}
           isRightInv assoc
       cancelId =
         replace {p=(\g' => g' = After cat f (After cat fInv g))}
           (LeftIdentity cat g) cancelInverse
     in
     sym cancelId))

public export
inversePreComposeIsPreComposeInverse :
  {cat : Category} -> {a, b, c : Object cat} ->
  (f : Morphism cat a b) ->
  (isIsomorphism : IsIsomorphism {cat} {a} {b} f) ->
  IsBijection (preCompose {cat} {a} {b} {c} f)
inversePreComposeIsPreComposeInverse f (fInv ** (isLeftInv, isRightInv)) =
  (preCompose fInv **
   (\g =>
     let
       assoc = Associativity cat g f fInv
       cancelInverse =
         replace {p=(\f' => After cat (After cat g f) fInv = After cat g f')}
           isRightInv assoc
       cancelId =
         replace {p=(\g' => After cat (After cat g f) fInv = g')}
           (RightIdentity cat g) cancelInverse
     in
     cancelId,
    \g =>
     let
       assoc = Associativity cat g fInv f
       cancelInverse =
         replace {p=(\f' => After cat (After cat g fInv) f = After cat g f')}
           isLeftInv assoc
       cancelId =
         replace {p=(\g' => After cat (After cat g fInv) f = g')}
           (RightIdentity cat g) cancelInverse
     in
     cancelId))

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
-- --------------------------------------------------------------- [ DVect.idr ]
-- Module    : DVect.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A `list` construct to create lists of dependent types.
|||
||| One of the problems with using dependent types is that types
||| depend on values. This affects the ability to construct lists of
||| values that have a dependent type. The existing `List` type cannot
||| be used as it requires all elements to have the same type.
module Data.DVect

import Data.Vect

%access export

using (aTy : Type, elemTy : (aTy -> Type), x : aTy)

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @len    The length of the list.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export
  data DVect : (aTy : Type)
                -> (len : Nat)
                -> (elemTy : aTy -> Type)
                -> (as : Vect len aTy)
                -> Type where
    ||| Create an empty List
    Nil  : DVect aTy Z elemTy Nil
    ||| Cons
    |||
    ||| @elem The element to add
    ||| @rest The list for `elem` to be added to.
    (::) : (elem : elemTy x)
        -> (rest : DVect aTy n elemTy xs)
        -> DVect aTy (S n) elemTy (x::xs)

-- -------------------------------------------------------------- [ Form Tests ]
isNil : DVect aTy n eTy as -> Bool
isNil Nil     = True
isNil (x::xs) = False

isCons : DVect aTy n eTy as -> Bool
isCons l = isNil l == False

-- ------------------------------------------------------------------ [ Length ]

length : DVect aTy n eTy as -> Nat
length {n} _ = n

-- ---------------------------------------------------------------- [ Indexing ]

{- TODO Safely Index the List

index : (n : Nat)
     -> (l : DVect aTy eTy as)
     -> (ok : lt n (length l) = True)
     -> (a : aTy ** eTy a)
index Z     (x::xs) p    = (_ ** x)
index (S n) (x::xs) p    = index n xs ...
index _     Nil     Refl   impossible
-}

index : (n : Nat)
     -> (l : DVect aTy l eTy as)
     -> Maybe $ DPair aTy eTy
index Z     (x::xs) = Just (_ ** x)
index (S n) (x::xs) = index n xs
index _     Nil     = Nothing

head : (l : DVect aTy n eTy as) -> {auto ok : isCons l = True} -> DPair aTy eTy
head Nil     {ok=Refl}   impossible
head (x::xs) {ok=p}    = (_ ** x)

tail : (l : DVect aTy (S n) eTy (a :: as))
    -> {auto ok : isCons l = True}
    -> (DVect aTy n eTy as)
tail Nil     {ok=Refl}   impossible
tail (x::xs) {ok=p}    = xs

last : (l : DVect aTy n eTy as) -> {auto ok : isCons l = True} -> DPair aTy eTy
last Nil        {ok=Refl}   impossible
last [x]        {ok=p}    = (_ ** x)
last (x::y::ys) {ok=p}    = last (y::ys) {ok=Refl}

-- TODO init

-- --------------------------------------------------------- [ Bob The Builder ]

(++) : DVect aTy x     eTy xs
    -> DVect aTy y     eTy ys
    -> DVect aTy (x+y) eTy (xs ++ ys)
(++) Nil     ys = ys
(++) (x::xs) ys = x :: (xs ++ ys)

-- TODO replicate

-- ---------------------------------------------------------------- [ SubLists ]
-- TODO

-- ----------------------------------------------------------------- [ Functor ]
-- TODO
{-
mapSV : (eXTy x -> eYTy y)
     -> (DVect xTy l eXTy xs)
     -> (ys : Vect l yTy ** DVect yTy l eYTy ys)
mapSV f Nil     = (Nil ** Nil)
mapSV f (x::xs) = let (ys ** xs') = mapSV f xs in (y :: ys ** f x ** xs')
-}
-- ---------------------------------------------------------------- [ Equality ]
-- TODO

-- ------------------------------------------------------------------- [ Order ]

-- TODO

-- ----------------------------------------------------------------- [ Folding ]
-- TODO

-- -------------------------------------------------------- [ Membership Tests ]
-- TODO

-- --------------------------------------------------------------- [ Searching ]
-- TODO

-- ----------------------------------------------------------------- [ Filters ]
-- TODO

-- ------------------------------------------------------------ [ Partitioning ]
-- TODO

-- -------------------------------------------------------------------- [ Show ]
-- TODO

-- ------------------------------------------- [ Applicative/Monad/Traversable ]
-- TODO

-- -------------------------------------------------------- [ Decidable Equals ]
-- TODO

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Schema

import SQLiteTypes

import Decidable.Equality
import Language.Reflection

%access public export
%default total

%auto_implicits on

infix 5 :::
data Attribute = (:::) String SQLiteType
%name Attribute attr,attr'

getName : Attribute -> String
getName (c:::_) = c

getTy : Attribute -> SQLiteType
getTy (_:::t) = t

attrEta : (attr : Attribute) -> (getName attr ::: getTy attr) = attr
attrEta (x ::: y) = Refl

attrInj : (c ::: t = c' ::: t') -> (c=c', t=t')
attrInj Refl = (Refl, Refl)

-- the first case forces it to get stuck if the constants are not in canonical form
foo : (x : String) -> (y : String) -> Dec (x = y)
foo "" "" = Yes Refl
foo x y with (decEq x y)
  foo x y | Yes _ = Yes (really_believe_me (Refl {x}))
  foo x y | No urgh = No urgh

implementation DecEq Attribute where
  decEq (x ::: y) (z ::: w) with (foo x z, decEq y w)
    decEq (x ::: y) (x ::: y) | (Yes Refl, Yes Refl) = Yes Refl
    decEq (x ::: y) (x ::: w) | (Yes Refl, No prf) = No $ prf . snd . attrInj
    decEq (x ::: y) (z ::: w) | (No prf, _) = No $ prf . fst . attrInj

data Schema = Nil | (::) Attribute Schema
%name Schema s,s'

append : (s1, s2 : Schema) -> Schema
append [] s2 = s2
append (attr :: s) s2 = attr :: (append s s2)

names : Schema -> List String
names [] = []
names ((n ::: _) :: s) = n :: names s

data HasCol : Schema -> Attribute -> Type where
  Here : HasCol (attr::s) attr
  There : HasCol s attr -> HasCol (attr'::s) attr

HasColNotEmpty : HasCol [] a -> Void
HasColNotEmpty Here impossible
HasColNotEmpty (There _) impossible

implementation Uninhabited (HasCol [] a) where
  uninhabited x = HasColNotEmpty x

decHasColLemma :  (HasCol s attr -> Void) ->
                  (attr' = attr -> Void) ->
                  HasCol (attr' :: s) attr -> Void
decHasColLemma h1 h2 Here = h2 Refl
decHasColLemma h1 h2 (There x) = h1 x

decHasCol : (s : Schema) -> (attr : Attribute) -> Dec (HasCol s attr)
decHasCol [] attr = No HasColNotEmpty
decHasCol (attr' :: s) attr with (decEq attr' attr)
  decHasCol (attr' :: s) attr' | (Yes Refl) = Yes Here
  decHasCol (attr' :: s) attr | (No f) with (decHasCol s attr)
    decHasCol (attr' :: s) attr | (No f) | (Yes x) = Yes (There x)
    decHasCol (attr' :: s) attr | (No f) | (No g) = No $ \h => decHasColLemma g f h

data SubSchema : Schema -> Schema -> Type where
  Empty : SubSchema [] s
  Head : (tailSub : SubSchema small large) ->
         (alsoThere : HasCol large attr) ->
         SubSchema (attr :: small) large

HasColNamed : Schema -> String -> Type
HasColNamed s col = (t : SQLiteType ** HasCol s (col ::: t))

decHasColNamed_lemma : ((HasColNamed s col) -> Void) -> ((col' = col) -> Void) ->
                       (t ** HasCol ((col' ::: ty) :: s) (col ::: t)) -> Void
decHasColNamed_lemma notThere notHere (ty ** Here)         = notHere Refl
decHasColNamed_lemma notThere notHere (ty ** (There more)) = notThere (ty ** more)

decHasColNamed : (s : Schema) -> (col : String) -> Dec (HasColNamed s col)
decHasColNamed [] col = No $ \h => HasColNotEmpty (snd h)
decHasColNamed ((col' ::: ty) :: s) col with (decEq col' col)
  decHasColNamed ((col ::: ty) :: s)  col | (Yes Refl) = Yes (ty ** Here)
  decHasColNamed ((col' ::: ty) :: s) col | (No f) with (decHasColNamed s col)
    decHasColNamed ((col' ::: ty) :: s) col | (No f) | (Yes x) =
      Yes (fst x ** There (snd x))
    decHasColNamed ((col' ::: ty) :: s) col | (No f) | (No g) = No (decHasColNamed_lemma g f)

colNames : Schema -> List String
colNames [] = []
colNames ((col ::: _) :: s) = col :: colNames s

data Disjointness : Type where
  Disjoint : Disjointness
  Overlap : (attr : Attribute) -> Disjointness

isDisjoint : (s1, s2 : Schema) -> Disjointness
isDisjoint [] s2 = Disjoint
isDisjoint (attr :: s) s2 with (decHasColNamed s2 (getName attr))
  isDisjoint (attr :: s) s2 | (Yes x) = Overlap attr
  isDisjoint (attr :: s) s2 | (No f) = isDisjoint s s2

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
%default total

isNat : Type -> Bool
isNat Nat = True
isNat Int = False
isNat _ = False

trivialEquality : isNat Int = False
trivialEquality = Refl


text:
> module So.Properties

> import Data.So

> import Decidable.Predicates
> import Unique.Predicates

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

* Introduction and elimination rules

> |||
> soIntro : (b : Bool) -> b = True -> So b
> soIntro True  Refl   = Oh
> soIntro False contra = void (trueNotFalse (sym contra))

> |||
> soElim : (b : Bool) -> So b -> b = True
> soElim True  Oh = Refl
> soElim False Oh impossible

** Or

> |||
> soOrIntro1 : (b1 : Bool) -> (b2 : Bool) -> So b1 -> So (b1 || b2)
> soOrIntro1 True _  Oh = Oh

> |||
> soOrIntro2 : (b1 : Bool) -> (b2 : Bool) -> So b2 -> So (b1 || b2)
> soOrIntro2 True  True Oh = Oh
> soOrIntro2 False True Oh = Oh

> |||
> soOrElim : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> Either (So b1) (So b2)
> soOrElim True  True  Oh = Left Oh
> soOrElim True  False Oh = Left Oh
> soOrElim False True  Oh = Right Oh
> soOrElim False False Oh impossible

> |||
> soOrElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b1) -> So b2
> soOrElim1 True  True  Oh Oh impossible
> soOrElim1 True  False Oh Oh impossible
> soOrElim1 False True  Oh Oh = Oh
> soOrElim1 False False Oh Oh impossible

> |||
> soOrElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 || b2) -> So (not b2) -> So b1
> soOrElim2 True  True  Oh Oh impossible
> soOrElim2 True  False Oh Oh = Oh
> soOrElim2 False True  Oh Oh impossible
> soOrElim2 False False Oh Oh impossible

** And

> |||
> soAndElim1 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b1
> soAndElim1 True  True  Oh = Oh
> soAndElim1 True  False Oh impossible
> soAndElim1 False True  Oh impossible
> soAndElim1 False False Oh impossible

> |||
> soAndElim2 : (b1 : Bool) -> (b2 : Bool) -> So (b1 && b2) -> So b2
> soAndElim2 True  True  Oh = Oh
> soAndElim2 True  False Oh impossible
> soAndElim2 False True  Oh impossible
> soAndElim2 False False Oh impossible

* Counter factuals

> |||
> contra : {b : Bool} -> b = False -> So b -> Void
> contra {b} p q = trueNotFalse (trans (sym (soElim b q)) p)

* Decidability

> ||| Lifted Booleans are decidable
> decSo : (b : Bool) -> Dec (So b)
> decSo True  = Yes Oh
> decSo False = No (\ oh => absurd oh)

> ||| Lifted Boolean functions are decidable
> dec1So : {A : Type} -> (p : A -> Bool) -> Dec1 (\ a => So (p a))
> dec1So p a = decSo (p a)

* Uniqueness

> ||| Lifted Booleans are unique
> uniqueSo : (b : Bool) -> Unique (So b)
> uniqueSo True  Oh Oh = Refl
> uniqueSo False Oh Oh impossible

> ||| Lifted Boolean functions are unique
> unique1So : {A : Type} -> (p : A -> Bool) -> Unique1 (\ a => So (p a))
> unique1So p a = uniqueSo (p a)

> {-

> ---}


text:
module Main

numTest : (Num a, Show a) => a -> a -> IO ()
numTest a b = do
  putStrLn $ show a ++ " + " ++ show b ++ " = " ++ show (a + b)
  putStrLn $ show a ++ " * " ++ show b ++ " = " ++ show (a * b)

integralTest : (Integral a, Show a) => a -> a -> IO ()
integralTest a b = do
  putStrLn $ show a ++ " div " ++ show b ++ " = " ++ show (a `div` b)
  putStrLn $ show a ++ " mod " ++ show b ++ " = " ++ show (a `mod` b)

fractionalTest : (Fractional a, Show a) => a -> a -> IO ()
fractionalTest a b = do
  putStrLn $ show a ++ " / " ++ show b ++ " = " ++ show (a / b)
  putStrLn $ "recip " ++ show a ++ " = " ++ show (recip a)
  putStrLn $ "recip " ++ show b ++ " = " ++ show (recip b)

showOrdering : Ordering -> String
showOrdering EQ = "EQ"
showOrdering LT = "LT"
showOrdering GT = "GT"

ordTest : (Ord a, Show a) => a -> a -> IO ()
ordTest a b = putStrLn $ "compare " ++ show a ++ " " ++ show b ++ " = " ++ showOrdering (compare a b)

int1 : Int
int1 = 2147483647

int2 : Int
int2 = -2147483648

int3 : Int
int3 = 4

integer1 : Integer
integer1 = 100000000000000009

integer2 : Integer
integer2 = 200000000000000008

bits8_1: Bits8
bits8_1 = 255

bits8_2: Bits8
bits8_2 = 255

bits16_1: Bits16
bits16_1 = 4097

bits16_2: Bits16
bits16_2 = 512

bits32_1: Bits32
bits32_1 = 8388608

bits32_2: Bits32
bits32_2 = 524288

bits64_1: Bits64
bits64_1 = 9223372036854775807

bits64_2: Bits64
bits64_2 = 281474976710656

double1 : Double
double1 = 24.234234

double2 : Double
double2 = 75676.23232

printHeader : String -> IO ()
printHeader header = do
  putStrLn ""
  putStrLn header
  putStrLn $ concat $ replicate (length header) "="

pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y],
                          x * x + y * y == z * z]
main : IO ()
main = do
  print "Hello "
  putStrLn "world!"
  printHeader "numTest on Int"
  numTest int1 int2

  printHeader "numTest on Integer"
  numTest integer1 integer2

  printHeader "numTest on Bits8"
  numTest bits8_1 bits8_2

  printHeader "numTest on Bits16"
  numTest bits16_1 bits16_2

  printHeader "numTest on Bits32"
  numTest bits32_1 bits32_2

  printHeader "numTest on Bits64"
  numTest bits64_1 bits64_2

  printHeader "numTest on Double"
  numTest double1 double2

  printHeader "integralTest on Int"
  integralTest int1 int2

  printHeader "integralTest on Integer"
  integralTest integer1 integer2

  printHeader "integralTest on Bits8"
  integralTest bits8_1 bits8_2

  printHeader "integralTest on Bits16"
  integralTest bits16_1 bits16_2

  printHeader "integralTest on Bits32"
  integralTest bits32_1 bits32_2

  printHeader "integralTest on Bits64"
  integralTest bits64_1 bits64_2

  printHeader "fractionalTest on Double"
  fractionalTest double1 double2

  printHeader "ordTest on Int"
  ordTest int1 int2

  printHeader "ordTest on Integer"
  ordTest integer1 integer2

  printHeader "ordTest on Bits8"
  ordTest bits8_1 bits8_2

  printHeader "ordTest on Bits16"
  ordTest bits16_1 bits16_2

  printHeader "ordTest on Bits32"
  ordTest bits32_1 bits32_2

  printHeader "ordTest on Bits64"
  ordTest bits64_1 bits64_2

  printHeader "ordTest on Double"
  ordTest double1 double2

  putStrLn ""
  printLn $ pythag 50

max_stars_repo_name: mmhelloworld/idris-jvm-hs

max_issues_repo_name: mmhelloworld/idris-jvm-hs

max_forks_repo_name: mmhelloworld/idris-jvm-hs


text:
module Decidable.Equality

import Data.Maybe
import Data.Either
import Data.Nat
import Data.List
import Data.List1

import public Decidable.Equality.Core as Decidable.Equality

%default total

--------------------------------------------------------------------------------
--- Unit
--------------------------------------------------------------------------------

public export
DecEq () where
  decEq () () = Yes Refl

--------------------------------------------------------------------------------
-- Booleans
--------------------------------------------------------------------------------

public export
DecEq Bool where
  decEq True  True  = Yes Refl
  decEq False False = Yes Refl
  decEq False True  = No absurd
  decEq True  False = No absurd

--------------------------------------------------------------------------------
-- Nat
--------------------------------------------------------------------------------

public export
DecEq Nat where
  decEq Z     Z     = Yes Refl
  decEq Z     (S _) = No absurd
  decEq (S _) Z     = No absurd
  decEq (S n) (S m) with (decEq n m)
   decEq (S n) (S m) | Yes p = Yes $ cong S p
   decEq (S n) (S m) | No p = No $ \h : (S n = S m) => p $ succInjective n m h

--------------------------------------------------------------------------------
-- Maybe
--------------------------------------------------------------------------------

public export
DecEq t => DecEq (Maybe t) where
  decEq Nothing Nothing = Yes Refl
  decEq Nothing (Just _) = No absurd
  decEq (Just _) Nothing = No absurd
  decEq (Just x') (Just y') with (decEq x' y')
    decEq (Just x') (Just y') | Yes p = Yes $ cong Just p
    decEq (Just x') (Just y') | No p
       = No $ \h : Just x' = Just y' => p $ justInjective h

--------------------------------------------------------------------------------
-- Either
--------------------------------------------------------------------------------

public export
(DecEq t, DecEq s) => DecEq (Either t s) where
  decEq (Left x) (Left y) with (decEq x y)
   decEq (Left x) (Left x) | Yes Refl = Yes Refl
   decEq (Left x) (Left y) | No contra = No (contra . leftInjective)
  decEq (Left x) (Right y) = No absurd
  decEq (Right x) (Left y) = No absurd
  decEq (Right x) (Right y) with (decEq x y)
   decEq (Right x) (Right x) | Yes Refl = Yes Refl
   decEq (Right x) (Right y) | No contra = No (contra . rightInjective)

--------------------------------------------------------------------------------
-- Tuple
--------------------------------------------------------------------------------

pairInjective : (a, b) = (c, d) -> (a = c, b = d)
pairInjective Refl = (Refl, Refl)

public export
(DecEq a, DecEq b) => DecEq (a, b) where
  decEq (a, b) (a', b') with (decEq a a')
    decEq (a, b) (a', b') | (No contra) =
      No $ contra . fst . pairInjective
    decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')
      decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl
      decEq (a, b) (a, b') | (Yes Refl) | (No contra) =
        No $ contra . snd . pairInjective

--------------------------------------------------------------------------------
-- List
--------------------------------------------------------------------------------

public export
DecEq a => DecEq (List a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) [] = No absurd
  decEq [] (x :: xs) = No absurd
  decEq (x :: xs) (y :: ys) with (decEq x y)
    decEq (x :: xs) (y :: ys) | No contra =
      No $ contra . fst . consInjective
    decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)
      decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl
      decEq (x :: xs) (x :: ys) | (Yes Refl) | (No contra) =
        No $ contra . snd . consInjective

--------------------------------------------------------------------------------
-- List1
--------------------------------------------------------------------------------

public export
DecEq a => DecEq (List1 a) where

  decEq (x ::: xs) (y ::: ys) with (decEq x y)
    decEq (x ::: xs) (y ::: ys) | No contra = No (contra . fst . consInjective)
    decEq (x ::: xs) (y ::: ys) | Yes eqxy with (decEq xs ys)
      decEq (x ::: xs) (y ::: ys) | Yes eqxy | No contra = No (contra . snd . consInjective)
      decEq (x ::: xs) (y ::: ys) | Yes eqxy | Yes eqxsys = Yes (cong2 (:::) eqxy eqxsys)

-- TODO: Other prelude data types

-- For the primitives, we have to cheat because we don't have access to their
-- internal implementations. We use believe_me for the inequality proofs
-- because we don't them to reduce (and they should never be needed anyway...)
-- A postulate would be better, but erasure analysis may think they're needed
-- for computation in a higher order setting.

--------------------------------------------------------------------------------
-- Int
--------------------------------------------------------------------------------
public export
implementation DecEq Int where
    decEq x y = case x == y of -- Blocks if x or y not concrete
                     True => Yes primitiveEq
                     False => No primitiveNotEq
       where primitiveEq : forall x, y . x = y
             primitiveEq = believe_me (Refl {x})
             primitiveNotEq : forall x, y . Not (x = y)
             primitiveNotEq prf = believe_me {b = Void} ()

--------------------------------------------------------------------------------
-- Char
--------------------------------------------------------------------------------
public export
implementation DecEq Char where
    decEq x y = case x == y of -- Blocks if x or y not concrete
                     True => Yes primitiveEq
                     False => No primitiveNotEq
       where primitiveEq : forall x, y . x = y
             primitiveEq = believe_me (Refl {x})
             primitiveNotEq : forall x, y . Not (x = y)
             primitiveNotEq prf = believe_me {b = Void} ()

--------------------------------------------------------------------------------
-- Integer
--------------------------------------------------------------------------------
public export
implementation DecEq Integer where
    decEq x y = case x == y of -- Blocks if x or y not concrete
                     True => Yes primitiveEq
                     False => No primitiveNotEq
       where primitiveEq : forall x, y . x = y
             primitiveEq = believe_me (Refl {x})
             primitiveNotEq : forall x, y . Not (x = y)
             primitiveNotEq prf = believe_me {b = Void} ()

--------------------------------------------------------------------------------
-- String
--------------------------------------------------------------------------------
public export
implementation DecEq String where
    decEq x y = case x == y of -- Blocks if x or y not concrete
                     True => Yes primitiveEq
                     False => No primitiveNotEq
       where primitiveEq : forall x, y . x = y
             primitiveEq = believe_me (Refl {x})
             primitiveNotEq : forall x, y . Not (x = y)
             primitiveNotEq prf = believe_me {b = Void} ()


text:
import Data.Fin
import Data.Vect
import Data.Vect.Quantifiers

%default total

namespace Kinding

  -- | Possible kinds of type
  data RepKind
    = Arr RepKind RepKind
    | Star
    -- TODO: add Constraint, Row, etc

  infixr 4 :=>
  (:=>) : RepKind -> RepKind -> RepKind
  (:=>) = Arr

  RepKinds : Nat -> Type
  RepKinds n = Vect n RepKind

namespace VariableReferencing

  -- | Reference a variable in scope of a given `Kind`
  data Item : Vect n t -> t -> Fin n -> Type where
    Stop : Item (k :: ks) k 0
    Pop  : Item ks k i -> Item (o :: ks) k (FS i)

  FromFin : (ks : RepKinds n) -> (i : Fin n) -> Item ks (Vect.index i ks) i
  FromFin (v :: vs) FZ     = Stop
  FromFin (v :: vs) (FS i) = Pop (FromFin vs i)

namespace Environments

  FnKind : RepKind
  FnKind = Star :=> Star :=> Star

  ArrKind : RepKind
  ArrKind = Star :=> Star

  DefaultEnv : Vect 2 RepKind
  DefaultEnv = [ FnKind
               , ArrKind
               ]

  FnType : Item DefaultEnv FnKind FZ
  FnType = FromFin DefaultEnv 0

  ArrayType : Item DefaultEnv (Star :=> Star) 1
  ArrayType = FromFin DefaultEnv 1

namespace Typing

  -- | Representation of types
  data RepType : (env : RepKinds e) ->
                 (scope : RepKinds n) ->
                 (kindOfType : RepKind) ->
                 Type where
    -- | Type variable
    Var : Item ks k i -> RepType es ks k
    -- | Universal quantification
    Forall : RepType es (ks ++ [k]) Star -> RepType es ks Star
    -- | Type application
    App : RepType es ks (i :=> o) -> RepType es ks i -> RepType es ks o
    -- | Function type - TODO: remove in favour of environment?
    Fun : RepType es ks Star -> RepType es ks Star -> RepType es ks Star
    -- | Reference types in the environment
    Other : Item es e i -> RepType es ks e

  extendTypeEnv : RepType es ks k -> RepType (e :: es) ks k
  extendTypeEnv (Var x) = Var x
  extendTypeEnv (Forall x) = Forall (extendTypeEnv x)
  extendTypeEnv (App x y) = App (extendTypeEnv x) (extendTypeEnv y)
  extendTypeEnv (Fun x y) = Fun (extendTypeEnv x) (extendTypeEnv y)
  extendTypeEnv (Other x) = Other (Pop x)

  -- | Proper types have `Kind` `Star`
  ProperType : RepKinds e -> RepKinds n -> Type
  ProperType es ks = RepType es ks Star

  var : (i : Fin n) -> RepType es ks (Vect.index i ks)
  var i {ks} = Var (FromFin ks i)

  infix 5 :$
  (:$) : RepType es ks (i :=> o) -> RepType es ks i -> RepType es ks o
  (:$) = App

  infixl 4 :->
  (:->) : ProperType es ks -> ProperType es ks -> ProperType es ks
  (:->) = Fun

  other : (i : Fin n) -> RepType es ks (Vect.index i es)
  other i {es} = Other (FromFin es i)

namespace Filling

  -- | Sequence of types to fill in the arguments of a higher kinded type
  data FilledKind : (env : RepKinds e) -> (typeVars : RepKinds n) -> (kind : RepKind) -> Type where
    Nil  : FilledKind es ts Star
    (::) : RepType es ts d -> FilledKind es ts c -> FilledKind es ts (d :=> c)

  extendFilledEnv : (e : RepKind) -> FilledKind es ks k -> FilledKind (e :: es) ks k
  extendFilledEnv e [] = []
  extendFilledEnv e (x :: y) = extendTypeEnv x :: extendFilledEnv e y

  filledType : FilledKind (with Vect (kind :: env)) vars kind ->
               ProperType (with Vect (kind :: env)) vars
  filledType xs = go (other 0) xs where
    go : RepType env vars kind -> FilledKind env vars kind -> ProperType env vars
    go m [] = m
    go m (x :: y) = go (m :$ x) y

  -- | Example: forall f a. Free f a
  filledKindExample : FilledKind [] [Star :=> Star, Star] ((Star :=> Star) :=> Star :=> Star)
  filledKindExample = [var 0, var 1]

namespace DataTyping

  -- | Representation of a data type's constructors
  record RepCtor (dataKind : RepKind) where
    constructor MkCtor
    name : String
    -- | Available types in the environment
    environment : RepKinds e
    -- | All top level type variables
    typeVars : RepKinds n
    -- | Constructor parameters with the `typeVars` and the data type in scope
    params : Vect paramCount (ProperType environment (dataKind :: typeVars))
    -- | Type arguments of the resulting data type
    finalTypeArgs : FilledKind environment (dataKind :: typeVars) dataKind

  -- | Representation of data types
  record RepData where
    constructor MkData
    -- The `Kind` of the data type, e.g. kind of `Maybe` is `Arr Star Star`
    kind : RepKind
    -- All constructors for the data type
    ctors : Vect sumCount (RepCtor kind)

  datatype : (kind : RepKind) -> Vect n (RepCtor kind) -> RepData
  datatype = MkData

  self : RepType es (k :: ks) k
  self = var 0

namespace Valuing

  -- rep was 3rd arg but https://github.com/idris-lang/Idris-dev/issues/1944
  data RepValue : ProperType env vars -> Type where
    MkValue : (rep : RepData) ->
              Item (ctors rep) ctor i ->
              (env : RepKinds e) ->
              (vars : RepKinds v) ->
              (args : All RepValue (params ctor)) ->
              (finalArgs : FilledKind env vars (kind rep)) ->
              RepValue (filledType (extendFilledEnv (kind rep) finalArgs))

namespace DataExamples

  -- Unit : * where
  --   Unit : Unit
  Unit : RepData
  Unit = datatype Star
    [ MkCtor "unit" [] [] [] []
    ]

  -- unit : Unit
  unit : RepValue (the (RepType [Star] [] Star) (other 0))
  unit = MkValue Unit Stop [] [] [] []

  -- Bool : * where
  --   True : Bool
  --   False : Bool
  Bool : RepData
  Bool = datatype Star
    [ MkCtor "true"  [] [] [] []
    , MkCtor "false" [] [] [] []
    ]

  true : RepValue (the (RepType [Star] [] Star) (other 0))
  true = MkValue Bool Stop [] [] [] []

  -- Maybe : * -> * where
  --   Nothing : forall (t : *). Maybe t
  --   Just    : forall (t : *). t -> Maybe t
  maybe : RepData
  maybe = datatype (Star :=> Star)
    [ MkCtor "nothing" [] [Star] []      [var 1]
    , MkCtor "just"    [] [Star] [var 1] [var 1]
    ]

  -- Either : * -> * -> * where
  --   Left  : forall (l, r : *). l -> Either l r
  --   Right : forall (l, r : *). r -> Either l r
  either : RepData
  either = datatype (Star :=> Star :=> Star)
    [ MkCtor "left"  [] [Star, Star] [var 1] [var 1, var 2]
    , MkCtor "right" [] [Star, Star] [var 2] [var 1, var 2]
    ]

  -- Pair : * -> * -> * where
  --   Pair : forall (l, r : *). l -> r -> Pair l r
  pair : RepData
  pair = datatype (Star :=> Star :=> Star)
    [ MkCtor "pair" [] [Star, Star] [var 1, var 2] [var 1, var 2]
    ]

  -- List : * -> * where
  --   Nil  : forall (t : *). List t
  --   Cons : forall (t : *). t -> List t -> List t
  list : RepData
  list = datatype (Star :=> Star)
    [ MkCtor "nil"  [] [Star] [] [var 1]
    , MkCtor "cons" [] [Star] [var 1, self :$ var 1] [var 1]
    ]

  -- Coyoneda : (* -> *) -> * -> * where
  --   Coyo : forall (f : * -> *) (a, b : *). (b -> a) -> (f b) -> Coyoneda f a
  coyoneda : RepData
  coyoneda = datatype ((Star :=> Star) :=> Star :=> Star)
    [ MkCtor "coyo" [] [Star :=> Star, Star, Star]
                       [var 3 :-> var 2, var 1 :$ var 2]
                       [var 1, var 2]
    ]

  -- Free : (* -> *) -> * -> * where
  --   Pure : forall (f : * -> *) (a : *). a -> Free f a
  --   Next : forall (f : * -> *) (a : *). f (Free f a) -> Free f a
  free : RepData
  free = datatype ((Star :=> Star) :=> Star :=> Star)
    [ MkCtor "pure" [] [Star :=> Star, Star] [var 2] [var 1, var 2]
    , MkCtor "next" [] [Star :=> Star, Star]
                       [var 1 :$ ((self :$ var 1) :$ var 2)]
                       [var 1, var 2]
    ]

  -- Exists : (* -> *) -> * where
  --   MkExists : forall (p : * -> *). (forall r. (forall i. p i -> r) -> r) -> Exists p
  exists : RepData
  exists = datatype ((Star :=> Star) :=> Star)
    [ MkCtor "mkExists" [] [Star :=> Star]
                           [Forall (Forall ((var 1 :$ var 3) :-> var 2) :-> var 2)]
                           [var 1]
    ]

  -- | Here we have a reference to `String : *`
  -- FullName : * where
  --   MkFullName : String -> String -> FullName
  fullName : RepData
  fullName = datatype Star
    [ MkCtor "mkFullName" [Star] [] [other 0, other 0] []
    ]

  {-
    POSSIBLE CONSIDERATIONS
    want to guarantee that computed instances can
      only use type args - cannot inspect types of parameters
      specify constraints: generally, for particular type arguments of higher kinded types, etc
      fail deriving: data type not compatible, etc
  -}

max_stars_repo_name: LiamGoodacre/instance-computer

max_issues_repo_name: LiamGoodacre/instance-computer

max_forks_repo_name: LiamGoodacre/instance-computer