module Cryptol.TypeCheck.Depends where
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position(Range, Located(..), thing)
import Cryptol.TypeCheck.AST(QName)
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 | NT P.Newtype
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.tpQName 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.tpQName as)))
}
)
getN (TS (P.TySyn x _ _)) = x
getN (NT x) = P.nName x
check (AcyclicSCC x) = return [x]
check (CyclicSCC xs) =
do recordError (RecursiveTypeDecls (map getN xs))
return []
orderBinds :: [P.Bind] -> [SCC P.Bind]
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
toTyDecl :: d -> Maybe TyDecl
isTopDecl :: d -> Bool
instance FromDecl P.TopDecl 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 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
mkScc :: [(a,[QName],[QName])] -> [SCC a]
mkScc ents = stronglyConnComp $ zipWith mkGr keys ents
where
keys = [ 0 :: Integer .. ]
mkGr i (x,_,uses) = (x,i,mapMaybe (`Map.lookup` nodeMap) uses)
nodeMap = Map.fromList $ concat $ zipWith mkNode keys ents
mkNode i (_,defs,_) = [ (d,i) | d <- defs ]
combineMaps :: [Map QName (Located a)] -> InferM (Map QName (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 :: [(QName, Located a)] -> InferM (Map QName (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)
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