aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
Commit message (Collapse)AuthorAge
...
| | | | * | | Internal API change to typeclasses eauto.Gravatar Théo Zimmermann2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit makes the traversing strategy of typeclasses eauto an optional argument of the function that implements it. This change should be non-breaking.
| | | | * | | Do not shelve non-class subgoals but fail, it shouldGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | be the instance writer's responsibility to not generated non-dependent non-class subgoals (otherwise we loose compatibility as shown in e.g. MathClasses, which goes into loops because of unexpectedly unconstrained goals). Reflect it in the doc.
| | | | * | | typeclasses eauto Implem/doc of shelving strategyGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now [typeclasses eauto] mimicks what happens during resolution faithfully, and the shelving behavior/requirements for a successful proof-search are documented.
| | | | * | | Fix [typeclasses eauto with] and nopattern hintsGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This was the source of a bug in #5115#c7.
| | | | * | | Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| | | | | | |
| | | | * | | Handle Unique Solutions flag.Gravatar Matthieu Sozeau2016-11-03
| | | | | | |
| | | | * | | TCS: error handling and debug printing in resolutionGravatar Matthieu Sozeau2016-11-03
| | | | | | |
| | | | * | | Fix bugs in Filtered Unification and cleanup codeGravatar Matthieu Sozeau2016-11-03
| | | | | | |
| | | | * | | Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
| | | | | | |
| | | | * | | Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | |_|/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
* | | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| | | | |
| | * | | | Fix printing of typeclasses eauto debug wrt intro.Gravatar Théo Zimmermann2016-10-24
| | | | | |
| | | * | | Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ / / | | | | | | | | | | | | | | | | | | | | reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
| * / / / sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| | |
| * | | Clean up type classes flags and update compat file.Gravatar Maxime Dénès2016-10-05
| | | |
| | | * Fix bug 4969, autoapply was not tagging shelved subgoals correctly as ↵Gravatar Matthieu Sozeau2016-09-29
| | |/ | |/| | | | | | | unresolvable
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\| |
| * | Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-08-30
| | |
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
| | |
* | | 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.
* | 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.
* | Typeclasses: fix treatment of exceptions in compatGravatar Matthieu Sozeau2016-06-27
| |
* | Typeclasses: mark unresolvable goals in new implementationGravatar Matthieu Sozeau2016-06-27
| |
* | We want tclORELSE to catch exceptions on backtrackingsGravatar Matthieu Sozeau2016-06-27
| |
* | Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
| |
* | Fix resolve_one_typeclass to use the new engineGravatar Matthieu Sozeau2016-06-16
| |
* | Bind resolve_one_typeclass to 8.5 or 8.6 resolutionGravatar Matthieu Sozeau2016-06-16
| |
* | Put autoapply back, lost during rebaseGravatar Matthieu Sozeau2016-06-16
| |
* | Cleanup and refactoringGravatar Matthieu Sozeau2016-06-16
| |
* | Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
| | | | | | | | Fix test-suite files
* | bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | Add an option to force backtracking at toplevel, which is used by default when calling typeclasses eauto on a set of goals. They might be depended on by other subgoals, so the tactic should be backtracking by default, a once can make it not backtrack.
* | Typeclasses: allow shelved subgoalsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | | | Be more lenient, allowing non-class subgoals to remain after resolution, this seems necessary when launching resolution in goals containing evars. Also put a tclONCE when hints don't need to backtrack.
* | Minor cleanupGravatar Matthieu Sozeau2016-06-16
| |
* | Typeclasses: refine the eauto tacticGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | | | | | - Treat shelved dependent subgoals that might not be resolved after some proof search correctly by restarting their resolution as soon as possible (if they are typeclasses in only_classes mode). - Treat dependencies between goals better, avoiding backtracking more often when dependencies allow.
* | Typeclasses: verbosity and Limit Intros optionsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | To deactivate the limitation of introductions (which was added to avoid eta expansions in proof terms). This can cause huge blowups due to dumb backtracking. The arrow introduction rule is reversible, so better do it eagerly!
* | typeclass resolution: add two compatibility optionsGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | | | | | | | | | | | Set Typeclasses Compatibility "8.5". uses the old resolution tactic (off by default, but useful for debugging incompatibilities) Set Typeclasses Unification Compatibility "8.5". uses the old clenv unification tactic in resolution even with the new proof engine (on by default for now). Also fix the 8.5-compatible unification with the new engine resolution function, by using with_shelf and unshelve.
* | Fix incorrect caching of local hints w.r.t sectionsGravatar Matthieu Sozeau2016-06-16
| |
* | Compat with ocaml 4.01Gravatar Matthieu Sozeau2016-06-16
| |
* | Fix iterative deepening strategy failing too earlyGravatar Matthieu Sozeau2016-06-16
| | | | | | | | | | | | Report limit exceeded on _any_ branch so that we pursue search if it was reached at least once. Add example by N. Tabareau in test-suite.
* | Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
| | | | | | | | Fix typo in proofview
* | Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
| | | | | | | | with full backtracking across multiple goals.
* | Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for ↵Gravatar Hugo Herbelin2016-06-02
| | | | | | | | uniformity.
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * alternate path separators in typeclass debug output (4736)Gravatar Paul Steckler2016-05-17
| |
* | Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|/
* Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
|
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
|
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:50:04 +0000