From: Michael N. <mic...@us...> - 2006-02-22 04:37:22
|
Update of /cvsroot/hol/hol98/src/integer In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv546/integer Modified Files: Holmakefile intSimps.sig intSimps.sml selftest.sml Log Message: Fix a bug in the normaliser, instantiate it for the integers, and list some tests for the integer instantiation. Index: Holmakefile =================================================================== RCS file: /cvsroot/hol/hol98/src/integer/Holmakefile,v retrieving revision 1.3 retrieving revision 1.4 diff -b -C2 -d -r1.3 -r1.4 *** Holmakefile 31 Oct 2003 04:53:36 -0000 1.3 --- Holmakefile 22 Feb 2006 04:37:12 -0000 1.4 *************** *** 1,4 **** EXTRA_CLEANS = selftest.exe ! selftest.exe: selftest.sml $(HOLMOSMLC) -o $@ $< --- 1,4 ---- EXTRA_CLEANS = selftest.exe ! selftest.exe: selftest.uo $(HOLMOSMLC) -o $@ $< Index: intSimps.sig =================================================================== RCS file: /cvsroot/hol/hol98/src/integer/intSimps.sig,v retrieving revision 1.8 retrieving revision 1.9 diff -b -C2 -d -r1.8 -r1.9 *** intSimps.sig 13 Jul 2005 01:42:08 -0000 1.8 --- intSimps.sig 22 Feb 2006 04:37:12 -0000 1.9 *************** *** 24,26 **** --- 24,33 ---- fails if there is no collecting to be done *) + val ADDL_CANON_CONV : term -> thm + (* collects up all terms, summing coefficients. Does more than + collect_additive_consts therefore. Left-associates. *) + val ADDR_CANON_CONV : term -> thm + (* collects up all terms, summing coefficients. Does more than + collect_additive_consts therefore. Right-associates. *) + end; Index: intSimps.sml =================================================================== RCS file: /cvsroot/hol/hol98/src/integer/intSimps.sml,v retrieving revision 1.20 retrieving revision 1.21 diff -b -C2 -d -r1.20 -r1.21 *** intSimps.sml 13 Jul 2005 01:42:08 -0000 1.20 --- intSimps.sml 22 Feb 2006 04:37:12 -0000 1.21 *************** *** 88,95 **** val _ = BasicProvers.augment_srw_ss [INT_REDUCE_ss]; ! (*---------------------------------------------------------------------------*) ! (* Accumulate literal additions in integer expressions *) ! (*---------------------------------------------------------------------------*) fun collect_additive_consts tm = let val summands = strip_plus tm --- 88,99 ---- val _ = BasicProvers.augment_srw_ss [INT_REDUCE_ss]; ! (* ---------------------------------------------------------------------- ! integer normalisations ! ---------------------------------------------------------------------- *) + (* Accumulate literal additions in integer expressions + (doesn't do coefficient gathering - just adds up literals, and + reassociates along the way) + *) fun collect_additive_consts tm = let val summands = strip_plus tm *************** *** 117,120 **** --- 121,175 ---- end + local + open intSyntax integerTheory GenPolyCanon + val assoc = INT_ADD_ASSOC + val comm = INT_ADD_COMM + fun is_good t = let + val (l,r) = dest_mult t + in + is_int_literal l + end handle HOL_ERR _ => false + fun non_coeff t = if is_good t then rand t + else if is_negated t then rand t + else t + fun add_coeff t = + if is_good t then ALL_CONV t + else if is_negated t then REWR_CONV INT_NEG_MINUS1 t + else REWR_CONV (GSYM INT_MUL_LID) t + val distrib = GSYM INT_RDISTRIB + fun merge t = let + val (l,r) = dest_plus t + in + if is_int_literal l andalso is_int_literal r then + REDUCE_CONV + else BINOP_CONV add_coeff THENC + REWR_CONV distrib THENC + LAND_CONV REDUCE_CONV + end t + in + val lintadd_gci = + GCI { dest = dest_plus, + assoc_mode = L, + is_literal = is_int_literal, + assoc = assoc, + symassoc = GSYM assoc, + comm = comm, + l_asscomm = derive_l_asscomm assoc comm, + r_asscomm = derive_r_asscomm assoc comm, + non_coeff = non_coeff, + merge = merge, + postnorm = REWR_CONV INT_MUL_LZERO ORELSEC + REWR_CONV INT_MUL_LID ORELSEC + TRY_CONV (REWR_CONV (GSYM INT_NEG_MINUS1)), + left_id = INT_ADD_LID, + right_id = INT_ADD_RID, + reducer = REDUCE_CONV } + val rintadd_gci = update_mode R lintadd_gci + val ADDL_CANON_CONV = gencanon lintadd_gci + val ADDR_CANON_CONV = gencanon rintadd_gci + end + + + (*---------------------------------------------------------------------------*) (* Support for ordered AC rewriting *) Index: selftest.sml =================================================================== RCS file: /cvsroot/hol/hol98/src/integer/selftest.sml,v retrieving revision 1.4 retrieving revision 1.5 diff -b -C2 -d -r1.4 -r1.5 *** selftest.sml 29 Jul 2004 09:44:09 -0000 1.4 --- selftest.sml 22 Feb 2006 04:37:12 -0000 1.5 *************** *** 1,4 **** --- 1,37 ---- + structure selftest = + struct + + open HolKernel boolLib Parse + + structure Parse = + struct + open Parse + val (Type,Term) = parse_from_grammars integerTheory.integer_grammars + end + open Parse + fun die s = (print (s^"\n"); Process.exit Process.failure) + val _ = print "Testing normalisers\n" + fun test (s, f, orig, answer) = let + val result = QCONV f orig + in + print (StringCvt.padRight #" " 60 (s ^ " " ^ term_to_string orig)); + if aconv (rhs (concl result)) answer then print "OK\n" + else die "FAILED!\n" + end + val _ = let + open intSimps + val AL = ADDL_CANON_CONV + val AR = ADDR_CANON_CONV + in + app test + [("ADDL_CANON_CONV", AL, ``~3 + ~y + x + x + 4``, ``2 * x + ~y + 1``), + ("ADDL_CANON_CONV", AL, ``~3 + ~y + x + x + 4 + y``, ``2 * x + 1``), + ("ADDR_CANON_CONV", AR, ``~3 + ~y + x + x + 4``, ``2 * x + (~y + 1)``), + ("ADDR_CANON_CONV", AR, ``~3 + ~y + x + x + 4 + y``, ``2 * x + 1``)] + end + + val progs = ["test_omega.exe", "test_coopers.exe"] *************** *** 37,38 **** --- 70,72 ---- val _ = Process.exit (if List.all run progs then Process.success else Process.failure) + end; (* struct *) \ No newline at end of file |