fixes for parser

coqd/connserv.py

@@ -1,7 +1,16 @@
 """
 Connserv
 ~~~~~~~~
-Handle protocol for connections
+Server for Coq protocol. Clients can connect and request server sessions based
+on a userid and a Coq command serialized into JSON::
+
+  {"command":"", "userid":""}
+
+ They then send commands and receive back JSON of
+the schema::
+
+  {'userid': self.userid, 'response': res}
+
 """
 from json import JSONDecoder, JSONEncoder
 
@@ -23,7 +32,7 @@ class CoqProtocol(Protocol):
     """
     class ActiveConn(object):
         """
-        Does some work for dealing with the backend interpreter
+        Talks to the specific backend instance associated with a userid
         """
         def __init__(self, userid):
             self.userid = userid
@@ -34,6 +43,7 @@ def __init__(self, userid):
             logging.debug("Coqtop Process started %s", self.proc)
 
         def read(self):
+            """poll results from the coqtop backend"""
             res = None
             self.proc.run(self.there)
             if self.here.poll():
@@ -42,6 +52,7 @@ def read(self):
             return {'userid': self.userid, 'response': res}
 
         def send(self, data):
+            """send results to our coqtop instance"""
             if self.proc.alive:
                 logging.debug("sending stuff")
                 self.here.send(data + " ")
@@ -70,11 +81,15 @@ def dataReceived(self, data):
         self.transport.loseConnection()
 
     def do_parse(self, output):
+        """Parse coqtop results and serialize"""
+        logging.debug("Unformatted Output: %s" % output)
         output = ' '.join(output.splitlines())
         result = parser.parse(output)
         return result
 
     def handle_command(self, userid, command):
+        """When a command is received send it to the specific backend for the
+        given userid"""
         if not command:
             resp_dict = {'userid': userid,
                          'response': ''}
@@ -98,13 +113,15 @@ def handle_command(self, userid, command):
         return resp_dict
 
     def connectionLost(self, reason):
+        """When the connection closes log the exit status"""
         if 'ConnectionDone' in ''.join(reason.parents):
             logging.debug("Connection closed cleanly")
         else:
             logging.debug("Connection didn't close correctly")
             raise reason
 
     def cleanup_session(self, userid):
+        """Close out sessions and remove the userid from the tracking table"""
         active_sess = self.active_conns.get(userid)
         if active_sess:
             active_sess.quit()

coqd/interp.py

@@ -1,10 +1,11 @@
 from code import InteractiveConsole
 from json import JSONDecoder, JSONEncoder
+import readline
 import logging
 import telnetlib
 
 
-def fee(command):
+def send(command):
     try:
         tn = telnetlib.Telnet('localhost', 8003)
         tn.write(JSONEncoder().encode(dict(userid=0,
@@ -15,7 +16,9 @@ def fee(command):
     except Exception:
         logging.error("Connection to coqd failed")
 
-
-foo = InteractiveConsole()
-f = foo.raw_input(">>>")
-fee(f)
+while True:
+    try:
+        prompt = raw_input(">>> ")
+        send(prompt)
+    except:
+        pass

coqd/parser/gram.py

@@ -54,9 +54,11 @@
 
 
 def p_proofst(p):
+
     """proofst : subgoal hyp goal term_prompt
                | subgoal goal term_prompt
-               | sysmsg term_prompt"""
+               | sysmsg term_prompt
+    """
     if len(p) == 5:
         p[0] = dict(subgoal=p[1],
                     hyp=p[2],
@@ -77,7 +79,8 @@ def p_proofst(p):
 
 
 def p_subgoal(p):
-    """subgoal : NUMBER SUBGOAL"""
+    """subgoal : NUMBER SUBGOAL
+               | SUBGOAL"""
     p[0] = ' '.join((str(p[1]), str(p[2])))
 
 
@@ -153,6 +156,8 @@ def p_idlist(p):
     """idlist : ID idlist
               | TILDE idlist
               | PLING idlist
+              | TRUE
+              | FALSE
               | ID
               """
     if len(p) == 3:
@@ -168,8 +173,10 @@ def p_term_prompt(p):
 
 
 def p_sysmsg(p):
-    """sysmsg : PROOF idlist DOT"""
-    p[0] = dict(msg=p[2])
+    """sysmsg : PROOF idlist DOT
+              | PROOF COMPLETED DOT
+              | thmname IS DEFINED"""
+    p[0] = dict(msg=' '.join(p[1:]))
 
 
 def p_proverstate(p):
@@ -181,9 +188,11 @@ def p_proverstate(p):
 
 def p_thmlist(p):
     """thmlist : thmname PIPE thmlist
-               | thmname PIPE"""
+               | thmname PIPE
+               | PIPE
+               """
     if len(p) == 4:
-        p[0] = dict(names=' ,'.join((p[1], p[3])))
+        p[0] = dict(names=' ,'.join((p[1], p[3]['names'])))
     else:
         p[0] = dict(names=p[1])
 

coqd/parser/lexer.py

@@ -4,9 +4,10 @@
 Token definitons for the Coqtop Output Language.
 
 .. warning:: It is not meant to be used on its own and will not provide a useful
-             language
+             language.
 
-To use import the tokens object::
+However you can use it with a parser by importing the tokens; to import the
+tokens object::
 
   from coqd.parser.lexer import tokens
 
@@ -22,10 +23,13 @@
             'Prop': 'PROP',
             'completed': 'COMPLETED',
             'defined': 'DEFINED',
+            'True': 'TRUE',
+            'False': 'FALSE',
             'forall': 'FORALL',
             'exists': 'EXISTS',
             'subgoal': 'SUBGOAL',
             'prompt': 'PROMPT',
+            'is': 'IS',
             'Exited': 'EXITED',
             'Qed': 'QED',
             }
@@ -61,7 +65,7 @@
 
 
 def t_ID(t):
-    """Ensure that reserved words are not overwritten with ID's"""
+    # Ensure that reserved words are not overwritten with ID's
     r'[a-zA-Z_][a-zA-Z_0-9\']*'
     t.type = reserved.get(t.value, 'ID')    # Check for reserved words
     return t
@@ -124,15 +128,23 @@ def t_newline(t):
 if __name__ == '__main__':
 
     # A little unit test for the lexer
-    s = """
+    s = ("""
 1 subgoal
 
   ============================
    forall A B  : Prop, A -> (~ ~ A) \/ B
 <prompt>Unnamed_thm < 2 |Unnamed_thm| 0 < </prompt>
+""",
 """
+1 subgoal
+  
+  ============================
+   True -> True
 
-    lex.input(s)
+<prompt>Unnamed_thm < 2 |Unnamed_thm| 0 < </prompt> 
+""",
+)
+    lex.input(s[1])
 
     while True:
         tok = lex.token()

coqd/runner.py

@@ -28,7 +28,9 @@ def options(parser):
                         help="load modules into coqd, more than one "
                         "can be specified",
                         )
-
+    parser.add_option("--serialize", action="store_true",
+                      default=False,
+                      help="Serialize output to JSON")
     return parser
 
 

coqd/test.py

@@ -42,6 +42,19 @@ def do_parse(s):
 #    A -> ~ ~ A \/ B > C
 # <prompt>Unnamed_thm < 2 |Unnamed_thm| 0 < </prompt>
 # """,
+"""
+1 subgoal
+  
+  ============================
+   True -> True
+
+<prompt>Unnamed_thm < 2 |Unnamed_thm| 0 < </prompt> 
+""",
+"""
+Unnamed_thm is defined
+
+<prompt>Coq < 5 || 0 < </prompt>
+""",
 )
 
     for x in s: