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