| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The word "increment" is more appropriate in this case than "lifting".
The world "lifting", in computer science, usually denotes something else:
https://en.wikipedia.org/wiki/Lambda_lifting
|
|
|
|
8a8caba3).
- Adding cLexer.current_file to the lexer state, i.e. making it a
component of the type "coq_parsable" of lexer state (it was
forgotten in b8ae2de5 and 8a8caba3).
- Inlining save_translator/restore_translator which have now lost most
of their substance.
|
|
There was no reason to keep them separate since quite a long time. Historically,
they were making Genarg depend or not on upper strata of the code, but since
it was moved to lib/ this is not justified anymore.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
"Context.{Rel,Named}.fold_constr"
|
|
Suggested by @ppedrot
|
|
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
|
|
In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.
We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.
This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.
|
|
|
|
|
|
|
|
|
|
|
|
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
|
I've included some other changes that didn't happen in this PR.
|
|
This is a first step to relay location info in an uniform way, as needed
by warnings and other mechanisms.
The location info remains unused for now, but coqtop printing could take
advantage of it if so wished.
|
|
|
|
|
|
functions about interpretation, internalization, externalization of
notations.
Main syntactic changes:
- subst_aconstr_in_glob_constr -> instantiate_notation_constr
(because aconstr has been renamed to notation_constr long time ago)
- extern_symbol -> extern_notation
(because symbol.ml has been renamed to notation.ml long time ago)
- documentation of notations_ops.mli
Main semantic changes:
- Notation_ops.eq_glob_constr which was partial eq disappears: use
glob_constr_eq instead
- In particular, this impacts a change on funind which now use the
(fully implemented) glob_constr_eq
Somehow, instantiate_notation_constr should be in notation_ops.ml for
symmetry with match_notation_constr but it is bit painful to do.
|
|
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|
|
|
|
|
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.
|
|
The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.
Some missing comments were added to the *.mli file.
The output of ocamldoc was checked whether it looks in a reasonable way.
"TODO: cleanup" was removed
The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)
The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)
The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)
The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})
The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.
Thrown exceptions are now documented.
Naming of formal parameters was made more consistent across different functions.
Comments of similar functions in different modules are now consistent.
Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
we can see the comments also there and do not need to open a different file if we want to see it.)
When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)
"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)
An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
|
|
|
|
|
|
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
|
|
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns
Still some questions:
- Should -> and <- apply to hypotheses or not (currently they apply to
hypotheses either when used in assert-style tactics or apply in, or
when the term to rewrite is a variable, in which case "subst" is
applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
quantifications?
|
|
- 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
|
|
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
|
|
which compute an abstraction of the goal over a term or a pattern.
|
|
|
|
- Clarification of the existence of three algorithms for solving
unconstrained evars:
- the type-class mechanism
- the heuristics for solving pending conversion problems and multi-candidates
- Declare Implicit Tactic (when called from tactics)
Main function for solving unconstrained evars (when not using
understand): Pretyping.solve_remaining_evars
- Clarification of the existence of three corresponding kinds of
errors when reporting about unsolved evars:
Main function for checking resolution of evars independently of the
understand functions: Pretyping.check_evars_are_solved
- Introduction of inference flags in pretyping for governing which
combination of the algorithms to use when calling some understand
function; there is also a flag of expanding or not evars and for
requiring or not the resolution of all evars
- Less hackish way of managing Pretyping.type_constraint: all three
different possibilities are now represented by three different
constructors
- Main semantical changes done:
- solving unconstrained evars and reporting is not any longer mixed:
one first tries to find unconstrained evars by any way possible;
one eventually reports on the existence of unsolved evars using
check_evars_are_solved
- checking unsolved evars is now done by looking at the evar map,
not by looking at the evars occurring in the terms to pretype; the
only observed consequence so far is in Cases.v because of subterms
(surprisingly) disappering after compilation of pattern-matching
- the API changed, see dev/doc/changes.txt
Still to do:
- Find more uniform naming schemes:
- for distinguishing when sigma is passed as a reference or as a value
(are used: suffix _evars, prefix e_)
- for distinguishing when evars are allowed to remain uninstantiated or not
(are used: suffix _evars, again, suffix _tcc, infix _open_)
- be more consistent on the use of names evd/sigma/evars or evdref/evars
- By the way, shouldn't "understand" be better renamed into "infer" or
"preinfer", or "pretype". Grammatically, "understanding a term" looks
strange.
- Investigate whether the inference flags in tacinterp.ml are really
what we want (e.g. do we really want that heuristic remains
activated when typeclasses are explicitly deactivated, idem in
Tacinterp.interp_open_constr where flags are strange).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15393 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
for the functions of unification.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14547 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13834 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Arguments bound with tactic(_) in TACTIC EXTEND rules are now of type
glob_tactic_expr, instead of glob_tactic_expr * tactic. Only the first
component is kept, the second one can be obtained with
Tacinterp.eval_tactic.
Rationale: these declare parsing rules, and eval_tactic is a semantic
action, and therefore should be done in the rule body
instead. Moreover, having the glob_tactic_expr and its evaluation
captured by these rules was quite confusing IMHO.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
them. This was the cause of the failure of compilation of
CyclicAxioms after "replace" starting supporting open constrs (r13206).
Seized the opportunity to clean a little bit things around nf_evar,
whd_evar, check_evars, etc.
Removed obsolete printer mod_self_id from dev/db.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
checking function was used instead of a test of existence in the context.
Also restricted constr_of_id which had no reason to interpret a
posteriori an already interpreted identifier as a global
reference. Consequently adapted funind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
swap in the evar flags and the isrec flag. (e.g. "induction" was
printed "edestruct").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13124 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
evar_map into a map for defined evars and a map for undefined evars.
Even before Spiwack's new proof engine, some Evd.fold were very
costly, e.g. in check_evars or progress_evar_map. With the new proof
engine, undefined evars traversals are apparently even more common (at
least, it improves significantly the complexity of some calls to omega
in JordanCurveTheorem - a new factor 5-7 after the factor 5-6 obtained
by removal of evar_merge in clenv_fchain in commit 13007, arriving to
figures comparable to the 8.3 ones).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
ML names
(late consequences of commit r12603)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12934 85f007b7-540e-0410-9357-904b9bb8a0f7
|
