text:
module ArithCmdDo

%default total

data Input = Answer Int | QuitCmd

data Command : Type -> Type where
     PutStr : String -> Command ()
     GetLine : Command String
    -- Ex 11.3 # 2
     ReadFile : String -> Command (Either FileError String)
     WriteFile : (filePath : String) -> (content : String) -> Command (Either FileError ())

     Pure : ty -> Command ty
     Bind : Command a -> (a -> Command b) -> Command b

data ConsoleIO : Type -> Type where
     Quit : a -> ConsoleIO a
     Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

data ShellInp : Type where
     Cat : String -> ShellInp
     Copy : (source : String) -> (destination : String) -> ShellInp
     Invalid : ShellInp
     Exit : ShellInp

data Fuel = Empty | More (Lazy Fuel)

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (ReadFile fp) = readFile fp
runCommand (WriteFile fp c) = writeFile fp c
runCommand (Pure x) = pure x
runCommand (Bind x f) = do res <- runCommand x
                           runCommand (f res)

partial
forever : Fuel
forever = More forever

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Empty y = pure Nothing
run (More x) (Quit y) = pure $ Just y
run (More x) (Do z f) = do res <- runCommand z
                           run x $ f res

namespace CommandDo
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf $ ConsoleIO b) -> ConsoleIO b
  (>>=) = Do

readInput : (prompt : String) -> Command Input
readInput prompt = do PutStr prompt
                      answer <- GetLine
                      if toLower answer == "quit"
                         then Pure QuitCmd
                         else Pure $ Answer $ cast answer

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

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

  -- Ex 11.3 # 1
  quiz : Stream Int -> (score : Nat) -> (qNum : Nat) -> ConsoleIO Nat
  quiz (n1 :: n2 :: ns) score qNum = do PutStr ("Score thus far: " ++ show score ++ " / " ++ show qNum ++ "\n")
                                        inp <- readInput (show n1 ++ " * " ++ show n2 ++ "? ")
                                        case inp of
                                              (Answer x) => if x == (n1 * n2)
                                                              then correct ns score qNum
                                                              else wrong ns (n1 * n2) score qNum
                                              QuitCmd => Quit score

partial
startQuiz : IO (Maybe Nat)
startQuiz = run forever $ quiz [1..] 0 0

-- Ex 11.3 # 3
readShellInput : (prompt : String) -> Command ShellInp
readShellInput prompt = do PutStr prompt
                           answer <- GetLine
                           case words answer of
                                ["cat", fp] => Pure $ Cat fp
                                ["copy", orgin, dest] => Pure $ Copy orgin dest
                                ["exit"] => Pure $ Exit
                                _ => Pure $ Invalid

myShell : ConsoleIO String
myShell = do input <- readShellInput "\nmyShell -TM-: "
             case input of
                  (Cat x) => do content <- ReadFile x
                                case content of
                                    (Left l) => do PutStr "File Read Error\n"
                                                   myShell
                                    (Right r) => PutStr r >>= \_ => myShell
                  (Copy source destination) => do content <- ReadFile source
                                                  case content of
                                                      (Left l) => PutStr "File Read Error\n" >>= \_ => myShell
                                                      (Right r) => WriteFile destination r >>= \_ => myShell
                  Invalid => PutStr "Please enter a valid command.\n" >>= \_ => myShell
                  Exit => Quit "Done"

partial
startShell : IO (Maybe String)
startShell = run forever myShell

max_stars_repo_path: Chapter 11/ArithCmdDo.idr

max_issues_repo_path: Chapter 11/ArithCmdDo.idr

max_forks_repo_path: Chapter 11/ArithCmdDo.idr


text:
module InterfaceWith0s

interface Lala (a : Type) where
  f : a -> a
  z : a -> a -> Bool
  0 prop : (x : a) -> z (f x) x = True

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
Toward $\pi$-calculus in idris
==============================

_WIP by [Dan Connolly][dckc], Apr 2018_

_This is a [literate idris][lp] document, with idris code ..._

> module picalc2
>
> %access export
> %default total

_... interspersed with text from ..._

* Milner, Robin. _[The polyadic π-calculus: a tutorial.][RM93]_
  In Logic and algebra of specification, pp. 203-246.
  Springer, Berlin, Heidelberg, 1993.

_We're having some fun with [KaTeX][] while we're at it._

[dckc]: http://www.madmode.com/contact/
[RM93]: https://pdfs.semanticscholar.org/5d25/0a3a14f68abb1ae0111d35b8220b4472b277.pdf
[lp]: http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#literate-programming
[KaTeX]: https://khan.github.io/KaTeX/

2.1 Basic ideas
---------------

The most primitive entity in $\pi$-calculus is a _name_. Names,
infinitely many, are $x, y, ... \in \mathcal{X}$; they have no
structure. In the basic version of $\pi$-calculus which we begin
with, there is only one other kind of entity; a _process_.
Processes are $P, Q, ... \in \mathcal{P}$ and are built from names
by this syntax

  $$P ::= \Sigma_{i\in I}\pi_i.P_i \;|\; P|Q \;|\; !P \;|\; (\nu x)P$$

> {- `mutual` lets us forward reference Action from Process.-}
>
> syntax [p] "|" [q] = Par p q;
> syntax "!" [p] = (Replicated p);
>
> mutual
>   ||| Processes are built from names, so `Process` is a
>   ||| type constructor from names.
>   data Process : {name: Type} -> Type where

The summation form represents a process able to take part in one --
but only one -- of several alternatives for communication.

>     Sum: (List (Action {name}, Process {name})) -> Process {name}

$P | Q$ -- "$P$ par $Q$" -- simply means that $P$ and $Q$ are
concurrently active.

>     Par: (P: Process {name}) -> (Q: Process {name}) -> Process {name}

$!P$ -- "bang $P$" means $P|P|...$ as many copies as you wish.

>     Replicated: (P: Process {name}) -> Process {name}

$(\nu x)P$ -- "new $x$ in $P$" -- restricts the use of the name $x$ to $P$.

>     New: (x: name) -> (P: Process {name}) -> Process {name}

In a summand $\pi.P$ the prefix $\pi$ represents an _atomic action_,
the first action performed by $\pi.P$.

>   data Action : {name: Type} -> Type where

There are two basic forms of prefix:

 - $x(y)$, which binds $y$ in the prefix process, means
   "input some name -- call it $y$ -- along the link named $x$"

>     Input: (x: name) -> (y: name) -> Action {name}

 - $\bar{x}y$ , which does not bind $y$, means "output the name $y$
   along the link named $x$".

>     Output: (x: name) -> (y: name) -> Action {name}
>

In the case $I = \emptyset$, we write the sum as $0$.

> zero: Process
> zero = Sum []

We call $x$ the _subject_ ...

> subject: Action {name} -> name
> subject (Input x y) = x
> subject (Output x y) = x

We call ... $y$ the _object_

> object: Action {name} -> name
> object (Input x y) = y
> object (Output x y) = y

2.2 Some simple examples
------------------------

_typo?_

Note that $R$ has become $\bar{y}v$ or $\bar{z}v$; ...

_should be:_

Note that $Q$ has become $\bar{y}v$ or $\bar{z}v$; ...

_no?_

2.3 Structural Congruence
-------------------------

_Note: In order to convince idris of the [totality][] of `fn` and
`bn`, we use `assert_smaller` to help it understand that `(Sum rest)`
is structurally smaller than `(Sum ((pi, P) :: rest))`._

[totality]: http://docs.idris-lang.org/en/latest/reference/misc.html?highlight=assert_smaller#totality-checking-assertions

> mutual
>   ||| free names of a process
>   fn: Eq name => (Process {name}) -> (List name)
>   fn (Sum []) = []
>   fn (Sum ((pi, P) :: rest)) = union (fna pi) (union (fn P)
>    (fn (assert_smaller (Sum ((pi, P) :: rest)) (Sum rest))) )
>   fn (P | Q) = union (fn P) (fn Q)
>   fn (Replicated P) = fn P
>   fn (New x P) = delete x (fn P)
>
>   ||| free names of an action
>   fna: (Action {name}) -> (List name)
>   fna (Input x y) = [x]
>   fna (Output x y) = [x, y]
>
> mutual
>   ||| _names_ of a process
>   n: Eq name => Process {name} -> (List name)
>   n (Sum []) = []
>   n (Sum ((pi, P) :: rest)) = union (n' pi) (union (n P)
>          (n (assert_smaller (Sum ((pi, P) :: rest)) (Sum rest))) )
>     where
>     n': (Action {name}) -> (List name)
>     n' (Input x y) = [x, y]
>     n' (Output x y) = [x, y]
>   n (P | Q) = union (n P) (n Q)
>   n (Replicated P) = n P
>   n (New x P) = union [x] (n P)
>
>   ||| bound names of a process
>   bn: Eq name => (Process {name}) -> (List name)
>   bn P = (n P) \\ (fn P)

_Yay... idris can now compute:_

```
λΠ> bn (Sum [((Output "x" "y"), zero)])
[] : List String
λΠ> fn (Sum [((Output "x" "y"), zero)])
["x", "y"] : List String
```

