|
| 1 | +--{-# OPTIONS_GHC -XNoMonomorphismRestriction #-} |
| 2 | + |
| 3 | +module AbstractDelta where |
| 4 | +import qualified Data.List as L |
| 5 | +import qualified Data.Map as M |
| 6 | +import qualified Data.Set as S |
| 7 | +import Data.Maybe |
| 8 | + |
| 9 | +type Prog = Lam |
| 10 | +type ProgM = M.Map Label Lam |
| 11 | + |
| 12 | +unionS xs = L.foldl' S.union S.empty xs |
| 13 | +unionmapM f xs = L.foldl' M.union M.empty $ map f xs |
| 14 | +unionmapS f xs = unionS $ map f xs |
| 15 | +-- labToLam_expr (CPSLam (txt, lab)) = M.insert lab txt (labToLam_lam txt) |
| 16 | +-- labToLam_expr _ = M.empty |
| 17 | +-- labToLam_call ((proc, args), _) = unionmapM labToLam_expr (proc:args) |
| 18 | +-- labToLam_lam (_, call) = labToLam_call call |
| 19 | + |
| 20 | +-- progm lam = labToLam_expr $ CPSLam lam |
| 21 | + |
| 22 | +type Label = [Int] |
| 23 | + |
| 24 | +newLab = [0] |
| 25 | +nextLab (minor:major) = (minor+1):major |
| 26 | +subLab lab = 0:lab |
| 27 | + |
| 28 | +type Var = String |
| 29 | + |
| 30 | +type DLamTxt = ([Var], DirectTerm) |
| 31 | +type DCallTxt = (DTerm, DTerm) |
| 32 | +data DirectTerm = DirectRef Var |
| 33 | + | DirectLam DLamTxt |
| 34 | + | DirectApp DCallTxt |
| 35 | +type DTerm = (DirectTerm, Label) |
| 36 | + |
| 37 | +type Ref = (Var, Label) |
| 38 | +type LamTxt = ([Var], Call) |
| 39 | +type Lam = (LamTxt, Label) |
| 40 | +type CallTxt = (CPSTerm, [CPSTerm]) |
| 41 | +type Call = (CallTxt, Label) |
| 42 | +data CPSTerm = CPSRef Ref |
| 43 | + | CPSLam Lam |
| 44 | + deriving (Show, Ord, Eq) |
| 45 | + |
| 46 | +directToCPS ((DirectRef var), lab) qont = |
| 47 | + ((qont, [CPSRef (var, lab)]), subLab lab) |
| 48 | +directToCPS ((DirectLam (formals, body)), lab) qont = ((qont, [CPSLam (, )]), ) |
| 49 | + where bodyCall = directToCPS body newK |
| 50 | + newK = CPSRef (, ) |
| 51 | +directToCPS ((DirectApp (proc, arg)), lab) qont = call |
| 52 | + where call = directToCPS proc () |
| 53 | + call' = directToCPS arg () |
| 54 | + call'' = ((u', [u'', qont]), ) |
| 55 | + u' = () |
| 56 | + u'' = () |
| 57 | + |
| 58 | +free_lam ((bvars, call), _) = S.difference (free_call call) $ S.fromList bvars |
| 59 | +free_call ((proc, args), _) = unionmapS free_expr (proc:args) |
| 60 | +free_expr (CPSRef (var, _)) = S.insert var S.empty |
| 61 | +free_expr (CPSLam lam) = free_lam lam |
| 62 | + |
| 63 | +mget dict key = fromJust $ M.lookup key dict |
| 64 | +bound progm lab = fst $ mget lab progm |
| 65 | + |
| 66 | +type EvalSt = (Call, Conf, Time) |
| 67 | +type ApplySt = (Proc, [Den], Conf, Time) |
| 68 | +data State = Eval EvalSt |
| 69 | + | Apply ApplySt |
| 70 | +data Result = FinalSt Den |
| 71 | + | NextSt EvalSt |
| 72 | + deriving (Show, Ord, Eq) |
| 73 | +type EvalConfs = M.Map (Call, Time) Conf |
| 74 | + |
| 75 | +type Conf = (VEnv, Measure) |
| 76 | +type VEnv = M.Map Bind Den |
| 77 | +type Bind = Var |
| 78 | +type Measure = M.Map Bind Count |
| 79 | +data Count = One | Many deriving (Show, Ord, Eq) |
| 80 | + |
| 81 | +addCount :: Count -> Count -> Count |
| 82 | +addCount _ _ = Many |
| 83 | + |
| 84 | +veJoin ve1 ve2 = M.unionsWith S.union [ve1, ve2] |
| 85 | +muJoin mu1 mu2 = M.unionsWith addCount [mu1, mu2] |
| 86 | +confJoin (v1, m1) (v2, m2) = (veJoin v1 v2, muJoin m1 m2) |
| 87 | + |
| 88 | +reachableMap kvs reached = M.difference kvs $ M.difference kvs reached |
| 89 | +confReachable (ve, mu) reached = (reachable ve, reachable mu) |
| 90 | + where reachable = flip reachableMap reached |
| 91 | + |
| 92 | +newconf = (M.empty, M.empty) |
| 93 | +confve (ve, _) = ve |
| 94 | +confmu (_, mu) = mu |
| 95 | + |
| 96 | +type Den = S.Set Val |
| 97 | +type Val = Proc |
| 98 | +data Proc = Clo Clo | Halt deriving (Show, Ord, Eq) |
| 99 | +type Clo = Lam |
| 100 | +data Time = Time deriving (Show, Ord, Eq) |
| 101 | + |
| 102 | +tsucc _ tm = tm |
| 103 | + |
| 104 | +touched_den Halt = S.empty |
| 105 | +touched_den (Clo lam) = free_lam lam |
| 106 | +touched_eval (call, _, _) = free_call call |
| 107 | +touched_apply (proc, args, _, _) = |
| 108 | + unionmapS touched_den $ S.elems $ unionS $ S.singleton proc:args |
| 109 | +touched_bind venv bd = unionmapS touched_den $ S.elems $ mget venv bd |
| 110 | + |
| 111 | +reachable_binds' ve seen bds = |
| 112 | + if S.null bds then seen |
| 113 | + else reachable_binds' ve (S.union seen bds') bds' |
| 114 | + where bds' = S.difference (unionmapS (touched_bind ve) (S.elems bds)) seen |
| 115 | + |
| 116 | +reachable_binds'' ve seen bds = reachable_binds' ve (S.union seen bds) bds |
| 117 | +reachable_binds ve bds = reachable_binds'' ve S.empty bds |
| 118 | + |
| 119 | +--reachable_den venv seen den = reachable_binds'' venv seen $ touched_den den |
| 120 | +reachable_eval st@(_, conf, _) = |
| 121 | + reachable_binds (confve conf) $ touched_eval st |
| 122 | +reachable_apply st@(_, _, conf, _) = |
| 123 | + reachable_binds (confve conf) $ touched_apply st |
| 124 | + |
| 125 | +zipWith_ _ [] [] = [] |
| 126 | +zipWith_ f (x:xs) (y:ys) = f x y : zipWith_ f xs ys |
| 127 | +zipWith_ _ _ _ = error "zipWith_ list args must be of the same length" |
| 128 | +zip_ xs ys = zipWith_ (,) xs ys |
| 129 | + |
| 130 | +evalArg (CPSRef (var, _)) venv = mget venv $ var |
| 131 | +evalArg (CPSLam lam) _ = S.singleton $ Clo lam |
| 132 | + |
| 133 | +evalToApply :: EvalSt -> S.Set ApplySt |
| 134 | +evalToApply st@(((pEx, aExs), _), conf, tm) = S.fromList apps |
| 135 | + where apps = map (\proc -> (proc, args, conf, tm')) $ S.elems procDen |
| 136 | + procDen = evalArg pEx $ confve conf |
| 137 | + args = map (\a -> evalArg a $ confve conf) aExs |
| 138 | + tm' = tsucc st tm |
| 139 | +applyToEval :: ApplySt -> Result |
| 140 | +applyToEval (Clo ((vars, call), _), args, conf, tm) = |
| 141 | + NextSt (call, (ve', mu'), tm) |
| 142 | + where ve' = veJoin ve veNew |
| 143 | + mu' = muJoin (confmu conf) muNew |
| 144 | + muNew = M.difference (M.fromList $ map (flip (,) One) vars) rebound |
| 145 | + rebound = M.filter (\x -> x) $ M.intersectionWith (==) ve veNew |
| 146 | + veNew = M.fromList $ zip_ vars args |
| 147 | + ve = (confve conf) |
| 148 | +applyToEval (Halt, [arg], _, _) = FinalSt arg |
| 149 | +applyToEval _ = error "halted with multiple values" |
| 150 | + |
| 151 | +progInitSt prog args = ((Clo prog), args++[S.singleton Halt], newconf, Time) |
| 152 | +evalProg prog args = applyToEval' $ progInitSt prog args |
| 153 | + |
| 154 | +hasNext (FinalSt _) = False |
| 155 | +hasNext _ = True |
| 156 | +nextEval (NextSt st) = st |
| 157 | +nextEval _ = error "attempted to continue from final state" |
| 158 | + |
| 159 | +evalToConf seen key = |
| 160 | + case M.lookup key seen of |
| 161 | + Nothing -> newconf |
| 162 | + Just conf -> conf |
| 163 | +isSubConf (ve1, _) (ve2, _) = M.isSubmapOfBy S.isSubsetOf ve1 ve2 |
| 164 | + |
| 165 | +setToMap ss = M.fromList $ map (\key -> (key, ())) $ S.elems ss |
| 166 | + |
| 167 | +collected_eval st@(call, conf, tm) = (call, confReachable conf reached, tm) |
| 168 | + where reached = setToMap $ reachable_eval st |
| 169 | +collected_apply st@(proc, args, conf, tm) = (proc, args, conf', tm) |
| 170 | + where conf' = confReachable conf reached |
| 171 | + reached = setToMap $ reachable_apply st |
| 172 | +-- only need one of these, right? |
| 173 | +evalToApply' = evalToApply . collected_eval |
| 174 | +applyToEval' = applyToEval . collected_apply |
| 175 | + |
| 176 | +widened confGlobal seen st@(call, conf, tm) = |
| 177 | + if isSubConf conf $ evalToConf seen key |
| 178 | + then Nothing |
| 179 | + else Just (conf', seen', (call, conf', tm)) |
| 180 | + where seen' = M.insert key conf' seen |
| 181 | + conf' = confJoin confGlobal conf |
| 182 | + key = (call, tm) |
| 183 | +-- non-widening... |
| 184 | +widened' confGlobal seen st@(call, conf, tm) = |
| 185 | + if isSubConf conf $ conf' |
| 186 | + then Nothing |
| 187 | + else Just (cfg, seen', st) |
| 188 | + where seen' = M.insert key conf'' seen |
| 189 | + cfg = confJoin confGlobal conf |
| 190 | + conf'' = confJoin conf' conf |
| 191 | + conf' = evalToConf seen key |
| 192 | + key = (call, tm) |
| 193 | + |
| 194 | +reachable_states' confGlobal seen [] = (confGlobal, seen) |
| 195 | +reachable_states' confGlobal seen (st:todo) = |
| 196 | + case widened' confGlobal seen st of |
| 197 | + Nothing -> reachable_states' confGlobal seen todo |
| 198 | + Just (confGlobal', seen', st') -> |
| 199 | + reachable_states' confGlobal' seen' todo' |
| 200 | + where todo' = S.elems $ S.union (S.fromList todo) nexts |
| 201 | + nexts = S.map nextEval $ S.filter hasNext $ results |
| 202 | + results = S.map applyToEval' $ evalToApply' st' |
| 203 | +reachable_states states = reachable_states' newconf M.empty states |
| 204 | +reachable_states_prog :: Clo -> [S.Set Proc] -> (Conf, EvalConfs) |
| 205 | +reachable_states_prog prog args = |
| 206 | + reachable_states $ map nextEval $ filter hasNext [evalProg prog args] |
| 207 | + |
| 208 | +---------------------------------------------------------------- |
| 209 | +mkRef var lab = CPSRef (var, [lab]) |
| 210 | +mkLam formals call lab = CPSLam ((formals, call), [lab]) |
| 211 | +mkCall proc args lab = ((proc, args), [lab]) |
| 212 | +mkLet var expr call lab0 lab1 = mkCall (mkLam [var] call lab0) [expr] lab1 |
| 213 | + |
| 214 | +-- (let* ((id (lambda (x) x)) |
| 215 | +-- (a (id (lambda (z) (halt z)))) |
| 216 | +-- (b (id (lambda (y) (halt y))))) |
| 217 | +-- (halt b)) |
| 218 | + |
| 219 | +CPSLam example = (mkLam ["halt"] (mkLet "id" (mkLam ["x", "k"] (mkCall (mkRef "k" 0) [(mkRef "x" 1)] 7) 11) |
| 220 | + (mkCall (mkRef "id" 2) |
| 221 | + [(mkLam ["z"] (mkCall (mkRef "halt" 20) [(mkRef "z" 3)] 8) 17), |
| 222 | + (mkLam ["a"] |
| 223 | + (mkCall (mkRef "id" 4) |
| 224 | + [(mkLam ["y"] (mkCall (mkRef "halt" 21) [(mkRef "y" 5)] 9) 18), |
| 225 | + (mkLam ["b"] (mkCall (mkRef "halt" 22) [(mkRef "b" 6)] 10) 19)] 12) 13)] 14) 15 16) 23) |
| 226 | + |
| 227 | +(confGlob, states) = reachable_states_prog example [] |
| 228 | + |
| 229 | +--showConf conf = M.fromList conf |
| 230 | + |
| 231 | +-- ("a",fromList [Clo ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),Clo ((["z"],((RefEx ("halt",20),[RefEx ("z",3)]),8)),17)]) |
| 232 | + |
| 233 | +-- ("b",fromList [Clo ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),Clo ((["z"],((RefEx ("halt",20),[RefEx ("z",3)]),8)),17)]) |
| 234 | + |
| 235 | +-- ("halt",fromList [Halt]) |
| 236 | + |
| 237 | +-- ("id",fromList [Clo ((["x","k"],((RefEx ("k",0),[RefEx ("x",1)]),7)),11)]) |
| 238 | + |
| 239 | +-- ("k",fromList [Clo ((["a"],((RefEx ("id",4),[LamEx ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),LamEx ((["b"],((RefEx ("halt",22),[RefEx ("b",6)]),10)),19)]),12)),13),Clo ((["b"],((RefEx ("halt",22),[RefEx ("b",6)]),10)),19)]) |
| 240 | + |
| 241 | +-- ("x",fromList [Clo ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),Clo ((["z"],((RefEx ("halt",20),[RefEx ("z",3)]),8)),17)]) |
| 242 | + |
| 243 | +-- collected |
| 244 | + |
| 245 | +-- ("b",fromList [Clo ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),Clo ((["z"],((RefEx ("halt",20),[RefEx ("z",3)]),8)),17)]) |
| 246 | + |
| 247 | +-- ("halt",fromList [Halt]) |
| 248 | + |
| 249 | +-- ("id",fromList [Clo ((["x","k"],((RefEx ("k",0),[RefEx ("x",1)]),7)),11)]) |
| 250 | + |
| 251 | +-- ("k",fromList [Clo ((["a"],((RefEx ("id",4),[LamEx ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),LamEx ((["b"],((RefEx ("halt",22),[RefEx ("b",6)]),10)),19)]),12)),13),Clo ((["b"],((RefEx ("halt",22),[RefEx ("b",6)]),10)),19)]) |
| 252 | + |
| 253 | +-- ("x",fromList [Clo ((["y"],((RefEx ("halt",21),[RefEx ("y",5)]),9)),18),Clo ((["z"],((RefEx ("halt",20),[RefEx ("z",3)]),8)),17)]) |
0 commit comments