coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Calling out to unification from a plugin

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Calling out to unification from a plugin
Date: Tue, 23 May 2017 20:16:15 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:qlzUOh/OpuJuIv9uRHKM819IXTAuvvDOBiVQ1KB42ukcTK2v8tzYMVDF4r011RmSDNudtq0My7KP9fuxBipYudfJmUtBWaIPfidGs/lepxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsowjcssgbjZFiJ6sz1xDFpmdEd/lMyW5mIV+enQzw6tus8JJm7i9dp+8v+8lcXKr1eKg1UaZWADM6PW4r+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAOUPPelar4fzqVgAowagCwawH+7g0CNEi2Xs0KEmz+gsEwfL1xEgEdIUt3TUqc34OqMIXuCuy6nIyyjIYfJM2Tf684jIaQ0qrPaOXb1qasrRzk8vFwzfjlWXsozlJDeY2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTHiIISz1DL7yR5wIAtKN23SU57fd6kEIZLuC2AK4R2RcYiTmd1syg50r0LoYC3cDQOxZg9xBPSa+aLf5aV7h/iTuqdPDR1iGxjdbminRi961Kgxff5VsSs0FZFsC5Fkt7Uu3AIzRPT68yHRuJk/ke9xTqDzg7T5vxHLEwqj6bbJJkhwrk/lpoXr0vPBDP5mELzjKOOd0Uk/Pan6/j/b7n4upORM5V4hwL+P6g0hMCzHOU1PhITU2WY5+iwzLjj8lf4QLVOgP02iK7ZsJXCKMQZvKG5GAhV0oAs6xalCDemy88YkH0cIVJKfRKIlYnpO1XULP/kCve/hkygkC13yPDeIr3hHpLNI2Dfn7fmZLZx8lJTyA4uzd9E/J9UEbEAIPfrWkDrrtDYDxk5Mxa1w+n9Etl92JkeCiqzBfqSN7qXuluV7MouJfONbckbomXTMf8gstznlng/0XAHerKylc8VYWu/GPt8JF6CMFLjh94AFSEBuQ9oH7+is0GLTTMGPyX6ZKk7/DxuUI8=

I'd guess you're looking for something like w_unify: https://github.com/coq/coq/blob/trunk/pretyping/unification.mli#L49

On Tue, May 23, 2017 at 1:30 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

I'm writing a Coq plugin that finds patches for small changes in theorems and proofs.

Right now, there is a point in my tool where it would be very useful to query out to unification rather than reinvent the wheel. The unification problems I'm dealing with should be easy enough for Coq to solve most of the time.

Does anyone know how I can call out to unification from a plugin in OCaml? Has anyone done this? I am on Coq 8.5 right now, which may make a difference since I know the unification algorithm and tooling has changed very recently.

Best,

Talia
University of Washington

[Coq-Club] Calling out to unification from a plugin, Talia Ringer, 05/23/2017
- Re: [Coq-Club] Calling out to unification from a plugin, Jason Gross, 05/23/2017
  - Re: [Coq-Club] Calling out to unification from a plugin, Abhishek Anand, 05/23/2017
- Re: [Coq-Club] Calling out to unification from a plugin, Emilio Jesús Gallego Arias, 05/24/2017