text:
--
-- Specification
--
-- a. Unsigned integers
--
--    Unsigned integers with a precision of x bit have a valid
--    range of [0,2^x - 1]. They support all the usual arithmetic
--    operations: +,*,-,div, and mod. If the result y of an operation
--    is outside the valid range, the unsigned remainder modulo 2^x of y
--    is returned instead. The same kind of truncation happens when
--    other numeric types are cast to one of the unsigned integer
--    types.
--
--    Example: For `Bits8` the valid range is [0,255]. Below are some
--             example calculations. All numbers are considered to be of type `Bits8`
--             unless specified otherwise:
--
--               255 + 7 = 6
--               3 * 128 = 128
--               (-1)    = 255
--               7 - 10  = 253
--
-- b. Signed integers
--
--    Signed integers with a precision of x bit have a valid
--    range of [-2^(x-1),2^(x-1) - 1]. They support all the usual arithmetic
--    operations: +,*,-,div, and mod. If the result `y` of an operation
--    is outside the valid range, the signed remainder modulo 2^x of `y`
--    is calculated and 2^x subtracted from the result if it
--    is still out of bounds. The same kind of truncation happens when
--    other numeric types are cast to one of the signed integer
--    types.
--
--    Example: For `Int8` the valid range is [-128,127]. Below are some
--             example calculations. All numbers are considered to be of type `Int8`
--             unless specified otherwise:
--
--               127 + 7   = -122
--               3 * 64    = -64
--               2 * (-64) = -128
--               (-129)    = 127
--               7 - 10    = -3
--
import Data.List
import Data.Stream

record IntType (a : Type) where
  constructor MkIntType
  name      : String
  signed    : Bool
  precision : Integer
  min       : Integer
  max       : Integer

intType : Bool -> String -> Integer -> IntType a
intType True  n p = let ma = prim__shl_Integer 1 (p - 1)
                     in MkIntType n True p (negate ma) (ma - 1)
intType False n p = let ma = prim__shl_Integer 1 p
                     in MkIntType n False p 0 (ma - 1)

bits8 : IntType Bits8
bits8 = intType False "Bits8" 8

bits16 : IntType Bits16
bits16 = intType False "Bits16" 16

bits32 : IntType Bits32
bits32 = intType False "Bits32" 32

bits64 : IntType Bits64
bits64 = intType False "Bits64" 64

int8 : IntType Int8
int8 = intType True "Int8" 8

int16 : IntType Int16
int16 = intType True "Int16" 16

int32 : IntType Int32
int32 = intType True "Int32" 32

int64 : IntType Int64
int64 = intType True "Int64" 64

int : IntType Int
int = intType True "Int" 64

record Op a where
  constructor MkOp
  name      : String
  op        : a -> a -> a
  opInt     : Integer -> Integer -> Integer
  allowZero : Bool
  type      : IntType a

add : Num a => IntType a -> Op a
add = MkOp "+" (+) (+) True

sub : Neg a => IntType a -> Op a
sub = MkOp "-" (-) (-) True

mul : Num a => IntType a -> Op a
mul = MkOp "*" (*) (*) True

div : Integral a => IntType a -> Op a
div = MkOp "div" (div) (div) False

mod : Integral a => IntType a -> Op a
mod = MkOp "mod" (mod) (mod) False

pairs : List (Integer,Integer)
pairs = let -- [1,2,4,8,16,...,18446744073709551616]
            powsOf2  = take 65 (iterate (*2) 1)

            -- powsOf2 ++ [0,1,3,7,...,18446744073709551615]
            naturals = powsOf2 ++ map (\x => x-1) powsOf2

            -- positive and negative versions of naturals
            ints     = naturals ++ map negate naturals

            -- naturals paired with ints
         in [| (,) ints naturals |]

-- This check does the following: For a given binary operation `op`,
-- calculate the result of applying the operation to all passed pairs
-- of integers in `pairs` and check, with the given bit size, if
-- the result is out of bounds. If it is, calculate the result
-- modulo 2^bits. This gives the reference result as an `Integer`.
--
-- Now perform the same operation with the same input but for
-- the integer type we'd like to check and cast the result back
-- to an `Integer`. Create a nice error message for every pair
-- that fails (returns an empty list if all goes well).
check :  (Num a, Cast a Integer) => Op a -> List String
check (MkOp name op opInt allowZero $ MkIntType type signed bits mi ma) =
  let ps = if allowZero then pairs
           else filter ((0 /=) . checkBounds . snd) pairs
   in mapMaybe failing ps

  where
    trueMod : Integer -> Integer -> Integer
    trueMod x y = let res = x `mod` y
                   in if res < 0 then res + y else res

    checkBounds : Integer -> Integer
    checkBounds n = let r1 = trueMod n (ma + 1 - mi)
                     in if r1 > ma
                           then r1 - (ma + 1 - mi)
                           else r1

    failing : (Integer,Integer) -> Maybe String
    failing (x,y) =
      let resInteger = opInt x y
          resMod     = checkBounds $ opInt (checkBounds x) (checkBounds y)
          resA       = cast {to = Integer} (op (fromInteger x) (fromInteger y))
       in if resA == resMod
             then Nothing
             else Just #"Error when calculating \#{show x} \#{name} \#{show y} for \#{type}: Expected \#{show resMod} but got \#{show resA} (unrounded: \#{show resInteger})"#

--------------------------------------------------------------------------------
--          Main
--------------------------------------------------------------------------------

main : IO ()
main = do traverse_ putStrLn . check $ add int8
          traverse_ putStrLn . check $ sub int8
          traverse_ putStrLn . check $ mul int8
          traverse_ putStrLn . check $ div int8
          traverse_ putStrLn . check $ mod int8

          traverse_ putStrLn . check $ add int16
          traverse_ putStrLn . check $ sub int16
          traverse_ putStrLn . check $ mul int16
          traverse_ putStrLn . check $ div int16
          traverse_ putStrLn . check $ mod int16

          traverse_ putStrLn . check $ add int32
          traverse_ putStrLn . check $ sub int32
          traverse_ putStrLn . check $ mul int32
          traverse_ putStrLn . check $ div int32
          traverse_ putStrLn . check $ mod int32

          traverse_ putStrLn . check $ add int64
          traverse_ putStrLn . check $ sub int64
          traverse_ putStrLn . check $ mul int64
          traverse_ putStrLn . check $ div int64
          traverse_ putStrLn . check $ mod int64

          traverse_ putStrLn . check $ add int
          traverse_ putStrLn . check $ sub int
          traverse_ putStrLn . check $ mul int
          traverse_ putStrLn . check $ div int
          traverse_ putStrLn . check $ mod int

          traverse_ putStrLn . check $ add bits8
          traverse_ putStrLn . check $ sub bits8
          traverse_ putStrLn . check $ mul bits8
          traverse_ putStrLn . check $ div bits8
          traverse_ putStrLn . check $ mod bits8

          traverse_ putStrLn . check $ add bits16
          traverse_ putStrLn . check $ sub bits16
          traverse_ putStrLn . check $ mul bits16
          traverse_ putStrLn . check $ div bits16
          traverse_ putStrLn . check $ mod bits16

          traverse_ putStrLn . check $ add bits32
          traverse_ putStrLn . check $ sub bits32
          traverse_ putStrLn . check $ mul bits32
          traverse_ putStrLn . check $ div bits32
          traverse_ putStrLn . check $ mod bits32

          traverse_ putStrLn . check $ add bits64
          traverse_ putStrLn . check $ sub bits64
          traverse_ putStrLn . check $ mul bits64
          traverse_ putStrLn . check $ div bits64
          traverse_ putStrLn . check $ mod bits64

ext: idr


text:
module Environment

import Control.ST
import Data.IORef
import Control.ST.Exception
import Data.SortedMap

%access public export

data Bindings : Type -> Type where
    MkBindings : SortedMap String (IORef a) -> Bindings a

BindingsRef : Type -> Type
BindingsRef a = IORef (Bindings a)

data EnvRef a =
    Global (BindingsRef a)
    | Frame (BindingsRef a) (EnvRef a)

interface Envir a (m: Type -> Type) | m where
    showEnv   : Show a => EnvRef a -> ST m String []
    initEnv   : List (String, a)             -> ST m (EnvRef a) []
    getVar    : EnvRef a -> String           -> ST m (Maybe a) []
    setVar    : EnvRef a -> String -> a      -> ST m Bool []
    defineVar  : EnvRef a -> String -> a      -> ST m () []
    bindVars  : EnvRef a -> List (String, a) -> ST m (EnvRef a) []

addBinding : HasReference ffi => (String, a) -> IO' ffi (String, IORef a)
addBinding (k, v) =
    do ref <- newIORef' v
       pure (k, ref)

getBindingsRef : EnvRef a -> BindingsRef a
getBindingsRef (Global bindRef) = bindRef
getBindingsRef (Frame bindRef _) = bindRef

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Main

mwhile : (test : IO Bool) -> (body : IO ()) -> IO ()
mwhile t b = do v <- t
                case v of
                     True => do b
                                mwhile t b
                     False => pure ()

dumpFile : String -> IO ()
dumpFile fn = do { Right h <- openFile fn Read
                   mwhile (do { -- putStrLn "TEST"
                                x <- fEOF h
                                pure (not x) })
                          (do { Right l <- fGetLine h
                                putStr l })
                   closeFile h }

main : IO ()
main = do { Right h <- openFile "testfile" WriteTruncate
            fPutStr h "Hello!\nWorld!\n...\n3\n4\nLast line\n"
            closeFile h
            putStrLn "Reading testfile"
            Right f <- readFile "testfile"
            putStrLn f
            putStrLn "---"
            dumpFile "testfile"
            putStrLn "---"
          }

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Data.ZZ.ZZModulo

import Control.Algebra
import Classes.Verified

import Data.ZZ
import Control.Algebra.NumericInstances

import Data.Fin.FinOrdering
import Data.Fin.Structural

import Control.Algebra.ZZDivisors
import Data.ZZ.ModuloVerification

{-
Table of contents

* Modulo for naturals
* Lemmas for applying (modNatFnIsRemainder)
* Derived modulo for ZZ
-}

{-
Modulo for naturals
-}

||| A manually verifiably total modulo for naturals:
||| It recurses precisely when
||| 	( Not (x `LT` m) ) & ( m, x > 0 ).
||| Not (x `LT` m) -> Either (x = m) (m `LT` x),
||| in former case ((x `minus` m) `modNat` m) is defined,
||| & latter case cannot hold indefinitely since
||| m > 0
||| ==>
||| the iterates of (`minus` m) are decreasing.
%reflection
modNatT : Nat -> Nat -> Nat
modNatT Z _ = Z
modNatT x Z = x
modNatT (S predx) (S predm) with (decLT (S predx) (S predm))
	| No notlt = ((S predx) `minus` (S predm)) `modNatT` (S predm)
	| Yes prlt = S predx

{-
Lemmas for applying (modNatFnIsRemainder)
-}

total
modNatTIdModZero : (x : Nat) -> x `modNatT` Z = x
modNatTIdModZero Z = Refl
modNatTIdModZero (S predx) = Refl

-- The LT implies subtracting m is reversible
total
modNatTCharizLT :
	(x, m : Nat)
	-> (x `LT` m)
	-> x `modNatT` m = x
modNatTCharizLT Z _ _ = Refl
modNatTCharizLT x Z ltpr = void $ succNotLTEzero ltpr
modNatTCharizLT (S predx) (S predm) ltpr with (decLT (S predx) (S predm))
	| No notlt = void $ notlt ltpr
	| Yes prlt = Refl

total
modNatTCharizEq : (m : Nat) -> m `modNatT` m = Z
modNatTCharizEq Z = Refl
modNatTCharizEq (S predm) with (decLT (S predm) (S predm))
	| No notlt = rewrite sym $ minusZeroN predm in Refl
	| Yes prlt = void $ notLTSelf prlt

total
modNatTCharizGTE :
	(x, m : Nat)
	-> (m `plus` x) `modNatT` m = x `modNatT` m
modNatTCharizGTE Z m
	= trans (rewrite plusZeroRightNeutral m in Refl)
	$ modNatTCharizEq m
