From 40c483a95f354e457e10d00951fd6a8eec08176d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Mon, 5 Nov 2018 13:32:36 -0800 Subject: Document undocumented flags and options Also remove a few undocumented settings --- doc/sphinx/addendum/extraction.rst | 48 +++++++++++++++++++++++++++++++++- doc/sphinx/addendum/type-classes.rst | 50 ++++++++++++++++++++++++------------ 2 files changed, 80 insertions(+), 18 deletions(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index b7d05fd6ef..8891234330 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -164,7 +164,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: .. cmd:: Extraction Inline {+ @qualid } In addition to the automatic inline feature, the constants - mentionned by this command will always be inlined during extraction. + mentioned by this command will always be inlined during extraction. .. cmd:: Extraction NoInline {+ @qualid } @@ -410,6 +410,52 @@ It is possible to instruct the extraction not to use particular filenames. For |OCaml|, a typical use of these commands is ``Extraction Blacklist String List``. +Additional settings +~~~~~~~~~~~~~~~~~~~ + +.. opt:: Extraction File Comment @string + :name: Extraction File Comment + + Provides a comment that is included at the beginning of the output files. + +.. opt:: Extraction Flag @num + :name: Extraction Flag + + Controls which optimizations are used during extraction, providing a finer-grained + control than :flag:`Extraction Optimize`. The bits of *num* are used as a bit mask. + Keeping an option off keeps the extracted ML more similar to the Coq term. + Values are: + + +-----+-------+----------------------------------------------------------------+ + | Bit | Value | Optimization (default is on unless noted otherwise) | + +-----+-------+----------------------------------------------------------------+ + | 0 | 1 | Remove local dummy variables | + +-----+-------+----------------------------------------------------------------+ + | 1 | 2 | Use special treatment for fixpoints | + +-----+-------+----------------------------------------------------------------+ + | 2 | 4 | Simplify case with iota-redux | + +-----+-------+----------------------------------------------------------------+ + | 3 | 8 | Factor case branches as functions | + +-----+-------+----------------------------------------------------------------+ + | 4 | 16 | (not available, default false) | + +-----+-------+----------------------------------------------------------------+ + | 5 | 32 | Simplify case as function of one argument | + +-----+-------+----------------------------------------------------------------+ + | 6 | 64 | Simplify case by swapping case and lambda | + +-----+-------+----------------------------------------------------------------+ + | 7 | 128 | Some case optimization | + +-----+-------+----------------------------------------------------------------+ + | 8 | 256 | Push arguments inside a letin | + +-----+-------+----------------------------------------------------------------+ + | 9 | 512 | Use linear let reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + | 10 | 1024 | Use linear beta reduction (default false) | + +-----+-------+----------------------------------------------------------------+ + +.. flag:: Extraction TypeExpand + + If set, fully expand Coq types in ML. **see type_expand in mlutil.ml** + Differences between |Coq| and ML type systems ---------------------------------------------- diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 98dfcb2373..7933cdaee0 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -461,12 +461,12 @@ type, like: This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -Options -~~~~~~~ +Settings +~~~~~~~~ .. flag:: Typeclasses Dependency Order - This option (on by default since 8.6) respects the dependency order + This flag (on by default since 8.6) respects the dependency order between subgoals, meaning that subgoals on which other subgoals depend come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in @@ -475,7 +475,7 @@ Options .. flag:: Typeclasses Filtered Unification - This option, available since Coq 8.6 and off by default, switches the + This flag, available since Coq 8.6 and off by default, switches the hint application procedure to a filter-then-unify strategy. To apply a hint, we first check that the goal *matches* syntactically the inferred or specified pattern of the hint, and only then try to @@ -483,13 +483,13 @@ Options improve performance by calling unification less often, matching syntactic patterns being very quick. This also provides more control on the triggering of instances. For example, forcing a constant to - explicitely appear in the pattern will make it never apply on a goal + explicitly appear in the pattern will make it never apply on a goal where there is a hole in that place. .. flag:: Typeclasses Limit Intros - This option (on by default) controls the ability to apply hints while + This flag (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction. @@ -503,16 +503,16 @@ Options .. flag:: Typeclass Resolution For Conversion - This option (on by default) controls the use of typeclass resolution + This flag (on by default) controls the use of typeclass resolution when a unification problem cannot be solved during elaboration/type - inference. With this option on, when a unification fails, typeclass + inference. With this flag on, when a unification fails, typeclass resolution is tried before launching unification once again. .. flag:: Typeclasses Strict Resolution - Typeclass declarations introduced when this option is set have a - stricter resolution behavior (the option is off by default). When + Typeclass declarations introduced when this flag is set have a + stricter resolution behavior (the flag is off by default). When looking for unifications of a goal with an instance of this class, we “freeze” all the existentials appearing in the goals, meaning that they are considered rigid during unification and cannot be @@ -528,15 +528,28 @@ Options .. flag:: Typeclasses Unique Instances - Typeclass declarations introduced when this option is set have a more - efficient resolution behavior (the option is off by default). When a + Typeclass declarations introduced when this flag is set have a more + efficient resolution behavior (the flag is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. +.. flag:: Typeclasses Iterative Deepening + + When this flag is set, the proof search strategy is breadth-first search. + Otherwise, the search strategy is depth-first search. The default is off. + :cmd:`Typeclasses eauto` is another way to set this flag. + +.. opt:: Typeclasses Depth @num + :name: Typeclasses Depth + + Sets the maximum proof search depth. The default is unbounded. + :cmd:`Typeclasses eauto` is another way to set this option. + .. flag:: Typeclasses Debug Controls whether typeclass resolution steps are shown during search. Setting this flag - also sets :opt:`Typeclasses Debug Verbosity` to 1. + also sets :opt:`Typeclasses Debug Verbosity` to 1. :cmd:`Typeclasses eauto` + is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @num :name: Typeclasses Debug Verbosity @@ -547,7 +560,7 @@ Options .. flag:: Refine Instance Mode - This option allows to switch the behavior of instance declarations made through + This flag allows to switch the behavior of instance declarations made through the Instance command. + When it is on (the default), instances that have unsolved holes in @@ -560,14 +573,17 @@ Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth + :name: Typeclasses eauto This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. + printed. This value also be set with :flag:`Typeclasses Debug`. + ``dfs, bfs`` This sets the search strategy to depth-first search (the - default) or breadth-first search. + default) or breadth-first search. This value can also be set with + :flag:`Typeclasses Iterative Deepening`. - + ``depth`` This sets the depth limit of the search. + + ``depth`` This sets the depth limit of the search. This value can also be set with + :opt:`Typeclasses Depth`. -- cgit v1.2.3 From 9903f6a7f86661549def884a0050d0f4537d52d7 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Wed, 28 Nov 2018 10:35:27 -0800 Subject: Add undocumented options from mattam82 --- doc/sphinx/addendum/extraction.rst | 4 ++-- doc/sphinx/addendum/program.rst | 8 ++++++++ doc/sphinx/addendum/type-classes.rst | 5 +++-- 3 files changed, 13 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/addendum') diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 8891234330..e93b01f14d 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -422,7 +422,7 @@ Additional settings :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained - control than :flag:`Extraction Optimize`. The bits of *num* are used as a bit mask. + control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: @@ -454,7 +454,7 @@ Additional settings .. flag:: Extraction TypeExpand - If set, fully expand Coq types in ML. **see type_expand in mlutil.ml** + If set, fully expand Coq types in ML. See the Coq source code to learn more. Differences between |Coq| and ML type systems ---------------------------------------------- diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 429dcbee69..56f84d0ff0 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -95,6 +95,14 @@ coercions. (the option is on by default). Coercion of subset types and pairs is still active in this case. +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + .. _syntactic_control: Syntactic control over equalities diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7933cdaee0..43d302114e 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -556,7 +556,8 @@ Settings Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option also sets :flag:`Typeclasses Debug`. + of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this + option to 0 turns that option off. .. flag:: Refine Instance Mode @@ -579,7 +580,7 @@ Typeclasses eauto `:=` resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. This value also be set with :flag:`Typeclasses Debug`. + printed. This value can also be set with :flag:`Typeclasses Debug`. + ``dfs, bfs`` This sets the search strategy to depth-first search (the default) or breadth-first search. This value can also be set with -- cgit v1.2.3