home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 2 / Apprentice-Release2.iso / Tools / Languages / Caml Light 0.61 / Binaries / examples / kb / go.ml < prev    next >
Encoding:
Text File  |  1993-09-24  |  1.8 KB  |  74 lines  |  [TEXT/ttxt]
  1. #open "prelude";;
  2. #open "terms";;
  3. #open "equation";;
  4. #open "order";;
  5. #open "kb";;
  6.  
  7. (* The axioms for groups *)
  8.  
  9. let group_rules = [
  10.   1, (1, (Term("*", [Term("U",[]); Var 1]), Var 1));
  11.   2, (1, (Term("*", [Term("I",[Var 1]); Var 1]), Term("U",[])));
  12.   3, (3, (Term("*", [Term("*", [Var 1; Var 2]); Var 3]),
  13.           Term("*", [Var 1; Term("*", [Var 2; Var 3])])))
  14. ];;
  15.  
  16. let group_precedence op1 op2 =
  17.   if op1 = op2 then Equal else
  18.   if (op1 = "I") or (op2 = "U") then Greater else NotGE
  19. ;;
  20.  
  21. let group_order = rpo group_precedence lex_ext 
  22. ;;
  23.  
  24. (* Another example *)
  25.  
  26. let geom_rules = [
  27.  1,(1,(Term ("*",[(Term ("U",[])); (Var 1)]),(Var 1)));
  28.  2,(1,(Term ("*",[(Term ("I",[(Var 1)])); (Var 1)]),(Term ("U",[]))));
  29.  3,(3,(Term ("*",[(Term ("*",[(Var 1); (Var 2)])); (Var 3)]),
  30.   (Term ("*",[(Var 1); (Term ("*",[(Var 2); (Var 3)]))]))));
  31.  4,(0,(Term ("*",[(Term ("A",[])); (Term ("B",[]))]),
  32.   (Term ("*",[(Term ("B",[])); (Term ("A",[]))]))));
  33.  5,(0,(Term ("*",[(Term ("C",[])); (Term ("C",[]))]),(Term ("U",[]))));
  34.  6,(0,
  35.   (Term
  36.    ("*",
  37.     [(Term ("C",[]));
  38.      (Term ("*",[(Term ("A",[])); (Term ("I",[(Term ("C",[]))]))]))]),
  39.   (Term ("I",[(Term ("A",[]))]))));
  40.  7,(0,
  41.   (Term
  42.    ("*",
  43.     [(Term ("C",[]));
  44.      (Term ("*",[(Term ("B",[])); (Term ("I",[(Term ("C",[]))]))]))]),
  45.   (Term ("B",[]))))
  46. ];;
  47.  
  48. let geom_rank = function
  49.     "U" -> 0
  50.   | "*" -> 1
  51.   | "I" -> 2
  52.   | "B" -> 3
  53.   | "C" -> 4
  54.   | "A" -> 5
  55.   |  _  -> failwith "Geom_rank"
  56. ;;
  57.  
  58. let geom_precedence op1 op2 =
  59.   let r1 = geom_rank op1
  60.   and r2 = geom_rank op2 in
  61.     if r1 = r2 then Equal else
  62.     if r1 > r2 then Greater else NotGE
  63. ;;
  64.  
  65. let geom_order = rpo geom_precedence lex_ext 
  66. ;;
  67.  
  68. kb_complete (gt_ord group_order) [] group_rules;;
  69.  
  70. (* If you have a fast machine, you may uncomment the following line: *)
  71.  
  72. (* print_newline(); kb_complete (gt_ord geom_order) [] geom_rules;; *)
  73.  
  74.