aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\
| * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |
* | 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.
* | Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | This ought to ease the understanding of the code.
* | Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | This was an easy to prove property that I somehow overlooked.
* | Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | This is actually useless, the code does not depend on the value of the entry for side-effects.
* | Remove a horrendous hack in Declare to retrieve exported side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | | | Instead of relying on a mutable state in the object pushed on the libstack, we export an API in the kernel that exports the side-effects of a given entry in the global environment.
* | More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
| | | | | | | | | | We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants.
* | Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
| |
* | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
|/ | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
* [api] Put modules in order in API.{mli,ml}Gravatar Emilio Jesus Gallego Arias2017-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We sort the dependency graph of API by following a logical declaration order in `API.{ml,mli}` related to the actual dependency order of Coq modules. Things are a bit tricky here as Coq itself relies on the fact that OCaml treats module interface and implementation separately dependency-wise; however, when resorting module alias the design seems to become more coupled. Currently, API exposes both "namespaces", asserting a large number of type equality between them, however the `API` namespace is not self-contained. In particular, this is a first step to solve problems such as `Summary.frozen` being used in `API.mli` but not declared by the `API.Summary` module, etc... In general we follow the invariant that a type used in `API` must have been declared before. Keep in mind that OCaml upstream has warned that it maybe tricky to alias objects in this way. In particular, after API the old `mli` only files have become full compilation units so we may want to be more careful here. The more "correct" declaration order allows us to remove the `API.Prelude` module, as well as some other declarations that I consider as spurious. We still maintain the large number of type aliases which will be removed in a future patch. We follow linking order except for files in `intf`, which are conceptually wrongly placed in the linking hierarchy but this doesn't matter as the files don't contain any implementation. We also move a couple of `.mli` only files to `.ml` so we are consistent, and correct their linking order in `mllib`, even if that doesn't matter as such `.ml`-only files contain no implementations.
* Merge PR #783: Remove some useless code in Term_typingGravatar Maxime Dénès2017-07-17
|\
* | The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
| |
* | Adding a comment regarding De Bruijn universe indices in the kernel.Gravatar Pierre-Marie Pédrot2017-07-12
| |
* | Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| |
* | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | | | The function turning a side-effect declaration into the corresponding entry was crazily wrong, as it used a named universe context quantifying over DeBruijn universe indices. Declaring such entries resulted in random anomalies. This fixes bug #5641.
* | Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
* | Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | | | | | We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
* | 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.
* | Asserting that monomorphic section variables have no abstracted context.Gravatar Pierre-Marie Pédrot2017-07-11
| |
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | | | | | This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
* | Removing a redundant universe instance information in native compute.Gravatar Pierre-Marie Pédrot2017-07-10
| | | | | | | | | | | | Global declarations used to carry universe instances with them, but it turns out this information is not used anywhere. Instead, instances were already properly encoded as the first argument of polymorphic definitions.
* | Merge PR #853: Clean 'with Definition' implementation.Gravatar Maxime Dénès2017-07-06
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
| * | Removing dead code in Subtyping.Gravatar Pierre-Marie Pédrot2017-07-04
| | | | | | | | | | | | | | | | | | | | | This code was a sketch of what to do when we properly implement module-level handling of instanciation of definitions by inductive types. It was completely dead code, called after an error, and somewhat incorrect. Instead of letting it bitrot, we remove it.
| * | Removing a few suspicious functions from the kernel.Gravatar Pierre-Marie Pédrot2017-07-03
| | | | | | | | | | | | | | | | | | These functions were messing with the deferred universe constraints in an error-prone way, and were only used for printing as of today. We inline the one used by the printer instead.
| * | Do not add original constraints to the environment in 'with Definition' check.Gravatar Pierre-Marie Pédrot2017-07-03
|/ / | | | | | | | | | | | | | | | | | | This was useless, because immediate constraints are assumed to already be in the current environment, while deferred constraints are useless for the conversion check of the definition types, as they only appear in the opaque body. This also clarifies a bit what is going on in the typing of module constraints w.r.t. global universes.
* | Fix a bug in cumulativityGravatar Amin Timany2017-06-16
| |
* | A short cleanupGravatar Amin Timany2017-06-16
| |
* | use map_constr more efficientlyGravatar Amin Timany2017-06-16
| |
* | OptimizationGravatar Amin Timany2017-06-16
| | | | | | | | | | Only try using cumulativity in conversion/subtyping if the universe instances are non-empty
* | Use a smart map_constrGravatar Amin Timany2017-06-16
| |
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
| |
* | Move univops from kernel to libraryGravatar Amin Timany2017-06-16
| |
* | Simplify Univ.mlGravatar Amin Timany2017-06-16
| |
* | Disable debug printingGravatar Amin Timany2017-06-16
| | | | | | | | Fix a mistake in record declaration
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
| |
* | Fix bugsGravatar Amin Timany2017-06-16
| |
* | Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany <amintimany@gmail.com> Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany <amintimany@gmail.com> Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany <amintimany@gmail.com> Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany <amintimany@gmail.com> Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany <amintimany@gmail.com> Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints.
* | Fix cum/conv for inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | | Fall back to the equating levels in case inductive is not fully applied instead of failing.
* | Use inductive subtyping for conv/cumulGravatar Amin Timany2017-06-16
| |
* | Add subtyping inference for inductive typesGravatar Amin Timany2017-06-16
| |
* | Correct subtyping check for constructorsGravatar Amin Timany2017-06-16
| |
* | Fix typo in error messageGravatar Amin Timany2017-06-16
| |
* | Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
| |
* | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
* | New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
| |
* | Extend definition of inductives to include subtyping infoGravatar Amin Timany2017-06-16
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 23:43:16 +0000