content: {- |
  Module      :  ./HasCASL/DataAna.hs
  Description :  analysis of data type declarations
  Copyright   :  (c) Christian Maeder and Uni Bremen 2002-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  analyse alternatives of data types
  -}
  
  module HasCASL.DataAna
      ( DataPat (..)
      , toDataPat
      , getConstrScheme
      , getSelScheme
      , anaAlts
      , makeDataSelEqs
      , inductionScheme
      , mkVarDecl
      ) where
  
  import Common.AS_Annotation
  import Common.Id
  import Common.Result
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.Builtin
  import HasCASL.Le
  import HasCASL.TypeAna
  import HasCASL.Unify
  
  import Control.Monad
  
  import Data.Maybe (mapMaybe)
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  {- | description of polymorphic data types. The top-level identifier is
  already renamed according the IdMap. -}
  data DataPat = DataPat IdMap Id [TypeArg] RawKind Type
  
  mkVarDecl :: Id -> Type -> VarDecl
  mkVarDecl i t = VarDecl i t Other nullRange
  
  mkSelId :: Range -> String -> Int -> Int -> Id
  mkSelId p str n m = mkId
      [Token (str ++ "_" ++ (if n < 1 then "" else show n ++ "_") ++ show m) p]
  
  mkSelVar :: Int -> Int -> Type -> VarDecl
  mkSelVar n m ty = mkVarDecl (mkSelId (getRange ty) "x" n m) ty
  
  genTuple :: Int -> Int -> [Selector] -> [(Selector, VarDecl)]
  genTuple _ _ [] = []
  genTuple n m (s@(Select _ ty _) : sels) =
      (s, mkSelVar n m ty) : genTuple n (m + 1) sels
  
  genSelVars :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
  genSelVars n sels = case sels of
    [ts] -> [genTuple 0 1 ts]
    _ -> if all isSingle sels
         then map (: []) $ genTuple 0 1 $ map head sels
         else genSelVarsAux n sels
  
  genSelVarsAux :: Int -> [[Selector]] -> [[(Selector, VarDecl)]]
  genSelVarsAux _ [] = []
  genSelVarsAux n (ts : sels) =
      genTuple n 1 ts : genSelVarsAux (n + 1) sels
  
  makeSelTupleEqs :: DataPat -> Term -> [(Selector, VarDecl)] -> [Named Term]
  makeSelTupleEqs dt ct = concatMap (\ (Select mi ty p, v) -> case mi of
       Just i -> let
           sc = getSelScheme dt p ty
           eq = mkEqTerm eqId ty nullRange
                (mkApplTerm (mkOpTerm i sc) [ct]) $ QualVar v
           in [makeNamed ("ga_select_" ++ show i) eq]
       _ -> [])
  
  makeSelEqs :: DataPat -> Term -> [[(Selector, VarDecl)]] -> [Named Term]
  makeSelEqs dt = concatMap . makeSelTupleEqs dt
  
  makeAltSelEqs :: DataPat -> AltDefn -> [Named Term]
  makeAltSelEqs dt@(DataPat _ _ iargs _ _) (Construct mc ts p sels) =
      case mc of
      Nothing -> []
      Just c -> let
        selvars = genSelVars 1 sels
        vars = map (map snd) selvars
        ars = mkSelArgs vars
        ct = mkApplTerm (mkOpTerm c $ getConstrScheme dt p ts) ars
        in map (mapNamed (mkForall (map GenTypeVarDecl iargs
             ++ map GenVarDecl (concat vars)))) $ makeSelEqs dt ct selvars
  
  mkSelArgs :: [[VarDecl]] -> [Term]
  mkSelArgs = map (\ vs -> mkTupleTerm (map QualVar vs) nullRange)
  
  getConstrScheme :: DataPat -> Partiality -> [Type] -> TypeScheme
  getConstrScheme (DataPat dm _ args _ rt) p ts =
    let realTs = map (mapType dm) ts
    in TypeScheme args (getFunType rt p realTs) nullRange
  
  getSelScheme :: DataPat -> Partiality -> Type -> TypeScheme
  getSelScheme (DataPat dm _ args _ rt) p t =
    let realT = mapType dm t
    in TypeScheme args (getSelType rt p realT) nullRange
  
  -- | remove variances from generalized type arguments
  toDataPat :: DataEntry -> DataPat
  toDataPat (DataEntry im i _ args rk _) = let j = Map.findWithDefault i i im in
    DataPat im j (map nonVarTypeArg args) rk $ patToType j args rk
  
  -- | create selector equations for a data type
  makeDataSelEqs :: DataPat -> [AltDefn] -> [Named Sentence]
  makeDataSelEqs dp = map (mapNamed Formula) . concatMap (makeAltSelEqs dp)
  
  -- | analyse the alternatives of a data type
  anaAlts :: GenKind -> [DataPat] -> DataPat -> [Alternative] -> Env
          -> Result [AltDefn]
  anaAlts genKind tys dt alts te =
      do l <- mapM (anaAlt genKind tys dt te) alts
         Result (checkUniqueness $ mapMaybe ( \ (Construct i _ _ _) -> i) l)
           $ Just ()
         return l
  
  anaAlt :: GenKind -> [DataPat] -> DataPat -> Env -> Alternative
         -> Result AltDefn
  anaAlt _ _ _ te (Subtype ts _) =
      do l <- mapM (`anaStarTypeM` te) ts
         return $ Construct Nothing (Set.toList $ Set.fromList $ map snd l)
             Partial []
  anaAlt genKind tys dt te (Constructor i cs p _) =
      do newCs <- mapM (anaComps genKind tys dt te) cs
         let sels = map snd newCs
         Result (checkUniqueness . mapMaybe ( \ (Select s _ _) -> s )
                $ concat sels) $ Just ()
         return $ Construct (Just i) (map fst newCs) p sels
  
  anaComps :: GenKind -> [DataPat] -> DataPat -> Env -> [Component]
           -> Result (Type, [Selector])
  anaComps genKind tys rt te cs =
      do newCs <- mapM (anaComp genKind tys rt te) cs
         return (mkProductType $ map fst newCs, map snd newCs)
  
  isPartialSelector :: Type -> Bool
  isPartialSelector ty = case ty of
    TypeAppl (TypeName i _ _) _ -> i == lazyTypeId
    _ -> False
  
  anaComp :: GenKind -> [DataPat] -> DataPat -> Env -> Component
          -> Result (Type, Selector)
  anaComp genKind tys rt te (Selector s _ t _ _) =
      do ct <- anaCompType genKind tys rt t te
         let (p, nct) = case getTypeAppl ct of
               (TypeName i _ _, [lt]) | i == lazyTypeId
                  && isPartialSelector t -> (Partial, lt)
               _ -> (Total, ct)
         return (nct, Select (Just s) nct p)
  anaComp genKind tys rt te (NoSelector t) =
      do ct <- anaCompType genKind tys rt t te
         return (ct, Select Nothing ct Partial)
  
  anaCompType :: GenKind -> [DataPat] -> DataPat -> Type -> Env -> Result Type
  anaCompType genKind tys (DataPat _ _ tArgs _ _) t te = do
      (_, ct) <- anaStarTypeM t te
      let ds = unboundTypevars True tArgs ct
      unless (null ds) $ Result ds Nothing
      mapM_ (checkMonomorphRecursion ct te) tys
      mapM_ (rejectNegativeOccurrence genKind ct te) tys
      return $ generalize tArgs ct
  
  checkMonomorphRecursion :: Type -> Env -> DataPat -> Result ()
  checkMonomorphRecursion t te (DataPat _ i _ _ rt) =
      case filter (\ ty -> not (lesserType te ty rt || lesserType te rt ty))
         $ findSubTypes (relatedTypeIds (typeMap te) i) i t of
        [] -> return ()
        ty : _ -> Result [Diag Error ("illegal polymorphic recursion"
                                   ++ expected rt ty) $ getRange ty] Nothing
  
  findSubTypes :: (Id -> Bool) -> Id -> Type -> [Type]
  findSubTypes chk i t = case getTypeAppl t of
      (TypeName j _ _, args) -> if chk j then [t]
                                else concatMap (findSubTypes chk i) args
      (topTy, args) -> concatMap (findSubTypes chk i) $ topTy : args
  
  rejectNegativeOccurrence :: GenKind -> Type -> Env -> DataPat -> Result ()
  rejectNegativeOccurrence genKind t te (DataPat _ i _ _ _) =
      case findNegativeOccurrence te i t of
        [] -> return ()
        ty : _ -> Result [mkDiag (case genKind of
               Free -> Error
               _ -> Hint) "negative datatype occurrence of" ty] $ Just ()
  
  findNegativeOccurrence :: Env -> Id -> Type -> [Type]
  findNegativeOccurrence te i t = let tm = typeMap te in case getTypeAppl t of
      (TypeName j _ _, _) | relatedTypeIds tm i j ->
        [] -- positive occurrence
      (topTy, [larg, rarg]) | lesserType te topTy (toFunType PFunArr) ->
         findSubTypes (== i) i larg ++ findNegativeOccurrence te i rarg
      (_, args) -> concatMap (findNegativeOccurrence te i) args
  
  relatedTypeIds :: TypeMap -> Id -> Id -> Bool
  relatedTypeIds tm i1 i2 =
      not $ Set.null $ Set.intersection (allRelIds tm i1) $ allRelIds tm i2
  
  allRelIds :: TypeMap -> Id -> Set.Set Id
  allRelIds tm i = Set.union (superIds tm i) $ subIds tm i
  
  subIds :: TypeMap -> Id -> Set.Set Id
  subIds tm i = foldr ( \ j s ->
                   if Set.member i $ superIds tm j then
                        Set.insert j s else s) Set.empty $ Map.keys tm
  
  mkPredVar :: DataPat -> VarDecl
  mkPredVar (DataPat _ i _ _ rt) = let ps = posOfId i in
    mkVarDecl (if isSimpleId i then mkId [mkSimpleId $ "p_" ++ show i]
               else Id [mkSimpleId "p"] [i] ps) (predType ps rt)
  
  mkPredAppl :: DataPat -> Term -> Term
  mkPredAppl dp t = mkApplTerm (QualVar $ mkPredVar dp) [t]
  
  mkPredToVarAppl :: DataPat -> VarDecl -> Term
  mkPredToVarAppl dp = mkPredAppl dp . QualVar
  
  mkConclusion :: DataPat -> Term
  mkConclusion dp@(DataPat _ _ _ _ ty) =
    let v = mkVarDecl (mkId [mkSimpleId "x"]) ty
    in mkForall [GenVarDecl v] $ mkPredToVarAppl dp v
  
  mkPremise :: Map.Map Type DataPat -> DataPat -> AltDefn -> [Term]
  mkPremise m dp (Construct mc ts p sels) =
      case mc of
      Nothing -> []
      Just c -> let
        vars = map (map snd) $ genSelVars 1 sels
        findHypo vd@(VarDecl _ ty _ _) =
          fmap (`mkPredToVarAppl` vd) $ Map.lookup ty m
        flatVars = concat vars
        indHypos = mapMaybe findHypo flatVars
        indConcl = mkPredAppl dp
          $ mkApplTerm (mkOpTerm c $ getConstrScheme dp p ts)
          $ mkSelArgs vars
        in [mkForall (map GenVarDecl flatVars) $
            if null indHypos then indConcl else
             mkLogTerm implId nullRange (mkConjunct indHypos) indConcl]
  
  mkConjunct :: [Term] -> Term
  mkConjunct ts = if null ts then error "HasCASL.DataAna.mkConjunct" else
    toBinJunctor andId ts nullRange
  
  mkPremises :: Map.Map Type DataPat -> DataEntry -> [Term]
  mkPremises m de@(DataEntry _ _ _ _ _ alts) =
      concatMap (mkPremise m $ toDataPat de) $ Set.toList alts
  
  joinTypeArgs :: [DataPat] -> Map.Map Id TypeArg
  joinTypeArgs = foldr (\ (DataPat _ _ iargs _ _) m ->
     foldr (\ ta -> Map.insert (getTypeVar ta) ta) m iargs) Map.empty
  
  inductionScheme :: [DataEntry] -> Term
  inductionScheme des =
      let dps = map toDataPat des
          m = Map.fromList $ map (\ dp@(DataPat _ _ _ _ ty) -> (ty, dp)) dps
      in mkForall (map GenTypeVarDecl (Map.elems $ joinTypeArgs dps)
                   ++ map (GenVarDecl . mkPredVar) dps)
         $ mkLogTerm implId nullRange
           (mkConjunct $ concatMap (mkPremises m) des)
           $ mkConjunct $ map mkConclusion dps
  