aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* [VM] Unify Const_sorts and Const_type, and remove Vsort.Gravatar Maxime Dénès2018-03-02
| | | | | This simplifies the representation of values, and brings it closer to the ones of the native compiler.
* comment "resolvability" bit in Evd.evar_mapGravatar Enrico Tassi2018-02-27
|
* Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Maxime Dénès2018-02-24
|\
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | | | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* | Merge PR #6767: [ci] add elpiGravatar Maxime Dénès2018-02-21
|\ \
| | * Fixes bug #6774 (anomaly with ill-typed template polymorphism).Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | Computation of the sort of the inductive type was done before ensuring that the arguments of the inductive type had the correct types, possibly brutally failing with `NotArity` in case one of the types expected to be typed with an arity was not so.
* | | Using an "as" clause when needed for printing irrefutable patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | Example which is now reprinted as parsed: fun '((x,y) as z) => (y,x)=z
* | | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"...
* | | Canonically add an encoding in glob_constr of "as" operator for cases_pattern.Gravatar Hugo Herbelin2018-02-20
| | |
* | | Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
| * pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
|/
* Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\
* | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | | | | | | No using a mutable counter to skip them, instead we keep them in the environment.
* | Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | | | | | | | | The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
| * detype_case predicate is not optionalGravatar Gaëtan Gilbert2018-02-14
|/
* Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\
* \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ | | | | | | | | | information.
* \ \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \ \
* \ \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \ \
| | | * | inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
| | | | |
| | | * | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
| | | * | Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
| | | | |
| | | * | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
| | | * | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | | |
| | | * | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
| | | * | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
| |_|/ / |/| | |
* | | | Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \
| | | * | More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
| | | | |
* | | | | [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
| | | | |
* | | | | [native_compute] Remove useless conversion to list in reification.Gravatar Maxime Dénès2018-02-05
| |_|/ / |/| | |
| * | | Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
|/ / /
* | | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \ \
| | * | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
* | | Merge PR #6666: Fix reduction of primitive projections on coinductive ↵Gravatar Maxime Dénès2018-01-30
|\ \ \ | | | | | | | | | | | | records for cbv and native_compute
| * | | [cbv] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| | | | | | | | | | | | | | | | Fixes #5286 (last remaining part).
* | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.
* | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Gravatar Maxime Dénès2018-01-23
|\ \ \ | | | | | | | | | | | | for primitive projections
| * | | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The constant_value function was actually not behaving the same as constant_value_in w.r.t. projections. The former was not used, and the only place that used the latter was in Tacred and was statically insensitive to the use of projections.
* | | | Fix context handling of fix and cofix in Ltac subterm matching.Gravatar Cyprien Mangin2018-01-19
| | | |
* | | | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
|/ / /
| * | Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
| | | | | | | | | | | | | | | | | | | | | We simply use a record and pack the rel and var substitutions in it. We also properly compose variable substitutions. Fixes #6534: Fresh variable generation in case of clash is buggy.
* | | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
| | | | | | | | | | | | | | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
* | | Using a dedicated type for Lib.abstr_info.Gravatar Pierre-Marie Pédrot2017-12-30
|/ /
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
| | | | | | | | | | | | Some code in typeclasses was even breaking the invariant that use_polymorphic_flag should not be called twice, but that code was morally dead it seems, so we remove it.
* | Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.Gravatar Maxime Dénès2017-12-27
|\ \
* \ \ Merge PR #6289: Remove unused boolean from cl_context field of ↵Gravatar Maxime Dénès2017-12-27
|\ \ \ | | | | | | | | | | | | Typeclasses.typeclass
| | * | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| |/ / |/| | | | | | | | | | | | | | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
* | | Merge PR #6436: Fix #5368: Canonical structure unification fails.Gravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \ \ \
| | * | | Fix #5368: Canonical structure unification fails.Gravatar Pierre-Marie Pédrot2017-12-15
| |/ / / |/| | | | | | | | | | | Universe instances were lost during constructions of the canonical instance.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 02:19:56 +0000