coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Walking the Coq environment for an ml-plugin

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Walking the Coq environment for an ml-plugin
Date: Fri, 17 Nov 2017 14:21:23 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-DM3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:/0higxK6cqwz9CoRq9mcpTZWNBhigK39O0sv0rFitYgXLPnxwZ3uMQTl6Ol3ixeRBMOAtKIC1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBWB6kG1uBUVA1DUMRd/brD+HZeXhMCq3ciz/YfSakNGnmzuT6l1KUCVoAPXu9UWybFlJ+5lyRbPrmFPdsxWwn9tLFOX2R3745Hjr9ZY7y1Mtqd5pIZ7WqLgcvFgQA==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

One of the requirements for my "arewrite" tactic is the ability to walk through and collect all available definitions from the environment. Consider a Coq source file with the following:

Require Import AdvancedRewrite.advancedRewrite.

Fixpoint fact (x : nat) := match x with

0 => 1

S n => fact n

end.

Theorem ac_plus: AC plus.

Theorem test1: fact 4 = 24.

Proof.

arewrite.

Abort.

From the ml code inside the "arewrite" tactic, I need to traverse the environment and retrieve the "fact" and "ac_plus" declarations. It would also be useful to traverse the declarations in any modules that are imported. How can I do this?

- Ken

[Coq-Club] Walking the Coq environment for an ml-plugin, Kenneth Roe, 11/17/2017
- Re: [Coq-Club] Walking the Coq environment for an ml-plugin, Hugo Herbelin, 11/18/2017