    -- |
    -- Module      :  $Header$
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE Safe #-}
    {-# LANGUAGE FlexibleInstances #-}
    module Cryptol.TypeCheck.Depends where

    import           Cryptol.ModuleSystem.Name (Name)
    import qualified Cryptol.Parser.AST as P
    import           Cryptol.Parser.Position(Range, Located(..), thing)
    import           Cryptol.Parser.Names (namesB, namesT)
    import           Cryptol.TypeCheck.Monad( InferM, recordError, getTVars
                                            , Error(..))

    import           Data.List(sortBy, groupBy)
    import           Data.Function(on)
    import           Data.Maybe(mapMaybe)
    import           Data.Graph.SCC(stronglyConnComp)
    import           Data.Graph (SCC(..))
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import qualified Data.Set as Set

    data TyDecl = TS (P.TySyn Name) | NT (P.Newtype Name)

    -- | Check for duplicate and recursive type synonyms.
    -- Returns the type-synonyms in dependency order.
    orderTyDecls :: [TyDecl] -> InferM [TyDecl]
    orderTyDecls ts =
      do vs <- getTVars
         ds <- combine $ map (toMap vs) ts
         let ordered = mkScc [ (t,[x],deps)
                                  | (x,(t,deps)) <- Map.toList (Map.map thing ds) ]
         concat `fmap` mapM check ordered

      where
      toMap vs ty@(NT (P.Newtype x as fs)) =
        ( thing x
        , x { thing = (ty, Set.toList $
                           Set.difference
                             (Set.unions (map (namesT vs . P.value) fs))
                             (Set.fromList (map P.tpName as))
                      )
            }
        )

      toMap vs ty@(TS (P.TySyn x as t)) =
            (thing x
            , x { thing = (ty, Set.toList $
                               Set.difference (namesT vs t)
                                              (Set.fromList (map P.tpName as)))
                 }
            )

      getN (TS (P.TySyn x _ _)) = thing x
      getN (NT x)               = thing (P.nName x)

      check (AcyclicSCC x) = return [x]

      -- We don't support any recursion, for now.
      -- We could support recursion between newtypes, or newtypes and tysysn.
      check (CyclicSCC xs) =
        do recordError (RecursiveTypeDecls (map getN xs))
           return [] -- XXX: This is likely to cause fake errors for missing
                     -- type synonyms. We could avoid this by, for example, checking
                     -- for recursive synonym errors, when looking up tycons.

    -- | Associate type signatures with bindings and order bindings by dependency.
    orderBinds :: [P.Bind Name] -> [SCC (P.Bind Name)]
    orderBinds bs = mkScc [ (b, map thing defs, Set.toList uses)
                          | b <- bs
                          , let (defs,uses) = namesB b
                          ]

    class FromDecl d where
      toBind    :: d -> Maybe (P.Bind Name)
      toTyDecl  :: d -> Maybe TyDecl
      isTopDecl :: d -> Bool

    instance FromDecl (P.TopDecl Name) where
      toBind (P.Decl x)         = toBind (P.tlValue x)
      toBind _                  = Nothing

      toTyDecl (P.TDNewtype d)  = Just (NT (P.tlValue d))
      toTyDecl (P.Decl x)       = toTyDecl (P.tlValue x)
      toTyDecl _                = Nothing

      isTopDecl _               = True

    instance FromDecl (P.Decl Name) where
      toBind (P.DLocated d _) = toBind d
      toBind (P.DBind b)      = return b
      toBind _                = Nothing

      toTyDecl (P.DLocated d _) = toTyDecl d
      toTyDecl (P.DType x)      = Just (TS x)
      toTyDecl _                = Nothing

      isTopDecl _               = False

    {- | Given a list of declarations, annoted with (i) the names that they
    define, and (ii) the names that they use, we compute a list of strongly
    connected components of the declarations.  The SCCs are in dependency order. -}
    mkScc :: [(a,[Name],[Name])] -> [SCC a]
    mkScc ents = stronglyConnComp $ zipWith mkGr keys ents
      where
      keys                    = [ 0 :: Integer .. ]

      mkGr i (x,_,uses)       = (x,i,mapMaybe (`Map.lookup` nodeMap) uses)

      -- Maps names to node ids.
      nodeMap                 = Map.fromList $ concat $ zipWith mkNode keys ents
      mkNode i (_,defs,_)     = [ (d,i) | d <- defs ]

    {- | Combine a bunch of definitions into a single map.  Here we check
    that each name is defined only onces. -}
    combineMaps :: [Map Name (Located a)] -> InferM (Map Name (Located a))
    combineMaps ms  =
       do mapM_ recordError $
            do m <- ms
               (x,rs) <- duplicates [ a { thing = x } | (x,a) <- Map.toList m ]
               return (RepeatedDefinitions x rs)
          return (Map.unions ms)

    {- | Combine a bunch of definitions into a single map.  Here we check
    that each name is defined only onces. -}
    combine :: [(Name, Located a)] -> InferM (Map Name (Located a))
    combine m =
      do mapM_ recordError $
          do (x,rs) <- duplicates [ a { thing = x } | (x,a) <- m ]
             return (RepeatedDefinitions x rs)
         return (Map.fromList m)

    -- | Identify multiple occurances of something.
    duplicates :: Ord a => [Located a] -> [(a,[Range])]
    duplicates = mapMaybe multiple
               . groupBy ((==) `on` thing)
               . sortBy (compare `on` thing)
      where
      multiple xs@(x : _ : _) = Just (thing x, map srcRange xs)
      multiple _              = Nothing