module Cryptol.IR.FreeVars
  ( FreeVars(..)
  , Deps(..)
  , Defs(..)
  , moduleDeps, transDeps
  ) where

import           Data.Set ( Set )
import qualified Data.Set as Set
import           Data.Map ( Map )
import qualified Data.Map as Map

import Cryptol.TypeCheck.AST
import Cryptol.Utils.RecordMap

data Deps = Deps { Deps -> Set Name
valDeps  :: Set Name
                   -- ^ Undefined value names

                 , Deps -> Set Name
tyDeps   :: Set Name
                   -- ^ Undefined type names (from newtype)

                 , Deps -> Set TParam
tyParams :: Set TParam
                   -- ^ Undefined type params (e.d. mod params)
                 } deriving Deps -> Deps -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Deps -> Deps -> Bool
$c/= :: Deps -> Deps -> Bool
== :: Deps -> Deps -> Bool
$c== :: Deps -> Deps -> Bool
Eq

instance Semigroup Deps where
  Deps
d1 <> :: Deps -> Deps -> Deps
<> Deps
d2 = forall a. Monoid a => [a] -> a
mconcat [Deps
d1,Deps
d2]

instance Monoid Deps where
  mempty :: Deps
mempty = Deps { valDeps :: Set Name
valDeps   = forall a. Set a
Set.empty
                , tyDeps :: Set Name
tyDeps    = forall a. Set a
Set.empty
                , tyParams :: Set TParam
tyParams  = forall a. Set a
Set.empty
                }

  mappend :: Deps -> Deps -> Deps
mappend = forall a. Semigroup a => a -> a -> a
(<>)

  mconcat :: [Deps] -> Deps
mconcat [Deps]
ds = Deps { valDeps :: Set Name
valDeps   = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map Deps -> Set Name
valDeps [Deps]
ds)
                    , tyDeps :: Set Name
tyDeps    = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map Deps -> Set Name
tyDeps  [Deps]
ds)
                    , tyParams :: Set TParam
tyParams  = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (forall a b. (a -> b) -> [a] -> [b]
map Deps -> Set TParam
tyParams [Deps]
ds)
                    }

rmTParam :: TParam -> Deps -> Deps
rmTParam :: TParam -> Deps -> Deps
rmTParam TParam
p Deps
x = Deps
x { tyParams :: Set TParam
tyParams = forall a. Ord a => a -> Set a -> Set a
Set.delete TParam
p (Deps -> Set TParam
tyParams Deps
x) }

rmVal :: Name -> Deps -> Deps
rmVal :: Name -> Deps -> Deps
rmVal Name
p Deps
x = Deps
x { valDeps :: Set Name
valDeps = forall a. Ord a => a -> Set a -> Set a
Set.delete Name
p (Deps -> Set Name
valDeps Deps
x) }

rmVals :: Set Name -> Deps -> Deps
rmVals :: Set Name -> Deps -> Deps
rmVals Set Name
p Deps
x = Deps
x { valDeps :: Set Name
valDeps = forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Deps -> Set Name
valDeps Deps
x) Set Name
p }


-- | Compute the transitive closure of the given dependencies.
transDeps :: Map Name Deps -> Map Name Deps
transDeps :: Map Name Deps -> Map Name Deps
transDeps Map Name Deps
mp0 = forall a b. (a, b) -> a
fst
              forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head
              forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Eq a => a -> a -> Bool
(/=))
              forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Map Name Deps]
steps (forall a. [a] -> [a]
tail [Map Name Deps]
steps)
  where
  step1 :: Map Name Deps -> Deps -> Deps
step1 Map Name Deps
mp Deps
d = forall a. Monoid a => [a] -> a
mconcat [ forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
                            forall a. Monoid a => a
mempty { valDeps :: Set Name
valDeps = forall a. a -> Set a
Set.singleton Name
x }
                            Name
x Map Name Deps
mp | Name
x <- forall a. Set a -> [a]
Set.toList (Deps -> Set Name
valDeps Deps
d) ]
  step :: Map Name Deps -> Map Name Deps
step Map Name Deps
mp = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Map Name Deps -> Deps -> Deps
step1 Map Name Deps
mp) Map Name Deps
mp

  steps :: [Map Name Deps]
steps = forall a. (a -> a) -> a -> [a]
iterate Map Name Deps -> Map Name Deps
step Map Name Deps
mp0

-- | Dependencies of top-level declarations in a module.
-- These are dependencies on module parameters or things
-- defined outside the module.
moduleDeps :: Module -> Map Name Deps
moduleDeps :: Module -> Map Name Deps
moduleDeps = Map Name Deps -> Map Name Deps
transDeps forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {d}. (Defs d, FreeVars d) => d -> Map Name Deps
fromDG forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall mname. ModuleG mname -> [DeclGroup]
mDecls
  where
  fromDG :: d -> Map Name Deps
