text:
module System.Bindings.LibUSB.SyncIO

import System.Bindings.LibUSB.Data
import System.Bindings.LibUSB.Devices

-- XXX Hack Hack Hack
nat_to_bits16 : Nat -> Bits16
nat_to_bits16 = fromInteger . toIntegerNat

libusb_control_transfer : DeviceHandle -> Bits8 -> Bits8 -> Bits16 -> Bits16
                        -> Buffer -> Int -> IO Int
libusb_control_transfer (MkDeviceHandle h) reqType request value index (MkBuffer len b) timeout =
  mkForeign (FFun "libusb_control_transfer" [FPtr, FBits8, FBits8, FBits16, FBits16, FPtr, FBits16, FInt] FInt) h reqType request value index b (nat_to_bits16 len) timeout

libusb_bulk_transfer : DeviceHandle -> Bits8 -> Buffer -> Int -> IO (Either Int Int)
libusb_bulk_transfer (MkDeviceHandle h) endpoint (MkBuffer len b) timeout = do
  res <- mkForeign (FFun "idris_libusb_bulk_transfer" [FPtr, FBits8, FPtr, FInt, FInt] FInt) h endpoint b (fromNat len) timeout
  return $ (Right 0) -- if res >= 0 then (Right res) else (Left res)

libusb_interrupt_transfer : DeviceHandle -> Bits8 -> Buffer -> Int -> IO (Either Int Int)
libusb_interrupt_transfer (MkDeviceHandle h) endpoint (MkBuffer len b) timeout = do
  res <- mkForeign (FFun "idris_libusb_interrupt_transfer" [FPtr, FBits8, FPtr, FInt, FInt] FInt) h endpoint b (fromNat len) timeout
  return $ if res >= 0 then (Right res) else (Left res)

max_stars_repo_name: idris-hackers/usb

max_issues_repo_name: idris-hackers/usb

max_forks_repo_name: idris-hackers/usb


text:
module Main
import Data.SortedMap

test : List Int -> IO ()
test xs = do let lst = Data.SortedMap.toList mp
             if length lst /= n
                then putStrLn $ "wrong length for " ++ show xs
                else do let res = map (\x => lookup x mp) xs
                        let found = mapMaybe id res
                        if length found /= n
                           then putStrLn $ "some lost in " ++ show xs ++ ": res=" ++ show res
                                            ++ " toList=" ++ show lst
                           else pure ()

  where
    mp : SortedMap Int ()
    mp = foldr (\x => \m => insert x () m) empty xs
    n : Nat
    n = length xs

main : IO ()
main = do test [1,2,3]
          test [4,3,2,1]
          test [1,2,3,4]

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Apply

-- These are not Biapplicatives.  Those are in Data.Biapplicative

import Bifunctor

infixl 4 <<$>>, <<&>>, <<.>>, <<., .>>, <<..>>

||| Primarily used to make the definitions of bilift2 and bilift3 pretty
|||
||| ```idris example
||| bimap const const <<$>> (1, 2) <<.>> (3, 4) == (1, 2)
||| ```
|||
export
(<<$>>) : (a -> b) -> a -> b
(<<$>>) = id

||| <<$>> with the arguments reversed
|||
||| ```idris example
||| (1, 2) <<&>> bimap const const <<.>> (3, 4) == (1, 2)
||| ```
|||
(<<&>>) : a -> (a -> b) -> b
(<<&>>) = flip id

||| Biapplys (not to be confused with Biapplicatives)
||| @p The action of the Biapply on pairs of objects
public export
interface Bifunctor p => Biapply (p : Type -> Type -> Type) where

  ||| Applys a Bifunctor of functions to another Bifunctor of the same type
  |||
  ||| ````idris example
  ||| (reverse, (\x => x + 1)) <<.>> ("hello", 1) == ("olleh", 2)
  ||| ````
  |||
  (<<.>>) : p (a -> b) (c -> d) -> p a c -> p b d

  ||| Given two Bifunctors, sequences them leftwards
  |||
  ||| ````idris example
  ||| ("hello", 1) <<. ("goodbye", 2) == ("hello", 1)
  ||| ````
  |||
  (<<.) : p a b -> p c d -> p a b
  a <<. b = bimap const const <<$>> a <<.>> b

  ||| Given two Bifunctors, sequences them rightwards
  |||
  ||| ````idris example
  ||| ("hello", 1) <<. ("goodbye", 2) == ("goodbye", 2)
  ||| ````
  |||
  (.>>) : p a b -> p c d -> p c d
  a .>> b = bimap (const id) (const id) <<$>> a <<.>> b

||| Lifts a pair of binary functions into a Bifunctor
|||
||| ````idris example
||| bilift2 (++) (+) ("hello", 1) ("goodbye", 2) == ("hellogoodbye", 3)
||| ````
|||
bilift2 : Biapply p => (a -> b -> c) -> (d -> e -> f) -> p a d -> p b e -> p c f
bilift2 f g a b = bimap f g <<$>> a <<.>> b

||| Lifts a pair of ternary functions into a Bifunctor
|||
||| ````idris example
||| bilift3 (\x,y,z => x ++ (y ++ z)) (\x,y,z => x + (y + z))
|||         ("hello", 1) ("goodbye", 2) ("hello again", 3) ==
||| ("hellogoodbyehello again", 6)
||| ````
|||
bilift3 : Biapply p => (a -> b -> c -> d) -> (e -> f -> g -> h)
        -> p a e -> p b f -> p c g -> p d h
bilift3 f g a b c = bimap f g <<$>> a <<.>> b <<.>> c

||| Applies the second of two Bifunctors to the first
|||
||| ````idris example
||| ("hello", 1) <<..>> (reverse, (\x => x + 1)) == ("olleh", 2)
||| ````
|||
(<<..>>): Biapply p => p a c -> p (a -> b) (c -> d) -> p b d
(<<..>>) = flip (<<.>>)

implementation Biapply Pair where
  (f, g) <<.>> (a, b) = (f a, g b)


text:
module Main

%default total

main : IO () =
  putStrLn "fspp"

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Types
import Control.Lens.Const
import Data.Contravariant
import Control.Lens.First
import Control.Monad.Identity
import Data.Bifunctor
import Data.Profunctor
import Data.Tagged

%default total

public export
Optic : (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type -> Type -> Type
Optic p f s t a b = p a (f b) -> p s (f t)

public export
Simple : (Type -> Type -> Type -> Type -> Type) -> Type -> Type -> Type
Simple p s a = p s s a a

public export
Optic' : (Type -> Type -> Type) -> (Type -> Type) -> Type -> Type -> Type
Optic' p f = Simple (Optic p f)

public export
LensLike : (Type -> Type) -> Type -> Type -> Type -> Type -> Type
LensLike = Optic Morphism

public export
LensLike' : (Type -> Type) -> Type -> Type -> Type
LensLike' f = Simple (LensLike f)

-- type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
public export
Lens : Type -> Type -> Type -> Type -> Type
Lens s t a b  = { f : Type -> Type } -> Functor f => LensLike f s t a b

-- type Lens' s a = Lens s s a a
public export
Lens' : Type -> Type -> Type
Lens' = Simple Lens

-- type Getting r s a = (a -> Const r a) -> s -> Const r s
public export
Getting : Type -> Type -> Type -> Type
Getting r = LensLike' (Const r)

-- type Getter s a = forall f. (Contravariant f, Functor f) => (a -> f a) -> s -> f s
public export
Getter : Type -> Type -> Type
Getter s a = { f : Type -> Type } -> (Contravariant f, Functor f) => LensLike' f s a

-- type ASetter s t a b = (a -> Identity b) -> s -> Identity t
public export
Setter : Type -> Type -> Type -> Type -> Type
Setter = LensLike Identity

public export
Setter' : Type -> Type -> Type
Setter' = Simple Setter

-- type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
public export
Traversal : Type -> Type -> Type -> Type -> Type
Traversal s t a b  = { f : Type -> Type } -> Applicative f => LensLike f s t a b

-- type Traversal' s a = Traversal s s a a
public export
Traversal' : Type -> Type -> Type
Traversal' = Simple Traversal

-- type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)
-- The choice of `Choice p` for a valid `Traversal` is the `(->)` implementation. Which is used
-- when using a prism as a getter or setter.

public export
Prism : Type -> Type -> Type -> Type -> Type
Prism s t a b  = {p : Type -> Type -> Type} -> { f : Type -> Type } ->
                 (Choice p,Applicative f) => Optic p f s t a b

public export
Prism' : Type -> Type -> Type
Prism' = Simple Prism

public export
Iso : Type -> Type -> Type -> Type -> Type
Iso s t a b = {p : Type -> Type -> Type} -> {f : Type -> Type} ->
              (Profunctor p,Functor f) => Optic p f s t a b

public export
Iso' : Type -> Type -> Type
Iso' = Simple Iso

-- type Review t b = forall p f. (Choice p, Bifunctor p, Settable f) => Optic' p f t b
public export
Review : Type -> Type -> Type -> Type -> Type
Review s t a b = { p : Type -> Type -> Type } -> { f : Type -> Type } ->
                 (Choice p, Bifunctor p) => Optic p Identity s t a b

-- type AReview t b = Optic' Tagged Identity t b
public export
AReview : Type -> Type -> Type
AReview t b = Optic' Tagged Identity t b

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


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative

import public Text.PrettyPrint.WL
import public Options.Applicative.Builder
import public Options.Applicative.Maybe
import public Options.Applicative.Run
import public Options.Applicative.Types
import public Options.Applicative.Usage
import public Control.Lens

%access public export

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

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
module Main
import QB.FFI

main : IO ()
main = do
    putStrLn' "hello world"


text:
||| http://okmij.org/ftp/Computation/free-monad.html
module Freer

%default total
%access public export

data FFree : (Type -> Type) -> Nat -> Type -> Type where
  FPure   : a -> FFree g n a
  FImpure : g x -> (x -> FFree g n a) -> FFree g (S n) a

Functor (FFree g n) where
  map f (FPure x)     = FPure (f x)
  map f (FImpure u q) = FImpure u (map f . q)

pure : a -> FFree g n a
pure = FPure

promote : {m : Nat} -> FFree g n a -> FFree g (n + m) a
promote (FPure x)     = FPure x
promote (FImpure u q) = FImpure u (promote . q)

assocS : (m : Nat) -> (n : Nat) -> m + S n = S (m + n)
assocS Z n = Refl
assocS (S m) n = cong $ assocS m n

apply : FFree g n (a -> b) -> FFree g m a -> FFree g (m + n) b
apply {n} {m} (FPure f) x =
  promote $ map f x
apply {n=S n} {m} (FImpure u q) x =
  let y = flip apply x . q
  in rewrite assocS m n in FImpure u y

