aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
Commit message (Collapse)AuthorAge
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* Unify pre_env and envGravatar Maxime Dénès2018-05-28
| | | | | We now have only two notions of environments in the kernel: env and safe_env.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* New IR in VM: Clambda.Gravatar Maxime Dénès2018-02-23
| | | | | | | | | | | | This intermediate representation serves two purposes: 1- It is a preliminary step for primitive machine integers, as iterators will be compiled to Clambda. 2- It makes the VM compilation passes closer to the ones of native_compute. Once we unifiy the representation of values, we should be able to factorize the lambda-code generation between the two compilers, as well as the reification code. This code was written by Benjamin Grégoire and myself.
* Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Gravatar Maxime Dénès2018-01-23
|\ | | | | | | for primitive projections
* \ Merge PR #6506: Fast rel lookupGravatar Maxime Dénès2018-01-22
|\ \
| | * 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.
* | Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | | | | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
| * Fast environment lookup for rels.Gravatar Pierre-Marie Pédrot2017-12-29
|/ | | | | We take advantage of the range structure to get a O(log n) retrieval of values bound to a rel in an environment.
* [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 computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
|
* Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.Gravatar Hugo Herbelin2017-08-12
| | | | | Indeed OCaml has a similar file and this conflicts, at least in debugger.
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | | The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
* 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.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* 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 ```
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* 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.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2016-10-12
| |
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
| |
| * Removing the now useless field env_named_val from named_context_val.Gravatar Pierre-Marie Pédrot2016-09-09
| | | | | | | | | | This field was only used by the VM before, but since the previous patches, this part of the code relies on the map instead.
| * More efficient implementation of map_named_val.Gravatar Pierre-Marie Pédrot2016-09-09
| |
| * Tentative fast-access named envGravatar Pierre-Marie Pédrot2016-09-09
| |
| * Packing the named_context_val in a proper record and marking it private.Gravatar Pierre-Marie Pédrot2016-09-09
| |
* | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵Gravatar Matej Kosik2016-08-25
|/ | | | "Context.{Rel,Named}.fold_constr"
* 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
* Fix bug #4825: [clear] should not dependency-check hypotheses that come ↵Gravatar Pierre-Marie Pédrot2016-06-20
| | | | above it.
* Reuse the typing_flags datatype for inductives.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
|
* Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
|
* CLEANUP: Simplifying the changes done in "kernel/*"Gravatar Matej Kosik2016-02-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ... ... ... ... ... ... ... ... ... ... ... ... ... ...
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | 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
|\|
| * Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
| | | | | | | | declare new universes (e.g. with).
| * Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
| |
* | Assertion checking that invariant enforced by 0f8d1b92 always holds.Gravatar Maxime Dénès2015-09-10
|/ | | | | When reifying a 31-bit integer after a VM computation, we check that no bit outside the 31 LSB is set to 1.
* Fixing pop_rel_context.Gravatar Hugo Herbelin2015-08-02
| | | | This is necessary for the patch for #4221 (817308ab5) to work.
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* Fixing pop_rel_contextGravatar Hugo Herbelin2015-08-02
|
* 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?
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
| | | | more than 245 constructors (unsupported by OCaml's runtime).
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.