From 3eddac0a8983298ae234e7588a2d54ec0548f29f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 13 May 2024 18:58:50 -0700 Subject: [PATCH] Update "proving my compiler incorrect" to new math delimiters Signed-off-by: Danila Fedorin --- content/blog/dyno_alloy/index.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/content/blog/dyno_alloy/index.md b/content/blog/dyno_alloy/index.md index f86d2bc..bb2334a 100644 --- a/content/blog/dyno_alloy/index.md +++ b/content/blog/dyno_alloy/index.md @@ -193,9 +193,9 @@ duplicate results (it's easier to check for duplicate definitions if you know a symbol is only returned from a search once). So, another feature of Dyno's scope search is an additional bitfield of what to _exclude_, which we set to be the previous search's filter. So if the first search looked for -symbols matching description \\(A\\), and the second search is supposed to -look for symbols matching description \\(B\\), __then really we do a search -for \\(A \\land \\lnot B\\) (that is, \\(A\\) and not \\(B\\))__. +symbols matching description \(A\), and the second search is supposed to +look for symbols matching description \(B\), __then really we do a search +for \(A \land \lnot B\) (that is, \(A\) and not \(B\))__. {{< dialog >}} {{< message "question" "reader" >}} @@ -612,7 +612,7 @@ set of flags in the `curFilter` bitfield. ### Modeling Search State Next, I needed to model the behavior the I described earlier: searching for -\\(A \\land \\lnot B\\), and taking the intersection of past searches +\(A \land \lnot B\), and taking the intersection of past searches when running subsequent searches. Dyno implemented this roughly as follows: @@ -622,7 +622,7 @@ Dyno implemented this roughly as follows: 2. When a scope was searched for the first time, its `curFilter` / search bitfield was stored into the mapping. 3. When a scope was searched after that, the previously-stored flags in the - mapping were excluded (that's the \\(A\\land\\lnot B\\) behavior), and + mapping were excluded (that's the \(A\land\lnot B\) behavior), and the bitfield in the mapping was updated to be the intersection of `curFilter` and the stored flags. @@ -723,7 +723,7 @@ should have? The `possibleState`, `updateOrSet`, and `excludeBitfield` lines encode the fact that a search occurred for `fs`. This must be a valid search, and the search state must be modified appropriately. Furthermore, -at the time this search takes place, to make the \\(\\lnot B\\) portion of +at the time this search takes place, to make the \(\lnot B\) portion of the algorithm work, the bitfield `exclude1` will be set based on the previous search state.