bind : (a -> FFree g n b) -> FFree g m a -> FFree g (n + m) b
bind {n} {m} f (FPure x) = promote $ f x
bind {n} {m=S m} f (FImpure u f') =
  let y = bind f . f'
  in rewrite assocS n m in FImpure u y

join : FFree g m (FFree g n a) -> FFree g (n + m) a
join = bind id

--Applicative (FFree g) where
--  pure = FPure
--
--infixr 5 >=>
--
--(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
--f >=> g = (>>= g) . f
--
--Monad (FFree g) where
--  (FPure x) >>= f = f x
--  (FImpure u f') >>= f = FImpure u (f' >=> f)


text:
module Example.DecEq'

public export
data Dec' : Type -> Type where
  Yes : (a : x) -> Dec' x
  No : Dec' x

public export
interface DecEq' t where
  decEq' : (x1 : t) -> (x2 : t) -> Dec' (x1 = x2)

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module A

export
data AFoo = MkAFoo


text:
import Data.Vect
import Data.Fin
import Language.Reflection

%language ElabReflection

data Ty : Type where
     Base : Type -> Ty
     Arrow : Ty -> Ty -> Ty

-- Ty can be translated to a host language type

interpTy : Ty -> Type
interpTy (Base t) = t
interpTy (Arrow s t) = (argTy : interpTy s) -> interpTy t

data HasType : Fin k -> Ty -> Vect k Ty -> Type where
     Stop : HasType FZ t (t :: gam)
     Pop  : HasType i t gam -> HasType (FS i) t (u :: gam)

data Lang : Vect k Ty -> Ty -> Type where
     Var : HasType i t gam -> Lang gam t
     Val : (x : interpTy a) -> Lang gam a
     Lam : (scope : Lang (s :: gam) t) -> Lang gam (Arrow s t)
     App : Lang gam (Arrow s t) -> Lang gam s -> Lang gam t;
     Op  : (interpTy a -> interpTy b -> interpTy c) ->
           Lang gam a -> Lang gam b -> Lang gam c

data Env : Vect n Ty -> Type where
     Nil : Env Nil
     (::) : (x : interpTy a) -> Env xs -> Env (a :: xs)

-- Find a value in an environment
lookupEnv : HasType i t gam -> Env gam -> Elab (interpTy t)
lookupEnv Stop (x :: xs) = pure x
lookupEnv (Pop var) (x :: env) = lookupEnv var env

interp : Env gam -> Lang gam t -> Elab (interpTy t)
interp env (Var x)
    = do res <- lookupEnv x env
         pure res
interp env (Val x) = pure x
interp env (Lam scope)
    = lambda _ (\val => interp (val :: env) scope)
interp env (App f a)
    = interp env f <*> interp env a
interp env (Op f x y) = f <$> interp env x <*> interp env y

%macro
eval : Env gam -> Lang gam t -> Elab (interpTy t)
eval = interp

testAdd : Lang gam (Arrow (Base Nat) (Arrow (Base Nat) (Base Nat)))
testAdd = Lam (Lam (Op plus (Var Stop) (Var (Pop Stop))))

evalAdd : Nat -> Nat -> Nat
evalAdd x y =let add = eval [] testAdd in add x y

testBlock : Lang gam (Base Nat)
testBlock = Op {a=Base Nat} {b=Base Nat} plus (Val 3) (Val 4)

evalBlock : Nat
evalBlock = eval [] testBlock


text:
module ZipFolds

-- Based on http://okmij.org/ftp/Haskell/zip-folds.lhs

data FR : (a : Type) -> Type where
  Cont : ({r : Type} -> (a -> r -> r) -> r -> r) -> FR a

ofList : List a -> FR a
ofList l = Cont (\f, r => foldr f r l)

toList : FR a -> List a
toList (Cont f) = f (::) []

map : (a -> b) -> FR a -> FR b
map f (Cont g) = Cont (\h => g (\x, r => h (f x) r))

filter : (a -> Bool) -> FR a -> FR a
filter f (Cont g) = Cont (\h => g (\x, r => if f x then h x r else r))

drop : Int -> FR a -> FR a
drop n (Cont f) = Cont (\g, z => let f' = f (acc g) (seed z) in f' n)
  where
    acc : (a -> r -> r) -> a -> (Int -> r) -> Int -> r
    acc f x r n = if n <= 0 then f x (r n) else r (n - 1)
    seed : r -> Int -> r
    seed x _ = x

zipWith : (a -> b -> c) -> FR a -> FR b -> FR c
zipWith t (Cont f) fr = Cont (\g, z => let f' = f (acc z g) (seed z) in f' fr)
  where
    acc : r -> (c -> r -> r) -> a -> (FR b -> r) -> FR b -> r
    acc z f x r (Cont r2) = r2 (\y, _ => f (t x y) (r (drop 1 (Cont r2)))) z
    seed : r -> FR b -> r
    seed x _ = x

stream : FR Int
stream = ofList [1..10]

test : List (Int, Int)
test = toList $ zipWith (\x, y => (x, y)) stream stream

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Refined

data Vect : (len : Nat) -> (elem : Type) -> Type where
  Nil  : Vect Z elem
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

-- Definitions

digits : List Char
digits = ['0'..'9']

lowerCase : List Char
lowerCase = ['a'..'z']

upperCase : List Char
upperCase = ['A'..'Z']

-- Elem property
data Elem : a -> List a -> Type where
  Here : Elem x (x :: xs)
  There : (later : Elem x xs) -> Elem x (y :: xs)

-- Elem examples

aIsLC : Elem 'a' Refined.lowerCase

bIsLC : Elem 'b' Refined.lowerCase

kIsLC : Elem 'k' Refined.lowerCase

-- Not true....

-- Properties
Digits : Char -> Type

LowerCase : Char -> Type

UpperCase : Char -> Type

-- Dependent pairs
x : (n : Nat ** Vect n Int)

-- Refinement type

-- x : Refined Char UpperCase

--refbIsLC : Refined Char LowerCase

-- Conversion

--toRefined : { a : Type } -> { P : a -> Type } -> ???

--testRefA : Refined Char LowerCase

--testRefB : Char `Refined` LowerCase

--fromRefined : { P : Char -> Type } -> ???

-- Examples

printChar : Char -> IO ()
printChar = printLn

main : IO ()

{-

Idris Refined
https://github.com/janschultecom/idris-refined

-}


text:
module Main

import BTree

main : HasIO io => io ()
main =  do let t = toTree [1, 8, 2, 7, 9, 3]
           printLn $ BTree.toList t

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
import Data.Vect

dvec : (n : Nat) -> {default (replicate n 1) xs : Vect n Nat} -> Nat
dvec n = foldr (+) Z xs


text:
import Extra.Prelude
import Extra.Language.Derive
import Language.Reflection
import Decidable.Equality

%language ElabReflection

data Tree a = Branch (Tree a) a (Tree a)
            | Leaf

mutual
  eqTree : Eq a
    => Tree a
    -> Tree a
    -> Bool
  %runElab deriveEq `{{ eqTree }} `{{ Tree }}

  Eq a => Eq (Tree a) where
    (==) = eqTree

mutual
  decEqTree : DecEq a
    => (x : Tree a)
    -> (y : Tree a)
    -> Dec (x = y)
  %runElab deriveDecEq `{{ decEqTree }} `{{ Tree }}

  DecEq a => DecEq (Tree a) where
    decEq = decEqTree

main : IO ()
main = putStrLn "Hi!"


text:
> module GeenricSimpleProb.BasicOperations

> import Data.List
> import Syntax.PreorderReasoning

> import GenericSimpleProb.SimpleProb
> import Fun.Operations
> import List.Operations
> import List.Properties

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

> |||
> toList : {A, B : Type} -> SimpleProb A B -> List (A, B)
> toList (MkSimpleProb aps _) = aps

> |||
> normalize : {A, B : Type} -> DecEq B => SimpleProb A B -> SimpleProb A B
> normalize {A} (MkSimpleProb Nil sum) = MkSimpleProb Nil sum
> normalize {A} (MkSimpleProb (ap :: Nil) sum) = MkSimpleProb (ap :: Nil) sum
> normalize {A} {B} (MkSimpleProb (ap :: ap' :: aps) sum) = MkSimpleProb aps' sum' where
>   aps' : List (A, B)
>   aps' = discardBySndZero (ap :: ap' :: aps)
>   sum' : sumMapSnd aps' = 1
>   sum' = trans (discardBySndZeroLemma (ap :: ap' :: aps)) sum

> {-

> |||
> support : {A : Type} -> SimpleProb A -> List A
> support sp = map fst (toList (normalize sp))

> |||
> probs : {A : Type} -> SimpleProb A -> List NonNegRational
> probs sp = map snd (toList (normalize sp))

> ||| 'prob sp a' is the probability of 'a' according to 'sp'
> prob : {A : Type} -> (Eq A) => SimpleProb A -> A -> NonNegRational
> prob (MkSimpleProb aps _) a = foldr f 0 aps where
>   f : (A, NonNegRational) -> NonNegRational -> NonNegRational
>   f (a', p') p = if (a == a') then p + p' else p

> ||| Make a SimpleProb in which all elements of a list have the same
> ||| probablility. If the list has no duplicates, this results in a
> ||| uniform probability distribution
> mkSimpleProb : {A : Type} -> (as : List A) -> ListOperations.NonEmpty as -> SimpleProb A
> mkSimpleProb      Nil      prf = absurd prf
> mkSimpleProb {A} (a :: as) _   = MkSimpleProb aps s1p where
>   m : Nat
>   m = length as
>   ps : List NonNegRational
>   ps = replicate (S m) (fromFraction (1, Element (S m) MkPositive))
>   sps : sum ps = fromFraction (S m, Element (S m) MkPositive)
>   sps = sumLemma0 (S m) m
>   aps : List (A, NonNegRational)
>   aps = zip (a :: as) ps
>   leq : length (a :: as) = length ps
>   leq = ( length (a :: as) )
>       ={ Refl }=
>         ( S (length as) )
>       ={ Refl }=
>         ( S m )
>       ={ sym (lengthReplicateLemma (S m) (fromFraction (1, Element (S m) MkPositive))) }=
>         ( length (replicate (S m) (fromFraction (1, Element (S m) MkPositive))) )
>       ={ Refl }=
>         ( length ps )
>       QED
>   s1p : sumMapSnd aps = 1
>   s1p = ( sumMapSnd aps )
>       ={ sumMapSndUnzipLemma aps }=
>         ( sum (snd (unzip aps)) )
>       ={ Refl }=
>         ( sum (snd (unzip (zip (a :: as) ps))) )
>       ={ cong {f = sum . snd} (unzipZipLemma (a :: as) ps leq) }=
>         ( sum (snd ((a :: as), ps)) )
>       ={ cong {f = sum} Refl }=
>         ( sum ps )
>       ={ sps }=
>         ( fromFraction (S m, Element (S m) MkPositive) )
>       ={ fromFractionEqLemma (S m, Element (S m) MkPositive) (S Z, Element (S Z) MkPositive) (multCommutative (S m) (S Z)) }=
>         ( fromFraction (S Z, Element (S Z) MkPositive) )
>       ={ Refl }=
>         ( 1 )
>       QED

> ---}

> {-

> prob : {A : Type} -> (DecEq A) => SimpleProb A -> A -> NonNegRational
> prob {A} (MkSimpleProb aps _) a = foldr f 0 aps where
>   f : (A, NonNegRational) -> NonNegRational -> NonNegRational
>   f (a', p') p with (decEq a a')
>     | (Yes _) = p + p'
>     | (No _)  = p

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Halfer

import public Numeric

%default total

||| Divide even integer by 2
public export
halfer : EvenInteger -> Integer
-- a: input integer
-- x: half of a
-- p: proof that x is the half of a
halfer (a ** (Factor (x ** p))) = cast x

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
{- Tests for typed native Dart lists -}
module Main

import Dart.Core
import Dart.FFI

%foreign """
Dart:code,
code() {}
printStrings($.List<$.String> list) => $.print(list);
printInts($.List<$.int> list) => $.print(list);
printIntegers($.List<$.BigInt> list) => $.print(list);
"""
prim__code : PrimIO ()

importForeignCode : IO ()
importForeignCode = primIO prim__code

%inline
printListVia : String -> {a : Type} -> Core.List a -> IO ()
printListVia f es = primIO $ prim__dart_invoke f [] [es] none

printStrings : Core.List String -> IO ()
printStrings = printListVia "printStrings"

printInts : Core.List Int -> IO ()
printInts = printListVia "printInts"

printIntegers : Core.List Integer -> IO ()
printIntegers = printListVia "printIntegers"

%inline
into : {element : Type} -> Core.List element -> Prelude.List element -> IO (Core.List element)
into list es = do
  traverse_ (flip add list) es
  pure list

main : IO ()
main = do
  importForeignCode
  printStrings empty
  printStrings (fromList ["do", "re"])
  printStrings !(into !new ["mi", "fa"])
  printInts empty
  printInts (fromList {element = Int} [1..10])
  printInts !(into !new [10..1])
  printIntegers empty
  printIntegers (fromList {element = Integer} [1..10])
  printIntegers !(into !new [10..1])


text:
module Zoo

data SourcePos = SP String Nat Nat
Show SourcePos where
  show (SP x k j) = x ++ ":" ++ (show k) ++ "," ++ (show j)

Name : Type
Name = String

mutual
  Ty : Type
  Ty = Tm

  RRaw : Type
  RRaw = Tm

  data Tm
    = Var Name
    | Lam Name Tm
    | App Tm Tm
    | U
    | Pi Name Ty Ty
    | Let Name Ty Tm Tm
    | SrcPos SourcePos Tm
%name Tm t, u

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

Env : Type
Env = List (Name, Maybe Val)
%name Env env, env1, env2, env3

fresh : Env -> Name -> Name
fresh env "_" = "_"
fresh [] x = x
fresh (y :: xs) x = case x == fst y of
                         False => fresh xs x
                         True => fresh xs (x ++ "'")

-- maybe (VVar x) id (fromJust $ lookup x env)

partial
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) = case (eval env t, eval env u) of
                          (VLam _ t', u') => t' u'
                          (t', u') => VApp t' u'
eval env (Lam x t) = VLam x (\u => eval ((x, Just u) :: env) t)
eval env (Pi x a b) = VPi x (eval env a) (\u => eval ((x, Just u) :: env) b)
eval env (Let x _ t u) = eval ((x, Just (eval env t)) :: env) u
eval env U = VU
eval env (SrcPos _ t) = eval env t

partial
quote : Env -> Val -> Tm
quote env (VVar x) = Var x
quote env (VApp t u) = App (quote env t) (quote env u)
quote env VU = U
quote env (VPi x a b) = let freshX = fresh env x in
                            Pi x (quote env a) (quote ((x, Nothing) :: env) (b (VVar x)))
quote env (VLam x t) = let freshX = fresh env x in
                           Lam x (quote ((x, Nothing) :: env) (t (VVar x)))

partial
nf : Env -> Tm -> Tm
nf env = quote env . eval env

partial
nf0 : Tm -> Tm
nf0 = nf []

partial
conv : Env -> Val -> Val -> Bool
conv env t u =
  case (t, u) of
       (VU, VU) => True
       (VPi x a b, VPi x' a' b') =>
         let gx = fresh env x in
         conv env a a' && conv ((gx, Nothing) :: env) (b (VVar gx)) (b' (VVar gx))
       (VLam x t, VLam x' t') =>
         let gx = fresh env x in
         conv ((gx, Nothing) :: env) (t (VVar gx)) (t' (VVar gx))

       -- checking eta conversion for Lam
       (VLam x t, u) =>
         let gx = fresh env x in
         conv ((gx, Nothing) :: env) (t (VVar gx)) (VApp u (VVar gx))
       (u, VLam x t) =>
         let gx = fresh env x in
         conv ((gx, Nothing) :: env) (VApp u (VVar gx)) (t (VVar gx))

       (VVar x, VVar x') => x == x'
       (VApp t u, VApp t' u') => conv env t t' && conv env u u'
       _ => False

VTy : Type
VTy = Val

Cxt : Type
Cxt = List (Name, VTy)

M : Type -> Type
M = Either (String, Maybe SourcePos)

report : String -> M a
report str = Left (str, Nothing)

quoteShow : Env -> Val -> String

addPos : SourcePos -> M a -> M a
addPos pos ma = case ma of
  Left (msg, Nothing) => Left (msg, Just pos)
  x => x

mutual
  partial
  infer : Env -> Cxt -> RRaw -> M VTy
  infer env cxt (Var x) =
    case lookup x cxt of
         Nothing => report $ "Name not in scope: " ++ x
         Just a  => Right a
  infer env cxt (Lam _ _) = report "Can't infer type for lambda expresion"
  infer env cxt (App t u) =
    do tty <- infer env cxt t
       (case tty of
             (VPi _ a b) =>
               do check env cxt u a
                  Right (b (eval env u))
             _ => report $
                    "Expected a function type, instead inferred:\n\n  "
                    ++ quoteShow env tty)
  infer env cxt U = Right VU
  infer env cxt (Pi x a b) =
    do Zoo.check env cxt a VU
       check ((x, Nothing) :: env) ((x, eval env a) :: cxt) b VU
       Right VU
  infer env cxt (Let x a t u) =
    let a' = eval env a in -- TODO not sure about
    do check env cxt a VU
       check env cxt t a'
       infer ((x, Just (eval env t)) :: env) ((x, a') :: cxt) u
  infer env cxt (SrcPos pos t) = addPos pos (infer env cxt t)

  partial
  check : Env -> Cxt -> RRaw -> VTy -> M ()
  check env cxt t a =
    case (t, a) of
         (SrcPos pos t', _) => addPos pos (check env cxt t' a)
         (Lam x t, VPi x' a b) =>
           let freshX' = fresh env x' in
           check ((x, Just (VVar freshX')) :: env) ((x, a) :: cxt) t (b (VVar x'))
         (Let x a' t' u, _) => -- TODO not sure about this one
           let a'' = eval env a' in
           do
             check env cxt a' VU
             check env cxt t' a''
             check ((x, Just (eval env t')) :: env) ((x, a'') :: cxt) u a
         _ => do
           tty <- infer env cxt t
           when (not (conv env tty a)) $
             -- (quoteShow env a) (quoteShow env tty))
             report ("type mismatch\n\nexpected type:\n\n  " ++ "" ++ "\n\ninferred type:\n\n " ++ "" ++ "\n")

-- printing

Show Tm where
  show (Var x) = x
  show (Lam x t) = "\\" ++ x ++ "." ++ (show t)
  show (App t u) = (show t) ++ (show u)
  show U = "U:"
  show (Pi x t u) = "(" ++ x ++ ":" ++ (show t) ++ "->" ++ (show u)
  show (Let x t u y) = "let " ++ x ++ " : " ++ (show t) ++ " = " ++ (show u) ++ " in " ++ (show y)
  show (SrcPos _ t) = show t

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
module Vect

%default total

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

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

-- finite sets

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

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

natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z (S _) = Just FZ
natToFin (S k) (S j) =
  case natToFin k j of
       Nothing => Nothing
       Just k' => Just (FS k')
natToFin _ _ = Nothing

vs : Vect 5 String
vs = ["hello", "world", "nice", "to", "meet"]

elementAt : { n : _ } -> Nat -> Vect n a -> Maybe a
elementAt idx vec = case natToFin idx n of
                         Nothing => Nothing
                         Just idx' => Just $ index idx' vec


text:
module Main

import Erlang

-- Wrappers around `create_curried_funX` that returns a curried, pure function

curriedFun1 : Int -> Int
curriedFun1 =
  let MkFun1 f = erlUnsafeCall (ErlFun1 Int Int) "test_support" "create_curried_fun1" []
  in f

curriedFun2 : Int -> Int -> Int
curriedFun2 =
  let MkFun1 f = erlUnsafeCall (ErlFun1 Int (ErlFun1 Int Int)) "test_support" "create_curried_fun2" []
  in (\x => let MkFun1 f' = f x in f')

-- Wrappers around `create_funX` that returns a pure function

callFun0 : Int
callFun0 =
  let MkFun0 fun = erlUnsafeCall (ErlFun0 Int) "test_support" "create_fun0" []
  in fun

callFun1 : Int -> Int
callFun1 =
  let MkFun1 fun = erlUnsafeCall (ErlFun1 Int Int) "test_support" "create_fun1" []
  in fun

callFun2 : Int -> Int -> Int
callFun2 =
  let MkFun2 fun = erlUnsafeCall (ErlFun2 Int Int Int) "test_support" "create_fun2" []
  in fun

-- Wrappers around `create_ioX` that returns an IO action

callIOFun0 : IO Int
callIOFun0 =
  let MkIOFun0 action = erlUnsafeCall (ErlIOFun0 Int) "test_support" "create_io0" []
  in action

callIOFun1 : Int -> IO Int
callIOFun1 =
  let MkIOFun1 action = erlUnsafeCall (ErlIOFun1 Int Int) "test_support" "create_io1" []
  in action

callIOFun2 : Int -> Int -> IO Int
callIOFun2 =
  let MkIOFun2 action = erlUnsafeCall (ErlIOFun2 Int Int Int) "test_support" "create_io2" []
  in action

-- Tests

curriedFunTest : IO ()
curriedFunTest = do
  putStrLn "curriedFunTest"
  printLn (curriedFun1 42)
  printLn (curriedFun2 42 100)

funTest : IO ()
funTest = do
  putStrLn "funTest"
  printLn callFun0
  printLn (callFun1 42)
  printLn (callFun2 1 2)

ioTest : IO ()
ioTest = do
  putStrLn "ioTest"
  res0 <- callIOFun0
  printLn res0
  res1 <- callIOFun1 42
  printLn res1
  res2 <- callIOFun2 1 2
  printLn res2

main : IO ()
main = do
  curriedFunTest
  funTest
  ioTest


text:
> module SimpleProb.BasicProperties

> import Data.List
> import Syntax.PreorderReasoning

> import SimpleProb.SimpleProb
> import SimpleProb.BasicOperations
> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Num.Refinements
> import List.Operations
> import List.Properties
> import Nat.Positive
> import Fraction.Normal

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

> |||
> toListLemma : {A : Type} -> (sp : SimpleProb A) -> sumMapSnd (toList sp) = 1
> toListLemma (MkSimpleProb _ prf) = prf

> |||
> sumProbsLemma : {A : Type} -> (sp : SimpleProb A) -> sum (probs sp) = 1
> sumProbsLemma {A} sp = ( sum (map snd (toList (normalize sp))) )
>                      ={ Refl }=
>                        ( sumMapSnd (toList (normalize sp)) )
>                      ={ toListLemma (normalize sp) }=
>                        ( 1 )
>                      QED

> |||
> lengthSupportProbsLemma : {A : Type} -> (sp : SimpleProb A) ->
>                           length (support sp) = length (probs sp)
> lengthSupportProbsLemma sp = lengthLemma (toList (normalize sp)) fst snd

> ||| SimpleProb is an implementation of Show
> implementation Show a => Show (SimpleProb a) where
>   show sp = show (toList sp)

> {-

> ---}


text:
module Control.Comonad.Traced

import public Control.Comonad.Traced.Traced as Control.Comonad.Traced
import public Control.Comonad.Traced.Interface as Control.Comonad.Traced


text:
module PLFI.Part1.Connectives

import Data.Fin
import PLFI.Part1.Isomorphism
import Syntax.PreorderReasoning.Generic

-- data _×_ (A B : Set) : Set where

--   ⟨_,_⟩ :
--       A
--     → B
--       -----
--     → A × B

test : (Int,Nat)
test = (0,0)

total
test2 : (Void,Nat)
test2 = (?x,0)

-- data TT : Type where
--   MkTT : TT

-- data TF : Type where

-- test3 : TF
-- test3 = ?x1

-- test4 : (TT, TT)
-- test4 = (MkTT, MkTT)

-- test5 : (TF, TT)
-- test5 = (?test5_rhs_1, MkTT)

-- test6 : (,) Nat Nat
-- test6 = (3,3)

data Sx : Nat -> Type where
  MkSx : Sx n

test7 : (x : Nat ** Sx x)
test7 = (3 ** MkSx)

test8 : DPair Nat (\x => Sx x)
test8 = MkDPair 3 MkSx

-- test8 : Sigma Nat (\x => Sx x)
-- test8 = MkSigma 3 MkSx

-- η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
etaTuple : {a,b : Type} -> (w : (a, b)) -> (fst w, snd w) === w
etaTuple (x, y) = Refl

-- data Bool : Set where
--   true  : Bool
--   false : Bool

-- data Tri : Set where
--   aa : Tri
--   bb : Tri
--   cc : Tri

data B : Type where
  True : B
  False : B

enumB : B -> Fin 2
enumB True = 0
enumB False = 1

-- data T : Type where
--   AA, BB, CC : T

-- enumT : T -> Fin 3
-- enumT AA = 0
-- enumT BB = 1
-- enumT CC = 2

tupleX : (a -> Fin n) -> (b -> Fin m) -> (a,b) -> Fin (n * m)
tupleX f s x = ?xy

-- timesCountBetween1and6 : (x: (Bool, Tri)) -> (timesCount x <= 6 && timesCount x >= 1) = True
-- timesCountBetween1and6 (False, Aa) = Refl
-- timesCountBetween1and6 (False, Bb) = Refl
-- timesCountBetween1and6 (False, Cc) = Refl
-- timesCountBetween1and6 (True, Aa) = Refl
-- timesCountBetween1and6 (True, Bb) = Refl
-- timesCountBetween1and6 (True, Cc) = Refl

-- ×-comm : ∀ {A B : Set} → A × B ≃ B × A
-- ×-comm =
--   record
--     { to       =  λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
--     ; from     =  λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
--     ; from∘to  =  λ{ ⟨ x , y ⟩ → refl }
--     ; to∘from  =  λ{ ⟨ y , x ⟩ → refl }
--     }

prodComm : Iso (a,b) (b,a)
prodComm =
  MkIso
    { to     = (\(x,y) => (y,x))
    , from   = (\(y,x) => (x,y))
    , fromTo = (\(x,y) => Refl)
    , toFrom = (\(y,x) => Refl)
    }

-- ×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
-- ×-assoc =
--   record
--     { to      = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ }
--     ; from    = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
--     ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
--     ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
--     }

prodAssoc : Iso ((a,b),c) (a,(b,c))
prodAssoc = MkIso
  { to      = \((x,y),z) => (x,(y,z))
  , from    = \(x,(y,z)) => ((x,y),z)
  , fromTo  = \((x,y),z) => Refl
  , toFrom  = \(x,(y,z)) => Refl
  }

-- data ⊤ : Set where
--   tt :
--     --
--     ⊤

data T : Type where
  TT : T

-- ------ T-I
-- TT : T

--  T , c
-- ------- T-E
--    c

-- elim:
-- c -> (T -> c)
-- c -> T -> c
-- c -> c

-- ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
-- ⊤-identityˡ =
--   record
--     { to      = λ{ ⟨ tt , x ⟩ → x }
--     ; from    = λ{ x → ⟨ tt , x ⟩ }
--     ; from∘to = λ{ ⟨ tt , x ⟩ → refl }
--     ; to∘from = λ{ x → refl }
--     }

ttIdentityL : {a : Type} -> Iso (T, a) a
ttIdentityL = MkIso
  { to     = \(TT,y) => y
  , from   = \x => (TT, x)
  , fromTo = \(TT,y) => Refl
  , toFrom = \y => Refl
  }

-- ⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
-- ⊤-identityʳ {A} =
--   ≃-begin
--     (A × ⊤)
--   ≃⟨ ×-comm ⟩
--     (⊤ × A)
--   ≃⟨ ⊤-identityˡ ⟩
--     A
--   ≃-∎

-- 0
test3 : {a,b,c : Type} -> Iso a b -> Iso b c -> Iso a c
test3 ab bc = CalcWith {leq = Iso} $
  |~ a
  <~ b ... (ab)
  <~ c ... (bc)

ttIdentityR : {a : Type} -> Iso (a,T) a
ttIdentityR = CalcWith {leq = Iso} $
  |~ (a, T)
  <~ (T, a)  ... prodComm
  <~ a       ... ttIdentityL

-- Same as Either, we are going to use Either
data Sum : Type -> Type -> Type where
  L : a -> Sum a b
  R : b -> Sum a b

-- the first introduces a formula for the connective, which appears in the conclusion but not in the hypotheses
--     x : a
-- ------------- Sum-I1
-- L x : Sum a b
--
--     x : b
-- ------------- Sum-I2
-- R x : Sum a b

-- the second eliminates a formula for the connective, which appears in a hypothesis but not in the conclusion
-- Sum a b , (a -> c) , (b -> c)
-- ----------------------------- Sum-E
--              c

-- case-⊎ : ∀ {A B C : Set}
--   → (A → C)
--   → (B → C)
--   → A ⊎ B
--     -----------
--   → C
-- case-⊎ f g (inj₁ x) = f x
-- case-⊎ f g (inj₂ y) = g y

-- either

-- η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w

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

etaEither : {a,b : Type} -> (w : Either a b) -> either Left Right w = w
etaEither (Left x) = Refl
etaEither (Right x) = Refl

testData1 : Either () Nat
testData1 = Right 1

test1 : Bool
test1 = either Left Right testData1 == (Right 1)

testData2 : Either Nat ()
testData2 = Left 2

test4 : Bool
test4 = either Left Right testData2 == (Left 2)

-- uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
uniqEither
  :  {a,b,c : Type} -> (h : Either a b -> c) -> (w : Either a b)
  -> either (h . Left) (h . Right) w = h w
uniqEither h (Left x) = Refl
uniqEither h (Right x) = Refl

-- test5 : let t = Nat = Nat in Either t t
-- test5 = Left Refl

commEither : Iso (Either a b) (Either b a)
commEither = MkIso
  { to     = either Right Left
  , from   = either Right Left
  , fromTo = \case
                (Left x) => Refl
                (Right x) => Refl
  , toFrom = \case
                (Left x) => Refl
                (Right x) => Refl
  }

assocEither : Iso (Either (Either a b) c) (Either a (Either b c))
assocEither = MkIso
  { to     = either (either Left (Right . Left)) (Right . Right)
  , from   = either (Left . Left) (either (Left . Right) Right)
  , fromTo = \case
                (Left (Left x))   => Refl
                (Left (Right x))  => Refl
                (Right x)         => Refl
  , toFrom = \case
                (Left x)          => Refl
                (Right (Left x))  => Refl
                (Right (Right x)) => Refl
  }

-- Couldn't parse any alternatives:
-- 1: Expected name.
-- ... (1 others)idris2
-- data G : Type where
--   { MkG : G
--   } -- c)

-- Without where clause it means something else, we declare this type, but we don't define it yet.
-- data F : Type          a)
-- declare data F : Type  a)

-- Suggestions for definition of empty type
-- data F : Type where -- b)

-- data F : Type where -- c)
--   impossible

-- data F : Type empty -- d)

-- data F : Type impossible -- e)

-- data F : Type where {}

data F : Type where -- c)

fElim : {0 a : Type} -> F -> a
fElim x impossible

fElim' : {a : Type} -> F -> a
fElim' = \x => case x of {} -- \case leads to a parse error

-- uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
-- uniq-⊥ h ()

uniqF : {c : Type} -> (h : F -> c) -> (w : F) -> fElim w = h w
uniqF h w impossible

-- ⊥-identityˡ

fIdentityL : Iso (Either F a) a
fIdentityL = MkIso
  { to     = either fElim id
  , from   = Right
  , fromTo = \case
                (Left x) => fElim x
                (Right x) => Refl
  , toFrom = \y => Refl
  }

fIdentityR : Iso (Either a F) a
fIdentityR = isoTrans commEither fIdentityL

-- η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
-- η-→ f = refl

-- TODO: Ask
--    a : Type
--    b : Type
--    f : a -> b
-- ------------------------------
-- xx : (\x => f x) = f
etaFun : {a,b : Type} -> (f : a -> b) -> (\x => f x) = f
etaFun f = Refl

--    a : Type
--    b : Type
--    f : a -> b
-- ------------------------------
-- xRefl : (\x => f x) = (\y => f y)
alphaFun : {a,b : Type} -> (f : a -> b) -> (\x => f x) = (\y => f y)
alphaFun f = Refl

-- Under the hood terms are normalized for alpha/eta equivalence?
alphaFun2 : {a,b,c : Type} -> (f : a -> b -> c) -> (z : b) -> (\x => f x z) = (\y => f y z)
alphaFun2 f z = Refl

betaFun : (y : Nat) -> (\x => x * x) y = y * y
betaFun y = Refl

namespace Newtype12

  export
  Person : Type
  Person = (String, Int)

  public export
  mkPerson : (String, Int) -> Person
  mkPerson = id

  public export
  unPerson : Person -> (String, Int)
  unPerson = id

  export
  0
  samePersonLemma : (p : Person) -> (mkPerson (unPerson p)) = p
  samePersonLemma p = Refl

  -- export
  -- samePersonLemma

test5 : Person
test5 = mkPerson ("Andor", 23)

-- samePersonLemma : (p : Person) -> (mkPerson (unPerson p)) = p
-- samePersonLemma p = Refl

samePersonLemmaR : (p : (String, Int)) -> (unPerson (mkPerson p) = p)
samePersonLemmaR p = ?h1_0

handwaving : {t : Type} -> (a : t) -> (b : t) -> (a = b)
handwaving a b = believe_me (the (a=a) Refl)

namespace Postulate

  export
  extensionality : {a,b : Type} -> {f,g : a -> b} -> ((x : a) -> f x = g x) -> f = g
  extensionality _ = handwaving f g

-- currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying : {a,b,c : Type} -> Iso (a -> b -> c) ((a,b) -> c)
currying = MkIso
  { to      = \f => \(x,y) => f x y
  , from    = \f => \x => \y => f (x, y)
  , fromTo  = \f => Refl
  , toFrom  = \g => extensionality (\(x,y) => Refl)
  }

-- c ^ (a + b) ~ c ^ a * c ^ b
-- →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
distribFunOverSumR : {a,b,c : Type} -> Iso (Either a b -> c) (a -> c, b -> c)
distribFunOverSumR = MkIso
  { to     = \f     => (f . Left, f . Right)
  , from   = \(f,g) => either f g
  , fromTo = \f     => extensionality (\case { Left x => Refl ; Right y => Refl })
  , toFrom = \(f,g) => Refl
  }

-- →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
-- (p * n) ^ m = (p ^ m) * (n ^ m)
distribFunOverProdL : {a,b,c : Type} -> Iso (a -> (b,c)) (a -> b, a -> c)
distribFunOverProdL = MkIso
  { to     = \f     => (fst . f, snd . f)
  , from   = \(f,g) => \x => (f x, g x)
  , fromTo = \f     => extensionality (\x => etaTuple (f x)) -- TODO: Next time cong
  , toFrom = \(f,g) => Refl
  }

-- →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
-- (p * n) ^ m = (p ^ m) * (n ^ m)
distribFunOverProdL2 : {a,b,c : Type} -> Iso (a -> (b,c)) (a -> b, a -> c)
distribFunOverProdL2 = MkIso
  { to     = \f     => (fst . f, snd . f)
  , from   = \(f,g) => \x => (f x, g x)
  , fromTo = \f     => extensionality (\x => cong id (cong id (cong id (etaTuple (f x)))))
  , toFrom = \(f,g) => Refl
  }

-- ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
distribProdOverSum  : {a,b,c : Type} -> Iso (Either a b, c) (Either (a,c) (b,c))
distribProdOverSum = MkIso
  { to = \(x,y) => bimap (,y) (,y) x
  , from = either (mapFst Left) (mapFst Right)
  -- , fromTo = \(x, y) => either (\z => ?h1) ?h2 x -- (const Refl) (const Refl) x
  , fromTo = \(x, y) => case x of
                (Left z) => Refl
                (Right z) => Refl
  , toFrom = \case
                (Left (x, y)) => Refl
                (Right (x, y)) => Refl
  }

-- ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
weakDistribSumOverProd : {a,b,c : Type} -> (Either (a,b) c) <= (Either a c, Either b c)
weakDistribSumOverProd = MkEmb
  { to = \case
            (Left (x, y)) => (Left x, Left y)
            (Right x) => (Right x, Right x)
  , from = \case
              ((Right x), y        ) => Right x
              ((Left x) , (Right y)) => Right y
              ((Left x) , (Left y) ) => Left (x, y)
  , fromTo = \case
                (Left (x, y)) => Refl
                (Right x) => Refl
  }

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module GenericArity

-- Inspired by https://strathprints.strath.ac.uk/68800/

import Data.Vect

%access public export

Types : Nat -> Type
Types n = Vect n Type

Arrows : (n : Nat) -> Types n -> Type -> Type
Arrows Z [] b = b
Arrows (S n) (a :: as) b = a -> Arrows n as b

Product : (n : Nat) -> Types n -> Type
Product Z [] = ()
Product (S n) (a :: as) = (a, Product n as)

curryn : (n : Nat) -> {as : Types n} -> (Product n as -> r) -> Arrows n as r
curryn Z {as = []} f = f ()
curryn (S n) {as = (a :: as)} f = curryn n . curry f

uncurryn : (n : Nat) -> {as : Types n} -> Arrows n as r -> (Product n as -> r)
uncurryn Z {as = []} f () = f
uncurryn (S n) {as = (a :: as)} f (x, prod) = uncurryn n (f x) prod

Cong : (n : Nat) -> {as : Types n} -> Arrows n as r -> Arrows n as r -> Type
Cong Z {as = []} f g = f = g
Cong (S n) {as = (a :: as)} f g = {x, y : a} -> x = y -> Cong n (f x) (g y)

congn : (n : Nat) -> {as : Types n} -> {r : Type} -> (f : Arrows n as r) -> Cong n {as} f f
congn Z {as = []} f = Refl
congn (S n) {as = (a :: as)} f = \(Refl {x}) => congn n {as} (f x)

cong : {a, b : Type} -> {f : a -> b} -> {x, y : a} -> x = y -> f x = f y
cong {a} {b} {f} = let r = congn 1 {as = (a :: [])} {r = b} f in r

testCong : (f : Int -> String -> Bool) -> f 1 "1" = f 1 "1"
testCong f = let r = congn 2 {as = (Int :: String :: [])} {r = Bool} f in r Refl Refl

Subst : (n : Nat) -> {as : Types n} -> Arrows n as Type -> Arrows n as Type -> Type
Subst Z {as = []} p q = p -> q
Subst (S n) {as = (a :: as)} p q = {x, y : a} -> x = y -> Subst n (p x) (p y)

substn : (n : Nat) -> {as : Types n} -> (p : Arrows n as Type) -> Subst n {as} p p
substn Z {as = []} p = id
substn (S n) {as = (a :: as)} p = \(Refl {x}) => substn n {as} (p x)

subst : {a : Type} -> (p : a -> Type) -> {x, y : a} -> x = y -> p x -> p y
subst {a} p = let r = substn 1 {as = (a :: [])} p in r

testSubst : (p : Int -> String -> Type) -> p 1 "1" -> p 1 "1"
testSubst p = let r = substn 2 {as = (Int :: String :: [])} p in r Refl Refl


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

import Effect.Perf

import Config.YAML

import Sif.Effs
import Sif.Options
import Sif.FileIO

%access export

private
convMaybe : Maybe String -> YAMLNode
convMaybe Nothing  = YAMLNull
convMaybe (Just m) = YAMLString m

private
convSplit : Pair Integer (Maybe String)
         -> Pair YAMLNode YAMLNode
convSplit (t,d) = MkPair
    (YAMLString "split")
    (YAMLMap
      [ MkPair (YAMLString "time") (YAMLFloat $ cast t)
      , MkPair (YAMLString "desc") (convMaybe d)])

private
doCounters : List (String, Nat) -> Pair YAMLNode YAMLNode
doCounters cs = MkPair (YAMLString "counters")
                       (YAMLMap $ map doConv cs)
  where
    doConv : Pair String Nat
          -> Pair YAMLNode YAMLNode
    doConv (k,v) = MkPair (YAMLString "counter")
                          (YAMLMap
      [ MkPair (YAMLString "value") (YAMLInt $ cast k)
      , MkPair (YAMLString "desc")  (YAMLString k)
      ])

private
doTimers : List (String, Timer) -> Pair YAMLNode YAMLNode
doTimers ts = MkPair (YAMLString "timers")
                     (YAMLMap (map doConv ts))
  where
    convSplits : List (Integer, Maybe String)
              -> List (YAMLNode, YAMLNode)
    convSplits xs = map convSplit xs

    convTimer : Timer -> YAMLNode
    convTimer (MkTimer d a z ss) = YAMLMap
        [ MkPair (YAMLString "desc")   (YAMLString d)
        , MkPair (YAMLString "start")  (YAMLFloat $ cast a)
        , MkPair (YAMLString "start")  (YAMLFloat $ cast z)
        , MkPair (YAMLString "splits") (YAMLMap $ convSplits ss)]

    doConv : Pair String Timer -> Pair YAMLNode YAMLNode
    doConv (k,v) = MkPair (YAMLString "timer")
                          (convTimer v)
private
doStamps : Integer
        -> List (String, Integer)
        -> Pair YAMLNode YAMLNode
doStamps s ss = MkPair (YAMLString "timestamps")
                       (YAMLMap $ map doConv ss)
  where
    doConv : Pair String Integer -> Pair YAMLNode YAMLNode
    doConv (m,i) = MkPair (YAMLString "stamp")
                          (YAMLMap [convSplit (i - s, Just m)])
private
toYAML : PMetrics -> YAMLNode
toYAML m = YAMLDoc Nil inner
  where
    inner : YAMLNode
    inner = YAMLMap
        [ doCounters (counters m)
        , doTimers (timers m)
        , doStamps (stime m) (stamps m)]

perfSetup : Sif ()
perfSetup = do
    os <- getOptions
    let (gather,display) = perf os
    if gather
      then collectPMetrics display
      else pure ()

displayPerfMetrics : Sif ()
displayPerfMetrics = do
    os <- getOptions
    mdata <- getPerfMetrics
    case perf os of
      (True, True)  => do
          printLn $ displayPerfMetrics mdata
          writeFile "perf.yaml" (YAML.toString $ toYAML mdata)
      (True, False) => do
          writeFile "perf.yaml" (YAML.toString $ toYAML mdata)
      otherwise => pure ()

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
-- ------------------------------------------------------ [ Tree.idr<RedBlack> ]
-- Module    : Tree.idr
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
-- http://www.cs.kent.ac.uk/people/staff/smk/redblack/Untyped.hs
module Data.RedBlack.Tree

%access export

private
data Colour = R | B

data Tree : Type -> Type where
  Empty : Tree a
  Node  : Colour -> a -> Tree a -> Tree a -> Tree a

balance : a -> Tree a -> Tree a -> Tree a
balance y (Node R x a              b) (Node R z c d) = Node R y (Node B x a b) (Node B z c d)
balance z (Node R y (Node R x a b) c) d              = Node R y (Node B x a b) (Node B z c d)
balance z (Node R x a                 (Node R y b c)) d = Node R y (Node B x a b) (Node B z c d)
balance x a                           (Node R y b (Node R z c d)) = Node R y (Node B x a b) (Node B z c d)
balance x a                           (Node R z (Node R y b c) d) = Node R y (Node B x a b) (Node B z c d)
balance x a                           b = Node B x a b

private
ins : Ord a => a -> Tree a -> Tree a
ins x Empty            = Node R x Empty Empty
ins x t@(Node B y a b) =
    case compare x y of
        LT => balance y (ins x a) b
        GT => balance y a         (ins x b)
        EQ => t
ins x t@(Node R y a b) =
    case compare x y of
        LT => Node R y (ins x a) b
        GT => Node R y a         (ins x b)
        EQ => t

foldr : (step : a -> p -> p) -> (init : p) -> Tree a -> p
foldr step init n = foldr' step init n
  where
    foldr' : (a -> p -> p) -> p -> Tree a -> p
    foldr' step' init' Empty = init'
    foldr' step' init' (Node _ val l r) = foldr' step' (step' val (foldr' step' init' r)) l

size : Tree a -> Nat
size t = Tree.foldr (\_,res => S res) Z t

contains : Ord a => a -> Tree a -> Bool
contains x Empty = False
contains x (Node _ y l r) =
  case compare x y of
    LT => contains x l
    GT => contains x r
    EQ => True

empty : Tree a
empty = Empty

insert : Ord a => a -> Tree a -> Tree a
insert x s = let Node _ z l r = ins x s in Node B z l r

toList : Tree a -> List a
toList Empty = Nil
toList (Node _ y l r) = Tree.toList l ++ [y] ++ Tree.toList r

fromList : Ord a => List a -> Tree a
fromList xs = foldl (flip $ insert) empty xs

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Depling.Pull

import Depling
import Data.Fin
import Data.Vect
import Utils

mutual
	total
	pull_ℙ : Fin (S n) -> DAST (a + (S n)) -> Maybe (DAST (a + n))
	pull_ℙ {a=Z} pv ast = pull pv ast
	pull_ℙ {a=S a} {n} pv ast =
		assert_total $
		replace {P=Maybe . DAST} (sym $ plusSuccRightSucc _ _) $
		pull_ℙ (FS pv) $
		replace (plusSuccRightSucc _ _) $
		ast

	total
	export
	pull : Fin (S n) -> DAST (S n) -> Maybe (DAST n)
	pull pv (ʌ v) = case fcompare v pv of
		FLT lt => Just $ ʌ $ finDown v {lt}
		FEQ eq => Nothing
		FGT gt => Just $ ʌ $ finD v {gt}
	pull pv (λ at b) = do
		at' <- pull pv at
		b' <- pull (FS pv) b
		pure $ λ at' b'
	pull pv (λT at rt) = do
		at' <- pull pv at
		rt' <- pull (FS pv) rt
		pure $ λT at' rt'
	pull pv (f =!= a) = do
		f' <- pull pv f
		a' <- pull pv a
		pure $ f' =!= a'
	pull pv 𝕋 = Just 𝕋
	pull pv (𝔽 at rt b) = do
		at' <- pull          pv  at
		rt' <- pull (FS$     pv) rt
		b'  <- pull (FS$ FS$ pv) b
		pure $ 𝔽 at' rt' b'
	pull pv (𝕌 n t) = do
		t' <- pull pv t
		pure $ 𝕌 n t'
	pull pv (ℂ cn as) = do
		as' <- sequence $ map (assert_total $ pull pv) as
		pure $ ℂ cn as'
	pull pv (ℙ v cn t f) = do
		v' <- pull pv v
		t' <- pull_ℙ pv t
		f' <- pull pv f
		pure $ ℙ v' cn t' f'
	pull pv (𝔹 t) = do
		t' <- pull pv t
		pure $ 𝔹 t'

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Data.Stream.Extra

%default total

||| Insert elements from a Foldable at the start of an existing Stream
||| @ pfx the Foldable containing elements to prepend
||| @ stream the Stream to prepend the elements to
public export
startWith : Foldable t => (pfx : t a) -> (stream : Stream a) -> Stream a
startWith pfx stream = foldr (\x, xs => x :: xs) stream pfx


text:
module Data.Time.Clock.UTCTime

import public Data.Time.Clock.Internal.UTCTime

import Data.Fixed
import Data.Time.Clock.DiffTime
import Data.Time.Calendar.Days
import Data.Time.LocalTime.Internal.LocalTime
import Data.Time.LocalTime.TimeZone
import Data.Time.LocalTime.ZonedTime

%default total
-- ---------------------------------------------------------------------------

-- orphan instance
public export Show UTCTime where show t = show $ utcToZonedTime utc t

export addUTCTime : NominalDiffTime -> UTCTime -> UTCTime
addUTCTime a b =
  let s = a.seconds + b.daytime.seconds
      d = s `div'` nominalDay.seconds
      t = s `mod'` nominalDay.seconds
      in MkUTCTime (addDays d b.day) (secondsToDiffTime t)

export diffUTCTime : UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime a b =
  let d = diffDays a.day b.day
      t = a.daytime.seconds - b.daytime.seconds
      in SecondsToDiffTime $ scale d nominalDay.seconds + t


text:
module Generic

%default total

double : Num ty => ty -> ty
double x = x + x

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- ---------------------------------------------------------- [ Projection.idr ]
-- Module    : Projection.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| How to project Interface Descriptions to local descriptions.
module Cordial.Model.Projection

import Data.Vect
import Data.DList

import Text.Markup.Edda

import public Cordial.Model.Common
import        Cordial.Model.Specification

%hide DList.map

%default total
%access public export

||| Projected port models abstractly an interfaces structure.
|||
||| A projected port is similar to an abstract port type with two major differences.
|||
||| 1. Flows reconstituted as directions based on the endpoint; and
||| 2. Use of the port (required or optional) translated from abstract port.
data ProjectedPortTy : (labelTy  : Type)
                    -> (endpoint : Endpoint)
                    -> (type   : PortTy annot labelTy)
                    -> Type
  where
    PPortDesc : (kind   : PortShape)
             -> (label  : Name nKind labelTy)
             -> (wireTy : WireTy)
             -> (dir    : Direction endpoint flow)
             -> (pwidth : PortWidthDesc kind)

             -> (sens   : Sensitivity)

             -> (required : Necessary endpoint req)

             -> (origin : Origin)

             -> (vorigin  : ValueOrigin width)

             -> ProjectedPortTy labelTy
                                endpoint
                                (PortDesc i kind label wireTy flow width sens req origin vorigin doc)

necessary : ProjectedPortTy labelTy endpoint type
         -> Necessary (calcOptTy endpoint (required type)) endpoint (required type) (calcOptKind endpoint (required type))
necessary (PPortDesc kind label wireTy dir pwidth sens required origin vorigin) = required

origin : (o : Origin)
      -> ProjectedPortTy l e (PortDesc i kind label wireTy flow width sens req origin vorigin doc)
      -> ProjectedPortTy l e (PortDesc i kind label wireTy flow width sens req o      vorigin doc)
origin o (PPortDesc k l w d p s r _ vo) = (PPortDesc k l w d p s r o vo)

data OptionalProjectedPort : (type : PortTy annot labelTy)
                          -> (endpoint : Endpoint)
                          -> (projectedType : ProjectedPortTy labelTy endpoint type)
                          -> Type
    where
      ProjectedPortIsOptional : (prf : OptionalPortType endpoint type)
                             -> OptionalProjectedPort type endpoint projectedType

data SystemProjectedPort : (type : PortTy annot labelTy)
                        -> (projectedType : ProjectedPortTy labelTy endpoint type)
                        -> Type
    where
      ProjectedPortIsSystem : (prf : SystemPortType type)
                           -> SystemProjectedPort type projectedType

data IPProjectedPort : (type : PortTy annot labelTy)
                    -> (projectedType : ProjectedPortTy labelTy endpoint type)
                    -> Type
    where
      ProjectedPortIsIP : (prf : IPPortType type)
                       -> IPProjectedPort type projectedType

projectedPortIsIP : (contra : SystemPortType type -> Void) -> SystemProjectedPort type projectedType -> Void
projectedPortIsIP contra (ProjectedPortIsSystem prf) = contra prf

projectedPortIsSystem : (contra : IPPortType type -> Void) -> IPProjectedPort type projectedType -> Void
projectedPortIsSystem contra (ProjectedPortIsIP prf) = contra prf

isProjectedPortIP : (projectedType : ProjectedPortTy labelTy endpoint type)
                 -> Dec (IPProjectedPort type projectedType)
isProjectedPortIP projectedType {type} with (isPortTypeIP type)
  isProjectedPortIP projectedType {type = type} | (Yes prf) = Yes (ProjectedPortIsIP prf)
  isProjectedPortIP projectedType {type = type} | (No contra) = No (projectedPortIsSystem contra)

isProjectedPortSystem : (projectedType : ProjectedPortTy labelTy endpoint type)
                     -> Dec (SystemProjectedPort type projectedType)
isProjectedPortSystem projectedType {type} with (isPortTypeSystem type)
  isProjectedPortSystem projectedType {type = type} | (Yes prf) = Yes (ProjectedPortIsSystem prf)
  isProjectedPortSystem projectedType {type = type} | (No contra) = No (projectedPortIsIP contra)

||| Projected port group is a list of projected ports in which we
||| collect at the type level the abstract ports indexing the
||| projected port types.
ProjectedPortGroupTy : (labelTy : Type)
                    -> (endpoint : Endpoint)
                    -> List (PortTy annot labelTy)
                    -> Type
ProjectedPortGroupTy labelTy endpoint =
  DList (PortTy annot labelTy) (ProjectedPortTy labelTy endpoint)

mapDList : (tyF  : aTy -> bTy)
        -> (valF : {a : aTy} -> {b : bTy} -> eTy a -> fTy b)
        -> DList.DList aTy eTy as
        -> DList.DList bTy fTy (map tyF as)
mapDList tyF valF []      = []
mapDList tyF valF (x::xs) = valF x :: Projection.mapDList tyF valF xs

setOrigin : (o : Origin)
       -> ProjectedPortGroupTy labelTy endpoint ps
       -> ProjectedPortGroupTy labelTy endpoint (map (record {origin = o}) ps)
setOrigin o pps with (pps)
  setOrigin o pps | [] = []
  setOrigin o pps | (elem :: rest) with (elem)
    setOrigin o pps | (elem :: rest) | (PPortDesc kind label wireTy dir pwidth sens required origin vorigin) =
     PPortDesc kind label wireTy dir pwidth sens required o vorigin :: setOrigin o rest

||| A projected interface is similar to an abstract interface but
||| containing list of projected ports.
|||
data ProjectedInterfaceTy : (labelTy     : Type)
                         -> (endpoint    : Endpoint)
                         -> (interfaceTy : InterfaceTy annot labelTy)
                         -> Type
  where
    MkPInterfaceTy : (vlnv : VLNV)
                  -> (commStyle : CommStyle)
                  -> (portgroup : ProjectedPortGroupTy labelTy endpoint (portTys ++ flatten chans))
                  -> ProjectedInterfaceTy labelTy endpoint (MkInterfaceTy vlnv i commStyle mc mp portTys chans doc)

projectedPortGroup : ProjectedInterfaceTy labelTy endpoint interfaceTy
                   -> ProjectedPortGroupTy labelTy endpoint (portGroupTy interfaceTy ++ flatten (channels interfaceTy))
projectedPortGroup (MkPInterfaceTy vlnv cStyle portgroup) = portgroup

||| A collection of projected interfaces.
data ProjectedInterfaceTys : (hs : List Type)
                          -> (interfaceTys : InterfaceTys annot hs)
                          -> (es           : List Endpoint)
                          -> Type
  where
    Nil : ProjectedInterfaceTys Nil Nil Nil
    (::) : {i : InterfaceTy annot labelTy}
        -> ProjectedInterfaceTy labelTy e i
        -> ProjectedInterfaceTys hs is es
        -> ProjectedInterfaceTys (labelTy::hs) (i :: is) (e::es)

data ProjectTypes : (endpoint : Endpoint)
                 -> (flow     : Flow)
                 -> (dty      : DirectionTy)
                 -> (opt      : OptionalTy)
                 -> (oty      : OptTy)
                 -> Type where
  Witness : (necessary : Necessary (calcOptTy endpoint opt) endpoint opt (calcOptKind endpoint opt))
         -> (direction : Direction (calcDirTy endpoint flow) endpoint flow (calcDirKind endpoint flow))
         -> ProjectTypes endpoint flow (calcDirTy endpoint flow) opt (calcOptTy endpoint opt)

projectTypes : (endpoint : Endpoint)
            -> (flow     : Flow)
            -> (opt      : OptionalTy)
            -> ProjectTypes endpoint flow (calcDirTy endpoint flow) opt (calcOptTy endpoint opt)
projectTypes endpoint flow opt = Witness (calcNecessary endpoint opt) (calcDirection endpoint flow)

||| Project an abstract port description according to the presented endpoint.
|||
||| @endpoint The 'direction' to project in.
||| @portTy   The abstract port to project.
projectPort : (endpoint : Endpoint)
           -> (portTy   : PortTy annot labelTy)
           -> ProjectedPortTy labelTy endpoint portTy
projectPort e p with (p)
  projectPort e p | (PortDesc info kind label wkind flow width sens required origin valueOrigin doc) with (projectTypes e flow required)
    projectPort e p | (PortDesc info kind label wkind flow width sens required origin valueOrigin doc) | (Witness necessary direction) =
      PPortDesc kind label wkind direction width sens necessary origin valueOrigin

||| Project an abstract interface description according to the presented endpoint.
|||
||| @endpoint    The 'direction' to project in.
||| @interfaceTy The abstract interface to project.
projectInterface : (endpoint    : Endpoint)
                -> (interfaceTy : InterfaceTy annot labelTy)
                -> ProjectedInterfaceTy labelTy endpoint interfaceTy
projectInterface endpoint (MkInterfaceTy vlnv info commStyle maxConsumers maxProducers ports chans doc) =
    MkPInterfaceTy vlnv commStyle (projectPorts ports ++ projectPorts (flatten chans))
  where
    projectPorts : (ps : List (PortTy annot labelTy))
                -> DList (PortTy annot labelTy) (ProjectedPortTy labelTy endpoint) ps
    projectPorts [] = []
    projectPorts (x :: xs) = projectPort endpoint x :: projectPorts xs

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Main

main : JS_IO ()
main = putStr' $ show $ take 5 $ repeat 1

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
import Js.DOM.Document

%default total

main : JS_IO ()
main = write "
Hello Electron, Hello Idris!
"

max_stars_repo_name: jheiling/idris-electron

max_issues_repo_name: jheiling/idris-electron

max_forks_repo_name: jheiling/idris-electron


text:
module Main

simple : String
simple = "hello"

add : Nat -> Nat -> Nat
add (S k) y = S (add k y)
add Z     y = y

getType : Bool -> Type
getType True  = Integer
getType False = String

bla : (x : Bool) -> getType x
bla True  = 0
bla False = "false"

main : IO ()
main = do
  putStrLn ("one: "   ++ simple)
  putStrLn ("two: "   ++ x)
  putStrLn ("three: " ++ y)
    where
      x : String
      x = cast $ cast { to = Int } (add 1 5)

      y : String
      y = bla False

max_stars_repo_name: mkulke/idris-playground

max_issues_repo_name: mkulke/idris-playground

max_forks_repo_name: mkulke/idris-playground


text:
||| The content of this module is based on the
||| tutorial post about [refined primitives](../../Doc/Primitives.md).
module Language.Reflection.Refined

import public Data.Maybe
import public Data.So
import public Language.Reflection.Derive

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

public export
maybeSo : (b : Bool) -> Maybe (So b)
maybeSo True  = Just Oh
maybeSo False = Nothing

public export
refineSo :  {f : a -> Bool}
         -> (make : (v : a) -> (0 prf : So $ f v) -> b)
         -> (val : a)
         -> Maybe b
refineSo make val = case maybeSo (f val) of
                         Just oh => Just $ make val oh
                         Nothing => Nothing

--------------------------------------------------------------------------------
--          Elab Scripts
--------------------------------------------------------------------------------

||| Creates an `Eq` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedEq "AtomicNr" `{{value}}
||| ```
export covering
refinedEq : (dataType : String) -> (accessor : Name) -> Elab ()
refinedEq dt accessor =
  let eqFun   = UN $ "implEq"   ++ dt
      tpe     = varStr dt
      acc     = var accessor

   in declare
        [ interfaceHint Public eqFun `(Eq ~(tpe))
        , def eqFun [patClause (var eqFun) `(mkEq ((==) `on` ~(acc)))]
        ]

||| Creates an `Ord` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedOrd "AtomicNr" `{{value}}
||| ```
export covering
refinedOrd : (dataType : String) -> (accessor : Name) -> Elab ()
refinedOrd dt accessor =
  let ordFun  = UN $ "implOrd"  ++ dt

      tpe     = varStr dt
      acc     = var accessor

   in declare
        [ interfaceHint Public ordFun `(Ord ~(tpe))
        , def ordFun [patClause (var ordFun) `(mkOrd (compare `on` ~(acc)))]
        ]

