aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/cctac.ml
Commit message (Collapse)AuthorAge
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* 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.
* Properly handling parameters of primitive projections in cctac.Gravatar Pierre-Marie Pédrot2017-08-29
|
* Correcting [build_discriminator] to make the test-suite passGravatar amblaf2017-07-31
|
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
|
* Explicit the unsafe flag of all calls to Refine.refine.Gravatar Pierre-Marie Pédrot2017-06-13
|
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* 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.
* Equality cleanup: remove constr_of_globalGravatar Matthieu Sozeau2017-05-29
|
* [coqlib] Deprecate redundant Coqlib functions.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | We remove redundant functions `coq_constant`, `gen_reference`, and `gen_constant`. This is a first step towards a lazy binding of libraries references. We have also chosen to untangle `constr` from `Coqlib`, as how to instantiate the reference (in particular wrt universes) is a client-side issue. (The client may want to provide an `evar_map` ?) c.f. #186
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Make congruence reuse discriminate instead of rolling its own.Gravatar Gaetan Gilbert2017-05-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes the produced terms a bit, eg Axiom T : Type. Lemma foo : true = false -> T. Proof. congruence. Qed. used to produce fun H : true = false => let Heq := H : true = false in @eq_rect Type True (fun X : Type => X) I T (@f_equal bool Type (fun t : bool => if t then True else T) true false Heq) now produces fun H : true = false => let Heq : true = false := H in let H0 : False := @eq_ind bool true (fun e : bool => if e then True else False) I false Heq in False_rect T H0 i.e. instead of proving [True = T] by [f_equal] then transporting [I] across this identity, it now proves [False] by [eq_ind] then uses exfalso.
| * Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
| |
| * Removing tactic compatibility layer in congruence.Gravatar Pierre-Marie Pédrot2017-04-24
| |
| * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
|/ | | | | | The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead.
* 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.
* Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
* 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.
* Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
|
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Removing compatibility layers in RetypingGravatar 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
|
* Proofview.Goal primitive 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
|
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Tacmach API using EConstr.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.
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| |
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | Suggested by @ppedrot
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/ | | | | | | 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.
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-07
|\
| * congruence: Restrict refreshing to SetGravatar Matthieu Sozeau2016-07-04
| | | | | | | | | | | | Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
| * congruence: remove casts of indexed termsGravatar Matthieu Sozeau2016-07-04
| | | | | | | | | | This fixes the end of bug #4069, provoked by a use of unshelve refine which introduces a cast.
| * congruence/univs: properly refresh (fix #4609)Gravatar Matthieu Sozeau2016-07-04
| | | | | | | | | | | | | | In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
* | 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
* | 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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 17:31:02 +0000