fromDG d
dg = let vs :: Deps
vs = forall e. FreeVars e => e -> Deps
freeVars d
dg
              in forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name
x,Deps
vs) | Name
x <- forall a. Set a -> [a]
Set.toList (forall d. Defs d => d -> Set Name
defs d
dg) ]

class FreeVars e where
  freeVars :: e -> Deps


instance FreeVars e => FreeVars [e] where
  freeVars :: [e] -> Deps
freeVars = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall e. FreeVars e => e -> Deps
freeVars


instance FreeVars DeclGroup where
  freeVars :: DeclGroup -> Deps
freeVars DeclGroup
dg = case DeclGroup
dg of
                  NonRecursive Decl
d -> forall e. FreeVars e => e -> Deps
freeVars Decl
d
                  Recursive [Decl]
ds   -> Set Name -> Deps -> Deps
rmVals (forall d. Defs d => d -> Set Name
defs [Decl]
ds) (forall e. FreeVars e => e -> Deps
freeVars [Decl]
ds)


instance FreeVars Decl where
  freeVars :: Decl -> Deps
freeVars Decl
d = forall e. FreeVars e => e -> Deps
freeVars (Decl -> DeclDef
dDefinition Decl
d) forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars (Decl -> Schema
dSignature Decl
d)


instance FreeVars DeclDef where
  freeVars :: DeclDef -> Deps
freeVars DeclDef
d = case DeclDef
d of
                 DeclDef
DPrim -> forall a. Monoid a => a
mempty
                 DForeign FFIFunType
_ -> forall a. Monoid a => a
mempty
                 DExpr Expr
e -> forall e. FreeVars e => e -> Deps
freeVars Expr
e


instance FreeVars Expr where
  freeVars :: Expr -> Deps
freeVars Expr
expr =
    case Expr
expr of
      ELocated Range
_r Expr
t     -> forall e. FreeVars e => e -> Deps
freeVars Expr
t
      EList [Expr]
es Type
t        -> forall e. FreeVars e => e -> Deps
freeVars [Expr]
es forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars Type
t
      ETuple [Expr]
es         -> forall e. FreeVars e => e -> Deps
freeVars [Expr]
es
      ERec RecordMap Ident Expr
fs           -> forall e. FreeVars e => e -> Deps
freeVars (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Expr
fs)
      ESel Expr
e Selector
_          -> forall e. FreeVars e => e -> Deps
freeVars Expr
e
      ESet Type
ty Expr
e Selector
_ Expr
v     -> forall e. FreeVars e => e -> Deps
freeVars Type
ty forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars [Expr
e,Expr
v]
      EIf Expr
e1 Expr
e2 Expr
e3      -> forall e. FreeVars e => e -> Deps
freeVars [Expr
e1,Expr
e2,Expr
e3]
      EComp Type
t1 Type
t2 Expr
e [[Match]]
mss -> forall e. FreeVars e => e -> Deps
freeVars [Type
t1,Type
t2] forall a. Semigroup a => a -> a -> a
<> Set Name -> Deps -> Deps
rmVals (forall d. Defs d => d -> Set Name
defs [[Match]]
mss) (forall e. FreeVars e => e -> Deps
freeVars Expr
e)
                                            forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. (FreeVars a, Defs a) => [a] -> Deps
foldFree [[Match]]
mss)
      EVar Name
x            -> forall a. Monoid a => a
mempty { valDeps :: Set Name
valDeps = forall a. a -> Set a
Set.singleton Name
x }
      ETAbs TParam
a Expr
e         -> TParam -> Deps -> Deps
rmTParam TParam
a (forall e. FreeVars e => e -> Deps
freeVars Expr
e)
      ETApp Expr
e Type
t         -> forall e. FreeVars e => e -> Deps
freeVars Expr
e forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars Type
t
      EApp Expr
e1 Expr
e2        -> forall e. FreeVars e => e -> Deps
freeVars [Expr
e1,Expr
e2]
      EAbs Name
x Type
t Expr
e        -> forall e. FreeVars e => e -> Deps
freeVars Type
t forall a. Semigroup a => a -> a -> a
<> Name -> Deps -> Deps
rmVal Name
x (forall e. FreeVars e => e -> Deps
freeVars Expr
e)
      EProofAbs Type
p Expr
e     -> forall e. FreeVars e => e -> Deps
freeVars Type
p forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars Expr
e
      EProofApp Expr
e       -> forall e. FreeVars e => e -> Deps
freeVars Expr
e
      EWhere Expr
e [DeclGroup]
ds       -> forall a. (FreeVars a, Defs a) => [a] -> Deps
foldFree [DeclGroup]
ds forall a. Semigroup a => a -> a -> a
<> Set Name -> Deps -> Deps
rmVals (forall d. Defs d => d -> Set Name
defs [DeclGroup]
ds) (forall e. FreeVars e => e -> Deps
freeVars Expr
e)
      EPropGuards [([Type], Expr)]
