src/HOL/Tools/Sledgehammer/MaSh/src/readData.py

have MaSh support nameless facts (i.e. proofs) and use that support

#     Title:      HOL/Tools/Sledgehammer/MaSh/src/readData.py
#     Author:     Daniel Kuehlwein, ICIS, Radboud University Nijmegen
#     Copyright   2012
#
# All functions to read the Isabelle output.

'''
All functions to read the Isabelle output.

Created on July 9, 2012

@author: Daniel Kuehlwein
'''

import sys,logging

def create_dependencies_dict(nameIdDict,inputFile):
    logger = logging.getLogger('create_dependencies_dict')
    dependenciesDict = {}
    IS = open(inputFile,'r')
    for line in IS:
        line = line.split(':')
        name = line[0]
        # Name Id
        if not nameIdDict.has_key(name):
            logger.warning('%s is missing in nameIdDict. Aborting.',name)
            sys.exit(-1)

        nameId = nameIdDict[name]
        dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()]
        # Store results, add p proves p
        if nameId == 0:
            dependenciesDict[nameId] = dependenciesIds
        else:
            dependenciesDict[nameId] = [nameId] + dependenciesIds
    IS.close()
    return dependenciesDict

def create_accessible_dict(nameIdDict,idNameDict,maxNameId,inputFile):
    logger = logging.getLogger('create_accessible_dict')
    accessibleDict = {}
    IS = open(inputFile,'r')
    for line in IS:
        line = line.split(':')
        name = line[0]
        # Name Id
        if not nameIdDict.has_key(name):
            logger.warning('%s is missing in nameIdDict. Adding it as theory.',name)
            nameIdDict[name] = maxNameId
            idNameDict[maxNameId] = name
            nameId = maxNameId
            maxNameId += 1
        else:
            nameId = nameIdDict[name]
        accessibleStrings = line[1].split()
        accessibleDict[nameId] = [nameIdDict[a.strip()] for a in accessibleStrings]
    IS.close()
    return accessibleDict,maxNameId