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