aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/indtypes.ml
Commit message (Collapse)AuthorAge
...
* | | Merge origin/v8.5 into trunkGravatar Hugo Herbelin2015-11-10
|\| | | | | | | | | | | Did some manual merge in tactics/tactics.ml.
| * | Dead code from the commit having introduced primitive projections (a4043608).Gravatar Hugo Herbelin2015-11-10
| | |
| * | Fixing a bug in reporting ill-formed constructor.Gravatar Hugo Herbelin2015-11-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, Inductive a (x:=1) := C : a -> True. was wrongly reporting Error: The type of constructor C is not valid; its conclusion must be "a" applied to its parameter. Also "simplifying" explain_ind_err.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\| |
| * | Fixing a bug in reporting ill-formed inductive.Gravatar Hugo Herbelin2015-10-22
| | | | | | | | | | | | Was introduced in b06d3badb (15 Jul 2015).
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\| |
| * | Univs: inductives, remove unneeded testGravatar Matthieu Sozeau2015-10-14
| | |
* | | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
| | | | | | | | | | | | | | | 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\| |
| * | Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-06
|\| |
| * | Implementing Herbelin's fix for the "NonPar" bugGravatar mlasson2015-09-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Hugo Herbelin proposed to modify directly the function "check_correct_par" to simplify commit c12b430 (see the pullrequest's discussion). Note that the constructor "LocalNonPar" has now three arguments (instead of two). In LocalNonPar (n,i,l) n denotes the position among real arguments (ie. ignoring letins), i is the rel index of the expecting argument in the context of parameters and l is the index of the inductive.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\| |
| * | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | in vo files (this was not done yet in 24d0027f0 and 090fffa57b). Reused field "engagement" to carry information about both impredicativity of set and type in type. For the record: maybe some further checks to do around the sort of the inductive types in coqchk?
| * | Kernel: primitive projections handling of let-insGravatar Matthieu Sozeau2015-07-09
| | | | | | | | | | | | | | | | | | | | | Fixes bug #4176 (actually two bugs in one) Correct computation of the type of primitive projections in presence of let-ins.
| * | Template polymorphism: A bug-fix for Bug #4258Gravatar mlasson2015-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reviewed by M. Sozeau This commit fixes template polymorphism and makes it more precise, applying to non-linear uses of the same universe in parameters of template-polymorphic inductives. See bug report and https://github.com/coq/coq/pull/69 for full details. I also removed some deadcode in checker/inductive.ml. I do not know if it is also necessary to fix checker/indtypes.ml.
| | * Add a corresponding field in `mutual_inductive_entry` (part 2).Gravatar Arnaud Spiwack2015-06-24
| | | | | | | | | | | | The request for positivity to be assumed is honored.
| | * Add a corresponding field in `mutual_inductive_entry` (part 1).Gravatar Arnaud Spiwack2015-06-24
| | | | | | | | | | | | The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
| | * Add a field in `mutual_inductive_body` to represent mutual inductive whose ↵Gravatar Arnaud Spiwack2015-06-24
| |/ |/| | | | | positivity is assumed.
* | Document the positivity checker.Gravatar Arnaud Spiwack2015-06-23
|/ | | | This is my attempt at understanding each case and subfunction of the positivity check and document each of them to the best of my capacity.
* Fixing computation of non-recursively uniform arguments in theGravatar Hugo Herbelin2015-03-24
| | | | presence of let-ins. This fixes #3491.
* Fixing wrong rel_context in checking positivity condition.Gravatar Hugo Herbelin2015-03-24
| | | | | | | | | | Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas.
* Univs: When computing the level of an inductive including indices, letsGravatar Matthieu Sozeau2015-02-14
| | | | do not contribute. Fixes bug #3808.
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
| | | | | | constr for primitive records (not used anywhere else than printing). Problem reported by P. LeFanu Lumsdaine on HoTT/HoTT. Also add some minor fixes in detyping and pretty printing related to universes.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
| | | | | | Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
* Fix treatment of universe context in typecheck inductive (was addedGravatar Matthieu Sozeau2014-12-15
| | | | twice). Thanks to Marc Lasson for spotting this.
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
| | | | | | | inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
| | | | | inductive types + deactivate test for equality of sort + deactivate the check that the constraints Prop/Set <= Type are declared).
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
| | | | | | | for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array.
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Fix generation of inductive elimination principle for primitive records.Gravatar Matthieu Sozeau2014-09-10
| | | | Let r.(p) be a strict subterm of r during the guardness check.
* Fix primitive projections declarations for inductive records.Gravatar Matthieu Sozeau2014-09-05
|
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
| | | | | | | | | | | now done entirely using declare_mind, which declares the associated constants for primitive records. This avoids a hack related to elimination schemes and ensures that the forward references to constants in the mutual inductive entry are properly declared just after the inductive. This also clarifies (and simplifies) the code of term_typing for constants which does not have to deal with building or checking projections anymore. Also fix printing of universes showing the de Bruijn encoding in a few places.
* Add test-suite file. Compute the name for the record binder in theGravatar Matthieu Sozeau2014-08-29
| | | | eta-expanded version of a projection as before.
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
| | | | | | | | | | | Now kernel/indtypes builds the corresponding terms (has to be trusted) while translate_constant just binds a constant name to the already entered projection body, avoiding the dubious "check" of user given terms. "case" Pattern-matching on primitive records is now disallowed, and the default scheme is implemented using projections and eta (all elimination tactics now use projections as well). Elaborate "let (x, y) := p in t" using let bindings for the projections of p too.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Move to a representation of universe polymorphic constants using indices for ↵Gravatar Matthieu Sozeau2014-08-03
| | | | | | | variables. Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's. Abstraction by variables is handled mostly inside the kernel but could be moved outside.
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - 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
* - Do module substitution inside mind_record.Gravatar Matthieu Sozeau2014-07-25
| | | | | - Distinguish between primitive and non-primitive records in the kernel declaration, so as to try eta-conversion on primitive records only.
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
| | | | | | instantiated in the return predicate are now taken into account. The resulting recargs tree is the intersection between the one of the branches and the appearing in the return predicate. Both the domain and co-domain are filtered.
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
| | | | more than one constructor.
* Cleanup code related to the constraint solving, which sits now outside theGravatar Matthieu Sozeau2014-07-03
| | | | kernel in library/universes.ml.
* Fix computation of inductive level in monomorphism + indices-matter mode.Gravatar Matthieu Sozeau2014-06-20
| | | | Fixes bug #3346.
* Fix a destArity that does not exactly match isArity in presence of let-ins.Gravatar Matthieu Sozeau2014-06-17
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
| | | | problem with hashconsing at the same time. This fixes bug# 3302.
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
| | | | | | | | | | | | | | | | | | - Remove Universe Polymorphism flags everywhere. - Properly infer, discharge template arities and fix substitution inside them (kernel code to check for correctness). - Fix tactics that were supposing universe polymorphic constants/inductives to be parametric on that status. Required to make interp_constr* return the whole evar universe context now. - Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing, sadly losing most of its benefits. Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting all serialization code. Conflicts: kernel/univ.ml tactics/tactics.ml theories/Logic/EqdepFacts.v
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:07:56 +0000