||| Creates a `Show` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedShow "AtomicNr" `{{value}}
||| ```
export covering
refinedShow : (dataType : String) -> (accessor : Name) -> Elab ()
refinedShow dt accessor =
  let showFun = UN $ "implShow" ++ dt

      tpe     = varStr dt
      acc     = var accessor

   in declare
        [ interfaceHint Public showFun `(Show ~(tpe))
        , def showFun [patClause (var showFun)
                       `(mkShowPrec (\p => showPrec p . ~(acc)))]
        ]

||| Convenience function combining `refinedEq`, `refinedOrd`,
||| and `refinedShow`.
export covering
refinedEqOrdShow : (dataType : String) -> (accessor : Name) -> Elab ()
refinedEqOrdShow dt acc = do refinedEq dt acc
                             refinedOrd dt acc
                             refinedShow dt acc

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined integral number.
|||
||| Conversion functions are called `refine` and `fromInteger`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedIntegral "AtomicNr"
|||                          `{{MkAtomicNr}}
|||                          `{{value}}
|||                          `(Int)
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq AtomicNr where
|||   (==) = (==) `on` value
|||
||| Ord AtomicNr where
|||   compare = compare `on` value
|||
||| Show AtomicNr where
|||   showPrec p = showPrec p . value
|||
||| namespace AtomicNr
|||   refine : Int -> Maybe AtomicNr
|||   refine = refineSo MkAtomicNr
|||
|||   fromInteger :  (v : Integer)
|||               -> {auto 0 _: IsJust (refine $ fromInteger v)}
|||               -> AtomicNr
|||   fromInteger v = fromJust (refine $ fromInteger v)
||| ```
export covering
refinedIntegral :  (dataType : String)
                -> (con      : Name)
                -> (accessor : Name)
                -> (tpe      : TTImp)
                -> Elab ()