modNatTCharizGTE x Z = Refl
modNatTCharizGTE (S predx) (S predm) with (decLT (S predm `plus` S predx) (S predm))
	| No notlt = rewrite natPlusInvertibleL (S predx) predm in Refl
	| Yes prlt = void $ notLTSelf $ lteUnsumLeftSummandLeft {y=S predx} prlt

total
modNatTIsRemainder :
	(x, m : Nat)
	-> (d : Nat ** (d `mult` m) `plus` (x `modNatT` m) = x)
modNatTIsRemainder =
	modNatFnIsRemainder
		modNatT
		modNatTIdModZero
		modNatTCharizLT
		modNatTCharizGTE

{-
-- Totally superfluous
modNatTCharizSucc :
	(x, m : Nat)
	-> S x `modNatT` m = (S $ x `modNatT` m) `modNatT` m
modNatTCharizSucc Z _ = ?modNatTCharizSucc_rhs_1
modNatTCharizSucc (S predx) m = ?modNatTCharizSucc_rhs_2
-}

{-
Derived modulo for ZZ
-}

total
modZT : ZZ -> ZZ -> ZZ
modZT = modZGenFn modNatT modNatTIsRemainder

quotientPartModZT :
	(x, m : ZZ)
	-> (x <-> (x `modZT` m)) `quotientOverZZ` m
quotientPartModZT = modZGenQuot modNatT modNatTIsRemainder


text:
module Chip8

import System
import Data.Bits
import Data.Fin
import Data.Buffer
import Data.Vect

import Utilities
import Constants
import Screen
import Keypad
import Cpu

%default total

public
export
data Chip8State =
  Active
  | WaitingForKey (Fin 16)
  | Halted String

public
export
record Chip8 where
  constructor MkChip8
  Computer : Cpu
  Display : Screen
  Memory : Buffer -- 4kb RAM
  Keys : Keypad
  State : Chip8State

export
newChip8 : IO Chip8
newChip8 =
  do
    buf <- Buffer.newBuffer RamSize
    case buf of
      Just ram =>
        let keys = MkKeypad $ Vect.replicate 16 False in
        pure $ MkChip8 newCpu newScreen ram keys Active
      Nothing =>
        do
          putStrLn "Not enough memory"
          System.exitFailure

export
loadROMAt : (chip : Chip8) -> (rom : Buffer) -> (address : Int) -> IO ()
loadROMAt chip rom address =
  let memory = Memory chip in
  let length = Buffer.size rom in
  do
    Buffer.copyData rom 0 length memory address

export
isHalted : (chip : Chip8) -> Maybe String
isHalted chip =
  case State chip of
    Halted error => Just error
    _ => Nothing

export
isKeyPressed : (chip : Chip8) -> (n : Fin 16) -> Bool
isKeyPressed chip n = isKeyPressed (Keys chip) n


text:
module Main

import Data.Vect

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

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

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

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

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

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

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

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

-- Exercise 2 and Exercise 3
searchString : (store : DataStore) -> (str : String) -> String
searchString store str = searchString' 0 (items store) str
  where
    searchString' : Nat -> Vect n String -> String -> String
    searchString' idx [] str = ""
    searchString' idx (x :: xs) str
      = let remainder = searchString' (idx + 1) xs str
        in case str `isInfixOf` x of
             False => remainder
             True => "ID " ++ show idx ++ ": " ++ x ++ "\n" ++ remainder

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

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


text:
data Name : Type where
  MN : Int -> Name

data IsVar : Name -> List Name -> Type where
  First : IsVar n (n :: ns)
  Later : IsVar n ns -> IsVar n (m :: ns)

data Expr : List Name -> Type where
  CLocal : (prf : IsVar x vars) -> Expr vars

data FunDecl : Type where
  MkFunDecl : (vars : List Name) -> Expr vars -> FunDecl

funDeclWorks : List FunDecl
funDeclWorks = [MkFunDecl [MN 0] (CLocal First)]

foo : Expr [MN 0]
foo = CLocal First

dpairFails : List (vars : List Name ** Expr vars)
dpairFails = [([MN 0] ** CLocal First)]

dpairWithExtraInfoWorks : List (vars : List Name ** Expr vars)
dpairWithExtraInfoWorks = [([MN 0] ** CLocal {x=MN 0} (First {ns=[]}))]

dpairWithExtraInfoBad : List (vars : List Name ** Expr vars)
dpairWithExtraInfoBad = [([MN 0] ** CLocal {x=MN 0} (First {ns=[MN 0]}))]


text:
module Main

import Common.Abbrev
import Common.Util
import Common.Interfaces
import Specifications.Semigroup
import Specifications.Monoid
import Specifications.Group
import Specifications.Order
import Specifications.Ring
import Specifications.TranslationInvariance
import Specifications.OrderedGroup
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing
import Symmetry.Opposite
import Symmetry.Abelian
import Proofs.OrderTheory
import Proofs.SemigroupTheory
import Proofs.GroupCancelationLemmas
import Proofs.GroupTheory
import Proofs.GroupCancelMisc
import Proofs.TranslationInvarianceTheory
import Proofs.DiscreteOrderTheory
import Proofs.Interval
import Proofs.RingTheory
import Instances.Notation
import Instances.TrustInteger
import Instances.OrderZZ
import Instances.ZZ
import Applications.Example

%default total

testAbsoluteValue : Integer -> Integer
testAbsoluteValue x = fst $
  absoluteValue (orderedGroup integerDiscreteOrderedGroup) x

testAbsoluteValueZZ : ZZ -> ZZ
testAbsoluteValueZZ x = fst $ absoluteValue zzOrderedGroup x

main : IO ()
main = do printLn $ map testAbsoluteValue [(-5)..5]
          printLn $ map testAbsoluteValueZZ (map fromInteger [(-10)..10])

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
||| This example follows the same framework as the tutorial, but with custom labels
||| We use a custom datatype for labels instead of `String`.
module Flexidisc.CustomLabels

import Flexidisc
import Flexidisc.InjectiveKey

%default total

export
data Feature = Firstname | Lastname | Age | ID

implementation InjectiveKey Feature Nat where

  inj Firstname = 0
  inj Lastname  = 1
  inj Age       = 2
  inj ID        = 3

  ret x with (toIntegerNat x)
    | 0 = Firstname
    | 1 = Lastname
    | 2 = Age
    | n = ID

  inv Firstname = Refl
  inv Lastname  = Refl
  inv Age       = Refl
  inv ID        = Refl

testEqFalse : Firstname == Lastname = False
testEqFalse = Refl

testEqTrue : Firstname == Firstname = True
testEqTrue = Refl

testOrdLT : Firstname < Lastname = True
testOrdLT = Refl

testOrdEQ : compare Firstname Firstname = EQ
testOrdEQ = Refl

person0 : Record Feature [Firstname ::: String]
person0 = [Firstname := "John"]

