Michael Norrish
Michael Norrish
My suspicion (from running the parser's test suite) is that `EVAL` on the parser is just super-slow on the experimental kernel. For example, it takes a minute to parse `val...
This issue is not a barrier to OpenTheory recording of CakeML anymore.
You've spelt Dijkstra as “disjkstra” ... (fingers are clearly too used to writing "disjunction" etc).
The graph is a finite map from nodes to lists of node-weight pairs (see `has_path` constant).
The `nil` corresponds to `cmlPtreeConversion`’s introduction of a variable that is called `""`. That string is indeed the empty list. I notice also that the sexp translation is also generating...
1. Notice how the sexp has a variable called `a`; the original does not; `cmlPtreeConversion` doesn't introduce such things, but the CF ANF-processing does. 2. The inversion theorem is only...
Cool that the AST to sexp stuff has been verified; I probably should have known/remembered this. I agree that ANFy things look to blame.
I don't understand how `uexi(s~s)_?s(i|e)` matches `UEXISTS_SIMP`. Does the translation of `~` insert `.*` on the front and back of the pattern? The code that translates `Twiddle a b` seems...
The `DBSearchParser` should also export the entry-point that turns the string into a regular expression.