coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: e AT x80.org (Emilio Jesús Gallego Arias)
- To: Kenneth Roe <kendroe AT hotmail.com>
- Cc: Coq-Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Optimizations to Coq data structures
- Date: Mon, 18 Sep 2017 16:41:05 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
- Ironport-phdr: 9a23:LV64GRR1XRB60KWlxuQZeQ3ytdpsv+yvbD5Q0YIujvd0So/mwa67bRON2/xhgRfzUJnB7Loc0qyN7PCmBDRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnY6Uy/yPgttJ+nzBpWaz4Huj7jzqNXvZFBriTy7bK9yZC+xoE2FtcQQjZFlJ44xzQfMq3pMPe9RwDU7C0iUmkPxztfgpNhk6SsY+98k9spBVu3Ycr+qVvR3BTAiPm8yrOTxtBDYDFjcrkAAW3kbx0IbSzPO6wv3C9Ko6nP3
- Organization: X80 Heavy Industries
Hi Kenneth,
a couple of comments:
Kenneth Roe
<kendroe AT hotmail.com>
writes:
> 1) Use a bignum format for natural numbers rather than the current
> "successor" format. Right now, using Talia Ringer's printAST library,
> I get the following representation for "100":
>
> printAST 100.
Umm, I think that "printAST" of 100 may not be the best name, as the AST
of 100 is:
(CPrim (Numeral 100 true))
Such primitives are then interpreted by the notation system to various
numerical formats that include binary and bignum representations,
depending on what options / packages you have enabled.
> 2) Intern symbols.
> 3) Intern subexpressions.
Coq uses hash-consing extensively, so indeed in many cases equality is
cheap; YMMV in the tactic layer thou, but I am not expert.
> 4) Maintain special handling for operators with associative and
> communitive properties. In my system operators with these properties
> have there terms sorted before interning the expression. Hence,
> "x+y+z" and "x+z+y" will be the same node in the sub term intern DAG.
Indeed better support for this in Coq would be great; the acc tactics
package provides some support for that, and IMHO it would be great if at
some point it would be distributed with Coq.
E.
- [Coq-Club] Optimizations to Coq data structures, Kenneth Roe, 09/18/2017
- Re: [Coq-Club] Optimizations to Coq data structures, Emilio Jesús Gallego Arias, 09/18/2017
Archive powered by MHonArc 2.6.18.