refinedIntegral dt con acc tpe =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN "refine")

   in refinedEqOrdShow dt acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : ~(tpe) -> Maybe ~(varStr dt)
             refine = refineSo ~(var con)

             public export
             fromInteger :  (n : Integer)
                         -> {auto 0 _: IsJust (~(refineNS) $ fromInteger n)}
                         -> ~(varStr dt)
             fromInteger n = fromJust (refine $ fromInteger n)
           ]
        ]

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedInt "AtomicNr"
||| ```
export covering
refinedInt : (dataType : String) -> Elab ()
refinedInt dt = refinedIntegral dt (UN $ "Mk" ++ dt) `{{value}} `(Int)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedBits8 : (dataType : String) -> Elab ()
refinedBits8 dt = refinedIntegral dt (UN $ "Mk" ++ dt) `{{value}} `(Bits8)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedBits16 : (dataType : String) -> Elab ()
refinedBits16 dt = refinedIntegral dt (UN $ "Mk" ++ dt) `{{value}} `(Bits16)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedBits32 : (dataType : String) -> Elab ()
refinedBits32 dt = refinedIntegral dt (UN $ "Mk" ++ dt) `{{value}} `(Bits32)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedBits64 : (dataType : String) -> Elab ()
refinedBits64 dt = refinedIntegral dt (UN $ "Mk" ++ dt) `{{value}} `(Bits64)

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined floating point
||| number.
|||
||| Conversion functions are called `refine` and `fromDouble`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record Abundance where
|||   constructor MkAbundance
|||   value : Double
|||   0 inBounds : So (0 < value && value <= 1)
|||
||| %runElab refinedFloating "Abundance" `{{MkAbundance}} `{{value}}
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq Abundance where
|||   (==) = (==) `on` value
|||
||| Ord Abundance where
|||   compare = compare `on` value
|||
||| Show Abundance where
|||   showPrec p = showPrec p . value
|||
||| namespace Abundance
|||   refine : Double -> Maybe Abundance
|||   refine = refineSo MkAbundance
|||
|||   fromDouble :  (v : Double)
|||              -> {auto 0 _: IsJust (refine v)}
|||              -> Abundance
|||   fromDouble v = fromJust (refine v)
||| ```
export covering
refinedFloating :  (dataType : String)
                -> (con      : Name)
                -> (accessor : Name)
                -> Elab ()
