aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
Commit message (Collapse)AuthorAge
* Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ | | | | | | constructs.
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/ | | | | | We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2Gravatar Maxime Dénès2017-11-16
|\
* | [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | | | | | We do up to `Term` which is the main bulk of the changes.
| * Use GHC.Base.Any for compatibility with GHC 8.2Gravatar Tej Chajed2017-10-25
|/ | | | Fixes #6022.
* Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
* Merge PR #1118: Extraction : minor support stuff for the new Extraction ↵Gravatar Maxime Dénès2017-10-06
|\ | | | | | | Compute plugin
* | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Gravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
| * Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-10-04
|/ | | | See https://github.com/letouzey/extraction-compute for more details
* 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).
* Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ | | | | | | work better on them
* | Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
| | | | | | | | | | | | | | | | As explained in edf85b9, the original commit that merged the module_body and module_type_body representations, this was delayed to a later time assumedly due to OCaml lack of GADTs. Actually, the only thing that was needed was polymorphic recursion, which has been around already for a relatively long time (since 3.12).
| * Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
|/
* Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
* \ \ Merge PR #889: Removing template polymorphism for definitions.Gravatar Maxime Dénès2017-07-28
|\ \ \
| | * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | |
| | | * Extraction: reduce primitive projections in types (fix bug 4709)Gravatar Pierre Letouzey2017-07-26
| |_|/ |/| |
* | | Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs ↵Gravatar Maxime Dénès2017-07-26
|\ \ \ | |_|/ |/| | | | | 4844 and 4824)
| | * Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* | Merge PR #905: [api] Remove type equalities from API.Gravatar Maxime Dénès2017-07-26
|\ \
* \ \ Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\ \ \
* \ \ \ Merge PR #859: Extraction TestCompileGravatar Maxime Dénès2017-07-26
|\ \ \ \
| | | * | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
| | | * Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs ↵Gravatar Pierre Letouzey2017-07-25
| |_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 4844 and 4824) The commit 8e257d4 (which consider the dummy type Tdummy to be polymorphic and hence immune of the need for unsafeCoerce) is quite wrong, even if in pratice it worked ok most of the time. The confusion comes from the fact that the dummy value (__ aka MLdummy internally) is implemented in Haskell as Prelude.error, hence it has indeed a polymorphic unrestricted type. But the dummy type Tdummy used when extracting types must be monomorphic (otherwise type parameters would have to be propagated out of any type definition involving Tdummy). We implement Tdummy by Haskell's (), which for instance isn't convertible to Any, as shown by the examples in bug reports 4844 and 4824. This fix will bring back some more unsafeCoerce in Haskell extraction, including possibly a few spurious ones. And these extra unsafeCoerce might also hinder further code optimisations. We tried to mitigate that by directly removing [MLmagic] constructors in front of [MLdummy _]. NB: even if the original bug report mentions universe polymorphism, this issue is almost unrelated to it. It just happens that when universe polymorphism is off, an inductive instance is fully placed in Prop (cf. template polymorphism) in the example, avoiding triggering the issue. Warning: the test-suite file is there for archiving the repro case, but currently it doesn't test much (we should run ghc on the extracted code).
| | * Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | Avoid Anomaly (or Assert False) when a module signature contains an applied functor followed by a "with Definition" or "with Module" Also fix the dependency computation in presence of a "with Definition" Concerning 4720, the code extracted out of this bug report was suboptimal in Coq 8.4 (it was compilable, but could have probably been tweaked into a real issue producing faulty code). But the example of 4720 (and some variants of it) was broken since 8.5, for the same reasons as 5177 and 5240. And the good news is that after these repairs, the example of bug 4720 is now extracted to correct code (the "with" is preserved).
* | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| |
* | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| |
| * Extraction TestCompile foo : a new command for extraction + ocamlcGravatar Pierre Letouzey2017-07-05
|/ | | | | | | | | | | | | Extraction TestCompile foo is equivalent to: Extraction "/tmp/testextraction1234.ml" foo ocamlfind ocamlc -I /tmp -c /tmp/testextraction1234.mli /tmp/testextraction1234.ml This command isn't meant for the end user, but rather as an helper for test-suite scripts. It only works with extraction to OCaml, and the generated code should be standalone.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* Merge PR#718: API cleanup: aliasesGravatar Maxime Dénès2017-06-12
|\
* | Remove remaining vo.itarget files (obsolete since PR #499)Gravatar Pierre Letouzey2017-06-10
| |
| * Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
|/
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Maxime Dénès2017-05-30
|\
| * 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]
* | [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.
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/ | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\
| * Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | This reverts commit 6d2802075606dcddb02dd13cbaf38ff76f8bf242, which is an 8.6 only commit.
| * Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
| |\
| | * Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
| | | | | | | | | | | | | | | This way, after we merge PR#220, scripts can be fixed in a way that is compatible with the 8.6 and trunk branches.
| * | [extraction] Flush formatters at end of output.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | Previous implementations of `Pp` flushed on newline, however, depending on the formatter this may not be always the case. We now alwayas flush the formatters before closing the file as this is the intended behavior.