coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gregory Malecha <gmalecha AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] overloading natural number notations for user types
- Date: Mon, 22 Feb 2016 09:19:03 -0800
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f181.google.com
- Ironport-phdr: 9a23:a1klWBXDQS9lGlqXlsoh1zQroDHV8LGtZVwlr6E/grcLSJyIuqrYZhOFt8tkgFKBZ4jH8fUM07OQ6PC/HzFcqs/Z6DgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVgUz2PlOftbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN4xxd7FTDSwnPmYp/4Wr8ECbFUrcrkcbB04Ri1JjBxXPpEXxWY60uS/nvMJ83jObNIv4V+Zndy6l6vJEUhLnjz0Wfxsw9GzcisU42K1eqRasrBx264HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5KVrJZMA==
Would Coercions fit the bill for the nat2mynat idea? Or are they not expressive enough.
On Sun, Feb 21, 2016 at 8:40 PM, Jason Gross <jasongross9 AT gmail.com> wrote:
Jonathan, how does that work on open terms? It'll work fine for parsing, probably (though I don't really want to be able to do arbitrary computation in the parsing of my numerals, that's perhaps a bit scary, but perhaps useful), but seems kind-of sketchy for printing.On Sun, Feb 21, 2016 at 9:08 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:I was thinking something even stupider than that! The user gives two functions that map between nats and the user type they want to represent with number notations:
Inductive mynat : Set := ...
Definition nat2mynat(n : nat) : mynat := ...
Definition mynat2nat(m: mynat) : nat := ...
Declare Nat Syntax mynat Using nat2mynat, mynat2nat : M_scope.
The parser would, whenever it sees a number in the scope M_scope, call nat2mynat and use the result. The printer would, whenever it sees a mynat in the scope M_scope, call mynat2nat, and print the resulting number.
-- Jonathan
On 02/21/2016 06:05 PM, Jason Gross wrote:
I was thinking something stupider: you pass in terms that are treated as
constructors and required to have the appropriate type signature (a type
"NAT", an "O : NAT", and an "S : NAT -> NAT" (hopefully the code can be
parametric over how many universes NAT uses, and whether its polymorphic or
not, etc), and then notations get translated to applications of S and O,
and applications of S and O get translated back, and if S and O happen to
unfold to other things, then unfolding them breaks the notation (which is
not the end of the world).
Even better would be to generalize the nat_syntax_plugin to handle things
like [trunc_index], i.e., things where the base case should be displayed as
1 or as -2, etc.
I do not think that we should have to trust Ltac code to get syntax for
custom natural numbers.
On Sun, Feb 21, 2016 at 5:49 PM, Pierre-Marie Pédrot <
pierre-marie.pedrot AT inria.fr> wrote:
On 21/02/2016 23:31, Jason Gross wrote:
How hard would it be to set up the syntax plugins already in Coq so thatNot that difficult, I believe. Yet, we need to rely on a meta-language
they registered vernaculars such as [Declare NatSyntax for nat in
nat_scope [O S].] and similarly for notations for negative numbers,
ascii, strings, etc?
to pattern-match over terms. Ltac would fit the bill, but I personally
find this use a little bit ugly. The vernacular would probably look like:
Parameter myNat : Type.
Ltac reify_myNat n :=
match n with
(* insert a code producing a Z from a myNat here *)
end.
Declare Nat Syntax myNat reify_myNat.
PMP
gregory malecha
- Re: [Coq-Club] overloading natural number notations for user types, (continued)
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/20/2016
- Re: [Coq-Club] overloading natural number notations for user types, Clément Pit--Claudel, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Assia Mahboubi, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Beta Ziliani, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jason Gross, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Gregory Malecha, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/22/2016
- Re: [Coq-Club] overloading natural number notations for user types, Jonathan Leivent, 02/24/2016
- [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jason Gross, 02/24/2016
- Re: [Coq-Club] why are Coercions restricted to names?, Jonathan Leivent, 02/25/2016
- Re: [Coq-Club] overloading natural number notations for user types, Pierre-Marie Pédrot, 02/21/2016
Archive powered by MHonArc 2.6.18.