refinedFloating dt con acc =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN "refine")

   in refinedEqOrdShow dt acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : Double -> Maybe ~(varStr dt)
             refine = refineSo ~(var con)

             public export
             fromDouble :  (n : Double)
                        -> {auto 0 _: IsJust (~(refineNS) n)}
                        -> ~(varStr dt)
             fromDouble n = fromJust (refine n)
           ]
        ]

||| Convenience version of `refinedFloating` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedDouble : (dataType : String) -> Elab ()
refinedDouble dt = refinedFloating dt (UN $ "Mk" ++ dt) `{{value}}

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined string value.
|||
||| Conversion functions are called `refine` and `fromString`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record Html where
|||   constructor MkHtml
|||   value : String
|||   0 inBounds : So (isValidHtml value)
|||
||| %runElab refinedText "Html" `{{MkHtml}} `{{value}}
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq Html where
|||   (==) = (==) `on` value
|||
||| Ord Html where
|||   compare = compare `on` value
|||
||| Show Html where
|||   showPrec p = showPrec p . value
|||
||| namespace Html
|||   refine : String -> Maybe Html
|||   refine = refineSo MkHtml
|||
|||   fromString :  (v : String)
|||              -> {auto 0 _: IsJust (refine v)}
|||              -> Html
|||   fromString v = fromJust (refine v)
||| ```
export covering
refinedText :  (dataType : String)
            -> (con      : Name)
            -> (accessor : Name)
            -> Elab ()
