Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/benchmarks/programs/k-b/knuth-bendix.sml
ViewVC logotype

Annotation of /sml/trunk/benchmarks/programs/k-b/knuth-bendix.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 193 - (view) (download)

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

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0