module Propability where
{- NIKI TO FIX:
this should be SAFE but z3 doesnot like it because
snd :: Int -> Int instead of
snd :: Int -> Real
-}
{-@ 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 [(k, Double)]
{-@ data DPD k = DPD (val::{v:[(k, Propability)]|(total v) = 1.0 }) @-}
{-@ measure total :: [(k, Double)] -> Double
total([]) = 0.0
total(x:xs) = (snd x) + (total xs)
@-}
dpd0 :: DPD Int
dpd0 = DPD [(1, 0.9), (2, 0.1)]