| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
(Sorry, was not intended to be pushed)
This reverts commit 5268efdefb396267bfda0c17eb045fa2ed516b3c.
|
|
This reverts commit bff2b36cb0e2dbd02c4f181fba545a420e847767.
|
|
|
|
In particular:
- abstracting the code using calls to Unix opendir, stat, and closedir,
- uniformly using warnings when a directory does not exist (coqtop was
ignoring silently and coqdep was exiting via handle_unix_error).
|
|
|
|
|
|
|
|
letting make validate progress.
|
|
|
|
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
|
inductive instantiation, now using substitution of levels.
Fixes the test-suite file coqchk/univ.
|
|
|
|
|
|
Conflicts:
checker/closure.ml
checker/closure.mli
checker/reduction.ml
|
|
|
|
|
|
The validation process was passing most of its time in the construction of
the name of the current context.
|
|
|
|
|
|
|
|
|
|
|
|
constraints only.
|
|
|
|
|
|
|
|
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
|
|
|
|
|
simplifying conversion code.
|
|
|
|
|
|
|
|
subst_univs_levels.
|
|
|
|
it to the new representation of projections and the new mind_finite
type.
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
|
|
|
|
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
|
|
|
and disable hashconsing of substituted instances which had a huge performance
penalty in general. They are hashconsed when put in the environment only now.
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
|
|
were never used and were responsible for code duplication.
|
|
I also took the opportunity to remove a lot of code not used by
the checker.
|
|
|
|
|
