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
, Deps -> Set Name
tyDeps :: Set Name
, Deps -> Set TParam
tyParams :: Set TParam
} 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 }
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
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