1module Cryptol.IR.FreeVars
2  ( FreeVars(..)
3  , Deps(..)
4  , Defs(..)
5  , moduleDeps, transDeps
6  ) where
7
8import           Data.Set ( Set )
9import qualified Data.Set as Set
10import           Data.Map ( Map )
11import qualified Data.Map as Map
12
13import Cryptol.TypeCheck.AST
14import Cryptol.Utils.RecordMap
15
16data Deps = Deps { valDeps  :: Set Name
17                   -- ^ Undefined value names
18
19                 , tyDeps   :: Set Name
20                   -- ^ Undefined type names (from newtype)
21
22                 , tyParams :: Set TParam
23                   -- ^ Undefined type params (e.d. mod params)
24                 } deriving Eq
25
26instance Semigroup Deps where
27  d1 <> d2 = mconcat [d1,d2]
28
29instance Monoid Deps where
30  mempty = Deps { valDeps   = Set.empty
31                , tyDeps    = Set.empty
32                , tyParams  = Set.empty
33                }
34
35  mappend d1 d2 = d1 <> d2
36
37  mconcat ds = Deps { valDeps   = Set.unions (map valDeps ds)
38                    , tyDeps    = Set.unions (map tyDeps  ds)
39                    , tyParams  = Set.unions (map tyParams ds)
40                    }
41
42rmTParam :: TParam -> Deps -> Deps
43rmTParam p x = x { tyParams = Set.delete p (tyParams x) }
44
45rmVal :: Name -> Deps -> Deps
46rmVal p x = x { valDeps = Set.delete p (valDeps x) }
47
48rmVals :: Set Name -> Deps -> Deps
49rmVals p x = x { valDeps = Set.difference (valDeps x) p }
50
51
52-- | Compute the transitive closure of the given dependencies.
53transDeps :: Map Name Deps -> Map Name Deps
54transDeps mp0 = fst
55              $ head
56              $ dropWhile (uncurry (/=))
57              $ zip steps (tail steps)
58  where
59  step1 mp d = mconcat [ Map.findWithDefault
60                            mempty { valDeps = Set.singleton x }
61                            x mp | x <- Set.toList (valDeps d) ]
62  step mp = fmap (step1 mp) mp
63
64  steps = iterate step mp0
65
66-- | Dependencies of top-level declarations in a module.
67-- These are dependencies on module parameters or things
68-- defined outside the module.
69moduleDeps :: Module -> Map Name Deps
70moduleDeps = transDeps . Map.unions . map fromDG . mDecls
71  where
72  fromDG dg = let vs = freeVars dg
73              in Map.fromList [ (x,vs) | x <- Set.toList (defs dg) ]
74
75class FreeVars e where
76  freeVars :: e -> Deps
77
78
79instance FreeVars e => FreeVars [e] where
80  freeVars = mconcat . map freeVars
81
82
83instance FreeVars DeclGroup where
84  freeVars dg = case dg of
85                  NonRecursive d -> freeVars d
86                  Recursive ds   -> rmVals (defs ds) (freeVars ds)
87
88
89instance FreeVars Decl where
90  freeVars d = freeVars (dDefinition d) <> freeVars (dSignature d)
91
92
93instance FreeVars DeclDef where
94  freeVars d = case d of
95                 DPrim -> mempty
96                 DExpr e -> freeVars e
97
98
99instance FreeVars Expr where
100  freeVars expr =
101    case expr of
102      ELocated _r t     -> freeVars t
103      EList es t        -> freeVars es <> freeVars t
104      ETuple es         -> freeVars es
105      ERec fs           -> freeVars (recordElements fs)
106      ESel e _          -> freeVars e
107      ESet ty e _ v     -> freeVars ty <> freeVars [e,v]
108      EIf e1 e2 e3      -> freeVars [e1,e2,e3]
109      EComp t1 t2 e mss -> freeVars [t1,t2] <> rmVals (defs mss) (freeVars e)
110                                            <> mconcat (map foldFree mss)
111      EVar x            -> mempty { valDeps = Set.singleton x }
112      ETAbs a e         -> rmTParam a (freeVars e)
113      ETApp e t         -> freeVars e <> freeVars t
114      EApp e1 e2        -> freeVars [e1,e2]
115      EAbs x t e        -> freeVars t <> rmVal x (freeVars e)
116      EProofAbs p e     -> freeVars p <> freeVars e
117      EProofApp e       -> freeVars e
118      EWhere e ds       -> foldFree ds <> rmVals (defs ds) (freeVars e)
119    where
120      foldFree :: (FreeVars a, Defs a) => [a] -> Deps
121      foldFree = foldr updateFree mempty
122      updateFree x rest = freeVars x <> rmVals (defs x) rest
123
124instance FreeVars Match where
125  freeVars m = case m of
126                 From _ t1 t2 e -> freeVars t1 <> freeVars t2 <> freeVars e
127                 Let d          -> freeVars d
128
129
130
131instance FreeVars Schema where
132  freeVars s = foldr rmTParam (freeVars (sProps s) <> freeVars (sType s))
133                              (sVars s)
134
135instance FreeVars Type where
136  freeVars ty =
137    case ty of
138      TCon tc ts -> freeVars tc <> freeVars ts
139      TVar tv -> freeVars tv
140
141      TUser _ _ t -> freeVars t
142      TRec fs     -> freeVars (recordElements fs)
143      TNewtype nt ts -> freeVars nt <> freeVars ts
144
145instance FreeVars TVar where
146  freeVars tv = case tv of
147                  TVBound p -> mempty { tyParams = Set.singleton p }
148                  _         -> mempty
149
150instance FreeVars TCon where
151  freeVars _tc = mempty
152
153instance FreeVars Newtype where
154  freeVars nt = foldr rmTParam base (ntParams nt)
155    where base = freeVars (ntConstraints nt) <> freeVars (recordElements (ntFields nt))
156
157
158--------------------------------------------------------------------------------
159
160class Defs d where
161  defs :: d -> Set Name
162
163instance Defs a => Defs [a] where
164  defs = Set.unions . map defs
165
166instance Defs DeclGroup where
167  defs dg = case dg of
168              Recursive ds   -> defs ds
169              NonRecursive d -> defs d
170
171instance Defs Decl where
172  defs d = Set.singleton (dName d)
173
174instance Defs Match where
175  defs m = case m of
176             From x _ _ _ -> Set.singleton x
177             Let d -> defs d
178