OKlibrary  0.2.1.6
ConstraintTemplateRewriteSystem.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.9.2010 (Swansea) */
00002 /* Copyright 2010, 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00023 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00024 
00025 kill(f)$
00026 
00027 /* ********************************************
00028    * Rewrite system functions                 *
00029    ********************************************
00030 */
00031 
00032 okltest_cstt_namespace_new(f) := block(
00033   assert(
00034     f(lambda([[a]],a),["",[],[],cstt_id_ns])(0) = [0,["",[],cstt_id_ns]]),
00035   assert(f(nounify(f),["",[],[],cstt_id_ns])(0) = nounify(f)(0,["",[],cstt_id_ns])),
00036   assert(f(lambda([[a]],a),["",[],[],nounify(f1)])(0) = nounify(f1)([0,["",[],nounify(f1)]])),
00037   assert(f(nounify(f2),["",[],[],nounify(f1)])(0) = nounify(f1)(nounify(f2)(0,["",[],nounify(f1)]))),
00038   assert(f(nounify(f2),[1,[],[],nounify(f1)])(0) =
00039     nounify(f1)(nounify(f2)(0,[1,[],nounify(f1)]))),
00040   true)$
00041 
00042 okltest_cstt_namespace_replace(f) := block(
00043   assert(f([1,2,'m],'n)  = [1,2,'n]),
00044   true)$
00045 
00046 /****************************
00047  * Constraints              *
00048  ****************************
00049 */
00050 
00051 okltest_cstt_new(f) := block(
00052   assert(f("f",[],[], cstt_id_ns) = ["f",[],cstt_id_ns]),
00053   for i : 0 thru 5 do
00054     assert(f("f",[i],[],cstt_id_ns) = ["f",[i],cstt_id_ns]),
00055   for i : 0 thru 5 do
00056     assert(f("f",[],[i],cstt_id_ns) = ["f",[],i,cstt_id_ns]),
00057   assert(f("f", [1,2,3],[],'n) = ["f",[1,2,3],'n]),
00058   assert(f("f", [1,2],[3,4],'n) = ["f",[1,2],3,4,'n]),
00059   true)$
00060 
00061 okltest_cstt_name(f) := block(
00062   assert(f([""]) = ""),
00063   assert(f(["test"]) = "test"),
00064   assert(f(["test1","test2"]) = "test1"),
00065   true)$
00066 
00067 okltest_cstt_vars_l(f) := block(
00068   assert(f([]) = []),
00069   assert(f([1]) = []),
00070   assert(f(["",[]]) = []),
00071   assert(f(["",""]) = []),
00072   assert(f(["",['a,'b]]) = ['a,'b]),
00073   true)$
00074 
00075 okltest_cstt_args_l(f) := block(
00076   assert(f([]) = []),
00077   assert(f([1,2]) = []),
00078   assert(f(["",[]]) = []),
00079   assert(f(["","",""]) = []),
00080   assert(f(["",[],'a,'b,f]) = ['a,'b]),
00081   true)$
00082 
00083 okltest_cstt_namespace_f(f) := block(
00084   assert(f([])(0) = 0),
00085   assert(f([1,2])(0) = 0),
00086   assert(f([1,2,3])(0) = 0),
00087   assert(f(["",[]])(0) = 0),
00088   assert(f(["","",""])(0) = 0),
00089   assert(f(["",[],['a,'b],lambda([a],2)])(0) = 2),
00090   true)$
00091 
00092 okltest_cstt_p(f) := block(
00093   assert(not(f([]))),
00094   assert(not(f([[]]))),
00095   assert(not(f(["test"]))),
00096   assert(f(["test",[]])),
00097   true)$
00098 
00099 okltest_cstt_named_p(f) := block(
00100   assert(not(f([],""))),
00101   assert(not(f([[]],""))),
00102   assert(not(f(["test"],""))),
00103   assert(not(f(["test",[]],"test2"))),
00104   assert(f(["test",[]],"test")),
00105   true)$
00106 
00107 /********************************
00108  * Rewrite functions            *
00109  ********************************
00110 */
00111 
00112 okltest_rewrite_all_csttl(f) := block([test_ctrb],
00113   assert(f([],[]) = []),
00114   assert(f([["f",[],'n],["g",[],'m]],[]) = [["g",[],'m],["f",[],'n]]),
00115   test_ctrb : [lambda([a],[["f1", a[2],a[3]]]),
00116                lambda([a],a),cstt_id_ns],
00117   assert(f([["x",[1,2,3],'n]], [["x",test_ctrb]]) =
00118     [["f1",[1,2,3],'n]]),
00119   true)$
00120 
00121 okltest_rewrite_all_cstt_vars_l(f) := block([test_ctrb,cst_t],
00122   assert(f([],[]) = []),
00123   assert(f([["f",[],'n],["g",[],'m]],[]) = []),
00124   test_ctrb : [lambda([a],[["f1", a[2],a[3]]]),
00125                lambda([a],a),lambda([a],
00126                  if a = cst_t then [1] else assert(false))],
00127   cst_t : ["x",[1,2,3],'n],
00128   assert(f([cst_t], [["x",test_ctrb]]) =
00129     [1]),  
00130   true)$
00131 
00132