{-# LANGUAGE ScopedTypeVariables #-}
{-@ LIQUID "--no-termination" @-}
module Class () where
import Language.Haskell.Liquid.Prelude
{-@ class measure sz :: forall a. a -> Int @-}
{-@ class Sized s where
size :: forall a. x:s a -> {v:Nat | v = sz x}
@-}
class Sized s where
size :: s a -> Int
instance Sized [] where
{-@ instance measure sz :: [a] -> Int
sz ([]) = 0
sz (x:xs) = 1 + (sz xs)
@-}
size [] = 0
size (x:xs) = 1 + size xs
-- The following is needed to make this work (but are invariants checked?)
{- invariant {v:[a] | sz v == len v} @-}
{-@ class (Sized s) => Indexable s where
index :: forall a. x:s a -> {v:Nat | v < sz x} -> a
@-}
class (Sized s) => Indexable s where
index :: s a -> Int -> a
instance Indexable [] where
index = (!!)