{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/156","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/156/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/156/comments","events_url":"https://api.github.com/repos/coq/coq/issues/156/events","html_url":"https://github.com/coq/coq/pull/156","id":147799905,"number":156,"title":"Numeral notation","user":{"login":"roglo","id":17253650,"avatar_url":"https://avatars.githubusercontent.com/u/17253650?v=3","gravatar_id":"","url":"https://api.github.com/users/roglo","html_url":"https://github.com/roglo","followers_url":"https://api.github.com/users/roglo/followers","following_url":"https://api.github.com/users/roglo/following{/other_user}","gists_url":"https://api.github.com/users/roglo/gists{/gist_id}","starred_url":"https://api.github.com/users/roglo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/roglo/subscriptions","organizations_url":"https://api.github.com/users/roglo/orgs","repos_url":"https://api.github.com/users/roglo/repos","events_url":"https://api.github.com/users/roglo/events{/privacy}","received_events_url":"https://api.github.com/users/roglo/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2016-04-12T16:07:19Z","updated_at":"2016-04-14T09:36:23Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/coq/coq/pulls/156","html_url":"https://github.com/coq/coq/pull/156","diff_url":"https://github.com/coq/coq/pull/156.diff","patch_url":"https://github.com/coq/coq/pull/156.patch"},"body":"Added a new vernac command \"Numeral Notation\". It allows to add parsing and printing strings of decimal digits (such as \"0\", \"-47\", \"223\") from and to any datatype. It has been implemented in the Coq library for Nat, Positive, N, Z, R, int31, bigN, bigZ, bigQ. The OCaml versions in plugins/syntax have been removed. See the examples of usage by typing\r\n   grep \"Numeral Notation\" theories/\\*/\\*.v theories/\\*/\\*/\\*/\\*.v\r\nand look at the contents of these files.\r\n\r\nA type named Z' have been added in Datatypes.v to deal with strings of digits. It is defined exactly like Z and positive, but with quotes. It could be Z if you decide to define Z here.\r\n\r\nSyntax:\r\n      Numeral Notation t f g : t_scope {(printing ...)} {(warning after w)}\r\n\r\n* t is the datatype\r\n* f is the parsing function with must be of type Z' -> option t, None means not recognized, like in the example \"Check (-1)%nat.\".\r\n* g is for printing and is either a function of type t -> option Z' or a Ltac, depending on the datatype t and the printing option (see below)\r\n* t_scope is the name of the scope of t\r\n* the optional (printing ...) tells to consider the list ... of constructors or axioms to print. See examples in Rdefinitions.v. In that case, g must be a Ltac. If absent, t is supposed to be an inductive type and the printed list are its constructors. In that case, g must be a function.\r\n* the optional (warning after w) where w is an integer tells to print a warning when using a too big number. See example in Nat.v. If you type e.g. Check 5001, you get the message.\r\n\r\nImplementation: the main stuff is in tacinterp.ml. I previously put it in vernacentries.ml but in the present trunk, this would create a circular dependency, the Numeral Notation possibly using the execution of tactics. This code of about 300 lines could be in a separate file, named for example \"numeral.ml\", thing like that.\r\n\r\nSmall thing: in this file (tacinterp.ml), I added a function named \"eval_tacexpr\" taking a tacexpr and returning a value option, to allow to call a Ltac and taking its result, like a function. Perhaps it could be useful for other Coq developers."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/209851024","html_url":"https://github.com/coq/coq/pull/156#issuecomment-209851024","issue_url":"https://api.github.com/repos/coq/coq/issues/156","id":209851024,"user":{"login":"silene","id":1674458,"avatar_url":"https://avatars.githubusercontent.com/u/1674458?v=3","gravatar_id":"","url":"https://api.github.com/users/silene","html_url":"https://github.com/silene","followers_url":"https://api.github.com/users/silene/followers","following_url":"https://api.github.com/users/silene/following{/other_user}","gists_url":"https://api.github.com/users/silene/gists{/gist_id}","starred_url":"https://api.github.com/users/silene/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/silene/subscriptions","organizations_url":"https://api.github.com/users/silene/orgs","repos_url":"https://api.github.com/users/silene/repos","events_url":"https://api.github.com/users/silene/events{/privacy}","received_events_url":"https://api.github.com/users/silene/received_events","type":"User","site_admin":false},"created_at":"2016-04-14T09:36:23Z","updated_at":"2016-04-14T09:36:23Z","body":"We do not have to do anything with the existing uses. If the embedding function is chosen in such a way that it matches the current representation (e.g. R_of_pos'), most manual proofs can be kept unchanged. It will require some changes to automatic tactics, since they will now encounter a new real \"constructor\", but the needed changes will be mostly innocuous. At worst, just forcing an expansion of the numerals as a preprocessing step should do the trick. Anyway, it will be worth fixing the automatic tactics (e.g. ring, lra, and so on), so that they benefit from the sleeker representation.\r\n\r\nNote that IZR is certainly not a good choice for an embedding function, since it causes an exponential blowup of terms. As for R_of_pos' (or equivalent), I don't think we need to go as far as making it opaque (it would break manual proofs), we just need to mark it \"nosimpl\", I think."}}