Commit a7a32655 authored by chak@cse.unsw.edu.au.'s avatar chak@cse.unsw.edu.au.
Browse files

Fixed bug in coercion for indexed data types

Mon Sep 18 19:12:51 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Fixed bug in coercion for indexed data types
  Fri Aug 25 16:45:29 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Fixed bug in coercion for indexed data types
    - Significant examples are starting to work; eg, generic finite maps:
    
    class GMapKey k where
      data GMap k :: * -> *
      empty       :: GMap k v
      lookup      :: k -> GMap k v -> Maybe v
      insert      :: k -> v -> GMap k v -> GMap k v
    
    instance GMapKey Int where
      data GMap Int v        = GMapInt (Map.Map Int v)
      empty                  = GMapInt Map.empty
      lookup k (GMapInt m)   = Map.lookup k m
      insert k v (GMapInt m) = GMapInt (Map.insert k v m)
    
    instance GMapKey Char where
      data GMap Char v        = GMapChar (GMap Int v)
      empty                   = GMapChar empty
      lookup k (GMapChar m)   = lookup (ord k) m
      insert k v (GMapChar m) = GMapChar (insert (ord k) v m)
    
    instance GMapKey () where
      data GMap () v           = GMapUnit (Maybe v)
      empty                    = GMapUnit Nothing
      lookup () (GMapUnit v)   = v
      insert () v (GMapUnit _) = GMapUnit $ Just v
    
    instance (GMapKey a, GMapKey b) => GMapKey (a, b) where
      data GMap (a, b) v            = GMapPair (GMap a (GMap b v))
      empty		                = GMapPair empty
      lookup (a, b) (GMapPair gm)   = lookup a gm >>= lookup b 
      insert (a, b) v (GMapPair gm) = GMapPair $ case lookup a gm of
    				    Nothing  -> insert a (insert b v empty) gm
    				    Just gm2 -> insert a (insert b v gm2  ) gm
    
    instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
      data GMap (Either a b) v                = GMapEither (GMap a v) (GMap b v)
      empty                                   = GMapEither empty empty
      lookup (Left  a) (GMapEither gm1  _gm2) = lookup a gm1
      lookup (Right b) (GMapEither _gm1 gm2 ) = lookup b gm2
      insert (Left  a) v (GMapEither gm1 gm2) = GMapEither (insert a v gm1) gm2
      insert (Right a) v (GMapEither gm1 gm2) = GMapEither gm1 (insert a v gm2)
    
parent 6791ad22
......@@ -340,10 +340,10 @@ mkDataInstCoercion name tvs family instTys rep_tycon
where
coArity = length tvs
rule args = (substTyWith tvs tys $ -- with sigma = [tys/tvs]
TyConApp family instTys, -- sigma (F ts)
TyConApp rep_tycon (mkTyVarTys tvs), -- :=: R tys
rest) -- surplus arguments
rule args = (substTyWith tvs tys $ -- with sigma = [tys/tvs],
TyConApp family instTys, -- sigma (F ts)
TyConApp rep_tycon tys, -- :=: R tys
rest) -- surplus arguments
where
tys = take coArity args
rest = drop coArity args
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment