Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Optimizations to Coq data structures

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Optimizations to Coq data structures


Chronological Thread 
  • 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.



Archive powered by MHonArc 2.6.18.

Top of Page