||| From here, we can access row by name.
|||
||| Fields are verified at compile time: if we try to access a field that is
||| not defined for our record, we obtain a compilation error, not a runtime
||| error.
|||
||| One of the key contribution in Flexidisc is that you can't declare the
||| smae field twice (no, it's not that easy)
||| If we add another field 'Firstname', even with a different type,
||| we'll obtain a compilation error.
person0Name : String
person0Name = get Firstname person0

||| or with the infix notation:
person0Name' : String
person0Name' = person0 !! Firstname

||| you can even lookup for fields that my or may not be there
person0age : Maybe Nat
person0age = Read.lookup Age person0

||| We can of course extend records:
||| we can use either the definition below or `person1 = ["Biri", "Nicolas"]
person1 : Record Feature [Age ::: Nat, Lastname ::: String, Firstname ::: String]
person1 = (Lastname := "Doe") :: (Age := the Nat 42) :: person0

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
||| The JSON language, as described at https://json.org/
module Language.JSON

import Language.JSON.Lexer
import Language.JSON.Parser

import public Language.JSON.Data

import public Text.Bounded

%default total

||| Parse a JSON string.
export
parse : String -> Maybe JSON
parse x = parseJSON !(lexJSON x)


text:
module BoundedGCD
import ZZ
import ZZUtils
import Divisors

%default total
%access public export

notLTEimpliesLT : (a: Nat) -> (b: Nat) -> (LTE a b -> Void) -> LTE (S b) a
notLTEimpliesLT Z b contra = void (contra (LTEZero))
notLTEimpliesLT (S k) Z f = LTESucc (LTEZero)
notLTEimpliesLT (S k) (S j) contra =
  LTESucc (notLTEimpliesLT k j previousContra) where
    previousContra = \evidence : (LTE k j) => contra (LTESucc evidence)

subWithBound: (n: Nat) -> (m: Nat) -> (LTE m n) -> (k: Nat ** LTE k n)
subWithBound n Z LTEZero = (n ** lteRefl)
subWithBound (S p) (S q) (LTESucc pf) = case subWithBound p q pf of
                                             (x ** pf) =>
                                                (x ** lteSuccRight pf)

boundedGCD : (bnd: Nat) -> (n: Nat) -> (m: Nat) -> (LTE n bnd) -> (LTE (S m) bnd) -> Nat
boundedGCD (S b) Z m x (LTESucc y) = m
boundedGCD (S b) (S k) Z x (LTESucc y) = (S k)
boundedGCD (S b) (S Z) (S j) (LTESucc x) (LTESucc y) = S Z
boundedGCD (S b) (S k) (S Z) (LTESucc x) (LTESucc y) = S Z
boundedGCD (S b) (S (S (k))) (S (S (j))) (LTESucc x) (LTESucc y) =
  case isLTE j k of
        (Yes prf) => case subWithBound k j prf of
                           (diff ** pf) => boundedGCD b (S (S j)) diff y (lteTransitive (LTESucc pf) x)
        (No contra) =>
          let
            ineq = notLTEimpliesLT j k contra
          in
            boundedGCD b (S (S j)) (S (S k)) y (lteTransitive (LTESucc (LTESucc ineq)) y)

gcdAlgo : Nat -> Nat -> Nat
gcdAlgo k j = case isLTE (S j) k of
                   (Yes prf) => boundedGCD k k j lteRefl prf
                   (No contra) =>
                      let
                        ineq = notLTEimpliesLT (S j) k contra
                      in
                        boundedGCD (S j) k j  (lteSuccLeft ineq) lteRefl

|||Given a proof that m<=n, returns n-m with proof that k = n-m<=n and
|||(Pos k)=(Pos n)+(-(Pos m) as integers
subWithBoundZ: (n: Nat) -> (m: Nat) -> (LTE m n) -> (k: Nat ** ((LTE k n),((Pos k)=(Pos n)+(-(Pos m)))))
subWithBoundZ n Z LTEZero = (n ** (lteRefl,rewrite plusZeroRightNeutralZ (Pos n) in
                                              Refl))
subWithBoundZ (S p) (S q) (LTESucc pf) = case subWithBoundZ p q pf of
                                             (x ** (pf,subpf)) =>
                                                (x ** (lteSuccRight pf,
                                                    (subSuccSuccNeutrtalZ subpf)))
|||Rewrites n = a + (-m) as a = n+ (1*m)
simpleRewrite:{n:ZZ}->{a:ZZ}->{m:ZZ}->(n= a+(-m))->(a= n +(1*m))
simpleRewrite prf {a}{n}{m} = rewrite sym $ plusZeroLeftNeutralZ a in
                        rewrite multOneLeftNeutralZ m in
                        rewrite sym $ plusNegateInverseLZ m in
                        rewrite plusCommutativeZ n m in
                        rewrite sym $ plusAssociativeZ m (-m) a in
                        rewrite plusCommutativeZ (-m) a in
                        cong (sym prf)

|||If n = a+ (-m), then gcd (m,n) = gcd (a,m)
helperboundedGCDZ:{n:ZZ}->{m:ZZ}->GCDZ m n d->
    (n= a+(-m))->GCDZ a m d
helperboundedGCDZ x prf = euclidConservesGcdWithProof {quot = (1)}  (simpleRewrite prf) x

||| Proves that Pos (k)+ (- (Pos (j)) = minusNatZ k j
simplerewrite2:{k:Nat}->{j:Nat}-> Pos (k)+ (- (Pos (j))) = minusNatZ k j
simplerewrite2 {k = k}{j = Z}= rewrite plusZeroRightNeutralZ (Pos k) in Refl
simplerewrite2 {k = k}{j = (S j)}= Refl

||| Proves that NotBothZero Z m implies (Pos m) is positive
notBothZeroZeroNatPos:{m:Nat}->NotBothZero Z m -> (IsPositive (Pos m))
notBothZeroZeroNatPos {m = (S k)} RightIsNotZero = Positive

|||A bounded GCD function that given a bound and natural numbers n and m such that
|||n and m are not both zero, returns gcd((Pos n),(Pos m)) with proof
boundedGCDZ : (bnd: Nat) -> (n: Nat) -> (m: Nat) -> (LTE n bnd) -> (LTE (S m) bnd)->
    (NotBothZero n m) -> (d:ZZ**GCDZ (Pos n) (Pos m) d)
boundedGCDZ (S b) Z m x (LTESucc y) nbz = ((Pos m)**(gcdSymZ (gcdOfZeroAndInteger (Pos m) (notBothZeroZeroNatPos nbz)) ))
boundedGCDZ (S b) (S k) Z x (LTESucc y) nbz = (Pos (S k)**gcdOfZeroAndInteger (Pos (S k)) Positive)
boundedGCDZ (S b) (S Z) (S j) (LTESucc x)  (LTESucc y) nbz = (1 **(gcdSymZ (gcdOfOneAndInteger (Pos (S j)))))
boundedGCDZ (S b) (S k) (S Z) (LTESucc x) (LTESucc y) nbz = (1 **(gcdOfOneAndInteger (Pos (S k))))
boundedGCDZ (S b) (S (S (k))) (S (S (j))) (LTESucc x) (LTESucc y) nbz =
  case isLTE j k of
        (Yes prf) => case subWithBoundZ k j prf of
                           (diff ** (pf,subpf)) => (case boundedGCDZ b (S (S j)) diff y (lteTransitive (LTESucc pf) x) LeftIsNotZero of
                             (d**gcdpf) => (d**(helperboundedGCDZ  gcdpf  (rewrite sym $simplerewrite2 {k=k}{j=j} in subpf))))
        (No contra) =>
           let
             ineq = notLTEimpliesLT j k contra
           in
             (case boundedGCDZ b (S (S j)) (S (S k)) y (lteTransitive (LTESucc (LTESucc ineq)) y) LeftIsNotZero of
               (d**gcdpf) => (d** (gcdSymZ gcdpf)))

|||A helper for bezReplace which does the rewrite as indicated in its type.
helperbezReplace:{v:ZZ}->{u:ZZ}->{j:Nat}->{diff:Nat}->{d:ZZ}->{k:Nat}->
       d =  ( u *(Pos (S (S j)))) + ( v*(Pos diff))->(Pos diff) = (Pos k )+(-(Pos j))->
         d=(u*(Pos (S (S j)))) + (v * ((Pos k) + (-(Pos j))))
helperbezReplace prf prf1 = rewrite sym $ prf1 in prf

|||A helper function for boundedGCDbez which does the rewrite as indicated in its type.
bezReplace:{v:ZZ}->{u:ZZ}->{j:Nat}->{diff:Nat}->{d:ZZ}->{k:Nat}->
       d =  ( u *(Pos (S (S j)))) + ( v*(Pos diff))->(Pos diff) = (Pos k )+(-(Pos j))->
                        d=v*(Pos (S(S k))) +(u+(-v))*(Pos (S (S j)))
bezReplace {v}{u}{j}{diff}{k} prf prf1 = rewrite plusCommutativeZ (v*(Pos (S(S k)))) ((u+(-v))*(Pos (S (S j)))) in
                                         rewrite plusCommutativeZ u (-v) in
                                         rewrite multDistributesOverPlusLeftZ  (-v) u (Pos (S (S j))) in
                                         rewrite multNegateLeftZ v (Pos (S (S j))) in
                                         rewrite sym $ multNegateRightZ v  (Pos (S (S j))) in
                                         rewrite sym $ plusAssociativeZ (v*(NegS (S j))) (u*(Pos (S (S j)))) (v*(Pos (S (S k)))) in
                                         rewrite plusCommutativeZ (u*(Pos (S (S j)))) (v*(Pos (S (S k)))) in
                                         rewrite plusAssociativeZ (v*(NegS (S j))) (v*(Pos (S (S k)))) (u*(Pos (S (S j)))) in
                                         rewrite sym $multDistributesOverPlusRightZ v (NegS (S j)) (Pos (S (S k))) in
                                         rewrite plusCommutativeZ  (v*(minusNatZ k j)) (u* (Pos (S (S j)))) in
                                         rewrite sym $ simplerewrite2 {k=k}{j=j}in
                                         helperbezReplace prf prf1

|||A bounded GCD function that given a bound and natural numbers n and m such that
|||n and m are not both zero, returns gcd((Pos n),(Pos m)) and bezout coefficients
|||with proof that it is the gcd and proof that it is a linear combination of
|||(Pos n) and (Pos m)
boundedGCDbez : (bnd: Nat) -> (n: Nat) -> (m: Nat) -> (LTE n bnd) -> (LTE (S m) bnd)->
    (NotBothZero n m) -> (d**((GCDZ (Pos n) (Pos m) d),(u:ZZ**v:ZZ**(d=(u*(Pos n))+(v*(Pos m))))))
boundedGCDbez (S b) Z m x (LTESucc y) nbz = ((Pos m)**((gcdSymZ (gcdOfZeroAndInteger (Pos m) (notBothZeroZeroNatPos nbz))),
                                                                  (0**1**(rewrite multOneLeftNeutralZ (Pos m) in Refl))))
boundedGCDbez (S b) (S k) Z x (LTESucc y) nbz = ((Pos (S k))**((gcdOfZeroAndInteger (Pos (S k)) Positive),(1**0**(   rewrite plusZeroRightNeutral k in
                                                                                rewrite plusZeroRightNeutral k in
                                                                                Refl))))
boundedGCDbez (S b) (S Z) (S j) (LTESucc x)  (LTESucc y) nbz = (1 **((gcdSymZ (gcdOfOneAndInteger (Pos (S j)))),(1**0**Refl)))
boundedGCDbez (S b) (S k) (S Z) (LTESucc x) (LTESucc y) nbz = (1 **((gcdOfOneAndInteger (Pos (S k))),(0**1**Refl)))
boundedGCDbez (S b) (S (S (k))) (S (S (j))) (LTESucc x) (LTESucc y) nbz =
  case isLTE j k of
        (Yes prf) => case subWithBoundZ k j prf of
                           (diff ** (pf,subpf)) => (case boundedGCDbez b (S (S j)) diff y (lteTransitive (LTESucc pf) x) LeftIsNotZero of
                             (d**(gcdpf,(u**v**eqpf))) => (d**((helperboundedGCDZ  gcdpf  (rewrite sym $simplerewrite2 {k=k}{j=j} in subpf)),
                                (v**(u+(-v)**( bezReplace eqpf subpf))))))
        (No contra) =>
           let
             ineq = notLTEimpliesLT j k contra
           in
             (case boundedGCDbez b (S (S j)) (S (S k)) y (lteTransitive (LTESucc (LTESucc ineq)) y) LeftIsNotZero of
               (d**(gcdpf,(u**v**eqpf))) => (d** ((gcdSymZ gcdpf), (v**u**
                                                rewrite plusCommutativeZ (v*(Pos (S (S k)) )) (u*(Pos (S (S j)) )) in
                                                  eqpf))))


text:
module Cordial.Model.Interface.PortViews

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import Cordial.Model.Common
import Cordial.Model.Specification
import Cordial.Model.Projection

import Cordial.Model.Interface.Kinds
import Cordial.Model.Interface.Ports
import Cordial.Model.Interface.PortGroup

%default total
%access public export
{-

data Necessary : (ty : OptTy)
              -> (endpoint : Endpoint)
              -> (optTy : OptionalTy)
              -> (prf : OptionalKind endpoint optTy ty)
              -> Type

-}

data SimplePort : Necessary ty endpoint opt prf -> Type where
  MkSimplePort : (type : PortTy annot labelTy)
              -> (pType : ProjectedPortTy labelTy endpoint type)
              -> (port : Port annot
                               labelTy
                               req
                               endpoint
                               endian
                               type
                               ptype)
              -> SimplePort req

data SimplePortGroup : Type where
   Empty : SimplePortGroup
   Add : (port : SimplePort req) -> (rest : SimplePortGroup) -> SimplePortGroup
   Skip : (rest : SimplePortGroup) -> SimplePortGroup

mkSimple : PortGroup annot labelTy endpoint endian ps pps
        -> SimplePortGroup
mkSimple Empty = Empty
mkSimple (Add port rest) = Add (MkSimplePort port) (mkSimple rest)
mkSimple (Skip rest) = Skip (mkSimple rest)

{-

||| A collection of ports that respects the projected port group.
|||
||| Universe that logical names arise from.
||| Are we producing/consuming information.
||| The originating projected port type that constrains the value level values.
|||
data PortGroup : (annot    : Type)
              -> (labelTy    : Type)
              -> (endpoint : Endpoint)
              -> (endian   : Maybe Endian)
              -> (ps       : PortGroupTy annot labelTy)
              -> (pportTys : DList (PortTy annot labelTy) (ProjectedPortTy labelTy endpoint) ps)
              -> Type
  where
    ||| No ports
    Empty : PortGroup annot labelTy endpoint endian Nil Nil

    ||| Add a port to the group such that the description comes from
    ||| the projected port list.
    Add  : (port : Port annot labelTy req endpoint endian (PortDesc  i k l ty f dw sen opt origin dv doc)
                                                          (PPortDesc   k l ty d dw sen req origin dv))
        -> (rest : PortGroup annot labelTy endpoint endian ps pps)
        -> PortGroup annot labelTy endpoint endian (PortDesc  i k l ty f dw sen opt origin dv doc :: ps)
                                                   (PPortDesc   k l ty d dw sen req origin dv     :: pps)

    ||| Skip an optional port from the projected port list.
    Skip : (rest : PortGroup annot labelTy endpoint endian ps pps)
        -> PortGroup annot labelTy endpoint endian (PortDesc  i k l ty f dw sen opt      origin dv doc :: ps)
                                                 (PPortDesc   k l ty d dw sen Optional origin dv     :: pps)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Hedgehog.Internal.Property

import Control.Monad.Either
import Control.Monad.Identity
import Control.Monad.Trans
import Control.Monad.Writer
import Data.DPair
import Data.Lazy
import Data.SortedMap
import Generics.Derive
import Hedgehog.Internal.Gen
import Hedgehog.Internal.Util
import Text.Show.Diff
import Text.Show.Pretty

%language ElabReflection

%default total

--------------------------------------------------------------------------------
--          Tagged Primitives
--------------------------------------------------------------------------------

public export
data Tag = ConfidenceTag
         | CoverCountTag
         | CoverPercentageTag
         | GroupNameTag
         | LabelNameTag
         | PropertyCountTag
         | PropertyNameTag
         | ShrinkCountTag
         | ShrinkLimitTag
         | TestCountTag
         | TestLimitTag

public export
record Tagged (tag : Tag) (t : Type) where
  constructor MkTagged
  unTag : t

public export %inline
Show t => Show (Tagged tag t) where
  show = show . unTag

public export %inline
Eq t => Eq (Tagged tag t) where
  (==) = (==) `on` unTag

public export %inline
Ord t => Ord (Tagged tag t) where
  compare = compare `on` unTag

public export %inline
Num t => Num (Tagged tag t) where
  fromInteger = MkTagged . fromInteger
  MkTagged x + MkTagged y = MkTagged (x + y)
  MkTagged x * MkTagged y = MkTagged (x * y)

public export %inline
FromString t => FromString (Tagged tag t) where
  fromString = MkTagged . fromString

public export %inline
Semigroup (Tagged tag Nat) where (<+>) = (+)

public export %inline
Monoid (Tagged tag Nat) where neutral = 0

||| The total number of tests which are covered by a classifier.
|||
||| Can be constructed using numeric literals.
public export
0 CoverCount : Type
CoverCount = Tagged CoverCountTag Nat

||| The name of a group of properties.
public export
0 GroupName : Type
GroupName = Tagged GroupNameTag String

||| The number of properties in a group.
public export
0 PropertyCount : Type
PropertyCount = Tagged PropertyCountTag Nat

||| The numbers of times a property was able to shrink after a failing test.
public export
0 ShrinkCount : Type
ShrinkCount = Tagged ShrinkCountTag Nat

||| The number of shrinks to try before giving up on shrinking.
|||
||| Can be constructed using numeric literals:
public export
0 ShrinkLimit : Type
ShrinkLimit = Tagged ShrinkLimitTag Nat

||| The number of tests a property ran successfully.
public export
0 TestCount : Type
TestCount = Tagged TestCountTag Nat

||| The number of successful tests that need to be run before a property test
||| is considered successful.
|||
||| Can be constructed using numeric literals.
public export
0 TestLimit : Type
TestLimit = Tagged TestLimitTag Nat

||| The name of a property.
public export
0 PropertyName : Type
PropertyName = Tagged PropertyNameTag String

||| The acceptable occurrence of false positives
|||
||| Example, `the Confidence 1000000000` would mean that
||| you'd accept a false positive
||| for 1 in 10^9 tests.
public export
record Confidence where
  constructor MkConfidence
  confidence : Bits64
  0 inBound    : confidence >= 2 = True

public export %inline
Eq Confidence where (==) = (==) `on` confidence

public export %inline
Ord Confidence where compare = compare `on` confidence

public export %inline
Show Confidence where showPrec p = showPrec p . confidence

namespace Confidence
  public export
  fromInteger :  (n : Integer)
              -> {auto 0 prf : the Bits64 (fromInteger n) >= 2 = True}
              -> Confidence
  fromInteger n = MkConfidence (fromInteger n) prf

||| The relative number of tests which are covered by a classifier.
public export
0 CoverPercentage : Type
CoverPercentage = Tagged CoverPercentageTag Double

||| The name of a classifier.
public export
0 LabelName : Type
LabelName = Tagged LabelNameTag String

--------------------------------------------------------------------------------
--          Journal
--------------------------------------------------------------------------------

||| The difference between some expected and actual value.
public export
record Diff where
  constructor MkDiff
  diffPrefix  : String
  diffRemoved : String
  diffInfix   : String
  diffAdded   : String
  diffSuffix  : String
  diffValue   : ValueDiff

%runElab derive "Hedgehog.Internal.Property.Diff" [Generic,Meta,Show,Eq]

||| Whether a test is covered by a classifier, and therefore belongs to a
||| 'Class'.
public export
data Cover = NotCovered | Covered

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

public export
Semigroup Cover where
  NotCovered <+> NotCovered = NotCovered
  _          <+> _          = Covered

public export
Monoid Cover where
  neutral = NotCovered

public export
toCoverCount : Cover -> CoverCount
toCoverCount NotCovered = 0
toCoverCount Covered    = 1

||| The extent to which a test is covered by a classifier.
|||
||| When a classifier's coverage does not exceed the required minimum, the
||| test will be failed.
public export
record Label a where
  constructor MkLabel
  labelName       : LabelName
  labelMinimum    : CoverPercentage
  labelAnnotation : a

%runElab derive "Label" [Generic,Meta,Show,Eq]

public export
Functor Label where
  map f = {labelAnnotation $= f}

public export
Foldable Label where
  foldl f a l = f a l.labelAnnotation
  foldr f a l = f l.labelAnnotation a
  null _ = False

public export
Traversable Label where
  traverse f l = (\v => {labelAnnotation := v} l) <$>
                 f l.labelAnnotation

||| This semigroup is right biased. The name, location and percentage from the
||| rightmost `Label` will be kept. This shouldn't be a problem since the
||| library doesn't allow setting multiple classes with the same 'ClassifierName'.
export
Semigroup a => Semigroup (Label a) where
  ll <+> lr = { labelAnnotation $= (ll.labelAnnotation <+>) } lr

||| Log messages which are recorded during a test run.
public export
data Log = Annotation (Lazy String)
         | Footnote (Lazy String)
         | LogLabel (Label Cover)

%runElab derive "Log" [Generic,Meta,Show,Eq]

||| A record containing the details of a test run.
public export
record Journal where
  constructor MkJournal
  journalLogs : List (Lazy Log)

%runElab derive "Journal" [Generic,Meta,Show,Eq,Semigroup,Monoid]

||| Details on where and why a test failed.
public export
record Failure where
  constructor MkFailure
  message : String
  diff    : Maybe Diff

%runElab derive "Failure" [Generic,Meta,Show,Eq]

||| The extent to which all classifiers cover a test.
|||
||| When a given classification's coverage does not exceed the required/
||| minimum, the test will be failed.
public export
record Coverage a where
  constructor MkCoverage
  coverageLabels : SortedMap LabelName (Label a)

%runElab derive "Coverage" [Generic,Meta,Show,Eq]

export
Functor Coverage where
  map f = {coverageLabels $= map (map f) }

export
Foldable Coverage where
  foldl f acc (MkCoverage sm) = foldl (foldl f) acc sm
  foldr f acc (MkCoverage sm) = foldr (\l,a => foldr f a l) acc sm
  null = null . coverageLabels

export
Traversable Coverage where
  traverse f (MkCoverage sm) = MkCoverage <$> traverse (traverse f) sm

export
Semigroup a => Semigroup (Coverage a) where
  MkCoverage c0 <+> MkCoverage c1 = MkCoverage $ c0 <+> c1

export
Semigroup a => Monoid (Coverage a) where
  neutral = MkCoverage empty

--------------------------------------------------------------------------------
--          Config
--------------------------------------------------------------------------------

public export
data TerminationCriteria =
    EarlyTermination Confidence TestLimit
  | NoEarlyTermination Confidence TestLimit
  | NoConfidenceTermination TestLimit

%runElab derive "TerminationCriteria" [Generic,Meta,Show,Eq]

public export
unCriteria : TerminationCriteria -> (Maybe Confidence, TestLimit)
unCriteria (EarlyTermination c t)      = (Just c, t)
unCriteria (NoEarlyTermination c t)    = (Just c, t)
unCriteria (NoConfidenceTermination t) = (Nothing, t)

||| Configuration for a property test.
public export
record PropertyConfig where
  constructor MkPropertyConfig
  shrinkLimit         : ShrinkLimit
  terminationCriteria : TerminationCriteria

%runElab derive "PropertyConfig" [Generic,Meta,Show,Eq]

||| The minimum amount of tests to run for a 'Property'
public export
defaultMinTests : TestLimit
defaultMinTests = 100

||| The default confidence allows one false positive in 10^9 tests
public export
defaultConfidence : Confidence
defaultConfidence = Confidence.fromInteger 1000000000

||| The default configuration for a property test.
public export
defaultConfig : PropertyConfig
defaultConfig =
  MkPropertyConfig {
      shrinkLimit = 1000
    , terminationCriteria = NoConfidenceTermination defaultMinTests
    }

--------------------------------------------------------------------------------
--          Test
--------------------------------------------------------------------------------

||| A test monad transformer allows the assertion of expectations.
public export
0 TestT : (Type -> Type) -> Type -> Type
TestT m = EitherT Failure (WriterT Journal m)

public export
0 Test : Type -> Type
Test = TestT Identity

export
mkTestT : Functor m => m (Either Failure a, Journal) -> TestT m a
mkTestT = MkEitherT . writerT

export
mkTest : (Either Failure a, Journal) -> Test a
mkTest = mkTestT . Id

export
runTestT : TestT m a -> m (Either Failure a, Journal)
runTestT = runWriterT . runEitherT

export
runTest : Test a -> (Either Failure a, Journal)
runTest = runIdentity . runTestT

||| Log some information which might be relevant to a potential test failure.
export
writeLog : Applicative m => Lazy Log -> TestT m ()
writeLog x = mkTestT $ pure (Right (), MkJournal [x])

||| Fail the test with an error message, useful for building other failure
||| combinators.
export
failWith : Applicative m => Maybe Diff -> String -> TestT m a
failWith diff msg = mkTestT $ pure (Left $ MkFailure msg diff, neutral)

||| Annotates the source code with a message that might be useful for
||| debugging a test failure.
export
annotate : Applicative m => Lazy String -> TestT m ()
annotate v = writeLog $ Annotation v

||| Annotates the source code with a value that might be useful for
||| debugging a test failure.
export covering
annotateShow : (Applicative m, Show a) => a -> TestT m ()
annotateShow v = annotate $ ppShow v

||| Logs a message to be displayed as additional information in the footer of
||| the failure report.
export
footnote : Applicative m => Lazy String -> TestT m ()
footnote v = writeLog $ Footnote v

||| Logs a value to be displayed as additional information in the footer of
||| the failure report.
export covering
footnoteShow : (Applicative m, Show a) => a -> TestT m ()
footnoteShow v = writeLog (Footnote $ ppShow v)

||| Fails with an error that shows the difference between two values.
export covering
failDiff : (Applicative m, Show a, Show b) => a -> b -> TestT m ()
failDiff x y =
  case valueDiff <$> reify x <*> reify y of
    Nothing =>
        failWith Nothing $
        unlines $ [
            "Failed"
          , "━━ lhs ━━"
          , ppShow x
          , "━━ rhs ━━"
          , ppShow y
          ]

    Just vdiff@(Same _) =>
        failWith (Just $
          MkDiff "━━━ Failed ("  "" "no differences" "" ") ━━━" vdiff) ""

    Just vdiff =>
        failWith (Just $
          MkDiff "━━━ Failed (" "- lhs" ") (" "+ rhs" ") ━━━" vdiff) ""

||| Causes a test to fail.
export
failure : Applicative m => TestT m a
failure = failWith Nothing ""

||| Another name for `pure ()`.
export
success : Monad m => TestT m ()
success = pure ()

||| Fails the test if the condition provided is 'False'.
export
assert : Monad m => Bool -> TestT m ()
assert ok = if ok then success else failure

||| Fails the test and shows a git-like diff if the comparison operation
||| evaluates to 'False' when applied to its arguments.
|||
||| The comparison function is the second argument, which may be
||| counter-intuitive to Haskell programmers. However, it allows operators to
||| be written infix for easy reading:
|||
||| This function behaves like the unix @diff@ tool, which gives a 0 exit
||| code if the compared files are identical, or a 1 exit code code
||| otherwise. Like unix @diff@, if the arguments fail the comparison, a
||| /diff is shown.
|||
export covering
diff :  (Monad m, Show a, Show b)
     => a -> (a -> b -> Bool) -> b -> TestT m ()
diff x op y = if x `op` y then success
                          else failDiff x y

infix 4 ===

||| Fails the test if the two arguments provided are not equal.
export covering
(===) : (Monad m, Eq a, Show a) => a -> a -> TestT m ()
(===) x y = diff x (==) y

infix 4 /==

||| Fails the test if the two arguments provided are equal.
export covering
(/==) : (Monad m, Eq a, Show a) => a -> a -> TestT m ()
(/==) x y = diff x (/=) y

||| Fails the test if the 'Either' is 'Left', otherwise returns the value in
||| the 'Right'.
export covering
evalEither : (Monad m, Show x) => Either x a -> TestT m a
evalEither (Left x)  = failWith Nothing (ppShow x)
evalEither (Right x) = pure x

||| Fails the test if the 'Maybe' is 'Nothing', otherwise returns the value in
||| the 'Just'.
export
evalMaybe : Monad m => Maybe a -> TestT m a
evalMaybe Nothing = failWith Nothing "the value was Nothing"
evalMaybe (Just x) = pure x

--------------------------------------------------------------------------------
--          PropertyT
--------------------------------------------------------------------------------

||| The property monad allows both the generation of test inputs
|||  and the assertion of expectations.
public export
0 PropertyT : Type -> Type
PropertyT = TestT Gen

||| Generates a random input for the test by running the provided generator.
|||
||| This is a the same as 'forAll' but allows the user to provide a custom
||| rendering function. This is useful for values which don't have a
||| 'Show' instance.
export
forAllWith : (a -> String) -> Gen a -> PropertyT a
forAllWith render gen = do x <- lift (lift gen)
                           annotate (render x)
                           pure x

||| Generates a random input for the test by running the provided generator.
export covering
forAll : Show a => Gen a -> PropertyT a
forAll = forAllWith ppShow

||| Lift a test in to a property.
export
test : Test a -> PropertyT a
test = mapEitherT $ mapWriterT (pure . runIdentity)

--------------------------------------------------------------------------------
--          Property
--------------------------------------------------------------------------------

||| A property test, along with some configurable limits like how many times
||| to run the test.
public export
record Property where
  constructor MkProperty
  config : PropertyConfig
  test   : PropertyT ()

namespace Property
  ||| Map a config modification function over a property.
  export
  mapConfig : (PropertyConfig -> PropertyConfig) -> Property -> Property
  mapConfig f p = { config $= f } p

  verifiedTermination : Property -> Property
  verifiedTermination =
    mapConfig $ \config =>
      let
        newTerminationCriteria = case config.terminationCriteria of
          NoEarlyTermination c tests    => EarlyTermination c tests
          NoConfidenceTermination tests => EarlyTermination defaultConfidence tests
          EarlyTermination c tests      => EarlyTermination c tests
      in { terminationCriteria := newTerminationCriteria } config

  ||| Adjust the number of times a property should be executed before it is considered
  ||| successful.
  export
  mapTests : (TestLimit -> TestLimit) -> Property -> Property
  mapTests f = mapConfig {terminationCriteria $= setLimit}
    where setLimit : TerminationCriteria -> TerminationCriteria
          setLimit (NoEarlyTermination c n)    = NoEarlyTermination c (f n)
          setLimit (NoConfidenceTermination n) = NoConfidenceTermination (f n)
          setLimit (EarlyTermination c n)      = EarlyTermination c (f n)

  ||| Set the number of times a property should be executed before it is considered
  ||| successful.
  |||
  ||| If you have a test that does not involve any generators and thus does not
  ||| need to run repeatedly, you can use @withTests 1@ to define a property that
  ||| will only be checked once.
  export
  withTests : TestLimit -> Property -> Property
  withTests = mapTests . const

  ||| Set the number of times a property is allowed to shrink before the test
  ||| runner gives up and prints the counterexample.
  export
  withShrinks : ShrinkLimit -> Property -> Property
  withShrinks n = mapConfig { shrinkLimit := n }

  ||| Make sure that the result is statistically significant in accordance to
  ||| the passed 'Confidence'
  export
  withConfidence : Confidence -> Property -> Property
  withConfidence c = mapConfig { terminationCriteria $= setConfidence }
    where setConfidence : TerminationCriteria -> TerminationCriteria
          setConfidence (NoEarlyTermination _ n)    = NoEarlyTermination c n
          setConfidence (NoConfidenceTermination n) = NoConfidenceTermination n
          setConfidence (EarlyTermination _ n)      = EarlyTermination c n

||| Creates a property with the default configuration.
export
property : PropertyT () -> Property
property = MkProperty defaultConfig

||| A named collection of property tests.
public export
record Group where
  constructor MkGroup
  name       : GroupName
  properties : List (PropertyName, Property)

namespace Group
  export
  mapProperty : (Property -> Property) -> Group -> Group
  mapProperty f = { properties $= map (mapSnd f) }

  ||| Map a config modification function over all
  ||| properties in a `Group`.
  export
  mapConfig : (PropertyConfig -> PropertyConfig) -> Group -> Group
  mapConfig = mapProperty . mapConfig

  ||| Set the number of times the properties in a `Group`
  ||| should be executed before they are considered
  ||| successful.
  export
  withTests : TestLimit -> Group -> Group
  withTests = mapProperty . withTests

  ||| Set the number of times the properties in a `Group`
  ||| are allowed to shrink before the test
  ||| runner gives up and prints the counterexample.
  export
  withShrinks : ShrinkLimit -> Group -> Group
  withShrinks = mapProperty . withShrinks

  ||| Make sure that the results of a `Group` are statistically
  ||| significant in accordance to the passed 'Confidence'
  export
  withConfidence : Confidence -> Group -> Group
  withConfidence = mapProperty . withConfidence

--------------------------------------------------------------------------------
--          Coverage
--------------------------------------------------------------------------------

export
coverPercentage : TestCount -> CoverCount -> CoverPercentage
coverPercentage (MkTagged tests) (MkTagged count) =
  let percentage  = the Double (cast count / cast tests * 100)
      thousandths = round {a = Double} $ percentage * 10
  in MkTagged (thousandths / 10)

export
labelCovered : TestCount -> Label CoverCount -> Bool
labelCovered tests (MkLabel _ min population) =
  coverPercentage tests population >= min

export
coverageFailures : TestCount -> Coverage CoverCount -> List $ Label CoverCount
coverageFailures tests (MkCoverage kvs) =
  filter (not . labelCovered tests) (values kvs)

||| All labels are covered
export
coverageSuccess : TestCount -> Coverage CoverCount -> Bool
coverageSuccess tests c = null $ coverageFailures tests c

||| Require a certain percentage of the tests to be covered by the
||| classifier.
|||
||| ```idris
|||    prop_with_coverage : Property
|||    prop_with_coverage =
|||      property $ do
|||        match <- forAll Gen.bool
|||        cover 30 "True" $ match
|||        cover 30 "False" $ not match
||| ```
|||
||| The example above requires a minimum of 30% coverage for both
||| classifiers. If these requirements are not met, it will fail the test.
export
cover : Monad m => CoverPercentage -> LabelName -> Bool -> TestT m ()
cover min name covered =
  let cover = if covered then Covered else NotCovered
   in writeLog $ LogLabel (MkLabel name min cover)

||| Records the proportion of tests which satisfy a given condition.
|||
||| ```idris example
|||    prop_with_classifier : Property
|||    prop_with_classifier =
|||      property $ do
|||        xs <- forAll $ Gen.list (Range.linear 0 100) Gen.alpha
|||        for_ xs $ \\x -> do
|||          classify "newborns" $ x == 0
|||          classify "children" $ x > 0 && x < 13
|||          classify "teens" $ x > 12 && x < 20
||| ```
export
classify : Monad m => LabelName -> Bool -> TestT m ()
classify name covered = cover 0 name covered

||| Add a label for each test run. It produces a table showing the percentage
||| of test runs that produced each label.
export
label : Monad m => LabelName -> TestT m ()
label name = cover 0 name True

||| Like 'label', but uses 'Show' to render its argument for display.
export
collect : (Monad m, Show a) => a -> TestT m ()
collect x = cover 0 (MkTagged $ show x) True

fromLabel : Label a -> Coverage a
fromLabel x = MkCoverage $ singleton (labelName x) x

unionsCoverage : Semigroup a => List (Coverage a) -> Coverage a
unionsCoverage = MkCoverage . concatMap coverageLabels

export
journalCoverage : Journal -> Coverage CoverCount
journalCoverage = map toCoverCount
                . unionsCoverage
                . (>>= fromLog)
                . journalLogs
  where fromLog : Lazy Log -> List (Coverage Cover)
        fromLog (LogLabel x)   = [fromLabel x]
        fromLog (Footnote _)   = []
        fromLog (Annotation _) = []

--------------------------------------------------------------------------------
--          Confidence
--------------------------------------------------------------------------------

-- not strictly true, but holds for the values we generate
-- in this module
times : InUnit -> InUnit -> InUnit
times (Element x _) (Element y _) =
  Element (x * y) (believe_me (Refl {x = True}))

oneMin : InUnit -> InUnit
oneMin (Element v _) = Element (1.0 - v) (believe_me (Refl {x = True} ))

half : InUnit -> InUnit
half = times (Element 0.5 Refl)

-- In order to get an accurate measurement with small sample sizes, we're
-- using the Wilson score interval
-- (<https://en.wikipedia.org/wiki/Binomial_proportion_confidence_interval#Wilson_score_interval wikipedia>) instead of a normal approximation interval.
wilsonBounds : Nat -> Nat -> InUnit -> (Double, Double)
wilsonBounds positives count acceptance =
  let
    p = the Double (cast positives / cast count)
    n = the Double (cast count)
    z = invnormcdf $ oneMin (half acceptance)

    midpoint = p + z * z / (2 * n)

    offset = z / (1 + z * z / n) * sqrt (p * (1 - p) / n + z * z / (4 * n * n))

    denominator = 1 + z * z / n

    low = (midpoint - offset) / denominator

    high = (midpoint + offset) / denominator
  in (low, high)

boundsForLabel : TestCount -> Confidence -> Label CoverCount -> (Double, Double)
boundsForLabel (MkTagged tests) (MkConfidence c ib) lbl =
  wilsonBounds (unTag lbl.labelAnnotation) tests (recipBits64 (Element c ib))

||| Is true when the test coverage satisfies the specified 'Confidence'
||| contstraint for all 'Coverage CoverCount's
export
confidenceSuccess : TestCount -> Confidence -> Coverage CoverCount -> Bool
confidenceSuccess tests confidence =
  all assertLow . values . coverageLabels
  where assertLow : Label CoverCount -> Bool
        assertLow cc =
          fst (boundsForLabel tests confidence cc) >=
          unTag cc.labelMinimum / 100.0

||| Is true when there exists a label that is sure to have failed according to
||| the 'Confidence' constraint
export
confidenceFailure : TestCount -> Confidence -> Coverage CoverCount -> Bool
confidenceFailure tests confidence =
  any assertHigh . values . coverageLabels
  where assertHigh : Label CoverCount -> Bool
        assertHigh cc =
          snd (boundsForLabel tests confidence cc) <
          (unTag cc.labelMinimum / 100.0)

export
multOf100 : TestCount -> Bool
multOf100 (MkTagged n) = natToInteger n `mod` 100 == 0

export
failureVerified : TestCount -> Coverage CoverCount -> Maybe Confidence -> Bool
failureVerified count cover conf =
  multOf100 count &&
  maybe False (\c => confidenceFailure count c cover) conf

export
successVerified : TestCount -> Coverage CoverCount -> Maybe Confidence -> Bool
successVerified count cover conf =
  multOf100 count &&
  maybe False (\c => confidenceSuccess count c cover) conf

export
abortEarly :  TerminationCriteria
           -> TestCount
           -> Coverage CoverCount
           -> Maybe Confidence
           -> Bool
abortEarly (EarlyTermination _ _) tests cover conf =
  let coverageReached     = successVerified tests cover conf
      coverageUnreachable = failureVerified tests cover conf
   in unTag tests >= unTag defaultMinTests &&
      (coverageReached || coverageUnreachable)

abortEarly _ _ _ _ = False


text:
module Main

import Erlang

-- Helper functions

sleep : Int -> IO ()
sleep ms = do
  pure $ erlUnsafeCall ErlTerm "timer" "sleep" [ms]
  pure ()

defaultTimeout : Int
defaultTimeout = 5000

-- Tests

testReceiveInteger : ErlPid -> IO ()
testReceiveInteger self = do
  putStrLn "testReceiveInteger"
  erlSpawnLink (do
    sleep 100
    erlSend self 42)
  result <- erlReceive defaultTimeout "not found" (map show integer)
  putStrLn result

testReceiveBinary : ErlPid -> IO ()
testReceiveBinary self = do
  putStrLn "testReceiveBinary"
  erlSpawnLink (do
    sleep 100
    erlSend self "hello")
  result <- erlReceive defaultTimeout "not found" string
  putStrLn result

testTimeout : IO ()
testTimeout = do
  putStrLn "testTimeout"
  result <- erlReceive 100 "not found" (any *> pure "found")
  putStrLn result

main : IO ()
main = do
  self <- erlSelf
  testReceiveInteger self
  testReceiveBinary self
  testTimeout


text:
natToInt : Nat -> Integer
natToInt Z = 0
natToInt (S k) = 1 + natToInt k

%builtin NaturalToInteger natToInt

lt : Nat -> Nat -> Bool
lt Z Z = False
lt Z _ = True
lt (S j) (S k) = lt j k
lt (S _) Z = False

%transform "lt" lt j k = intToBool (prim__lt_Integer (natToInt j) (natToInt k))

main : IO ()
main = do
    printLn $ natToInt 3141592
    printLn $ natToInt 12345
    printLn $ lt 100 1000
    printLn $ lt 9566 7554


text:
module Chapter4

-- enumerated types

data Direction = North | East | South | West

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

-- union types

{-
||| Represents possible shapes
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double
           -}

data Shape : Type where
  Triangle : Double -> Double -> Shape
  Rectangle : Double -> Double -> Shape
  Circle : Double -> Shape

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

-- recursive types

data Picture : Type where
  Primitive : Shape -> Picture
  Combine : Picture -> Picture -> Picture
  Rotate : Double -> Picture -> Picture
  Translate : Double -> Double -> Picture -> Picture

testPicture : Picture
testPicture = Combine (Combine (Translate 5 5 (Primitive (Rectangle 20 10)))
                               (Translate 35 5 (Primitive (Circle 5))))
                      (Translate 15 25 (Primitive (Triangle 10 10)))

pictureArea : Picture -> Double
pictureArea (Primitive s) = area s
pictureArea (Combine p1 p2) = pictureArea p1 + pictureArea p2
pictureArea (Rotate _ p) = pictureArea p
pictureArea (Translate _ _ p) = pictureArea p

-- generic types

data Biggest = NoTriangle | Size Double

biggestTriangle : Picture -> Biggest
biggestTriangle (Primitive s) = case s of
                                     t@(Triangle _ _) => Size (area t)
                                     _ => NoTriangle
biggestTriangle (Combine p1 p2) = case biggestTriangle p1 of
                                       Size d1 => case biggestTriangle p2 of
                                                       Size d2 => Size (max d1 d2)
                                                       NoTriangle => NoTriangle
                                       NoTriangle => case biggestTriangle p2 of
                                                          Size d2 => Size d2
                                                          NoTriangle => NoTriangle
biggestTriangle (Rotate _ p) = case biggestTriangle p of
                                    s@(Size _) => s
                                    _ => NoTriangle
biggestTriangle (Translate _ _ p) = case biggestTriangle p of
                                         s@(Size _) => s
                                         _ => NoTriangle

safeDivide : Double -> Double -> Maybe Double
safeDivide x y = if y == 0 then Nothing
                           else Just (x / y)

data Tree elem = Empty | Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node l v r) = case compare x v of
                             GT => Node l v (insert x r)
                             EQ => orig
                             LT => Node (insert x l) v r

data BSTree : (elem : Type) -> Type where
  BSEmpty : Ord elem => BSTree elem
  BSNode : Ord elem => (left : BSTree elem) -> (val : elem) -> (right : BSTree elem) -> BSTree elem

insertBST : elem -> BSTree elem -> BSTree elem
insertBST x BSEmpty = BSNode BSEmpty x BSEmpty
insertBST x orig@(BSNode l v r) = case compare x v of
                                    LT => BSNode (insertBST x l) v r
                                    EQ => orig
                                    GT => BSNode l v (insertBST x r)

-- dependent types

-- linear types

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:
total
notHack : Nat -> (Nat, Nat)
notHack Z = (Z, Z)
notHack (S n) = let (baz1, baz2) = notHack n
                in (baz2, S baz1)

total
hack : Nat -> (Void, Void)
hack n = let (baz1, baz2) = hack n
         in (baz1, baz2)


text:
module Postgres.Notification

import System.FFI
import Postgres.Utility
import Postgres.Data.Conn
import Postgres.Data.ResultStatus
import Postgres.DB.Core
import Postgres.DB.Wait
import Postgres.Result
import Postgres.Exec

||| Internal type representative of the libpq struct of the same
||| name.
PGnotify : Type
PGnotify = Struct "PGnotify" [("relname", (Ptr String)), ("be_pid", Int), ("extra", (Ptr String))]

public export
record Notification where
  constructor MkNotification
  channel : String
  payload : String

notificationChannel : PGnotify -> String
notificationChannel n = prim__string_value $ getField n "relname"

notificationPayload : PGnotify -> String
notificationPayload n = prim__string_value $ getField n "extra"

notification : PGnotify -> Notification
notification n = MkNotification (notificationChannel n) (notificationPayload n)

%foreign libpq "PQnotifies"
prim__dbGetNextNotification : Ptr PGconn -> PrimIO (Ptr PGnotify)

||| Takes a PGnotify struct pointer to a PGnotify struct.
||| IMPORTANT: Be sure you have checked that the struct pointer
|||    is non-null before calling this.
|||
||| NOTE: Unless you need to hold onto the PGnotify struct for longer,
|||    call the notificationStruct function instead which will take care
|||    of freeing memory for you.
%foreign helper "notify_struct"
prim__dbNotifyStruct : Ptr PGnotify -> PGnotify

%foreign libpq "PQfreemem"
prim__dbFreeNotifyStruct : Ptr PGnotify -> PrimIO ()

||| Takes a PGnotify struct pointer to a PGnotify struct.
||| IMPORTANT: Be sure you have checked that the struct pointer
|||    is non-null before calling this.
notificationStruct : HasIO io => Ptr PGnotify -> io PGnotify
notificationStruct ptr = let res = prim__dbNotifyStruct ptr in
                             do primIO $ prim__dbFreeNotifyStruct ptr
                                pure res

%foreign helper "is_null"
prim__isNullNotifyStruct : Ptr PGnotify -> Int

isNullNotification : Ptr PGnotify -> Bool
isNullNotification ptr = intToBool $ prim__isNullNotifyStruct ptr

--
-- Listen
--

||| Start listening for notifications on the given channel.
export
pgListen : (channel: String) -> Conn -> IO ResultStatus
pgListen channel conn = withExecResult conn ("LISTEN " ++ channel) (\r => pure $ pgResultStatus r)

--
-- Retrieve
--

||| Gets the next notification _of those sitting around locally_.
||| Returns `Nothing` if there are no notifications.
|||
||| See `libpq` documentation on `PQnotifies` for details on the
||| distinction between retrieving notifications from the server and
||| getting the next notification that has already been retrieved.
|||
||| NOTE: This function _does_ consume input to make sure no notification
|||  sent by the server but not processed by the client yet gets
|||  missed.
export
pgNextNotification : Conn -> IO (Maybe Notification)
pgNextNotification (MkConn conn) = do True <- pgConsumeInput (MkConn conn)
                                        | False => pure Nothing
                                      notify <- primIO $ prim__dbGetNextNotification conn
                                      if isNullNotification notify
                                         then pure $ Nothing
                                         else do derefNotify <- notificationStruct notify
                                                 pure $ Just (notification derefNotify)

--
-- Loop Retrieval
--

||| First waits for activity from server
||| then checks if there is a new notification
||| then either returns a notification or cycles
cycle : Conn -> IO Notification
cycle conn = do True <- pgWait conn
                  | False => cycle conn
                Nothing <- pgNextNotification conn
                 | Just n => pure n
                cycle conn

||| Produce a potentially infinite stream of notifications.
||| Unlike `pgNextNotificaiton`, this will wait for the server
||| to deliver a notification.
|||
||| This _is_ an infinite sequence with a blocking wait for the
||| next notification so it is of somewhat limited utility
||| compared to checking for new notifications at a natural point
||| in your programs existing logic loop unless your entire loop
||| is dictated by notification arrival anyway.
export
partial
pgNotificationStream : Conn -> Stream (IO Notification)
pgNotificationStream conn = next :: (pgNotificationStream conn) where
  next : IO Notification
  next = do Nothing <- pgNextNotification conn
             | Just n => pure n
            cycle conn

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
import CommonTestingStuff

par : Applicative m => Coop m Unit -> Coop m Unit -> Coop m Unit
par = ignore .: zip

export
main : IO Unit
main = do putStrLn "before coop"
          runCoop $ do
  offset <- currentTime
  printTime offset "start"
  par
    (forever $ do
      printTime offset "proc 1, one"
      printTime offset "proc 1, another")
    (forever $ do
      printTime offset "                     proc 2, one"
      printTime offset "                     proc 2, another")
  printTime offset "end"


text:
module Pretty

import Data.List
import Data.String

%default total

export
data Doc : Type where
  Text : String -> Doc
  Vcat : List Doc -> Doc
  Hang : Doc -> Doc -> Doc
  Indent : Doc -> Doc

public export
interface Pretty a where
  pretty : a -> Doc

export
Semigroup Doc where
  (<+>) = Hang

export
Monoid Doc where
  neutral = Text ""

export
text : String -> Doc
text = Text

export
show : Show a => a -> Doc
show = Text . show

infixr 2 $$
export
($$) : Doc -> Doc -> Doc
($$) (Vcat xs) (Vcat ys) = Vcat (xs ++ ys)
($$) x (Vcat ys) = Vcat (x :: ys)
($$) (Vcat xs) y = Vcat (xs ++ [y])
($$) x y = Vcat [x,y]

export
vcat : List Doc -> Doc
vcat = Vcat

export
vsep : List Doc -> Doc
vsep = vcat . intersperse neutral

export
punctuate : Doc -> List Doc -> Doc
punctuate sep = concat . intersperse sep

export
hsep : List Doc -> Doc
hsep = punctuate (text " ")

infixl 6 <++>
export
(<++>) : Doc -> Doc -> Doc
(<++>) x y = x <+> text " " <+> y

export
indent : Doc -> Doc
indent = Indent

export
indentBlock : List Doc -> Doc
indentBlock = indent . vcat

export
parens : Doc -> Doc
parens d = text "(" <+> d <+> text ")"

export
brackets : Doc -> Doc
brackets d = text "[" <+> d <+> text "]"

export
braces : Doc -> Doc
braces d = text "{" <+> d <+> text "}"

private
tcMap : (a -> b) -> List a -> List b
tcMap f = go []
  where
    go : List b -> List a -> List b
    go acc [] = reverse acc
    go acc (x :: xs) = go (f x :: acc) xs

private
hang : String -> List String -> List String -> List String
hang ind [] ys = ys
hang ind xs [] = xs
hang ind [x] (y :: ys) = (x ++ y) :: tcMap (ind++) ys
hang ind (x :: xs) ys = x :: hang ind xs ys

private
render' : String -> Doc -> List String
render' ind (Text s) = [s]
render' ind (Vcat ls) = assert_total $ concatMap (render' ind) ls
render' ind (Hang x y) = hang ind (render' ind x) (render' ind y)
render' ind (Indent x) = tcMap (ind++) $ render' ind x

export
render : String -> Doc -> String
render ind = fastAppend . tcMap (++"\n") . render' ind

export
Show Doc where
  show = render "  "

export
prettyShow : Pretty a => a -> String
prettyShow = render "  " . pretty


text:
plusId : (n, m, o : Nat) -> (n = m) -> (m = o) -> n + m = m + o
plusId n m o prf prf1 = rewrite prf in rewrite prf1 in Refl

mult0Plus : (n, m : Nat) -> (0 + n) * m = n * (0 + m)
mult0Plus n m = Refl

mult_S_1 : (n, m : Nat) -> (m = S n) -> m * (1 + n) = m * m
mult_S_1 n m prf = rewrite prf in Refl

andb_true_elim_2 : (b, c : Bool) -> b && c = True -> c = True
andb_true_elim_2 False False Refl impossible
andb_true_elim_2 True False Refl impossible
andb_true_elim_2 False True prf = Refl
andb_true_elim_2 True True prf = Refl

zero_nbeq_plus_1 : (n : Nat) -> 0 == (n + 1) = False
zero_nbeq_plus_1 Z = Refl
zero_nbeq_plus_1 (S k) = Refl


text:
module Data.SOP.POP

import Data.SOP.Utils
import Data.SOP.Interfaces
import Data.SOP.NP

import Decidable.Equality

%default total

||| A product of products.
|||
||| The elements of the inner products are
||| applications of the parameter f. The type POP is indexed by the list of lists
||| that determines the lengths of both the outer and all the inner products, as
||| well as the types of all the elements of the inner products.
|||
||| A POP is reminiscent of a two-dimensional table (but the inner lists can all be
||| of different length). In the context of the SOP approach to
||| generic programming, a POP is useful to represent information
||| that is available for all arguments of all constructors of a datatype.
public export
data POP_ : (k : Type) -> (f : k -> Type) -> (kss : List (List k)) -> Type where
  MkPOP : NP_ (List k) (NP_ k f) kss -> POP_ k f kss

||| Type alias for `POP_` with type parameter `k` being
||| implicit. This reflects the kind-polymorphic data type
||| in Haskell.
public export
POP : {k : Type} -> (f : k -> Type) -> (kss : List (List k)) -> Type
POP = POP_ k

public export %inline
unPOP : POP_ k f kss -> NP_ (List k) (NP_ k f) kss
unPOP (MkPOP np) = np

--------------------------------------------------------------------------------
--          Specialized Interface Functions
--------------------------------------------------------------------------------

||| Specialiced version of `hmap`
public export
mapPOP : (fun : forall a . f a -> g a) -> POP f kss -> POP g kss
mapPOP fun = MkPOP . mapNP (\p => mapNP fun p) . unPOP

||| Specialization of `hpure`.
public export
purePOP : {kss : _} -> (forall a . f a) -> POP f kss
purePOP {kss = []}     fun = MkPOP []
purePOP {kss = _ :: _} fun = let (MkPOP nps) = purePOP fun
                              in MkPOP $ pureNP fun :: nps

||| Specialization of `hap`.
public export
hapPOP : POP (\a => f a -> g a) kss -> POP f kss -> POP g kss
hapPOP (MkPOP fs) = MkPOP . hliftA2 (\p => hapNP p) fs . unPOP

||| Specialization of `hfoldl`
public export
foldlPOP : (fun : acc -> el -> acc) -> acc -> POP (K el) kss -> acc
foldlPOP _   acc (MkPOP [])     = acc
foldlPOP fun acc (MkPOP (h::t)) = foldlPOP fun (foldlNP fun acc h) (MkPOP t)

||| Specialization of `hfoldr`
public export
foldrPOP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> POP (K el) kss -> acc
foldrPOP _   acc (MkPOP [])     = acc
foldrPOP fun acc (MkPOP (h::t)) = foldrNP fun (foldrPOP fun acc (MkPOP t)) h

||| Specialization of `hsequence`
public export
sequencePOP : Applicative g => POP (\a => g (f a)) kss -> g (POP f kss)
sequencePOP = map MkPOP . sequenceNP . mapNP (\p => sequenceNP p) . unPOP

||| Specialization of `hcollapse`
public export
collapsePOP : POP (K a) kss -> (List $ List a)
collapsePOP = collapseNP . mapNP (\v => collapseNP v) . unPOP

--------------------------------------------------------------------------------
--          Interface Conversions
--------------------------------------------------------------------------------

||| This is needed to implement `Ord` below.
public export %hint
ordToEqPOP :  POP (Ord . f) kss -> POP (Eq . f) kss
ordToEqPOP = mapPOP (\_ => materialize Eq)

||| This is needed to implement `Monoid` below.
public export %hint
monoidToSemigroupPOP : POP (Monoid . f) kss -> POP (Semigroup . f) kss
monoidToSemigroupPOP = mapPOP (\_ => materialize Semigroup)

||| Converts a POP of constraints to an n-ary sum
||| holding constrains about the inner n-ary sum.
|||
||| Example : POP Eq typess -> NP (Eq . NP I) typess
|||
||| In the example above, we convert a POP of `Eq` instances
||| into an n-ary sum of Eq instances of the inner products.
||| This allows us to for instance implent `Eq (POP f kss) ` below
||| via a direct call to (==) specialized to Eq (NP (NP f) kss).
public export %hint
popToNP :  POP_ k (c . f) kss
        -> {auto prf : forall ks . NP_ k (c . f) ks => c (NP_ k f ks)}
        -> NP_ (List k) (c . NP_ k f) kss
popToNP (MkPOP nps) = hmap (\_ => prf) nps

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
HPure k (List $ List k) (POP_ k) where hpure  = purePOP

public export %inline
HFunctor k (List $ List k) (POP_ k) where hmap  = mapPOP

public export %inline
HAp k (List $ List k) (POP_ k) (POP_ k) where hap = hapPOP

public export %inline
HFold k (List $ List k) (POP_ k) where
  hfoldl = foldlPOP
  hfoldr = foldrPOP

public export %inline
HSequence k (List $ List k) (POP_ k) where hsequence = sequencePOP

public export %inline
HCollapse k (List $ List k) (POP_ k) (List . List) where
  hcollapse = collapsePOP

public export
POP (Eq . f) kss => Eq (POP_ k f kss) where
  MkPOP a == MkPOP b = a == b

public export
POP (Ord . f) kss => Ord (POP_ k f kss) where
  compare (MkPOP a) (MkPOP b) = compare a b

public export
POP (Semigroup . f) kss => Semigroup (POP_ k f kss) where
  MkPOP a <+> MkPOP b = MkPOP $ a <+> b

public export
POP (Monoid . f) kss => Monoid (POP_ k f kss) where
  neutral = MkPOP neutral

public export
POP (Show . f) kss => Show (POP_ k f kss) where
  showPrec p (MkPOP np) = showCon p "MkPOP" (show np)

private
mkPOPInjective : MkPOP a = MkPOP b -> a = b
mkPOPInjective Refl = Refl

public export
POP (DecEq . f) kss => DecEq (POP_ k f kss) where
  decEq (MkPOP a) (MkPOP b) with (decEq a b)
    decEq (MkPOP a) (MkPOP a) | Yes Refl   = Yes $ cong MkPOP Refl
    decEq (MkPOP a) (MkPOP b) | No  contra = No (contra . mkPOPInjective)


text:
%default total

namespace a


text:
module Shape_abs

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

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

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

export
circle : Double -> Shape
circle = Circle


text:
module Network.HTTP

import public Network.HTTP.Protocol
import public Network.HTTP.Message
import public Network.HTTP.Error
import public Network.HTTP.Method
import public Network.HTTP.Header
import public Network.HTTP.URL
import public Network.HTTP.Path
import public Network.HTTP.Status
import public Network.HTTP.Client
import public Network.TLS
import public Network.TLS.Signature
import public Utils.Streaming

-- needed for proving url
import public Data.String


text:
f : Nat -> Int -> Int -> Int
f (S k) m n = f k m n
f Z m n = if m == n then 0 else 1

main : IO ()
main = do
  putStrLn "hello world"
  printLn $ f 4 3 2

max_stars_repo_name: ziman/idris-scheme

max_issues_repo_name: ziman/idris-scheme

max_forks_repo_name: ziman/idris-scheme


text:
data MyCmd : Type -> Type where
  Display : String -> MyCmd ()
  Input : MyCmd String

  Pure : ty -> MyCmd ty
  (>>=) : MyCmd a -> (a -> MyCmd b) -> MyCmd b

runMyCmd : MyCmd a -> IO a
runMyCmd (Display str) = putStrLn str
runMyCmd Input = do str <- getLine
                    pure str
runMyCmd (Pure x) = pure x
runMyCmd (c >>= f) = do res <- runMyCmd c
                        runMyCmd (f res)

myCmdTest : MyCmd ()
myCmdTest = do Display "Hello"
               x <- Input
               Display x
               Pure ()


text:
||| An expression language with mechanical proof of type-safety.
|||
||| `Tupled` is an expression language supporting Let-bindings, and
||| Tuples.  Standard constructions are used to represent the language
||| as an EDSL, together with proof of progress taken from PLFA Part
||| 2.
|||
||| This module compliments Section 3 of the Functional Pearl, but does
||| not appear due to similarities with `Razor.Recorded`.
|||
module Razor.Tupled

import Razor.Common

%default total

namespace Types

  public export
  data Ty = TyInt
          | TyChar
          | TyTuple (Vect (S n) Ty)

namespace Terms

  mutual
    ||| Fields in a Tuple.
    public export
    data Fields : (g     : List Ty)
               -> (types : Vect (S n) Ty)
               -> Type
      where
        Singleton : {ty    : Ty}
                 -> (field : Tupled g ty)
                          -> Fields g (ty::Nil)

        Extend : {ty    : Ty}
              -> {tys   : Vect (S n) Ty}
              -> (field : Tupled g ty)
              -> (rest  : Fields g      tys)
                       -> Fields g (ty::tys)

    public export
    data Tupled : List Ty -> Ty -> Type where
         -- Let-Bindings & Variables
          Var : Elem ty g -> Tupled g ty

          Let : (this     : Tupled        g  expr)
             -> (beInThis : Tupled (expr::g) body)
                         -> Tupled        g  body

          -- Base Values
          I : Int  -> Tupled g TyInt
          C : Char -> Tupled g TyChar

          -- Tuples & Accessors
          MkTuple : {types : Vect (S n) Ty}
                 -> (values : Fields g          types)
                           -> Tupled g (TyTuple types)

          Proj : {types : Vect (S n) Ty}
              -> (i     : Fin (S n))
              -> (tuple : Tupled g (TyTuple types))
              -> (idx   : AtIndex i types ty)
                       -> Tupled g ty

  public export
  index : {types  : Vect (S n) Ty}
       -> (fields : Fields  g types)
       -> (idx    : AtIndex i types ty)
                 -> Tupled  g       ty
  index (Singleton field) Here = field
  index (Extend field rest) Here = field

  index (Singleton _) (There Here) impossible
  index (Singleton _) (There (There later)) impossible

  index (Extend field rest) (There later)
    = index rest later

namespace Renaming

  public export
  weaken : (Contains  old           type -> Contains  new           type)
        -> (Contains (old += type') type -> Contains (new += type') type)

  weaken func Here         = Here
  weaken func (There rest) = There (func rest)

  mutual
    namespace Fields
      public export
      rename : (forall type  . Contains old type -> Contains new type)
            -> (forall types . Fields old types -> Fields new types)
      rename f (Singleton first)  = Singleton (rename f first)
      rename f (Extend next rest) = Extend (rename f next) (rename f rest)

    public export
    rename : (forall type . Contains old type -> Contains new type)
          -> (forall type . Tupled   old type -> Tupled   new type)
    -- Let-Bindings & Variables
    rename f (Var x) = Var (f x)
    rename f (Let this beInThis) = Let (rename f this)
                                       (rename (weaken f) beInThis)

    -- Base Values
    rename f (I x) = I x
    rename f (C x) = C x

    -- Tuples & Accessors
    rename f (MkTuple values)   = MkTuple (rename f values)
    rename f (Proj i tuple idx) = Proj i (rename f tuple) idx

namespace Substitution

  public export
  weakens : (forall type . Contains  old           type -> Tupled  new           type)
         -> (forall type . Contains (old += type') type -> Tupled (new += type') type)
  weakens f Here         = Var Here
  weakens f (There rest) = rename There (f rest)

  namespace General
    mutual
      namespace Fields
        public export
        subst : (f     : forall type . Contains old type -> Tupled new type)
             -> (forall types . Fields old types -> Fields new types)
        subst f (Singleton first) = Singleton (subst f first)
        subst f (Extend next rest) = Extend (subst f next) (subst f rest)

      public export
      subst : (forall type . Contains old type -> Tupled new type)
           -> (forall type . Tupled   old type -> Tupled new type)
      -- Let-Bindings & Variables
      subst f (Var x) = f x
      subst f (Let this beInThis) = Let (subst f this)
                                        (subst (weakens f) beInThis)

      -- Base Values
      subst f (I x) = I x
      subst f (C x) = C x

      -- Tuples & Accesors
      subst f (MkTuple values)   = MkTuple (subst f values)
      subst f (Proj i tuple idx) = Proj i (subst f tuple) idx

  namespace Single
    public export
    apply : (this   : Tupled ctxt typeB)
         -> (idx    : Contains (ctxt += typeB) typeA)
                   -> Tupled ctxt typeA
    apply this Here         = this
    apply this (There rest) = Var rest

    public export
    subst : (this   : Tupled  ctxt           typeB)
         -> (inThis : Tupled (ctxt += typeB) typeA)
                   -> Tupled  ctxt           typeA
    subst {ctxt} {typeA} {typeB} this inThis = General.subst (apply this) inThis

namespace Values
  mutual
    namespace Fields
      public export
      data Value : (fields : Fields g types) -> Type
        where
          SingletonV : (field : Value v) -> Value (Singleton v)
          ExtendV : {field  : Tupled ctxt type}
                 -> {fields : Fields ctxt types}
                 -> (next : Value field)
                 -> (rest : Value fields)
                         -> Value (Extend field fields)

    public export
    data Value : Tupled ctxt type -> Type where

      -- Base Values
      IV : Value (I i)
      CV : Value (C c)

      -- Tuples
      MkTupleV : Value fields
              -> Value (MkTuple fields)

namespace Reduction

  mutual
    namespace Fields
      public export
      data Redux : (this, that : Fields g types) -> Type where
          -- Single field.
          SimplifySingleton : (prf : Redux this that)
                                  -> Redux (Singleton this) (Singleton that)

          SimplifyExtend : {this, that : Tupled ctxt type}
                        -> {rest : Fields ctxt types}
                        -> (prf : Redux this that)
                        -> Redux (Extend this rest) (Extend that rest)

          SimplifyExtendV : {this, that : Fields ctxt types}
                         -> (value      : Values.Value v)
                         -> (rest       : Fields.Redux this that)
                                       -> Redux (Extend v this) (Extend v that)

    public export
    data Redux : (this, that : Tupled ctxt type) -> Type where
      -- Let Bindings
      SimplifyLetValue : Redux this that
                      -> Redux (Let this body)
                               (Let that body)
      ReduceLetBody : Value value
                   -> Redux (Let value body)
                            (subst value body)

      SimplifyTupleR : Redux this that
                    -> Redux (MkTuple this) (MkTuple that)

      -- Accessors
      SimplifyProj : {0  labels : Vect (S n) Ty}
                  -> {   this, that : Tupled g (TyTuple labels)}
                  -> {0  idx        : AtIndex i labels ty}
                  -> Redux this that
                  -> Redux (Proj i this idx) (Proj i that idx)

      ReduceProj : {types  : Vect (S n) Ty}
                -> {fields : Fields g types}
                -> {idx    : AtIndex i types type}
                -> (values : Value fields)
                    -> Redux (Proj i (MkTuple fields) idx)
                             (index fields idx)

namespace Progress

  public export
  data Progress : (term : Tupled Nil type) -> Type where
      Done : Value term -> Progress term
      Step : {this,that : Tupled Nil type} -> (step : Redux this that) -> Progress this

  namespace Fields
    public export
    data Progress : (fields : Fields Nil types) -> Type where
      Done : (value : Value fields) -> Progress fields
      Step : {this,that : Fields Nil types} -> (step  : Redux this that) -> Progress this

  mutual
    namespace Fields
      public export
      progress : (fields : Fields Nil types) -> Progress fields
      progress (Singleton first) with (progress first)
        progress (Singleton first) | (Done x) = Done (SingletonV x)
        progress (Singleton first) | (Step prf) = Step (SimplifySingleton prf)

      progress (Extend next rest) with (progress next)
        progress (Extend next rest) | (Done x) with (progress rest)
          progress (Extend next rest) | (Done x) | (Done xs)  = Done (ExtendV x xs)
          progress (Extend next rest) | (Done x) | (Step prf) = Step (SimplifyExtendV x prf)

        progress (Extend next rest) | (Step prf) = Step (SimplifyExtend prf)

    public export
    progress : (term : Tupled Nil type) -> Progress term
    progress (Var Here) impossible

    -- Let-Bindings & Variables
    progress (Var _) impossible
    progress (Let this beInThis) with (progress this)
      progress (Let this beInThis) | (Done x) = Step (ReduceLetBody x)
      progress (Let this beInThis) | (Step prf) = Step (SimplifyLetValue prf)

    -- Base Values
    progress (I x) = Done IV
    progress (C x) = Done CV

    -- Tuples & Accessors
    progress (MkTuple values) with (progress values)
      progress (MkTuple values) | (Done v)   = Done (MkTupleV v)
      progress (MkTuple values) | (Step prf) = Step (SimplifyTupleR prf)

    progress (Proj i tuple idx) with (progress tuple)
      progress (Proj i (MkTuple fields) idx) | (Done (MkTupleV x)) = Step (ReduceProj x)
      progress (Proj i tuple idx) | (Step prf) = Step (SimplifyProj prf)

namespace Evaluation

  public export
  data Reduces : (this : Tupled ctxt type)
              -> (that : Tupled ctxt type)
              -> Type
    where
      Refl  : {this : Tupled ctxt type}
                   -> Reduces this this
      Trans : {this, that, end : Tupled ctxt type}
           -> Redux this that
           -> Reduces that end
           -> Reduces this end

  public export
  data Finished : (term : Tupled ctxt type)
                       -> Type
    where
      Normalised : {term : Tupled ctxt type} -> Value term -> Finished term
      OOF : Finished term

  public export
  data Steps : (term : Tupled Nil type) -> Type where
    MkSteps : {this, that : Tupled Nil type}
           -> (steps  : Inf (Reduces this that))
           -> (result : Finished that)
           -> Steps this

  public export
  data Fuel = Empty | More (Lazy Fuel)

  public export
  covering
  forever : Fuel
  forever = More forever

  public export
  compute : (fuel : Fuel)
         -> (term : Tupled Nil type)
         -> Steps term
  compute Empty term = MkSteps Refl OOF
  compute (More fuel) term with (progress term)
    compute (More fuel) term | (Done value) = MkSteps Refl (Normalised value)
    compute (More fuel) term | (Step step {that}) with (compute fuel that)
      compute (More fuel) term | (Step step {that = that}) | (MkSteps steps result)
        = MkSteps (Trans step steps) result

public export
covering
run : (this : Tupled Nil type)
           -> Maybe (Subset (Tupled Nil type) (Reduces this))
run this with (compute forever this)
  run this | (MkSteps steps (Normalised {term} x)) = Just (Element term steps)
  run this | (MkSteps steps OOF) = Nothing

namespace Examples
    public export
    abc : Tupled Nil (TyTuple [TyInt, TyChar, TyChar])
    abc = MkTuple (Extend (I 1) (Extend (C 'c') (Singleton (C '2'))))

    public export
    a : Tupled Nil (TyInt)
    a = Proj FZ abc Here

    public export
    b : Tupled Nil (TyChar)
    b = Proj (FS FZ) abc (There Here)

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
module Gspider.Types.RestrictedCharString

import Data.So

%access private

||| Returns true if the given list of characters `str` contains only characters specified in `chars`.
|||
||| @chars the list of permitted characters
||| @str the string to check
madeOf' : (chars : List Char) -> (str : List Char) -> Bool
madeOf' chars [] = True
madeOf' chars (x :: xs) = elem x chars && madeOf' chars xs

||| Returns true if the given string `str` contains only characters specified in `chars`.
|||
||| @chars the list of permitted characters
||| @str the string to check
export
madeOf : (chars : List Char) -> (str : String) -> Bool
madeOf chars str = madeOf' chars (unpack str)

||| Strings that are restricted to only a specific set of characters.
|||
||| @allowed the list of characters allowed in the string
public export
data RestrictedCharString : (allowed : List Char) -> Type where
  ||| Constructs a restricted character set string with the specified value.
  |||
  ||| @val the value of the string
  MkRestrictedCharString : (val : String) ->
                           {auto prf : So (madeOf allowed val)} ->
                           RestrictedCharString allowed

||| Attempts to restricts a string to contain only a specific set of characters.
|||
||| @chars the list of characters allowed in the string
||| @str the string to attempt to restrict
export
restrictStr : (chars : List Char) -> (str : String) -> Maybe (RestrictedCharString chars)
restrictStr chars str = case choose (madeOf chars str) of
  Left _ => Just (MkRestrictedCharString str)
  Right _ => Nothing

||| Converts a list of strings to a list of strings with a restricted character set, where possible.
|||
||| @chars the set of characters to use to restrict strings
||| @strs the list of strings to convert
export
convertToRestricted : (chars : List Char) -> (strs : List String) -> List (RestrictedCharString chars)
convertToRestricted chars strs = catMaybes (map (restrictStr chars) strs)

||| Converts a string restricted to containing only a specific set of characters to an unrestricted string.
|||
||| @str the string to unrestrict
export
unrestrictStr : (str : RestrictedCharString _) -> String
unrestrictStr (MkRestrictedCharString str) = str

||| Converts a list of strings containing only a specific set of characters to a list of unrestricted strings.
|||
||| @strs the list of strings to convert
export
convertFromRestricted : (strs : List (RestrictedCharString _)) -> List String
convertFromRestricted strs = map unrestrictStr strs

||| Equality for restricted character set strings.
|||
||| @x some restricted character set string
||| @y some restricted character set string
equal : (x : RestrictedCharString s) -> (y : RestrictedCharString s) -> Bool
equal (MkRestrictedCharString u) (MkRestrictedCharString v) = u == v

||| Inequality for restricted character set strings.
|||
||| @x some restricted character set string
||| @y some restricted character set string
notEqual : (x : RestrictedCharString s) -> (y : RestrictedCharString s) -> Bool
notEqual (MkRestrictedCharString u) (MkRestrictedCharString v) = u /= v

||| Implement equality for restricted character set strings.
public export
Eq (RestrictedCharString s) where
  (==) = equal
  (/=) = notEqual

||| Comparison for restricted character set strings.
|||
||| @x some restricted character set string
||| @y some restricted character set string
compare' : (x : RestrictedCharString s) -> (y : RestrictedCharString s) -> Ordering
compare' (MkRestrictedCharString u) (MkRestrictedCharString v) = compare u v

||| Implement orderability for restricted character set strings.
public export
Ord (RestrictedCharString s) where
  compare x y = compare' x y

max_stars_repo_name: sr-lab/gspider

max_issues_repo_name: sr-lab/gspider

max_forks_repo_name: sr-lab/gspider


text:
||| Shaped data.
module Data.Schema.Data

import Data.Schema.Restricted
import Data.Schema

%default total

public export
data Data : Schema n b -> Type where
 -- [ Shape ]
 --
 -- The core shape of data is that of a Rose Tree: Leaves are concrete values; and branches are nodes.
 -- We differ by loosing the restrictions on node shapes.
 --
  Leaf : (name  : n)
      -> (value : type)
      -> (prf   : Restriction type restriction value)
               -> Data (Simple (MkAtom name type restriction validType))

  Branch : (name  : n)
        -> (value : Data               complex)
                 -> Data (Complex name complex)

  Empty  : Data Empty

  -- [ Sequencing ]
  --
  -- Eat and Empty are artefacts from the total schema specification.
  -- It would be better if there is a single `Seq` constructor but alas no.

  SeqEat : (this :      Data         sthis)
        -> (that : Inf (Data               sthat))
                ->      Data (SeqEat sthis sthat)

  SeqEmpty : (this : Data           sthis)
          -> (that : Data                 sthat)
                  -> Data (SeqEmpty sthis sthat)

  -- [ Choice ]
  --
  -- This and that, may lead to noisy data when `Alt` is nested.
  --
  -- [ Q ] How to address such noisey shaped data?

  This : (this : Data sthis)
              -> Data (Alt sthis sthat)

  That : (that : Data sthat)
              -> Data (Alt sthis sthat)

-- [ EOF ]

max_stars_repo_name: jfdm/idris-shaped

max_issues_repo_name: jfdm/idris-shaped

max_forks_repo_name: jfdm/idris-shaped


text:
-- Example of a recursive type.
data MyNat = Z | S MyNat

-- Example of a union type.
||| Represents shapes.
data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its lengths and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

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

data Picture = ||| Uses the Shape type defined as the primitive.
               Primitive Shape
             | ||| Builds a picture by combining two smaller pictures.
               Combine Picture Picture
             | ||| Builds a picture by rotating another picture through an angle.
               Rotate Double Picture
             | ||| Builds a picture by moving to another location.
               Translate Double Double Picture

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

testPicture : Picture
testPicture = Combine (Translate 5 5 rectangle)
              (Combine (Translate 35 5 circle)
              (Translate 15 25 triangle))

%name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

pictureArea : Picture -> Double
pictureArea (Primitive shape) = area shape
pictureArea (Combine pic1 pic2) = pictureArea pic1 + pictureArea pic2
pictureArea (Rotate x pic) = pictureArea pic
pictureArea (Translate x y pic) = pictureArea pic

maybeMax : Ord a => Maybe a -> Maybe a -> Maybe a
maybeMax Nothing Nothing = Nothing
maybeMax Nothing (Just x) = Just x
maybeMax (Just x) Nothing = Just x
maybeMax (Just x) (Just y) = Just $ max x y

biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive tri@(Triangle x y)) = Just $ area tri
biggestTriangle (Primitive _) = Nothing
biggestTriangle (Combine pic1 pic2) = maybeMax (biggestTriangle pic1) (biggestTriangle pic2)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic