hets/HasCASL/DataAna.hs

	DataAna.hs revision e774ab5733a1d673b123b0e63b14dd533e6fd4fc
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule      :  $Header$
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright   :  (c) Christian Maeder and Uni Bremen 2002-2003
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer  :  hets@tzi.de
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability   :  provisional
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability :  non-portable (MonadState)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannanalyse alternatives of data types
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule HasCASL.DataAna where
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.As
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Id
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Lib.State
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Result
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.Le
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.TypeAna
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HasCASL.Unify
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.Maybe
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.List
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaAlts :: Type -> [Alternative] -> State Env [AltDefn]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaAlts dt alts = do ll <- mapM (anaAlt dt) alts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann             let l = concat ll
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann             addDiags (checkUniqueness $ map
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann                    ( \ (Construct i _ _ _) -> i) l)
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann             return l
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaAlt :: Type -> Alternative -> State Env [AltDefn]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaAlt _ (Subtype ts ps) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann    do mapM_ anaStarType ts
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann       addDiags [Diag Warning "data subtype ignored" $ firstPos ts ps]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann       return []
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannanaAlt dt (Constructor i cs p _) =
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann    do newCs <- mapM (anaComp i dt) $ zip cs $ map (:[]) [1..]
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann       let mts = map fst newCs
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann       if all isJust mts then
6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann      do let sels = concatMap snd newCs
         con = Construct i (catMaybes mts) p sels
         -- check for disjoint selectors
         addDiags (checkUniqueness $ map ( \ (Select s _ _) -> s ) sels)
         return [con]
      else return []

getConstrType :: Type -> Partiality -> [Type] -> Type
getConstrType dt p = addPartiality p .
               foldr ( \ c r -> FunType c FunArr r [] ) dt


addPartiality :: Partiality -> Type -> Type
addPartiality Total t = t
addPartiality Partial t = makePartial t

makePartial :: Type -> Type
makePartial t =
    case t of
       FunType t1 a t2 ps ->
           case t2 of
               FunType _ _ _ _ -> FunType t1 a (makePartial t2) ps
               _ -> FunType t1 PFunArr t2 ps
       _ -> LazyType t []

anaComp :: Id -> Type -> (Components, [Int])
    -> State Env (Maybe Type, [Selector])
anaComp _ rt (Selector s p t _ _, _) =
    do mt <- anaCompType rt t
       case mt of
           Just ct -> return (mt, [Select s ct p])
       _ -> return (Nothing, [])
anaComp con rt (NoSelector t, i) =
    do mt <- anaCompType rt t
       case mt of
           Just ct -> return (mt, [Select (simpleIdToId $ mkSimpleId
               ("%(" ++ showPretty rt "." ++
                showId con ".sel_" ++ show i ++ ")%"))
                   ct Partial])
       _ -> return  (Nothing, [])

anaComp con rt (NestedComponents cs ps, i) =
    do newCs <- mapM (anaComp con rt) $ zip cs $ map (:i) [1..]
       let mts = map fst newCs
       if all isJust mts then
      return (Just $ ProductType (catMaybes mts) ps,
          concatMap snd newCs)
      else return  (Nothing, [])

getSelType :: Type -> Partiality -> Type -> Type
getSelType dt p rt = addPartiality p $ FunType dt FunArr rt []

anaCompType :: Type -> Type -> State Env (Maybe Type)
anaCompType dt t = do
    mt <- anaStarType t
    case mt of
        Nothing -> return Nothing
        Just ct -> unboundTypevars (varsOf dt) ct

unboundTypevars :: [TypeArg] -> Type -> State Env (Maybe Type)
unboundTypevars args ct = do
    let restVars = varsOf ct \\ args
    if null restVars then do return $ Just ct
       else do addDiags [Diag Error ("unbound type variable(s)\n\t"
                     ++ showSepList ("," ++) showPretty
                     restVars "") $ posOf restVars]
           return Nothing