coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 (n m : nat) (A : Type) (f : A -> A) (x : A),
nat_rect (fun _ : nat => A) x (fun _ : nat => f) (n + m) = nat_rect (fun _ : nat => A) (nat_rect (fun _ : nat => A) x (fun _ : nat => f) m) (fun _ : nat => f) 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 (A : Type) (f : A -> A) (x : A) (n : nat), nat_rect (fun _ : nat => A) x (fun _ : nat => f) (S n) = nat_rect (fun _ : nat => A) (f x) (fun _ : nat => f) 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 According
to the brief documentation, it seems have to
send a list of search constraint and boolean
value pairs inside So is
there any examples to use Thank you, |
- [Coq-Club] questions about using search command in coqtop ideslave, zjhsdtc, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, zjhsdtc, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, James Smith, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, James Smith, 10/06/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, James Smith, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, zjhsdtc, 10/05/2016
- Re: [Coq-Club] questions about using search command in coqtop ideslave, CJ Bell, 10/05/2016
Archive powered by MHonArc 2.6.18.