content: module NameMapsPropDecorate where
  import NameMaps
  import TiPropDecorate
  --import PropSyntax(AssertionI,PredicateI)
  import NameMapsDecorate(mts)
  import TiTypes
  --import TiKinds
  import NameMapsProp()
  --import NameMapsPropStruct(bothtype,bothval)
  import HsIdent(mapHsIdent2)
  import MapDeclM
  --import MapDeclMBaseStruct()
  import MapDeclMPropStruct()
  import MUtils
  import AccList
  
  instance AccNames i (TiDecls i) where
    accNames f (Decs ds (ks,ts)) = accNames f ds . accNames f ts -- hmm, ks?
  
  instance AccNames i (TiDecl i) where
    accNames f (Dec d) = accNames f d
  
  instance AccNames i (TiExp i) where
    accNames f (Exp e) = accNames f e
    accNames f (TiSpec i _ ts) = accNames f i . accNames f ts
    accNames f (TiTyped e t) = a e . a t
      where a x = accNames f x
  
  instance AccNames i (TiAssertion i) where accNames = accNamesRec
  instance AccNames i (TiPredicate i) where accNames = accNamesRec
  
  instance AccNames i (OTiAssertion i) where
    accNames f (OA is ds pa) = accList f is . accNames f ds . accNames f pa
  
  --------------------------------------------------------------------------------
  
  instance MapNames i1 (TiDecls i1) i2 (TiDecls i2) where
    mapNames2 c f (Decs ds (ks,ts)) = Decs (m ds) (mks ks,mts c f ts)
      where
        m x = mapNames2 c f x
        mks = map mk
        mk (i:>:(k,ti)) = bothtype mapHsIdent2 f i:>:(k,m ti)
  
  instance MapNames i1 (TiDecl i1) i2 (TiDecl i2) where
    mapNames2 c f (Dec d) = Dec (mapNames2 c f d)
  
  instance MapNames i1 (TiExp i1) i2 (TiExp i2) where
    mapNames2 c f (Exp e) = Exp (mapNames2 c f e)
    mapNames2 c f (TiSpec i sc ts)= TiSpec (bothval mapHsIdent2 f i) (m sc) (m ts)
      where m x = mapNames2 c f x
    mapNames2 c f (TiTyped e t) = TiTyped (m e) (m t)
      where m x = mapNames2 c f x
  
  instance MapNames i1 (TiAssertion i1) i2 (TiAssertion i2) where
    mapNames2 = mapNames2Rec
  instance MapNames i1 (TiPredicate i1) i2 (TiPredicate i2) where
    mapNames2 = mapNames2Rec
  
  instance MapNames i1 (OTiAssertion i1) i2 (OTiAssertion i2) where
    mapNames2 c f@(vf,cf) (OA is ds pa) = OA is' ds' (m pa)
      where
         is' = map (vf (defval Pattern)) is
         ds' = [(vf (defval Local) i:>:m' t,m e)|(i:>:t,e)<-ds]
         m x = mapNames2 c f x
         m' x = mapNames2 Local f x
  
  --------------------------------------------------------------------------------
  
  instance MapDeclM (TiDecls i) (TiDecls i) where
    mapDeclM f (Decs ds dt) = flip Decs dt # mapDeclM f ds
  
  instance MapDeclM (TiDecl i) (TiDecls i) where mapDeclM  = std_mapDeclM
  
  instance MapDeclM (TiExp i) (TiDecls i) where
    mapDeclM f (Exp e) = Exp # mapDeclM f e
    mapDeclM f (TiTyped e t) = flip TiTyped t # mapDeclM f e
    mapDeclM f e@(TiSpec{}) = return e
  
  instance MapDeclM (TiAssertion i) (TiDecls i) where mapDeclM = std_mapDeclM
  instance MapDeclM (TiPredicate i) (TiDecls i) where mapDeclM = std_mapDeclM
  
  instance MapDeclM (OTiAssertion i) (TiDecls i) where
    mapDeclM f (OA is ds pa) = OA is ds # mapDeclM f pa
  