aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
|
* More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\
| * Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
| | | | | | | | A single terminal character can take up to 5 bytes, e.g. "''^A'".
| * Fix bug #3825: Universe annotations on notations should pass through or be ↵Gravatar Pierre-Marie Pédrot2016-05-03
| | | | | | | | rejected.
* | Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
* | Revert "Not taking arguments given by name or position into account when"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit f7ea0193c1aac918d8ed2df0d53df38dde5d1152.
* | Revert "Being defensive in printing implicit arguments also with manual"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 2211eeda012477b26081738fccc59aa31fb0a565.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
* | Revert "Warn about possible shadowing of a name occurring in a "in" clause."Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit 46f876a9404844487476415af2e6f6d938558d15.
* | Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ↵Gravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64.
* | Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
* | Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
| |
* | Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
| | | | | | | | VERNAC EXTEND.
* | Being defensive in printing implicit arguments also with manualGravatar Hugo Herbelin2016-04-27
| | | | | | | | implicit arguments when in beautification mode.
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available.
* | A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
| | | | | | | | clause of a "match" over an irrefutable pattern.
* | Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | in interning of patterns. No semantic changes (except the type of ids_of_cases_indtype).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-24
|\|
| * Fixing #4677 (collision of a global variable and of a local variableGravatar Hugo Herbelin2016-04-19
| | | | | | | | | | while eta-expanding a notation) + a more serious variant of it (alpha-conversion incorrect wrt eta-expansion).
* | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq ↵Gravatar Matthieu Sozeau2016-04-04
|\ \ | | | | | | | | | into JasonGross-trunk-function_scope
* | | Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
| | |
* | | Removing dead code in Genarg.Gravatar Pierre-Marie Pédrot2016-03-19
| | |
* | | Removing the special status of generic entries defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there.
* | | Removing the registering of default values for generic arguments.Gravatar Pierre-Marie Pédrot2016-03-17
| | |
* | | Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable).
* | | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
| | |
* | | A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \ \ | | |/ | |/|
| * | Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop.Gravatar Pierre-Marie Pédrot2016-03-03
| | | | | | | | | | | | | | | | | | | | | Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash.
* | | Printing notations: Cleaning in anticipation of fixing #4592.Gravatar Hugo Herbelin2016-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env.
* | | The tactic generic argument now returns a value rather than a glob_expr.Gravatar Pierre-Marie Pédrot2016-02-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side.
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* \ \ \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
|\ \ \ \ | | |/ / | |/| |
| * | | Do not give a name to anonymous evars anymore. See bug #4547.Gravatar Pierre-Marie Pédrot2016-02-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced.
| | * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| |
| * | Implement support for universe binder lists in Instance and Program ↵Gravatar Matthieu Sozeau2016-01-23
| | | | | | | | | | | | Fixpoint/Definition.
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| | |
* | | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| | |
* | | Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
| | | | | | | | | | | | This will allow an easier landing of the rewriting of Genarg.
* | | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
| | |
* | | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
| | |
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\| |
| * | Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| | | | | | | | | | | | | | | Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v).
| * | Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
| | | | | | | | | | | | | | | This fixes a TODO in map_constr_expr_with_binders, a bug in is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 12:48:02 +0000