aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/reductionops.ml
Commit message (Collapse)AuthorAge
* Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
| | | | | | | The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\
| * Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
| |
* | Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
|/ | | | | | This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
|
* Merge PR#714: Print feature Proof-of-Concept (episode 2)Gravatar Maxime Dénès2017-06-13
|\
* \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
| | * Added support for a side effect on constants in reduction functions.Gravatar Thomas Sibut-Pinote2017-06-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml.
* | | 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 ```
* | Merge PR#670: Postponing of universe constraints unification in term equality.Gravatar Maxime Dénès2017-06-01
|\ \
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | | [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.
| * | Postponing of universe constraints unification in term equality.Gravatar Pierre-Marie Pédrot2017-05-23
|/ / | | | | | | | | | | Instead of calling the universe unification at each term node, we accumulate them and try to perform unification at the very end. This seems to be experimentally faster.
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| |
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |
| * Reinstate fixpoint refolding in [cbn], deactivated by mistake.Gravatar Matthieu Sozeau2017-04-13
| | | | | | | | Add a test-suite file to be sure we won't regress silently.
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | | | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | 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.
* | | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Cc API using EConstr.Gravatar 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
| | |
* | | Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Clenv 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
| | |
* | | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | |
* | | Pretyping 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 branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|/| | | |/
| * Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
| | | | | | | | | | | | | | | | | | | | | | | | In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel.
* | Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | | | | We return an option type, as constraints were always dropped if the boolean was false. They did not make much sense anyway.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Remove incorrect assertion in cbn (bug #4822).Gravatar Guillaume Melquiond2016-09-28
| | | | | | | | | | | | This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion).
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * no-refold patchGravatar Paul Steckler2016-09-09
| | | | | | | | | | | | Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ | |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
* | [pp] Fix newline issues.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | | | This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where we got a few cases wrong wrt to newline endings. Thanks to @herbelin for pointing it out. This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:44:11 +0000