_next step(s): use techniques from
[rhocaml](https://github.com/leithaus/rhocaml) to define
structural equivalence and then prove the laws._

<style type="text/css">
.sourceCode { background: azure }
</style>

ext: lidr

max_stars_repo_name: jimscarver/togl

max_issues_repo_name: jimscarver/togl

max_forks_repo_name: jimscarver/togl


text:
||| This module is about *aliases* for pins that belong to some hardware protocol (bus)
module Arduino.Protocols

import Arduino.Boards

import Data.Vect
import Data.Vect.Quantifiers

%default total
%access public export

-----------------
--- Protocols ---
-----------------

-- TODO to think whether can pins used in different protocols intersect with each other?
-- TODO to think why digital, PWM, DAC and ADC are not just yet another protocols?

record HardwareProtocol where
  constructor MkProtocol
  protocolName : String
  protocolPinsCount : Nat

interface HasDigitalPins board => HasProtocol (0 prot : HardwareProtocol) (0 board : Board) where
  ProtocolPinGroupsCount : Nat

  ProtocolPins : Fin ProtocolPinGroupsCount -> Vect (protocolPinsCount prot) Pin

  AllProtocolPins : Vect (ProtocolPinGroupsCount * protocolPinsCount prot) Pin
  AllProtocolPins = ?flattenSomehow -- map ProtocolPins (allFinsTo ProtocolPinGroupsCount)
    where
      allFinsTo : (n : Nat) -> Vect n (Fin n)
      allFinsTo Z     = []
      allFinsTo (S n) = last :: map weaken (allFinsTo n)

  AllProtocolPinsDigital : All (CanBeDigital {board}) AllProtocolPins
  AllProtocolPinsDifferent : AllDiffer AllProtocolPins

--- UART ---

UART : HardwareProtocol
UART = MkProtocol "UART" 2

TX : HasProtocol UART board => Fin (ProtocolPinGroupsCount {prot=UART} {board}) -> Pin
RX : HasProtocol UART board => Fin (ProtocolPinGroupsCount {prot=UART} {board}) -> Pin

TX {board} = Data.Vect.index 0 . ProtocolPins {prot=UART} {board}
RX {board} = Data.Vect.index 1 . ProtocolPins {prot=UART} {board}

--- I2C ---

I2C : HardwareProtocol
I2C = MkProtocol "I2C" 2

SDA : HasProtocol I2C board => Fin (ProtocolPinGroupsCount {prot=I2C} {board}) -> Pin
SCL : HasProtocol I2C board => Fin (ProtocolPinGroupsCount {prot=I2C} {board}) -> Pin

SDA {board} = Data.Vect.index 0 . ProtocolPins {prot=I2C} {board}
SCL {board} = Data.Vect.index 1 . ProtocolPins {prot=I2C} {board}

--- SPI ---

SPI : HardwareProtocol
SPI = MkProtocol "SPI" 4

MISO : HasProtocol SPI board => Fin (ProtocolPinGroupsCount {prot=SPI} {board}) -> Pin
MOSI : HasProtocol SPI board => Fin (ProtocolPinGroupsCount {prot=SPI} {board}) -> Pin
SCK  : HasProtocol SPI board => Fin (ProtocolPinGroupsCount {prot=SPI} {board}) -> Pin
SS   : HasProtocol SPI board => Fin (ProtocolPinGroupsCount {prot=SPI} {board}) -> Pin

MISO {board} = Data.Vect.index 0 . ProtocolPins {prot=SPI} {board}
MOSI {board} = Data.Vect.index 1 . ProtocolPins {prot=SPI} {board}
SCK  {board} = Data.Vect.index 2 . ProtocolPins {prot=SPI} {board}
SS   {board} = Data.Vect.index 3 . ProtocolPins {prot=SPI} {board}

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Data.Maybe

public export
isNothing : Maybe a -> Bool
isNothing Nothing  = True
isNothing (Just _) = False

public export
isJust : Maybe a -> Bool
isJust Nothing  = False
isJust (Just _) = True

||| Proof that some `Maybe` is actually `Just`
public export
data IsJust : Maybe a -> Type where
  ItIsJust : IsJust (Just x)

export
Uninhabited (IsJust Nothing) where
  uninhabited ItIsJust impossible

||| Decide whether a 'Maybe' is 'Just'
public export
isItJust : (v : Maybe a) -> Dec (IsJust v)
isItJust (Just _) = Yes ItIsJust
isItJust Nothing = No absurd

||| Convert a `Maybe a` value to an `a` value by providing a default `a` value
||| in the case that the `Maybe` value is `Nothing`.
public export
fromMaybe : (Lazy a) -> Maybe a -> a
fromMaybe def Nothing  = def
fromMaybe _   (Just j) = j

||| Returns the `a` value of a `Maybe a` which is proved `Just`.
public export
fromJust : (v : Maybe a) -> IsJust v => a
fromJust (Just x) = x
fromJust Nothing impossible

||| Returns `Just` the given value if the conditional is `True`
||| and `Nothing` if the conditional is `False`.
public export
toMaybe : Bool -> Lazy a -> Maybe a
toMaybe True  j = Just j
toMaybe False _ = Nothing

export
justInjective : Just x = Just y -> x = y
justInjective Refl = Refl

||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case
||| that the `Maybe` value is `Nothing`.
public export
lowerMaybe : Monoid a => Maybe a -> a
lowerMaybe Nothing = neutral
lowerMaybe (Just x) = x

||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
export
raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
raiseToMaybe x = if x == neutral then Nothing else Just x


text:
module Reverse

import Data.Strings
import System.REPL

main : IO ()
main = repl "Enter a string: " reverse

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:
module Compiler.ES.Node

import Compiler.ES.ES

import Compiler.Common
import Compiler.CompileExpr

import Core.Context
import Core.TT
import Utils.Path

import System
import System.File

import Data.Maybe

findNode : IO String
findNode =
  do env <- getEnv "NODE"
     pure $ fromMaybe "/usr/bin/env node" env

||| Compile a TT expression to Node
compileToNode : Ref Ctxt Defs ->
              ClosedTerm -> Core String
compileToNode c tm = do
  compileToES c tm ["node", "javascript"]

||| Node implementation of the `compileExpr` interface.
compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile
    = do es <- compileToNode c tm
         let out = outputDir </> outfile
         Right () <- coreLift (writeFile out es)
            | Left err => throw (FileErr out err)
         pure (Just out)

||| Node implementation of the `executeExpr` interface.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
= do let outn = tmpDir </> "_tmp_node" ++ ".js"
     js <- compileToNode c tm
     Right () <- coreLift $ writeFile outn js
        | Left err => throw (FileErr outn err)
     node <- coreLift findNode
     coreLift $ system (node ++ " " ++ outn)
     pure ()

compileLibrary : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> (libName : String) -> (changedModules : Maybe (List ModuleIdent)) -> Core (Maybe (String, List String))
compileLibrary c tmpDir outputDir libName changedModules = do
  coreLift $ putStrLn "Compiling to library is not supported."
  pure Nothing

||| Codegen wrapper for Node implementation.
export
codegenNode : Codegen
codegenNode = MkCG compileExpr executeExpr compileLibrary


text:
module Crypto.Curve

import Crypto.Random
import Data.Bits
import Utils.Misc

public export
interface Point p where
  to_affine : p -> (Integer, Integer)
  generator : p
  infinity : p
  bits : Nat
  modulus : Integer
  order : Integer

  point_add : p -> p -> p
  mul : Integer -> p -> p

  encode : p -> List Bits8
  decode : List Bits8 -> Maybe p

Point p => Eq p where
  (==) a b = (to_affine a) == (to_affine b)

public export
data ECDSASignature : (p : Type) -> Type where
  MkSignature : (Point p) => p -> (Integer, Integer) -> ECDSASignature p

public export
ecdsa_sign : (Point p, MonadRandom m) => (sk : Integer) -> (msg : Integer) -> m (ECDSASignature p)
ecdsa_sign {p} private_key message = do
  k <- uniform_random' 1 (order {p} - 1)
  let public_key = mul private_key generator {p}
  let (x, y) = to_affine $ mul k generator {p}
  let r = x `mod` (order {p})
  let s = mul_mod (inv_mul_mod k $ order {p}) (message + (r * private_key)) (order {p})
  if (r == 0) || (s == 0)
     then ecdsa_sign {p} private_key message
     else pure $ MkSignature public_key (r, s)

within_interval : Point p => Integer -> Bool
within_interval n = n > 0 && n < (order {p})

public export
ecdsa_verify : Integer -> ECDSASignature p -> Bool
ecdsa_verify message (MkSignature public_key (r, s)) =
  let n = order {p}
      s_inv = inv_mul_mod s n
      u1 = mul_mod message s_inv n
      u2 = mul_mod r s_inv n
      pt = point_add (mul u1 generator) (mul u2 public_key)
      (x, _) = to_affine pt
  in within_interval {p} r && within_interval {p} s && (infinity /= pt) && (r `mod'` n) == (x `mod'` n)


text:
import Data.Vect

fourInts: Vect 4 Int
fourInts = [1, 2, 2, 4]

sixInts: Vect 6 Int
sixInts = [1, 2, 3, 4, 5, 7]

tenInts: Vect 10 Int
tenInts = fourInts ++ sixInts


text:
data Command : Type -> Type where
    PutStr : String -> Command ()
    GetLine : Command String
    ReadFile : String -> Command (Either FileError String)
    WriteFile : String -> String -> Command (Either FileError ())

    Pure : ty -> Command ty
    Bind : Command a -> (a -> Command b) -> Command b

namespace CommandDo
    (>>=) : Command a -> (a -> Command b) -> Command b
    (>>=) = Bind

total
runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (ReadFile fileName) = readFile fileName
runCommand (WriteFile fileName contents) = writeFile fileName contents
runCommand (Pure val) = pure val
runCommand (Bind c f) = do res <- runCommand c
                           runCommand (f res)

data ConsoleIO : Type -> Type where
    Quit : a -> ConsoleIO a
    Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace ConsoleDo
    (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
    (>>=) = Do

data ShellCommand : Type -> Type where
    Cat : Command String -> ShellCommand (Command String)
    Copy : String -> String -> Command () -> ShellCommand (Command ())
    Exit : ShellCommand ()

--             ("copy" :: source :: dest :: []) =>
--                 do
--                     Right contents <- ReadFile source
--                     Right () <- WriteFile dest contents
--                     Pure ()
            -- ("exit" :: []) =>
            --     do

shell : ConsoleIO String
shell =
    do
        PutStr "$ "
        command <- GetLine
        let command = words command
        case command of
            ("cat" :: filename :: []) =>
                do
                    Right contents <- ReadFile filename
                    PutStr contents
                    shell

            ("copy" :: src :: dst :: []) =>
                do
                    Right contents <- ReadFile src
                    Right () <- WriteFile dst contents
                    PutStr "Copying complete!"
                    shell

            ("exit" :: []) =>
                Quit "Bye-bye!"


text:
module Main

import Erlang

%cg erlang export exports

printHello : IO ErlAtom
printHello = do
  putStrLn "Hello"
  pure (MkAtom "ok")

exports : ErlExport
exports =
  Fun "foo" 42 <+>
    Fun "print_hello" (MkIOFun0 printHello)


text:
module FieldAxioms

import ZZ
import ZZUtils
import GCDZZ
import Divisors
import Rationals

%default total

-- The field axioms which require the custom equality EqRat type are verified here.

EqRatAddInvLeft: (x: ZZPair) -> (a: NotZero (snd x))
-> (EqRat (AddRationals x a (AddInverse x a) (xAndInverseNotZeroPlus x a)) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a))
EqRatAddInvLeft x a = eqMeansEqRat (AddRationals x a (AddInverse x a) (xAndInverseNotZeroPlus x a)) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a) (addInverseLeft x a)

EqRatAddInvRight: (x: ZZPair) -> (a: NotZero (snd x))
-> (EqRat (AddRationals (AddInverse x a) (xAndInverseNotZeroPlus x a) x a) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a))
EqRatAddInvRight x a = eqMeansEqRat (AddRationals (AddInverse x a) (xAndInverseNotZeroPlus x a) x a) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a) (addInverseRight x a)

EqRatMultInvLeft: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x))
-> (EqRat (MultiplyRationals x b (MultInverse x a b) (xAndInverseNotZeroMult x a b)) (productNonZero b (xAndInverseNotZeroMult x a b)) ((fst x)*(snd x), (fst x)*(snd x)) (productNonZero a b))
EqRatMultInvLeft x a b = eqMeansEqRat (MultiplyRationals x b (MultInverse x a b) (xAndInverseNotZeroMult x a b)) (productNonZero b (xAndInverseNotZeroMult x a b)) ((fst x)*(snd x), (fst x)*(snd x)) (productNonZero a b) (multInverseLeft x a b)

EqRatMultInvRight: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x))
-> (EqRat (MultiplyRationals (MultInverse x a b) (xAndInverseNotZeroMult x a b) x b) (productNonZero (xAndInverseNotZeroMult x a b) b) ((snd x)*(fst x), (snd x)*(fst x)) (productNonZero b a))
EqRatMultInvRight x a b = eqMeansEqRat (MultiplyRationals (MultInverse x a b) (xAndInverseNotZeroMult x a b) x b) (productNonZero (xAndInverseNotZeroMult x a b) b) ((snd x)*(fst x), (snd x)*(fst x)) (productNonZero b a) (multInverseRight x a b)

-- All of the following proofs involve the use of EqRat and its associated properties which are
-- reflexvity, symmetry, transitivity, and the fact that two elements being equal is enough to construct
-- an element of EqRat.

|||Constructs an equality between (a,b) + (c,d) and (c,d) + (a,b)
plusCommQEqRat: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) ->
(EqRat (AddRationals x a y b) (productNonZero a b) (AddRationals y b x a) (productNonZero b a))
plusCommQEqRat x a y b = eqMeansEqRat (AddRationals x a y b) (productNonZero a b) (AddRationals y b x a) (productNonZero b a) (plusCommutativeQ x a y b)

|||Constructs an equality between (a,b)*(c,d) and (c,d)*(a,b)
multCommQEqRat: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) ->
(EqRat (MultiplyRationals x a y b) (productNonZero a b) (MultiplyRationals y b x a) (productNonZero b a))
multCommQEqRat x a y b = eqMeansEqRat (MultiplyRationals x a y b) (productNonZero a b) (MultiplyRationals y b x a) (productNonZero b a) (multCommutativeQ x a y b)

|||Constructs an equality between (a,b) + (0,1) and (a,b).
addIdRightEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (AddRationals x a (0,1) PositiveZ) (productNonZero a (PositiveZ)) x a)
addIdRightEqRat x a = eqMeansEqRat (AddRationals x a (0,1) PositiveZ) (productNonZero a (PositiveZ)) (x) (a) (zeroAddIdentityRight x a)

|||Constructs an equality between (a,b) and (a,b) + (0,1).
addIdLeftEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (AddRationals (0,1) PositiveZ x a) (productNonZero (PositiveZ) a) x a)
addIdLeftEqRat x a = eqMeansEqRat (AddRationals (0,1) PositiveZ x a) (productNonZero (PositiveZ) a) (x) (a) (zeroAddIdentityLeft x a)

