aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
|
* Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
|
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| | | | | | | | | | Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
| |
| * 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-29
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|
* mergeGravatar Matej Kosik2016-01-11
|\
| * 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.
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
| | | | | | | | | | Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
| |
* | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
| |
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|/
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
|
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
|
* API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|
* Fixing compilation of mli documentation.Gravatar Hugo Herbelin2015-12-05
| | | | | Using dummy comment to @raise to please ocamldoc. Please change MS or PMP, if needed.
* Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file.
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
| | | | | | | | | | Redefining adjust_subst_to_rel_context from instantiate_context who was hidden in inductiveops.ml, renamed the latter into subst_of_rel_context_instance and moving them to Vars. The new name highlights that the input is an instance (as for applist) and the output a substitution (as for substl). This is a clearer unified interface, centralizing the difficult de-Bruijn job in one place. It saves a couple of List.rev.
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
| | | | | next to each other, waiting for possible integration into a more uniform API.
* Remove unneeded fixpoint in normalize_context_set. Note that it is noGravatar Matthieu Sozeau2015-12-01
| | | | | | longer stable w.r.t. equality constraints as the universe graph will choose different canonical levels depending on the equalities given to it (l = r vs r = l).
* More efficient implementation of equality-up-to-universes in Universes.Gravatar Pierre-Marie Pédrot2015-11-26
| | | | | | Instead of accumulating constraints which are not present in the original graph, we parametrize the equality function by a function actually merging those constraints in the current graph. This prevents doing the work twice.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|
* More invariants in UState.Gravatar Pierre-Marie Pédrot2015-11-26
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|
* Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|
* Removing some unsafe uses of monotonicity.Gravatar Pierre-Marie Pédrot2015-10-19
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-19
|
* Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18
|
* Clarifying and documenting the UState API.Gravatar Pierre-Marie Pédrot2015-10-17
|
* Dedicated file for universe unification context manipulation.Gravatar Pierre-Marie Pédrot2015-10-17
| | | | | | | This allows to remove a lot of independent code from Evd which was put into the UState module. The API is not perfect yet, but this is a first pass. Names of data structures should be thought about too because they are way too similar.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|
* 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-06
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|
* Removing meta_with_name from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing subst_defined_metas_evars from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|
* Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| | | | | | The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap.
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|
* Fix documentation.Gravatar Matthieu Sozeau2015-07-27
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|