/ Garbo / Garbo.cdr / mac / progrmng / cmlmcmpw.sit / Caml Light / examples / kb / go.ml

< prev

next >

MacOS 8.1

Win98

DOS

browse contents

view JSON data

view as text

+--------+-------------------------+-------------------------+--------+--------+
|00000000| 00 05 67 6f 2e 6d 6c 00 | 00 00 00 00 00 00 00 00 |..go.ml.|........|
|00000010| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|00000020| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|00000030| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|00000040| 00 54 45 58 54 4d 50 53 | 20 01 00 00 00 00 00 00 |.TEXTMPS| .......|
|00000050| 00 00 00 00 00 07 1c 00 | 00 01 7e a4 61 f5 9e a4 |........|..~.a...|
|00000060| 61 f5 9e 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |a.......|........|
|00000070| 00 00 00 00 00 00 00 00 | 00 00 81 81 b5 05 00 00 |........|........|
|00000080| 23 6f 70 65 6e 20 22 70 | 72 65 6c 75 64 65 22 3b |#open "p|relude";|
|00000090| 3b 0d 23 6f 70 65 6e 20 | 22 74 65 72 6d 73 22 3b |;.#open |"terms";|
|000000a0| 3b 0d 23 6f 70 65 6e 20 | 22 65 71 75 61 74 69 6f |;.#open |"equatio|
|000000b0| 6e 22 3b 3b 0d 23 6f 70 | 65 6e 20 22 6f 72 64 65 |n";;.#op|en "orde|
|000000c0| 72 22 3b 3b 0d 23 6f 70 | 65 6e 20 22 6b 62 22 3b |r";;.#op|en "kb";|
|000000d0| 3b 0d 0d 28 2a 20 54 68 | 65 20 61 78 69 6f 6d 73 |;..(* Th|e axioms|
|000000e0| 20 66 6f 72 20 67 72 6f | 75 70 73 20 2a 29 0d 0d | for gro|ups *)..|
|000000f0| 6c 65 74 20 47 72 6f 75 | 70 5f 72 75 6c 65 73 20 |let Grou|p_rules |
|00000100| 3d 20 5b 0d 20 20 31 2c | 20 28 31 2c 20 28 54 65 |= [.  1,| (1, (Te|
|00000110| 72 6d 28 22 2a 22 2c 20 | 5b 54 65 72 6d 28 22 55 |rm("*", |[Term("U|
|00000120| 22 2c 5b 5d 29 3b 20 56 | 61 72 20 31 5d 29 2c 20 |",[]); V|ar 1]), |
|00000130| 56 61 72 20 31 29 29 3b | 0d 20 20 32 2c 20 28 31 |Var 1));|.  2, (1|
|00000140| 2c 20 28 54 65 72 6d 28 | 22 2a 22 2c 20 5b 54 65 |, (Term(|"*", [Te|
|00000150| 72 6d 28 22 49 22 2c 5b | 56 61 72 20 31 5d 29 3b |rm("I",[|Var 1]);|
|00000160| 20 56 61 72 20 31 5d 29 | 2c 20 54 65 72 6d 28 22 | Var 1])|, Term("|
|00000170| 55 22 2c 5b 5d 29 29 29 | 3b 0d 20 20 33 2c 20 28 |U",[])))|;.  3, (|
|00000180| 33 2c 20 28 54 65 72 6d | 28 22 2a 22 2c 20 5b 54 |3, (Term|("*", [T|
|00000190| 65 72 6d 28 22 2a 22 2c | 20 5b 56 61 72 20 31 3b |erm("*",| [Var 1;|
|000001a0| 20 56 61 72 20 32 5d 29 | 3b 20 56 61 72 20 33 5d | Var 2])|; Var 3]|
|000001b0| 29 2c 0d 20 20 20 20 20 | 20 20 20 20 20 54 65 72 |),.     |     Ter|
|000001c0| 6d 28 22 2a 22 2c 20 5b | 56 61 72 20 31 3b 20 54 |m("*", [|Var 1; T|
|000001d0| 65 72 6d 28 22 2a 22 2c | 20 5b 56 61 72 20 32 3b |erm("*",| [Var 2;|
|000001e0| 20 56 61 72 20 33 5d 29 | 5d 29 29 29 0d 5d 3b 3b | Var 3])|]))).];;|
|000001f0| 0d 0d 6c 65 74 20 47 72 | 6f 75 70 5f 70 72 65 63 |..let Gr|oup_prec|
|00000200| 65 64 65 6e 63 65 20 6f | 70 31 20 6f 70 32 20 3d |edence o|p1 op2 =|
|00000210| 0d 20 20 69 66 20 6f 70 | 31 20 3d 20 6f 70 32 20 |.  if op|1 = op2 |
|00000220| 74 68 65 6e 20 45 71 75 | 61 6c 20 65 6c 73 65 0d |then Equ|al else.|
|00000230| 20 20 69 66 20 28 6f 70 | 31 20 3d 20 22 49 22 29 |  if (op|1 = "I")|
|00000240| 20 6f 72 20 28 6f 70 32 | 20 3d 20 22 55 22 29 20 | or (op2| = "U") |
|00000250| 74 68 65 6e 20 47 72 65 | 61 74 65 72 20 65 6c 73 |then Gre|ater els|
|00000260| 65 20 4e 6f 74 47 45 0d | 3b 3b 0d 0d 6c 65 74 20 |e NotGE.|;;..let |
|00000270| 47 72 6f 75 70 5f 6f 72 | 64 65 72 20 3d 20 72 70 |Group_or|der = rp|
|00000280| 6f 20 47 72 6f 75 70 5f | 70 72 65 63 65 64 65 6e |o Group_|preceden|
|00000290| 63 65 20 6c 65 78 5f 65 | 78 74 20 0d 3b 3b 0d 0d |ce lex_e|xt .;;..|
|000002a0| 28 2a 20 41 6e 6f 74 68 | 65 72 20 65 78 61 6d 70 |(* Anoth|er examp|
|000002b0| 6c 65 20 2a 29 0d 0d 6c | 65 74 20 47 65 6f 6d 5f |le *)..l|et Geom_|
|000002c0| 72 75 6c 65 73 20 3d 20 | 5b 0d 20 31 2c 28 31 2c |rules = |[. 1,(1,|
|000002d0| 28 54 65 72 6d 20 28 22 | 2a 22 2c 5b 28 54 65 72 |(Term ("|*",[(Ter|
|000002e0| 6d 20 28 22 55 22 2c 5b | 5d 29 29 3b 20 28 56 61 |m ("U",[|])); (Va|
|000002f0| 72 20 31 29 5d 29 2c 28 | 56 61 72 20 31 29 29 29 |r 1)]),(|Var 1)))|
|00000300| 3b 0d 20 32 2c 28 31 2c | 28 54 65 72 6d 20 28 22 |;. 2,(1,|(Term ("|
|00000310| 2a 22 2c 5b 28 54 65 72 | 6d 20 28 22 49 22 2c 5b |*",[(Ter|m ("I",[|
|00000320| 28 56 61 72 20 31 29 5d | 29 29 3b 20 28 56 61 72 |(Var 1)]|)); (Var|
|00000330| 20 31 29 5d 29 2c 28 54 | 65 72 6d 20 28 22 55 22 | 1)]),(T|erm ("U"|
|00000340| 2c 5b 5d 29 29 29 29 3b | 0d 20 33 2c 28 33 2c 28 |,[]))));|. 3,(3,(|
|00000350| 54 65 72 6d 20 28 22 2a | 22 2c 5b 28 54 65 72 6d |Term ("*|",[(Term|
|00000360| 20 28 22 2a 22 2c 5b 28 | 56 61 72 20 31 29 3b 20 | ("*",[(|Var 1); |
|00000370| 28 56 61 72 20 32 29 5d | 29 29 3b 20 28 56 61 72 |(Var 2)]|)); (Var|
|00000380| 20 33 29 5d 29 2c 0d 20 | 20 28 54 65 72 6d 20 28 | 3)]),. | (Term (|
|00000390| 22 2a 22 2c 5b 28 56 61 | 72 20 31 29 3b 20 28 54 |"*",[(Va|r 1); (T|
|000003a0| 65 72 6d 20 28 22 2a 22 | 2c 5b 28 56 61 72 20 32 |erm ("*"|,[(Var 2|
|000003b0| 29 3b 20 28 56 61 72 20 | 33 29 5d 29 29 5d 29 29 |); (Var |3)]))]))|
|000003c0| 29 29 3b 0d 20 34 2c 28 | 30 2c 28 54 65 72 6d 20 |));. 4,(|0,(Term |
|000003d0| 28 22 2a 22 2c 5b 28 54 | 65 72 6d 20 28 22 41 22 |("*",[(T|erm ("A"|
|000003e0| 2c 5b 5d 29 29 3b 20 28 | 54 65 72 6d 20 28 22 42 |,[])); (|Term ("B|
|000003f0| 22 2c 5b 5d 29 29 5d 29 | 2c 0d 20 20 28 54 65 72 |",[]))])|,.  (Ter|
|00000400| 6d 20 28 22 2a 22 2c 5b | 28 54 65 72 6d 20 28 22 |m ("*",[|(Term ("|
|00000410| 42 22 2c 5b 5d 29 29 3b | 20 28 54 65 72 6d 20 28 |B",[]));| (Term (|
|00000420| 22 41 22 2c 5b 5d 29 29 | 5d 29 29 29 29 3b 0d 20 |"A",[]))|]))));. |
|00000430| 35 2c 28 30 2c 28 54 65 | 72 6d 20 28 22 2a 22 2c |5,(0,(Te|rm ("*",|
|00000440| 5b 28 54 65 72 6d 20 28 | 22 43 22 2c 5b 5d 29 29 |[(Term (|"C",[]))|
|00000450| 3b 20 28 54 65 72 6d 20 | 28 22 43 22 2c 5b 5d 29 |; (Term |("C",[])|
|00000460| 29 5d 29 2c 28 54 65 72 | 6d 20 28 22 55 22 2c 5b |)]),(Ter|m ("U",[|
|00000470| 5d 29 29 29 29 3b 0d 20 | 36 2c 28 30 2c 0d 20 20 |]))));. |6,(0,.  |
|00000480| 28 54 65 72 6d 0d 20 20 | 20 28 22 2a 22 2c 0d 20 |(Term.  | ("*",. |
|00000490| 20 20 20 5b 28 54 65 72 | 6d 20 28 22 43 22 2c 5b |   [(Ter|m ("C",[|
|000004a0| 5d 29 29 3b 0d 20 20 20 | 20 20 28 54 65 72 6d 20 |]));.   |  (Term |
|000004b0| 28 22 2a 22 2c 5b 28 54 | 65 72 6d 20 28 22 41 22 |("*",[(T|erm ("A"|
|000004c0| 2c 5b 5d 29 29 3b 20 28 | 54 65 72 6d 20 28 22 49 |,[])); (|Term ("I|
|000004d0| 22 2c 5b 28 54 65 72 6d | 20 28 22 43 22 2c 5b 5d |",[(Term| ("C",[]|
|000004e0| 29 29 5d 29 29 5d 29 29 | 5d 29 2c 0d 20 20 28 54 |))]))]))|]),.  (T|
|000004f0| 65 72 6d 20 28 22 49 22 | 2c 5b 28 54 65 72 6d 20 |erm ("I"|,[(Term |
|00000500| 28 22 41 22 2c 5b 5d 29 | 29 5d 29 29 29 29 3b 0d |("A",[])|)]))));.|
|00000510| 20 37 2c 28 30 2c 0d 20 | 20 28 54 65 72 6d 0d 20 | 7,(0,. | (Term. |
|00000520| 20 20 28 22 2a 22 2c 0d | 20 20 20 20 5b 28 54 65 |  ("*",.|    [(Te|
|00000530| 72 6d 20 28 22 43 22 2c | 5b 5d 29 29 3b 0d 20 20 |rm ("C",|[]));.  |
|00000540| 20 20 20 28 54 65 72 6d | 20 28 22 2a 22 2c 5b 28 |   (Term| ("*",[(|
|00000550| 54 65 72 6d 20 28 22 42 | 22 2c 5b 5d 29 29 3b 20 |Term ("B|",[])); |
|00000560| 28 54 65 72 6d 20 28 22 | 49 22 2c 5b 28 54 65 72 |(Term ("|I",[(Ter|
|00000570| 6d 20 28 22 43 22 2c 5b | 5d 29 29 5d 29 29 5d 29 |m ("C",[|]))]))])|
|00000580| 29 5d 29 2c 0d 20 20 28 | 54 65 72 6d 20 28 22 42 |)]),.  (|Term ("B|
|00000590| 22 2c 5b 5d 29 29 29 29 | 0d 5d 3b 3b 0d 0d 6c 65 |",[]))))|.];;..le|
|000005a0| 74 20 47 65 6f 6d 5f 72 | 61 6e 6b 20 3d 20 66 75 |t Geom_r|ank = fu|
|000005b0| 6e 63 74 69 6f 6e 0d 20 | 20 20 20 22 55 22 20 2d |nction. |   "U" -|
|000005c0| 3e 20 30 0d 20 20 7c 20 | 22 2a 22 20 2d 3e 20 31 |> 0.  | |"*" -> 1|
|000005d0| 0d 20 20 7c 20 22 49 22 | 20 2d 3e 20 32 0d 20 20 |.  | "I"| -> 2.  |
|000005e0| 7c 20 22 42 22 20 2d 3e | 20 33 0d 20 20 7c 20 22 || "B" ->| 3.  | "|
|000005f0| 43 22 20 2d 3e 20 34 0d | 20 20 7c 20 22 41 22 20 |C" -> 4.|  | "A" |
|00000600| 2d 3e 20 35 0d 3b 3b 0d | 0d 6c 65 74 20 47 65 6f |-> 5.;;.|.let Geo|
|00000610| 6d 5f 70 72 65 63 65 64 | 65 6e 63 65 20 6f 70 31 |m_preced|ence op1|
|00000620| 20 6f 70 32 20 3d 0d 20 | 20 6c 65 74 20 72 31 20 | op2 =. | let r1 |
|00000630| 3d 20 47 65 6f 6d 5f 72 | 61 6e 6b 20 6f 70 31 0d |= Geom_r|ank op1.|
|00000640| 20 20 61 6e 64 20 72 32 | 20 3d 20 47 65 6f 6d 5f |  and r2| = Geom_|
|00000650| 72 61 6e 6b 20 6f 70 32 | 20 69 6e 0d 20 20 20 20 |rank op2| in.    |
|00000660| 69 66 20 72 31 20 3d 20 | 72 32 20 74 68 65 6e 20 |if r1 = |r2 then |
|00000670| 45 71 75 61 6c 20 65 6c | 73 65 0d 20 20 20 20 69 |Equal el|se.    i|
|00000680| 66 20 72 31 20 3e 20 72 | 32 20 74 68 65 6e 20 47 |f r1 > r|2 then G|
|00000690| 72 65 61 74 65 72 20 65 | 6c 73 65 20 4e 6f 74 47 |reater e|lse NotG|
|000006a0| 45 0d 3b 3b 0d 0d 6c 65 | 74 20 47 65 6f 6d 5f 6f |E.;;..le|t Geom_o|
|000006b0| 72 64 65 72 20 3d 20 72 | 70 6f 20 47 65 6f 6d 5f |rder = r|po Geom_|
|000006c0| 70 72 65 63 65 64 65 6e | 63 65 20 6c 65 78 5f 65 |preceden|ce lex_e|
|000006d0| 78 74 20 0d 3b 3b 0d 0d | 6b 62 5f 63 6f 6d 70 6c |xt .;;..|kb_compl|
|000006e0| 65 74 65 20 28 67 74 5f | 6f 72 64 20 47 72 6f 75 |ete (gt_|ord Grou|
|000006f0| 70 5f 6f 72 64 65 72 29 | 20 5b 5d 20 47 72 6f 75 |p_order)| [] Grou|
|00000700| 70 5f 72 75 6c 65 73 3b | 3b 0d 0d 28 2a 20 49 66 |p_rules;|;..(* If|
|00000710| 20 79 6f 75 20 68 61 76 | 65 20 61 20 66 61 73 74 | you hav|e a fast|
|00000720| 20 6d 61 63 68 69 6e 65 | 2c 20 79 6f 75 20 6d 61 | machine|, you ma|
|00000730| 79 20 75 6e 63 6f 6d 6d | 65 6e 74 20 74 68 65 20 |y uncomm|ent the |
|00000740| 66 6f 6c 6c 6f 77 69 6e | 67 20 6c 69 6e 65 3a 20 |followin|g line: |
|00000750| 2a 29 0d 0d 28 2a 20 70 | 72 69 6e 74 5f 6e 65 77 |*)..(* p|rint_new|
|00000760| 6c 69 6e 65 28 29 3b 20 | 6b 62 5f 63 6f 6d 70 6c |line(); |kb_compl|
|00000770| 65 74 65 20 28 67 74 5f | 6f 72 64 20 47 65 6f 6d |ete (gt_|ord Geom|
|00000780| 5f 6f 72 64 65 72 29 20 | 5b 5d 20 47 65 6f 6d 5f |_order) |[] Geom_|
|00000790| 72 75 6c 65 73 3b 3b 20 | 20 2a 29 0d 00 00 00 00 |rules;; | *).....|
|000007a0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|000007b0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|000007c0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|000007d0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|000007e0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|000007f0| 00 00 00 00 00 00 00 00 | 00 00 00 00 00 00 00 00 |........|........|
|00000800| 00 00 01 00 00 00 01 4c | 00 00 00 4c 00 00 00 32 |.......L|...L...2|
|00000810| 3b 0d 23 6f 70 65 6e 20 | 22 74 65 72 6d 73 22 3b |;.#open |"terms";|
|00000820| 3b 0d 23 6f 70 65 6e 20 | 22 65 71 75 61 74 69 6f |;.#open |"equatio|
|00000830| 05 67 6f 2e 6d 6c 02 00 | 00 00 54 45 58 54 4d 50 |.go.ml..|..TEXTMP|
|00000840| 53 20 01 00 00 00 00 c0 | 00 00 00 00 1b 67 00 00 |S ......|.....g..|
|00000850| 00 00 54 45 58 54 4d 50 | 53 20 01 00 00 00 00 c0 |..TEXTMP|S ......|
|00000860| 00 00 13 2d 00 00 00 00 | 00 00 00 00 1c cf 00 00 |...-....|........|
|00000870| 00 00 a4 58 5d 4f 00 00 | 07 1c 00 00 01 7e 73 20 |...X]O..|.....~s |
|00000880| 3d 20 5b 0d 20 20 31 2c | 20 28 31 2c 20 28 54 65 |= [.  1,| (1, (Te|
|00000890| 72 6d 28 22 2a 22 2c 20 | 5b 54 65 72 6d 28 22 55 |rm("*", |[Term("U|
|000008a0| 22 2c 5b 5d 29 3b 20 56 | 61 72 20 31 5d 29 2c 20 |",[]); V|ar 1]), |
|000008b0| 56 61 72 20 31 29 29 3b | 0d 20 20 32 2c 20 28 31 |Var 1));|.  2, (1|
|000008c0| 2c 20 28 54 65 72 6d 28 | 22 2a 22 2c 20 5b 54 65 |, (Term(|"*", [Te|
|000008d0| 72 6d 28 22 49 22 2c 5b | 56 61 72 20 31 5d 29 3b |rm("I",[|Var 1]);|
|000008e0| 20 56 61 72 20 31 5d 29 | 2c 20 54 65 72 6d 28 22 | Var 1])|, Term("|
|000008f0| 55 22 2c 5b 5d 29 29 29 | 3b 0d 20 20 33 2c 20 28 |U",[])))|;.  3, (|
|00000900| 00 00 00 48 00 09 4d 6f | 6e 61 63 6f 00 00 a8 6c |...H..Mo|naco...l|
|00000910| 00 00 00 14 00 01 a9 98 | 00 0a 00 03 00 00 01 00 |........|........|
|00000920| 00 1e a9 5c 00 00 00 06 | 00 04 00 3c 00 24 01 53 |...\....|...<.$.S|
|00000930| 01 bd 00 3c 00 24 01 53 | 01 bd a4 61 bd 5e 00 00 |...<.$.S|...a.^..|
|00000940| 07 1c 00 00 07 1c 00 00 | 05 fb 01 00 00 00 01 00 |........|........|
|00000950| 00 00 01 4c 00 00 00 4c | 00 00 00 32 00 54 c7 3c |...L...L|...2.T.<|
|00000960| 05 84 00 00 00 1c 00 32 | 00 00 4d 50 53 52 00 00 |.......2|..MPSR..|
|00000970| 00 0a 03 ed ff ff 00 00 | 00 00 00 56 6f 78 00 00 |........|...Vox..|
+--------+-------------------------+-------------------------+--------+--------+