aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/common.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* [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
|
* Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* [pp] Remove `Pp.stras`.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | Mostly unused, we ought to limit spacing in the boxes themselves.
* [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
* Extraction : get_duplicates (via option) instead of check_duplicates (via ↵Gravatar Pierre Letouzey2017-02-07
| | | | | | Not_found) This clarifies the execution flow
* CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
| | | | | | | The word "increment" is more appropriate in this case than "lifting". The world "lifting", in computer science, usually denotes something else: https://en.wikipedia.org/wiki/Lambda_lifting
* Extraction: code cleanup in CommonGravatar Pierre Letouzey2016-05-20
|
* Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)Gravatar Pierre Letouzey2016-05-19
|
* 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 _)
* JSON extraction: construct full names (dot-separated) in pp_globalGravatar Nickolai Zeldovich2015-04-09
| | | | This is important to disambiguate identical names from different modules.
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch allows Coq terms to be extracted into the widely used JSON format. This is useful in at least two cases: - One might want to manipulate Coq values outside of Coq, but without being forced to use one of the three existing extraction languages (OCaml, Haskell, or Scheme), and without having to compile Coq's extracted result. This is especially useful when a Coq evaluation produces some data structure that needs to be moved out of Coq. Having to invoke an OCaml/Haskell/Scheme compiler just to get a data structure out of Coq is somewhat awkward. - One might want to experiment with extracting Coq code into other languages (Go, Javascript, etc), without having to write the whole extraction logic in OCaml and recompile Coq's extraction plugin each time. This makes it easy to quickly prototype extraction in any language, without having to build Coq from source. Extraction to JSON is implemented by adding the JSON "pseudo-language" to the extraction facility. Thus, one can extract the JSON encoding of a single term using: Extraction Language JSON. Extraction qualid. and extract an entire Coq library "ident" into "ident.json" using: Extraction Language JSON. Extraction Library ident. Nota (Pierre Letouzey) : this is an updated version of the original PullRequest, updated to match recent changes in trunk
* Fix specialized extraction of ascii characters into Haskell. (Fix bug #4181)Gravatar Nickolai Zeldovich2015-04-08
| | | | | | | | | | | The extraction machinery has specialized support for extracting [ascii] characters into native characters in the target language, as opposed to using an explicit constructor from 8 boolean bits. This works by hard-coding the name of the character type in the target language. Unfortunately, the hard-coded type for Haskell was "Char", not the fully-qualified "Prelude.Char". As a result, it was impossible to extract characters into Haskell without getting type errors about "Char". This patch changes this hard-coded name to "Prelude.Char".
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Extraction: minor tweaks to ease ongoing experiments about LambdaGravatar Pierre Letouzey2015-01-11
| | | | | | - Common.get_native_char instead of just a pp function of this char - Enrich the record projection table
* Fixing Pervasives.equality in extraction.Gravatar Pierre-Marie Pédrot2014-03-03
|
* 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
* Removing Gmap from Extraction pluginGravatar ppedrot2013-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16511 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 mod_bound_idGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 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
* 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
* 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
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)Gravatar letouzey2012-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15525 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: global reference should be indexed on their user part (fix #2540)Gravatar letouzey2011-05-19
| | | | | | | | | Since in Extract_env we recreate constant and mind whose canonical part might be inaccurate, we shouldn't use an Hashtbl on global_reference derived from these constant and mind, otherwise equivalent refs could be considered distinct. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14141 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: fix printing of haskell modular namesGravatar letouzey2011-03-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: improved indentation of extracted code (fix #2497)Gravatar letouzey2011-03-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For Haskell, we still try to provide readable indentation, but we now avoid relying on this indentation for correctness. Instead, we use layout-independant syntax with { } when necessary (after "case of" and "let"). It is much safer this way, even if the syntax gets a bit more cumbersome. For people allergic to {;}, they can most of the time do a tr -d "{;}" without changing the meaning of the program. Be careful nonetheless: since "case of" is now delimited, some parenthesis that used to be mandatory are now removed. Note also that the initial "module ... where" is still without { }: even when Format goes crazy it doesn't tamper with column 0. Other modifications: - Using "Set Printing Width" now affects uniformly the extraction pretty-printers. You can set a greater value than the default 78 before extracting a program that you know to be "really deep". - In ocaml (and also a bit in Haskell), we now try to avoid abusing of 2-char-right-indentation. For instance | is now aligned with the "m" of match. This way, max_indent will be reached less frequently. - As soon as a pretty-print box contains an explicit newline, we set its virtual size to a big number, in order to prevent this box to be part of some horizontal arrangement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code in extractionGravatar letouzey2010-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: multiple fixes related with the Not_found encountered by X. LeroyGravatar letouzey2010-09-17
| | | | | | | | | | | | | | | | | | | Cf. coqdev for the details of the bug report. - Protect some Hashtbl.find and other risky functions in order to avoid as much as possible to end with an irritating Anomaly : Not_found. - Re-enable in pp_ocaml_extern the case of a module-file used as a module (e.g. module A' := A for A.v) when doing modular extraction. - Rework the code that decides to "open" or not modules initially: opening A when A contains a submodule B hides the file B even when B isn't opened itself, we avoid that now. - Fix some tables (sets or maps) used by extraction for which it is critical to consider constants/inductives/global_reference _not_ modulo the equivalence of Elie, but rather via Pervasives.compare. Still to do : avoid appearance of '_a in extracted code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13424 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: fix a bit the extraction under modulesGravatar letouzey2010-07-15
| | | | | | | | | | | | | | | | | | Extraction under modules is highly experimental, and just work a bit. Don't expect too much of it. With this commit, I simply avoid a few "assert false" to occur when we are under modules. But things are still quite wrong, for instance with: Definition foo. Module M. Definition bar := foo. Recursive Extraction bar. Extraction of bar is ok, but foo isn't displayed, since extraction can't get it: Lib.contents_after doesn't mention it, it is probably in some frozen summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: some more work on the (re)naming frameworkGravatar letouzey2010-07-07
| | | | | | | | | | | | | - MPbound can be part of visible_mps (when printing the type of a module parameter, or when printing body of a With), hence the locality test base_mp mp = base_mp (top_visible_mp ()) isn't accurate. - new organisation, pp_ocaml_gen is splitted in many sub-functions, attempt to be clearer - the shortcut (if List.length ls = 1 then ...) isn't safe, we might detect name conflict even in this case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13248 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 05:10:13 +0000