pytact.common

  1"""
  2common  wrapping functions for python - capnp - tactician interface
  3
  4provides class Proving with method run_prover that evaluates your python
  5proving session in coq environment over capnp communication
  6
  7you need yourself to establish socket/pipe connection with capnp end of coq
  8and instantiate Proving object with
  9"""
 10
 11import pkg_resources
 12import os
 13import logging
 14import asyncio
 15import functools
 16from typing import List
 17import capnp
 18
 19test_filename_stdin = pkg_resources.resource_filename('pytact','tests/TestReinforceStdin.v')
 20test_filename_tcp  =  pkg_resources.resource_filename('pytact','tests/TestReinforceTcp.v')
 21
 22def testfile(fname: str):
 23    return pkg_resources.resource_filename('pytact', os.path.join('tests', fname))
 24
 25
 26logger = logging.getLogger(__name__)
 27
 28
 29
 30
 31
 32class Connection:
 33    """
 34    wrapper class for serving capnp  connection
 35    this wrapper is not specialized to a particular capnp schema
 36    """
 37    async def _reading_socket(self):
 38        """
 39        This loop reads from connected pipe and writes to local capnp client
 40        """
 41        client = self.client
 42        reader = self.reader
 43        while not reader.at_eof():
 44            data = await reader.read(4096)
 45            logger.debug("read from socket %d bytes", len(data))
 46            client.write(data)
 47            logger.debug("wrote to client %d bytes", len(data))
 48
 49        logger.debug("_reading_socket ended")
 50        return '_reading_socket ended'
 51
 52
 53    async def _writing_socket(self):
 54        """
 55        This reads from local capnp client and writes to connected pipe
 56        """
 57        client = self.client
 58        writer = self.writer
 59        while True:
 60            data = await client.read(4096)
 61            logger.debug("read from client %d bytes", len(data))
 62
 63            writer.write(data.tobytes())
 64            await writer.drain()
 65            logger.debug("wrote to socket %d bytes", len(data))
 66
 67        logger.debug("_writing to socket ended")
 68        return '_writing_socket ended'
 69
 70    def __init__(self, reader, writer):
 71        self.reader = reader
 72        self.writer = writer
 73
 74        logger.debug("starting capnp client")
 75
 76        import pytact.graph_api_capnp as api
 77        self.api = api
 78
 79        self.client = capnp.TwoPartyClient()
 80
 81
 82
 83    async def run(self, proc):
 84        """
 85        this method runs the function proc
 86        that defines the process of interacting with capnp connection
 87        on python side
 88
 89        the function proc should be of async awaitable type that takes
 90        two arguments, proc(client, api), the types of client and api
 91        are like in these cals
 92
 93        client = capnp.TwoPartyClient()
 94        api = capnp.load(api.capnp)
 95
 96        and returns None when completed
 97
 98        example:
 99
100        async def proc(client)
101            # do your interaction with with capnp client using the api
102            return
103
104        """
105
106        read_task = asyncio.create_task(self._reading_socket())
107        write_task = asyncio.create_task(self._writing_socket())
108        proc_task = asyncio.create_task(proc(self.client, self.api))
109
110        _done, _pending = await asyncio.wait([read_task, write_task, proc_task],
111                                           return_when=asyncio.FIRST_COMPLETED)
112
113        if proc_task.done():
114            logger.debug("process with capnp ended %s", repr(proc_task))
115            if proc_task.exception():
116                raise Exception("EXCEPTION in connection task; this is not expected, debug: %s",
117                                repr(proc_task))
118
119        else:
120            if read_task.done():
121                raise Exception("reading_socket ended before reinforce ended: "
122                             "possibly terminated from other side")
123            if write_task.done():
124                raise Exception("_writing_socket ended ended before reinforce ended: "
125                             "possibly connection broken")
126
127        read_task.cancel()
128        write_task.cancel()
129        proc_task.cancel()
130        self.writer.close()
131
132        logger.info("serving connection finished")
133
134class Proving(Connection):
135    """
136    this is a higher level wrapper over Connection class that
137    provides higher level run_prover method that takes as an input
138    and runs your function prover and provides
139    to prover the pull object of graph_api.capnp schema
140
141    Example:
142
143    proving = Proving(reader, writer)
144    await proving.run_prover(your_super_prover)
145
146    where reader and writer are the read and write end of socket/pipe to
147    the other end of capnp coq
148
149    and where you need to implement your_super_prover function as you like
150
151    See doc string of run_prover method
152    """
153    @staticmethod
154    async def __proc(prover, client, api):
155        logger.info("calling PullReinforce")
156        pull = client.bootstrap().cast_as(api.PullReinforce)
157        await prover(pull)
158
159    async def run_prover(self, prover):
160        """
161        The method run_prover runs your function prover in coq
162        evaluation session  using capnp protocol graph_api.capnp schema
163
164        Your function prover should take one argument
165
166        pull
167
168        that is an object defined by graph_api.capnp schema
169
170        You can start the  proving session in your functin prover
171        by opening coq proving environment with a call to pull as follows:
172
173        response = await pull.reinforce(lemma).a_wait
174
175        You get available tactics with
176
177        available = await response.available.tactics().a_wait
178
179        You get the context and goal packed in response.result
180        as specified in graph_api.capnp schema
181
182        NOTICE: the implementation of this class depends on the particular naming
183        and data structures we have chosen in graph_api.capnp schema
184
185        This is subject to change
186        """
187        await self.run(functools.partial(self.__proc, prover))
188
189
190def globalNode(nodeIndex):
191    """
192    returns capnp global node argument given local node index
193    """
194    return {'depIndex': 0, 'nodeIndex': nodeIndex}
195
196def capnpLocalTactic(ident: int, local_arguments: List[int]):
197    """
198    returns capnpTactic argument given  ident and a list of local nodes
199    """
200    res = {'ident': ident}, [{'term': globalNode(nodeIndex)} for nodeIndex in local_arguments]
201#           'arguments': [{'term': globalNode(nodeIndex)} for nodeIndex in local_arguments]}
202    return res
203
204def graph_api_capnp():
205    return pkg_resources.resource_filename('pytact','graph_api.capnp')
206
207async def runTactic(obj, tactic, vis=None):
208    """
209    wrapper on capnp runTactic with logging
210    vis: pytact.graph_visualize.Visualizer
211    """
212    logger.info("awaiting tactic %s", repr(tactic))
213    if isinstance(tactic, str):
214        resp = await obj.runTextTactic(tactic).a_wait()
215    else:
216        resp = await obj.runTactic(*tactic).a_wait()
217    result = resp.result
218    logger.info('received result of type %s', result.which())
219    if result.which() == 'newState':
220        logger.info('new proof state: %s', result.newState.state.text)
221        root = result.newState.state.root
222        context = list(result.newState.state.context)
223        logger.debug('with root: %d', root)
224        logger.debug('with context: %s', repr(context))
225    if vis is not None:
226        vis.render(result)
227
228    if result.which() == 'protocolError':
229        logger.error('received protocolError %s', result.protocolError.which())
230    #    raise ProtocolError  # our code is wrong
231
232    return result