aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/ocaml.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* allow :: and , as infix opsGravatar Paul Steckler2017-11-27
|
* allow whitespace around infix opGravatar Paul Steckler2017-11-22
|
* use OCaml criteria for infix ops, #6212Gravatar Paul Steckler2017-11-22
|
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
* Extraction cosmetic: no whitespaces in printing empty modulesGravatar Pierre Letouzey2017-02-07
|
* Extraction: simplify the generated code for difficult name conflictsGravatar Pierre Letouzey2017-02-07
| | | | | | No more pp_alias_spec et pp_alias_decl. Instead, we use "include" and "module type of". The extracted code might hence need OCaml 3.12 (quite rarely)
* Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Gravatar Pierre Letouzey2017-02-07
| | | | | | Not_found) This clarifies the execution flow
* Extraction: fix complexity issue #5310Gravatar Pierre Letouzey2017-02-07
| | | | | | | | | | | | | | | | | | | | | | | | A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
* 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
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Extraction: fix a few little glitches with my last commit (replacing unused ↵Gravatar Pierre Letouzey2015-12-15
| | | | vars by _)
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
|
* Extraction: fix a pretty-print issueGravatar Pierre Letouzey2015-12-14
| | | | | Some explicit '\n' in Pp.str were interacting badly with Format boxes in Compcert, leading to right-flushed "sig..end" blocks in some .mli
* Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")Gravatar Pierre Letouzey2015-12-14
|
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
| | | | | | | | | | | | | | | | | | | Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly.
* Extraction: avoid generating some blanks at end-of-lineGravatar Pierre Letouzey2015-12-12
|
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
|
* Fix previous commit on extraction.Gravatar Maxime Dénès2015-01-23
| | | | | Since name clashes are discovered by side effects, the order of traversal of module structs cannot be changed.
* Extraction: fix #3629.Gravatar Maxime Dénès2015-01-23
| | | | | | The control flow of extraction is hard to read due to exceptions. When meeting an inlined constant extracted to custom code, they could desynchronize some tables in charge of detecting name clashes, leading to an anomaly.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Extraction: no more ascii blob in type variables (fix #3227)Gravatar Pierre Letouzey2015-01-11
| | | | | | Since type variables are local to the definition, we simply rename them in case of unicode chars. We also get rid of any ' to avoid Ocaml illegal 'a' type var (clash with char litteral).
* 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
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dir_path --> DirPathGravatar letouzey2013-02-19
| | | | | | | | Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of LabelGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid initial strange empty comments after Arnaud's hackGravatar letouzey2012-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15942 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
* 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
* 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
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 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
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | | | | Scheme comments are output on a single line because Ocaml's Format module which serves as a backend to Pp has an integer, rather than a string as identation value, so we cannot make it so that each new line in the comment starts with ";; ". I've tried something with Pp.ifb but it was hackish at best and had somewhat strange results. Known bug: as Pp.std_ppcmds is non-persistent, the comment is actually printed only once per Extraction command, even if it outputs several files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15763 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 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
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
| | | | | | | | | | | | | | | | | The MLcase has notably changed: - No more case_info in it, but only a type annotation - No more "one branch for one constructor", but rather a sequence of patterns. Earlier "full" pattern correspond to pattern Pusual. Patterns Pwild and Prel allow to encode optimized matchs without hacks as earlier. Other pattern situations aren't used (yet) by extraction, but only by P.N Tollitte's code. A MLtuple constructor has been introduced. It isn't used by the extraction for the moment, but only but P.N. Tollitte's code. Many pretty-print functions in ocaml.ml and other have been reorganized git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: allow extraction of records with anonymous fields (fix #2555)Gravatar letouzey2011-08-25
| | | | | | | | | | For Ocaml, we now use the extraction-reserved substring "__" : The name foo__i will be pick for i-th field of record foo if it is anonymous. For Haskell, still no printing of records as native records, hence nothing to do. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Set Extraction KeepSingleton: an option for not decapsulating singleton typesGravatar letouzey2011-07-04
| | | | | | | | | | | | A informative inductive type with one constructor C and one informative arg to C is normally extracted as an identity, with C removed, see for example the "sig" type. When this new option is set, these singleton types are left untouch, providing extracted code which is closer to the initial Coq development. Feature requested by Wouter Swiestra. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid lots of late mind_of_knGravatar letouzey2011-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14142 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: allow extracting Ascii.ascii to native Char in Haskell (fix #2515)Gravatar letouzey2011-04-15
| | | | | | We simply factorize code that was already existing for Ocaml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid printing unused mutual fix components (fix #2477)Gravatar letouzey2011-03-07
| | | | | | | This happens for instance when the main component of the fixpoint block has been provided via Extract Constant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13889 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 05:19:42 +0000