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