Propability.hs

{-@ LIQUID "--prune-unsorted" @-}

module Propability where

{-@ type Propability = {v:Double | ((0.0 <= v) && (v <= 1.0)) } @-}

{-@ p :: Propability @-}
p :: Double
p = 0.8

{-@ q :: Propability @-}
q :: Double
q = 1.8


data DPD k = DPD [Pair k Double]

data Pair x y = P x y
{-@ data DPD k = DPD (val::{v:[Pair k Propability]|(total v) = 1.0 }) @-}

{-@ measure total @-}
total :: [Pair k Double] -> Double
total [] = 0.0
total (x:xs) = (sndP x) + (total xs)

{-@ measure sndP @-} 
sndP :: Pair x Double -> Double
sndP (P x y) = y

dpd0 :: DPD Int
dpd0 = DPD [P 1 0.8, P 2 0.1, P 3 0.1]

dpd1 :: DPD Int
dpd1 = DPD [P 1 0.8, P 2 0.1, P 3 0.1, P 4 0.1]