content: {- |
  Module      :  ./HasCASL/VarDecl.hs
  Description :  analyse var decls
  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 generic var (or type var) decls
  
  -}
  
  module HasCASL.VarDecl where
  
  import HasCASL.As
  import HasCASL.AsUtils
  import HasCASL.Builtin
  import HasCASL.ClassAna
  import HasCASL.FoldTerm
  import HasCASL.FoldType
  import HasCASL.Le
  import HasCASL.MapTerm
  import HasCASL.Merge
  import HasCASL.ParseTerm
  import HasCASL.PrintLe
  import HasCASL.TypeAna
  import HasCASL.Unify
  
  import Common.AnnoState
  import Common.DocUtils
  import Common.Id
  import Common.Lib.MapSet (setToMap)
  import Common.Lib.State
  import Common.Parsec
  import Common.Result
  
  import Text.ParserCombinators.Parsec (runParser, eof)
  
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  
  import Data.List as List
  import Data.Maybe
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  -- | quantify
  mkEnvForall :: Env -> Term -> Range -> Term
  mkEnvForall e t ps =
    let tys = getAllTypes t
        tyVs = getTypeVars (localTypeVars e) tys ps
        vs = map GenTypeVarDecl (genTypeArgs tyVs)
             ++ map GenVarDecl (Set.toList $ freeVars t)
    in if null vs then t else
           mapTerm (id, replAlias (\ i rk v ->
                 TypeName i rk $
                 case elemIndex i $ map getTypeVar tyVs of
                   Just j -> - (j + 1)
                   _ -> v))
           $ QuantifiedTerm Universal vs t ps
  
  getTypeVars :: LocalTypeVars -> [Type] -> Range -> [TypeArg]
  getTypeVars e tys ps =
    let is = Set.unions $ map (idsOf (>= 0)) tys
        tyVs = Map.intersection e $ setToMap is
        dTys = Map.foldr (\ (TypeVarDefn _ vk _ _) l -> case vk of
               Downset ty -> ty : l
               _ -> l) [] tyVs
        dis = Set.unions $ map (idsOf (>= 0)) dTys
    in if Set.isSubsetOf dis is then
            map ( \ (i, TypeVarDefn v vk rk c) -> TypeArg i v vk rk c Other ps)
            $ Map.toList tyVs
       else getTypeVars e (dTys ++ tys) ps
  
  anaStarType :: Type -> State Env (Maybe Type)
  anaStarType t = fmap (fmap snd) $ anaType (Just universe, t)
  
  anaType :: (Maybe Kind, Type)
          -> State Env (Maybe ((RawKind, Set.Set Kind), Type))
  anaType = fromResult . anaTypeM
  
  anaTypeScheme :: TypeScheme -> State Env (Maybe TypeScheme)
  anaTypeScheme (TypeScheme tArgs ty p) =
      do tvs <- gets localTypeVars    -- save global variables
         mArgs <- mapM anaddTypeVarDecl tArgs
         let newArgs = catMaybes mArgs
         mt <- anaStarType ty
         case mt of
             Nothing -> do putLocalTypeVars tvs       -- forget local variables
                           return Nothing
             Just newTy -> do
                 let newSc = TypeScheme newArgs newTy p
                 gTy <- generalizeS newSc
                 putLocalTypeVars tvs       -- forget local variables
                 return $ Just gTy
  
  generalizeS :: TypeScheme -> State Env TypeScheme
  generalizeS sc@(TypeScheme tArgs ty p) = do
      let fvs = freeTVars ty
          svs = sortBy comp fvs
          comp a b = compare (fst a) $ fst b
      tvs <- gets localTypeVars
      let newArgs = map ( \ (_, (i, _)) -> case Map.lookup i tvs of
                    Nothing -> error "generalizeS"
                    Just (TypeVarDefn v vk rk c) ->
                        TypeArg i v vk rk c Other nullRange) svs
          newSc = TypeScheme (genTypeArgs newArgs) (generalize newArgs ty) p
      if null tArgs then return newSc
         else do
           addDiags $ generalizable False sc
           return newSc
  
  -- | store type id and check kind arity (warn on redeclared types)
  addTypeId :: Bool -> TypeDefn -> Kind -> Id -> State Env Bool
  addTypeId warn dfn k i = do
      tvs <- gets localTypeVars
      case Map.lookup i tvs of
          Just _ -> do
              when warn $ addDiags [mkDiag Warning
                                    "new type shadows type variable" i]
              putLocalTypeVars $ Map.delete i tvs
          Nothing -> return ()
      cm <- gets classMap
      case Map.lookup i cm of
        Just _ -> do
            addDiags [mkDiag Error "class name used as type" i]
            return False
        Nothing -> addTypeKind warn dfn i k
  
  -- | check if the kind only misses variance indicators of the known raw kind
  isLiberalKind :: ClassMap -> Bool -> RawKind -> Kind -> Maybe Kind
  isLiberalKind cm b ok k = case ok of
      ClassKind _ -> Just k
      FunKind ov fok aok _ -> case k of
          FunKind v fk ak ps -> do
              nfk <- isLiberalKind cm (not b) fok fk
              nak <- isLiberalKind cm b aok ak
              return $ FunKind (liberalVariance b ov v) nfk nak ps
          ClassKind i -> case Map.lookup i cm of
             Just ci -> maybe Nothing (const $ Just k) $ minRawKind "" ok
                        $ rawKind ci
             _ -> Nothing
  
  liberalVariance :: Bool -> Variance -> Variance -> Variance
  liberalVariance b v1 v2 = if b then minVariance v1 v2 else
         revVariance $ minVariance (revVariance v1) $ revVariance v2
  
  -- | lifted 'anaKindM'
  anaKind :: Kind -> State Env RawKind
  anaKind k = do
      mrk <- fromResult $ anaKindM k . classMap
      case mrk of
        Nothing -> error "anaKind"
        Just rk -> return rk
  
  -- | store type as is (warn on redeclared types)
  addTypeKind :: Bool -> TypeDefn -> Id -> Kind -> State Env Bool
  addTypeKind warn d i k = do
    e <- get
    rk <- anaKind k
    let tm = typeMap e
        cm = classMap e
        addTypeSym = unless (Map.member i bTypes)
                          . addSymbol . idToTypeSymbol i
    unless (placeCount i <= kindArity rk)
      $ addDiags [mkDiag Error "wrong arity of" i]
    case Map.lookup i tm of
      Nothing -> do
        addTypeSym rk
        putTypeMap $ Map.insert i (TypeInfo rk (Set.singleton k) Set.empty d) tm
        return True
      Just (TypeInfo ok oldks sups dfn) ->
        case minRawKind "" ok rk of
        Nothing -> do
          addDiags $ diffKindDiag i ok rk
          return False
        Just r -> case isLiberalKind cm True r k of
         Just nk -> do
          let isNewInst = newKind cm nk oldks
              insts = if isNewInst then addNewKind cm nk oldks else oldks
              Result ds mDef = mergeTypeDefn dfn d
          when (warn && not isNewInst && case (dfn, d) of
             (PreDatatype, DatatypeDefn _) -> False
             _ -> True)
            $ addDiags [mkDiag Hint "redeclared type" i]
          case mDef of
            Just newDefn -> do
              addTypeSym r
              putTypeMap $ Map.insert i (TypeInfo r insts sups newDefn) tm
              return True
            _ -> do
              addDiags $ map (improveDiag i) ds
              return False
         Nothing -> do
           addDiags [mkDiag Error "cannot refine kind" i]
           return False
  
  nonUniqueKind :: (GetRange a, Pretty a) => Set.Set Kind -> RawKind -> a ->
                   (Kind -> State Env (Maybe b)) -> State Env (Maybe b)
  nonUniqueKind ks rk a f = case Set.toList ks of
      [k] -> f k
      _ -> do
        addDiags [mkDiag Warning "non-unique kind for" a]
        f (rawToKind rk)
  
  -- | analyse a type argument
  anaddTypeVarDecl :: TypeArg -> State Env (Maybe TypeArg)
  anaddTypeVarDecl (TypeArg i v vk _ _ s ps) = do
    cm <- gets classMap
    case Map.lookup i cm of
      Just _ -> do
          addDiags [mkDiag Error "class used as type variable" i]
          return Nothing
      Nothing -> do
       c <- toEnvState inc
       case vk of
        VarKind k ->
          let Result ds (Just rk) = anaKindM k cm
          in if null ds then do
              addLocalTypeVar True (TypeVarDefn v vk rk c) i
              return $ Just $ TypeArg i v vk rk c s ps
          else do addDiags ds
                  return Nothing
        Downset t -> do
          mt <- anaType (Nothing, t)
          case mt of
              Nothing -> return Nothing
              Just ((rk, ks), nt) ->
                  nonUniqueKind ks rk t $ \ k -> do
                     let nd = Downset (KindedType nt (Set.singleton k) nullRange)
                     addLocalTypeVar True (TypeVarDefn NonVar nd rk c) i
                     return $ Just $ TypeArg i v (Downset nt) rk c s ps
        MissingKind -> do
          tvs <- gets localTypeVars
          case Map.lookup i tvs of
              Nothing -> do
                  addDiags [mkDiag Error "unknown type variable" i]
                  let dvk = VarKind universe
                  addLocalTypeVar True (TypeVarDefn v dvk rStar c) i
                  return $ Just $ TypeArg i v dvk rStar c s ps
              Just (TypeVarDefn v0 dvk rk _) -> do
                  addLocalTypeVar False (TypeVarDefn v0 dvk rk c) i
                  return $ Just $ TypeArg i v0 dvk rk c s ps
  
  -- | partition information of an uninstantiated identifier
  partitionOpId :: Env -> Id -> TypeScheme -> (Set.Set OpInfo, Set.Set OpInfo)
  partitionOpId e i sc =
      Set.partition ((sc ==) . opType)
             $ Map.findWithDefault Set.empty i $ assumps e
  
  checkUnusedTypevars :: TypeScheme -> State Env TypeScheme
  checkUnusedTypevars sc@(TypeScheme tArgs t ps) = do
      let ls = map (fst . snd) $ leaves (< 0) t -- generic vars
          rest = map getTypeVar tArgs List.\\ ls
      unless (null rest)
        $ addDiags [Diag Warning ("unused type variables: "
                                  ++ show (ppWithCommas rest)) ps]
      return sc
  
  checkPlaceCount :: Env -> Id -> TypeScheme -> [Diagnosis]
  checkPlaceCount e i (TypeScheme _ ty _) =
      if placeCount i > 1 then
          let (fty, fargs) = getTypeAppl ty in
          if length fargs == 2 && lesserType e fty (toFunType PFunArr) then
              let (pty, ts) = getTypeAppl (head fargs)
                  n = length ts in
              if n > 1 && lesserType e pty (toProdType n nullRange) then
                      [mkDiag Warning "wrong number of places in" i
                      | placeCount i /= n ]
              else [mkDiag Warning "expected tuple argument for" i]
          else [mkDiag Warning "expected function type for" i]
      else []
  
  -- | storing an operation
  addOpId :: Id -> TypeScheme -> Set.Set OpAttr -> OpDefn -> State Env Bool
  addOpId i oldSc attrs dfn = do
      sc@(TypeScheme _ ty _) <- checkUnusedTypevars oldSc
      e <- get
      let as = assumps e
          bs = binders e
          ds = checkPlaceCount e i sc
          (l, r) = partitionOpId e i sc
          oInfo = OpInfo sc attrs dfn
          Result es mo = foldM mergeOpInfo oInfo $ Set.toList l
      addDiags ds
      addDiags $ map (improveDiag i) es
      if i `elem` map fst bList then
        addDiags [mkDiag Warning "ignoring declaration for builtin identifier" i]
        else unless (Set.null l) $ addDiags
        [mkDiag Hint ("repeated declaration of '" ++ showId i "' with type") ty]
      when (Map.member i bs) $ do
        addDiags [mkDiag Warning "identifier shadows binder" i]
        putBinders $ Map.delete i bs
      case mo of
        Nothing -> return False
        Just oi -> do
          addSymbol $ idToOpSymbol i $ opType oi
          putAssumps $ Map.insert i (Set.insert oi r) as
          return True
  
  -- | add a local variable with an analysed type (if True then warn)
  addLocalVar :: Bool -> VarDecl -> State Env ()
  addLocalVar warn (VarDecl v t _ _) =
      do e <- get
         let vs = localVars e
         when warn $ do
           when (Map.member v $ assumps e)
             $ addDiags [mkDiag Hint "variable shadows global name(s)" v]
           when (Map.member v vs)
             $ addDiags [mkDiag Hint "rebound variable" v]
           when (Map.member v $ localTypeVars e)
             $ addDiags [mkDiag Warning "variable also known as type variable" v]
         putLocalVars $ Map.insert v (VarDefn t) vs
  
  -- | add analysed local variable or type variable declaration
  addGenVarDecl :: GenVarDecl -> State Env ()
  addGenVarDecl (GenVarDecl v) = addLocalVar True v
  addGenVarDecl (GenTypeVarDecl t) = addTypeVarDecl False t
  
  -- | analyse and add local variable or type variable declaration
  anaddGenVarDecl :: Bool -> GenVarDecl -> State Env (Maybe GenVarDecl)
  anaddGenVarDecl warn gv = case gv of
      GenVarDecl v -> optAnaddVarDecl warn v
      GenTypeVarDecl t -> fmap (fmap GenTypeVarDecl) $ anaddTypeVarDecl t
  
  convTypeToKind :: Type -> Maybe (Variance, Kind)
  convTypeToKind ty = let s = showDoc ty "" in
      case runParser (extKind << eof) (emptyAnnos ()) "" s of
      Right (v, k) -> Just (v, k)
      _ -> Nothing
  
  convertTypeToKind :: Env -> Type -> Result (Variance, Kind)
  convertTypeToKind e ty = case convTypeToKind ty of
      Just (v, k) -> let Result ds _ = anaKindM k $ classMap e in
                 if null ds then return (v, k) else Result ds Nothing
      _ -> Fail.fail $ "not a kind '" ++ showDoc ty "'"
  
  -- | local variable or type variable declaration
  optAnaddVarDecl :: Bool -> VarDecl -> State Env (Maybe GenVarDecl)
  optAnaddVarDecl warn vd@(VarDecl v t s q) =
      let varDecl = do mvd <- anaVarDecl vd
                       case mvd of
                           Nothing -> return Nothing
                           Just nvd -> do
                               let movd = makeMonomorph nvd
                               addLocalVar warn movd
                               return $ Just $ GenVarDecl movd
      in if isSimpleId v then
      do e <- get
         let Result ds mk = convertTypeToKind e t
         case mk of
             Just (vv, k) -> do
                 addDiags [mkDiag Hint "is type variable" v]
                 tv <- anaddTypeVarDecl $ TypeArg v vv (VarKind k) rStar 0 s q
                 return $ fmap GenTypeVarDecl tv
             _ -> do addDiags $ map ( \ d -> Diag Hint (diagString d) q) ds
                     varDecl
      else varDecl
  
  makeMonomorph :: VarDecl -> VarDecl
  makeMonomorph (VarDecl v t sk ps) = VarDecl v (monoType t) sk ps
  
  monoType :: Type -> Type
  monoType = foldType mapTypeRec
    { foldTypeName = \ t i k n -> if n > 0 then TypeName i k 0 else t }
  
  -- | analyse variable declaration
  anaVarDecl :: VarDecl -> State Env (Maybe VarDecl)
  anaVarDecl (VarDecl v oldT sk ps) =
      do mt <- anaStarType oldT
         return $ case mt of
                 Nothing -> Nothing
                 Just t -> Just $ VarDecl v t sk ps
  