refinedText dt con acc =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN "refine")

   in refinedEqOrdShow dt acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : String -> Maybe ~(varStr dt)
             refine = refineSo ~(var con)

             public export
             fromString :  (n : String)
                        -> {auto 0 _: IsJust (~(refineNS) n)}
                        -> ~(varStr dt)
             fromString n = fromJust (refine n)
           ]
        ]

||| Convenience version of `refinedText` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export covering
refinedString : (dataType : String) -> Elab ()
refinedString dt = refinedText dt (UN $ "Mk" ++ dt) `{{value}}


text:
module Mrk.LinkTypes

%default total
%access public export

data LinkType
  = Alternate
  | Archives
  | Author
  | Bookmark
  | External
  | Feed
  | First
  | Help
  | Icon
  | Index
  | Last
  | License
  | Next
  | Nofollow
  | Noreferrer
  | Pingback
  | Prefetch
  | Prev
  | Search
  | Stylesheet
  | Sidebar
  | Tag
  | Up
%name LinkType rel

Show LinkType where
  show x =
    case x of
         Alternate => "alternate"
         Archives => "archives"
         Author => "author"
         Bookmark => "bookmark"
         External => "external"
         Feed => "feed"
         First => "first"
         Help => "help"
         Icon => "icon"
         Index => "index"
         Last => "last"
         License => "license"
         Next => "next"
         Nofollow => "nofollow"
         Noreferrer => "noreferrer"
         Pingback => "pingback"
         Prefetch => "prefetch"
         Prev => "prev"
         Search => "search"
         Stylesheet => "stylesheet"
         Sidebar => "sidebar"
         Tag => "tag"
         Up => "up"

Eq LinkType where
  (==) x y = show x == show y

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module CIL.System.IO.File

import CIL.FFI

%access public export

namespace System.IO.File

  %inline
  FileTy : CILTy
  FileTy = CILTyRef "System.IO.FileSystem" "System.IO.File"

  %inline
  ReadAllText : String -> CIL_IO String
  ReadAllText = invokeStatic FileTy "ReadAllText" (String -> CIL_IO String)

  %inline
  WriteAllText : String -> String -> CIL_IO ()
  WriteAllText = invokeStatic FileTy "WriteAllText" (String -> String -> CIL_IO ())

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Main

import Lightyear.Core

main : IO ()
main = putStrLn "Hello, world!"

max_stars_repo_name: samvher/tsqlparser

max_issues_repo_name: samvher/tsqlparser

max_forks_repo_name: samvher/tsqlparser


text:
= Maps: Total and Partial Maps

> module Maps
>
> import Logic
> import IndProp
>
> %access public export
>

Maps (or dictionaries) are ubiquitous data structures both generally and in the
theory of programming languages in particular; we're going to need them in many
places in the coming chapters. They also make a nice case study using ideas
we've seen in previous chapters, including building data structures out of
higher-order functions (from `Basics` and `Poly`) and the use of reflection to
streamline proofs (from `IndProp`).

We'll define two flavors of maps: _total_ maps, which include a "default"
element to be returned when a key being looked up doesn't exist, and _partial_
maps, which return a \idr{Maybe} to indicate success or failure. The latter is
defined in terms of the former, using \idr{Nothing} as the default element.

== The Idris Standard Library

\todo[inline]{Edit}

One small digression before we get to maps.

Unlike the chapters we have seen so far, this one does not `Require Import` the
chapter before it (and, transitively, all the earlier chapters). Instead, in
this chapter and from now, on we're going to import the definitions and theorems
we need directly from Idris's standard library stuff. You should not notice much
difference, though, because we've been careful to name our own definitions and
theorems the same as their counterparts in the standard library, wherever they
overlap.

```coq
Require Import Idris.Arith.Arith.
Require Import Idris.Bool.Bool.
Require Import Idris.Strings.String.
Require Import Idris.Logic.FunctionalExtensionality.
```

Documentation for the standard library can be found at
\url{https://www.idris-lang.org/docs/current/}.

The \idr{:search} command is a good way to look for theorems involving objects
of specific types. Take a minute now to experiment with it.

== Identifiers

First, we need a type for the keys that we use to index into our maps. For this
purpose, we again use the type \idr{Id} from the `Lists` chapter. To make this
chapter self contained, we repeat its definition here, together with the
equality comparison function for \idr{Id} and its fundamental property.

> data Id : Type where
>   MkId : String -> Id
>
> beq_id : (x1, x2 : Id) -> Bool
> beq_id (MkId n1) (MkId n2) = decAsBool $ decEq n1 n2
>

\todo[inline]{Edit}

(The function \idr{decEq} comes from Idris's string library. If you check its
result type, you'll see that it does not actually return a \idr{Bool}, but
rather a type that looks like \idr{Either (x = y) (Not (x = y))}, called a
{Dec}, which can be thought of as an "evidence-carrying boolean." Formally, an
element of \idr{Dec (x=y)} is either a proof that two things are equal or a
proof that they are unequal, together with a tag indicating which. But for
present purposes you can think of it as just a fancy \idr{Bool}.)

> beq_id_refl : (x : Id) -> True = beq_id x x
> beq_id_refl (MkId n) with (decEq n n)
>   beq_id_refl _ | Yes _     = Refl
>   beq_id_refl _ | No contra = absurd $ contra Refl
>

The following useful property of  \idr{beq_id} follows from an analogous lemma
about strings:

> beq_id_true_iff : (beq_id x y = True) <-> x = y
> beq_id_true_iff = (bto, bfro)
>   where
>     bto : (beq_id x y = True) -> x = y
>     bto {x=MkId n1} {y=MkId n2} prf with (decEq n1 n2)
>       bto Refl | Yes eq = cong {f=MkId} eq
>       bto Refl | No _ impossible
>
>     idInj : MkId x = MkId y -> x = y
>     idInj Refl = Refl
>
>     bfro : (x = y) -> beq_id x y = True
>     bfro {x=MkId n1} {y=MkId n2} prf with (decEq n1 n2)
>       bfro _   | Yes _     = Refl
>       bfro prf | No contra = absurd $ contra $ idInj prf
>

Similarly:

> beq_id_false_iff : (beq_id x y = False) <-> Not (x = y)
> beq_id_false_iff = (to, fro)
>   where
>     to : (beq_id x y = False) -> Not (x = y)
>     to beqf = (snd not_true_iff_false) beqf . (snd beq_id_true_iff)
>
>     fro : (Not (x = y)) -> beq_id x y = False
>     fro noteq = (fst not_true_iff_false) $ noteq . (fst beq_id_true_iff)
>

== Total Maps

Our main job in this chapter will be to build a definition of partial maps that
is similar in behavior to the one we saw in the `Lists` chapter, plus
accompanying lemmas about its behavior.

This time around, though, we're going to use _functions_, rather than lists of
key-value pairs, to build maps. The advantage of this representation is that it
offers a more _extensional_ view of maps, where two maps that respond to queries
in the same way will be represented as literally the same thing (the very same
function), rather than just "equivalent" data structures. This, in turn,
simplifies proofs that use maps.

We build partial maps in two steps. First, we define a type of _total maps_ that
return a default value when we look up a key that is not present in the map.

> TotalMap : Type -> Type
> TotalMap a = Id -> a
>

Intuitively, a total map over an element type \idr{a} is just a function that
can be used to look up \idr{Id}s, yielding \idr{a}s.

The function \idr{t_empty} yields an empty total map, given a default element;
this map always returns the default element when applied to any id.

> t_empty : (v : a) -> TotalMap a
> t_empty v = \_ => v
>

We can also write this as:

```idris
t_empty = const
```

More interesting is the \idr{update} function, which (as before) takes a map
\idr{m}, a key \idr{x}, and a value \idr{v} and returns a new map that takes
\idr{x} to \idr{v} and takes every other key to whatever \idr{m} does.

> t_update : (x : Id) -> (v : a) -> (m : TotalMap a) -> TotalMap a
> t_update x v m = \x' => if beq_id x x' then v else m x'
>

This definition is a nice example of higher-order programming: \idr{t_update}
takes a _function_ \idr{m} and yields a new function \idr{\x' => ...} that
behaves like the desired map.

For example, we can build a map taking \idr{Id}s to \idr{Bool}s, where \idr{Id
3} is mapped to \idr{True} and every other key is mapped to \idr{False}, like
this:

\todo[inline]{Seems like a wrong description in the book here}

> examplemap : TotalMap Bool
> examplemap = t_update (MkId "foo") False $
>              t_update (MkId "bar") True $
>              t_empty False
>

This completes the definition of total maps. Note that we don't need to define a
\idr{find} operation because it is just function application!

> update_example1 : examplemap (MkId "baz") = False
> update_example1 = Refl
>
> update_example2 : examplemap (MkId "foo") = False
> update_example2 = Refl
>
> update_example3 : examplemap (MkId "quux") = False
> update_example3 = Refl
>
> update_example4 : examplemap (MkId "bar") = True
> update_example4 = Refl
>

To use maps in later chapters, we'll need several fundamental facts about how
they behave. Even if you don't work the following exercises, make sure you
thoroughly understand the statements of the lemmas! (Some of the proofs require
the functional extensionality axiom, which is discussed in the `Logic` chapter.)

==== Exercise: 1 star, optional (t_apply_empty)

First, the empty map returns its default element for all keys:

> t_apply_empty : t_empty v x = v
> t_apply_empty = ?t_apply_empty_rhs
>

$\square$

==== Exercise: 2 stars, optional (t_update_eq)

Next, if we update a map \idr{m} at a key \idr{x} with a new value \idr{v} and
then look up \idr{x} in the map resulting from the \idr{update}, we get back
\idr{v}:

> t_update_eq : (t_update x v m) x = v
> t_update_eq = ?t_update_eq_rhs
>

$\square$

==== Exercise: 2 stars, optional (t_update_neq)

On the other hand, if we update a map \idr{m} at a key \idr{x1} and then look up
a _different_ key \idr{x2} in the resulting map, we get the same result that
\idr{m} would have given:

> t_update_neq : Not (x1 = x2) -> (t_update x1 v m) x2 = m x2
> t_update_neq neq = ?t_update_neq_rhs
>

$\square$

==== Exercise: 2 stars, optional (t_update_shadow)

If we update a map \idr{m} at a key \idr{x} with a value \idr{v1} and then
update again with the same key \idr{x} and another value \idr{v2}, the resulting
map behaves the same (gives the same result when applied to any key) as the
simpler map obtained by performing just the second \idr{update} on \idr{m}:

> t_update_shadow : t_update x v2 $ t_update x v1 m = t_update x v2 m
> t_update_shadow = ?t_update_shadow_rhs
>

$\square$

For the final two lemmas about total maps, it's convenient to use the reflection
idioms introduced in chapter `IndProp`. We begin by proving a fundamental
_reflection lemma_ relating the equality proposition on \idr{Id}s with the
boolean function \idr{beq_id}.

==== Exercise: 2 stars, optional (beq_idP)

Use the proof of \idr{beq_natP} in chapter `IndProp` as a template to prove the
following:

> beq_idP : {x, y : Id} -> Reflect (x = y) (beq_id x y)
> beq_idP = ?beq_idP_rhs
>

$\square$

Now, given \idr{Id}s \idr{x1} and \idr{x2}, we can use \idr{with (beq_idP x1
x2)} to simultaneously perform case analysis on the result of \idr{beq_id x1 x2}
and generate hypotheses about the equality (in the sense of \idr{=}) of \idr{x1}
and \idr{x2}.

==== Exercise: 2 stars (t_update_same)

With the example in chapter `IndProp` as a template, use \idr{beq_idP} to prove
the following theorem, which states that if we update a map to assign key
\idr{x} the same value as it already has in \idr{m}, then the result is equal to
\idr{m}:

> t_update_same : t_update x (m x) m = m
> t_update_same = ?t_update_same_rhs
>

$\square$

==== Exercise: 3 stars, recommended (t_update_permute)

Use \idr{beq_idP} to prove one final property of the \idr{update} function: If
we update a map \idr{m} at two distinct keys, it doesn't matter in which order
we do the updates.

> t_update_permute : Not (x2 = x1) -> t_update x1 v1 $ t_update x2 v2 m
>                                   = t_update x2 v2 $ t_update x1 v1 m
> t_update_permute neq = ?t_update_permute_rhs
>

$\square$

== Partial maps

Finally, we define _partial maps_ on top of total maps. A partial map with
elements of type \idr{a} is simply a total map with elements of type \idr{Maybe
a} and default element \idr{Nothing}.

> PartialMap : Type -> Type
> PartialMap a = TotalMap (Maybe a)
>
> empty : PartialMap a
> empty = t_empty Nothing
>
> update : (x : Id) -> (v : a) -> (m : PartialMap a) -> PartialMap a
> update x v m = t_update x (Just v) m
>

We now straightforwardly lift all of the basic lemmas about total maps to
partial maps.

> apply_empty : empty {a} x = Nothing {a}
> apply_empty = Refl
>
> update_eq : (update x v m) x = Just v
> update_eq {v} = t_update_eq {v=Just v}
>
> update_neq : Not (x2 = x1) -> (update x2 v m) x1 = m x1
> update_neq {x1} {x2} {v} = t_update_neq {x1=x2} {x2=x1} {v=Just v}
>
> update_shadow : update x v2 $ update x v1 m = update x v2 m
> update_shadow {v1} {v2} = t_update_shadow {v1=Just v1} {v2=Just v2}
>
> update_same : m x = Just v -> update x v m = m
> update_same prf = rewrite sym prf in t_update_same
>
> update_permute : Not (x2 = x1) -> update x1 v1 $ update x2 v2 m
>                                 = update x2 v2 $ update x1 v1 m
> update_permute {v1} {v2} = t_update_permute {v1=Just v1} {v2=Just v2}

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Replica.Other.Free

%default total

public export
data Ap : (Type -> Type) -> Type -> Type where
  Pure : a -> Ap f a
  MkAp : f a -> Ap f (a -> b) -> Ap f b

export
Functor (Ap f) where
  map func (Pure x) = Pure (func x)
  map func (MkAp x y) = MkAp x (map (func .) y)

export
Applicative (Ap f) where
  pure = Pure
  (<*>) (Pure y) x = map y x
  (<*>) e@(MkAp y z) x = MkAp y $ assert_smaller e (map flip z) <*> x

export
runAp : Applicative g => (forall x. f x -> g x) -> Ap f c -> g c
runAp func (Pure x) = pure x
runAp func (MkAp x y) = runAp func y <*> func x

export
runApM : Monoid m => (forall x. f x -> m) -> Ap f c -> m
runApM func (Pure x) = neutral
runApM func (MkAp x y) = runApM func y <+> func x

export
liftAp : f a -> Ap f a
liftAp x = MkAp x (Pure id)

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module PlusComm

%access export
%default total

namespace Conat
  %access public export

  codata Conat : Type where
    Coz : Conat
    Cos : Conat -> Conat

  codata Bisimulation : Conat -> Conat -> Type where
    Biz : Bisimulation Coz Coz
    Bis : {a : Conat} -> {b : Conat} ->
          (Bisimulation a b) ->
          (Bisimulation (Cos a) (Cos b))

  MuGen : Conat
  MuGen = Cos MuGen

muGenSucc : Bisimulation (Cos MuGen) MuGen
muGenSucc = Bis muGenSucc

public export
Add : Conat -> Conat -> Conat
Add Coz     Coz     = Coz
Add (Cos a) Coz     = Cos a
Add Coz     (Cos b) = Cos b
Add (Cos a) (Cos b) = Cos $ Cos $ Add a b

biX : (x : Conat) -> Bisimulation x x
biX Coz     = Biz
biX (Cos x) = Bis $ biX x

total
plusCommutative : (a : Conat) -> (b : Conat) -> Bisimulation (Add a b) (Add b a)
plusCommutative Coz     Coz     = Biz
plusCommutative Coz     (Cos y) = biX $ Cos y
plusCommutative (Cos x) Coz     = biX $ Cos x
plusCommutative (Cos x) (Cos y) = Bis $ Bis $ plusCommutative x y

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
||| SipHash24 copied from C [reference implementation](https://github.com/veorq/SipHash/blob/master/siphash.c)
||| and rust https://doc.rust-lang.org/src/core/hash/sip.rs.html
module Data.Hashable.SipHashV2

import Data.Buffer

%default total

%inline
CROUNDS : Nat
CROUNDS = 2

%inline
DROUNDS : Nat
DROUNDS = 4

record HashState where
    constructor MkST
    v0 : Bits64
    v1 : Bits64
    v2 : Bits64
    v3 : Bits64

initHashState : HashState
initHashState = MkST
    { v0 = 0x736f6d6570736575
    , v1 = 0x646f72616e646f6d
    , v2 = 0x6c7967656e657261
    , v3 = 0x7465646279746573
    }

record PartialHash where
    constructor MkPartial
    tail : Bits64
    index : Bits64
    length : Bits64
    hst : HashState

initPartial : PartialHash
initPartial = MkPartial 0 0 0 initHashState

%inline
shl : Bits64 -> Bits64 -> Bits64
shl = prim__shl_Bits64

%inline
shr : Bits64 -> Bits64 -> Bits64
shr = prim__shr_Bits64

%inline
bor : Bits64 -> Bits64 -> Bits64
bor = prim__or_Bits64

%inline
xor : Bits64 -> Bits64 -> Bits64
xor = prim__xor_Bits64

%inline
and : Bits64 -> Bits64 -> Bits64
and = prim__and_Bits64

%inline
shr16 : Bits16 -> Bits16 -> Bits16
shr16 = prim__shr_Bits16

%inline
shr32 : Bits32 -> Bits32 -> Bits32
shr32 = prim__shr_Bits32

%inline
andInt : Int -> Int -> Int
andInt = prim__and_Int

%inline
%spec b
rotl : Bits64 -> (b : Bits64) -> Bits64
rotl x b = (x `shl` b) `bor` (x `shr` (64 - b))

-- Make the length the smallest multiple of 8 tail >= the given number
%inline
fullSize : Int -> Int
fullSize x =
    let left = x `andInt` 7
     in if (x `andInt` 7) == 0
        then x
        else x - left + 8

compress : HashState -> HashState
compress (MkST v0 v1 v2 v3) =
    let v0 = v0 + v1;
        v1 = v1 `rotl` 13;
        v1 = v1 `xor` v0;
        v0 = v0 `rotl` 32;
        v2 = v2 + v3;
        v3 = v3 `rotl` 16;
        v3 = v3 `xor` v2;
        v0 = v0 + v3;
        v3 = v3 `rotl` 21;
        v3 = v3 `xor` v0;
        v2 = v2 + v1;
        v1 = v1 `rotl` 17;
        v1 = v1 `xor` v2;
        v2 = v2 `rotl` 32;
    in MkST v0 v1 v2 v3

%inline
%spec rounds, f
repeat : (rounds : Nat) -> (f : a -> a) -> a -> a
repeat Z f x = x
repeat (S k) f x = repeat k f (f x)

%inline
hashBits64 : HashState -> Bits64 -> HashState
hashBits64 (MkST v0 v1 v2 v3) m =
    let v3 = v3 `xor` m
        MkST v0 v1 v2 v3 = repeat CROUNDS compress $ MkST v0 v1 v2 v3
        v0 = v0 `xor` m
     in MkST v0 v1 v2 v3

export
finish : PartialHash -> Bits64
finish (MkPartial tail index length hst) =
    let MkST v0 v1 v2 v3 = hst
        rest = ((length `and` 0xff) `shl` 56) `bor` tail
        v3 = v3 `xor` rest
        MkST v0 v1 v2 v3 = repeat CROUNDS compress $ MkST v0 v1 v2 v3
        v0 = v0 `xor` rest
        v2 = v2 `xor` 0xff
        MkST v0 v1 v2 v3 = repeat DROUNDS compress $ MkST v0 v1 v2 v3
     in (v0 `xor` v1) `xor` (v2 `xor` v3)

export
addBits8 : PartialHash -> Bits8 -> PartialHash
addBits8 (MkPartial tail index len hs) x = case index of
    -- finished a set of tail
    56 => MkPartial 0 0 (len + 1) $ hashBits64 hs (tail `bor` (cast x `shl` 56))
    -- add byte to partial
    _ => MkPartial (tail `bor` (cast x `shl` index)) (index + 8) (len + 1) hs

export
addBits16 : PartialHash -> Bits16 -> PartialHash
addBits16 ph x = addBits8 (addBits8 ph $ cast x) (cast $ x `shr16` 8)

export
addBits32 : PartialHash -> Bits32 -> PartialHash
addBits32 ph x = addBits16 (addBits16 ph $ cast x) (cast $ x `shr32` 16)

export
addBits64 : PartialHash -> Bits64 -> PartialHash
addBits64 (MkPartial tail index length hst) x = MkPartial tail index (length + 8) $ hashBits64 hst x

hashBuffer' : PartialHash -> Buffer -> Int -> Int -> IO PartialHash
hashBuffer' ph buf len idx = if idx >= len
    then pure ph
    else do
        word <- getBits64 buf idx
        let ph = addBits64 ph word
        hashBuffer' ph buf len (assert_smaller idx $ idx + 8)

hashBuffer : PartialHash -> Buffer -> IO PartialHash
hashBuffer ph buf = do
    rawLen <- rawSize buf
    let len = fullSize rawLen
    Just buf' <- resizeBuffer buf len
        | Nothing => hashBuffer' ph buf (rawLen `andInt` (- 7)) 0
    hashBuffer' ph buf' len 0


text:
module Russell

-- Based on https://github.com/agda/agda/blob/master/test/Succeed/Russell.agda

data U : Type where
  Set : (I : Type) -> (I -> U) -> U

Regular : U -> Type
Regular (Set I f) = (i : I) -> (f i = Set I f) -> Void

R : U
R = Set (DPair U Regular) fst

notRegular : Regular R -> Void
notRegular reg = reg (R ** reg) Refl

transport : {A : Type} -> (C : A -> Type) -> {x : A} -> {y : A} -> x = y -> C x -> C y
transport _ Refl ca = ca

regular : Regular R
regular (x ** pf) eq = transport Regular eq pf (x ** pf) eq

absurd : Void
absurd = notRegular regular

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets