/
logic.py
165 lines (143 loc) · 4.78 KB
/
logic.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
"""This module implements a declarative Logic language using Scheme syntax.
Logic is a variant of the Prolog language, based on scmlog by Paul Hilfinger
and the logic programming example in SICP.
All valid logic expressions are Scheme lists. Valid forms include:
(fact ...): Assert a consequent, followed by zero or more hypotheses
(query ...): Query zero or more relations simultaneously
(load PATH): Load a .logic file by evaluating its expressions
"""
from scheme import Frame
from scheme_reader import Pair, nil, read_line
from scheme_primitives import *
from ucb import main, trace
import scheme
import scheme_reader
import scheme_test
facts = []
#############
# Inference #
#############
def do_query(clauses):
"""Yield all bindings that simultaneously satisfy clauses."""
for env in search(clauses, Frame(None), 0):
yield [(v, ground(v, env)) for v in get_vars(clauses)]
DEPTH_LIMIT = 20
def search(clauses, env, depth):
"""Search for an application of rules to establish all the clauses,
non-destructively extending the unifier env. Limit the search to
the nested application of depth rules."""
if clauses is nil:
yield env
elif DEPTH_LIMIT is None or depth <= DEPTH_LIMIT:
for fact in facts:
fact = rename_variables(fact, get_unique_id())
env_head = Frame(env)
if unify(fact.first, clauses.first, env_head):
for env_rule in search(fact.second, env_head, depth+1):
for result in search(clauses.second, env_rule, depth+1):
yield result
def unify(e, f, env):
"""Destructively extend env so as to unify (make equal) e and f, returning
True if this succeeds and False otherwise. env may be modified in either
case (its existing bindings are never changed)."""
e = lookup(e, env)
f = lookup(f, env)
if e == f:
return True
elif isvar(e):
env.define(e, f)
return True
elif isvar(f):
env.define(f, e)
return True
elif scheme_atomp(e) or scheme_atomp(f):
return False
else:
return unify(e.first, f.first, env) and unify(e.second, f.second, env)
################
# Environments #
################
def lookup(sym, env):
"""Look up a symbol repeatedly until it is fully resolved."""
try:
return lookup(env.lookup(sym), env)
except:
return sym
def ground(expr, env):
"""Replace all variables with their values in expr."""
if scheme_symbolp(expr):
resolved = lookup(expr, env)
if expr != resolved:
return ground(resolved, env)
else:
return expr
elif scheme_pairp(expr):
return Pair(ground(expr.first, env), ground(expr.second, env))
else:
return expr
#####################
# Support functions #
#####################
def get_vars(expr):
"""Return all logical vars in expr as a list."""
if isvar(expr):
return [expr]
elif scheme_pairp(expr):
vs = get_vars(expr.first)
for v in get_vars(expr.second):
if v not in vs:
vs.append(v)
return vs
else:
return []
IDENTIFIER = 0
def get_unique_id():
"""Return a unique identifier."""
global IDENTIFIER
IDENTIFIER += 1
return IDENTIFIER
def rename_variables(expr, n):
"""Rename all variables in expr with an identifier N."""
if isvar(expr):
return expr + '_' + str(n)
elif scheme_pairp(expr):
return Pair(rename_variables(expr.first, n),
rename_variables(expr.second, n))
else:
return expr
def isvar(symbol):
"""Return whether symbol is a logical variable."""
return scheme_symbolp(symbol) and symbol.startswith("?")
##################
# User Interface #
##################
def process_input(expr, env):
"""Process an input expr, which may be a fact or query."""
assert scheme_listp(expr)
if expr.first in ("fact", "!"):
facts.append(expr.second)
elif expr.first in ("query", "?"):
results = do_query(expr.second)
success = False
for result in results:
if not success:
print('Success!')
success = True
result_str = "\t".join("{0}: {1}".format(k[1:], v) for k, v in result)
if result_str:
print(result_str)
if not success:
print('Failed.')
elif expr.first == "load":
scheme.scheme_load(expr.second.first, env)
else:
print("Please provide a fact or query.")
@main
def run(*argv):
scheme_reader.buffer_input.__defaults__ = ('logic> ',)
scheme_reader.buffer_lines.__defaults__ = ('logic> ',)
scheme.scheme_eval = process_input
if argv and argv[0] == '-test':
scheme_test.run_tests(*argv[1:])
else:
scheme.run(*argv)