Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | (*kitknuth_bendix36c.sml*) |
2 | ||
3 | (* | |
4 | ||
5 | kitknuth-bendixnewcopy.sml | |
6 | ||
7 | This is a revised version of knuth-bendix.sml in which | |
8 | (a) val has been converted to fun for function values | |
9 | (b) exceptions that carry values have been avoided | |
10 | (c) functions have been moved around to pass fewer of them | |
11 | as parameters | |
12 | (d) long tail-recursions have been broken into batches of 1, | |
13 | with user-programmed copying between the batches | |
14 | ||
15 | *) | |
16 | local | |
17 | ||
18 | fun eq_integer (x: int, y: int): bool = x = y | |
19 | fun eq_string (x: string, y: string): bool = x = y | |
20 | ||
21 | (* | |
22 | signature KB = | |
23 | sig | |
24 | datatype term = Var of int | Term of string * term list | |
25 | datatype ordering = Greater | Equal | NotGE | |
26 | val rpo: (string -> string -> ordering) -> | |
27 | ((term * term -> ordering) -> term * term -> ordering) -> | |
28 | term * term -> ordering | |
29 | val lex_ext: (term * term -> ordering) -> term * term -> ordering | |
30 | val kb_complete: | |
31 | (term * term -> bool) -> (int * (int * (term * term))) list -> | |
32 | ('a * ('b * (term * term))) list -> unit | |
33 | include BMARK | |
34 | end; | |
35 | *) | |
36 | (* | |
37 | structure Main : KB = | |
38 | struct | |
39 | *) | |
40 | fun length l = let | |
41 | fun j(k, nil) = k | |
42 | | j(k, a::x) = j(k+1,x) | |
43 | in | |
44 | j(0,l) | |
45 | end | |
46 | fun op @ (nil, l) = l | |
47 | | op @ (a::r, l) = a :: (r@l) | |
48 | fun rev l = let | |
49 | fun f (nil, h) = h | |
50 | | f (a::r, h) = f(r, a::h) | |
51 | in | |
52 | f(l,nil) | |
53 | end | |
54 | fun app f = let | |
55 | fun app_rec [] = () | |
56 | | app_rec (a::L) = (f a; app_rec L) | |
57 | in | |
58 | app_rec | |
59 | end | |
60 | (* | |
61 | fun map f = let | |
62 | fun map_rec [] = [] | |
63 | | map_rec (a::L) = f a :: map_rec L | |
64 | in | |
65 | map_rec | |
66 | end | |
67 | *) | |
68 | ||
69 | (******* Quelques definitions du prelude CAML **************) | |
70 | ||
71 | exception Failure of string | |
72 | exception FailItList2 | |
73 | exception FailTryFind | |
74 | exception FailFind | |
75 | exception FailChange | |
76 | exception FailReplace | |
77 | exception FailMatching | |
78 | exception FailUnify | |
79 | exception FailPretty | |
80 | exception Fail | |
81 | exception FailMrewrite1 | |
82 | exception FailRemEQ | |
83 | exception FailMultExt | |
84 | exception FailLexExt | |
85 | exception FailKbComplettion | |
86 | ||
87 | fun failwith s = raise(Failure s) | |
88 | ||
89 | fun fst (x,y) = x | |
90 | and snd (x,y) = y | |
91 | ||
92 | ||
93 | (* | |
94 | fun it_list f = | |
95 | let fun it_rec a [] = a | |
96 | | it_rec a (b::L) = it_rec (f a b) L | |
97 | in it_rec | |
98 | end | |
99 | *) | |
100 | fun it_list f a [] = a | |
101 | | it_list f a (b::L) = it_list f (f a b) L | |
102 | ||
103 | fun it_list2 f = | |
104 | let fun it_rec a [] [] = a | |
105 | | it_rec a (a1::L1) (a2::L2) = it_rec (f a (a1,a2)) L1 L2 | |
106 | | it_rec _ _ _ = raise FailItList2 | |
107 | in it_rec | |
108 | end | |
109 | ||
110 | fun exists p = | |
111 | let fun exists_rec [] = false | |
112 | | exists_rec (a::L) = (p a) orelse (exists_rec L) | |
113 | in exists_rec | |
114 | end | |
115 | ||
116 | fun for_all p = | |
117 | let fun for_all_rec [] = true | |
118 | | for_all_rec (a::L) = (p a) andalso (for_all_rec L) | |
119 | in for_all_rec | |
120 | end | |
121 | ||
122 | fun rev_append [] L = L | |
123 | | rev_append (x::L1) L2 = rev_append L1 (x::L2) | |
124 | ||
125 | fun try_find f = | |
126 | let fun try_find_rec [] = raise FailTryFind | |
127 | | try_find_rec (a::L) = (f a) handle _ => try_find_rec L | |
128 | in try_find_rec | |
129 | end | |
130 | ||
131 | fun partition p = | |
132 | let fun part_rec [] = ([],[]) | |
133 | | part_rec (a::L) = | |
134 | let val (pos,neg) = part_rec L in | |
135 | if p a then ((a::pos), neg) else (pos, (a::neg)) | |
136 | end | |
137 | in part_rec | |
138 | end | |
139 | ||
140 | (* 3- Les ensembles et les listes d'association *) | |
141 | ||
142 | (* | |
143 | fun mem eq a = | |
144 | let fun mem_rec [] = false | |
145 | | mem_rec (b::L) = (eq(a,b)) orelse mem_rec L | |
146 | in mem_rec | |
147 | end | |
148 | *) | |
149 | fun mem eq a []= false | |
150 | | mem eq a (b::L) = eq(a,b) orelse mem eq a L | |
151 | ||
152 | fun union eq L1 L2 = | |
153 | let fun union_rec [] = L2 | |
154 | | union_rec (a::L) = | |
155 | if mem eq a L2 then union_rec L else a :: union_rec L | |
156 | in union_rec L1 | |
157 | end | |
158 | ||
159 | (* | |
160 | fun mem_assoc eq a = | |
161 | let fun mem_rec [] = false | |
162 | | mem_rec ((b,_)::L) = (eq(a,b)) orelse mem_rec L | |
163 | in mem_rec | |
164 | end | |
165 | *) | |
166 | ||
167 | fun mem_assoc eq a [] = false | |
168 | | mem_assoc eq a ((b,_)::L) = eq(a,b) orelse mem_assoc eq a L | |
169 | ||
170 | fun assoc eq a = | |
171 | let fun assoc_rec [] = raise FailFind | |
172 | | assoc_rec ((b,d)::L) = if eq(a,b) then d else assoc_rec L | |
173 | in assoc_rec | |
174 | end | |
175 | ||
176 | (* 4- Les sorties *) | |
177 | ||
178 | (* val print_string = String.print; *) | |
179 | (* Lars *) | |
180 | fun print_string x = print x | |
181 | ||
182 | (* val print_num = Integer.print; *) | |
183 | (* Lars *) | |
184 | local | |
185 | fun digit n = chr(ord #"0" + n) | |
186 | fun digits(n,acc) = | |
187 | if n >=0 andalso n<=9 then digit n:: acc | |
188 | else digits (n div 10, digit(n mod 10) :: acc) | |
189 | fun string(n) = implode(digits(n,[])) | |
190 | in | |
191 | fun print_num n = print_string(string n) | |
192 | end | |
193 | ||
194 | (* fun print_newline () = String.print "\n"; *) | |
195 | (* Lars *) | |
196 | fun print_newline () = print "\n" | |
197 | ||
198 | (* fun message s = (String.print s; String.print "\n"); *) | |
199 | (* Lars *) | |
200 | fun message s = (print s; print "\n") | |
201 | ||
202 | (* 5- Les ensembles *) | |
203 | ||
204 | fun union eq L1 = | |
205 | let fun union_rec [] = L1 | |
206 | | union_rec (a::L) = if mem eq a L1 then union_rec L else a :: union_rec L | |
207 | in union_rec | |
208 | end | |
209 | ||
210 | (****************** Term manipulations *****************) | |
211 | ||
212 | ||
213 | datatype term | |
214 | = Var of int | |
215 | | Term of string * term list | |
216 | ||
217 | (* Lars, from now on: seek on eq_X to see what I have modified *) | |
218 | ||
219 | fun map' f ([]:term list) : term list = [] | |
220 | | map' f (term::terms) = f term :: map' f terms | |
221 | ||
222 | fun copy_term (Var n) = Var (n+0) | |
223 | | copy_term (Term(s, l)) = Term(s, map' copy_term l) | |
224 | ||
225 | fun eq_term x = | |
226 | (fn (Var i1, Var i2) => | |
227 | eq_integer(i1,i2) | |
228 | | (Term(s1,ts1),Term(s2,ts2)) => | |
229 | eq_string(s1,s2) andalso (eq_term_list(ts1,ts2)) | |
230 | | _ => false) x | |
231 | and eq_term_list x = | |
232 | (fn ([],[]) => true | |
233 | | (t1::ts1,t2::ts2) => eq_term(t1,t2) andalso eq_term_list(ts1,ts2) | |
234 | | _ => false) x | |
235 | ||
236 | fun vars (Var n) = [n] | |
237 | | vars (Term(_,L)) = vars_of_list L | |
238 | and vars_of_list [] = [] | |
239 | | vars_of_list (t::r) = union eq_integer (vars t) (vars_of_list r) | |
240 | ||
241 | (* | |
242 | fun substitute subst = | |
243 | let fun subst_rec (Term(oper,sons)) = Term(oper, map subst_rec sons) | |
244 | | subst_rec (t as (Var n)) = (assoc eq_integer n subst) handle _ => t | |
245 | in subst_rec | |
246 | end | |
247 | *) | |
248 | fun substitute subst (t as Term(oper,[])) = t | |
249 | | substitute subst (Term(oper,sons)) = Term(oper, map (substitute subst) sons) | |
250 | | substitute subst (t as (Var n)) = (assoc eq_integer n subst) handle _ => t | |
251 | ||
252 | fun change f = | |
253 | let fun change_rec (h::t) n = if eq_integer(n,1) then f h :: t | |
254 | else h :: change_rec t (n-1) | |
255 | | change_rec _ _ = raise FailChange | |
256 | in change_rec | |
257 | end | |
258 | ||
259 | (* Term replacement replace M u N => M[u<-N] *) | |
260 | fun replace M u N = | |
261 | let fun reprec (_, []) = N | |
262 | | reprec (Term(oper,sons), (n::u)) = | |
263 | Term(oper, change (fn P => reprec(P,u)) sons n) | |
264 | | reprec _ = raise FailReplace | |
265 | in reprec(M,u) | |
266 | end | |
267 | ||
268 | (* matching = - : (term -> term -> subst) *) | |
269 | fun matching term1 term2 = | |
270 | let fun match_rec subst (Var v, M) = | |
271 | if mem_assoc eq_integer v subst then | |
272 | if eq_term(M,assoc eq_integer v subst) then subst else raise FailMatching | |
273 | else | |
274 | (v,M) :: subst | |
275 | | match_rec subst (Term(op1,sons1), Term(op2,sons2)) = | |
276 | if eq_string(op1,op2) then it_list2 match_rec subst sons1 sons2 | |
277 | else raise FailMatching | |
278 | | match_rec _ _ = raise FailMatching | |
279 | in match_rec [] (term1,term2) | |
280 | end | |
281 | ||
282 | (* A naive unification algorithm *) | |
283 | ||
284 | fun compsubst subst1 subst2 = | |
285 | (map (fn (v,t) => (v, substitute subst1 t)) subst2) @ subst1 | |
286 | ||
287 | fun occurs n = | |
288 | let fun occur_rec (Var m) = eq_integer(m,n) | |
289 | | occur_rec (Term(_,sons)) = exists occur_rec sons | |
290 | in occur_rec | |
291 | end | |
292 | ||
293 | fun unify ((term1 as (Var n1)), term2) = | |
294 | if eq_term(term1,term2) then [] | |
295 | else if occurs n1 term2 then raise FailUnify | |
296 | else [(n1,term2)] | |
297 | | unify (term1, Var n2) = | |
298 | if occurs n2 term1 then raise FailUnify | |
299 | else [(n2,term1)] | |
300 | | unify (Term(op1,sons1), Term(op2,sons2)) = | |
301 | if eq_string(op1,op2) then | |
302 | it_list2 (fn s => fn (t1,t2) => compsubst (unify(substitute s t1, | |
303 | substitute s t2)) s) | |
304 | [] sons1 sons2 | |
305 | else raise FailUnify | |
306 | ||
307 | (* We need to print terms with variables independently from input terms | |
308 | obtained by parsing. We give arbitrary names v1,v2,... to their variables. *) | |
309 | ||
310 | val INFIXES = ["+","*"] | |
311 | ||
312 | fun pretty_term (Var n) = | |
313 | (print_string "v"; print_num n) | |
314 | | pretty_term (Term (oper,sons)) = | |
315 | if mem eq_string oper INFIXES then | |
316 | case sons of | |
317 | [s1,s2] => | |
318 | (pretty_close s1; print_string oper; pretty_close s2) | |
319 | | _ => | |
320 | raise FailPretty (* "pretty_term : infix arity <> 2"*) | |
321 | else | |
322 | (print_string oper; | |
323 | case sons of | |
324 | [] => () | |
325 | | t::lt =>(print_string "("; | |
326 | pretty_term t; | |
327 | app (fn t => (print_string ","; pretty_term t)) lt; | |
328 | print_string ")")) | |
329 | and pretty_close (M as Term(oper, _)) = | |
330 | if mem eq_string oper INFIXES then | |
331 | (print_string "("; pretty_term M; print_string ")") | |
332 | else pretty_term M | |
333 | | pretty_close M = pretty_term M | |
334 | ||
335 | (****************** Equation manipulations *************) | |
336 | ||
337 | (* standardizes an equation so its variables are 1,2,... *) | |
338 | ||
339 | fun mk_rule M N = | |
340 | let val all_vars = union eq_integer (vars M) (vars N) | |
341 | val (k,subst) = | |
342 | it_list (fn (i,sigma) => fn v => (i+1,(v,Var(i))::sigma)) | |
343 | (1,[]) all_vars | |
344 | in (k-1, (substitute subst M, substitute subst N)) | |
345 | end | |
346 | ||
347 | (* checks that rules are numbered in sequence and returns their number *) | |
348 | fun check_rules x = | |
349 | it_list (fn n => fn (k,_) => | |
350 | if eq_integer(k,n+1) then k | |
351 | else raise Fail (*failwith "Rule numbers not in sequence"*) | |
352 | ) 0 x | |
353 | ||
354 | fun pretty_rule (k,(n,(M,N))) = | |
355 | (print_num k; print_string " : "; | |
356 | pretty_term M; print_string " = "; pretty_term N; | |
357 | print_newline()) | |
358 | ||
359 | fun pretty_rules l = app pretty_rule l | |
360 | ||
361 | fun copy_rules [] = [] | |
362 | | copy_rules ((k,(n,(M,N)))::rest) = (k+0,(n+0,(copy_term M, copy_term N))):: copy_rules rest | |
363 | ||
364 | (****************** Rewriting **************************) | |
365 | ||
366 | (* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M. | |
367 | With sigma = matching L M, we define the image of M by eq as sigma(R) *) | |
368 | fun reduce L M = | |
369 | substitute (matching L M) | |
370 | ||
371 | (* A more efficient version of can (rewrite1 (L,R)) for R arbitrary *) | |
372 | fun reducible L = | |
373 | let fun redrec M = | |
374 | (matching L M; true) | |
375 | handle _ => | |
376 | case M of Term(_,sons) => exists redrec sons | |
377 | | _ => false | |
378 | in redrec | |
379 | end | |
380 | ||
381 | (* mreduce : rules -> term -> term *) | |
382 | fun mreduce rules M = | |
383 | let fun redex (_,(_,(L,R))) = reduce L M R in try_find redex rules end | |
384 | ||
385 | (* One step of rewriting in leftmost-outermost strategy, with multiple rules *) | |
386 | (* fails if no redex is found *) | |
387 | (* mrewrite1 : rules -> term -> term *) | |
388 | fun mrewrite1 rules = | |
389 | let fun rewrec M = | |
390 | (mreduce rules M) handle _ => | |
391 | let fun tryrec [] = raise FailMrewrite1 (*failwith "mrewrite1"*) | |
392 | | tryrec (son::rest) = | |
393 | (rewrec son :: rest) handle _ => son :: tryrec rest | |
394 | in case M of | |
395 | Term(f, sons) => Term(f, tryrec sons) | |
396 | | _ => raise FailMrewrite1 (*failwith "mrewrite1"*) | |
397 | end | |
398 | in rewrec | |
399 | end | |
400 | ||
401 | (* Iterating rewrite1. Returns a normal form. May loop forever *) | |
402 | (* mrewrite_all : rules -> term -> term *) | |
403 | fun mrewrite_all rules M = | |
404 | let fun rew_loop M = | |
405 | rew_loop(mrewrite1 rules M) handle _ => M | |
406 | in rew_loop M | |
407 | end | |
408 | ||
409 | (* | |
410 | pretty_term (mrewrite_all Group_rules M where M,_=<<A*(I(B)*B)>>);; | |
411 | ==> A*U | |
412 | *) | |
413 | ||
414 | ||
415 | (************************ Recursive Path Ordering ****************************) | |
416 | ||
417 | datatype ordering = Greater | Equal | NotGE | |
418 | ||
419 | ||
420 | fun eq_ordering (Greater,Greater) = true (*lars *) | |
421 | | eq_ordering (Equal,Equal) = true | |
422 | | eq_ordering (NotGE,NotGE) = true | |
423 | | eq_ordering _ = false | |
424 | ||
425 | fun ge_ord order pair = case order pair of NotGE => false | _ => true | |
426 | and gt_ord order pair = case order pair of Greater => true | _ => false | |
427 | and eq_ord order pair = case order pair of Equal => true | _ => false | |
428 | ||
429 | fun rem_eq equiv = | |
430 | let fun remrec x [] = raise FailRemEQ (*failwith "rem_eq"*) | |
431 | | remrec x (y::l) = if equiv (x,y) then l else y :: remrec x l | |
432 | in remrec | |
433 | end | |
434 | ||
435 | fun diff_eq equiv (x,y) = | |
436 | let fun diffrec (p as ([],_)) = p | |
437 | | diffrec ((h::t), y) = | |
438 | diffrec (t,rem_eq equiv h y) handle _ => | |
439 | let val (x',y') = diffrec (t,y) in (h::x',y') end | |
440 | in if length x > length y then diffrec(y,x) else diffrec(x,y) | |
441 | end | |
442 | ||
443 | (* multiset extension of order *) | |
444 | fun mult_ext order (Term(_,sons1), Term(_,sons2)) = | |
445 | (case diff_eq (eq_ord order) (sons1,sons2) of | |
446 | ([],[]) => Equal | |
447 | | (l1,l2) => | |
448 | if for_all (fn N => exists (fn M => eq_ordering(order (M,N),Greater)) l1) l2 | |
449 | then Greater else NotGE) | |
450 | | mult_ext order (_, _) = raise FailMultExt (*failwith "mult_ext"*) | |
451 | ||
452 | (* lexicographic extension of order *) | |
453 | fun lex_ext order ((M as Term(_,sons1)), (N as Term(_,sons2))) = | |
454 | let fun lexrec ([] , []) = Equal | |
455 | | lexrec ([] , _ ) = NotGE | |
456 | | lexrec ( _ , []) = Greater | |
457 | | lexrec (x1::l1, x2::l2) = | |
458 | case order (x1,x2) of | |
459 | Greater => if for_all (fn N' => gt_ord order (M,N')) l2 | |
460 | then Greater else NotGE | |
461 | | Equal => lexrec (l1,l2) | |
462 | | NotGE => if exists (fn M' => ge_ord order (M',N)) l1 | |
463 | then Greater else NotGE | |
464 | in lexrec (sons1, sons2) | |
465 | end | |
466 | | lex_ext order _ = raise FailLexExt (*failwith "lex_ext"*) | |
467 | ||
468 | (* recursive path ordering *) | |
469 | fun Group_rules() = [ | |
470 | (1, (1, (Term("*", [Term("U",[]), Var 1]), Var 1))), | |
471 | (2, (1, (Term("*", [Term("I",[Var 1]), Var 1]), Term("U",[])))), | |
472 | (3, (3, (Term("*", [Term("*", [Var 1, Var 2]), Var 3]), | |
473 | Term("*", [Var 1, Term("*", [Var 2, Var 3])]))))] | |
474 | ||
475 | fun Geom_rules() = [ | |
476 | (1,(1,(Term ("*",[(Term ("U",[])), (Var 1)]),(Var 1)))), | |
477 | (2,(1,(Term ("*",[(Term ("I",[(Var 1)])), (Var 1)]),(Term ("U",[]))))), | |
478 | (3,(3,(Term ("*",[(Term ("*",[(Var 1), (Var 2)])), (Var 3)]), | |
479 | (Term ("*",[(Var 1), (Term ("*",[(Var 2), (Var 3)]))]))))), | |
480 | (4,(0,(Term ("*",[(Term ("A",[])), (Term ("B",[]))]), | |
481 | (Term ("*",[(Term ("B",[])), (Term ("A",[]))]))))), | |
482 | (5,(0,(Term ("*",[(Term ("C",[])), (Term ("C",[]))]),(Term ("U",[]))))), | |
483 | (6,(0, | |
484 | (Term | |
485 | ("*", | |
486 | [(Term ("C",[])), | |
487 | (Term ("*",[(Term ("A",[])), (Term ("I",[(Term ("C",[]))]))]))]), | |
488 | (Term ("I",[(Term ("A",[]))]))))), | |
489 | (7,(0, | |
490 | (Term | |
491 | ("*", | |
492 | [(Term ("C",[])), | |
493 | (Term ("*",[(Term ("B",[])), (Term ("I",[(Term ("C",[]))]))]))]), | |
494 | (Term ("B",[]))))) | |
495 | ] | |
496 | ||
497 | fun Group_rank "U" = 0 | |
498 | | Group_rank "*" = 1 | |
499 | | Group_rank "I" = 2 | |
500 | | Group_rank "B" = 3 | |
501 | | Group_rank "C" = 4 | |
502 | | Group_rank "A" = 5 | |
503 | | Group_rank _ = 100 (*added, to avoid non-exhaustive patter (mads) *) | |
504 | ||
505 | fun Group_precedence op1 op2 = | |
506 | let val r1 = Group_rank op1 | |
507 | val r2 = Group_rank op2 | |
508 | in | |
509 | if eq_integer(r1,r2) then Equal else | |
510 | if r1 > r2 then Greater else NotGE | |
511 | end | |
512 | ||
513 | ||
514 | fun rpo () = | |
515 | let fun rporec (M,N) = | |
516 | if eq_term(M,N) then Equal else | |
517 | case M of | |
518 | Var m => NotGE | |
519 | | Term(op1,sons1) => | |
520 | case N of | |
521 | Var n => | |
522 | if occurs n M then Greater else NotGE | |
523 | | Term(op2,sons2) => | |
524 | case (Group_precedence op1 op2) of | |
525 | Greater => | |
526 | if for_all (fn N' => gt_ord rporec (M,N')) sons2 | |
527 | then Greater else NotGE | |
528 | | Equal => | |
529 | lex_ext rporec (M,N) | |
530 | | NotGE => | |
531 | if exists (fn M' => ge_ord rporec (M',N)) sons1 | |
532 | then Greater else NotGE | |
533 | in rporec | |
534 | end | |
535 | ||
536 | fun Group_order x = rpo () x | |
537 | ||
538 | fun greater pair = | |
539 | case Group_order pair of Greater => true | _ => false | |
540 | ||
541 | (****************** Critical pairs *********************) | |
542 | ||
543 | (* All (u,sig) such that N/u (&var) unifies with M, | |
544 | with principal unifier sig *) | |
545 | ||
546 | fun super M = | |
547 | let fun suprec (N as Term(_,sons)) = | |
548 | let fun collate (pairs,n) son = | |
549 | (pairs @ map (fn (u,sigma) => (n::u,sigma)) (suprec son), n+1) | |
550 | val insides : (int list * (int*term)list)list = (*type constraint added (mads)*) | |
551 | fst (it_list collate ([],1) sons) | |
552 | in ([], unify(M,N)) :: insides handle _ => insides | |
553 | end | |
554 | | suprec _ = [] | |
555 | in suprec | |
556 | end | |
557 | ||
558 | ||
559 | (******************** | |
560 | ||
561 | Ex : | |
562 | ||
563 | let (M,_) = <<F(A,B)>> | |
564 | and (N,_) = <<H(F(A,x),F(x,y))>> in super M N;; | |
565 | ==> [[1],[2,Term ("B",[])]; x <- B | |
566 | [2],[2,Term ("A",[]); 1,Term ("B",[])]] x <- A y <- B | |
567 | *) | |
568 | ||
569 | (* All (u,sigma), u&[], such that N/u unifies with M *) | |
570 | (* super_strict : term -> term -> (num list & subst) list *) | |
571 | ||
572 | fun super_strict M (Term(_,sons)) = | |
573 | let fun collate (pairs,n) son = | |
574 | (pairs @ map (fn (u,sigma) => (n::u,sigma)) (super M son), n+1) | |
575 | in fst (it_list collate ([],1) sons) end | |
576 | | super_strict _ _ = [] | |
577 | ||
578 | (* Critical pairs of L1=R1 with L2=R2 *) | |
579 | (* critical_pairs : term_pair -> term_pair -> term_pair list *) | |
580 | fun critical_pairs (L1,R1) (L2,R2) = | |
581 | let fun mk_pair (u,sigma) = | |
582 | (substitute sigma (replace L2 u R1), substitute sigma R2) in | |
583 | map mk_pair (super L1 L2) | |
584 | end | |
585 | ||
586 | (* Strict critical pairs of L1=R1 with L2=R2 *) | |
587 | (* strict_critical_pairs : term_pair -> term_pair -> term_pair list *) | |
588 | fun strict_critical_pairs (* r1908 *) (L1,R1) (L2,R2) = | |
589 | let fun mk_pair (u,sigma) = | |
590 | (substitute sigma (replace L2 u R1), substitute sigma R2) in (* these applications of substitute put terms attop *) | |
591 | map mk_pair (super_strict L1 L2) | |
592 | end | |
593 | ||
594 | (* All critical pairs of eq1 with eq2 *) | |
595 | fun mutual_critical_pairs eq1 eq2 = | |
596 | (strict_critical_pairs eq1 eq2) @ (critical_pairs eq2 eq1) | |
597 | ||
598 | (* Renaming of variables *) | |
599 | ||
600 | fun rename n (t1,t2) = | |
601 | let fun ren_rec (Var k) = Var(k+n) | |
602 | | ren_rec (Term(oper,sons)) = Term(oper, map ren_rec sons) | |
603 | in (ren_rec t1, ren_rec t2) | |
604 | end | |
605 | ||
606 | (************************ Completion ******************************) | |
607 | ||
608 | fun deletion_message (k,_) = | |
609 | (print_string "Rule ";print_num k; message " deleted") | |
610 | ||
611 | (* Generate failure message *) | |
612 | fun non_orientable (M,N) = | |
613 | (pretty_term M; print_string " = "; pretty_term N; print_newline()) | |
614 | ||
615 | fun copy_termpairlist [] = [] | |
616 | | copy_termpairlist ((M,N)::rest) = (copy_term M, copy_term N):: copy_termpairlist rest | |
617 | ||
618 | fun copy_int_pair(x,y) = (x+0, y+0) | |
619 | fun copy_int_pair_list l = map copy_int_pair l | |
620 | fun copy_int (x) = x+0 | |
621 | ||
622 | ||
623 | ||
624 | fun copy_arg(interm:bool, n, rules, failures, p, eps) = | |
625 | (interm, n, copy_rules rules, copy_termpairlist failures, copy_int_pair p, copy_termpairlist eps) | |
626 | ||
627 | (* Improved Knuth-Bendix completion procedure *) | |
628 | (* kb_completion : num -> rules -> term_pair list -> (num & num) -> term_pair list -> rules *) | |
629 | fun kb_completion (* [r2225] *)(arg as (done,n, rules, list, (k,l), eps)) = | |
630 | let fun kbrec (* [r2272] *) count n rules = | |
631 | let fun normal_form x = mrewrite_all rules x | |
632 | fun get_rule k = assoc eq_integer k rules | |
633 | fun process failures = | |
634 | let fun processf (k,l) = | |
635 | let fun processkl [] = | |
636 | if k<l then next_criticals (k+1,l) else | |
637 | if l<n then next_criticals (1,l+1) else | |
638 | (case failures of | |
639 | [] => (true, n, rules, [], (k,l), failures) (* successful completion *) | |
640 | | _ => (message "Non-orientable equations :"; | |
641 | app non_orientable failures; | |
642 | raise FailKbComplettion (*failwith "kb_completion"*) )) | |
643 | | processkl ((M,N)::eqs) = | |
644 | let val M' = normal_form M | |
645 | val N' = normal_form N | |
646 | fun enter_rule(left,right) = | |
647 | let val new_rule = (n+1, mk_rule left right) in | |
648 | (pretty_rule new_rule; | |
649 | let fun left_reducible (_,(_,(L,_))) = reducible left L | |
650 | val (redl,irredl) = partition left_reducible rules | |
651 | in (app deletion_message redl; | |
652 | let fun right_reduce (m,(_,(L,R))) = | |
653 | (m,mk_rule L (mrewrite_all (new_rule::rules) R)); | |
654 | val irreds = map right_reduce irredl | |
655 | val eqs' = map (fn (_,(_,pair)) => pair) redl | |
656 | in if count>0 | |
657 | then (kbrec (count-1) ((n+1)) ((new_rule::irreds)) [] ((k,l)) | |
658 | ((eqs @ eqs' @ failures)) | |
659 | ) | |
660 | else (false,n+1, new_rule::irreds, [], (k,l), (eqs @ eqs' @ failures)) | |
661 | end) | |
662 | end) | |
663 | end | |
664 | in if eq_term(M',N') then processkl eqs else | |
665 | if greater(M',N') then enter_rule( M', N') | |
666 | else | |
667 | if greater(N',M') then enter_rule( N', M') | |
668 | else | |
669 | (process ( ((M', N')::failures)) ( (k,l)) ( eqs)) | |
670 | end | |
671 | in processkl | |
672 | end | |
673 | and next_criticals (k,l) = | |
674 | (let val (v,el) = get_rule l in | |
675 | if eq_integer(k,l) then | |
676 | processf (k,l) (strict_critical_pairs el (rename v el)) | |
677 | else | |
678 | (let val (_,ek) = get_rule k in | |
679 | processf (k,l) (mutual_critical_pairs el (rename v ek)) | |
680 | end | |
681 | handle FailFind (*rule k deleted*) => | |
682 | next_criticals (k+1,l)) | |
683 | end | |
684 | handle FailFind (*rule l deleted*) => | |
685 | next_criticals (1,l+1)) | |
686 | in processf | |
687 | end | |
688 | in process | |
689 | end | |
690 | ||
691 | fun kb_outer (* [r2517] *)(arg as (_, n, rules, failures, (k,l), other_failures)) = | |
692 | case kbrec 1 n rules failures (k,l) other_failures of | |
693 | result as (true,_, result_rules,_,_,_) => if false then arg else result | |
694 | | arg0 as (false, n', rules', failures', (k',l'), eqs') => | |
695 | kb_outer(let val arg1 = copy_arg arg0 | |
696 | in (*resetRegions arg0;*) | |
697 | copy_arg(arg1) | |
698 | end | |
699 | ) | |
700 | ||
701 | ||
702 | in (fn (_,_,x,_,_,_) => x)(kb_outer(arg)) | |
703 | end | |
704 | ||
705 | fun kb_complete complete_rules (* the terms in the complete_rules are global *) rules = | |
706 | let val n = check_rules complete_rules | |
707 | val eqs = map (fn (_,(_,pair)) => pair) rules | |
708 | (* letregion r2656 *) | |
709 | val completed_rules = | |
710 | (* the copying in the line below is to avoid that kb_completion is called with attop modes *) | |
711 | kb_completion(false,n+0, copy_rules complete_rules, [], (n+0,n+0), copy_termpairlist eqs) | |
712 | in (message "Canonical set found :"; | |
713 | pretty_rules (rev completed_rules); | |
714 | (* end r2683 *) | |
715 | ()) | |
716 | end | |
717 | ||
718 | ||
719 | fun doit() = kb_complete [] (* terms in list global *) (Geom_rules()) | |
720 | fun testit _ = () | |
721 | ||
722 | ||
723 | in (*local*) | |
724 | val _ = (doit(); doit(); doit()) | |
725 | end (*local*) | |
726 |