aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Collapse)Author
2013-05-30bwaa, a Pervasive.comparepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16542 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Removing Gmap from Extraction pluginppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16511 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Use the Hook module here and there.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-22code simplifications concerning Summaryletouzey
- Most of the time, the table registered via Summary.declare_summary is just a single reference. A new function Summary.ref now allows to both declare this ref and register it to summary in one shot. - Clarifications concerning the role of [init_function]. For statically registered tables that don't need a special initializer, just do nothing there (see the new Summary.nop function). Beware: now that Summary exports a function named "ref", any code that do an "open Summary" will probably fail to compile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-18Extraction AccessOpaque is now activated again by default (#2952)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16315 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16306 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16285 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26kernel/declarations becomes a pure mliletouzey
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16249 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16248 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
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
2013-02-19Classops : avoid some use of Gmapletouzey
Gmap uses Pervasives.compare which may interact badly with structures like pairs of kernel names For the moment, we consider elements in classes and coercions only according to their user kernel name: this provides maximal compatibility. But it could be interesting to try using comparision according to canonical kernel names... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16218 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18use List.rev_map whenever possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Extraction: same as commit 16203, hopefully without NotASort exnsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16209 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-14Fix extraction of inductive types that Coq auto-detects to be in Propletouzey
Typical example : Inductive t := T : t -> t. Earlier, the extraction was using a shortcut to get the sort of t (via some mind_arity stuff), but this was producing a less precise answer (here InType) than a full Retyping.get_sort_family_of (here InProp since t is a singleton type, with no content). The extraction of t was hence awkward, since the type of the constructor T was computed with the precise method, and its argument was optimized out. Now the whole t is considered logical by the extraction. NB: to avoid this clever but highly non-intuitive behavior of Coq placing the above t in Prop, for the moment you have to fix its sort, for instance: Inductive t : Set := T : t -> t. Using Type instead of Set still activates Coq's minimal sort detection... Instead, you could also use one specific TypeX obtained via Definition TypeX := Type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16203 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Array.create is deprecatedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16104 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of nameppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of mod_bound_idppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16098 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of Labelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16089 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-17Extraction of projections: restrict a hack to ocaml only (fix #2941)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16074 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of dir_pathppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Added a CString module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Extraction Implicit: consider the parameters of a constructor (fix #2905)letouzey
The parameters of a constructor C are part of the type of C, we should take them in account when retrieving the argument(s) declared as implicit. This way, the Extraction Implicit should now be correct when given named arguments of constructors with parameters. When positional numbers are given to Extraction Implicit, these numbers should now be increased by the number of parameters for this constructor. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15943 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15942 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-30Fix Separate extraction when a module-as-file is aliased (#2917)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15940 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15818 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-18Cleaning interface of Util.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15817 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
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
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
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
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
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
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
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
2012-08-24Fix Extraction Implicit on axioms.aspiwack
There was a small bug causing the type in OCaml commentary not to honor the implicit declaration, whereas the rest of the code did. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15764 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
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
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
Extracted code need not preserve typing relations (e:t) from the source code. This may be a problem as the extracted code may not implement the intented interface. This option disables the optimisations which would prevent an extracted term's type to be its extracted source term's type. At this point the only such optimization is (I think) removing some dummy λ-abstractions in constant definitions. Extraction Implicit is still honored in this mode, and it's mostly necessary to produce reasonable types. So in the conservative type mode, which abstractions can be removed and which can'tt is entirely under the user's control. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15762 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
So PrintName and Extraction dump globals when they exist git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15691 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Dump references in Extractionpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15682 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Dump referencespboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15679 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15525 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-01More cleaningppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:47:03 +0000