module FunFM(FM,empty,lookup,update) where
import Prelude hiding (lookup)
import FM
import Nat

newtype FM v = FM (Nat->v)

--instance Eq k => FiniteMap (FM k) k where

instance FiniteMap FM where
  empty = emptyFM
  lookup = lookupFM
  update  = updateFM

emptyFM = FM . const
lookupFM (FM f) = f
updateFM k v (FM fm) = FM $ \ k' -> if k'==k then v else fm k'

{-P:
assert LookupUpdateFM = LookupUpdate lookupFM updateFM  {-#cert:LookupUpdate#-}
assert UpdateSameFM   = UpdateSame   lookupFM updateFM  {-#cert:UpdateSame#-}
assert UpdateOtherFM  = UpdateOther  lookupFM updateFM  {-#cert:UpdateOther#-}

-}