aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/scheme.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [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
|
* 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.
* [safe-string] plugins/extractionGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | No functional change.
* Revert "Extraction: avoid deprecated functions of module String"Gravatar Pierre Letouzey2017-02-07
| | | | | | This reverts commit 69c4e7cfa0271f024b2178082e4be2e3ca3be263. String.capitalize_ascii are only available for ocaml >= 4.03, sorry...
* Extraction: avoid deprecated functions of module StringGravatar Pierre Letouzey2017-02-07
| | | | | - A few tweaks of string are now done via the Bytes module - lots of String.capitalize_ascii and co
* 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: 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.
* Fix some typos.Gravatar Guillaume Melquiond2015-04-02
|
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* 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
* 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
* 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
* 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
* 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
* 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: 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
* Extraction: Add missing parenthesis around emulated pattern-match (fix #2478)Gravatar letouzey2011-02-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13861 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction : fix Extract Inlined Constant for Haskell and Scheme (#2469)Gravatar letouzey2011-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
| | | | | | | | We now keep some type information in the "info" field of constructors and cases, and compact a match with some default branches (or remove this match completely) only if this transformation is type-preserving. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Library Foo creates Foo.ml, not foo.mlGravatar letouzey2010-07-07
| | | | | | | | | | And similarly for Haskell: we do not force capitalized/uncapitalized filenames anymore, but we rather follow the name of the .v file (with new extensions of course). Ok, this is an incompatible change, but it is really convenient, some people where actually already doing some hacks to have this behavior (cf. Compcert). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13260 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: (yet another) rework of the renaming codeGravatar letouzey2010-07-05
| | | | | | | | | | | | | | | - Add module parameters in the structure of visible_layer, in order for module params to be part of name clash detection, avoiding this way a source of potentially wrong code. - In case of clash, module params are alpha-renamed to something unique (Foo__XXX where XXX is the number contained in the mbid). This solves some situations that were unsupported by extraction. for instance the "Module F (X:T). Module X:=X. ... End F." - We now check in Coq identifiers the presence of the extraction-reserved string __. If it is found, we issue a warning (which might become an error someday). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: better support of modulesGravatar letouzey2010-07-02
| | | | | | | | | | | | | - For Haskell, modules abbreviations and applied functors are expanded. The only remaining sitation that isn't supported is extracting functors and applying them after extraction. - Add a module extraction for Scheme with the same capabilities as for Haskell (with no Extraction Library, though). - Nicer extracted module types (use of the mb.mod_type_alg if present) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13236 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: no more MPself hence no need for subst during ppGravatar letouzey2010-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
| | | | | | | | | | | For instance: Extract Inductive nat => int [ "0" "succ" ] "(fun fO fS n => if n=0 then fO () else fS (n-1))". See Extraction.v for more details and caveat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: ad-hoc identifier type with annotations for reductionsGravatar letouzey2010-04-16
| | | | | | | | | | | | | | | | * An inductive constructor Dummy instead of a constant dummy_name * The Tmp constructor indicates that the corresponding MLlam or MLletin is extraction-specific and can be reduced if possible * When inlining a glob (for instance a recursor), we tag some lambdas as reducible. In (nat_rect Fo Fs n), the head lams of Fo and Fs are treated this way, in order for the recursive call inside nat_rect to be correctly pushed as deeper as possible. * This way, we can stop allowing by default linear beta/let reduction even under binders (can be activated back via Set Extraction Flag). * Btw, fix the strange definition of non_stricts for (x y). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12938 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 20:54:33 +0000