From 05e0c8425d9c0ccd0c6b98f552f29c6884bef0b0 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:00:33 +0100 Subject: [PATCH 01/10] Fix build status badge --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d5c1f6d..df0b00d 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# Probability [![Build Status](https://travis-ci.org/BlackBrane/probability.svg?branch=master)](https://travis-ci.org/BlackBrane/probability) +# Probability [![Build Status](https://travis-ci.org/fieldstrength/probability.svg?branch=master)](https://travis-ci.org/fieldstrength/probability) _Probabilistic computation in Idris._ From d3523eafef58fb040d58fd460bf42390af00f1eb Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:07:52 +0100 Subject: [PATCH 02/10] Update Float type to Double --- src/Probability/Core.idr | 4 ++-- src/Probability/Display.idr | 32 ++++++++++++++++---------------- src/Probability/Utils.idr | 2 +- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/src/Probability/Core.idr b/src/Probability/Core.idr index 76d5ef5..aaa7054 100644 --- a/src/Probability/Core.idr +++ b/src/Probability/Core.idr @@ -17,7 +17,7 @@ data Probability p a = Pr (List (a,p)) ---- Types ---- Prob : Type -> Type -Prob = Probability Float +Prob = Probability Double Transition : Type -> Type -> Type Transition a b = a -> Prob b @@ -46,7 +46,7 @@ flat : List a -> Prob a flat l = let s = (1 / (cast $ length l)) in Pr $ (\x => (x,s)) <$> l -shape : List a -> List Float -> Prob a +shape : List a -> List Double -> Prob a shape xs ps = Pr $ zipWith MkPair xs (normalize ps) diff --git a/src/Probability/Display.idr b/src/Probability/Display.idr index f8e2ffe..ccb5fa0 100644 --- a/src/Probability/Display.idr +++ b/src/Probability/Display.idr @@ -7,18 +7,18 @@ import Probability.Utils %default total ||| Sets the width of terminal graph displays -width : Float +width : Double width = 30 ---- Floating Point Utils ---- -castFN : Float -> Nat +castFN : Double -> Nat castFN = cast . cast {to=Integer} -intPart : Float -> Float +intPart : Double -> Double intPart = cast . cast {to=Integer} -fracPart : Float -> Float +fracPart : Double -> Double fracPart x = x - intPart x ||| Raise a float to an arbitrary integral power @@ -38,25 +38,25 @@ tipChars = ["▉", "▎", "▏"] -tipVals : List Float +tipVals : List Double tipVals = (+ 0.0625) . (/8) . cast <$> reverse [1..7] -- = [15/16, 13/16, 11/16, 9/16, 7/16, 5/16, 3/16] -tips : List (Float,String) +tips : List (Double,String) tips = zipWith MkPair tipVals tipChars -selectTip : Float -> String +selectTip : Double -> String selectTip x = let l = filter (\p => fst p < x) tips in case l of [] => "" ((f,s)::ss) => s -bar : Float -> String +bar : Double -> String bar f = pack (replicate (castFN f) '█') ++ selectTip (fracPart f) -bars : List Float -> List String +bars : List Double -> List String bars l = let mx = foldr max 0 l in map bar $ map (* width/mx) l @@ -82,26 +82,26 @@ digit 7 = '7' digit 8 = '8' digit 9 = '9' -digAt : Float -> Integer -> Integer +digAt : Double -> Integer -> Integer digAt x i = flip mod 10 $ cast $ abs $ x / (fpow 10 i) -charAt : Float -> Integer -> Char +charAt : Double -> Integer -> Char charAt x i = digit $ digAt x i -scanUp : Float -> Integer -> Integer +scanUp : Double -> Integer -> Integer scanUp x n = if x < (fpow 10 $ n + 1) then n else scanUp x (n + 1) -scanDown : Float -> Integer -> Integer +scanDown : Double -> Integer -> Integer scanDown x n = if x > (fpow 10 $ -n) then -n else scanDown x (n + 1) -||| Find the leading digit of a Float -maxdig : Float -> Integer +||| Find the leading digit of a Double +maxdig : Double -> Integer maxdig x = if x > 1 then scanUp x 0 else scanDown x 1 ||| Show 4 digits (not necessarily significant) of a percentage -showPercent : Float -> String +showPercent : Double -> String showPercent x = let y = 100 * x s1 = pack $ (charAt y) <$> [1,0] s2 = pack $ (charAt y) <$> [-1,-2] diff --git a/src/Probability/Utils.idr b/src/Probability/Utils.idr index ff40ce8..799f57d 100644 --- a/src/Probability/Utils.idr +++ b/src/Probability/Utils.idr @@ -19,7 +19,7 @@ vecEq [] [] = True vecEq _ _ = False -normalize : List Float -> List Float +normalize : List Double -> List Double normalize l = (/ (sum l)) <$> l left : (a -> c) -> (a,b) -> (c,b) From 1e0e962ad2363ae883fbd61453950585b0c1a85f Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:08:52 +0100 Subject: [PATCH 03/10] Update last usage of Float to Double --- src/Probability/Display.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Probability/Display.idr b/src/Probability/Display.idr index ccb5fa0..3763489 100644 --- a/src/Probability/Display.idr +++ b/src/Probability/Display.idr @@ -21,10 +21,10 @@ intPart = cast . cast {to=Integer} fracPart : Double -> Double fracPart x = x - intPart x -||| Raise a float to an arbitrary integral power -fpow : Float -> Integer -> Float fpow f p = if p >= 0 then pow f (cast p) else 1 / (pow f $ cast $ abs p) +||| Raise a double to an arbitrary integral power +fpow : Double -> Integer -> Double ---- Display Bars ---- From 12848ddad6be7a7f97a466d6eeeb2a1a0098d658 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:21:34 +0100 Subject: [PATCH 04/10] Fix silly mistake introduced by last commit --- src/Probability/Display.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Probability/Display.idr b/src/Probability/Display.idr index 3763489..fe8eda1 100644 --- a/src/Probability/Display.idr +++ b/src/Probability/Display.idr @@ -21,10 +21,10 @@ intPart = cast . cast {to=Integer} fracPart : Double -> Double fracPart x = x - intPart x -fpow f p = if p >= 0 then pow f (cast p) - else 1 / (pow f $ cast $ abs p) ||| Raise a double to an arbitrary integral power fpow : Double -> Integer -> Double +fpow f p = if p >= 0 then pow f (cast p) + else 1 / (pow f $ cast $ abs p) ---- Display Bars ---- From a9d47d3fb5946ef40dab06e80743d09d3579c7e2 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:21:49 +0100 Subject: [PATCH 05/10] Bring language syntax up to date --- src/Probability/Core.idr | 15 ++++++++------- src/Probability/Examples/MontyHall.idr | 12 ++++++------ src/Probability/Monad.idr | 1 + src/Probability/Utils.idr | 1 + 4 files changed, 16 insertions(+), 13 deletions(-) diff --git a/src/Probability/Core.idr b/src/Probability/Core.idr index aaa7054..3661ae2 100644 --- a/src/Probability/Core.idr +++ b/src/Probability/Core.idr @@ -5,23 +5,24 @@ import Probability.Utils %default total +%access export + ||| Representation of a probability distribution -abstract data Probability p a = Pr (List (a,p)) -%access public - - ---- Types ---- +public export Prob : Type -> Type Prob = Probability Double +public export Transition : Type -> Type -> Type Transition a b = a -> Prob b +public export Trans : Type -> Type Trans t = Transition t t @@ -52,14 +53,14 @@ shape xs ps = Pr $ zipWith MkPair xs (normalize ps) ---- Instances ---- -instance Functor (Probability p) where +Functor (Probability p) where map f (Pr l) = Pr $ left f <$> l -instance Num p => Applicative (Probability p) where +Num p => Applicative (Probability p) where pure = certainly fm <*> m = Pr [ (f x, q*w) | (f,w) <- runProb fm, (x,q) <- runProb m ] -instance Num p => Monad (Probability p) where +Num p => Monad (Probability p) where d >>= f = Pr [ (y, q*w) | (x,w) <- runProb d, (y,q) <- runProb (f x) ] diff --git a/src/Probability/Examples/MontyHall.idr b/src/Probability/Examples/MontyHall.idr index ad18120..a9042ed 100644 --- a/src/Probability/Examples/MontyHall.idr +++ b/src/Probability/Examples/MontyHall.idr @@ -11,13 +11,13 @@ import Data.Vect data Door = One | Two | Three -instance Eq Door where +Eq Door where One == One = True Two == Two = True Three == Three = True _ == _ = False -instance Show Door where +Show Door where show One = "Door #1" show Two = "Door #2" show Three = "Door #3" @@ -47,10 +47,10 @@ score {k} v = case k of data GameScore = Score (Vect (S (S n)) Door) -instance Eq GameScore where +Eq GameScore where (Score v) == (Score w) = vecEq v w -instance Show GameScore where +Show GameScore where show (Score v) = let status = if score v then " WIN " else " LOSE " in status ++ show v @@ -58,10 +58,10 @@ instance Show GameScore where data GameOutcome = Outcome (Monty (S (S n))) -instance Eq GameOutcome where +Eq GameOutcome where (Outcome v) == (Outcome w) = score v == score w -instance Show GameOutcome where +Show GameOutcome where show (Outcome v) = if score v then " WIN " else " LOSE " diff --git a/src/Probability/Monad.idr b/src/Probability/Monad.idr index 3504244..6c6a484 100644 --- a/src/Probability/Monad.idr +++ b/src/Probability/Monad.idr @@ -3,6 +3,7 @@ module Probability.Monad %default total +%access export infixr 6 >=> (>=>) : Monad m => (a -> m b) -> (b -> m c) -> a -> m c diff --git a/src/Probability/Utils.idr b/src/Probability/Utils.idr index 799f57d..07adedc 100644 --- a/src/Probability/Utils.idr +++ b/src/Probability/Utils.idr @@ -5,6 +5,7 @@ import Data.Vect %default total +%access export infixl 5 ::~ From d9cf4fd4b192d532611e00b880426ee5f75cf577 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:28:28 +0100 Subject: [PATCH 06/10] Fix namespacing issue on pow function --- src/Probability/Display.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Probability/Display.idr b/src/Probability/Display.idr index fe8eda1..dbc05b8 100644 --- a/src/Probability/Display.idr +++ b/src/Probability/Display.idr @@ -23,8 +23,8 @@ fracPart x = x - intPart x ||| Raise a double to an arbitrary integral power fpow : Double -> Integer -> Double -fpow f p = if p >= 0 then pow f (cast p) - else 1 / (pow f $ cast $ abs p) +fpow f p = if p >= 0 then Prelude.pow f (cast p) + else 1 / (Prelude.pow f $ cast $ abs p) ---- Display Bars ---- From 5d4d46ef389cc7b2bc367e072323e6154bdee5b1 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 12:34:42 +0100 Subject: [PATCH 07/10] Change deprecated use of return to pure --- src/Probability/Monad.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Probability/Monad.idr b/src/Probability/Monad.idr index 6c6a484..94148fd 100644 --- a/src/Probability/Monad.idr +++ b/src/Probability/Monad.idr @@ -15,7 +15,7 @@ infixl 6 <=< sequ : Monad m => List (a -> m a) -> a -> m a -sequ = foldl (>=>) return +sequ = foldl (>=>) pure perform : Monad m => Nat -> (a -> m a) -> a -> m a From 76b62b43076355cadd46178c107e2a96bb53077a Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 13:59:40 +0100 Subject: [PATCH 08/10] Add travis_wait to prevent build timeout --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index ab36809..3f2e38a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,7 +1,7 @@ language: haskell install: - - cabal install idris + - travis_wait cabal install idris script: - idris --install probability.ipkg From eba6b791fa0ea4edc3203f263cb1851f7d2be3cc Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 14:32:59 +0100 Subject: [PATCH 09/10] Boost timeout to attempt to fix Travis build --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 3f2e38a..3a7e052 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,7 +1,7 @@ language: haskell install: - - travis_wait cabal install idris + - travis_wait 60 cabal install idris script: - idris --install probability.ipkg From 4fdba1dd9ae8dbfebcb135f6cf3ce996784101f5 Mon Sep 17 00:00:00 2001 From: Saul Johnson Date: Tue, 2 Jul 2019 20:54:10 +0100 Subject: [PATCH 10/10] Update Travis script to run Idris correctly --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 3a7e052..5dd1f97 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,4 +4,4 @@ install: - travis_wait 60 cabal install idris script: - - idris --install probability.ipkg + - ~/.cabal/bin/idris --install probability.ipkg