6.30.2010

Moar Parsing

I burned the midnight oil a bit last night working on my output serializer/parser and got it working. The grammar is nearly complete, with only 1 shift/reduce conflict. The parser will take a coqtop response, such as
1 subgoal
  A : Prop
  B : Prop
  C : Prop    
  ============================
   A -> ~ ~ A \/ B > C
"""

and turn that into a mostly correct python object, which for now is just a dict:
{   'goal': {   'expr': (   {   'expr': ('A', '~ ~ A'), 'operator': '->'},
                            {   'expr': ('B', 'C'), 'operator': '>'}),
                'operator': '\\/'},
    'hyp': [   {   'name': 'A', 'type': 'Prop'},
               [{   'name': 'B', 'type': 'Prop'}, {   'name': 'C', 'type': 'Prop'}]],
    'subgoal': '1 subgoal'}

It's pretty cool to see it work correctly on my sample strings, but the next step will be to bring it into the request/response lifecycle and see how well these objects will serialize. Still for now, progress has been made!