| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Defined constants
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
|
|
Helps with #12566
|
|
|
|
declaration path
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
|
|
This is a leftover after the unification of constant information,
`kind` is now correctly set by the single caller of
`Obls.add_mutual_definitions`.
|
|
Ack-by: gares
Reviewed-by: ppedrot
|
|
This is about the third time I try to kill this file but for some reason
it is still here.
|
|
Fixes #11970.
|
|
This is to anticipate further not-only-parsing uses of the notation.
|
|
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
|
|
Exceptions should not printed except for the top-level.
There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
|
|
This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.
Incidentally fixes #12649.
|
|
|
|
This is also needed in equations.
|
|
|
|
This is for use in Equations. At some point we should make all hook aware
of state, but this should suffice for now.
Note the comments as the role of hooks here, this may need further
cleanup indeed.
|
|
This is already taken of by `declare_definition`, by consistency with
the mutual case.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
This is essential to allow hooks to modify state.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
It used to be a big functor but changed in
8c5adfd5acb883a3bc2850b6fc8c29d352a421f8
The functor indent is now incorrect.
|
|
Fix #12651
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
Fix #12551
|
|
After #12504 , we can encapsulate and consolidate low-level state
logic in `Vernacstate`, removing `States` which is now a stub.
There is hope to clean up some stuff regarding the handling of
low-level proof state, by moving both `Evarutil.meta_counter` and
`Evd.evar_counter_summary` into the proof state itself [obligations
state is taken care in #11836] , but this will take some time.
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: maximedenes
|
|
Reviewed-by: ejgallego
|
|
Now that `Printmods` is above `Declaremods`, we don't need to pass the
extra `mod_ops` argument.
|
|
We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.
Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.
|
|
definitions
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
|
|
|
|
This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
|
|
|
|
This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.
In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.
Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
|
|
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
|
|
|
|
Now that the interface has mostly stabilized, we move code around to
respect internal dependency order.
This will allow us to start sharing more code in the 4 principal
cases, and also paves the way for the full merging of obligations and
the removal of the Proof_ending type in favor of stronger type
abstraction.
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
|
