925 lines
25 KiB
Standard ML
925 lines
25 KiB
Standard ML
(* terms.sml:
|
|
*
|
|
* Manipulations over terms
|
|
*)
|
|
|
|
signature TERMS =
|
|
sig
|
|
type head;
|
|
datatype term =
|
|
Var of int
|
|
| Prop of head * term list;
|
|
datatype binding = Bind of int * term;
|
|
val get: string -> head
|
|
and headname: head -> string
|
|
and add_lemma: term -> unit
|
|
and apply_subst: binding list -> term -> term
|
|
and rewrite: term -> term
|
|
end;
|
|
|
|
structure Terms:TERMS =
|
|
struct
|
|
|
|
datatype term
|
|
= Var of int
|
|
| Prop of { name: string, props: (term * term) list ref } * term list
|
|
|
|
type head = { name: string, props: (term * term) list ref }
|
|
|
|
val lemmas = ref ([] : head list)
|
|
|
|
(* replacement for property lists *)
|
|
|
|
fun headname {name = n, props=p} = n;
|
|
|
|
fun get name =
|
|
let fun get_rec ((hd1 as {name=n,...})::hdl) =
|
|
if n = name then hd1 else get_rec hdl
|
|
| get_rec [] =
|
|
let val entry = {name = name, props = ref []} in
|
|
lemmas := entry :: !lemmas;
|
|
entry
|
|
end
|
|
in
|
|
get_rec (!lemmas)
|
|
end
|
|
;
|
|
|
|
fun add_lemma (Prop(_, [(left as Prop({props=r,...},_)), right])) =
|
|
r := (left, right) :: !r
|
|
;
|
|
|
|
(* substitutions *)
|
|
|
|
exception failure of string;
|
|
|
|
datatype binding = Bind of int * term
|
|
;
|
|
|
|
fun get_binding v =
|
|
let fun get_rec [] = raise (failure "unbound")
|
|
| get_rec (Bind(w,t)::rest) =
|
|
if v = w then t else get_rec rest
|
|
in
|
|
get_rec
|
|
end
|
|
;
|
|
|
|
fun apply_subst alist =
|
|
let fun as_rec (term as Var v) =
|
|
((get_binding v alist) handle failure _ => term)
|
|
| as_rec (Prop (head,argl)) =
|
|
Prop (head, map as_rec argl)
|
|
in
|
|
as_rec
|
|
end
|
|
;
|
|
|
|
exception Unify;
|
|
|
|
fun unify (term1, term2) = unify1 (term1, term2, [])
|
|
and unify1 (term1, term2, unify_subst) =
|
|
(case term2 of
|
|
Var v =>
|
|
((if get_binding v unify_subst = term1
|
|
then unify_subst
|
|
else raise Unify)
|
|
handle failure _ =>
|
|
Bind(v,term1)::unify_subst)
|
|
| Prop (head2,argl2) =>
|
|
case term1 of
|
|
Var _ => raise Unify
|
|
| Prop (head1,argl1) =>
|
|
if head1=head2 then unify1_lst (argl1, argl2, unify_subst)
|
|
else raise Unify)
|
|
and unify1_lst ([], [], unify_subst) = unify_subst
|
|
| unify1_lst (h1::r1, h2::r2, unify_subst) =
|
|
unify1_lst(r1, r2, unify1(h1, h2, unify_subst))
|
|
| unify1_lst _ = raise Unify
|
|
;
|
|
|
|
fun rewrite (term as Var _) = term
|
|
| rewrite (Prop ((head as {props=p,...}), argl)) =
|
|
rewrite_with_lemmas (Prop (head, map rewrite argl), !p)
|
|
and rewrite_with_lemmas (term, []) = term
|
|
| rewrite_with_lemmas (term, (t1,t2)::rest) =
|
|
rewrite (apply_subst (unify (term, t1)) t2)
|
|
handle unify =>
|
|
rewrite_with_lemmas (term, rest)
|
|
;
|
|
end;
|
|
(* rules.sml:
|
|
*)
|
|
|
|
structure Rules =
|
|
struct
|
|
|
|
open Terms;
|
|
|
|
datatype cterm = CVar of int | CProp of string * cterm list;
|
|
|
|
fun cterm_to_term (CVar v) = Var v
|
|
| cterm_to_term (CProp(p, l)) = Prop(get p, map cterm_to_term l)
|
|
|
|
fun add t = add_lemma (cterm_to_term t)
|
|
|
|
val _ = (
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("compile",[CVar 5]),
|
|
CProp
|
|
("reverse",
|
|
[CProp ("codegen",[CProp ("optimize",[CVar 5]), CProp ("nil",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("eqp",[CVar 23, CVar 24]),
|
|
CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("gt",[CVar 23, CVar 24]), CProp ("lt",[CVar 24, CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("le",[CVar 23, CVar 24]), CProp ("ge",[CVar 24, CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("ge",[CVar 23, CVar 24]), CProp ("le",[CVar 24, CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("boolean",[CVar 23]),
|
|
CProp
|
|
("or",
|
|
[CProp ("equal",[CVar 23, CProp ("true",[])]),
|
|
CProp ("equal",[CVar 23, CProp ("false",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("iff",[CVar 23, CVar 24]),
|
|
CProp
|
|
("and",
|
|
[CProp ("implies",[CVar 23, CVar 24]),
|
|
CProp ("implies",[CVar 24, CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("even1",[CVar 23]),
|
|
CProp
|
|
("if",
|
|
[CProp ("zerop",[CVar 23]), CProp ("true",[]),
|
|
CProp ("odd",[CProp ("sub1",[CVar 23])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("countps_",[CVar 11, CVar 15]),
|
|
CProp ("countps_loop",[CVar 11, CVar 15, CProp ("zero",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("fact_",[CVar 8]),
|
|
CProp ("fact_loop",[CVar 8, CProp ("one",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("reverse_",[CVar 23]),
|
|
CProp ("reverse_loop",[CVar 23, CProp ("nil",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("divides",[CVar 23, CVar 24]),
|
|
CProp ("zerop",[CProp ("remainder",[CVar 24, CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("assume_true",[CVar 21, CVar 0]),
|
|
CProp ("cons",[CProp ("cons",[CVar 21, CProp ("true",[])]), CVar 0])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("assume_false",[CVar 21, CVar 0]),
|
|
CProp ("cons",[CProp ("cons",[CVar 21, CProp ("false",[])]), CVar 0])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("tautology_checker",[CVar 23]),
|
|
CProp ("tautologyp",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("falsify",[CVar 23]),
|
|
CProp ("falsify1",[CProp ("normalize",[CVar 23]), CProp ("nil",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("prime",[CVar 23]),
|
|
CProp
|
|
("and",
|
|
[CProp ("not",[CProp ("zerop",[CVar 23])]),
|
|
CProp
|
|
("not",
|
|
[CProp ("equal",[CVar 23, CProp ("add1",[CProp ("zero",[])])])]),
|
|
CProp ("prime1",[CVar 23, CProp ("sub1",[CVar 23])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("and",[CVar 15, CVar 16]),
|
|
CProp
|
|
("if",
|
|
[CVar 15,
|
|
CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
|
|
CProp ("false",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("or",[CVar 15, CVar 16]),
|
|
CProp
|
|
("if",
|
|
[CVar 15, CProp ("true",[]),
|
|
CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
|
|
CProp ("false",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("not",[CVar 15]),
|
|
CProp ("if",[CVar 15, CProp ("false",[]), CProp ("true",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("implies",[CVar 15, CVar 16]),
|
|
CProp
|
|
("if",
|
|
[CVar 15,
|
|
CProp ("if",[CVar 16, CProp ("true",[]), CProp ("false",[])]),
|
|
CProp ("true",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("fix",[CVar 23]),
|
|
CProp ("if",[CProp ("numberp",[CVar 23]), CVar 23, CProp ("zero",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("if",[CProp ("if",[CVar 0, CVar 1, CVar 2]), CVar 3, CVar 4]),
|
|
CProp
|
|
("if",
|
|
[CVar 0, CProp ("if",[CVar 1, CVar 3, CVar 4]),
|
|
CProp ("if",[CVar 2, CVar 3, CVar 4])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("zerop",[CVar 23]),
|
|
CProp
|
|
("or",
|
|
[CProp ("equal",[CVar 23, CProp ("zero",[])]),
|
|
CProp ("not",[CProp ("numberp",[CVar 23])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("plus",[CProp ("plus",[CVar 23, CVar 24]), CVar 25]),
|
|
CProp ("plus",[CVar 23, CProp ("plus",[CVar 24, CVar 25])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CProp ("plus",[CVar 0, CVar 1]), CProp ("zero",[])]),
|
|
CProp ("and",[CProp ("zerop",[CVar 0]), CProp ("zerop",[CVar 1])])]));
|
|
add (CProp
|
|
("equal",[CProp ("difference",[CVar 23, CVar 23]), CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("plus",[CVar 0, CVar 1]), CProp ("plus",[CVar 0, CVar 2])]),
|
|
CProp ("equal",[CProp ("fix",[CVar 1]), CProp ("fix",[CVar 2])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",[CProp ("zero",[]), CProp ("difference",[CVar 23, CVar 24])]),
|
|
CProp ("not",[CProp ("gt",[CVar 24, CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CVar 23, CProp ("difference",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("numberp",[CVar 23]),
|
|
CProp
|
|
("or",
|
|
[CProp ("equal",[CVar 23, CProp ("zero",[])]),
|
|
CProp ("zerop",[CVar 24])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("meaning",
|
|
[CProp ("plus_tree",[CProp ("append",[CVar 23, CVar 24])]), CVar 0]),
|
|
CProp
|
|
("plus",
|
|
[CProp ("meaning",[CProp ("plus_tree",[CVar 23]), CVar 0]),
|
|
CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("meaning",
|
|
[CProp ("plus_tree",[CProp ("plus_fringe",[CVar 23])]), CVar 0]),
|
|
CProp ("fix",[CProp ("meaning",[CVar 23, CVar 0])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("append",[CProp ("append",[CVar 23, CVar 24]), CVar 25]),
|
|
CProp ("append",[CVar 23, CProp ("append",[CVar 24, CVar 25])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("reverse",[CProp ("append",[CVar 0, CVar 1])]),
|
|
CProp
|
|
("append",[CProp ("reverse",[CVar 1]), CProp ("reverse",[CVar 0])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("times",[CVar 23, CProp ("plus",[CVar 24, CVar 25])]),
|
|
CProp
|
|
("plus",
|
|
[CProp ("times",[CVar 23, CVar 24]),
|
|
CProp ("times",[CVar 23, CVar 25])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("times",[CProp ("times",[CVar 23, CVar 24]), CVar 25]),
|
|
CProp ("times",[CVar 23, CProp ("times",[CVar 24, CVar 25])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",[CProp ("times",[CVar 23, CVar 24]), CProp ("zero",[])]),
|
|
CProp ("or",[CProp ("zerop",[CVar 23]), CProp ("zerop",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("exec",[CProp ("append",[CVar 23, CVar 24]), CVar 15, CVar 4]),
|
|
CProp
|
|
("exec",[CVar 24, CProp ("exec",[CVar 23, CVar 15, CVar 4]), CVar 4])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("mc_flatten",[CVar 23, CVar 24]),
|
|
CProp ("append",[CProp ("flatten",[CVar 23]), CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("member",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
|
|
CProp
|
|
("or",
|
|
[CProp ("member",[CVar 23, CVar 0]),
|
|
CProp ("member",[CVar 23, CVar 1])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("member",[CVar 23, CProp ("reverse",[CVar 24])]),
|
|
CProp ("member",[CVar 23, CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("length",[CProp ("reverse",[CVar 23])]),
|
|
CProp ("length",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("member",[CVar 0, CProp ("intersect",[CVar 1, CVar 2])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("member",[CVar 0, CVar 1]), CProp ("member",[CVar 0, CVar 2])])]));
|
|
add (CProp
|
|
("equal",[CProp ("nth",[CProp ("zero",[]), CVar 8]), CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("exp",[CVar 8, CProp ("plus",[CVar 9, CVar 10])]),
|
|
CProp
|
|
("times",
|
|
[CProp ("exp",[CVar 8, CVar 9]), CProp ("exp",[CVar 8, CVar 10])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("exp",[CVar 8, CProp ("times",[CVar 9, CVar 10])]),
|
|
CProp ("exp",[CProp ("exp",[CVar 8, CVar 9]), CVar 10])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("reverse_loop",[CVar 23, CVar 24]),
|
|
CProp ("append",[CProp ("reverse",[CVar 23]), CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("reverse_loop",[CVar 23, CProp ("nil",[])]),
|
|
CProp ("reverse",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("count_list",[CVar 25, CProp ("sort_lp",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("plus",
|
|
[CProp ("count_list",[CVar 25, CVar 23]),
|
|
CProp ("count_list",[CVar 25, CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("append",[CVar 0, CVar 1]), CProp ("append",[CVar 0, CVar 2])]),
|
|
CProp ("equal",[CVar 1, CVar 2])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("plus",
|
|
[CProp ("remainder",[CVar 23, CVar 24]),
|
|
CProp ("times",[CVar 24, CProp ("quotient",[CVar 23, CVar 24])])]),
|
|
CProp ("fix",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("power_eval",[CProp ("big_plus",[CVar 11, CVar 8, CVar 1]), CVar 1]),
|
|
CProp ("plus",[CProp ("power_eval",[CVar 11, CVar 1]), CVar 8])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("power_eval",
|
|
[CProp ("big_plus",[CVar 23, CVar 24, CVar 8, CVar 1]), CVar 1]),
|
|
CProp
|
|
("plus",
|
|
[CVar 8,
|
|
CProp
|
|
("plus",
|
|
[CProp ("power_eval",[CVar 23, CVar 1]),
|
|
CProp ("power_eval",[CVar 24, CVar 1])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("remainder",[CVar 24, CProp ("one",[])]), CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 24]),
|
|
CProp ("not",[CProp ("zerop",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",[CProp ("remainder",[CVar 23, CVar 23]), CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("lt",[CProp ("quotient",[CVar 8, CVar 9]), CVar 8]),
|
|
CProp
|
|
("and",
|
|
[CProp ("not",[CProp ("zerop",[CVar 8])]),
|
|
CProp
|
|
("or",
|
|
[CProp ("zerop",[CVar 9]),
|
|
CProp ("not",[CProp ("equal",[CVar 9, CProp ("one",[])])])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("lt",[CProp ("remainder",[CVar 23, CVar 24]), CVar 23]),
|
|
CProp
|
|
("and",
|
|
[CProp ("not",[CProp ("zerop",[CVar 24])]),
|
|
CProp ("not",[CProp ("zerop",[CVar 23])]),
|
|
CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("power_eval",[CProp ("power_rep",[CVar 8, CVar 1]), CVar 1]),
|
|
CProp ("fix",[CVar 8])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("power_eval",
|
|
[CProp
|
|
("big_plus",
|
|
[CProp ("power_rep",[CVar 8, CVar 1]),
|
|
CProp ("power_rep",[CVar 9, CVar 1]), CProp ("zero",[]),
|
|
CVar 1]),
|
|
CVar 1]),
|
|
CProp ("plus",[CVar 8, CVar 9])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("gcd",[CVar 23, CVar 24]), CProp ("gcd",[CVar 24, CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("nth",[CProp ("append",[CVar 0, CVar 1]), CVar 8]),
|
|
CProp
|
|
("append",
|
|
[CProp ("nth",[CVar 0, CVar 8]),
|
|
CProp
|
|
("nth",
|
|
[CVar 1, CProp ("difference",[CVar 8, CProp ("length",[CVar 0])])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("difference",[CProp ("plus",[CVar 23, CVar 24]), CVar 23]),
|
|
CProp ("fix",[CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("difference",[CProp ("plus",[CVar 24, CVar 23]), CVar 23]),
|
|
CProp ("fix",[CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("difference",
|
|
[CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
|
|
CProp ("difference",[CVar 24, CVar 25])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("times",[CVar 23, CProp ("difference",[CVar 2, CVar 22])]),
|
|
CProp
|
|
("difference",
|
|
[CProp ("times",[CVar 2, CVar 23]),
|
|
CProp ("times",[CVar 22, CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("remainder",[CProp ("times",[CVar 23, CVar 25]), CVar 25]),
|
|
CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("difference",
|
|
[CProp ("plus",[CVar 1, CProp ("plus",[CVar 0, CVar 2])]), CVar 0]),
|
|
CProp ("plus",[CVar 1, CVar 2])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("difference",
|
|
[CProp ("add1",[CProp ("plus",[CVar 24, CVar 25])]), CVar 25]),
|
|
CProp ("add1",[CVar 24])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("lt",
|
|
[CProp ("plus",[CVar 23, CVar 24]), CProp ("plus",[CVar 23, CVar 25])]),
|
|
CProp ("lt",[CVar 24, CVar 25])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("lt",
|
|
[CProp ("times",[CVar 23, CVar 25]),
|
|
CProp ("times",[CVar 24, CVar 25])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("not",[CProp ("zerop",[CVar 25])]),
|
|
CProp ("lt",[CVar 23, CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("lt",[CVar 24, CProp ("plus",[CVar 23, CVar 24])]),
|
|
CProp ("not",[CProp ("zerop",[CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("gcd",
|
|
[CProp ("times",[CVar 23, CVar 25]),
|
|
CProp ("times",[CVar 24, CVar 25])]),
|
|
CProp ("times",[CVar 25, CProp ("gcd",[CVar 23, CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("value",[CProp ("normalize",[CVar 23]), CVar 0]),
|
|
CProp ("value",[CVar 23, CVar 0])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("flatten",[CVar 23]),
|
|
CProp ("cons",[CVar 24, CProp ("nil",[])])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("nlistp",[CVar 23]), CProp ("equal",[CVar 23, CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("listp",[CProp ("gother",[CVar 23])]),
|
|
CProp ("listp",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("samefringe",[CVar 23, CVar 24]),
|
|
CProp
|
|
("equal",[CProp ("flatten",[CVar 23]), CProp ("flatten",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("zero",[])]),
|
|
CProp
|
|
("and",
|
|
[CProp
|
|
("or",
|
|
[CProp ("zerop",[CVar 24]),
|
|
CProp ("equal",[CVar 24, CProp ("one",[])])]),
|
|
CProp ("equal",[CVar 23, CProp ("zero",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("greatest_factor",[CVar 23, CVar 24]), CProp ("one",[])]),
|
|
CProp ("equal",[CVar 23, CProp ("one",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("numberp",[CProp ("greatest_factor",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("not",
|
|
[CProp
|
|
("and",
|
|
[CProp
|
|
("or",
|
|
[CProp ("zerop",[CVar 24]),
|
|
CProp ("equal",[CVar 24, CProp ("one",[])])]),
|
|
CProp ("not",[CProp ("numberp",[CVar 23])])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("times_list",[CProp ("append",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("times",
|
|
[CProp ("times_list",[CVar 23]), CProp ("times_list",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("prime_list",[CProp ("append",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("prime_list",[CVar 23]), CProp ("prime_list",[CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CVar 25, CProp ("times",[CVar 22, CVar 25])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("numberp",[CVar 25]),
|
|
CProp
|
|
("or",
|
|
[CProp ("equal",[CVar 25, CProp ("zero",[])]),
|
|
CProp ("equal",[CVar 22, CProp ("one",[])])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("ge",[CVar 23, CVar 24]),
|
|
CProp ("not",[CProp ("lt",[CVar 23, CVar 24])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CVar 23, CProp ("times",[CVar 23, CVar 24])]),
|
|
CProp
|
|
("or",
|
|
[CProp ("equal",[CVar 23, CProp ("zero",[])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("numberp",[CVar 23]),
|
|
CProp ("equal",[CVar 24, CProp ("one",[])])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("remainder",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
|
|
CProp ("zero",[])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CProp ("times",[CVar 0, CVar 1]), CProp ("one",[])]),
|
|
CProp
|
|
("and",
|
|
[CProp ("not",[CProp ("equal",[CVar 0, CProp ("zero",[])])]),
|
|
CProp ("not",[CProp ("equal",[CVar 1, CProp ("zero",[])])]),
|
|
CProp ("numberp",[CVar 0]), CProp ("numberp",[CVar 1]),
|
|
CProp ("equal",[CProp ("sub1",[CVar 0]), CProp ("zero",[])]),
|
|
CProp ("equal",[CProp ("sub1",[CVar 1]), CProp ("zero",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("lt",
|
|
[CProp ("length",[CProp ("delete",[CVar 23, CVar 11])]),
|
|
CProp ("length",[CVar 11])]),
|
|
CProp ("member",[CVar 23, CVar 11])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("sort2",[CProp ("delete",[CVar 23, CVar 11])]),
|
|
CProp ("delete",[CVar 23, CProp ("sort2",[CVar 11])])]));
|
|
add (CProp ("equal",[CProp ("dsort",[CVar 23]), CProp ("sort2",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("length",
|
|
[CProp
|
|
("cons",
|
|
[CVar 0,
|
|
CProp
|
|
("cons",
|
|
[CVar 1,
|
|
CProp
|
|
("cons",
|
|
[CVar 2,
|
|
CProp
|
|
("cons",
|
|
[CVar 3,
|
|
CProp ("cons",[CVar 4, CProp ("cons",[CVar 5, CVar 6])])])])])])])
|
|
, CProp ("plus",[CProp ("six",[]), CProp ("length",[CVar 6])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("difference",
|
|
[CProp ("add1",[CProp ("add1",[CVar 23])]), CProp ("two",[])]),
|
|
CProp ("fix",[CVar 23])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("quotient",
|
|
[CProp ("plus",[CVar 23, CProp ("plus",[CVar 23, CVar 24])]),
|
|
CProp ("two",[])]),
|
|
CProp
|
|
("plus",[CVar 23, CProp ("quotient",[CVar 24, CProp ("two",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("sigma",[CProp ("zero",[]), CVar 8]),
|
|
CProp
|
|
("quotient",
|
|
[CProp ("times",[CVar 8, CProp ("add1",[CVar 8])]), CProp ("two",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("plus",[CVar 23, CProp ("add1",[CVar 24])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("numberp",[CVar 24]),
|
|
CProp ("add1",[CProp ("plus",[CVar 23, CVar 24])]),
|
|
CProp ("add1",[CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("equal",
|
|
[CProp ("difference",[CVar 23, CVar 24]),
|
|
CProp ("difference",[CVar 25, CVar 24])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("lt",[CVar 23, CVar 24]),
|
|
CProp ("not",[CProp ("lt",[CVar 24, CVar 25])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("lt",[CVar 25, CVar 24]),
|
|
CProp ("not",[CProp ("lt",[CVar 24, CVar 23])]),
|
|
CProp ("equal",[CProp ("fix",[CVar 23]), CProp ("fix",[CVar 25])])])])])
|
|
);
|
|
add (CProp
|
|
("equal",
|
|
[CProp
|
|
("meaning",
|
|
[CProp ("plus_tree",[CProp ("delete",[CVar 23, CVar 24])]), CVar 0]),
|
|
CProp
|
|
("if",
|
|
[CProp ("member",[CVar 23, CVar 24]),
|
|
CProp
|
|
("difference",
|
|
[CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0]),
|
|
CProp ("meaning",[CVar 23, CVar 0])]),
|
|
CProp ("meaning",[CProp ("plus_tree",[CVar 24]), CVar 0])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("times",[CVar 23, CProp ("add1",[CVar 24])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("numberp",[CVar 24]),
|
|
CProp
|
|
("plus",
|
|
[CVar 23, CProp ("times",[CVar 23, CVar 24]),
|
|
CProp ("fix",[CVar 23])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("nth",[CProp ("nil",[]), CVar 8]),
|
|
CProp
|
|
("if",[CProp ("zerop",[CVar 8]), CProp ("nil",[]), CProp ("zero",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("last",[CProp ("append",[CVar 0, CVar 1])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("listp",[CVar 1]), CProp ("last",[CVar 1]),
|
|
CProp
|
|
("if",
|
|
[CProp ("listp",[CVar 0]),
|
|
CProp ("cons",[CProp ("car",[CProp ("last",[CVar 0])]), CVar 1]),
|
|
CVar 1])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("equal",[CProp ("lt",[CVar 23, CVar 24]), CVar 25]),
|
|
CProp
|
|
("if",
|
|
[CProp ("lt",[CVar 23, CVar 24]),
|
|
CProp ("equal",[CProp ("true",[]), CVar 25]),
|
|
CProp ("equal",[CProp ("false",[]), CVar 25])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("assignment",[CVar 23, CProp ("append",[CVar 0, CVar 1])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("assignedp",[CVar 23, CVar 0]),
|
|
CProp ("assignment",[CVar 23, CVar 0]),
|
|
CProp ("assignment",[CVar 23, CVar 1])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("car",[CProp ("gother",[CVar 23])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("listp",[CVar 23]),
|
|
CProp ("car",[CProp ("flatten",[CVar 23])]), CProp ("zero",[])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("flatten",[CProp ("cdr",[CProp ("gother",[CVar 23])])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("listp",[CVar 23]),
|
|
CProp ("cdr",[CProp ("flatten",[CVar 23])]),
|
|
CProp ("cons",[CProp ("zero",[]), CProp ("nil",[])])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("quotient",[CProp ("times",[CVar 24, CVar 23]), CVar 24]),
|
|
CProp
|
|
("if",
|
|
[CProp ("zerop",[CVar 24]), CProp ("zero",[]),
|
|
CProp ("fix",[CVar 23])])]));
|
|
add (CProp
|
|
("equal",
|
|
[CProp ("get",[CVar 9, CProp ("set",[CVar 8, CVar 21, CVar 12])]),
|
|
CProp
|
|
("if",
|
|
[CProp ("eqp",[CVar 9, CVar 8]), CVar 21,
|
|
CProp ("get",[CVar 9, CVar 12])])])))
|
|
|
|
end; (* Rules *)
|
|
|
|
(* boyer.sml:
|
|
*
|
|
* Tautology checker
|
|
*)
|
|
|
|
signature BOYER =
|
|
sig
|
|
include TERMS
|
|
val tautp: term -> bool
|
|
end
|
|
|
|
structure Boyer: BOYER =
|
|
struct
|
|
|
|
open Terms
|
|
|
|
fun mem x [] = false
|
|
| mem x (y::L) = x=y orelse mem x L
|
|
|
|
fun truep (x, lst) =
|
|
case x of
|
|
Prop(head, _) =>
|
|
headname head = "true" orelse mem x lst
|
|
| _ =>
|
|
mem x lst
|
|
|
|
and falsep (x, lst) =
|
|
case x of
|
|
Prop(head, _) =>
|
|
headname head = "false" orelse mem x lst
|
|
| _ =>
|
|
mem x lst
|
|
|
|
fun tautologyp (x, true_lst, false_lst) =
|
|
if truep (x, true_lst) then true else
|
|
if falsep (x, false_lst) then false else
|
|
(case x of
|
|
Var _ => false
|
|
| Prop (head,[test, yes, no]) =>
|
|
if headname head = "if" then
|
|
if truep (test, true_lst) then
|
|
tautologyp (yes, true_lst, false_lst)
|
|
else if falsep (test, false_lst) then
|
|
tautologyp (no, true_lst, false_lst)
|
|
else tautologyp (yes, test::true_lst, false_lst) andalso
|
|
tautologyp (no, true_lst, test::false_lst)
|
|
else
|
|
false)
|
|
|
|
fun tautp x = tautologyp(rewrite x, [], []);
|
|
|
|
end; (* Boyer *)
|
|
|
|
signature BMARK =
|
|
sig
|
|
val doit : unit -> unit
|
|
val testit : TextIO.outstream -> unit
|
|
end;
|
|
|
|
(* the benchmark *)
|
|
structure Main : BMARK =
|
|
struct
|
|
|
|
open Terms;
|
|
open Boyer;
|
|
|
|
val subst =
|
|
[Bind(23,
|
|
Prop
|
|
(get "f",
|
|
[Prop
|
|
(get "plus",
|
|
[Prop (get "plus",[Var 0, Var 1]),
|
|
Prop (get "plus",[Var 2, Prop (get "zero",[])])])])),
|
|
Bind(24,
|
|
Prop
|
|
(get "f",
|
|
[Prop
|
|
(get "times",
|
|
[Prop (get "times",[Var 0, Var 1]),
|
|
Prop (get "plus",[Var 2, Var 3])])])),
|
|
Bind(25,
|
|
Prop
|
|
(get "f",
|
|
[Prop
|
|
(get "reverse",
|
|
[Prop
|
|
(get "append",
|
|
[Prop (get "append",[Var 0, Var 1]),
|
|
Prop (get "nil",[])])])])),
|
|
Bind(20,
|
|
Prop
|
|
(get "equal",
|
|
[Prop (get "plus",[Var 0, Var 1]),
|
|
Prop (get "difference",[Var 23, Var 24])])),
|
|
Bind(22,
|
|
Prop
|
|
(get "lt",
|
|
[Prop (get "remainder",[Var 0, Var 1]),
|
|
Prop (get "member",[Var 0, Prop (get "length",[Var 1])])]))]
|
|
|
|
val term =
|
|
Prop
|
|
(get "implies",
|
|
[Prop
|
|
(get "and",
|
|
[Prop (get "implies",[Var 23, Var 24]),
|
|
Prop
|
|
(get "and",
|
|
[Prop (get "implies",[Var 24, Var 25]),
|
|
Prop
|
|
(get "and",
|
|
[Prop (get "implies",[Var 25, Var 20]),
|
|
Prop (get "implies",[Var 20, Var 22])])])]),
|
|
Prop (get "implies",[Var 23, Var 22])])
|
|
|
|
fun testit outstrm = if tautp (apply_subst subst term)
|
|
then TextIO.output (outstrm, "Proved!\n")
|
|
else TextIO.output (outstrm, "Cannot prove!\n")
|
|
|
|
fun doit () = (tautp (apply_subst subst term); ())
|
|
|
|
end; (* Main *)
|
|
|
|
fun smlboyer_benchmark (n : int) =
|
|
run_benchmark ("smlboyer",
|
|
n,
|
|
Main.doit,
|
|
fn (result) => true)
|
|
|
|
fun main () = smlboyer_benchmark (smlboyer_iters)
|