|||Constructs an equality between (a,b)*(1,1) and (a,b).
multIdRightEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (MultiplyRationals x a (1,1) PositiveZ) (productNonZero a (PositiveZ)) x a)
multIdRightEqRat x a = eqMeansEqRat (MultiplyRationals x a (1,1) PositiveZ) (productNonZero a (PositiveZ)) (x) (a) (oneMultIdentityRight x a)

|||Constructs an equality between (a,b)*(1,1) and (a,b).
multIdLeftEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (MultiplyRationals (1,1) PositiveZ x a) (productNonZero (PositiveZ) a) x a)
multIdLeftEqRat x a = eqMeansEqRat (MultiplyRationals (1,1) PositiveZ x a) (productNonZero (PositiveZ) a) (x) (a) (oneMultIdentityLeft x a)

|||Constructs an equality between ((a,b)+(-a,b)) and 0.
addInverseLeftEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (AddRationals x a (AddInverse x a) (xAndInverseNotZeroPlus x a) ) (productNonZero a (xAndInverseNotZeroPlus x a)) (0,1) PositiveZ)
addInverseLeftEqRat x a = EqRatTrans (AddRationals x a (AddInverse x a) (xAndInverseNotZeroPlus x a)) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a) (0,1) (PositiveZ) (EqRatAddInvLeft x a) (reducedFormZeroRight ((snd x)*(snd x)) (productNonZero a a))

|||Constructs an equality between 0 and ((a,b)+(-a,b)).
addInverseRightEqRat: (x: ZZPair) -> (a: NotZero (snd x)) ->
(EqRat (AddRationals (AddInverse x a) (xAndInverseNotZeroPlus x a) x a) (productNonZero a (xAndInverseNotZeroPlus x a)) (0,1) PositiveZ)
addInverseRightEqRat x a = EqRatTrans (AddRationals (AddInverse x a) (xAndInverseNotZeroPlus x a) x a) (productNonZero a (xAndInverseNotZeroPlus x a)) ((Pos 0), (snd x)*(snd x)) (productNonZero a a) (0,1) (PositiveZ) (EqRatAddInvRight x a) (reducedFormZeroRight ((snd x)*(snd x)) (productNonZero a a))

|||Constructs an equality between (a,b)*(b,a) and (1,1).
multInverseLeftEqRat: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x)) ->
(EqRat (MultiplyRationals x b (MultInverse x a b) (xAndInverseNotZeroMult x a b)) (productNonZero b (xAndInverseNotZeroMult x a b)) (1,1) (PositiveZ))
multInverseLeftEqRat x a b = EqRatTrans (MultiplyRationals x b (MultInverse x a b) (xAndInverseNotZeroMult x a b)) (productNonZero b (xAndInverseNotZeroMult x a b)) ((fst x)*(snd x), (fst x)*(snd x)) (productNonZero a b) (1,1) (PositiveZ) (EqRatMultInvLeft x a b) (reducedFormOneRight ((fst x)*(snd x)) (productNonZero a b))

|||Constructs an equality between (1,1) and (a,b)*(b,a).
multInverseRightEqRat: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x)) ->
(EqRat (MultiplyRationals (MultInverse x a b) (xAndInverseNotZeroMult x a b) x b) (productNonZero (xAndInverseNotZeroMult x a b) b) (1,1) (PositiveZ))
multInverseRightEqRat x a b = EqRatTrans (MultiplyRationals (MultInverse x a b) (xAndInverseNotZeroMult x a b) x b) (productNonZero (xAndInverseNotZeroMult x a b) b) ((snd x)*(fst x), (snd x)*(fst x)) (productNonZero b a) (1,1) (PositiveZ) (EqRatMultInvRight x a b) (reducedFormOneRight ((snd x)*(fst x)) (productNonZero b a))

|||Constructs an EqRat element of associativity for addition.
plusAssocQEqRat: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (z: ZZPair) -> (c: NotZero (snd z)) ->
(EqRat (AddRationals (AddRationals x a y b) (productNonZero a b) z c) (productNonZero (productNonZero a b) c) (AddRationals x a (AddRationals y b z c) (productNonZero b c)) (productNonZero a (productNonZero b c)))
plusAssocQEqRat x a y b z c = eqMeansEqRat (AddRationals (AddRationals x a y b) (productNonZero a b) z c) (productNonZero (productNonZero a b) c) (AddRationals x a (AddRationals y b z c) (productNonZero b c)) (productNonZero a (productNonZero b c)) (plusAssociativeQ x a y b z c)

|||Constructs an EqRat element of associativity for multiplication.
multAssocQEqRat: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (z: ZZPair) -> (c: NotZero (snd z)) ->
(EqRat (MultiplyRationals (MultiplyRationals x a y b) (productNonZero a b) z c) (productNonZero (productNonZero a b) c) (MultiplyRationals x a (MultiplyRationals y b z c) (productNonZero b c)) (productNonZero a (productNonZero b c)))
multAssocQEqRat x a y b z c = eqMeansEqRat (MultiplyRationals (MultiplyRationals x a y b) (productNonZero a b) z c) (productNonZero (productNonZero a b) c) (MultiplyRationals x a (MultiplyRationals y b z c) (productNonZero b c)) (productNonZero a (productNonZero b c)) (multAssociativeQ x a y b z c)


text:
-- test that a sent thing arrives and is the thing that was sent

import System
import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          let val = 3
          (MkDPair bc send) <- becomeSender bcRef
          (MkDPair bc' recv) <- becomeReceiver Blocking bcRef

          send Signal bc val
          val' <- recv bc'
          if val /= val'
             then putStrLn "ERROR: Value changed in transit."
             else putStrLn "Success!"


text:
module Main

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

identity : ty -> ty
identity x = x

the2 : (ty : Type) -> ty -> ty
the2 ty x = x

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

-- Shape : Type
-- rotate : Shape -> Shape

longer : String -> String -> Nat
longer w1 w2
  = let l1 = length w1
        l2 = length w2
    in if l1 > l2 then l1 else l2

||| Calculates the value of the pythagoras equasion.
||| @x a value for the first side of a triangle
||| @y a value for the second side of a triangle
pythagoras : (x : Double) -> (y : Double) -> Double
pythagoras x y = sqrt (square x + square y)
  where
    square : Double -> Double
    square x = x * x

main : IO ()
main = do
  putStrLn $ cast $ twice double $ the2 Int $ identity 3
  putStrLn $ cast $ longer "Hello" "World!"
  putStrLn $ cast $ pythagoras 1 3

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

strToInput : String -> Maybe Input
strToInput "insert" = Just COIN
strToInput "vend" = Just VEND
strToInput "change" = Just CHANGE
strToInput x = if all isDigit (unpack x)
                  then Just (REFILL (cast x))
                  else Nothing

data CoinResult = Inserted | Rejected

data MachineCmd : (ty : Type) -> VendState -> (ty -> VendState) -> Type where
-- data MachineCmd : Type -> VendState -> VendState -> Type where
     InsertCoin : MachineCmd CoinResult (pounds, chocs)
                       (\res => case res of
                                     Inserted => (S pounds, chocs)
                                     Rejected => (pounds, chocs))

     Vend       : MachineCmd () (S pounds, S chocs) (const (pounds, chocs))
     GetCoins   : MachineCmd () (pounds, chocs)     (const (Z, chocs))

     Display : String ->
                  MachineCmd () state               (const state)
     Refill : (bars : Nat) ->
                  MachineCmd () (Z, chocs)          (const (Z, bars + chocs))

     GetInput : MachineCmd (Maybe Input) state (const state)

     Pure : (x:ty) -> MachineCmd ty (state_fn x) state_fn
     (>>=) : MachineCmd a state1 state2_fn
             -> ((x : a) -> MachineCmd b (state2_fn x) state3_fn)
             -> MachineCmd b state1 state3_fn

data MachineIO : VendState -> Type where
  Do : MachineCmd a state1 state2
       -> ((x : a) -> Inf (MachineIO (state2 x)))
       -> MachineIO state1

runMachine : MachineCmd ty inState outState -> IO ty
runMachine InsertCoin =
  do putStrLn "Coin inserted"
     pure Inserted
runMachine Vend = putStrLn "Please take your chocolate"
runMachine {inState = (pounds, _)} GetCoins
     = putStrLn (show pounds ++ " coins returned")
runMachine (Display str) = putStrLn str
runMachine (Refill bars)
     = putStrLn ("Chocolate remaining: " ++ show bars)
runMachine {inState = (pounds, chocs)} GetInput
     = do putStrLn ("Coins: " ++ show pounds ++ "; " ++
                    "Stock: " ++ show chocs)
          putStr "> "
          x <- getLine
          pure (strToInput x)
runMachine (Pure x) = pure x
runMachine (cmd >>= prog) = do x <- runMachine cmd
                               runMachine (prog x)

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> MachineIO state -> IO ()
run (More fuel) (Do c f)
     = do res <- runMachine c
          run fuel (f res)
run Dry p = pure ()

namespace MachineDo
  (>>=) : MachineCmd a state1 state2 ->
          (a -> Inf (MachineIO state2)) -> MachineIO state1
  (>>=) = Do

mutual
  vend : MachineIO (pounds, chocs)
  vend {pounds = S p} {chocs = S c} = do Vend
                                         Display "Enjoy!"
                                         machineLoop
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _ = do Display "Can't refill: Coins in machine"
                machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
       do Just x <- GetInput | Nothing => do Display "Invalid input"
                                             machineLoop
          case x of
              COIN => do InsertCoin
                         machineLoop
              VEND => vend
              CHANGE => do GetCoins
                           Display "Change returned"
                           machineLoop
              REFILL num => refill num

main : IO ()
main = run forever (machineLoop {pounds = 0} {chocs = 1})

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
-- vim: ft=idris sw= ts=2 et

import Data.So

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

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

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

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

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

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Task.Equality

import Task.Internal
import Task.Semantics

import Helpers

%default total
%access export

-- Equivallence ----------------------------------------------------------------

equivallent : MonadRef l m => TaskT m a -> TaskT m a -> m Bool
equivallent {a} t1 t2 = do
  t1' <- normalise t1
  t2' <- normalise t2
  v1 <- value t1'
  v2 <- value t2'
  let _ = eq a --NOTE: Brings `Eq` in scope for universe type `a`
  pure $ v1 == v2

-- Similarity ------------------------------------------------------------------

similar : MonadTrace NotApplicable m => MonadRef l m => TaskT m a -> TaskT m a -> m Bool
similar {a} t1 t2 = do
  t1' <- normalise t1
  t2' <- normalise t2
  v1 <- value t1'
  v2 <- value t2'
  let _ = eq a --NOTE: Brings `Eq` in scope for universe type `a`
  if v1 == v2 then do
    ok12 <- sim t1 t2
    ok21 <- sim t2 t1
    pure $ ok12 && ok21
  else
    pure False
where
    sim : MonadTrace NotApplicable m => MonadRef l m => TaskT m a -> TaskT m a -> m Bool
    sim t1 t2 = do
      is1 <- inputs t1
      is2 <- inputs t2
      pairs <- sequence [ bisequence ( handle t1 i1, handle t2 i2 ) | i1 <- is1, i2 <- is2, i2 =~ i1 ]
      results <- sequence $ map (uncurry similar) pairs
      pure $ and results

-- Conform ---------------------------------------------------------------------

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module Network.TLS.Record

import Utils.Bytes
import Utils.Misc
import Utils.Show
import Data.Vect
import public Network.TLS.HelloExtension
import public Network.TLS.Handshake
import public Network.TLS.Magic
import public Network.TLS.Parsing
import public Network.TLS.Wrapper

public export
data Record : RecordType -> Type where
  ChangeCipherSpec : (body : List Bits8) -> Record ChangeCipherSpec
  Handshake : (handshakes : List (DPair _ Handshake)) -> Record Handshake
  ApplicationData : (body : List Bits8) -> Record ApplicationData
  Alert : (AlertLevel, AlertDescription) -> Record Alert

public export
Show (Record type) where
  show (ChangeCipherSpec body) = show_record "ChangeCipherSpec"
    [ ("body", xxd body)
    ]
  show (Handshake handshakes) = show_record "Handshake"
    [ ("handshakes", show (map (\x => show x.snd) handshakes))
    ]
  show (ApplicationData body) = show_record "ApplicationData"
    [ ("body", xxd body)
    ]
  show (Alert (lvl, desc)) = show_record "Alert"
    [ ("alert_level", show lvl)
    , ("alert", show desc)
    ]

XRecord : Type
XRecord = Eithers [Record ChangeCipherSpec, Record Handshake, Record ApplicationData, Record Alert]

hack_record : DPair _ Record -> XRecord
hack_record (ChangeCipherSpec ** x) = Left x
hack_record (Handshake ** x)        = Right (Left x)
hack_record (ApplicationData  ** x) = Right (Right (Left x))
hack_record (Alert ** x)            = Right (Right (Right x))

fix_record : XRecord -> DPair _ Record
fix_record (Left x)                  = (ChangeCipherSpec ** x)
fix_record (Right (Left x))          = (Handshake ** x)
fix_record (Right (Right (Left x)))  = (ApplicationData ** x)
fix_record (Right (Right (Right x))) = (Alert ** x)

XRecordWithVersion : Type
XRecordWithVersion = Eithers
  [ (TLSVersion, Record ChangeCipherSpec)
  , (TLSVersion, Record Handshake)
  , (TLSVersion, Record ApplicationData)
  , (TLSVersion, Record Alert)
  ]

hack_record_with_version : (TLSVersion, DPair _ Record) -> XRecordWithVersion
hack_record_with_version (v, (ChangeCipherSpec ** x)) = Left (v, x)
hack_record_with_version (v, (Handshake ** x))        = Right (Left (v, x))
hack_record_with_version (v, (ApplicationData  ** x)) = Right (Right (Left (v, x)))
hack_record_with_version (v, (Alert ** x))            = Right (Right (Right (v, x)))

fix_record_with_version : XRecordWithVersion -> (TLSVersion, DPair _ Record)
fix_record_with_version (Left (v, x))                  = (v, (ChangeCipherSpec ** x))
fix_record_with_version (Right (Left (v, x)))          = (v, (Handshake ** x))
fix_record_with_version (Right (Right (Left (v, x))))  = (v, (ApplicationData ** x))
fix_record_with_version (Right (Right (Right (v, x)))) = (v, (Alert ** x))

namespace Parsing
  export
  no_id_change_cipher_spec : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record ChangeCipherSpec)
  no_id_change_cipher_spec = map (\a => ChangeCipherSpec a) (\(ChangeCipherSpec a) => a)
    $ lengthed_list 2 token

  export
  no_id_handshake : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Handshake)
  no_id_handshake = map (\a => Handshake a) (\(Handshake a) => a)
    $ lengthed_list 2 handshake

  export
  no_id_handshake2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Handshake)
  no_id_handshake2 = map (\a => Handshake a) (\(Handshake a) => a)
    $ lengthed_list 2 handshake2

  export
  no_id_application_data : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record ApplicationData)
  no_id_application_data = map (\a => ApplicationData a) (\(ApplicationData a) => a)
    $ lengthed_list 2 token

  export
  record_type_with_version : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion)
  record_type_with_version = record_type <*>> tls_version

  export
  record_type_with_version_with_length : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion, Nat)
  record_type_with_version_with_length = record_type <*>> tls_version <*>> nat 2

  export
  alert : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (AlertLevel, AlertDescription)
  alert = under "alert protocol" $ alert_level <*>> alert_description

  export
  no_id_alert : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Record Alert)
  no_id_alert = map (\((), a) => Alert a) (\(Alert a) => ((), a)) $ is [0x00, 0x02] <*>> alert

  export
  with_id_with_version : (Cons (Posed Bits8) i, Monoid i) => {type : RecordType} -> Parserializer Bits8 i (SimpleError String) (Record type) -> Parserializer Bits8 i (SimpleError String) (TLSVersion, Record type)
  with_id_with_version pser = under (show type <+> " record") $ is (to_vect $ record_type_to_id type) *> (tls_version <*>> pser)

  export
  arecord : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (TLSVersion, DPair _ Record)
  arecord =
    map fix_record_with_version hack_record_with_version
    $ (with_id_with_version no_id_change_cipher_spec)
    <|> (with_id_with_version no_id_handshake)
    <|> (with_id_with_version no_id_application_data)
    <|> (with_id_with_version no_id_alert)

  export
  arecord2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (TLSVersion, DPair _ Record)
  arecord2 =
    map fix_record_with_version hack_record_with_version
    $ (with_id_with_version no_id_change_cipher_spec)
    <|> (with_id_with_version no_id_handshake2)
    <|> (with_id_with_version no_id_application_data)
    <|> (with_id_with_version no_id_alert)

  export
  alert_or_arecord : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))
  alert_or_arecord = alert <|> arecord

  export
  alert_or_arecord2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))
  alert_or_arecord2 = alert <|> arecord2

  export
  wrapper2 : (Cons (Posed Bits8) i, Monoid i) => {iv_size : Nat} -> {mac_size : Nat} -> Parserializer Bits8 i (SimpleError String) (RecordType, TLSVersion, Wrapper2 iv_size mac_size)
  wrapper2 =
    record_type
    <*>> tls_version
    <*>> (mapEither (\x => maybe_to_either (from_application_data2 x) (msg "cannot parse wrapper")) to_application_data2 $ lengthed_list 2 token)


