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/todo/vboyer/boyer.sml+
ViewVC logotype

Annotation of /sml/trunk/benchmarks/todo/vboyer/boyer.sml+

Parent Directory Parent Directory | Revision Log Revision Log


Revision 193 - (view) (download)

1 : monnier 193 (* boyer.sm:
2 :     *
3 :     * Tautology checker
4 :     *)
5 :    
6 :     signature BOYER =
7 :     sig
8 :     open Terms;
9 :     val tautp: term -> bool;
10 :     end;
11 :    
12 :     structure Boyer: BOYER =
13 :     struct
14 :    
15 :     open Terms
16 :    
17 :     fun mem x [] = false
18 :     | mem x (y::L) = x=y orelse mem x L
19 :    
20 :     fun truep (x, lst) = (case x
21 :     of Prop(head, _) => headname head = "true" orelse mem x lst
22 :     | _ => mem x lst
23 :     (* end case *))
24 :    
25 :     fun falsep (x, lst) = (case x
26 :     of Prop(head, _) => headname head = "false" orelse mem x lst
27 :     | _ => mem x lst
28 :     (* end case *))
29 :    
30 :     fun tautologyp (x, true_lst, false_lst) =
31 :     if truep (x, true_lst)
32 :     then true
33 :     else if falsep (x, false_lst)
34 :     then false
35 :     else (case x
36 :     of Var _ => false
37 :     | Prop (head, #[test, yes, no]) =>
38 :     if headname head = "if"
39 :     then if truep (test, true_lst)
40 :     then tautologyp (yes, true_lst, false_lst)
41 :     else if falsep (test, false_lst)
42 :     then tautologyp (no, true_lst, false_lst)
43 :     else (tautologyp (yes, test::true_lst, false_lst)
44 :     andalso tautologyp (no, true_lst, test::false_lst))
45 :     else false)
46 :    
47 :     fun tautp x = tautologyp(rewrite x, [], []);
48 :    
49 :     end; (* Boyer *)
50 :    
51 :     (* the benchmark *)
52 :     structure Main : BMARK =
53 :     struct
54 :    
55 :     open Terms;
56 :     open Boyer;
57 :    
58 :     val subst =
59 :     [Bind(23,
60 :     Prop
61 :     (get "f",
62 :     #[Prop
63 :     (get "plus",
64 :     #[Prop (get "plus",#[Var 0, Var 1]),
65 :     Prop (get "plus",#[Var 2, Prop (get "zero",[])])])])),
66 :     Bind(24,
67 :     Prop
68 :     (get "f",
69 :     #[Prop
70 :     (get "times",
71 :     #[Prop (get "times",#[Var 0, Var 1]),
72 :     Prop (get "plus",#[Var 2, Var 3])])])),
73 :     Bind(25,
74 :     Prop
75 :     (get "f",
76 :     #[Prop
77 :     (get "reverse",
78 :     #[Prop
79 :     (get "append",
80 :     #[Prop (get "append",#[Var 0, Var 1]),
81 :     Prop (get "nil",[])])])])),
82 :     Bind(20,
83 :     Prop
84 :     (get "equal",
85 :     #[Prop (get "plus",#[Var 0, Var 1]),
86 :     Prop (get "difference",#[Var 23, Var 24])])),
87 :     Bind(22,
88 :     Prop
89 :     (get "lt",
90 :     #[Prop (get "remainder",#[Var 0, Var 1]),
91 :     Prop (get "member",#[Var 0, Prop (get "length",#[Var 1])])]))]
92 :    
93 :     val term =
94 :     Prop
95 :     (get "implies",
96 :     #[Prop
97 :     (get "and",
98 :     #[Prop (get "implies",#[Var 23, Var 24]),
99 :     Prop
100 :     (get "and",
101 :     #[Prop (get "implies",#[Var 24, Var 25]),
102 :     Prop
103 :     (get "and",
104 :     #[Prop (get "implies",#[Var 25, Var 20]),
105 :     Prop (get "implies",#[Var 20, Var 22])])])]),
106 :     Prop (get "implies",#[Var 23, Var 22])])
107 :    
108 :     fun testit outstrm = if tautp (apply_subst subst term)
109 :     then output (outstrm, "Proved!\n")
110 :     else output (outstrm, "Cannot prove!\n")
111 :    
112 :     fun doit () = (tautp (apply_subst subst term); ())
113 :    
114 :     end; (* Main *)

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