Collection of saw-core-rocq cleanups and fixes - #3361
Conversation
e4ecfbb to
1032f4e
Compare
|
This is ready to look at, though it probably isn't quite working yet |
| [] -> intro' <> ":" | ||
| _ -> | ||
| let short = PP.group $ intro' <+> PP.hsep params' <+> ":" |
There was a problem hiding this comment.
What do you think about putting space before the colon (e.g., printing FunsTo_Nil : FunsTo a instead of FunsTo_Nil: FunsTo a)? Currently, we are a bit inconsistent here, as we print FunsTo_Nil: FunsTo a (without space before the colon) but also forall (_1 : Type) (with space before the colon). I don't know if one is necessarily considered more correct than the other, although I'm used to seeing space before the colon in OCaml (e.g., in the output of ocamlformat), as well as in Rocq's own error messages.
There was a problem hiding this comment.
I'm used to writing both OCaml and Rocq without that space so I changed it intentionally. (Not all at once, so I could have missed some; if you see any inconsistency remaining in the final version, mark it up.)
I think it's markedly more readable this way, though that may just be a matter of being used to it.
(for functions, the form is foo (a: t1) (b: t2) : t3, still with a space, because otherwise it's weird.)
| let newstate imp x ty = ([], imp, [x], ty) | ||
| addstate imp x ty (others, previmp, prevnames, prevty) = | ||
| if imp == previmp && sameTerm ty prevty then | ||
| (others, previmp, x : prevnames, prevty) | ||
| else | ||
| ((previmp, reverse prevnames, prevty) : others, imp, [x], ty) | ||
| popstate (others, imp, names, ty) = | ||
| let others' = (imp, reverse names, ty) : others in | ||
| NamedPiBinders' $ reverse others' | ||
| in | ||
|
|
||
| let once (results, state) b = case state of | ||
| Nothing -> case b of | ||
| PiBinder imp Nothing ty -> | ||
| let here = AnonPiBinder' imp ty in | ||
| (here : results, Nothing) | ||
| PiBinder imp (Just x) ty -> | ||
| (results, Just $ newstate imp x ty) | ||
| Just s -> case b of | ||
| PiBinder imp Nothing ty -> | ||
| let prev = popstate s | ||
| here = AnonPiBinder' imp ty | ||
| in | ||
| (here : prev : results, Nothing) | ||
| PiBinder imp (Just x) ty -> | ||
| let s' = addstate imp x ty s in | ||
| (results, Just s') | ||
| in | ||
| let (results, state) = foldl once ([], Nothing) bs0 | ||
| results' = case state of | ||
| Nothing -> results | ||
| Just s -> popstate s : results | ||
| in | ||
| reverse results' |
There was a problem hiding this comment.
I think the code here would benefit from some type signatures, as it's a bit tricky to follow along with what's going on at a glance.
| -- Explicit parameters with a type are grouped by type: "(x y: a)" | ||
| -- Implicit parameters are grouped by maybe-type: "{x y}", "{x y: a}". | ||
| -- | ||
| data Binder' |
There was a problem hiding this comment.
I find the name "Binder'" to be a bit misleading, as it's possible for a single Binder' value to contain multiple Rocq binders because of ExplicitTypedBinders' or ImplicitBinders'. How about naming this something like ContractedBinders instead?
(Similar comments apply to PiBinder' as well.)
There was a problem hiding this comment.
Both of those were intended to be plural, but apparently I forgot to actually do it last night... fixed now.
|
|
||
| ## Bug Fixes | ||
|
|
||
| * The printing in the Rocq exporter has been fixed. |
There was a problem hiding this comment.
Fixed in what sense? It might help to clarify is the changes are solely for the sake of readability or if they fix a bug that would cause Rocq to reject generated code.
There was a problem hiding this comment.
I guess the intended tone didn't come across.
There was a problem hiding this comment.
(I have changed it)
| - working-directory: otherTests/saw-core-rocq | ||
| shell: bash | ||
| run: opam exec -- make -j rocq |
There was a problem hiding this comment.
Some more debugging is needed here, based on the CI output here:
Run opam exec -- make -j rocq
for f in *.v; do make ${f%.v}.vo || exit 1; done
make[1]: *** No rule to make target '*.vo'. Stop.
make[1]: Entering directory '/home/runner/work/saw-script/saw-script/otherTests/saw-core-rocq'
make[1]: Leaving directory '/home/runner/work/saw-script/saw-script/otherTests/saw-core-rocq'
make: *** [Makefile:21: rocq] Error 1
There was a problem hiding this comment.
Yeah, that's caused by the .v files not being there. I'll change it to run test.sh first to regenerate them, and if that doesn't work we may need to rearrange things further.
f996a9f to
ebd720c
Compare
|
(that rebase retcons the changelog message and the CI adjustments; if it works I'll also rebase on master) |
|
Ok, it seems to have worked |
(mostly: add comments, mark terms that are types as types) NFCI.
(mostly: add comments, remove silly synonyms, use the right synonyms) NFCI.
This is not necessary here for namespace control, since this file really only contains printing logic. But it's the way things are everywhere else in SAW and there's some value to that uniformity; also it's generally helpful to know at a glance which calls are actually prettyprinter operations. NFCI
This is not really working as intended yet, but it's already a vast improvement because it introduces at least SOME line breaks. So I'll call it a win. Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Update test reference outputs. NFCI, depending on whether you consider formatting "functional"
Share one copy of the code. Don't render to text before writing to a file, since there's no need and that materializes large strings in memory. Set the layout options explicitly instead of using the defaults. Don't use "show". This causes fewer unnecessary blank lines to appear, which wasn't intended but I'll call it good.
This doesn't make much difference, and makes some things come out better and others worse, but seems to be net positive, and the things it fixes are more significant than the things it breaks.
This accidentally fixed a bug where some identifiers in (* "foo" was skipped *) comments weren't quoted. Run with that.
Instead of: forall (a: nat), forall (b: nat), forall (c: bool), blah we print forall (a b: nat) (c: bool), blah This is both idiomatic usage and a lot more compact. I'd originally intended to do this as an AST transform, but for the moment it turns out to make more sense to do it on the fly while printing. At some point we might want to lower the AST to a concrete syntax tree, in which case this transform can become part of that pass.
This means we get (x y: bool) instead of (x: bool) (y: bool).
We want to be able to build the test output, so instead of dumping the test material to stdout, put each exported item in its own file. Split the reference outputs accordingly. Add a test-and-diff variant for this. It lives next to the other one in intTests' support dir because there isn't a better place for it, even though perhaps it doesn't really belong there.
You can now, if you've already built saw-core-rocq/rocq, run "make rocq" in here and it will build all the .v files and diff the build output. You'll also want to run "make rocqdepend" so it reruns if you change stuff in the handwritten tree. The diffing is done kind of on a shoestring as a temporary measure, because some of the files don't build. (That's #3339 and #3340.)
That's the one that runs Rocq on the .v files. There's also a saw-core-rocq-tests among the Cabal tests, which is the one that generates them.
This builds, or attempts to build, all the .v files output by otherTests/saw-core-rocq-tests.
Co-authored-by: Ryan Scott <rscott@galois.com>
Co-authored-by: Ryan Scott <rscott@galois.com>
(by request, seems like a good plan)
ebd720c to
fd47fb4
Compare
2 participants
This is a collection of assorted saw-core-rocq fixes. This is meant to go under #3360; the latter got pushed first because it was more important to get a draft out for people to look at.