diff options
Diffstat (limited to 'ocaml-binary-annot/testsuite/tests/misc/boyer.ml')
| -rw-r--r-- | ocaml-binary-annot/testsuite/tests/misc/boyer.ml | 911 |
1 files changed, 911 insertions, 0 deletions
diff --git a/ocaml-binary-annot/testsuite/tests/misc/boyer.ml b/ocaml-binary-annot/testsuite/tests/misc/boyer.ml new file mode 100644 index 0000000000..c2c7689618 --- /dev/null +++ b/ocaml-binary-annot/testsuite/tests/misc/boyer.ml @@ -0,0 +1,911 @@ +(***********************************************************************) +(* *) +(* Objective Caml *) +(* *) +(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) +(* *) +(* Copyright 1996 Institut National de Recherche en Informatique et *) +(* en Automatique. All rights reserved. This file is distributed *) +(* under the terms of the Q Public License version 1.0. *) +(* *) +(***********************************************************************) + +(* $Id: boyer.ml 7017 2005-08-12 09:22:04Z xleroy $ *) + +(* Manipulations over terms *) + +type term = + Var of int + | Prop of head * term list +and head = + { name: string; + mutable props: (term * term) list } + +let rec print_term = function + Var v -> + print_string "v"; print_int v + | Prop (head,argl) -> + print_string "("; + print_string head.name; + List.iter (fun t -> print_string " "; print_term t) argl; + print_string ")" + +let lemmas = ref ([] : head list) + +(* Replacement for property lists *) + +let get name = + let rec get_rec = function + hd1::hdl -> + if hd1.name = name then hd1 else get_rec hdl + | [] -> + let entry = {name = name; props = []} in + lemmas := entry :: !lemmas; + entry + in get_rec !lemmas + +let add_lemma = function + | Prop(_, [(Prop(headl,_) as left); right]) -> + headl.props <- (left, right) :: headl.props + | _ -> assert false + +(* Substitutions *) + +type subst = Bind of int * term + +let get_binding v list = + let rec get_rec = function + [] -> failwith "unbound" + | Bind(w,t)::rest -> if v = w then t else get_rec rest + in get_rec list + +let apply_subst alist term = + let rec as_rec = function + Var v -> begin try get_binding v alist with Failure _ -> term end + | Prop (head,argl) -> Prop (head, List.map as_rec argl) + in as_rec term + +exception Unify + +let rec unify term1 term2 = + unify1 term1 term2 [] + +and unify1 term1 term2 unify_subst = + match term2 with + Var v -> + begin try + if get_binding v unify_subst = term1 + then unify_subst + else raise Unify + with Failure _ -> + Bind(v,term1) :: unify_subst + end + | Prop (head2, argl2) -> + match term1 with + Var _ -> raise Unify + | Prop (head1,argl1) -> + if head1 == head2 + then unify1_lst argl1 argl2 unify_subst + else raise Unify + +and unify1_lst l1 l2 unify_subst = + match (l1, l2) with + ([], []) -> unify_subst + | (h1::r1, h2::r2) -> unify1_lst r1 r2 (unify1 h1 h2 unify_subst) + | _ -> raise Unify + + +let rec rewrite = function + Var _ as term -> term + | Prop (head, argl) -> + rewrite_with_lemmas (Prop (head, List.map rewrite argl)) head.props +and rewrite_with_lemmas term lemmas = + match lemmas with + [] -> + term + | (t1,t2)::rest -> + try + rewrite (apply_subst (unify term t1) t2) + with Unify -> + rewrite_with_lemmas term rest + +type cterm = CVar of int | CProp of string * cterm list + +let rec cterm_to_term = function + CVar v -> Var v + | CProp(p, l) -> Prop(get p, List.map cterm_to_term l) + +let add t = add_lemma (cterm_to_term t) + +let _ = +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])])])) + +(* Tautology checker *) + +let truep x lst = + match x with + Prop(head, _) -> + head.name = "true" || List.mem x lst + | _ -> + List.mem x lst + +and falsep x lst = + match x with + Prop(head, _) -> + head.name = "false" || List.mem x lst + | _ -> + List.mem x lst + + +let rec tautologyp x true_lst false_lst = + if truep x true_lst then true else + if falsep x false_lst then false else begin +(* + print_term x; print_newline(); +*) + match x with + Var _ -> false + | Prop (head,[test; yes; no]) -> + if head.name = "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 && + tautologyp no true_lst (test::false_lst) + else + false + | _ -> assert false + end + + +let tautp x = +(* print_term x; print_string"\n"; *) + let y = rewrite x in +(* print_term y; print_string "\n"; *) + tautologyp y [] [] + +(* the benchmark *) + +let subst = +[Bind(23, cterm_to_term( + CProp + ("f", + [CProp + ("plus", + [CProp ("plus",[CVar 0; CVar 1]); + CProp ("plus",[CVar 2; CProp ("zero",[])])])]))); + Bind(24, cterm_to_term( + CProp + ("f", + [CProp + ("times", + [CProp ("times",[CVar 0; CVar 1]); + CProp ("plus",[CVar 2; CVar 3])])]))); + Bind(25, cterm_to_term( + CProp + ("f", + [CProp + ("reverse", + [CProp + ("append", + [CProp ("append",[CVar 0; CVar 1]); + CProp ("nil",[])])])]))); + Bind(20, cterm_to_term( + CProp + ("equal", + [CProp ("plus",[CVar 0; CVar 1]); + CProp ("difference",[CVar 23; CVar 24])]))); + Bind(22, cterm_to_term( + CProp + ("lt", + [CProp ("remainder",[CVar 0; CVar 1]); + CProp ("member",[CVar 0; CProp ("length",[CVar 1])])])))] + +let term = cterm_to_term( + CProp + ("implies", + [CProp + ("and", + [CProp ("implies",[CVar 23; CVar 24]); + CProp + ("and", + [CProp ("implies",[CVar 24; CVar 25]); + CProp + ("and", + [CProp ("implies",[CVar 25; CVar 20]); + CProp ("implies",[CVar 20; CVar 22])])])]); + CProp ("implies",[CVar 23; CVar 22])])) + +let _ = + let ok = ref true in + for i = 1 to 50 do + if not (tautp (apply_subst subst term)) then ok := false + done; + if !ok then + print_string "Proved!\n" + else + print_string "Cannot prove!\n"; + exit 0 + +(********* +with + failure s -> + print_string "Exception failure("; print_string s; print_string ")\n" + | Unify -> + print_string "Exception Unify\n" + | match_failure(file,start,stop) -> + print_string "Exception match_failure("; + print_string file; + print_string ","; + print_int start; + print_string ","; + print_int stop; + print_string ")\n" + | _ -> + print_string "Exception ?\n" + +**********) |