| Age | Commit message (Collapse) | Author |
|---|
|
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
|
This allows to issue a more appropriate message when a notation with a
{ } cannot be defined because of an incompatible level. E.g.:
Notation "{ A } + B" := (sumbool A B) (at level 20).
|
|
- Formerly, notations such as "{ A } + { B }" were typically split
into "{ _ }" and "_ + _". We keep the split only for parsing, which
is where it is really needed, but not anymore for interpretation,
nor printing.
- As a consequence, one notation string can give rise to several
grammar entries, but still only one printing entry.
- As another consequence, "{ A } + { B }" and "A + { B }" must be
reserved to be used, which is after all the natural expectation,
even if the sublevels are constrained.
- We also now keep the information "is ident", "is binder" in the
"key" characterizing the level of a notation.
|
|
|
|
|
|
|
|
|
|
This new function is similar to declare_numeral_interpreter,
but works on a lower level : instead of bigint, numbers are
represented as string of their decimal digits (plus a boolean sign)
|
|
|
|
|
|
|
|
The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.
The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.
This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
|
|
Now it is a private field, locations are optional.
|
|
The ML side lacks a method to query Coq for notations with defined
parsing/printing rules. This commit adds a method
`get_defined_notations` to that purpose.
This is very useful for instance in plugins like SerAPI.
In the medium-term, the `Notation` interface may benefit from a bit of
refactoring to allow programmatic access and manipulation of notations.
|
|
|
|
|
|
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
|
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
|
into JasonGross-trunk-function_scope
|
|
|
|
|
|
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
|
|
|
This reverts commit 124734fd2c523909802d095abb37350519856864.
|
|
|
|
so that one can retrieve them and pass them to third party tools (i.e.
print the AST with the notations attached to the nodes concerned).
Available syntax:
- all in one:
Notation "a /\ b" := ... (format "...", format "latex" "#1 \wedge #2").
- a posteriori:
Format Notation "a /\ b" "latex" "#1 \wedge #2".
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
type in "cast" to activate the temporary interpretation scope.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
First Notations, syntactic definitions, primitive entries are tackled to build
raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns
are internalized as cases_pattern or applied inductive (dealing with implicit
args, or_pattern refactoring, aliases).
It is more uniform, it allows notations for non fully applied constructors but :
- It does not raise a warning when an identifier is also a global_reference
different than a constructor.
- It looks for implicit arguments twice. (because finding scopes of arguments
asks for implicit arguments).
- It does not deal anymore with constants that evaluates to constructor. (This one
is voluntary, dealing with implicit & notations is already a hell full of bugs
so what will be next step ? Any terms that computes to a pattern ???)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixes the test-suite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
longer be bound to Funclass or Sortclass (this does not seem to be
useful). [An exception is when using modules, if a constant foo is
expanded into a type, a "Bind Scope sc with foo" starts binding
Sortclass].
Also reworked reference manual for Arguments Scopes and Bind Scopes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactic arguments of ltac functions).
Added support for recursive entries in ARGUMENT EXTEND, for right-hand
sides of ARGUMENT EXTEND raising exceptions and for right-hand sides
referring to "loc". Also fixed parsing level of initial value in
create_arg (raw instead of glob). Thanks to the Ssreflect plugin for
revealing these problems.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
The new vernacular "Arguments" attaches to constants the extra-logical
piece of information regarding implicit arguments, notation scopes and
the behaviour of the simpl tactic. The About vernacular is extended to
print the new extra logical data for simpl.
Examples:
Arguments foo {A B}%type f [T] x.
(* declares A B and T as implicit arguments, A B maximally inserted.
declares type_scope on A and B *)
Arguments foo {A%type b%nat} p%myscope q.
(* declares A and b as maximally inserted implicit arguments.
declares type_scope on A, nat_scope on b and the scope delimited by
myscope on p *)
Arguments foo (A B)%type c d.
(* declares A and b in type_scope, but not as implicit arguments. *)
Arguments foo A B c.
(* leaves implicit arguments and scopes declared for foo untouched *)
Arguments foo A B c : clear implicits
(* equivalente too Implicit Arguments foo [] *)
Arguments foo A B c : clear scopes
(* equivalente too Arguments Scope foo [_ _ _] *)
Arguments foo A B c : clear scopes, clear implicits
Arguments foo A B c : clear implicits, clear scopes
Arguments foo A B c : clear scopes and implicits
Arguments foo A B c : clear implicits and scopes
(* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *)
Arguments foo A B c : default implicits.
(* equivalent to Implicit Arguments foo. *)
Arguments foo {A B} x , A [B] x.
(* equivalent to Implicit Arguments foo [[A] [B]] [B]. *)
Arguments foo a !b c !d.
(* foo is unfolded by simpl if b and d evaluate to a constructor *)
Arguments foo a b c / d.
(* foo is unfolded by simpl if applied to 3 arguments *)
Arguments foo a !b c / d.
(* foo is unfolded by simpl if applied to 3 arguments and if b
evaluates to a constructor *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
