Browse files

Conversion to add NUMERAL to numeric literals

Applied (with CONV_RULE) to all theorems resulting from reading an
OpenTheory article. Articles don't have to (and probably won't) use
HOL4's NUMERAL tag on their literals, but many HOL4 tactics and rewrites
exploit it.

 - Definitions can still end up without tags, since they are byproducts
   of defining constants and not actually part of an article's exports
   (but usually there would be an exported theorem corresponding to each
   definition, which will get tags added).
 - Hypotheses won't be treated (just because CONV_RULE doesn't do that;
   a hyp+concl-affecting rule could be used instead).
 - In future it would be good to support more variations on numerals,
   for example by translating binary numerals to Norrish numerals.
   Currently I think reading binary numerals will fail because there's
   no mapping for Number.Numeral.bit0.
  • Loading branch information...
xrchz committed Feb 10, 2012
1 parent 6a36264 commit eebb1d062b5c98147fd23eda5f6fae7279b24d85
Showing with 36 additions and 1 deletion.
  1. +3 −0 src/opentheory/Opentheory.sig
  2. +33 −1 src/opentheory/Opentheory.sml
@@ -68,4 +68,7 @@ Given a list (usually by calling [Net.listItems] on the result of
[read_article]), calls [Theory.delete_const] on any constants in the current
theory that do not appear in some theorem in the list.
+val NUMERAL_conv : Conv.conv
@@ -63,6 +63,35 @@ in
+(* useful elsewhere? *)
+val NUMERAL_conv = let (* wrap numeric literals in NUMERAL tag *)
+ open Conv numSyntax arithmeticTheory
+ exception Nonlit
+ fun lit_conv tm = let (* detect literals, and replace 0 by ZERO *)
+ val (f,_) = dest_comb tm in
+ if f = bit1_tm orelse f = bit2_tm then
+ RAND_CONV lit_conv tm
+ else raise Nonlit
+ end handle HOL_ERR _ =>
+ if tm = zero_tm then SYM ALT_ZERO else
+ if tm = alt_zero_tm then raise UNCHANGED else
+ raise Nonlit
+ fun add_tag_conv tm = SYM (SPEC tm NUMERAL_DEF)
+ fun conv tm = let
+ val (f,_) = dest_comb tm in
+ if f = bit1_tm orelse f = bit2_tm then
+ (RAND_CONV lit_conv THENC add_tag_conv) tm
+ handle Nonlit => RAND_CONV conv tm
+ else if f = numeral_tm then
+ raise UNCHANGED (* nb: assuming incoming NUMERAL tags are good *)
+ (* alternative: check if it's actually a literal with lit_conv, and
+ strip the tag if Nonlit is raised *)
+ else COMB_CONV conv tm
+ end handle HOL_ERR _ => ABS_CONV conv tm
+ handle HOL_ERR _ =>
+ if tm = alt_zero_tm then ALT_ZERO else raise UNCHANGED
+in conv end
fun eq (h,c) th =
aconv (concl th) c andalso
@@ -209,7 +238,10 @@ fun raw_read_article input
| SOME line => let
val {stack,dict,thms} = f (trimr line) x
in loop {stack=stack,dict=dict,thms=thms,line_num=line_num+1} end
-in #thms (loop {stack=[],dict=Map.mkDict(,thms=Net.empty,line_num=1}) end
+ (#thms (loop {stack=[],dict=Map.mkDict(,thms=Net.empty,line_num=1}))
fun read_article s r = raw_read_article (TextIO.openIn s) r

0 comments on commit eebb1d0

Please sign in to comment.