annotate lab4/test/pprolog.p @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
rev   line source
0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1 (* A prolog interpreter running a program that computes tilings *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
3 (* This program is the output of a macro processor, so contains many
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
4 untidy expressions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7 (* tunable parameters *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8 const
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9 MAXSYMBOLS = 511; (* max no. of symbols *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10 HASHFACTOR = 90; (* percent loading factor for hash table *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11 MAXCHARS = 2048; (* max chars in symbols *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12 MAXSTRING = 128; (* max string length *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 MAXARITY = 63; (* max arity of function, vars in clause *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14 MEMSIZE = 25000; (* size of |mem| array *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 (* special character values *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17 const ENDSTR = chr(0); (* end of string *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18 TAB = chr(9); (* tab character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 ENDLINE = chr(10); (* newline character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 ENDFILE = chr(127); (* end of file *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22 var run: boolean; (* whether execution should continue *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23 dflag: boolean; (* switch for debugging code *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25 type
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 permstring = integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 tempstring = array MAXSTRING of char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30 charptr: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 charbuf: array MAXCHARS of char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33 (* |StringLength| -- length of a tempstring *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34 proc StringLength(var s: tempstring): integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37 i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 while s[i] <> ENDSTR do i := i+1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39 return i
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 (* |SaveString| -- make a tempstring permanent *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43 proc SaveString(var s: tempstring): permstring;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 var p, i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46 if charptr + StringLength(s) + 1 > MAXCHARS then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 newline(); print_string("Panic: "); print_string("out of string space"); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 p := charptr; i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50 repeat
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 charbuf[charptr] := s[i]; charptr := charptr+1; i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52 until charbuf[charptr-1] = ENDSTR;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56 (* |StringEqual| -- compare a tempstring to a permstring *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 proc StringEqual(var s1: tempstring; s2: permstring): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 while (s1[i] <> ENDSTR) and (s1[i] = charbuf[s2+i]) do i := i+1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 return (s1[i] = charbuf[s2+i])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 (* |WriteString| -- print a permstring *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 proc WriteString(s: permstring);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 i := s;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 while charbuf[i] <> ENDSTR do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 print_char(charbuf[i]); i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 type
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 ptr = integer; (* index into |mem| array *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 const NULL = 0; (* null pointer *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80 type term = ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82 const FUNC = 1; (* compound term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 INT = 2; (* integer *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 CHRCTR = 3; (* character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 CELL = 4; (* variable cell *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 REF = 5; (* variable reference *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 UNDO = 6; (* trail item *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 const TERM_SIZE = 2; (* \dots\ plus no. of args *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92 lsp, gsp, hp, hmark: ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 mem: array MEMSIZE+1 of integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95 (* |LocAlloc| -- allocate space on local stack *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 proc LocAlloc(size: integer): ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 var p: ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 if lsp + size >= gsp then newline(); print_string("Panic: "); print_string("out of stack space"); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 p := lsp + 1; lsp := lsp + size; return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 (* |GloAlloc| -- allocate space on global stack *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 proc GloAlloc(kind, size: integer): ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 var p: ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107 if gsp - size <= lsp then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 newline(); print_string("Panic: "); print_string("out of stack space"); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110 gsp := gsp - size; p := gsp;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111 mem[p] := lsl(kind, 8) + size;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 (* |HeapAlloc| -- allocate space on heap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 proc HeapAlloc(size: integer): ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117 var p: ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119 if hp + size > MEMSIZE then newline(); print_string("Panic: "); print_string("out of heap space"); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120 p := hp + 1; hp := hp + size; return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 var infile: array 3000 of char; pin, pout: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125 proc prog(line: array 60 of char);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 for i := 0 to 59 do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 infile[pin] := line[i]; pin := pin+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131 infile[pin] := ENDLINE; pin := pin+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 proc rdchar(var ch: char);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136 if pout >= pin then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 ch := ENDFILE
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 ch := infile[pout]; pout := pout+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
143 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
144 pbchar: char; (* pushed-back char, else |ENDFILE| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
145 lineno: integer; (* line number in current file *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
146
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
147 (* |GetChar| -- get a character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
148 proc GetChar(): char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
149 var ch: char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
150 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
151 if pbchar <> ENDFILE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
152 ch := pbchar; pbchar := ENDFILE
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
153 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
154 rdchar(ch);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
155 if ch = ENDLINE then lineno := lineno+1 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
156 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
157 return ch
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
158 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
159
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
160 (* |PushBack| -- push back a character on the input *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
161 proc PushBack(ch: char);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
162 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
163 pbchar := ch
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
164 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
165
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
166 type clause = ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
167
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
168 const CLAUSE_SIZE = 4; (* ... plus size of body + 1 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
169
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
170 type frame = ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
171
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
172 const FRAME_SIZE = 7; (* \dots plus space for local variables *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
173
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
174 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
175 current: ptr; (* current goal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
176 call: term; (* |Deref|'ed first literal of goal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
177 goalframe: frame; (* current stack frame *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
178 choice: frame; (* last choice point *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
179 base: frame; (* frame for original goal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
180 prok: clause; (* clauses left to try on current goal *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
181
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
182 (* |Deref| -- follow |VAR| and |CELL| pointers *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
183 proc Deref(t: term; e: frame): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
184 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
185 if t = NULL then newline(); print_string("Panic: "); print_string("Deref"); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
186 if (lsr(mem[t], 8) = REF) and (e <> NULL) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
187 t := (e+7+(mem[t+1]-1)*TERM_SIZE)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
188 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
189 while (lsr(mem[t], 8) = CELL) and (mem[t+1] <> NULL) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
190 t := mem[t+1]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
191 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
192 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
193 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
194
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
195 type symbol = integer; (* index in |symtab| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
196
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
197 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
198 nsymbols: integer; (* number of symbols *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
199 symtab: array MAXSYMBOLS+1 of record
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
200 name: integer; (* print name: index in |charbuf| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
201 arity: integer; (* number of arguments or -1 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
202 action: integer; (* code if built-in, 0 otherwise *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
203 prok: clause (* clause chain *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
204 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
205 cons, eqsym, cutsym, nilsym, notsym: symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
206 node: symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
207
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
208 (* |Lookup| -- convert string to internal symbol *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
209 proc Lookup(var name: tempstring): symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
210 var h, i: integer; p: symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
211 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
212 (* Compute the hash function in |h| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
213 h := 0; i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
214 while name[i] <> ENDSTR do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
215 h := (5 * h + ord(name[i])) mod MAXSYMBOLS; i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
216 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
217
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
218 (* Search the hash table *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
219 p := h+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
220 while symtab[p].name <> -1 do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
221 if StringEqual(name, symtab[p].name) then return p end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
222 p := p-1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
223 if p = 0 then p := MAXSYMBOLS end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
224 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
225
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
226 (* Not found: enter a new symbol *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
227 (* Be careful to avoid overflow on 16 bit machines: *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
228 if nsymbols >= (MAXSYMBOLS div 10) * (HASHFACTOR div 10) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
229 newline(); print_string("Panic: "); print_string("out of symbol space"); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
230 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
231 symtab[p].name := SaveString(name);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
232 symtab[p].arity := -1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
233 symtab[p].action := 0; symtab[p].prok := NULL;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
234 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
235 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
236
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
237 type keyword = array 8 of char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
238
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
239 (* |Enter| -- define a built-in symbol *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
240 proc Enter(name: keyword; arity: integer; action: integer): symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
241 var s: symbol; i: integer; temp: tempstring;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
242 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
243 i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
244 while name[i] <> ' ' do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
245 temp[i] := name[i]; i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
246 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
247 temp[i] := ENDSTR; s := Lookup(temp);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
248 symtab[s].arity := arity; symtab[s].action := action;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
249 return s
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
250 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
251
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
252 (* Codes for built-in relations *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
253 const
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
254 CUT = 1; (* $!/0$ *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
255 CALL = 2; (* |call/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
256 PLUS = 3; (* |plus/3| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
257 TIMES = 4; (* |times/3| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
258 ISINT = 5; (* |integer/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
259 ISCHAR = 6; (* |char/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
260 NAFF = 7; (* |not/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
261 EQUALITY = 8; (* |=/2| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
262 FAIL = 9; (* |false/0| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
263 PRINT = 10; (* |print/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
264 NL = 11; (* |nl/0| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
265
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
266 (* |InitSymbols| -- initialize and define standard symbols *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
267 proc InitSymbols();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
268 var i: integer; dummy: symbol;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
269 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
270 nsymbols := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
271 for i := 1 to MAXSYMBOLS do symtab[i].name := -1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
272 cons := Enter(": ", 2, 0);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
273 cutsym := Enter("! ", 0, CUT);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
274 eqsym := Enter("= ", 2, EQUALITY);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
275 nilsym := Enter("nil ", 0, 0);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
276 notsym := Enter("not ", 1, NAFF);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
277 node := Enter("node ", 2, 0);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
278 dummy := Enter("call ", 1, CALL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
279 dummy := Enter("plus ", 3, PLUS);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
280 dummy := Enter("times ", 3, TIMES);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
281 dummy := Enter("integer ", 1, ISINT);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
282 dummy := Enter("char ", 1, ISCHAR);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
283 dummy := Enter("false ", 0, FAIL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
284 dummy := Enter("print ", 1, PRINT);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
285 dummy := Enter("nl ", 0, NL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
286 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
287
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
288 (* |AddClause| -- insert a clause at the end of its chain *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
289 proc AddClause(c: clause);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
290 var s: symbol; p: clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
291 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
292 s := mem[mem[c+3]+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
293 if symtab[s].action <> 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
294 newline(); print_string("Error: "); print_string("cannot add clauses to built-in relation "); run := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
295 WriteString(symtab[s].name)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
296 elsif symtab[s].prok = NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
297 symtab[s].prok := c
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
298 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
299 p := symtab[s].prok;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
300 while mem[p+2] <> NULL do p := mem[p+2] end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
301 mem[p+2] := c
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
302 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
303 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
304
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
305 type argbuf = array MAXARITY+1 of term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
306
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
307 (* |MakeCompound| -- construct a compound term on the heap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
308 proc MakeCompound(fun: symbol; var arg: argbuf): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
309 var p: term; i, n: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
310 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
311 n := symtab[fun].arity;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
312 p := HeapAlloc(TERM_SIZE+n);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
313 mem[p] := lsl(FUNC, 8) + TERM_SIZE+n;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
314 mem[p+1] := fun;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
315 for i := 1 to n do mem[p+i+1] := arg[i] end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
316 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
317 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
318
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
319 (* |MakeNode| -- construct a compound term with up to 2 arguments *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
320 proc MakeNode(fun: symbol; a1, a2: term): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
321 var arg: argbuf;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
322 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
323 arg[1] := a1; arg[2] := a2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
324 return MakeCompound(fun, arg)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
325 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
326
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
327 var refnode: array MAXARITY+1 of term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
328
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
329 (* |MakeRef| -- return a reference cell prepared earlier *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
330 proc MakeRef(offset: integer): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
331 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
332 return refnode[offset]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
333 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
334
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
335 (* |MakeInt| -- construct an integer node on the heap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
336 proc MakeInt(i: integer): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
337 var p: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
338 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
339 p := HeapAlloc(TERM_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
340 mem[p] := lsl(INT, 8) + TERM_SIZE;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
341 mem[p+1] := i; return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
342 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
343
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
344 (* |MakeChar| -- construct a character node on the heap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
345 proc MakeChar(c: char): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
346 var p: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
347 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
348 p := HeapAlloc(TERM_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
349 mem[p] := lsl(CHRCTR, 8) + TERM_SIZE;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
350 mem[p+1] := ord(c); return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
351 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
352
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
353 (* |MakeString| -- construct a string as a Prolog list of chars *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
354 proc MakeString(var s: tempstring): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
355 var p: term; i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
356 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
357 i := StringLength(s);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
358 p := MakeNode(nilsym, NULL, NULL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
359 while i > 0 do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
360 i := i-1; p := MakeNode(cons, MakeChar(s[i]), p)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
361 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
362 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
363 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
364
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
365 (* |MakeClause| -- construct a clause on the heap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
366 proc MakeClause(nvars: integer; head: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
367 var body: argbuf; nbody: integer): clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
368 var p: clause; i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
369 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
370 p := HeapAlloc(CLAUSE_SIZE + nbody + 1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
371 mem[p] := nvars; mem[p+2] := NULL; mem[p+3] := head;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
372 for i := 1 to nbody do mem[(p+4)+i-1] := body[i] end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
373 mem[(p+4)+nbody+1-1] := NULL;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
374 if head = NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
375 mem[p+1] := 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
376 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
377 mem[p+1] := Key(head, NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
378 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
379 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
380 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
381
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
382 (* operator priorities *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
383 const
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
384 MAXPRIO = 2; (* isolated term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
385 ARGPRIO = 2; (* function arguments *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
386 EQPRIO = 2; (* equals sign *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
387 CONSPRIO = 1; (* colon *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
388
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
389 (* |IsString| -- check if a list represents a string *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
390 proc IsString(t: term; e: frame): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
391 const limit = 128;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
392 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
393 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
394 i := 0; t := Deref(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
395 while i < limit do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
396 if (lsr(mem[t], 8) <> FUNC) or (mem[t+1] <> cons) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
397 return (lsr(mem[t], 8) = FUNC) and (mem[t+1] = nilsym)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
398 elsif lsr(mem[Deref(mem[t+1+1], e)], 8) <> CHRCTR then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
399 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
400 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
401 i := i+1; t := Deref(mem[t+2+1], e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
402 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
403 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
404 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
405 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
406
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
407 (* |IsList| -- check if a term is a proper list *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
408 proc IsList(t: term; e: frame): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
409 const limit = 128;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
410 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
411 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
412 i := 0; t := Deref(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
413 while i < limit do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
414 if (lsr(mem[t], 8) <> FUNC) or (mem[t+1] <> cons) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
415 return (lsr(mem[t], 8) = FUNC) and (mem[t+1] = nilsym)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
416 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
417 i := i+1; t := Deref(mem[t+2+1], e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
418 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
419 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
420 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
421 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
422
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
423 (* |ShowString| -- print a list as a string *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
424 proc ShowString(t: term; e: frame);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
425 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
426 t := Deref(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
427 print_char('"');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
428 while mem[t+1] <> nilsym do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
429 print_char(chr(mem[Deref(mem[t+1+1], e)+1]));
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
430 t := Deref(mem[t+2+1], e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
431 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
432 print_char('"')
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
433 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
434
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
435 (* |PrintCompound| -- print a compound term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
436 proc PrintCompound(t: term; e: frame; prio: integer);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
437 var f: symbol; i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
438 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
439 f := mem[t+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
440 if f = cons then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
441 (* |t| is a list: try printing as a string, or use infix : *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
442 if IsString(t, e) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
443 ShowString(t, e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
444 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
445 if prio < CONSPRIO then print_char('(') end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
446 PrintTerm(mem[t+1+1], e, CONSPRIO-1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
447 print_char(':');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
448 PrintTerm(mem[t+2+1], e, CONSPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
449 if prio < CONSPRIO then print_char(')') end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
450 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
451 elsif f = eqsym then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
452 (* |t| is an equation: use infix = *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
453 if prio < EQPRIO then print_char('(') end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
454 PrintTerm(mem[t+1+1], e, EQPRIO-1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
455 print_string(" = ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
456 PrintTerm(mem[t+2+1], e, EQPRIO-1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
457 if prio < EQPRIO then print_char(')') end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
458 elsif f = notsym then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
459 (* |t| is a literal 'not P' *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
460 print_string("not ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
461 PrintTerm(mem[t+1+1], e, MAXPRIO)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
462 elsif (f = node) and IsList(mem[t+2+1], e) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
463 PrintNode(t, e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
464 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
465 (* use ordinary notation *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
466 WriteString(symtab[f].name);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
467 if symtab[f].arity > 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
468 print_char('(');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
469 PrintTerm(mem[t+1+1], e, ARGPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
470 for i := 2 to symtab[f].arity do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
471 print_string(", ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
472 PrintTerm(mem[t+i+1], e, ARGPRIO)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
473 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
474 print_char(')')
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
475 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
476 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
477 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
478
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
479 (* |PrintNode| -- print and optree node *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
480 proc PrintNode(t: term; e: frame);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
481 var u: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
482 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
483 print_char('<');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
484 PrintTerm(mem[t+1+1], e, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
485 u := Deref(mem[t+2+1], e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
486 while mem[u+1] <> nilsym do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
487 print_string(", ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
488 PrintTerm(mem[u+1+1], e, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
489 u := Deref(mem[u+2+1], e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
490 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
491 print_char('>');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
492 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
493
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
494 (* |PrintTerm| -- print a term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
495 proc PrintTerm(t: term; e: frame; prio: integer);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
496 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
497 t := Deref(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
498 if t = NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
499 print_string("*null-term*")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
500 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
501 case lsr(mem[t], 8) of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
502 FUNC:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
503 PrintCompound(t, e, prio)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
504 | INT:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
505 print_num(mem[t+1])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
506 | CHRCTR:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
507 print_char(''''); print_char(chr(mem[t+1])); print_char('''')
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
508 | CELL:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
509 if (t >= gsp) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
510 print_char('G'); print_num((MEMSIZE - t) div TERM_SIZE)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
511 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
512 print_char('L'); print_num((t - hp) div TERM_SIZE)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
513 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
514 | REF:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
515 print_char('@'); print_num(mem[t+1])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
516 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
517 print_string("*unknown-term(tag=");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
518 print_num(lsr(mem[t], 8)); print_string(")*")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
519 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
520 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
521 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
522
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
523 (* |PrintClause| -- print a clause *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
524 proc PrintClause(c: clause);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
525 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
526 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
527 if c = NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
528 print_string("*null-clause*"); newline();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
529 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
530 if mem[c+3] <> NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
531 PrintTerm(mem[c+3], NULL, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
532 print_char(' ')
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
533 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
534 print_string(":- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
535 if mem[(c+4)+1-1] <> NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
536 PrintTerm(mem[(c+4)+1-1], NULL, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
537 i := 2;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
538 while mem[(c+4)+i-1] <> NULL do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
539 print_string(", ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
540 PrintTerm(mem[(c+4)+i-1], NULL, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
541 i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
542 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
543 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
544 print_char('.'); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
545 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
546 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
547
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
548 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
549 token: integer; (* last token from input *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
550 tokval: symbol; (* if |token = IDENT|, the identifier*)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
551 tokival: integer; (* if |token = NUMBER|, the number *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
552 toksval: tempstring; (* if |token = STRCON|, the string *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
553 errflag: boolean; (* whether recovering from an error *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
554 errcount: integer; (* number of errors found so far *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
555
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
556 (* Possible values for |token|: *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
557 const
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
558 IDENT = 1; (* identifier: see |tokval| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
559 VARIABLE = 2; (* variable: see |tokval| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
560 NUMBER = 3; (* number: see |tokival| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
561 CHCON = 4; (* char constant: see |tokival| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
562 STRCON = 5; (* string constant: see |toksval| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
563 ARROW = 6; (* |':-'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
564 LPAR = 7; (* |'('| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
565 RPAR = 8; (* |')'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
566 COMMA = 9; (* |','| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
567 DOT = 10; (* |'.'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
568 COLON = 11; (* |':'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
569 EQUAL = 12; (* |'='| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
570 NEGATE = 13; (* |'not'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
571 EOFTOK = 14; (* end of file *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
572 LANGLE = 15; (* |'<'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
573 RANGLE = 16; (* |'>'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
574 HASH = 17; (* |'#'| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
575
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
576 (* |ShowError| -- report error location *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
577 proc ShowError();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
578 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
579 errflag := true; errcount := errcount+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
580 print_string("Line "); print_num(lineno); print_char(' ');
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
581 print_string("Syntax error - ")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
582 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
583
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
584 (* |Recover| -- discard rest of input clause *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
585 proc Recover();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
586 var ch: char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
587 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
588 if errcount >= 20 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
589 print_string("Too many errors: I am giving up"); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
590 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
591 if token <> DOT then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
592 repeat
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
593 ch := GetChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
594 until (ch = '.') or (ch = ENDFILE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
595 token := DOT
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
596 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
597 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
598
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
599 (* |Scan| -- read one symbol from |infile| into |token|. *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
600 proc Scan();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
601 var ch, ch2: char; i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
602 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
603 ch := GetChar(); token := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
604 while token = 0 do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
605 (* Loop after white-space or comment *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
606 if ch = ENDFILE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
607 token := EOFTOK
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
608 elsif (ch = ' ') or (ch = TAB) or (ch = ENDLINE) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
609 ch := GetChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
610 elsif ((((ch >= 'A') and (ch <= 'Z')) or (ch = '_')) or ((ch >= 'a') and (ch <= 'z'))) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
611 if (((ch >= 'A') and (ch <= 'Z')) or (ch = '_')) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
612 token := VARIABLE
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
613 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
614 token := IDENT
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
615 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
616 i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
617 while ((((ch >= 'A') and (ch <= 'Z')) or (ch = '_')) or ((ch >= 'a') and (ch <= 'z'))) or ((ch >= '0') and (ch <= '9')) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
618 if i > MAXSTRING then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
619 newline(); print_string("Panic: "); print_string("identifier too long"); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
620 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
621 toksval[i] := ch; ch := GetChar(); i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
622 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
623 PushBack(ch);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
624 toksval[i] := ENDSTR; tokval := Lookup(toksval);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
625 if tokval = notsym then token := NEGATE end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
626 elsif ((ch >= '0') and (ch <= '9')) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
627 token := NUMBER; tokival := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
628 while ((ch >= '0') and (ch <= '9')) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
629 tokival := 10 * tokival + (ord(ch) - ord('0'));
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
630 ch := GetChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
631 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
632 PushBack(ch)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
633 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
634 case ch of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
635 '(': token := LPAR
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
636 | ')': token := RPAR
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
637 | ',': token := COMMA
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
638 | '.': token := DOT
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
639 | '=': token := EQUAL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
640 | '<': token := LANGLE
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
641 | '>': token := RANGLE
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
642 | '#': token := HASH
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
643 | '!': token := IDENT; tokval := cutsym
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
644 | '/':
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
645 ch := GetChar();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
646 if ch <> '*' then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
647 if not errflag then ShowError(); print_string("bad token /"); newline(); Recover() end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
648 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
649 ch2 := ' '; ch := GetChar();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
650 while (ch <> ENDFILE) and not ((ch2 = '*') and (ch = '/')) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
651 ch2 := ch; ch := GetChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
652 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
653 if ch = ENDFILE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
654 if not errflag then ShowError(); print_string("end of file in comment"); newline(); Recover() end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
655 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
656 ch := GetChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
657 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
658 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
659 | ':':
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
660 ch := GetChar();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
661 if ch = '-' then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
662 token := ARROW
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
663 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
664 PushBack(ch); token := COLON
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
665 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
666 | '''':
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
667 token := CHCON; tokival := ord(GetChar()); ch := GetChar();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
668 if ch <> '''' then if not errflag then ShowError(); print_string("missing quote"); newline(); Recover() end end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
669 | '"':
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
670 token := STRCON; i := 0; ch := GetChar();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
671 while (ch <> '"') and (ch <> ENDLINE) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
672 toksval[i] := ch; ch := GetChar(); i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
673 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
674 toksval[i] := ENDSTR;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
675 if ch = ENDLINE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
676 if not errflag then ShowError(); print_string("unterminated string"); newline(); Recover() end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
677 PushBack(ch)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
678 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
679 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
680 if not errflag then ShowError(); print_string("illegal character"); newline(); Recover() end; print_char(ch); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
681 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
682 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
683 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
684 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
685
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
686 (* |PrintToken| -- print a token as a string *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
687 proc PrintToken(t: integer);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
688 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
689 case t of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
690 IDENT:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
691 print_string("identifier "); WriteString(symtab[tokval].name)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
692 | VARIABLE:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
693 print_string("variable "); WriteString(symtab[tokval].name)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
694 | NUMBER: print_string("number");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
695 | CHCON: print_string("char constant");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
696 | ARROW: print_string(":-");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
697 | LPAR: print_string("(");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
698 | RPAR: print_string(")");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
699 | COMMA: print_string(",");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
700 | DOT: print_string(".");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
701 | COLON: print_string(":");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
702 | EQUAL: print_string("=");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
703 | STRCON: print_string("string constant")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
704 | LANGLE: print_string("<")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
705 | RANGLE: print_string(">")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
706 | HASH: print_string("#")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
707 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
708 print_string("unknown token")
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
709 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
710 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
711
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
712 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
713 nvars: integer; (* no. of variables so far *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
714 vartable: array MAXARITY+1 of symbol; (* names of the variables *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
715
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
716 (* |VarRep| -- look up a variable name *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
717 proc VarRep(name: symbol): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
718 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
719 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
720 if nvars = MAXARITY then newline(); print_string("Panic: "); print_string("too many variables"); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
721 i := 1; vartable[nvars+1] := name; (* sentinel *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
722 while name <> vartable[i] do i := i+1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
723 if i = nvars+1 then nvars := nvars+1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
724 return MakeRef(i)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
725 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
726
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
727 (* |ShowAnswer| -- display answer and get response *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
728 proc ShowAnswer(bindings: frame);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
729 var i: integer; ch, ch2: char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
730 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
731 if nvars = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
732 print_string("yes"); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
733 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
734 for i := 1 to nvars do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
735 WriteString(symtab[vartable[i]].name); print_string(" = ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
736 PrintTerm((bindings+7+(i-1)*TERM_SIZE), NULL, EQPRIO-1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
737 newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
738 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
739 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
740 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
741
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
742 (* |Eat| -- check for an expected token and discard it *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
743 proc Eat(expected: integer);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
744 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
745 if token = expected then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
746 if token <> DOT then Scan() end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
747 elsif not errflag then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
748 ShowError();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
749 print_string("expected "); PrintToken(expected);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
750 print_string(", found "); PrintToken(token); newline();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
751 Recover()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
752 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
753 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
754
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
755 (* |ParseCompound| -- parse a compound term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
756 proc ParseCompound(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
757 var fun: symbol; arg: argbuf; n: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
758 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
759 fun := tokval; n := 0; Eat(IDENT);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
760 if token = LPAR then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
761 Eat(LPAR); n := 1; arg[1] := ParseTerm();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
762 while token = COMMA do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
763 Eat(COMMA); n := n+1; arg[n] := ParseTerm()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
764 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
765 Eat(RPAR)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
766 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
767 if symtab[fun].arity = -1 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
768 symtab[fun].arity := n
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
769 elsif symtab[fun].arity <> n then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
770 if not errflag then ShowError(); print_string("wrong number of args"); newline(); Recover() end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
771 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
772 return MakeCompound(fun, arg)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
773 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
774
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
775 (* |ParsePrimary| -- parse a primary *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
776 proc ParsePrimary(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
777 var t: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
778 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
779 if token = IDENT then t := ParseCompound()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
780 elsif token = VARIABLE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
781 t := VarRep(tokval); Eat(VARIABLE)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
782 elsif token = NUMBER then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
783 t := MakeInt(tokival); Eat(NUMBER)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
784 elsif token = CHCON then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
785 t := MakeChar(chr(tokival)); Eat(CHCON)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
786 elsif token = STRCON then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
787 t := MakeString(toksval); Eat(STRCON)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
788 elsif token = LPAR then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
789 Eat(LPAR); t := ParseTerm(); Eat(RPAR)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
790 elsif token = LANGLE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
791 t := ParseNode()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
792 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
793 if not errflag then ShowError(); print_string("expected a term"); newline(); Recover() end; t := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
794 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
795 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
796 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
797
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
798 (* |ParseNode| -- parse an optree node *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
799 proc ParseNode(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
800 var tag, kids: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
801 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
802 Eat(LANGLE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
803 tag := ParseTerm();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
804 kids := ParseKids();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
805 Eat(RANGLE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
806 return MakeNode(node, tag, kids)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
807 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
808
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
809 (* |ParseKids| -- parse children of an optree node *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
810 proc ParseKids(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
811 var head, tail: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
812 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
813 if token <> COMMA then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
814 return MakeNode(nilsym, NULL, NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
815 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
816 Eat(COMMA);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
817 head := ParseTerm();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
818 tail := ParseKids();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
819 return MakeNode(cons, head, tail)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
820 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
821 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
822
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
823 (* |ParseFactor| -- parse a factor *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
824 proc ParseFactor(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
825 var t: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
826 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
827 t := ParsePrimary();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
828 if token <> COLON then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
829 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
830 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
831 Eat(COLON);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
832 return MakeNode(cons, t, ParseFactor())
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
833 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
834 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
835
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
836 (* |ParseTerm| -- parse a term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
837 proc ParseTerm(): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
838 var t: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
839 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
840 t := ParseFactor();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
841 if token <> EQUAL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
842 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
843 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
844 Eat(EQUAL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
845 return MakeNode(eqsym, t, ParseFactor())
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
846 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
847 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
848
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
849 (* |CheckAtom| -- check that a literal is a compound term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
850 proc CheckAtom(a: term);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
851 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
852 if lsr(mem[a], 8) <> FUNC then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
853 if not errflag then ShowError(); print_string("literal must be a compound term"); newline(); Recover() end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
854 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
855 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
856
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
857 (* |ParseClause| -- parse a clause *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
858 proc ParseClause(): clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
859 var head, t: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
860 body: argbuf;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
861 n: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
862 minus, more: boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
863 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
864 if token = HASH then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
865 Eat(HASH); head := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
866 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
867 head := ParseTerm();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
868 CheckAtom(head)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
869 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
870 Eat(ARROW);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
871 n := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
872 if token <> DOT then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
873 more := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
874 while more do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
875 n := n+1; minus := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
876 if token = NEGATE then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
877 Eat(NEGATE); minus := true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
878 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
879 t := ParseTerm(); CheckAtom(t);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
880 if minus then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
881 body[n] := MakeNode(notsym, t, NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
882 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
883 body[n] := t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
884 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
885 if token = COMMA then Eat(COMMA) else more := false end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
886 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
887 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
888 Eat(DOT);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
889
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
890 if errflag then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
891 return NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
892 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
893 return MakeClause(nvars, head, body, n)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
894 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
895 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
896
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
897 (* |ReadClause| -- read a clause from |infile| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
898 proc ReadClause(): clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
899 var c: clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
900 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
901 repeat
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
902 hp := hmark; nvars := 0; errflag := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
903 Scan();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
904 if token = EOFTOK then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
905 c := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
906 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
907 c := ParseClause()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
908 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
909 until (not errflag) or (token = EOFTOK);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
910 return c
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
911 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
912
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
913 type trail = ptr;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
914
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
915 const TRAIL_SIZE = 3;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
916
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
917 var trhead: trail; (* start of the trail *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
918
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
919 (* |Save| -- add a variable to the trail if it is critical *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
920 proc Save(v: term);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
921 var p: trail;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
922 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
923 if ((v < choice) or (v >= mem[choice+4])) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
924 p := GloAlloc(UNDO, TRAIL_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
925 mem[p+1] := v; mem[p+2] := trhead; trhead := p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
926 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
927 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
928
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
929 (* |Restore| -- undo bindings back to previous state *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
930 proc Restore();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
931 var v: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
932 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
933 while (trhead <> mem[choice+5]) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
934 v := mem[trhead+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
935 if v <> NULL then mem[v+1] := NULL end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
936 trhead := mem[trhead+2]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
937 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
938 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
939
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
940 (* |Commit| -- blank out trail entries not needed after cut *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
941 proc Commit();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
942 var p: trail;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
943 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
944 p := trhead;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
945 while (p <> NULL) and (p < mem[choice+4]) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
946 if (mem[p+1] <> NULL) and not ((mem[p+1] < choice) or (mem[p+1] >= mem[choice+4])) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
947 mem[p+1] := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
948 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
949 p := mem[p+2]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
950 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
951 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
952
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
953 (* |GloCopy| -- copy a term onto the global stack *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
954 proc GloCopy(t: term; e: frame): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
955 var tt: term; i, n: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
956 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
957 t := Deref(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
958 if (t >= gsp) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
959 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
960 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
961 case lsr(mem[t], 8) of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
962 FUNC:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
963 n := symtab[mem[t+1]].arity;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
964 if (t <= hp) and (n = 0) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
965 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
966 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
967 tt := GloAlloc(FUNC, TERM_SIZE+n);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
968 mem[tt+1] := mem[t+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
969 for i := 1 to n do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
970 mem[tt+i+1] := GloCopy(mem[t+i+1], e)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
971 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
972 return tt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
973 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
974 | CELL:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
975 tt := GloAlloc(CELL, TERM_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
976 mem[tt+1] := NULL;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
977 Save(t); mem[t+1] := tt;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
978 return tt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
979 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
980 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
981 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
982 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
983 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
984
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
985 (* |Share| -- bind two variables together *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
986 proc Share(v1, v2: term);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
987 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
988 if (v1 * (2 * ord((v1 >= gsp)) - 1)) <= (v2 * (2 * ord((v2 >= gsp)) - 1)) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
989 Save(v1); mem[v1+1] := v2
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
990 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
991 Save(v2); mem[v2+1] := v1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
992 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
993 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
994
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
995 (* |Unify| -- find and apply unifier for two terms *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
996 proc Unify(t1: term; e1: frame; t2: term; e2: frame): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
997 var i: integer; match: boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
998 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
999 t1 := Deref(t1, e1); t2 := Deref(t2, e2);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1000 if t1 = t2 then (* Includes unifying a var with itself *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1001 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1002 elsif (lsr(mem[t1], 8) = CELL) and (lsr(mem[t2], 8) = CELL) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1003 Share(t1, t2); return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1004 elsif lsr(mem[t1], 8) = CELL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1005 Save(t1); mem[t1+1] := GloCopy(t2, e2); return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1006 elsif lsr(mem[t2], 8) = CELL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1007 Save(t2); mem[t2+1] := GloCopy(t1, e1); return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1008 elsif lsr(mem[t1], 8) <> lsr(mem[t2], 8) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1009 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1010 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1011 case lsr(mem[t1], 8) of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1012 FUNC:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1013 if (mem[t1+1] <> mem[t2+1]) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1014 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1015 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1016 i := 1; match := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1017 while match and (i <= symtab[mem[t1+1]].arity) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1018 match := Unify(mem[t1+i+1], e1, mem[t2+i+1], e2);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1019 i := i+1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1020 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1021 return match
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1022 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1023 | INT:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1024 return (mem[t1+1] = mem[t2+1])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1025 | CHRCTR:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1026 return (mem[t1+1] = mem[t2+1])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1027 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1028 newline(); print_string("Panic: "); print_string("bad tag" (*t_kind(t1):1, " in ", "Unify"*)); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1029 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1030 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1031 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1032
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1033 (* |Key| -- unification key of a term *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1034 proc Key(t: term; e: frame): integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1035 var t0: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1036 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1037 (* The argument |t| must be a direct pointer to a compound term.
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1038 The value returned is |key(t)|: if |t1| and |t2| are unifiable,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1039 then |key(t1) = 0| or |key(t2) = 0| or |key(t1) = key(t2)|. *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1040
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1041 if t = NULL then newline(); print_string("Panic: "); print_string("Key"); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1042 if lsr(mem[t], 8) <> FUNC then newline(); print_string("Panic: "); print_string("bad tag" (*t_kind(t):1, " in ", "Key1"*)); newline(); exit(2) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1043
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1044 if symtab[mem[t+1]].arity = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1045 return 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1046 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1047 t0 := Deref(mem[t+1+1], e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1048 case lsr(mem[t0], 8) of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1049 FUNC: return mem[t0+1]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1050 | INT: return mem[t0+1] + 1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1051 | CHRCTR: return mem[t0+1] + 1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1052 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1053 return 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1054 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1055 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1056 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1057
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1058 (* |Search| -- find the first clause that might match *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1059 proc Search(t: term; e: frame; p: clause): clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1060 var k: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1061 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1062 k := Key(t, e);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1063 if k <> 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1064 while (p <> NULL) and (mem[p+1] <> 0) and (mem[p+1] <> k) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1065 p := mem[p+2]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1066 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1067 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1068 return p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1069 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1070
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1071 var ok: boolean; (* whether execution succeeded *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1072
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1073 (* |PushFrame| -- create a new local stack frame *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1074 proc PushFrame(nvars: integer; retry: clause);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1075 var f: frame; i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1076 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1077 f := LocAlloc((FRAME_SIZE + (nvars)*TERM_SIZE));
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1078 mem[f] := current; mem[f+1] := goalframe;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1079 mem[f+2] := retry; mem[f+3] := choice;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1080 mem[f+4] := gsp; mem[f+5] := trhead;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1081 mem[f+6] := nvars;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1082 for i := 1 to nvars do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1083 mem[(f+7+(i-1)*TERM_SIZE)] := lsl(CELL, 8) + TERM_SIZE;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1084 mem[(f+7+(i-1)*TERM_SIZE)+1] := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1085 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1086 goalframe := f;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1087 if retry <> NULL then choice := goalframe end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1088 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1089
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1090 (* |TroStep| -- perform a resolution step with tail-recursion *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1091 proc TroStep();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1092 var temp: frame; oldsize, newsize, i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1093 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1094 if dflag then print_string("(TRO)"); newline() end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1095
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1096 oldsize := (FRAME_SIZE + (mem[goalframe+6])*TERM_SIZE); (* size of old frame *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1097 newsize := (FRAME_SIZE + (mem[prok])*TERM_SIZE); (* size of new frame *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1098 temp := LocAlloc(newsize);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1099 temp := goalframe + newsize; (* copy old frame here *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1100
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1101 (* Copy the old frame: in reverse order in case of overlap *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1102 for i := 1 to oldsize do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1103 mem[temp+oldsize-i] := mem[goalframe+oldsize-i]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1104 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1105
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1106 (* Adjust internal pointers in the copy *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1107 for i := 1 to mem[goalframe+6] do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1108 if (lsr(mem[(temp+7+(i-1)*TERM_SIZE)], 8) = CELL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1109 and (mem[(temp+7+(i-1)*TERM_SIZE)+1] <> NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1110 and (goalframe <= mem[(temp+7+(i-1)*TERM_SIZE)+1])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1111 and (mem[(temp+7+(i-1)*TERM_SIZE)+1] < goalframe + oldsize) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1112 mem[(temp+7+(i-1)*TERM_SIZE)+1] := mem[(temp+7+(i-1)*TERM_SIZE)+1] + newsize
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1113 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1114 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1115
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1116 (* Overwrite the old frame with the new one *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1117 mem[goalframe+6] := mem[prok];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1118 for i := 1 to mem[goalframe+6] do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1119 mem[(goalframe+7+(i-1)*TERM_SIZE)] := lsl(CELL, 8) + TERM_SIZE;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1120 mem[(goalframe+7+(i-1)*TERM_SIZE)+1] := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1121 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1122
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1123 (* Perform the resolution step *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1124 ok := Unify(call, temp, mem[prok+3], goalframe);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1125 current := (prok+4);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1126 lsp := temp-1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1127 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1128
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1129 (* |Step| -- perform a resolution step *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1130 proc Step();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1131 var retry: clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1132 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1133 if symtab[mem[call+1]].action <> 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1134 ok := DoBuiltin(symtab[mem[call+1]].action)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1135 elsif prok = NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1136 ok := false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1137 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1138 retry := Search(call, goalframe, mem[prok+2]);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1139 if (mem[(current)+1] = NULL) and (choice < goalframe)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1140 and (retry = NULL) and (goalframe <> base) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1141 TroStep()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1142 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1143 PushFrame(mem[prok], retry);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1144 ok := Unify(call, mem[goalframe+1], mem[prok+3], goalframe);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1145 current := (prok+4);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1146 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1147 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1148 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1149
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1150 (* |Unwind| -- return from completed clauses *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1151 proc Unwind();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1152 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1153 while (mem[current] = NULL) and (goalframe <> base) do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1154 if dflag then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1155 print_string("Exit"); print_string(": ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1156 PrintTerm(mem[mem[goalframe]], mem[goalframe+1], MAXPRIO); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1157 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1158 current := (mem[goalframe])+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1159 if goalframe > choice then lsp := goalframe-1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1160 goalframe := mem[goalframe+1]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1161 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1162 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1163
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1164 (* |Backtrack| -- roll back to the last choice-point *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1165 proc Backtrack();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1166 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1167 Restore();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1168 current := mem[choice]; goalframe := mem[choice+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1169 call := Deref(mem[current], goalframe);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1170 prok := mem[choice+2]; gsp := mem[choice+4];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1171 lsp := choice-1; choice := mem[choice+3];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1172 if dflag then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1173 print_string("Redo"); print_string(": ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1174 PrintTerm(call, goalframe, MAXPRIO); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1175 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1176 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1177
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1178 (* |Resume| -- continue execution *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1179 proc Resume();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1180 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1181 while run do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1182 if ok then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1183 if mem[current] = NULL then return end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1184 call := Deref(mem[current], goalframe);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1185 if dflag then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1186 print_string("Call"); print_string(": ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1187 PrintTerm(call, goalframe, MAXPRIO); newline()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1188 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1189 if (symtab[mem[call+1]].prok = NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1190 and (symtab[mem[call+1]].action = 0) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1191 newline(); print_string("Error: "); print_string("call to undefined relation "); run := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1192 WriteString(symtab[mem[call+1]].name);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1193 return
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1194 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1195 prok := Search(call, goalframe, symtab[mem[call+1]].prok)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1196 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1197 if choice <= base then return end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1198 Backtrack()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1199 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1200 Step();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1201 if ok then Unwind() end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1202 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1203 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1204
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1205 (* |Execute| -- solve a goal by SLD-resolution *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1206 proc Execute(g: clause);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1207 var nsoln: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1208 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1209 lsp := hp; gsp := MEMSIZE+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1210 current := NULL; goalframe := NULL; choice := NULL; trhead := NULL;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1211 PushFrame(mem[g], NULL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1212 choice := goalframe; base := goalframe; current := (g+4);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1213 run := true; ok := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1214 Resume();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1215 if not run then return end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1216 while ok do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1217 nsoln := nsoln+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1218 ShowAnswer(base);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1219 newline();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1220 ok := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1221 Resume();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1222 if not run then return end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1223 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1224
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1225 if nsoln = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1226 print_string("no"); newline(); newline();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1227 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1228 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1229
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1230 var
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1231 av: argbuf; (* |GetArgs| puts arguments here *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1232 callbody: ptr; (* dummy clause body used by |call/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1233
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1234 (* |GetArgs| -- set up |av| array *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1235 proc GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1236 var i: integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1237 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1238 for i := 1 to symtab[mem[call+1]].arity do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1239 av[i] := Deref(mem[call+i+1], goalframe)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1240 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1241 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1242
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1243 proc NewInt(n: integer): term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1244 var t: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1245 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1246 t := GloAlloc(INT, TERM_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1247 mem[t+1] := n;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1248 return t
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1249 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1250
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1251 (* |DoCut| -- built-in relation !/0 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1252 proc DoCut(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1253 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1254 choice := mem[goalframe+3];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1255 lsp := goalframe + (FRAME_SIZE + (mem[goalframe+6])*TERM_SIZE) - 1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1256 Commit();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1257 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1258 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1259 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1260
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1261 (* |DoCall| -- built-in relation |call/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1262 proc DoCall(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1263 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1264 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1265 if not (lsr(mem[av[1]], 8) = FUNC) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1266 newline(); print_string("Error: "); print_string("bad argument to call/1"); run := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1267 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1268 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1269 PushFrame(1, NULL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1270 mem[(goalframe+7+(1-1)*TERM_SIZE)+1] :=
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1271 GloCopy(av[1], mem[goalframe+1]);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1272 current := callbody;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1273 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1274 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1275 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1276
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1277 (* |DoNot| -- built-in relation |not/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1278 proc DoNot(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1279 var savebase: frame;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1280 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1281 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1282 if not (lsr(mem[av[1]], 8) = FUNC) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1283 newline(); print_string("Error: "); print_string("bad argument to call/1"); run := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1284 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1285 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1286 PushFrame(1, NULL);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1287 savebase := base; base := goalframe; choice := goalframe;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1288 mem[(goalframe+7+(1-1)*TERM_SIZE)+1] :=
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1289 GloCopy(av[1], mem[goalframe+1]);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1290 current := callbody; ok := true;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1291 Resume();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1292 choice := mem[base+3]; goalframe := mem[base+1];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1293 if not ok then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1294 current := (mem[base])+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1295 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1296 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1297 Commit();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1298 return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1299 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1300 lsp := base-1; base := savebase
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1301 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1302 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1303
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1304 (* |DoPlus| -- built-in relation |plus/3| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1305 proc DoPlus(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1306 var result: boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1307 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1308 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1309 result := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1310 if (lsr(mem[av[1]], 8) = INT) and (lsr(mem[av[2]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1311 result := Unify(av[3], goalframe, NewInt(mem[av[1]+1] + mem[av[2]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1312 elsif (lsr(mem[av[1]], 8) = INT) and (lsr(mem[av[3]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1313 if mem[av[1]+1] <= mem[av[3]+1] then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1314 result := Unify(av[2], goalframe,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1315 NewInt(mem[av[3]+1] - mem[av[1]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1316 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1317 elsif (lsr(mem[av[2]], 8) = INT) and (lsr(mem[av[3]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1318 if mem[av[2]+1] <= mem[av[3]+1] then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1319 result := Unify(av[1], goalframe, NewInt(mem[av[3]+1] - mem[av[2]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1320 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1321 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1322 newline(); print_string("Error: "); print_string("plus/3 needs at least two integers"); run := false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1323 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1324 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1325 return result
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1326 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1327
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1328 (* |DoTimes| -- built-in relation |times/3| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1329 proc DoTimes(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1330 var result: boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1331 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1332 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1333 result := false;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1334 if (lsr(mem[av[1]], 8) = INT) and (lsr(mem[av[2]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1335 result := Unify(av[3], goalframe,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1336 NewInt(mem[av[1]+1] * mem[av[2]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1337 elsif (lsr(mem[av[1]], 8) = INT) and (lsr(mem[av[3]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1338 if mem[av[1]+1] <> 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1339 if mem[av[3]+1] mod mem[av[1]+1] = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1340 result := Unify(av[2], goalframe,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1341 NewInt(mem[av[3]+1] div mem[av[1]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1342 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1343 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1344 elsif (lsr(mem[av[2]], 8) = INT) and (lsr(mem[av[3]], 8) = INT) then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1345 if mem[av[2]+1] <> 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1346 if mem[av[3]+1] mod mem[av[2]+1] = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1347 result := Unify(av[1], goalframe,
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1348 NewInt(mem[av[3]+1] div mem[av[2]+1]), NULL)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1349 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1350 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1351 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1352 newline(); print_string("Error: "); print_string("times/3 needs at least two integers"); run := false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1353 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1354 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1355 return result
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1356 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1357
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1358 (* |DoEqual| -- built-in relation |=/2| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1359 proc DoEqual(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1360 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1361 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1362 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1363 return Unify(av[1], goalframe, av[2], goalframe)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1364 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1365
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1366 (* |DoInteger| -- built-in relation |integer/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1367 proc DoInteger(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1368 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1369 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1370 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1371 return (lsr(mem[av[1]], 8) = INT)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1372 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1373
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1374 (* |DoChar| -- built-in relation |char/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1375 proc DoChar(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1376 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1377 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1378 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1379 return (lsr(mem[av[1]], 8) = CHRCTR)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1380 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1381
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1382 (* |DoPrint| -- built-in relation |print/1| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1383 proc DoPrint(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1384 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1385 GetArgs();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1386 PrintTerm(av[1], goalframe, MAXPRIO);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1387 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1388 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1389 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1390
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1391 (* |DoNl| -- built-in relation |nl/0| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1392 proc DoNl(): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1393 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1394 newline();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1395 current := (current)+1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1396 return true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1397 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1398
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1399 (* |DoBuiltin| -- switch for built-in relations *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1400 proc DoBuiltin(action: integer): boolean;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1401 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1402 case action of
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1403 CUT: return DoCut()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1404 | CALL: return DoCall()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1405 | PLUS: return DoPlus()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1406 | TIMES: return DoTimes()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1407 | ISINT: return DoInteger()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1408 | ISCHAR: return DoChar()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1409 | NAFF: return DoNot()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1410 | EQUALITY: return DoEqual()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1411 | FAIL: return false
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1412 | PRINT: return DoPrint()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1413 | NL: return DoNl()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1414 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1415 newline(); print_string("Panic: "); print_string("bad tag" (*action:1, " in ", "DoBuiltin"*)); newline(); exit(2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1416 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1417 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1418
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1419 (* |Initialize| -- initialize everything *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1420 proc Initialize();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1421 var i: integer; p: term;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1422 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1423 dflag := false; errcount := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1424 pbchar := ENDFILE; charptr := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1425 hp := 0; InitSymbols();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1426
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1427 (* Set up the |refnode| array *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1428 for i := 1 to MAXARITY do
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1429 p := HeapAlloc(TERM_SIZE);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1430 mem[p] := lsl(REF, 8) + TERM_SIZE;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1431 mem[p+1] := i; refnode[i] := p
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1432 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1433
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1434 (* The dummy clause $\it call(\sci p) \IF p$ is used by |call/1|. *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1435 callbody := HeapAlloc(2);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1436 mem[callbody] := MakeRef(1);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1437 mem[(callbody)+1] := NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1438 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1439
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1440 (* |ReadFile| -- read and process clauses from an open file *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1441 proc ReadFile();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1442 var c: clause;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1443 ch: char;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1444 begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1445 lineno := 1;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1446 repeat
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1447 hmark := hp;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1448 c := ReadClause();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1449 if c <> NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1450 if dflag then PrintClause(c) end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1451 if mem[c+3] <> NULL then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1452 AddClause(c)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1453 else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1454 Execute(c);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1455 hp := hmark
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1456 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1457 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1458 until c = NULL
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1459 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1460
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1461 begin (* main program *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1462 prog("subject( ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1463 prog(" <store, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1464 prog(" <load, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1465 prog(" <plusa, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1466 prog(" <global(a)>, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1467 prog(" <lsl, <load, <local(16)>>, <const(2)>>>>, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1468 prog(" <local(20)>> ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1469 prog(") :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1470
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1471 prog("rule(""*str"", stmt, <store, reg, addr>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1472 prog("rule(""*ldr"", reg, <load, addr>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1473 prog("rule(""*addfp"", reg, <local(N)>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1474 prog("rule(""local"", addr, <local(N)>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1475 prog("rule(""*add"", reg, <plusa, reg, rand>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1476 prog("rule(""index"", addr, <plusa, reg, reg>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1477 prog("rule(""scale"", addr, ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1478 prog(" <plusa, reg, <lsl, reg, <const(N)>>>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1479 prog("rule(""*global"", reg, <global(X)>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1480 prog("rule(""*lsl"", reg, <lsl, reg, rand>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1481 prog("rule(""lshiftc"", rand, <lsl, reg, <const(N)>>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1482 prog("rule(""lshiftr"", rand, <lsl, reg, reg>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1483 prog("rule(""*mov"", reg, <const(N)>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1484 prog("rule(""const"", rand, <const(N)>) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1485 prog("rule(""reg"", rand, reg) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1486 prog("rule(""indir"", addr, reg) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1487
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1488 prog("use_rule(NT, Tree, node(Name, Kids)) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1489 prog(" rule(Name, NT, RHS), match(RHS, Tree, Kids, nil). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1490
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1491 prog("match(NT, Tree, Parse:Kids0, Kids0) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1492 prog(" use_rule(NT, Tree, Parse). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1493
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1494 prog("match(node(W, PS), node(W, TS), Kids, Kids0) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1495 prog(" matchall(PS, TS, Kids, Kids0). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1496
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1497 prog("matchall(nil, nil, Kids0, Kids0) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1498 prog("matchall(P:PS, T:TS, Kids, Kids0) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1499 prog(" match(P, T, Kids, Kids1), matchall(PS, TS, Kids1, Kids0). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1500
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1501 prog("cost(node(X, TS), C) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1502 prog(" opcost(X, A), allcosts(TS, B), plus(A, B, C). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1503
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1504 prog("allcosts(nil, 0) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1505 prog("allcosts(T:TS, C) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1506 prog(" cost(T, A), allcosts(TS, B), plus(A, B, C). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1507
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1508 prog("opcost('*':_, 1) :- !. ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1509 prog("opcost(_, 0) :- . ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1510
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1511 prog("answer(P, C) :- ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1512 prog(" subject(T), use_rule(stmt, T, P), cost(P, C). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1513
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1514 prog("min(N, P) :- min1(N, 0, P). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1515 prog("min1(N, N, P) :- call(P), !. ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1516 prog("min1(N, N0, P) :- plus(N0, 1, N1), min1(N, N1, P). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1517
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1518 prog("# :- answer(P, C). ");
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1519
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1520 Initialize();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1521 ReadFile()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1522 end.
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1523
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1524 (*<<
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1525 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"local">>, <"const">>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1526 C = 5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1527
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1528 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"local">>, <"const">>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1529 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1530
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1531 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"local">>, <"reg", <"*mov">>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1532 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1533
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1534 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"local">>, <"reg", <"*mov">>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1535 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1536
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1537 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"const">>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1538 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1539
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1540 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"const">>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1541 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1542
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1543 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"reg", <"*mov">>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1544 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1545
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1546 P = <"*str", <"*ldr", <"index", <"*global">, <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"reg", <"*mov">>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1547 C = 8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1548
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1549 P = <"*str", <"*ldr", <"scale", <"*global">, <"*ldr", <"local">>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1550 C = 4
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1551
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1552 P = <"*str", <"*ldr", <"scale", <"*global">, <"*ldr", <"local">>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1553 C = 5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1554
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1555 P = <"*str", <"*ldr", <"scale", <"*global">, <"*ldr", <"indir", <"*addfp">>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1556 C = 5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1557
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1558 P = <"*str", <"*ldr", <"scale", <"*global">, <"*ldr", <"indir", <"*addfp">>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1559 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1560
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1561 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftc", <"*ldr", <"local">>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1562 C = 5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1563
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1564 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftc", <"*ldr", <"local">>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1565 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1566
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1567 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftc", <"*ldr", <"indir", <"*addfp">>>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1568 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1569
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1570 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftc", <"*ldr", <"indir", <"*addfp">>>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1571 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1572
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1573 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftr", <"*ldr", <"local">>, <"*mov">>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1574 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1575
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1576 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftr", <"*ldr", <"local">>, <"*mov">>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1577 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1578
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1579 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftr", <"*ldr", <"indir", <"*addfp">>>, <"*mov">>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1580 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1581
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1582 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"lshiftr", <"*ldr", <"indir", <"*addfp">>>, <"*mov">>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1583 C = 8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1584
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1585 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"local">>, <"const">>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1586 C = 6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1587
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1588 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"local">>, <"const">>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1589 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1590
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1591 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"local">>, <"reg", <"*mov">>>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1592 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1593
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1594 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"local">>, <"reg", <"*mov">>>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1595 C = 8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1596
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1597 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"const">>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1598 C = 7
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1599
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1600 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"const">>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1601 C = 8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1602
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1603 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"reg", <"*mov">>>>>>>, <"local">>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1604 C = 8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1605
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1606 P = <"*str", <"*ldr", <"indir", <"*add", <"*global">, <"reg", <"*lsl", <"*ldr", <"indir", <"*addfp">>>, <"reg", <"*mov">>>>>>>, <"indir", <"*addfp">>>
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1607 C = 9
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1608
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1609 >>*)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1610
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1611 (*[[
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1612 @ picoPascal compiler output
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1613 .include "fixup.s"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1614 .global pmain
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1615
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1616 @ proc StringLength(var s: tempstring): integer;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1617 .text
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1618 _StringLength:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1619 mov ip, sp
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1620 stmfd sp!, {r0-r1}
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1621 stmfd sp!, {r4-r10, fp, ip, lr}
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1622 mov fp, sp
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1623 @ i := 0;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1624 mov r4, #0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1625 .L147:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1626 @ while s[i] <> ENDSTR do i := i+1 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1627 ldr r0, [fp, #40]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1628 add r0, r0, r4
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1629 ldrb r0, [r0]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1630 cmp r0, #0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1631 beq .L149
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1632 add r4, r4, #1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1633 b .L147
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1634 .L149:
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1635 @ return i
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1636 mov r0, r4
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1637 ldmfd fp, {r4-r10, fp, sp, pc}
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1638 .ltorg