aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/util.ml
Commit message (Collapse)AuthorAge
* Util.Empty: implement using polymorphic record.Gravatar Gaëtan Gilbert2018-07-03
|
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Adding function to be typically used to pass values from an OCaml "when" clause.Gravatar Hugo Herbelin2017-09-12
|
* Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
|
* [safe-string] lib/miscelaneaGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | No functional change.js
* CLEANUP: switching from "right-to-left" to "left-to-right" function ↵Gravatar Matej Kosik2016-08-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | composition operator. Short story: This pull-request: (1) removes the definition of the "right-to-left" function composition operator (2) adds the definition of the "left-to-right" function composition operator (3) rewrites the code relying on "right-to-left" function composition to rely on "left-to-right" function composition operator instead. Long story: In mathematics, function composition is traditionally denoted with ∘ operator. Ocaml standard library does not provide analogous operator under any name. Batteries Included provides provides two alternatives: _ % _ and _ %> _ The first operator one corresponds to the classical ∘ operator routinely used in mathematics. I.e.: (f4 % f3 % f2 % f1) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "right-to-left" composition because: - the function we write as first (f4) will be called as last - and the function write as last (f1) will be called as first. The meaning of the second operator is this: (f1 %> f2 %> f3 %> f4) x ≜ (f4 ∘ f3 ∘ f2 ∘ f1) x We can call it "left-to-right" composition because: - the function we write as first (f1) will be called first - and the function we write as last (f4) will be called last That is, the functions are written in the same order in which we write and read them. I think that it makes sense to prefer the "left-to-right" variant because it enables us to write functions in the same order in which they will be actually called and it thus better fits our culture (we read/write from left to right).
* Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.Gravatar Hugo Herbelin2016-04-15
|
* Adding a few functions on type union.Gravatar Hugo Herbelin2016-03-13
|
* CLEANUP: Renaming "Util.compose" function to "%"Gravatar Matej Kosik2016-02-17
| | | | | | | | | | | I propose to change the name of the "Util.compose" function to "%". Reasons: 1. If one wants to express function composition, then the new name enables us to achieve this goal easier. 2. In "Batteries Included" they had made the same choice.
* Leveraging GADTs to provide a better Dyn API.Gravatar Pierre-Marie Pédrot2015-12-05
|
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
| | | | | | | | File system.ml seemed like a better choice than util.ml for sharing the code, but it was bringing a bunch of useless dependencies to the IDE. There are presumably several other tools that would benefit from using open_utf8_file_in instead of open_in, e.g. coqdoc.
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* Util.un_op -> Option.defaultGravatar Pierre Boutillier2014-12-14
|
* Searchxxx now search also the hypothesis and support goal selector.Gravatar Pierre Courtieu2014-12-12
| | | | Documentation also updated.
* Making map_union a standard function of the ML library.Gravatar Hugo Herbelin2014-11-19
|
* Adding a new Control file centralizing the control options of Coq.Gravatar Pierre-Marie Pédrot2014-06-07
|
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
|
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
|
* Allocation friendly version of Util.iterate.Gravatar ppedrot2013-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clib: fold_left_until added to CListGravatar gareuselesinge2013-10-10
| | | | | | | CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing some lone List.assoc & List.mem in lib.Gravatar ppedrot2013-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the type of Ltac values. Now they are toplevel genericGravatar ppedrot2013-06-12
| | | | | | | | | arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Quite ad-hoc for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphizationsGravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a CString module.Gravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
| | | | | | | | | | | | | | | | | the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
| | | | | | | | writing our own comparison functions, and enforcing monomorphization in many places. This should be more efficient, btw. Still a work in progress. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15932 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
| | | | | | peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added some tricky tail-rec versions of List functions to CListGravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert copy/pasted function in to minilib thanks to clib.cmaGravatar pboutill2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding newline after warning and restoring distinction betweenGravatar herbelin2012-04-15
| | | | | | fatal and non fatal identifier check errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
| | | | | | | | | | | | | | | | | | ?x[t1..tm] = ?y[u1..un] when ?x occurs in u1..un with no (easy) way to know if it occurs in rigid position or not. Such equations typically come from matching problems such as "match a return ?T[a] with pair a1 a2 => a1 end" where, a is in type "?A * ?B", and, in the branch, the return clause, of the form "?T[pair ?A ?B a1 a2]", has to be unified with ?A. This possible dependency is kept since commits r15060-15062. The heuristic is to restrict ?T so that the dependency is removed, leading to a behavior similar to the one existing before these commits. This allows BGsection15.v, from contrib Ssreflect, to compile as it did before these commits. Also, removed one function exported without true need in r15061. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
| | | | | | change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Yet another subtlety with bug 2732: when several grammar rules of aGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | TACTIC EXTEND block possibly parse the stand-alone name of a tactic, then only the first rule must be registered in the atomic tactic table so as to be consistent with what happens when the tactic is invoked directly via its parsing rules and not via the interpretation of a reference in the atomic tactic table. Concretely, this affects TACTIC EXTEND blocks of the form TACTIC EXTEND foo [ "bar" tactic_opt(tac) -> ... ] | [ "bar" constr_list(tac) -> ... ] where both rules parses "bar" alone but only the first rule must be registered in the atomic table, git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
| | | | | | | | | | instantiating them in the unification algorithm used for tactics. This allows to discard ill-typed uses of first-order unification which otherwise would have been fatal (this incidentally allows to partially restore some compatibility with 8.3 that was broken after eta was added in unification). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14812 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 13:04:23 +0000