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