text:
||| A port of Edward Kmett's `machines` library to Idris.
module Machines

data Mealy : Type -> Type -> Type where
  MkMealy : (a -> (b, Mealy a b)) -> Mealy a b

max_stars_repo_name: taktoa/idris-regexp

max_issues_repo_name: taktoa/idris-regexp

max_forks_repo_name: taktoa/idris-regexp


text:
module Network.HTTP.Pool.Common

import System.Concurrency
import Network.HTTP.Scheduler

public export
data Event : Type -> Type where
  Request : ScheduleRequest e IO -> Event e
  Kill : Maybe Condition -> Event e


text:
%default total

data Foo : Type where
  Fee : Foo

x : Foo
x = Fee

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


text:
module Main

import CatR
import CatI

main : IO ()
main = putStrLn "Welcome to the Paris Idris Group!"


text:
module Main

import Control.Monad.State

increase : Nat -> State Nat ()
increase inc = do
  current <- get
  put (current + inc)

main : IO ()
main = do
  printLn $ runState (increase 5) 89
  printLn $ evalState (increase 5) 89
  printLn $ execState (increase 5) 89

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
||| Projection based on Full Merge.
|||
||| The Tech Report 'A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming' (DTRS12-2) defines a 'full merge' operation.
||| This merge operation improves the expressiveness of projection compared to Plain Merge.
|||
module Sessions.Projection.Full

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta

import Sessions.Global
import Sessions.Global.Involved

import Sessions.Local
import Sessions.Local.Same

import public Sessions.Projection.Error

%default total

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
= Lists : Working with Structured Data

> module Lists

> import Basics

> %hide Prelude.Basics.fst
> %hide Prelude.Basics.snd
> %hide Prelude.Nat.pred
> %hide Prelude.List.(++)

> %access public export
> %default total

== Pairs of Numbers

In an inductive type definition, each constructor can take any number of
arguments -- none (as with \idr{True} and \idr{Z}), one (as with \idr{S}), or
more than one, as here:

> data NatProd : Type where
>   Pair : Nat -> Nat -> NatProd

This declaration can be read: "There is just one way to construct a pair of
numbers: by applying the constructor \idr{Pair} to two arguments of type
\idr{Nat}."

```idris
λΠ> :t Pair 3 5
```

Here are two simple functions for extracting the first and second components of
a pair. The definitions also illustrate how to do pattern matching on
two-argument constructors.

> fst : (p : NatProd) -> Nat
> fst (Pair x y) = x

> snd : (p : NatProd) -> Nat
> snd (Pair x y) = y

```idris
λΠ> fst (Pair 3 5)
3 : Nat
```

Since pairs are used quite a bit, it is nice to be able to write them with the
standard mathematical notation \idr{(x,y)} instead of \idr{Pair x y}. We can
tell Idris to allow this with a \idr{syntax} declaration.

> syntax "(" [x] "," [y] ")" = Pair x y

The new pair notation can be used both in expressions and in pattern matches
(indeed, we've actually seen this already in the previous chapter, in the
definition of the \idr{minus} function -- this works because the pair notation
is also provided as part of the standard library):

```idris
λΠ> fst (3,5)
3 : Nat
```

> fst' : (p : NatProd) -> Nat
> fst' (x,y) = x

> snd' : (p : NatProd) -> Nat
> snd' (x,y) = y

> swap_pair : (p : NatProd) -> NatProd
> swap_pair (x,y) = (y,x)

Let's try to prove a few simple facts about pairs.

If we state things in a particular (and slightly peculiar) way, we can complete
proofs with just reflexivity (and its built-in simplification):

> surjective_pairing' : (n,m : Nat) -> (n,m) = (fst (n,m), snd (n,m))
> surjective_pairing' n m = Refl

But \idr{Refl} is not enough if we state the lemma in a more natural way:

```idris
surjective_pairing_stuck : (p : NatProd) -> p = (fst p, snd p)
surjective_pairing_stuck p = Refl
```
```
When checking right hand side of
  surjective_pairing_stuck with expected type p = Pair (fst p) (snd p)
...
Type mismatch between p and Pair (fst p) (snd p)
```

We have to expose the structure of \idr{p} so that Idris can perform the pattern
match in \idr{fst} and \idr{snd}. We can do this with \idr{case}.

> surjective_pairing : (p : NatProd) -> p = (fst p, snd p)
> surjective_pairing p = case p of (n,m) => Refl

Notice that \idr{case} matches just one pattern here. That's because
\idr{NatProd}s can only be constructed in one way.

=== Exercise: 1 star (snd_fst_is_swap)

> snd_fst_is_swap : (p : NatProd) -> (snd p, fst p) = swap_pair p
> snd_fst_is_swap p = ?snd_fst_is_swap_rhs

$\square$

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

> fst_swap_is_snd : (p : NatProd) -> fst (swap_pair p) = snd p
> fst_swap_is_snd p = ?fst_swap_is_snd_rhs

$\square$

== Lists of Numbers

Generalizing the definition of pairs, we can describe the type of _lists_ of
numbers like this: "A list is either the empty list or else a pair of a number
and another list."

> data NatList : Type where
>   Nil : NatList
>   (::) : Nat -> NatList -> NatList

For example, here is a three-element list:

> mylist : NatList
> mylist = (::) 1 ((::) 2 ((::) 3 Nil))

\todo[inline]{Edit the section - Idris's list sugar automatically works for
anything with constructors \idr{Nil} and \idr{(::)}}

As with pairs, it is more convenient to write lists in familiar programming
notation. The following declarations allow us to use \idr{::} as an infix Cons
operator and square brackets as an "outfix" notation for constructing lists.

It is not necessary to understand the details of these declarations, but in case
you are interested, here is roughly what's going on. The right associativity
annotation tells Coq how to parenthesize expressions involving several uses of
:: so that, for example, the next three declarations mean exactly the same
thing:

> mylist1 : NatList
> mylist1 = 1 :: (2 :: (3 :: Nil))

> mylist2 : NatList
> mylist2 = 1::2::3::[]

> mylist3 : NatList
> mylist3 = [1,2,3]

The at level 60 part tells Coq how to parenthesize expressions that involve both
:: and some other infix operator. For example, since we defined + as infix
notation for the plus function at level 50,

```coq
Notation "x + y" := ( plus x y )
( at level 50, left associativity ).
```

the `+` operator will bind tighter than `::` , so `1 + 2 :: [3]` will be parsed,
as we'd expect, as `(1 + 2) :: [3]` rather than `1 + (2 :: [3])`.

(Expressions like "`1 + 2 :: [3]`" can be a little confusing when you read them
in a `.v` file. The inner brackets, around `3`, indicate a list, but the outer
brackets, which are invisible in the HTML rendering, are there to instruct the
"coqdoc" tool that the bracketed part should be displayed as Coq code rather
than running text.)

The second and third `Notation` declarations above introduce the standard
square-bracket notation for lists; the right-hand side of the third one
illustrates Coq's syntax for declaring n-ary notations and translating them to
nested sequences of binary constructors.

=== Repeat

A number of functions are useful for manipulating lists. For example, the
\idr{repeat} function takes a number \idr{n} and a \idr{count} and returns a
list of length \idr{count} where every element is \idr{n}.

