FM.hs

module FM where
import Nat

--class FiniteMap fm k | fm->k where
class FiniteMap fm where
  empty :: v -> fm v
  lookup :: fm v -> Nat -> v
  update :: Nat -> v -> fm v -> fm v

{-P:
-- Instances are expected to satisfy these properties:
property LookupUpdate =
  {| lookup, update |
       All k . All k' . All v . All fm1 . All fm2 .
       {lookup fm1 k} === {lookup fm2 k} ==>
       {lookup (update k' v fm1) k} === {lookup (update k' v fm2) k} |}

property UpdateSame =
  {| lookup, update |
       All k . All v . All fm . {lookup (update k v fm) k} === v |}

property UpdateOther =
  {| lookup, update |
        All k1 . All k2 . All v . All fm .
        -/ (k1===k2) ==>
        {lookup (update k2 v fm) k1} === {lookup fm k1} |}

-}