guards Type
_ -> forall a. Monoid a => [a] -> a
mconcat [ forall e. FreeVars e => e -> Deps
freeVars Expr
e | ([Type]
_, Expr
e) <- [([Type], Expr)]
guards ]
    where
      foldFree :: (FreeVars a, Defs a) => [a] -> Deps
      foldFree :: forall a. (FreeVars a, Defs a) => [a] -> Deps
foldFree = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {d}. (FreeVars d, Defs d) => d -> Deps -> Deps
updateFree forall a. Monoid a => a
mempty
      updateFree :: d -> Deps -> Deps
updateFree d
x Deps
rest = forall e. FreeVars e => e -> Deps
freeVars d
x forall a. Semigroup a => a -> a -> a
<> Set Name -> Deps -> Deps
rmVals (forall d. Defs d => d -> Set Name
defs d
x) Deps
rest

instance FreeVars Match where
  freeVars :: Match -> Deps
freeVars Match
m = case Match
m of
                 From Name
_ Type
t1 Type
t2 Expr
e -> forall e. FreeVars e => e -> Deps
freeVars Type
t1 forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars Type
t2 forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars Expr
e
                 Let Decl
d          -> forall e. FreeVars e => e -> Deps
freeVars Decl
d



instance FreeVars Schema where
  freeVars :: Schema -> Deps
freeVars Schema
s = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Deps -> Deps
rmTParam (forall e. FreeVars e => e -> Deps
freeVars (Schema -> [Type]
sProps Schema
s) forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars (Schema -> Type
sType Schema
s))
                              (Schema -> [TParam]
sVars Schema
s)

instance FreeVars Type where
  freeVars :: Type -> Deps
freeVars Type
ty =
    case Type
ty of
      TCon TCon
tc [Type]
ts -> forall e. FreeVars e => e -> Deps
freeVars TCon
tc forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars [Type]
ts
      TVar TVar
tv -> forall e. FreeVars e => e -> Deps
freeVars TVar
tv

      TUser Name
_ [Type]
_ Type
t -> forall e. FreeVars e => e -> Deps
freeVars Type
t
      TRec RecordMap Ident Type
fs     -> forall e. FreeVars e => e -> Deps
freeVars (forall a b. RecordMap a b -> [b]
recordElements RecordMap Ident Type
fs)
      TNewtype Newtype
nt [Type]
ts -> forall e. FreeVars e => e -> Deps
freeVars Newtype
nt forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars [Type]
ts

instance FreeVars TVar where
  freeVars :: TVar -> Deps
freeVars TVar
tv = case TVar
tv of
                  TVBound TParam
p -> forall a. Monoid a => a
mempty { tyParams :: Set TParam
tyParams = forall a. a -> Set a
Set.singleton TParam
p }
                  TVar
_         -> forall a. Monoid a => a
mempty

instance FreeVars TCon where
  freeVars :: TCon -> Deps
freeVars TCon
_tc = forall a. Monoid a => a
mempty

instance FreeVars Newtype where
  freeVars :: Newtype -> Deps
freeVars Newtype
nt = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Deps -> Deps
rmTParam Deps
base (Newtype -> [TParam]
ntParams Newtype
nt)
    where base :: Deps
base = forall e. FreeVars e => e -> Deps
freeVars (Newtype -> [Type]
ntConstraints Newtype
nt) forall a. Semigroup a => a -> a -> a
<> forall e. FreeVars e => e -> Deps
freeVars (forall a b. RecordMap a b -> [b]
recordElements (Newtype -> RecordMap Ident Type
ntFields Newtype
nt))


--------------------------------------------------------------------------------

class Defs d where
  defs :: d -> Set Name

instance Defs a => Defs [a] where
  defs :: [a] -> Set Name
defs = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall d. Defs d => d -> Set Name
defs

instance Defs DeclGroup where
  defs :: DeclGroup -> Set Name
defs DeclGroup
dg = case DeclGroup
dg of
              Recursive [Decl]
ds   -> forall d. Defs d => d -> Set Name
defs [Decl]
ds
              NonRecursive Decl
d -> forall d. Defs d => d -> Set Name
defs Decl
d

instance Defs Decl where
  defs :: Decl -> Set Name
defs Decl
d = forall a. a -> Set a
Set.singleton (Decl -> Name
dName Decl
d)

instance Defs Match where
  defs :: Match -> Set Name
defs Match
m = case Match
m of
             From Name
x Type
_ Type
_ Expr
_ -> forall a. a -> Set a
Set.singleton Name
x
             Let Decl
d -> forall d. Defs d => d -> Set Name
defs Decl
d