coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Plugin tutorial for traversing the Gallina AST

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Plugin tutorial for traversing the Gallina AST
Date: Mon, 27 Feb 2017 00:33:05 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wr0-f179.google.com
Ironport-phdr: 9a23:/v2RWRBerm+MQkPpMQqKUyQJP3N1i/DPJgcQr6AfoPdwSPv9r8bcNUDSrc9gkEXOFd2CrakV1qyM7+u5Bz1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbN/IA+ooQjeucUanIpvJ6IswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28dYsPCO8BMP5GoYbno1sOrAGxDhSwCuPuzD9IiWH53bcn2OkmDQHGxg0gH9QBsHvKttX4L7sdUfuvwKjG1zrDdPNW2Tb76IjHbhAhpveMUahufsXM1EkiDgXIhUiep4ziOjOazOUNs26D4upvVOKvl24nqxxqrTS12sgsjYzJi4QIwV7H7SV02Jg5KcG8RUJhYtOpEIFcuzyEO4Z1WM8uXmNltSI8x7Ybo5C0ZjIKx44ixxPHa/yIbYyI4hX7WeaUOzh4hXZldKuxhhao7USs0+P8WtS23VtOtCZFnd7MtncC1xzX9MeLUOdy/kCk2TqX1gDT7P9LIVwsmKbFN5IsxqQ8m5kTvEjZAyP6hkb7gLWLekgm/uWk8+Hnba/npp+YOY90kAb+MqE2l8yjG+Q4Mw4OX2eF9uSmz7Ds4Vb5TK9Ej/IsianZsJHaJcIUpq6lBA9V1Jwv5AiiADe7yNgYh2UILEpZeBKbiIjkI03BIPfhDfumn1uslCpryOvdM736ApTNK2DDn637cbZ87U5c0gszwspF65JaELFSaM70D0T2rZnTCgIzGw2y2efuTttnha0EXmfaPqadMaqai16O6e81a72Qfo4TtzvnA/M+oeHnln84n1ABeq/v0JcKPiPrVs96KlmUNCK/yuwKFn0H61Iz

Hi all,

For my research I need to have a good understanding of how to traverse the Gallina AST, so I wrote a plugin that is basically a tutorial for traversing the AST. My goal with this plugin is to make it easy for anyone who wants to write a plugin that compiles Gallina code.

The plugin is here: https://github.com/uwplse/CoqAST

The actual functionality is not very interesting (it prints s-expressions, which SerAPI does well already). The code is based off of template-coq. I spent a lot of time writing comments in the code to try to explain what it is actually doing in hopes that this will help other researchers and compiler hackers.

I very strongly encourage anyone who is interested to fork it, play around with it, and submit pull requests for anything that is incomplete, incorrect, or confusing. I'm hoping that after some community development, plugin compiler developers will be able to just play with this plugin and not ever have to look into the internals of the kernel.

[Coq-Club] Plugin tutorial for traversing the Gallina AST, Talia Ringer, 02/27/2017