> repeat : (n, count : Nat) -> NatList
> repeat n Z = []
> repeat n (S k) = n :: repeat n k

=== Length

The \idr{length} function calculates the length of a list.

> length : (l : NatList) -> Nat
> length [] = Z
> length (h :: t) = S (length t)

=== Append

The \idr{app} function concatenates (appends) two lists.

> app : (l1, l2 : NatList) -> NatList
> app [] l2 = l2
> app (h :: t) l2 = h :: app t l2

Actually, \idr{app} will be used a lot in some parts of what follows, so it is
convenient to have an infix operator for it.

> infixr 7 ++

> (++) : (x, y : NatList) -> NatList
> (++) = app

> test_app1 : [1,2,3] ++ [4,5,6] = [1,2,3,4,5,6]
> test_app1 = Refl

> test_app2 : [] ++ [4,5] = [4,5]
> test_app2 = Refl

> test_app3 : [1,2,3] ++ [] = [1,2,3]
> test_app3 = Refl

=== Head (with default) and Tail

Here are two smaller examples of programming with lists. The \idr{hd} function
returns the first element (the "head") of the list, while \idr{tl} returns
everything but the first element (the "tail"). Of course, the empty list has no
first element, so we must pass a default value to be returned in that case.

> hd : (default : Nat) -> (l : NatList) -> Nat
> hd default [] = default
> hd default (h :: t) = h

> tl : (l : NatList) -> NatList
> tl [] = []
> tl (h :: t) = t

> test_hd1 : hd 0 [1,2,3] = 1
> test_hd1 = Refl

> test_hd2 : hd 0 [] = 0
> test_hd2 = Refl

> test_tl : tl [1,2,3] = [2,3]
> test_tl = Refl

=== Exercises

==== Exercise: 2 stars, recommended (list_funs)

Complete the definitions of \idr{nonzeros}, \idr{oddmembers} and
\idr{countoddmembers} below. Have a look at the tests to understand what these
functions should do.

> nonzeros : (l : NatList) -> NatList
> nonzeros l = ?nonzeros_rhs

> test_nonzeros : nonzeros [0,1,0,2,3,0,0] = [1,2,3]
> test_nonzeros = ?test_nonzeros_rhs

> oddmembers : (l : NatList) -> NatList
> oddmembers l = ?oddmembers_rhs

> test_oddmembers : oddmembers [0,1,0,2,3,0,0] = [1,3]
> test_oddmembers = ?test_oddmembers_rhs

> countoddmembers : (l : NatList) -> Nat
> countoddmembers l = ?countoddmembers_rhs

> test_countoddmembers1 : countoddmembers [1,0,3,1,4,5] = 4
> test_countoddmembers1 = ?test_countoddmembers1_rhs

$\square$

==== Exercise: 3 stars, advanced (alternate)

Complete the definition of \idr{alternate}, which "zips up" two lists into one,
alternating between elements taken from the first list and elements from the
second. See the tests below for more specific examples.

Note: one natural and elegant way of writing \idr{alternate} will fail to
satisfy Idris's requirement that all function definitions be "obviously
terminating." If you find yourself in this rut, look for a slightly more verbose
solution that considers elements of both lists at the same time. (One possible
solution requires defining a new kind of pairs, but this is not the only way.)

> alternate : (l1, l2 : NatList) -> NatList
> alternate l1 l2 = ?alternate_rhs

> test_alternate1 : alternate [1,2,3] [4,5,6] =
>                             [1,4,2,5,3,6]
> test_alternate1 = ?test_alternate1_rhs

> test_alternate2 : alternate [1] [4,5,6] = [1,4,5,6]
> test_alternate2 = ?test_alternate2_rhs

> test_alternate3 : alternate [1,2,3] [4] = [1,4,2,3]
> test_alternate3 = ?test_alternate3_rhs

> test_alternate4 : alternate [] [20,30] = [20,30]
> test_alternate4 = ?test_alternate4_rhs

$\square$

=== Bags via Lists

A \idr{Bag} (or \idr{Multiset}) is like a set, except that each element can
appear multiple times rather than just once. One possible implementation is to
represent a bag of numbers as a list.

> Bag : Type
> Bag = NatList

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

Complete the following definitions for the functions \idr{count}, \idr{sum},
\idr{add}, and \idr{member} for bags.

> count : (v : Nat) -> (s : Bag) -> Nat
> count v s = ?count_rhs

All these proofs can be done just by \idr{Refl}.

> test_count1 : count 1 [1,2,3,1,4,1] = 3
> test_count1 = ?test_count1_rhs

> test_count2 : count 6 [1,2,3,1,4,1] = 0
> test_count2 = ?test_count2_rhs

Multiset \idr{sum} is similar to set \idr{union}: \idr{sum a b} contains all the
elements of \idr{a} and of \idr{b}. (Mathematicians usually define union on
multisets a little bit differently, which is why we don't use that name for this
operation.)

\todo[inline]{How to forbid recursion here? Edit}

For \idr{sum} we're giving you a header that does not give explicit names to the
arguments. Moreover, it uses the keyword Definition instead of Fixpoint, so
even if you had names for the arguments, you wouldn't be able to process them
recursively. The point of stating the question this way is to encourage you to
think about whether sum can be implemented in another way -- perhaps by using
functions that have already been defined.

> sum : Bag -> Bag -> Bag
> sum x y = ?sum_rhs

> test_sum1 : count 1 (sum [1,2,3] [1,4,1]) = 3
> test_sum1 = ?test_sum1_rhs

> add : (v : Nat) -> (s : Bag) -> Bag
> add v s = ?add_rhs

> test_add1 : count 1 (add 1 [1,4,1]) = 3
> test_add1 = ?test_add1_rhs

> test_add2 : count 5 (add 1 [1,4,1]) = 0
> test_add2 = ?test_add2_rhs

> member : (v : Nat) -> (s : Bag) -> Bool
> member v s = ?member_rhs

> test_member1 : member 1 [1,4,1] = True
> test_member1 = ?test_member1_rhs

> test_member2 : member 2 [1,4,1] = False
> test_member2 = ?test_member2_rhs

$\square$

==== Exercise: 3 stars, optional (bag_more_functions)

Here are some more bag functions for you to practice with.

When \idr{remove_one} is applied to a bag without the number to remove, it
should return the same bag unchanged.

> remove_one : (v : Nat) -> (s : Bag) -> Bag
> remove_one v s = ?remove_one_rhs

> test_remove_one1 : count 5 (remove_one 5 [2,1,5,4,1]) = 0
> test_remove_one1 = ?test_remove_one1_rhs

> test_remove_one2 : count 5 (remove_one 5 [2,1,4,1]) = 0
> test_remove_one2 = ?test_remove_one2_rhs

> test_remove_one3 : count 4 (remove_one 5 [2,1,5,4,1,4]) = 2
> test_remove_one3 = ?test_remove_one3_rhs

> test_remove_one4 : count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1
> test_remove_one4 = ?test_remove_one4_rhs

> remove_all : (v : Nat) -> (s : Bag) -> Bag
> remove_all v s = ?remove_all_rhs

> test_remove_all1 : count 5 (remove_all 5 [2,1,5,4,1]) = 0
> test_remove_all1 = ?test_remove_all1_rhs

> test_remove_all2 : count 5 (remove_all 5 [2,1,4,1]) = 0
> test_remove_all2 = ?test_remove_all2_rhs

> test_remove_all3 : count 4 (remove_all 5 [2,1,5,4,1,4]) = 2
> test_remove_all3 = ?test_remove_all3_rhs

> test_remove_all4 : count 5
>                    (remove_all 5 [2,1,5,4,5,1,4,5,1,4]) = 0
> test_remove_all4 = ?test_remove_all4_rhs

> subset : (s1 : Bag) -> (s2 : Bag) -> Bool
> subset s1 s2 = ?subset_rhs

> test_subset1 : subset [1,2] [2,1,4,1] = True
> test_subset1 = ?test_subset1_rhs

> test_subset2 : subset [1,2,2] [2,1,4,1] = False
> test_subset2 = ?test_subset2_rhs

$\square$

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

Write down an interesting theorem \idr{bag_theorem} about bags involving the
functions \idr{count} and \idr{add}, and prove it. Note that, since this problem
is somewhat open-ended, it's possible that you may come up with a theorem which
is true, but whose proof requires techniques you haven't learned yet. Feel free
to ask for help if you get stuck!

> bag_theorem : ?bag_theorem

$\square$

== Reasoning About Lists

As with numbers, simple facts about list-processing functions can sometimes be
proved entirely by simplification. For example, the simplification performed by
\idr{Refl} is enough for this theorem...

> nil_app : (l : NatList) -> ([] ++ l) = l
> nil_app l = Refl

... because the \idr{[]} is substituted into the "scrutinee" (the value being
"scrutinized" by the match) in the definition of \idr{app}, allowing the match
itself to be simplified.

Also, as with numbers, it is sometimes helpful to perform case analysis on the
possible shapes (empty or non-empty) of an unknown list.

