Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] questions about using search command in coqtop ideslave

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] questions about using search command in coqtop ideslave


Chronological Thread 
  • From: James Smith <jecs AT imperial.ac.uk>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] questions about using search command in coqtop ideslave
  • Date: Wed, 5 Oct 2016 20:43:53 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jecs AT imperial.ac.uk; spf=Pass smtp.mailfrom=jecs AT imperial.ac.uk; spf=None smtp.helo=postmaster AT smtp1.cc.ic.ac.uk
  • Ironport-phdr: 9a23:2gAZlR/+VMVTqf9uRHKM819IXTAuvvDOBiVQ1KB+1OocTK2v8tzYMVDF4r011RmSDN+dsKoP0raO++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHdvZiN3y3OSv8bXSZR9JjXyze+BcNhKz+CfYs8QNybBnK7oxgk/Lr3BTU+VT3W5yJFuX2R/3oNqzqs0wux9Msu4sopYTGZ7xeL41GORV

Hi,

I saw something come up the other week on this XML protocol, I'm very interested in it. I googled it at the time but came up empty handed.

Not being conversant in ML, can I ask whether there is any chance of some conventional documentation on this protocol any time soon?

Kind regards,

James

On 05/10/16 14:49, zjhsdtc wrote:

Hi CJ Bell,

Thanks for the detailed answer! and xmlprotocol.ml is pretty neat, i will try to search around the source code before my next question about Coq :D


2016-10-05 11:53 GMT+08:00 CJ Bell <siegebell+coq AT gmail.com>:
The code for encoding and decoding this call is here:
1. the type of the Search call is a list of pairs, the first being a constraint and the second a bool: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L464
2. the constraint type: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L25
3. the return type is a list of pairs of Coq objects and strings: https://github.com/coq/coq/blob/trunk/ide/xmlprotocol.ml#L488

Example search for regex "nat_rect.+":
<call val="Search"><list><pair><search_cst val="name_pattern"><string>nat_rect.+</string></search_cst><bool val="true"/></pair></list></call
Returns:
<value val="good"><list><coq_object><list><string>Coq</string><string>Init</string><string>Peano</string></list><list><string>nat_rect_plus</string></list><string>forall&nbsp;(n&nbsp;m&nbsp;:&nbsp;nat)&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(f&nbsp;:&nbsp;A&nbsp;-&gt;&nbsp;A)&nbsp;(x&nbsp;:&nbsp;A),
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;(n&nbsp;+&nbsp;m)&nbsp;=
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)
&nbsp;&nbsp;(nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;m)&nbsp;
&nbsp;&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;n</string></coq_object><coq_object><list><string>Coq</string><string>Init</string><string>Peano</string></list><list><string>nat_rect_succ_r</string></list><string>forall&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(f&nbsp;:&nbsp;A&nbsp;-&gt;&nbsp;A)&nbsp;(x&nbsp;:&nbsp;A)&nbsp;(n&nbsp;:&nbsp;nat),
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;x&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;(S&nbsp;n)&nbsp;=
nat_rect&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;A)&nbsp;(f&nbsp;x)&nbsp;(fun&nbsp;_&nbsp;:&nbsp;nat&nbsp;=&gt;&nbsp;f)&nbsp;n</string></coq_object></list></value>


-cj

On Tue, Oct 4, 2016 at 9:49 PM, zjhsdtc <zjhsdtc AT gmail.com> wrote:

Hi all,

There is something that has confused me for quite a while. if we use coqtop -ideslave --help-XML-protocol, it will produce a list of commands available in the ideslave, e.g. the Goal command, so we can simply send <call val="Goal"><unit/></call> to ideslave, i can easily play around with these commands except the Search one.

According to the brief documentation, it seems have to send a list of search constraint and boolean value pairs inside <call val="Search">...</call>, but after trying and failing for many times, i still can not find a way to construct a qualified xml message to stand for a search command.

So is there any examples to use Search command in ideslave or anyone have an idea how to use it?

Thank you,







Archive powered by MHonArc 2.6.18.

Top of Page