Appearance
| 1 | namespace Syntax.Process is | |
| 2 | use Symbol = Semantic.Symbols.Symbol | |
| 3 | use LOCATION = Source.LOCATION | |
| 4 | ||
| 5 | // One heap fact crossed by one call during a body walk, and what | |
| 6 | // the walk did about it: killed it, because the relations solved by | |
| 7 | // the previous effects round could not show the callee left it | |
| 8 | // alone, or kept it - because they could, or because no relations | |
| 9 | // had been solved yet. `function` is the definition whose walk | |
| 10 | // made the record, so that walk alone can be redone. | |
| 11 | class KILL( | |
| 12 | file_name: string, | |
| 13 | crossing: CROSSING, | |
| 14 | target: Symbol?, | |
| 15 | path: ACCESS_PATH?, | |
| 16 | is_presence: bool, | |
| 17 | killed: bool | |
| 18 | ) is | |
| 19 | function: Trees.Definitions.FUNCTION? public | |
| 20 | ||
| 21 | // Whether this records a fact that was never formed, because a | |
| 22 | // getter the value is read through cannot back one, rather than | |
| 23 | // a call that ended a fact that was. The crossing then names the | |
| 24 | // getter's own declaration, which is no call site, and a use | |
| 25 | // short of the fact is short of it from the start. | |
| 26 | declined: bool public | |
| 27 | ||
| 28 | // What the dropped fact said the value was, for a type fact of a | |
| 29 | // formed narrowing. Null for a presence fact, and for a record | |
| 30 | // made where no fact was formed. A use that fails for want of | |
| 31 | // this fact is reported with the call attached, and what the | |
| 32 | // fact said is how that is judged. | |
| 33 | narrowed_type: Semantic.Types.Type? public | |
| 34 | si | |
| 35 | ||
| 36 | // The combined type + effect solve, in-walk form. When a | |
| 37 | // solved set of effect relations exists, the call transfer asks of | |
| 38 | // every heap fact live across a call whether the callee provably | |
| 39 | // left it alone, and drops the fact at the call when it cannot - | |
| 40 | // the fact's validity region ends there, the widened view flows | |
| 41 | // on, and a use only the fact satisfied is an ordinary type error. | |
| 42 | // | |
| 43 | // Every crossing a fact takes is recorded here with the walk's | |
| 44 | // decision. After each solve the decisions are re-asked against the | |
| 45 | // new relations: a fact kept across a call that cannot now be | |
| 46 | // discharged - every crossing of a walk made before any solve, and | |
| 47 | // some after an edit - or dropped at one that now can, makes its | |
| 48 | // body inexact, and the driver re-walks inexact bodies until a | |
| 49 | // solve finds none. The ledger keys nothing on rendered text: it | |
| 50 | // holds the crossing, fact and definition objects the walk | |
| 51 | // recorded. | |
| 52 | class KILL_LEDGER is | |
| 53 | _kills: Collections.LIST[KILL] static | |
| 54 | ||
| 55 | init() static is | |
| 56 | _kills = Collections.LIST[KILL]() | |
| 57 | _restart_bodies = Collections.SET[Trees.Definitions.FUNCTION]() | |
| 58 | si | |
| 59 | ||
| 60 | // The file whose bodies are being walked, for records made | |
| 61 | // where no location is at hand. | |
| 62 | current_file: string? public static | |
| 63 | ||
| 64 | // The definition whose body is being walked. Set for the | |
| 65 | // duration of each definition's walk by compile-expressions; | |
| 66 | // a record made outside one is keyed on its file alone. | |
| 67 | current_function: Trees.Definitions.FUNCTION? public static | |
| 68 | ||
| 69 | // Set while a walk must keep every fact whatever the relations | |
| 70 | // say: the start of a descent from the top. | |
| 71 | kills_suspended: bool public static | |
| 72 | ||
| 73 | // Set while the driver re-walks inexact bodies against the | |
| 74 | // relations, as opposed to an edit path walking a body against | |
| 75 | // the last complete solve. | |
| 76 | in_descent: bool public static | |
| 77 | ||
| 78 | // Whether some body was walked with kills outside a descent since | |
| 79 | // the last descent from the top - so the next COMPILE must restart | |
| 80 | // from the top to be sure of reaching the same answer batch would. | |
| 81 | needs_restart: bool public static | |
| 82 | ||
| 83 | // The definitions whose walk killed outside a descent since the | |
| 84 | // last descent from the top: the only bodies that started the | |
| 85 | // descent below the top, so the only ones a restart re-walks. | |
| 86 | _restart_bodies: Collections.SET[Trees.Definitions.FUNCTION] static | |
| 87 | ||
| 88 | // Whether the walk can consult relations at all. | |
| 89 | can_kill_in_walk: bool static => EFFECTS.is_complete /\ !kills_suspended | |
| 90 | ||
| 91 | record(kill: KILL) static is | |
| 92 | kill.function = current_function | |
| 93 | ||
| 94 | if kill.killed /\ !in_descent then | |
| 95 | needs_restart = true | |
| 96 | ||
| 97 | if let function = current_function then | |
| 98 | _restart_bodies.add(function) | |
| 99 | fi | |
| 100 | fi | |
| 101 | ||
| 102 | _kills.add(kill) | |
| 103 | si | |
| 104 | ||
| 105 | // Hand over the bodies a restart has to re-walk and start | |
| 106 | // afresh: those whose walk killed outside a descent. | |
| 107 | take_restart_bodies() -> Collections.SET[Trees.Definitions.FUNCTION] static is | |
| 108 | let result = _restart_bodies | |
| 109 | ||
| 110 | _restart_bodies = Collections.SET[Trees.Definitions.FUNCTION]() | |
| 111 | needs_restart = false | |
| 112 | ||
| 113 | return result | |
| 114 | si | |
| 115 | ||
| 116 | // Every definition whose last walk killed something. | |
| 117 | bodies_with_kills() -> Collections.SET[Trees.Definitions.FUNCTION] static is | |
| 118 | let result = Collections.SET[Trees.Definitions.FUNCTION]() | |
| 119 | ||
| 120 | for kill in _kills do | |
| 121 | if kill.killed then | |
| 122 | if let function = kill.function then | |
| 123 | result.add(function) | |
| 124 | fi | |
| 125 | fi | |
| 126 | od | |
| 127 | ||
| 128 | return result | |
| 129 | si | |
| 130 | ||
| 131 | // The file's walk is being redone from its source: whatever it | |
| 132 | // recorded is superseded by the walk to come. | |
| 133 | clear_for(file_name: string) static is | |
| 134 | _drop_where(kill => kill.file_name =~ file_name) | |
| 135 | si | |
| 136 | ||
| 137 | // One definition's body walk is being redone. | |
| 138 | clear_for(function: Trees.Definitions.FUNCTION) static is | |
| 139 | _drop_where(kill => kill.function == function) | |
| 140 | si | |
| 141 | ||
| 142 | _drop_where(condition: (KILL) -> bool) static is | |
| 143 | let kept = Collections.LIST[KILL]() | |
| 144 | ||
| 145 | for kill in _kills do | |
| 146 | if !condition(kill) then | |
| 147 | kept.add(kill) | |
| 148 | fi | |
| 149 | od | |
| 150 | ||
| 151 | _kills = kept | |
| 152 | si | |
| 153 | ||
| 154 | // One line per record, for comparing what walks recorded. | |
| 155 | dump(writer: IO.TextWriter) static is | |
| 156 | for kill in _kills do | |
| 157 | let what = if let target = kill.target then target.name elif let path = kill.path then path.to_string() else "?" fi | |
| 158 | ||
| 159 | writer.write_line("{kill.file_name} {if let function = kill.function then function.location.start_line else 0 fi} {kill.crossing.location} {if kill.is_presence then "presence" else "type" fi} {what} {if kill.killed then "killed" else "kept" fi}") | |
| 160 | od | |
| 161 | si | |
| 162 | ||
| 163 | clear_all() static is | |
| 164 | _kills.clear() | |
| 165 | si | |
| 166 | ||
| 167 | // The call that dropped a fact about this target nearest above | |
| 168 | // `at`, if one did. Asked at a use that failed for want of the | |
| 169 | // fact, so that the error can name the call that ended it; | |
| 170 | // `is_presence` picks the domain. A value narrowed more than | |
| 171 | // once in a body has a record per drop, each of a fact | |
| 172 | // re-established since the last, so the one the use is short of | |
| 173 | // is the last drop written before it - an earlier one belongs | |
| 174 | // to a narrowing this use never had. | |
| 175 | last_dropped_before(target: Symbol?, path: ACCESS_PATH?, is_presence: bool, at: LOCATION) -> KILL? static is | |
| 176 | let result: KILL? mut = null | |
| 177 | ||
| 178 | for kill in _kills do | |
| 179 | if | |
| 180 | kill.killed /\ | |
| 181 | !kill.declined /\ | |
| 182 | kill.is_presence == is_presence /\ | |
| 183 | kill.function == current_function /\ | |
| 184 | _describes(kill, target, path) /\ | |
| 185 | _precedes(kill.crossing.location, at) | |
| 186 | then | |
| 187 | if !result? \/ kill.crossing.location.start > result.crossing.location.start then | |
| 188 | result = kill | |
| 189 | fi | |
| 190 | fi | |
| 191 | od | |
| 192 | ||
| 193 | return result | |
| 194 | si | |
| 195 | ||
| 196 | // Whether a call written here could have ended a fact a use at | |
| 197 | // `use` needed: the same file, and not below it. | |
| 198 | _precedes(call: LOCATION, at: LOCATION) -> bool static => | |
| 199 | call.file_name =~ at.file_name /\ call.start <= at.start | |
| 200 | ||
| 201 | _describes(kill: KILL, target: Symbol?, path: ACCESS_PATH?) -> bool static is | |
| 202 | if let killed_target = kill.target then | |
| 203 | return target? /\ killed_target == target | |
| 204 | fi | |
| 205 | ||
| 206 | if let killed_path = kill.path then | |
| 207 | return path? /\ killed_path.equals(path) | |
| 208 | fi | |
| 209 | ||
| 210 | return false | |
| 211 | si | |
| 212 | ||
| 213 | // After a solve: every body whose walk decided some crossing | |
| 214 | // differently from the way the new relations would, and the | |
| 215 | // files of the records made outside any definition's walk. | |
| 216 | // Both empty means the last walk of every body agrees with the | |
| 217 | // relations, which is the fixpoint. | |
| 218 | take_inexact() -> INEXACT static is | |
| 219 | let result = INEXACT() | |
| 220 | ||
| 221 | let stopwatch = System.Diagnostics.Stopwatch.start_new() | |
| 222 | let asked mut = 0 | |
| 223 | let killed mut = 0 | |
| 224 | ||
| 225 | for kill in _kills do | |
| 226 | if kill.killed then | |
| 227 | killed = killed + 1 | |
| 228 | fi | |
| 229 | ||
| 230 | if let function = kill.function then | |
| 231 | if result.bodies.contains(function) then | |
| 232 | continue | |
| 233 | fi | |
| 234 | elif result.files.contains(kill.file_name) then | |
| 235 | continue | |
| 236 | fi | |
| 237 | ||
| 238 | asked = asked + 1 | |
| 239 | ||
| 240 | let discharged = RELIANCES.crossing_discharged(kill.crossing, kill.target, kill.path, kill.is_presence) | |
| 241 | ||
| 242 | if discharged == kill.killed then | |
| 243 | if let function = kill.function then | |
| 244 | result.bodies.add(function) | |
| 245 | else | |
| 246 | result.files.add(kill.file_name) | |
| 247 | fi | |
| 248 | fi | |
| 249 | od | |
| 250 | ||
| 251 | if System.Environment.get_environment_variable("GHUL_EFFECTS_TIMING")? then | |
| 252 | IO.Std.error.write_line("ledger: {_kills.count} records ({killed} killed), {asked} re-asked in {stopwatch.elapsed_milliseconds} ms, {result.bodies.count} body(ies) and {result.files.count} file(s) inexact") | |
| 253 | fi | |
| 254 | ||
| 255 | return result | |
| 256 | si | |
| 257 | si | |
| 258 | ||
| 259 | // What a solve found inexact: the definitions whose body walks | |
| 260 | // disagree with the relations, and the files of records that were | |
| 261 | // made outside a definition's walk. | |
| 262 | class INEXACT is | |
| 263 | bodies: Collections.SET[Trees.Definitions.FUNCTION] | |
| 264 | files: Collections.SET[string] | |
| 265 | ||
| 266 | init() is | |
| 267 | bodies = Collections.SET[Trees.Definitions.FUNCTION]() | |
| 268 | files = Collections.SET[string]() | |
| 269 | si | |
| 270 | ||
| 271 | is_empty: bool => bodies.count == 0 /\ files.count == 0 | |
| 272 | si | |
| 273 | si |