> tl_length_pred : (l : NatList) -> pred (length l) = length (tl l)
> tl_length_pred [] = Refl
> tl_length_pred (n::l') = Refl

Here, the \idr{Nil} case works because we've chosen to define \idr{tl Nil =
Nil}. Notice that the case for \idr{Cons} introduces two names, \idr{n} and
\idr{l'}, corresponding to the fact that the \idr{Cons} constructor for lists
takes two arguments (the head and tail of the list it is constructing).

Usually, though, interesting theorems about lists require induction for their
proofs.

==== Micro-Sermon

Simply reading example proof scripts will not get you very far! It is important
to work through the details of each one, using Idris and thinking about what
each step achieves. Otherwise it is more or less guaranteed that the exercises
will make no sense when you get to them. 'Nuff said.

=== Induction on Lists

Proofs by induction over datatypes like \idr{NatList} are a little less familiar
than standard natural number induction, but the idea is equally simple. Each
\idr{data} declaration defines a set of data values that can be built up using
the declared constructors: a boolean can be either \idr{True} or \idr{False}; a
number can be either \idr{Z} or \idr{S} applied to another number; a list can be
either \idr{Nil} or \idr{Cons} applied to a number and a list.

Moreover, applications of the declared constructors to one another are the
_only_ possible shapes that elements of an inductively defined set can have, and
this fact directly gives rise to a way of reasoning about inductively defined
sets: a number is either \idr{Z} or else it is \idr{S} applied to some _smaller_
number; a list is either \idr{Nil} or else it is \idr{Cons} applied to some
number and some _smaller_ list; etc. So, if we have in mind some proposition
\idr{p} that mentions a list \idr{l} and we want to argue that \idr{p} holds for
_all_ lists, we can reason as follows:

  - First, show that \idr{p} is true of \idr{l} when \idr{l} is \idr{Nil}.

  - Then show that \idr{P} is true of \idr{l} when \idr{l} is \idr{Cons n l'}
    for some number \idr{n} and some smaller list \idr{l'}, assuming that
    \idr{p} is true for \idr{l'}.

Since larger lists can only be built up from smaller ones, eventually reaching
\idr{Nil}, these two arguments together establish the truth of \idr{p} for all
lists \idr{l}. Here's a concrete example:

> app_assoc : (l1, l2, l3 : NatList) -> ((l1 ++ l2) ++ l3) = (l1 ++ (l2 ++ l3))
> app_assoc [] l2 l3 = Refl
> app_assoc (n::l1') l2 l3 =
>   let inductiveHypothesis = app_assoc l1' l2 l3 in
>     rewrite inductiveHypothesis in Refl

\todo[inline]{Edit}

Notice that, as when doing induction on natural numbers, the as ... clause
provided to the induction tactic gives a name to the induction hypothesis
corresponding to the smaller list l1' in the cons case. Once again, this Coq
proof is not especially illuminating as a static written document -- it is easy
to see what's going on if you are reading the proof in an interactive Coq
session and you can see the current goal and context at each point, but this
state is not visible in the written-down parts of the Coq proof. So a
natural-language proof -- one written for human readers -- will need to include
more explicit signposts; in particular, it will help the reader stay oriented if
we remind them exactly what the induction hypothesis is in the second case.

For comparison, here is an informal proof of the same theorem.

_Theorem_: For all lists \idr{l1}, \idr{l2}, and \idr{l3},

           \idr{(l1 ++ l2) ++ l3 = l1 ++ (l2 ++l3)}.

_Proof_: By induction on \idr{l1}.

  - First, suppose \idr{l1 = []}. We must show

    \idr{([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)},

    which follows directly from the definition of \idr{++}.

  - Next, suppose \idr{l1 = n :: l1'}, with

    \idr{(l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)}

    (the induction hypothesis). We must show

    \idr{((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3)}.

    By the definition of \idr{++}, this follows from

    \idr{n :: ((l1' ++ l2) ++ l 3) = n :: (l1' ++ (l2 ++ l3))},

    which is immediate from the induction hypothesis. $\square$

==== Reversing a List

For a slightly more involved example of inductive proof over lists, suppose we
use \idr{app} to define a list-reversing function \idr{rev}:

> rev : (l : NatList) -> NatList
> rev Nil = Nil
> rev (h :: t) = (rev t) ++ [h]

> test_rev1 : rev [1,2,3] = [3,2,1]
> test_rev1 = Refl

> test_rev2 : rev Nil = Nil
> test_rev2 = Refl

==== Properties of rev

Now let's prove some theorems about our newly defined \idr{rev}. For something a
bit more challenging than what we've seen, let's prove that reversing a list
does not change its length. Our first attempt gets stuck in the successor
case...

```idris
rev_length_firsttry : (l : NatList) -> length (rev l) = length l
rev_length_firsttry Nil = Refl
rev_length_firsttry (n :: l') =
-- Now we seem to be stuck: the goal is an equality involving `++`, but we don't
-- have any useful equations in either the immediate context or in the global
-- environment! We can make a little progress by using the IH to rewrite the
-- goal...
  let inductiveHypothesis = rev_length_firsttry l' in
    rewrite inductiveHypothesis in
-- ... but now we can't go any further.
      Refl
```

So let's take the equation relating \idr{++} and \idr{length} that would have
enabled us to make progress and prove it as a separate lemma.

> app_length : (l1, l2 : NatList) ->
>               length (l1 ++ l2) = (length l1) + (length l2)
> app_length Nil l2 = Refl
> app_length (n :: l1') l2 =
>   let inductiveHypothesis = app_length l1' l2 in
>     rewrite inductiveHypothesis in
>       Refl

Note that, to make the lemma as general as possible, we quantify over _all_
\idr{NatList}s, not just those that result from an application of \idr{rev}.
This should seem natural, because the truth of the goal clearly doesn't depend
on the list having been reversed. Moreover, it is easier to prove the more
general property.

Now we can complete the original proof.

> rev_length : (l : NatList) -> length (rev l) = length l
> rev_length Nil = Refl
> rev_length (n :: l') =
>   rewrite app_length (rev l') [n] in
> -- Prelude's version of `Induction.plus_comm`
>     rewrite plusCommutative (length (rev l')) 1 in
>       let inductiveHypothesis = rev_length l' in
>         rewrite inductiveHypothesis in Refl

For comparison, here are informal proofs of these two theorems:

_Theorem_: For all lists \idr{l1} and \idr{l2},

           \idr{length (l1 ++ l2) = length l1 + length l2}.

_Proof_: By induction on \idr{l1}.

  - First, suppose \idr{l1 = []}. We must show

    \idr{length ([] ++ l2) = length [] + length l2},

    which follows directly from the definitions of \idr{length} and \idr{++}.

  - Next, suppose \idr{l1 = n :: l1'}, with

    \idr{length (l1' ++ l2) = length l1' + length l2}.

    We must show

    \idr{length ((n :: l1') ++ l2) = length (n :: l1') + length l2)}.

    This follows directly from the definitions of \idr{length} and \idr{++}
    together with the induction hypothesis. $\square$

_Theorem_: For all lists \idr{l}, \idr{length (rev l) = length l}.

_Proof_: By induction on \idr{l}.

  - First, suppose \idr{l = []}. We must show

    \idr{length (rev []) = length []},

    which follows directly from the definitions of \idr{length} and \idr{rev}.

  - Next, suppose l = n :: l' , with

    \idr{length (rev l') = length l'}.

    We must show

    \idr{length (rev (n :: l')) = length (n :: l')}.

    By the definition of \idr{rev}, this follows from

    \idr{length ((rev l') ++ [n]) = S (length l')}

    which, by the previous lemma, is the same as

    \idr{length (rev l') + length [n] = S (length l')}.

    This follows directly from the induction hypothesis and the definition of
    \idr{length}. $\square$

The style of these proofs is rather longwinded and pedantic. After the first
few, we might find it easier to follow proofs that give fewer details (which can
easily work out in our own minds or on scratch paper if necessary) and just
highlight the non-obvious steps. In this more compressed style, the above proof
might look like this:

_Theorem_: For all lists \idr{l}, \idr{length (rev l) = length l}.

_Proof_: First, observe that length \idr{(l ++ [n]) = S (length l)} for any
\idr{l} (this follows by a straightforward induction on \idr{l}). The main
property again follows by induction on \idr{l}, using the observation together
with the induction hypothesis in the case where \idr{l = n' :: l'}. $\square$

Which style is preferable in a given situation depends on the sophistication of
the expected audience and how similar the proof at hand is to ones that the
audience will already be familiar with. The more pedantic style is a good
default for our present purposes.

=== Search

\ \todo[inline]{Edit, mention \idr{:s} and \idr{:apropos}?}

We've seen that proofs can make use of other theorems we've already proved,
e.g., using \idr{rewrite}. But in order to refer to a theorem, we need to know
its name! Indeed, it is often hard even to remember what theorems have been
proven, much less what they are called.

Coq's `Search` command is quite helpful with this. Typing `Search foo` will
cause Coq to display a list of all theorems involving `foo`. For example, try
uncommenting the following line to see a list of theorems that we have proved
about `rev`:

```coq
(* Search rev. *)
```

Keep `Search` in mind as you do the following exercises and throughout the rest
of the book; it can save you a lot of time!

If you are using ProofGeneral, you can run `Search` with `C-c C-a C-a`. Pasting
its response into your buffer can be accomplished with `C-c C-;`.

=== List Exercises, Part 1

==== Exercise: 3 stars (list_exercises)

More practice with lists:

> app_nil_r : (l : NatList) -> (l ++ []) = l
> app_nil_r l = ?app_nil_r_rhs

> rev_app_distr : (l1, l2 : NatList) -> rev (l1 ++ l2) = (rev l2) ++ (rev l1)
> rev_app_distr l1 l2 = ?rev_app_distr_rhs

> rev_involutive : (l : NatList) -> rev (rev l) = l
> rev_involutive l = ?rev_involutive_rhs

There is a short solution to the next one. If you find yourself getting tangled
up, step back and try to look for a simpler way.

> app_assoc4 : (l1, l2, l3, l4 : NatList) ->
>              (l1 ++ (l2 ++ (l3 ++ l4))) = ((l1 ++ l2) ++ l3) ++ l4
> app_assoc4 l1 l2 l3 l4 = ?app_assoc4_rhs

An exercise about your implementation of \idr{nonzeros}:

> nonzeros_app : (l1, l2 : NatList) ->
>                 nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2)
> nonzeros_app l1 l2 = ?nonzeros_app_rhs

$\square$

==== Exercise: 2 stars (beq_NatList)

Fill in the definition of \idr{beq_NatList}, which compares lists of numbers for
equality. Prove that \idr{beq_NatList l l} yields \idr{True} for every list
\idr{l}.

> beq_NatList : (l1, l2 : NatList) -> Bool
> beq_NatList l1 l2 = ?beq_NatList_rhs

> test_beq_NatList1 : beq_NatList Nil Nil = True
> test_beq_NatList1 = ?test_beq_NatList1_rhs

> test_beq_NatList2 : beq_NatList [1,2,3] [1,2,3] = True
> test_beq_NatList2 = ?test_beq_NatList2_rhs

> test_beq_NatList3 : beq_NatList [1,2,3] [1,2,4] = False
> test_beq_NatList3 = ?test_beq_NatList3_rhs

> beq_NatList_refl : (l : NatList) -> True = beq_NatList l l
> beq_NatList_refl l = ?beq_NatList_refl_rhs

$\square$

=== List Exercises, Part 2

==== Exercise: 3 stars, advanced (bag_proofs)

Here are a couple of little theorems to prove about your definitions about bags
above.

> count_member_nonzero : (s : Bag) -> lte 1 (count 1 (1 :: s)) = True
> count_member_nonzero s = ?count_member_nonzero_rhs

The following lemma about \idr{lte} might help you in the next proof.

> ble_n_Sn : (n : Nat) -> lte n (S n) = True
> ble_n_Sn Z = Refl
> ble_n_Sn (S k) =
>   let inductiveHypothesis = ble_n_Sn k in
>     rewrite inductiveHypothesis in Refl

> remove_decreases_count : (s : Bag) ->
>                          lte (count 0 (remove_one 0 s)) (count 0 s) = True
> remove_decreases_count s = ?remove_decreases_count_rhs

$\square$

==== Exercise: 3 stars, optional (bag_count_sum)

Write down an interesting theorem \idr{bag_count_sum} about bags involving the
functions \idr{count} and \idr{sum}, and prove it. (You may find that the
difficulty of the proof depends on how you defined \idr{count}!)

> bag_count_sum : ?bag_count_sum

$\square$

==== Exercise: 4 stars, advanced (rev_injective)

Prove that the \idr{rev} function is injective -- that is,

> rev_injective : (l1, l2 : NatList) -> rev l1 = rev l2 -> l1 = l2
> rev_injective l1 l2 prf = ?rev_injective_rhs

(There is a hard way and an easy way to do this.)

$\square$

== Options

Suppose we want to write a function that returns the \idr{n}th element of some
list. If we give it type \idr{Nat -> NatList -> Nat}, then we'll have to choose
some number to return when the list is too short...

> nth_bad : (l : NatList) -> (n : Nat) -> Nat
> nth_bad Nil n = 42 -- arbitrary!
> nth_bad (a :: l') n = case n == 0 of
>                         True => a
>                         False => nth_bad l' (pred n)

This solution is not so good: If \idr{nth_bad} returns \idr{42}, we can't tell
whether that value actually appears on the input without further processing. A
better alternative is to change the return type of \idr{nth_bad} to include an
error value as a possible outcome. We call this type \idr{NatOption}.

> data NatOption : Type where
>   Some : Nat -> NatOption
>   None : NatOption

We can then change the above definition of \idr{nth_bad} to return \idr{None}
when the list is too short and \idr{Some a} when the list has enough members and
\idr{a} appears at position \idr{n}. We call this new function \idr{nth_error}
to indicate that it may result in an error.

> nth_error : (l : NatList) -> (n : Nat) -> NatOption
> nth_error Nil n = None
> nth_error (a :: l') n = case n == 0 of
>                           True => Some a
>                           False => nth_error l' (pred n)

> test_nth_error1 : nth_error [4,5,6,7] 0 = Some 4
> test_nth_error1 = Refl

> test_nth_error2 : nth_error [4,5,6,7] 3 = Some 7
> test_nth_error2 = Refl

> test_nth_error3 : nth_error [4,5,6,7] 9 = None
> test_nth_error3 = Refl

This example is also an opportunity to introduce one more small feature of Idris
programming language: conditional expressions...

> nth_error' : (l : NatList) -> (n : Nat) -> NatOption
> nth_error' Nil n = None
> nth_error' (a :: l') n = if n == 0
>                            then Some a
>                            else nth_error' l' (pred n)

\todo[inline]{Edit or remove this paragraph, doesn't seem to hold in Idris}

Coq's conditionals are exactly like those found in any other language, with one
small generalization. Since the boolean type is not built in, Coq actually
supports conditional expressions over any inductively defined type with exactly
two constructors. The guard is considered true if it evaluates to the first
constructor in the Inductive definition and false if it evaluates to the second.

The function below pulls the \idr{Nat} out of a \idr{NatOption}, returning a
supplied default in the \idr{None} case.

> option_elim : (d : Nat) -> (o : NatOption) -> Nat
> option_elim d (Some k) = k
> option_elim d None = d

==== Exercise: 2 stars (hd_error)

Using the same idea, fix the \idr{hd} function from earlier so we don't have to
pass a default element for the \idr{Nil} case.

> hd_error : (l : NatList) -> NatOption
> hd_error l = ?hd_error_rhs

> test_hd_error1 : hd_error [] = None
> test_hd_error1 = ?test_hd_error1_rhs

> test_hd_error2 : hd_error [1] = Some 1
> test_hd_error2 = ?test_hd_error2_rhs

> test_hd_error3 : hd_error [5,6] = Some 5
> test_hd_error3 = ?test_hd_error3_rhs

$\square$

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

This exercise relates your new \idr{hd_error} to the old \idr{hd}.

> option_elim_hd : (l : NatList) -> (default : Nat) ->
>                  hd default l = option_elim default (hd_error l)
> option_elim_hd l default = ?option_elim_hd_rhs

$\square$

== Partial Maps

As a final illustration of how data structures can be defined in Idris, here is
a simple _partial map_ data type, analogous to the map or dictionary data
structures found in most programming languages.

First, we define a new inductive datatype \idr{Id} to serve as the "keys" of our
partial maps.

> data Id : Type where
>   MkId : Nat -> Id

Internally, an \idr{Id} is just a number. Introducing a separate type by
wrapping each \idr{Nat} with the tag \idr{MkId} makes definitions more readable
and gives us the flexibility to change representations later if we wish.

We'll also need an equality test for \idr{Id}s:

> beq_id : (x1, x2 : Id) -> Bool
> beq_id (MkId n1) (MkId n2) = n1 == n2

==== Exercise: 1 star (beq_id_refl)

> beq_id_refl : (x : Id) -> True = beq_id x x
> beq_id_refl x = ?beq_id_refl_rhs

$\square$

Now we define the type of partial maps:

> namespace PartialMap

>   data PartialMap : Type where
>     Empty : PartialMap
>     Record : Id -> Nat -> PartialMap -> PartialMap

This declaration can be read: "There are two ways to construct a
\idr{PartialMap}: either using the constructor \idr{Empty} to represent an empty
partial map, or by applying the constructor \idr{Record} to a key, a value, and
an existing \idr{PartialMap} to construct a \idr{PartialMap} with an additional
key-to-value mapping."

The \idr{update} function overrides the entry for a given key in a partial map
(or adds a new entry if the given key is not already present).

>   update : (d : PartialMap) -> (x : Id) -> (value : Nat) -> PartialMap
>   update d x value = Record x value d

Last, the \idr{find} function searches a \idr{PartialMap} for a given key. It
returns \idr{None} if the key was not found and \idr{Some val} if the key was
associated with \idr{val}. If the same key is mapped to multiple values,
\idr{find} will return the first one it encounters.

>   find : (x : Id) -> (d : PartialMap) -> NatOption
>   find x Empty = None
>   find x (Record y v d') = if beq_id x y
>                              then Some v
>                              else find x d'

==== Exercise: 1 star (update_eq)

>   update_eq : (d : PartialMap) -> (x : Id) -> (v : Nat) ->
>               find x (update d x v) = Some v
>   update_eq d x v = ?update_eq_rhs

$\square$

==== Exercise: 1 star (update_neq)

>   update_neq : (d : PartialMap) -> (x, y : Id) -> (o : Nat) ->
>                 beq_id x y = False ->
>                 find x (update d y o) = find x d
>   update_neq d x y o prf = ?update_neq_rhs

$\square$

==== Exercise: 2 stars (baz_num_elts)

Consider the following inductive definition:

> data Baz : Type where
>   Baz1 : Baz -> Baz
>   Baz2 : Baz -> Bool -> Baz

How _many_ elements does the type \idr{Baz} have? (Answer in English or the
natural language of your choice.)

$\square$

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Test.Extra.ListTest

import IdrTest.Test
import IdrTest.Expectation

import Extra.List

export
suite : Test
suite =
  describe "List Extra Tests" [
    describe "Length" [
      test "Populated List" (\_ => assertEq
        (length [1,2,3])
        3
      ),
      test "Empty" (\_ => assertEq
        (length (the (List Int) []))
        0
      )
    ],
    describe "Range" [
      test "Simple Range" (\_ => assertEq
        (range 5)
        [0,1,2,3,4]
      ),
      test "Empty Range" (\_ => assertEq
        (range 0)
        []
      )
    ],
    describe "Zip with Index" [
      test "Simple List" (\_ => assertEq
        (zipWithIndex ['a', 'b', 'c', 'd'])
        [('a', 0), ('b', 1), ('c', 2), ('d', 3)]
      ),
      test "Empty List" (\_ => assertEq
        (zipWithIndex (the (List Int) []))
        []
      )
    ],
    describe "Find all" [
      test "Find all simple" (\_ => assertEq
        (findAll (unpack "abcbcd") (unpack "bc"))
        ([1, 3])
      )
    ],
    describe "Replace" [
      test "Replace simple" (\_ => assertEq
        (replace (unpack "abcbcd") (unpack "bc") (unpack "zzz"))
        (unpack "azzzzzzd")
      )
    ]
  ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
totalLen : List String -> Nat
totalLen [] = 0
totalLen xs = foldr (\str, len => length str + len) 0 xs


text:
module Spacing

no : {n : Nat} -> Nat
no {n} = ?no_rhs

spaced : {n : Nat} -> Nat
spaced { n } = ?spaced_rhs

s1 : {n : Nat} -> Nat
s1 { n} = ?s1_rhs

s2 : {n : Nat} -> Nat
s2 {  n} = ?s2_rhs

s3 : {n : Nat} -> Nat
s3 {   n} = ?s3_rhs

noSEq : {n : Nat} -> Nat
noSEq {n = a} = ?noSEq_rhs

spacedEq : {n : Nat} -> Nat
spacedEq { n = a } = ?spacedEq_rhs

s1Eq : {n : Nat} -> Nat
s1Eq { n = a} = ?s1Eq_rhs

s2Eq : {n : Nat} -> Nat
s2Eq {  n = a} = ?s2Eq_rhs

s3Eq : {n : Nat} -> Nat
s3Eq {   n = a} = ?s3Eq_rhs

weirdNo : {n : Nat} -> Nat
weirdNo {n } = ?weirdNo_rhs

weird0a : {n : Nat} -> Nat
weird0a {n= a} = ?weird0a_rhs

weird0b : {n : Nat} -> Nat
weird0b {n =b} = ?weird0b_rhs

weird1a : {n : Nat} -> Nat
weird1a { n= a} = ?weird1a_rhs

weird1b : {n : Nat} -> Nat
weird1b { n =b} = ?weird1b_rhs

weird2a : {n : Nat} -> Nat
weird2a {  n=  a} = ?weird2a_rhs

weird2b : {n : Nat} -> Nat
weird2b {  n  =b} = ?weird2b_rhs

weirdSpacedA : {n : Nat} -> Nat
weirdSpacedA {  n= a } = ?weirdSpacedA_rhs

weirdSpacedB : {n : Nat} -> Nat
weirdSpacedB {  n =b } = ?weirdSpacedB_rhs


text:
module Language.CSV

import Data.List
import Text.Lexer
import Text.Parser
import Text.Token

%default total

public export
data CSVTokenKind
  = TextData
  | Comma
  | CRLF
  | DQuote

export
Eq CSVTokenKind where
  TextData == TextData = True
  Comma == Comma = True
  CRLF == CRLF = True
  DQuote == DQuote = True
  _ == _ = False

export
TokenKind CSVTokenKind where
  TokType TextData = String
  TokType Comma = String
  TokType CRLF = String
  TokType DQuote = String

  tokValue TextData s = s
  tokValue Comma s = s
  tokValue CRLF s = s
  tokValue DQuote s = s

public export
CSVToken : Type
CSVToken = Token CSVTokenKind

export
Eq CSVToken where
  (==) (Tok kind text) (Tok kind' text') = kind == kind' && text == text'

export
Show CSVToken where
  show (Tok TextData s) = s
  show (Tok Comma _) = "COMMA"
  show (Tok CRLF _) = "CRLF"
  show (Tok DQuote _) = "DQUOTE"

private
csvTokenMap : TokenMap CSVToken
csvTokenMap = toTokenMap $
  [ (is ',', Comma)
  , (exact "\r\n", CRLF)
  , (is '"', DQuote)
  , (any <+> many (non $ oneOf "\r\n,\""), TextData)
  ]

export
lexCSV : String -> Maybe (List CSVToken)
lexCSV str =
  case lex csvTokenMap str of
       (tokens, _, _, "") => Just $ map TokenData.tok tokens
       _                  => Nothing

public export
CSV : Type
CSV = List (List String)

comma : Grammar CSVToken True String
comma = match Comma

crlf : Grammar CSVToken True String
crlf = match CRLF

dQuote : Grammar CSVToken True String
dQuote = match DQuote

textData : Grammar CSVToken True String
textData = map concat $ some (match TextData)

twoDQuote : Grammar CSVToken True String
twoDQuote = match DQuote *> match DQuote *> pure "\"\""

nonEscaped : Grammar CSVToken True String
nonEscaped = textData

escaped : Grammar CSVToken True String
escaped = do
  dQuote
  commit
  els <- some (textData <|> twoDQuote <|> comma <|> crlf)
  dQuote
  pure $ concat els

field : Grammar CSVToken True String
field = escaped <|> nonEscaped

rec : Grammar CSVToken True (List String)
rec = sepBy1 comma field

export
csv : Grammar CSVToken True CSV
csv = sepBy1 crlf rec <* optional crlf

export
parseCSV : List CSVToken -> Maybe CSV
parseCSV toks =
  case Text.Parser.Core.parse csv  $ toks of
    Right (dat, [])       => Just dat
    Right (dat, toks)     => Just $ dat ++ [[show toks]]
    Left (Error err toks) => Just $ [[err]] ++ [[show toks]]

export
parse : String -> Maybe CSV
parse x = parseCSV !(lexCSV x)

max_stars_repo_name: wchresta/csv-parser

max_issues_repo_name: wchresta/csv-parser

max_forks_repo_name: wchresta/csv-parser


text:
module Testing

import Data.Vect
import Data.IORef
import Data.SortedSet

%default total

data Pets = Dogs Nat | Cats Nat | NoPets

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

giveMeNumber : (multiple : Bool) -> (isSingleton multiple)
giveMeNumber False = [2,2,2]
giveMeNumber True = 2

hasSpecialSymbols : String -> Type
hasSpecialSymbols password =
  let specialCharacters = Data.SortedSet.toList (intersection (fromList ['#','%','&','+']) (fromList $ unpack password))
  in length specialCharacters `GT` 0

longEnoughPassword : String -> Nat -> Type
longEnoughPassword password n = length password `GTE` n

passwordRequirements : String -> Type
passwordRequirements password = (password ** Pair (hasSpecialSymbols password) (longEnoughPassword password 12))

record Login where
  constructor MkLogin
  loginName : String
  password : (p : String ** length p `GTE` 12)

passwordStrengthChecker : (password : String) -> Dec (length password `GTE` 12)
passwordStrengthChecker password = isLTE 12 (length password)

createNewUser : (loginName : String) -> (password : String) -> Either String Login
createNewUser loginName password = case passwordStrengthChecker password of
  Yes prf => Right $ MkLogin loginName (password ** prf)
  No prf  => Left "Password was not long enough"

symbolCheck : (password : String) -> Dec (hasSpecialSymbols password)
symbolCheck password =
  let specialCharacters =
    Data.SortedSet.toList (intersection (fromList ['#','%','&','+']) (fromList $ unpack password))
  in isLTE 1 (length specialCharacters)

checkRequirements : (p : String) -> Either String (passwordRequirements p)
checkRequirements password =
  case (symbolCheck password, passwordStrengthChecker password) of
    (Yes prf1, Yes prf2) => Right $ (password ** (prf1,prf2))
    _ => Left "Not good enough password"

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

data MyList : (a : Type) -> Type where
  Nil : MyList a
  (::) : (x : a) -> (xs : MyList a) -> MyList a

data PriceCategory = Regular | Membership

data ProductPrice : (price : Double) -> PriceCategory -> Type where
  RegularPrice : ProductPrice price Regular
  BestBeforePrice : ProductPrice price Regular
  MembershipPrice : (discountPercent : Double) -> ProductPrice price Membership

calculateFinalPrice : (productPrice : ProductPrice price category) -> Double
calculateFinalPrice {price} RegularPrice = price
calculateFinalPrice {price} BestBeforePrice = 0.7 * price
calculateFinalPrice {price} (MembershipPrice discount) = discount * price

limitedOffer : (productPrice : ProductPrice price category) -> {auto p : price < 20.0 = True} -> Double
limitedOffer {price} _ = 0.5 * price

toRegularPrice : (price : Double) -> (ProductPrice price Regular)
toRegularPrice price = RegularPrice

unitTest1 : limitedOffer (toRegularPrice 19.0) = 0.5 * 19.0
unitTest1 = Refl

--unitTest2 : limitedOffer (toRegularPrice 21.0) = 0.5 * 21.0

sayLength : Vect n a -> String
sayLength {n} _ = "You gave Vector of length " ++ (cast n)

record Car where
  constructor MkCar
  model : String
  year : Int

car : Car
car = MkCar "Ferrari" 1988

data Access = LoggedOut | LoggedIn

data UsernameCheck = Authorized | NotAuthorized

data DataStore : (a : Type) -> (beforeState : Access) -> (afterStateFn : a -> Access) -> Type where
  LoginToStore : (username : String)
               -> DataStore UsernameCheck LoggedOut (\check => case check of
                                                                    Authorized => LoggedIn
                                                                    NotAuthorized => LoggedOut)
  LogoutFromStore : DataStore () LoggedIn (const LoggedOut)

  AddToList : a -> List a -> DataStore (List a) LoggedIn (const LoggedIn)
  Display : (Show a) => a -> DataStore () LoggedIn (const LoggedIn)
  Message : String -> DataStore () state (const state)

  Pure : (res : m) -> DataStore m (stateFn res) stateFn
  (>>=) : DataStore a state1 state2Fn -> ((res : a) -> DataStore b (state2Fn res) state3Fn) -> DataStore b state1 state3Fn

addAndDisplay : DataStore () LoggedOut (const LoggedOut)
addAndDisplay = do
  res <- LoginToStore "root"
  case res of
    NotAuthorized => Message "Not authorized user"
    Authorized => do
      store <- AddToList "Super secret secret" []
      Display store
      store <- AddToList "Second super secret secret" store
      Display store
      LogoutFromStore

runDataStore : DataStore res state1 state2fn -> IO res
runDataStore (LoginToStore username) =
  case username of
    "root" => pure Authorized
    _      => pure NotAuthorized
runDataStore LogoutFromStore = pure ()
runDataStore (AddToList x xs) = pure (x :: xs)
runDataStore (Display as) = do putStrLn $ show as
                               pure ()
runDataStore (Message s) = do putStrLn s
                              pure ()
runDataStore (Pure x) = pure x
runDataStore (x >>= f) = do r <- runDataStore x
                            runDataStore (f r)

data Zones = A | B | C | D | E

implementation Eq Zones where
  A == A = True
  B == B = True
  C == C = True
  D == D = True
  E == E = True
  _ == _ = False

implementation Ord Zones where
  compare a b = if a == b then EQ else
                   case (a,b) of
                     (A, _) => LT
                     (_, A) => GT
                     (B, _) => LT
                     (_, B) => GT
                     (C, _) => LT
                     (_, C) => GT
                     (D, _) => LT
                     (_, D) => GT
                     (E, _) => LT
                     (_, E) => GT

--test : DataStore () LoggedOut (const LoggedOut)
--test = LoginToStore "user" >>= \res => LogoutFromStore
--test = do
--  LoginToStore "user"
--  LogoutFromStore

-- Local Variables:
-- idris-load-packages: ("pruviloj" "prelude" "effects" "contrib" "base")
-- End:

max_stars_repo_name: neurogoo/idris-intro-presentation

max_issues_repo_name: neurogoo/idris-intro-presentation

max_forks_repo_name: neurogoo/idris-intro-presentation


text:
--
-- copyright (c) 2017 Simon Beaumont
--

||| This module defines an AST for the Dirac notation of linear algebra.

module Language.Dirac.AST

import public Data.Complex -- for complex amplitides

import Data.Fin  -- finite domain
import Data.Vect -- for finite lists
import Data.Matrix -- for matrices (in one intepretation)

||| The types in Dirac notation - the attempt here is to keep these as
||| abstract as possible and then provide concrete implmentations.

data Typ =
     ||| A real valued expression (R)
     Real |
     ||| A complex valued expression  (C)
     Amplitude |
     ||| The primary type of state
     Ket Nat |
     ||| Adjoint dual of a Ket
     Bra Nat |
     ||| Unitary operator
     Operator Nat |
     ||| Self adjoint operator
     Measure Nat |
     ||| A typed functional language
     Function Typ Typ

||| Transform AST type to a concrete Idris type

interpTyp : Typ -> Type
interpTyp Real = Double
interpTyp Amplitude = Complex Double
interpTyp (Ket n) = Vect n (Complex Double)
interpTyp (Bra n) = Vect n (Complex Double)
interpTyp (Operator n) = Matrix n n (Complex Double)
interpTyp (Measure n) = Matrix n n (Complex Double)
interpTyp (Function a t) = interpTyp a -> interpTyp t

-- Context of language evaluation - taken from well typed interpreter
-- example in Idris documentation

using (G : Vect n Typ)

  ||| Variables are deBruijn indexed
  data HasType : (i : Fin n) -> Vect n Typ -> Typ -> Type where
    Stop : HasType FZ (t :: G) t
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t

  ||| Type indexed expressions
  data Expr : Vect n Typ -> Typ -> Type where
    ||| Variable constructor
    Var : HasType i G t -> Expr G t
    ||| Real value
    RVal : (x : Double) -> Expr G Real
    ||| Complex value
    CVal : (z : (Complex Double)) -> Expr G Amplitude
    ||| Arbitrary binary op -- TODO might need more sophisitcated ops
    Op : (interpTyp a -> interpTyp b -> interpTyp c) -> Expr G a -> Expr G b -> Expr G c
    ||| Lambda
    Lam : Expr (a :: G) t -> Expr G (Function a t)
    ||| Function application
    App : Expr G (Function a t) -> Expr G a -> Expr G t

  ||| Get a value from the enviroment of in scope expressions

  data Env : Vect n Typ -> Type where
    Nil  : Env Nil
    (::) : interpTyp a -> Env G -> Env (a :: G)

  lookup : HasType i G t -> Env G -> interpTyp t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs

  ||| An interpreter takes an expression in an environment
  ||| into an Idris value

  interp : Env G -> Expr G t -> interpTyp t
  interp env (Var i)     = lookup i env
  interp env (RVal x)    = x
  interp env (CVal z)    = z
  interp env (Lam sc)    = \x => interp (x :: env) sc
  interp env (App f s)   = interp env f (interp env s)
  interp env (Op op x y) = op (interp env x) (interp env y)

  -- Examples

  ||| Add two complex amplitudes
  add : Expr G (Function Amplitude (Function Amplitude Amplitude))
  add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

  -- ||| Add two Kets (Qubits)
  sum : Expr G (Function (Ket 2) (Function (Ket 2) (Ket 2)))
  sum = Lam (Lam (Op (Data.Vect.zipWith (+)) (Var Stop) (Var (Pop Stop))))

-- Local Variables:
-- idris-load-packages: ("base" "contrib")
-- End:

max_stars_repo_name: sebeaumont/hilbert

max_issues_repo_name: sebeaumont/hilbert

max_forks_repo_name: sebeaumont/hilbert


text:
module Control.Monad.Logic

import public Control.Monad.Identity
import public Control.Monad.Logic.Interface
import public Control.Monad.Logic.Logic


text:
module Util

import public Effects
import public Effect.Random

import public Data.Vect
import public Data.Matrix
import public Data.Matrix.Numeric

%access public export

infixl 5 <+ -- add a vector to each row of a matrix

||| Maximum size of the integer distribution
RAND_MAX : Integer
RAND_MAX = 32767

||| Generate a random Double in the range of  [0.0, 1.0]
rndUnitDouble : Eff Double [RND]
rndUnitDouble =
  pure $ (fromInteger !(rndInt 0 RAND_MAX)) / fromInteger RAND_MAX

||| Generate a randome Double in the range of [min, max]
rndDouble : (min : Double) -> (max : Double) -> Eff Double [RND]
rndDouble min max =
  pure $ (min + (max - min) * !rndUnitDouble)

||| Generate a random vector of length n of Doubles in the range of [min, max]
rndVect : (n : Nat) ->
          (min: Double) ->
          (max: Double) ->
          Eff (Vect n Double) [RND]
rndVect Z _ _ = pure []
rndVect (S k) min max = pure (!(rndDouble min max) :: !(rndVect k min max))

||| Generate an n x m matrix of random Doubles in the range of [min, max]
rndMat : (n : Nat) ->
         (m : Nat) ->
         (min : Double) ->
         (max: Double) ->
         Eff (Matrix n m Double) [RND]
rndMat Z _ _ _ = pure []
rndMat (S k) m min max = pure (!(rndVect m min max) :: !(rndMat k m min max))

||| Generate a vector of length n of Doubles initialized to 0.0
zeroVect : (n : Nat) -> Vect n Double
zeroVect Z = []
zeroVect (S k) = 0.0 :: zeroVect k

||| Generate an n x m matrix of random Doubles initialized to 0.0
zeroMat : (n : Nat) -> (m : Nat) -> Matrix n m Double
zeroMat Z _ = []
zeroMat (S k) m = zeroVect m :: zeroMat k m

||| Add a vector to each row of a matrix
(<+) : Matrix n m Double -> Vect m Double -> Matrix n m Double
(<+) [] _ = []
(<+) (x :: xs) v = (x + v) :: (xs <+ v)


text:
module Meriv.Core.Interp

import Meriv.Core.Interfaces.Unifiable

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype


text:
module Text.CSS.Declaration

import Text.CSS.Color
import Text.CSS.ListStyleType
import Text.CSS.Property

%default total

public export
record Declaration where
  constructor MkDeclaration
  property : Property tpe
  value    : tpe

infixl 8 .=

export %inline
(.=) : Property t -> t -> Declaration
(.=) = MkDeclaration

export %inline
render : Declaration -> String
render (MkDeclaration p v) = renderProp p v ++ ";"


text:
module Optimisation.OrderAndEliminateDefinitions

import Core.Context
import Data.List
import Data.SortedSet
import Data.SortedMap
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Utils.Helpers
import CairoCode.Traversal.Base
import Primitives.Primitives

-- Topological Orderer (it is so small that it is not worth a file)
sortUsedDefsTopologicalRecurive : SortedMap Name CairoDef -> SortedSet Name -> Name -> (SortedSet Name, List (Name, CairoDef))
sortUsedDefsTopologicalRecurive allDefs done cur = if contains cur done
    then (done, [])
    else case lookup cur allDefs of
      Nothing => (done, [])
      Just curDef => let (newDone, orderedDefs) = processDef (cur, curDef) in (newDone, orderedDefs ++ [(cur, curDef)])
  where dependencyCollector : InstVisit CairoReg -> SortedSet Name
        dependencyCollector (VisitMkClosure _ name _ _) = singleton name
        dependencyCollector (VisitCall _ _ name _) = singleton name
        dependencyCollector (VisitOp _ _ primFn _) = primFnDependencyNames primFn
        dependencyCollector _ = empty
        dependencies : (Name, CairoDef) -> SortedSet Name
        dependencies def = snd $ runVisitConcatCairoDef (pureTraversal dependencyCollector) def
        processDep : (SortedSet Name, List (Name, CairoDef)) -> Name -> (SortedSet Name, List (Name, CairoDef))
        processDep (nd, acc) n = let (rdone, res) = sortUsedDefsTopologicalRecurive allDefs nd n in (rdone, acc ++ res)
        processDef : (Name, CairoDef) -> (SortedSet Name, List (Name, CairoDef))
        processDef curDef = foldl processDep (insert cur done, []) (dependencies curDef)

export
orderUsedDefs : Name -> List (Name, CairoDef) -> List (Name, CairoDef)
orderUsedDefs entry cairocode = snd (sortUsedDefsTopologicalRecurive (fromList cairocode) empty entry)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro