Section.t is never empty #10829
Section.t is never empty #10829
Conversation
kernel/safe_typing.ml
Outdated
| @@ -404,7 +408,7 @@ let check_current_library dir senv = match senv.modvariant with | |||
| (** When operating on modules, we're normally outside sections *) | |||
|
|
|||
| let check_empty_context senv = | |||
| assert (Environ.empty_context senv.env && Section.is_empty senv.sections) | |||
| assert (Environ.empty_context senv.env && senv.sections = None) | |||
| let c, r, typ = Term_typing.translate_local_def senv.env id de in | ||
| let x = Context.make_annot id r in | ||
| let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in | ||
| { senv with sections; env = env'' } | ||
| { senv with sections=Some sections; env = env'' } |
There was a problem hiding this comment.
Spaces are not a threatened species, please put a pair between equality, as well as everywhere below. Even better, reuse the punning and leave that line unchanged, writing above instead let sections = Some (Section.push_local sections) in.
| @@ -20,7 +20,9 @@ type section_entry = | |||
|
|
|||
| type 'a entry_map = 'a Cmap.t * 'a Mindmap.t | |||
|
|
|||
| type 'a section = { | |||
| type 'a t = { | |||
| sec_prev : 'a t option; | |||
There was a problem hiding this comment.
Really not pretty, I'd prefer a list and ensuring everywhere that it's not empty.
There was a problem hiding this comment.
We use non-empty lists in a few places already so indeed we could add a generic NEList data structure to the libraries.
There was a problem hiding this comment.
TBH I don't see a need to use nonempty lists here, having the outer section be a member of the current one seems to work fine.
| let get_section = function | ||
| | None -> CErrors.user_err Pp.(str "No open section.") | ||
| | Some s -> s |
There was a problem hiding this comment.
[nit] It seems that the users below follow the same pattern to an extent that it could be worth to make this into a combinator with_open_section and refactor a bit more.
ejgallego
added
the
needs: rebase
SkySkimmer
force-pushed
the
section-nonempty
branch
from
5b634b9
to
92c3254
Compare
coqbot
removed
the
needs: rebase
ejgallego
added
kind: cleanup
|
This PR got stuck, but it seems like a nice one to me, what should be done? |
SkySkimmer
force-pushed
the
section-nonempty
branch
from
92c3254
to
5605b38
Compare
coqbot
removed
the
needs: rebase
kernel/safe_typing.mli
Outdated
| val sections_of_safe_env : safe_environment -> section_data Section.t | ||
| val sections_of_safe_env : safe_environment -> section_data Section.t option | ||
|
|
||
| val force_sections_of_safe_env : safe_environment -> section_data Section.t |
There was a problem hiding this comment.
Why export this if there are no users? I don't think it's the job of the kernel to display nice messages when there is a programming error.
There was a problem hiding this comment.
There's a user in lib
There was a problem hiding this comment.
Ah, yes, sorry. (Still seems strange to export, but fine.)
There was a problem hiding this comment.
We could move it to lib and make it internal
There was a problem hiding this comment.
I'd prefer so if possible. Not to mention the fact that this is quite ill-named...
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
SkySkimmer
force-pushed
the
section-nonempty
branch
from
5605b38
to
88dfc41
Compare
Ack-by: ejgallego Reviewed-by: ppedrot
This approach using
type t = { sec_prev: t option; sec_... }makesit easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using
type t = section * section listwhichneeds some boilerplate to update.