Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update "proving my compiler incorrect" to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 18:58:50 -07:00
parent 6e7ac1c1ca
commit 3eddac0a89
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
content/blog/dyno_alloy/index.md
View File

@ -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 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 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 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 symbols matching description \(A\), and the second search is supposed to
look for symbols matching description \\(B\\), __then really we do a search look for symbols matching description \(B\), __then really we do a search
for \\(A \\land \\lnot B\\) (that is, \\(A\\) and not \\(B\\))__. for \(A \land \lnot B\) (that is, \(A\) and not \(B\))__.
{{< dialog >}} {{< dialog >}}
{{< message "question" "reader" >}} {{< message "question" "reader" >}}
@ -612,7 +612,7 @@ set of flags in the `curFilter` bitfield.
### Modeling Search State ### Modeling Search State
Next, I needed to model the behavior the I described earlier: searching for 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. when running subsequent searches.
Dyno implemented this roughly as follows: 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 2. When a scope was searched for the first time, its `curFilter` / search
bitfield was stored into the mapping. bitfield was stored into the mapping.
3. When a scope was searched after that, the previously-stored flags in the 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 the bitfield in the mapping was updated to be the intersection of
`curFilter` and the stored flags. `curFilter` and the stored flags.
@ -723,7 +723,7 @@ should have?
The `possibleState`, `updateOrSet`, and `excludeBitfield` The `possibleState`, `updateOrSet`, and `excludeBitfield`
lines encode the fact that a search occurred for `fs`. This must be a valid 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, 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 the algorithm work, the bitfield `exclude1` will be set based on the
previous search state. previous search state.