1
2
3
4
5
6
7
8
9 """
10 A version of first order predicate logic, built on
11 top of the typed lambda calculus.
12 """
13
14 import re
15 import operator
16
17 from nltk.compat import defaultdict
18 from nltk.internals import Counter
19
20 APP = 'APP'
21
22 _counter = Counter()
23
25 LAMBDA = '\\'; LAMBDA_LIST = ['\\']
26
27
28 EXISTS = 'exists'; EXISTS_LIST = ['some', 'exists', 'exist']
29 ALL = 'all'; ALL_LIST = ['all', 'forall']
30
31
32 DOT = '.'
33 OPEN = '('
34 CLOSE = ')'
35 COMMA = ','
36
37
38 NOT = '-'; NOT_LIST = ['not', '-', '!']
39 AND = '&'; AND_LIST = ['and', '&', '^']
40 OR = '|'; OR_LIST = ['or', '|']
41 IMP = '->'; IMP_LIST = ['implies', '->', '=>']
42 IFF = '<->'; IFF_LIST = ['iff', '<->', '<=>']
43 EQ = '='; EQ_LIST = ['=', '==']
44 NEQ = '!='; NEQ_LIST = ['!=']
45
46
47 BINOPS = AND_LIST + OR_LIST + IMP_LIST + IFF_LIST
48 QUANTS = EXISTS_LIST + ALL_LIST
49 PUNCT = [DOT, OPEN, CLOSE, COMMA]
50
51 TOKENS = BINOPS + EQ_LIST + NEQ_LIST + QUANTS + LAMBDA_LIST + PUNCT + NOT_LIST
52
53
54 SYMBOLS = [x for x in TOKENS if re.match(r'^[-\\.(),!&^|>=<]*$', x)]
55
56
64
66 """
67 Equality predicates
68 """
69 names = ["equality", "inequality"]
70 for pair in zip(names, [Tokens.EQ, Tokens.NEQ]):
71 print "%-15s\t%s" % pair
72
80
81
84 """
85 @param name: the name of the variable
86 """
87 assert isinstance(name, str), "%s is not a string" % name
88 self.name = name
89
92
94 return not (self == other)
95
98
101
102 - def visit(self, function, combinator, default):
104
106 return hash(self.name)
107
110
112 return 'Variable(\'' + self.name + '\')'
116 """
117 Return a new, unique variable.
118 param pattern: C{Variable} that is being replaced. The new variable must
119 be the same type.
120 param term: a C{set} of C{Variable}s that should not be returned from
121 this function.
122 return: C{Variable}
123 """
124 if pattern is not None:
125 if is_indvar(pattern.name):
126 prefix = 'z'
127 elif is_funcvar(pattern.name):
128 prefix = 'F'
129 elif is_eventvar(pattern.name):
130 prefix = 'e0'
131 else:
132 assert False, "Cannot generate a unique constant"
133 else:
134 prefix = 'z'
135
136 v = Variable(prefix + str(_counter.get()))
137 while ignore is not None and v in ignore:
138 v = Variable(prefix + str(_counter.get()))
139 return v
140
151
152
156
158 return hash(str(self))
159
205
209
211 return other == ANY_TYPE or self == other
212
214 if self.matches(other):
215 return self
216 else:
217 return None
218
225
232
239
240 -class AnyType(BasicType, ComplexType):
243
244 first = property(lambda self: self)
245 second = property(lambda self: self)
246
249
252
255
258
261
262
263 TRUTH_TYPE = TruthValueType()
264 ENTITY_TYPE = EntityType()
265 EVENT_TYPE = EventType()
266 ANY_TYPE = AnyType()
267
268
270 assert isinstance(type_string, str)
271 type_string = type_string.replace(' ', '')
272
273 if type_string[0] == '<':
274 assert type_string[-1] == '>'
275 paren_count = 0
276 for i,char in enumerate(type_string):
277 if char == '<':
278 paren_count += 1
279 elif char == '>':
280 paren_count -= 1
281 assert paren_count > 0
282 elif char == ',':
283 if paren_count == 1:
284 break
285 return ComplexType(parse_type(type_string[1 :i ]),
286 parse_type(type_string[i+1:-1]))
287 elif type_string[0] == str(ENTITY_TYPE):
288 return ENTITY_TYPE
289 elif type_string[0] == str(TRUTH_TYPE):
290 return TRUTH_TYPE
291 elif type_string[0] == str(ANY_TYPE):
292 return ANY_TYPE
293 else:
294 raise ParseException("Unexpected character: '%s'." % type_string[0])
295
296
300
302 - def __init__(self, variable, expression=None):
303 if expression:
304 msg = "The variable \'%s\' was found in multiple places with different"\
305 " types in \'%s\'." % (variable, expression)
306 else:
307 msg = "The variable \'%s\' was found in multiple places with different"\
308 " types." % (variable)
309 Exception.__init__(self, msg)
312 - def __init__(self, expression, other_type):
313 Exception.__init__(self, "The type of '%s', '%s', cannot be "
314 "resolved with type '%s'" % \
315 (expression, expression.type, other_type))
318 - def __init__(self, expression, other_type, allowed_type):
319 Exception.__init__(self, "Cannot set type of %s '%s' to '%s'; "
320 "must match type '%s'." %
321 (expression.__class__.__name__, expression,
322 other_type, allowed_type))
326 """
327 Ensure correct typing across a collection of C{Expression}s.
328 @param expressions: a collection of expressions
329 @param signature: C{dict} that maps variable names to types (or string
330 representations of types)
331 """
332
333 for expression in expressions:
334 signature = expression.typecheck(signature)
335
336 for expression in expressions[:-1]:
337 expression.typecheck(signature)
338 return signature
339
340
342 """
343 An interface for classes that can perform substitutions for
344 variables.
345 """
347 """
348 @return: The object that is obtained by replacing
349 each variable bound by C{bindings} with its values.
350 Aliases are already resolved. (maybe?)
351 @rtype: (any)
352 """
353 raise NotImplementedError()
354
356 """
357 @return: A list of all variables in this object.
358 """
359 raise NotImplementedError()
360
361
363 """This is the base abstract object for all logical expressions"""
364
365 - def __call__(self, other, *additional):
366 accum = self.applyto(other)
367 for a in additional:
368 accum = accum(a)
369 return accum
370
374
377
379 """If this is a negated expression, remove the negation.
380 Otherwise add a negation."""
381 return -self
382
386
388 assert isinstance(other, Expression), "%s is not an Expression" % other
389 return OrExpression(self, other)
390
394
398
400 raise NotImplementedError()
401
403 return not (self == other)
404
405 - def equiv(self, other, prover=None):
406 """
407 Check for logical equivalence.
408 Pass the expression (self <-> other) to the theorem prover.
409 If the prover says it is valid, then the self and other are equal.
410
411 @param other: an C{Expression} to check equality against
412 @param prover: a C{nltk.inference.api.Prover}
413 """
414 assert isinstance(other, Expression), "%s is not an Expression" % other
415
416 if prover is None:
417 from nltk.inference import Prover9
418 prover = Prover9()
419 bicond = IffExpression(self.simplify(), other.simplify())
420 return prover.prove(bicond)
421
423 return hash(repr(self))
424
440
442 """
443 Infer and check types. Raise exceptions if necessary.
444 @param signature: C{dict} that maps variable names to types (or string
445 representations of types)
446 @return: the signature, plus any additional type mappings
447 """
448 sig = defaultdict(list)
449 if signature:
450 for (key, val) in signature.iteritems():
451 varEx = VariableExpression(Variable(key))
452 if isinstance(val, Type):
453 varEx.type = val
454 else:
455 varEx.type = parse_type(val)
456 sig[key].append(varEx)
457
458 self._set_type(signature=sig)
459
460 return dict([(key, vars[0].type) for (key, vars) in sig.iteritems()])
461
463 """
464 Find the type of the given variable as it is used in this expression.
465 For example, finding the type of "P" in "P(x) & Q(x,y)" yields "<e,t>"
466 @param variable: C{Variable}
467 """
468 raise NotImplementedError()
469
471 """
472 Set the type of this expression to be the given type. Raise type
473 exceptions where applicable.
474 @param other_type: C{Type} to set
475 @param signature: C{dict<str, list<AbstractVariableExpression>>} store
476 all variable expressions with a given name
477 """
478 raise NotImplementedError()
479
480 - def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
481 """
482 Replace every instance of 'variable' with 'expression'
483 @param variable: C{Variable} The variable to replace
484 @param expression: C{Expression} The expression with which to replace it
485 @param replace_bound: C{boolean} Should bound variables be replaced?
486 """
487 assert isinstance(variable, Variable), "%s is not a Variable" % variable
488 assert isinstance(expression, Expression), "%s is not an Expression" % expression
489
490 def combinator(a, *additional):
491 if len(additional) == 0:
492 return self.__class__(a)
493 elif len(additional) == 1:
494 return self.__class__(a, additional[0])
495
496 return self.visit(lambda e: e.replace(variable, expression, replace_bound, alpha_convert),
497 combinator, set())
498
510
511 result = self
512 for i,v in enumerate(sorted(list(f(self)))):
513 if is_eventvar(v.name):
514 newVar = 'e0%s' % (i+1)
515 else:
516 newVar = 'z%s' % (i+1)
517 result = result.replace(v,
518 self.make_VariableExpression(Variable(newVar)), True)
519 return result
520
521 - def visit(self, function, combinator, default):
522 """
523 Recursively visit sub expressions
524 @param function: C{Function} to call on each sub expression
525 @param combinator: C{Function} to combine the results of the
526 function calls
527 @return: result of combination
528 """
529 raise NotImplementedError()
530
532 return '<%s %s>' % (self.__class__.__name__, self)
533
536
538 """
539 Return a set of all the variables that are available to be replaced.
540 This includes free (non-bound) variables as well as predicates.
541 @return: C{set} of C{Variable}s
542 """
543 return self.visit(lambda e: isinstance(e,Variable) and
544 set([e]) or e.variables(),
545 lambda *parts: reduce(operator.or_, parts), set())
546
547 - def free(self, indvar_only=True):
548 """
549 Return a set of all the free (non-bound) variables in self. Variables
550 serving as predicates are not included.
551 @param indvar_only: C{boolean} only return individual variables?
552 @return: C{set} of C{Variable}s
553 """
554 return self.visit(lambda e: isinstance(e,Variable) and
555 set([e]) or e.free(indvar_only),
556 lambda *parts: reduce(operator.or_, parts), set())
557
559 """
560 @return: beta-converted version of this expression
561 """
562 def combinator(a, *additional):
563 if len(additional) == 0:
564 return self.__class__(a)
565 elif len(additional) == 1:
566 return self.__class__(a, additional[0])
567
568 return self.visit(lambda e: isinstance(e,Variable)
569 and e or e.simplify(), combinator, set())
570
573
574
576 r"""
577 This class is used to represent two related types of logical expressions.
578
579 The first is a Predicate Expression, such as "P(x,y)". A predicate
580 expression is comprised of a C{FunctionVariableExpression} or
581 C{ConstantExpression} as the predicate and a list of Expressions as the
582 arguments.
583
584 The second is a an application of one expression to another, such as
585 "(\x.dog(x))(fido)".
586
587 The reason Predicate Expressions are treated as Application Expressions is
588 that the Variable Expression predicate of the expression may be replaced
589 with another Expression, such as a LambdaExpression, which would mean that
590 the Predicate should be thought of as being applied to the arguments.
591
592 The LogicParser will always curry arguments in a application expression.
593 So, "\x y.see(x,y)(john,mary)" will be represented internally as
594 "((\x y.(see(x))(y))(john))(mary)". This simplifies the internals since
595 there will always be exactly one argument in an application.
596
597 The str() method will usually print the curried forms of application
598 expressions. The one exception is when the the application expression is
599 really a predicate expression (ie, underlying function is an
600 C{AbstractVariableExpression}). This means that the example from above
601 will be returned as "(\x y.see(x,y)(john))(mary)".
602 """
603 - def __init__(self, function, argument):
604 """
605 @param function: C{Expression}, for the function expression
606 @param argument: C{Expression}, for the argument
607 """
608 assert isinstance(function, Expression), "%s is not an Expression" % function
609 assert isinstance(argument, Expression), "%s is not an Expression" % argument
610 self.function = function
611 self.argument = argument
612
614 function = self.function.simplify()
615 argument = self.argument.simplify()
616 if isinstance(function, LambdaExpression):
617 return function.term.replace(function.variable, argument).simplify()
618 else:
619 return self.__class__(function, argument)
620
621 - def free(self, indvar_only=True):
622 """@see: Expression.free()"""
623 if isinstance(self.function, AbstractVariableExpression):
624 return self.argument.free(indvar_only)
625 else:
626 return self.function.free(indvar_only) | \
627 self.argument.free(indvar_only)
628
634
635 type = property(_get_type)
636
638 """@see Expression._set_type()"""
639 assert isinstance(other_type, Type)
640
641 if signature == None:
642 signature = defaultdict(list)
643
644 self.argument._set_type(ANY_TYPE, signature)
645 try:
646 self.function._set_type(ComplexType(self.argument.type, other_type), signature)
647 except TypeResolutionException:
648 raise TypeException(
649 "The function '%s' is of type '%s' and cannot be applied "
650 "to '%s' of type '%s'. Its argument must match type '%s'."
651 % (self.function, self.function.type, self.argument,
652 self.argument.type, self.function.type.first))
653
655 """@see Expression.findtype()"""
656 assert isinstance(variable, Variable), "%s is not a Variable" % variable
657 function, args = self.uncurry()
658 if not isinstance(function, AbstractVariableExpression):
659
660 function = self.function
661 args = [self.argument]
662
663 found = [arg.findtype(variable) for arg in [function]+args]
664
665 unique = []
666 for f in found:
667 if f != ANY_TYPE:
668 if unique:
669 for u in unique:
670 if f.matches(u):
671 break
672 else:
673 unique.append(f)
674
675 if len(unique) == 1:
676 return list(unique)[0]
677 else:
678 return ANY_TYPE
679
680 - def visit(self, function, combinator, default):
681 """@see: Expression.visit()"""
682 return combinator(function(self.function), function(self.argument))
683
685 return isinstance(other, ApplicationExpression) and \
686 self.function == other.function and \
687 self.argument == other.argument
688
716
718 """
719 Uncurry this application expression
720
721 return: A tuple (base-function, arg-list)
722 """
723 function = self.function
724 args = [self.argument]
725 while isinstance(function, ApplicationExpression):
726
727 args.insert(0, function.argument)
728 function = function.function
729 return (function, args)
730
731 args = property(lambda self: self.uncurry()[1], doc="uncurried arg-list")
732
734 """This class represents a variable to be used as a predicate or entity"""
736 """
737 @param variable: C{Variable}, for the variable
738 """
739 assert isinstance(variable, Variable), "%s is not a Variable" % variable
740 self.variable = variable
741
744
745 - def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
746 """@see: Expression.replace()"""
747 assert isinstance(variable, Variable), "%s is not an Variable" % variable
748 assert isinstance(expression, Expression), "%s is not an Expression" % expression
749 if self.variable == variable:
750 return expression
751 else:
752 return self
753
770
772 """@see Expression.findtype()"""
773 assert isinstance(variable, Variable), "%s is not a Variable" % variable
774 if self.variable == variable:
775 return self.type
776 else:
777 return ANY_TYPE
778
779 - def visit(self, function, combinator, default):
780 """@see: Expression.visit()"""
781 return combinator(function(self.variable))
782
784 """Allow equality between instances of C{AbstractVariableExpression}
785 subtypes."""
786 return isinstance(other, AbstractVariableExpression) and \
787 self.variable == other.variable
788
790 return str(self.variable)
791
792
794 """This class represents variables that take the form of a single lowercase
795 character (other than 'e') followed by zero or more digits."""
807
808 type = property(lambda self: ENTITY_TYPE, _set_type)
809
811 """This class represents variables that take the form of a single uppercase
812 character followed by zero or more digits."""
813 type = ANY_TYPE
814
815 - def free(self, indvar_only=True):
816 """@see: Expression.free()"""
817 if not indvar_only:
818 return set([self.variable])
819 else:
820 return set()
821
823 """This class represents variables that take the form of a single lowercase
824 'e' character followed by zero or more digits."""
825 type = EVENT_TYPE
826
828 """This class represents variables that do not take the form of a single
829 character followed by zero or more digits."""
830 type = ENTITY_TYPE
831
855
856 - def free(self, indvar_only=True):
857 """@see: Expression.free()"""
858 if not indvar_only:
859 return set([self.variable])
860 else:
861 return set()
862
863
878
879
881 """This an abstract class for any Expression that binds a variable in an
882 Expression. This includes LambdaExpressions and Quantified Expressions"""
884 """
885 @param variable: C{Variable}, for the variable
886 @param term: C{Expression}, for the term
887 """
888 assert isinstance(variable, Variable), "%s is not a Variable" % variable
889 assert isinstance(term, Expression), "%s is not an Expression" % term
890 self.variable = variable
891 self.term = term
892
893 - def replace(self, variable, expression, replace_bound=False, alpha_convert=True):
894 """@see: Expression.replace()"""
895 assert isinstance(variable, Variable), "%s is not a Variable" % variable
896 assert isinstance(expression, Expression), "%s is not an Expression" % expression
897
898 if self.variable == variable:
899 if replace_bound:
900 assert isinstance(expression, AbstractVariableExpression),\
901 "%s is not a AbstractVariableExpression" % expression
902 return self.__class__(expression.variable,
903 self.term.replace(variable, expression, True, alpha_convert))
904 else:
905 return self
906 else:
907
908
909 if alpha_convert and self.variable in expression.free():
910 self = self.alpha_convert(unique_variable(pattern=self.variable))
911
912
913 return self.__class__(self.variable,
914 self.term.replace(variable, expression, replace_bound, alpha_convert))
915
917 """Rename all occurrences of the variable introduced by this variable
918 binder in the expression to @C{newvar}.
919 @param newvar: C{Variable}, for the new variable
920 """
921 assert isinstance(newvar, Variable), "%s is not a Variable" % newvar
922 return self.__class__(newvar,
923 self.term.replace(self.variable,
924 VariableExpression(newvar),
925 True))
926
928 """@see: Expression.variables()"""
929 return self.term.variables() - set([self.variable])
930
931 - def free(self, indvar_only=True):
932 """@see: Expression.free()"""
933 return self.term.free(indvar_only) - set([self.variable])
934
936 """@see Expression.findtype()"""
937 assert isinstance(variable, Variable), "%s is not a Variable" % variable
938 if variable == self.variable:
939 return ANY_TYPE
940 else:
941 return self.term.findtype(variable)
942
943 - def visit(self, function, combinator, default):
944 """@see: Expression.visit()"""
945 return combinator(function(self.variable), function(self.term))
946
948 r"""Defines equality modulo alphabetic variance. If we are comparing
949 \x.M and \y.N, then check equality of M and N[x/y]."""
950 if isinstance(self, other.__class__) or \
951 isinstance(other, self.__class__):
952 if self.variable == other.variable:
953 return self.term == other.term
954 else:
955
956 varex = VariableExpression(self.variable)
957 return self.term == other.term.replace(other.variable, varex)
958 else:
959 return False
960
961
986
987
1010
1014
1018
1019
1022 assert isinstance(term, Expression), "%s is not an Expression" % term
1023 self.term = term
1024
1025 type = property(lambda self: TRUTH_TYPE)
1026
1037
1039 assert isinstance(variable, Variable), "%s is not a Variable" % variable
1040 return self.term.findtype(variable)
1041
1042 - def visit(self, function, combinator, default):
1043 """@see: Expression.visit()"""
1044 return combinator(function(self.term))
1045
1047 """@see: Expression.negate()"""
1048 return self.term
1049
1052
1063
1064 type = property(lambda self: TRUTH_TYPE)
1065
1077
1078 - def visit(self, function, combinator, default):
1081
1083 return (isinstance(self, other.__class__) or \
1084 isinstance(other, self.__class__)) and \
1085 self.first == other.first and self.second == other.second
1086
1092
1095
1096
1109
1111 """This class represents conjunctions"""
1114
1116 s = str(subex)
1117 if isinstance(subex, AndExpression):
1118 return s[1:-1]
1119 return s
1120
1122 """This class represents disjunctions"""
1125
1127 s = str(subex)
1128 if isinstance(subex, OrExpression):
1129 return s[1:-1]
1130 return s
1131
1133 """This class represents implications"""
1136
1138 """This class represents biconditionals"""
1141
1142
1144 """This class represents equality expressions like "(x = y)"."""
1156
1159
1160
1162 """A lambda calculus expression parser."""
1163
1165 """
1166 @param type_check: C{boolean} should type checking be performed?
1167 to their types.
1168 """
1169 assert isinstance(type_check, bool)
1170
1171 self._currentIndex = 0
1172 self._buffer = []
1173 self.type_check = type_check
1174
1175 """A list of tuples of quote characters. The 4-tuple is comprised
1176 of the start character, the end character, the escape character, and
1177 a boolean indicating whether the quotes should be included in the
1178 result. Quotes are used to signify that a token should be treated as
1179 atomic, ignoring any special characters within the token. The escape
1180 character allows the quote end character to be used within the quote.
1181 If True, the boolean indicates that the final token should contain the
1182 quote and escape characters.
1183 This method exists to be overridden"""
1184 self.quote_chars = []
1185
1186 self.operator_precedence = dict(
1187 [(x,1) for x in Tokens.LAMBDA_LIST] + \
1188 [(x,2) for x in Tokens.NOT_LIST] + \
1189 [(APP,3)] + \
1190 [(x,4) for x in Tokens.EQ_LIST+Tokens.NEQ_LIST] + \
1191 [(x,5) for x in Tokens.QUANTS] + \
1192 [(x,6) for x in Tokens.AND_LIST] + \
1193 [(x,7) for x in Tokens.OR_LIST] + \
1194 [(x,8) for x in Tokens.IMP_LIST] + \
1195 [(x,9) for x in Tokens.IFF_LIST] + \
1196 [(None,10)])
1197 self.right_associated_operations = [APP]
1198
1199 - def parse(self, data, signature=None):
1225
1227 """Split the data into tokens"""
1228 out = []
1229 mapping = {}
1230 tokenTrie = StringTrie(self.get_all_symbols())
1231 token = ''
1232 data_idx = 0
1233 token_start_idx = data_idx
1234 while data_idx < len(data):
1235 cur_data_idx = data_idx
1236 quoted_token, data_idx = self.process_quoted_token(data_idx, data)
1237 if quoted_token:
1238 if not token:
1239 token_start_idx = cur_data_idx
1240 token += quoted_token
1241 continue
1242
1243 st = tokenTrie
1244 c = data[data_idx]
1245 symbol = ''
1246 while c in st:
1247 symbol += c
1248 st = st[c]
1249 if len(data)-data_idx > len(symbol):
1250 c = data[data_idx+len(symbol)]
1251 else:
1252 break
1253 if StringTrie.LEAF in st:
1254
1255 if token:
1256 mapping[len(out)] = token_start_idx
1257 out.append(token)
1258 token = ''
1259 mapping[len(out)] = data_idx
1260 out.append(symbol)
1261 data_idx += len(symbol)
1262 else:
1263 if data[data_idx] in ' \t\n':
1264 if token:
1265 mapping[len(out)] = token_start_idx
1266 out.append(token)
1267 token = ''
1268 else:
1269 if not token:
1270 token_start_idx = data_idx
1271 token += data[data_idx]
1272 data_idx += 1
1273 if token:
1274 mapping[len(out)] = token_start_idx
1275 out.append(token)
1276 mapping[len(out)] = len(data)
1277 mapping[len(out)+1] = len(data)+1
1278 return out, mapping
1279
1281 token = ''
1282 c = data[data_idx]
1283 i = data_idx
1284 for start, end, escape, incl_quotes in self.quote_chars:
1285 if c == start:
1286 if incl_quotes:
1287 token += c
1288 i += 1
1289 while data[i] != end:
1290 if data[i] == escape:
1291 if incl_quotes:
1292 token += data[i]
1293 i += 1
1294 if len(data) == i:
1295 raise ParseException(None, "End of input reached. "
1296 "Escape character [%s] found at end."
1297 % escape)
1298 token += data[i]
1299 else:
1300 token += data[i]
1301 i += 1
1302 if len(data) == i:
1303 raise ParseException(None, "End of input reached. "
1304 "Expected: [%s]" % end)
1305 if incl_quotes:
1306 token += data[i]
1307 i += 1
1308 if not token:
1309 raise ParseException(None, 'Empty quoted token found')
1310 break
1311 return token, i
1312
1314 """This method exists to be overridden"""
1315 return Tokens.SYMBOLS
1316
1318 """Return TRUE if the given location is within the buffer"""
1319 return self._currentIndex+location < len(self._buffer)
1320
1321 - def token(self, location=None):
1322 """Get the next waiting token. If a location is given, then
1323 return the token at currentIndex+location without advancing
1324 currentIndex; setting it gives lookahead/lookback capability."""
1325 try:
1326 if location == None:
1327 tok = self._buffer[self._currentIndex]
1328 self._currentIndex += 1
1329 else:
1330 tok = self._buffer[self._currentIndex+location]
1331 return tok
1332 except IndexError:
1333 raise ExpectedMoreTokensException(self._currentIndex+1)
1334
1337
1351
1352 - def handle(self, tok, context):
1369
1378
1381
1384
1407
1418
1439
1462
1472
1474 return factory(variable, term)
1475
1481
1494
1496 """This method serves as a hook for other logic parsers that
1497 have different equality expression classes"""
1498 return EqualityExpression(first, second)
1499
1514
1528
1531
1533 """Attempt to make an application expression. The next tokens are
1534 a list of arguments in parens, then the argument expression is a
1535 function being applied to the arguments. Otherwise, return the
1536 argument expression."""
1537 if self.has_priority(APP, context):
1538 if self.inRange(0) and self.token(0) == Tokens.OPEN:
1539 if not isinstance(expression, LambdaExpression) and \
1540 not isinstance(expression, ApplicationExpression) and \
1541 not isinstance(expression, FunctionVariableExpression) and \
1542 not isinstance(expression, ConstantExpression):
1543 raise ParseException(self._currentIndex,
1544 "The function '" + str(expression) +
1545 "' is not a Lambda Expression, an "
1546 "Application Expression, or a "
1547 "functional predicate, so it may "
1548 "not take arguments.")
1549 self.token()
1550
1551 accum = self.make_ApplicationExpression(expression, self.parse_Expression(APP))
1552 while self.inRange(0) and self.token(0) == Tokens.COMMA:
1553 self.token()
1554 accum = self.make_ApplicationExpression(accum, self.parse_Expression(APP))
1555 self.assertNextToken(Tokens.CLOSE)
1556 return accum
1557 return expression
1558
1561
1564
1567
1569 return self.operator_precedence[operation] < self.operator_precedence[context] or \
1570 (operation in self.right_associated_operations and \
1571 self.operator_precedence[operation] == self.operator_precedence[context])
1572
1585
1593
1595 if self.inRange(0):
1596 msg = 'Next token: ' + self.token(0)
1597 else:
1598 msg = 'No more tokens'
1599 return '<' + self.__class__.__name__ + ': ' + msg + '>'
1600
1601
1603 LEAF = "<leaf>"
1604
1610
1612 if len(string):
1613 self[string[0]].insert(string[1:])
1614 else:
1615
1616 self[StringTrie.LEAF] = None
1617
1618
1623
1625 - def __init__(self, index, unexpected=None, expected=None, message=None):
1626 if unexpected and expected:
1627 msg = "Unexpected token: '%s'. " \
1628 "Expected token '%s'." % (unexpected, expected)
1629 elif unexpected:
1630 msg = "Unexpected token: '%s'." % unexpected
1631 if message:
1632 msg += ' '+message
1633 else:
1634 msg = "Expected token '%s'." % expected
1635 ParseException.__init__(self, index, msg)
1638 - def __init__(self, index, message=None):
1639 if not message:
1640 message = 'More tokens expected.'
1641 ParseException.__init__(self, index, 'End of input found. ' + message)
1645 """
1646 An individual variable must be a single lowercase character other than 'e',
1647 followed by zero or more digits.
1648
1649 @param expr: C{str}
1650 @return: C{boolean} True if expr is of the correct form
1651 """
1652 assert isinstance(expr, str), "%s is not a string" % expr
1653 return re.match(r'^[a-df-z]\d*$', expr) is not None
1654
1656 """
1657 A function variable must be a single uppercase character followed by
1658 zero or more digits.
1659
1660 @param expr: C{str}
1661 @return: C{boolean} True if expr is of the correct form
1662 """
1663 assert isinstance(expr, str), "%s is not a string" % expr
1664 return re.match(r'^[A-Z]\d*$', expr) is not None
1665
1667 """
1668 An event variable must be a single lowercase 'e' character followed by
1669 zero or more digits.
1670
1671 @param expr: C{str}
1672 @return: C{boolean} True if expr is of the correct form
1673 """
1674 assert isinstance(expr, str), "%s is not a string" % expr
1675 return re.match(r'^e\d*$', expr) is not None
1676
1677
1679 p = LogicParser().parse
1680 print '='*20 + 'Test parser' + '='*20
1681 print p(r'john')
1682 print p(r'man(x)')
1683 print p(r'-man(x)')
1684 print p(r'(man(x) & tall(x) & walks(x))')
1685 print p(r'exists x.(man(x) & tall(x) & walks(x))')
1686 print p(r'\x.man(x)')
1687 print p(r'\x.man(x)(john)')
1688 print p(r'\x y.sees(x,y)')
1689 print p(r'\x y.sees(x,y)(a,b)')
1690 print p(r'(\x.exists y.walks(x,y))(x)')
1691 print p(r'exists x.x = y')
1692 print p(r'exists x.(x = y)')
1693 print p('P(x) & x=y & P(y)')
1694 print p(r'\P Q.exists x.(P(x) & Q(x))')
1695 print p(r'man(x) <-> tall(x)')
1696
1697 print '='*20 + 'Test simplify' + '='*20
1698 print p(r'\x.\y.sees(x,y)(john)(mary)').simplify()
1699 print p(r'\x.\y.sees(x,y)(john, mary)').simplify()
1700 print p(r'all x.(man(x) & (\x.exists y.walks(x,y))(x))').simplify()
1701 print p(r'(\P.\Q.exists x.(P(x) & Q(x)))(\x.dog(x))(\x.bark(x))').simplify()
1702
1703 print '='*20 + 'Test alpha conversion and binder expression equality' + '='*20
1704 e1 = p('exists x.P(x)')
1705 print e1
1706 e2 = e1.alpha_convert(Variable('z'))
1707 print e2
1708 print e1 == e2
1709
1725
1731
1734
1735 if __name__ == '__main__':
1736 demo()
1737 demo_errors()
1738