aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
Commit message (Collapse)AuthorAge
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
| | | | | | | | | | | | | We remove most of what was deprecated in `Term`. Now, `intf` and `kernel` are almost deprecation-free, tho I am not very convinced about the whole `Term -> Constr` renaming but I'm afraid there is no way back. Inconsistencies with the constructor policy (see #6440) remain along the code-base and I'm afraid I don't see a plan to reconcile them. The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a good idea as someone added a `List` module inside it.
* Deprecate Typing.e_* functionsGravatar Gaëtan Gilbert2018-05-14
|
* Deprecate Evarconv.e_conv,e_cumulGravatar Gaëtan Gilbert2018-05-11
|
* Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| | | | clear_hyps remain with no alternative
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| | | | | | | | This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | |
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| | |
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | Now it is a private field, locations are optional.
* | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ / | | | | | | | | We continue the uniformization pass. No big news here, trying to be minimally invasive.
| * Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ | | | Also remove obvious comments.
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | For now we only normalize sorts, and we leave instances for the next commit.
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
|
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Classops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| | | | | | | | | | | | | | | | | | | | | | 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.
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | | | | | | | | 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.
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Program: cleanup in cases, add optionsGravatar Matthieu Sozeau2016-06-29
| | | | | | | Unset Program Generalized Coercion to avoid coercion of general applications. Unset Program Cases to deactivate generation equalities and disequalities of cases.
* Rework treatment of default transparency of obligationsGravatar Matthieu Sozeau2016-06-27
| | | | | | | | | | | | | | | | By default obligations defined by tactics are defined transparently or opaque according to the Obligations Transparent flag, except proofs of subset obligations which are treated as opaque by default. When the user proves the obligation using Qed or Defined, this information takes precedence, and only when the obligation cannot be Qed'ed because it contains references to a recursive function an error is raised (this prevents the guardness checker error). Shrinked obligations were not doings this correctly. Forcing transparency due to fixpoint prototypes takes precedence over the user preference. Program: do not force opacity of subset proofs, maintaining compatibility.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
| * More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Gravatar Hugo Herbelin2016-06-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When typing a "with clause fails, type classes are used to possibly help to insert coercions. If this heuristic fails, do not consider it anymore to be the best failure since it has made type classes choices which may be inconsistent with other constraints and on which no backtracking is possible anymore (see new example in test suite file 4782.v). This does not mean that using type classes at this point is good. It may find an instance which help to find a coercion, but which might still be a choice of instance and coercion which is incompatible with other constraints. I tend to think that a convenient way to go to deal with the absence of backtracking in inserting coercions would be to have special For the record, here is a some comments of what happens regarding f9695eb4b and 827663982. In the presence of an instance (x:=t) given in a "with" clause, with t:T, and x expected of type T', the situation is the following: Before f9695eb4b: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is postponed to w_merge, even though there is no way to get more information since T ant T' are closed. As a result, t may be ill-typed and the unification may try to unify ill-formed terms, leading to #4872. - If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it fails, e.g. because a wrong type class instance is found, it was postponed to w_merge as above, and the test for coercion is retried now interleaved with type classes. After f9695eb4b and 827663982e: - If T and T' are closed and T <= T' is not satisfiable (no coercion or not convertible), the test for possible insertion of a coercion is an immediate failure. This fixes #4872. - However, If T and T' are not closed and contains evars of type a type class, inference of type classes is tried. If it gives closed terms and fails, this is immediate failure without backtracking on type classes, resulting in the problem added here to file 4872.v. The current fix does not consider the result of the use of type classes while trying to insert a coercion to be the last word on it. So, it fails with an error which is not the error for conversion of closed terms (ConversionFailed), therefore in a way expected by f9695eb4b and 827663982e, and the "with" typing problem is then postponed again.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\|
| * Fix a bug in Program coercion codeGravatar Matthieu Sozeau2016-03-25
| | | | | | | | | | It was not accounting for the universe constraints generated by applications of the coercion.