[Hol-checkins] CVS: hol98/src/integer Holmakefile,1.3,1.4 intSimps.sig,1.8,1.9 intSimps.sml,1.20,1.21 selftest.sml,1.4,1.5

[Michael N. <mic...@us...>]

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