← Back to branch summary

~ubuntu-branches/ubuntu/hardy/ocaml-doc/hardy

« back to all changes in this revision

Viewing changes to examples/kb/go.ml

  • Committer: Bazaar Package Importer
  • Author(s): Samuel Mimram
  • Date: 2007-09-08 01:49:22 UTC
  • mfrom: (0.1.3 upstream)
  • Revision ID: james.westby@ubuntu.com-20070908014922-lvihyehz0ndq7suu
Tags: 3.10-1
* New upstream release.
* Removed camlp4 documentation since it is not up-to-date.
* Updated to standards version 3.7.2, no changes needed.
* Updated my email address.

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/kb/go.ml
1
 
open Terms;;
2
 
open Order;;
3
 
open Kb;;
4
 
 
5
 
(* The axioms for groups *)
6
 
 
7
 
let group_rules = [
8
 
  1, (1, (Term("*", [Term("U", []); Var 1]), Var 1));
9
 
  2, (1, (Term("*", [Term("I", [Var 1]); Var 1]), Term("U", [])));
10
 
  3, (3, (Term("*", [Term("*", [Var 1; Var 2]); Var 3]),
11
 
          Term("*", [Var 1; Term("*", [Var 2; Var 3])])))
12
 
];;
13
 
 
14
 
let group_precedence op1 op2 =
15
 
  if op1 = op2 then Equal else
16
 
  if (op1 = "I") or (op2 = "U") then Greater else NotGE
17
 
;;
18
 
 
19
 
let group_order = rpo group_precedence lex_ext 
20
 
;;
21
 
 
22
 
(* Another example *)
23
 
 
24
 
let geom_rules = [
25
 
 1, (1, (Term ("*", [(Term ("U", [])); (Var 1)]), (Var 1)));
26
 
 2, (1, (Term ("*", [(Term ("I", [(Var 1)])); (Var 1)]), (Term ("U", []))));
27
 
 3, (3, (Term ("*", [(Term ("*", [(Var 1); (Var 2)])); (Var 3)]),
28
 
  (Term ("*", [(Var 1); (Term ("*", [(Var 2); (Var 3)]))]))));
29
 
 4, (0, (Term ("*", [(Term ("A", [])); (Term ("B", []))]),
30
 
  (Term ("*", [(Term ("B", [])); (Term ("A", []))]))));
31
 
 5, (0, (Term ("*", [(Term ("C", [])); (Term ("C", []))]), (Term ("U", []))));
32
 
 6, (0,
33
 
  (Term
34
 
   ("*",
35
 
    [(Term ("C", []));
36
 
     (Term ("*", [(Term ("A", [])); (Term ("I", [(Term ("C", []))]))]))]),
37
 
  (Term ("I", [(Term ("A", []))]))));
38
 
 7, (0,
39
 
  (Term
40
 
   ("*",
41
 
    [(Term ("C", []));
42
 
     (Term ("*", [(Term ("B", [])); (Term ("I", [(Term ("C", []))]))]))]),
43
 
  (Term ("B", []))))
44
 
];;
45
 
 
46
 
let geom_rank = function
47
 
  | "U" -> 0
48
 
  | "*" -> 1
49
 
  | "I" -> 2
50
 
  | "B" -> 3
51
 
  | "C" -> 4
52
 
  | "A" -> 5
53
 
  |  _  -> failwith "Geom_rank"
54
 
;;
55
 
 
56
 
let geom_precedence op1 op2 =
57
 
  let r1 = geom_rank op1
58
 
  and r2 = geom_rank op2 in
59
 
  if r1 = r2 then Equal else
60
 
  if r1 > r2 then Greater else NotGE
61
 
;;
62
 
 
63
 
let geom_order = rpo geom_precedence lex_ext 
64
 
;;
65
 
 
66
 
kb_complete (gt_ord group_order) [] group_rules;;
67
 
 
68
 
(* If you have a fast machine, you may uncomment the following line: *)
69
 
 
70
 
(* print_newline(); kb_complete (gt_ord geom_order) [] geom_rules;; *)
71