| Age | Commit message (Collapse) | Author |
|---|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
|
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
|
|
|
|
|
|
Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.
HoTT_coq_117.v tests all of this.
|
|
|
|
We simply explicit that the type is actually referring to the return type,
not to the type of the argument of the pattern-matching. Note that the
heuristic could be enhanced so as to use the same code in both let-style
and match-style pattern-matching, but I'm leaving this for another time.
|
|
|
|
in error messages
|
|
|
|
|
|
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.
If multiple modules define a function with a same name, e.g.:
Context.{Rel,Named}.get_type
those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
|
|
|
|
|
|
Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.
Minor change of the API (adding one error case to recursion_scheme_error).
|
|
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
|
Goal 0=0 -> true=true.
intro H; rewrite H1.
was highlighting H1 but
Goal 0=0 -> true=true.
intro H; rewrite H.
was only highlighting the whole "intro H; rewrite H".
|
|
|
|
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
|
|
|
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
g I. (* Was printing Top.Top#<>#1 *)
idtac; f I. (* Was not properly locating error *)
This is a "a minima" fix.
This a different fix than in trunk, so the merge will have to take the
trunk version.
|
|
|
|
Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
|
|
|
|
|
|
|
|
|
|
Originally, rel-context was represented as:
Context.rel_context = Names.Name.t * Constr.t option * Constr.t
Now it is represented as:
Context.Rel.t = LocalAssum of Names.Name.t * Constr.t
| LocalDef of Names.Name.t * Constr.t * Constr.t
Originally, named-context was represented as:
Context.named_context = Names.Id.t * Constr.t option * Constr.t
Now it is represented as:
Context.Named.t = LocalAssum of Names.Id.t * Constr.t
| LocalDef of Names.Id.t * Constr.t * Constr.t
Motivation:
(1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction"
function which looked like this:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
Suppose that you do not know about rel-context and named-context.
(that is the case of people who just started to read the source code)
Merlin would tell you that the type of the value you are destructing
by "match" is:
'a * 'b option * Constr.t (* worst-case scenario *)
or
Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *)
To me, this is akin to wearing an opaque veil.
It is hard to figure out the meaning of the values you are looking at.
In particular, it is hard to discover the connection between the value
we are destructing above and the datatypes and functions defined
in the "kernel/context.ml" file.
In this case, the connection is there, but it is not visible
(between the function above and the "Context" module).
------------------------------------------------------------------------
Now consider, what happens when the reader see the same function
presented in the following form:
let test_strict_disjunction n lc =
Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
| [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
If the reader haven't seen "LocalAssum" before, (s)he can use Merlin
to jump to the corresponding definition and learn more.
In this case, the connection is there, and it is directly visible
(between the function above and the "Context" module).
(2) Also, if we already have the concepts such as:
- local declaration
- local assumption
- local definition
and we describe these notions meticulously in the Reference Manual,
then it is a real pity not to reinforce the connection
of the actual code with the abstract description we published.
|
|
multiple patterns.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
For instance, calling only Id.print is faster than calling both str and
Id.to_string, since the latter performs a copy. It also makes the code a
bit simpler to read.
|
|
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
|
When F is a Functor, doing an 'Include F' triggers the 'Include Self'
mechanism: the current context is used as an pseudo-argument to F.
This may fail with a subtype error if the current context isn't adequate.
|
|
|
|
|
|
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
|
Fixes #3809.
|
|
printing functions touched in the kernel).
|
|
|
|
|
|
in reporting the chain of causes when unification fails.
|
|
pattern-matching predicate.
|
|
|
|
Still to do:
- Decide between using SeveralInstancesFound or raising an error when
multiple instances exist.
- Use a proper printer for evars instead of the debugging
pr_evar_map_filter printer in pr_constraints.
|
|
|
