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

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Thu Oct 03 19:01:10 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Fri Oct 04 09:46:08 2013 +0200
@@ -4,11 +4,12 @@
 #
 # Persistent dictionaries: accessibility, dependencies, and features.
 
-import logging,sys
+import sys
 from os.path import join
 from Queue import Queue
 from readData import create_accessible_dict,create_dependencies_dict
 from cPickle import load,dump
+from exceptions import LookupError
 
 class Dictionaries(object):
     '''
@@ -56,7 +57,6 @@
         self.changed = True
 
     def create_feature_dict(self,inputFile):
-        logger = logging.getLogger('create_feature_dict')
         self.featureDict = {}
         IS = open(inputFile,'r')
         for line in IS:
@@ -64,7 +64,7 @@
             name = line[0]
             # Name Id
             if self.nameIdDict.has_key(name):
-                logger.warning('%s appears twice in the feature file. Aborting.',name)
+                raise LookupError('%s appears twice in the feature file. Aborting.'% name)
                 sys.exit(-1)
             else:
                 self.nameIdDict[name] = self.maxNameId
@@ -134,6 +134,13 @@
                         unexpandedQueue.put(a)
         return list(accessibles)
 
+    def parse_unExpAcc(self,line):
+        try:
+            unExpAcc = [self.nameIdDict[a.strip()] for a in line.split()]            
+        except:
+            raise LookupError('Cannot find the accessibles:%s. Accessibles need to be introduced before referring to them.' % line)
+        return unExpAcc
+
     def parse_fact(self,line):
         """
         Parses a single line, extracting accessibles, features, and dependencies.
@@ -147,8 +154,9 @@
         nameId = self.get_name_id(name)
         line = line[1].split(';')
         # Accessible Ids
-        unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
-        self.accessibleDict[nameId] = unExpAcc
+        #unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
+        #self.accessibleDict[nameId] = unExpAcc
+        self.accessibleDict[nameId] = self.parse_unExpAcc(line[0])
         features = self.get_features(line)
         self.featureDict[nameId] = features
         self.dependenciesDict[nameId] = [self.nameIdDict[d.strip()] for d in line[2].split()]        
@@ -180,7 +188,7 @@
         name = None
         numberOfPredictions = None
 
-        # Check whether there is a problem name:
+        # How many predictions should be returned:
         tmp = line.split('#')
         if len(tmp) == 2:
             numberOfPredictions = int(tmp[0].strip())
@@ -194,8 +202,11 @@
 
         # line = accessibles;features
         line = line.split(';')
+        features = self.get_features(line)
+        
         # Accessible Ids, expand and store the accessibles.
-        unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
+        #unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
+        unExpAcc = self.parse_unExpAcc(line[0])        
         if len(self.expandedAccessibles.keys())>=100:
             self.expandedAccessibles = {}
             self.changed = True
@@ -205,7 +216,7 @@
                 self.expandedAccessibles[accId] = self.expand_accessibles(accIdAcc)
                 self.changed = True
         accessibles = self.expand_accessibles(unExpAcc)
-        features = self.get_features(line)
+        
         # Get hints:
         if len(line) == 3:
             hints = [self.nameIdDict[d.strip()] for d in line[2].split()]