--- a/NEWS Mon Jan 16 20:32:33 2012 +0100
+++ b/NEWS Mon Jan 16 21:50:15 2012 +0100
@@ -26,7 +26,8 @@
* Renamed inner syntax categories "num" to "num_token" and "xnum" to
"xnum_token", in accordance to existing "float_token". Minor
INCOMPATIBILITY. Note that in practice "num_const" etc. are mainly
-used instead.
+used instead (which also include position information via
+constraints).
*** Pure ***
--- a/src/HOL/Library/Numeral_Type.thy Mon Jan 16 20:32:33 2012 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Mon Jan 16 21:50:15 2012 +0100
@@ -296,7 +296,7 @@
subsection {* Syntax *}
syntax
- "_NumeralType" :: "num_const => type" ("_")
+ "_NumeralType" :: "num_token => type" ("_")
"_NumeralType0" :: type ("0")
"_NumeralType1" :: type ("1")
@@ -306,46 +306,45 @@
parse_translation {*
let
-fun mk_bintype n =
- let
- fun mk_bit 0 = Syntax.const @{type_syntax bit0}
- | mk_bit 1 = Syntax.const @{type_syntax bit1};
- fun bin_of n =
- if n = 1 then Syntax.const @{type_syntax num1}
- else if n = 0 then Syntax.const @{type_syntax num0}
- else if n = ~1 then raise TERM ("negative type numeral", [])
- else
- let val (q, r) = Integer.div_mod n 2;
- in mk_bit r $ bin_of q end;
- in bin_of n end;
+ fun mk_bintype n =
+ let
+ fun mk_bit 0 = Syntax.const @{type_syntax bit0}
+ | mk_bit 1 = Syntax.const @{type_syntax bit1};
+ fun bin_of n =
+ if n = 1 then Syntax.const @{type_syntax num1}
+ else if n = 0 then Syntax.const @{type_syntax num0}
+ else if n = ~1 then raise TERM ("negative type numeral", [])
+ else
+ let val (q, r) = Integer.div_mod n 2;
+ in mk_bit r $ bin_of q end;
+ in bin_of n end;
-fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
- mk_bintype (the (Int.fromString str))
- | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
+ fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
+ | numeral_tr ts = raise TERM ("numeral_tr", ts);
in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
*}
print_translation {*
let
-fun int_of [] = 0
- | int_of (b :: bs) = b + 2 * int_of bs;
+ fun int_of [] = 0
+ | int_of (b :: bs) = b + 2 * int_of bs;
-fun bin_of (Const (@{type_syntax num0}, _)) = []
- | bin_of (Const (@{type_syntax num1}, _)) = [1]
- | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
- | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
- | bin_of t = raise TERM ("bin_of", [t]);
+ fun bin_of (Const (@{type_syntax num0}, _)) = []
+ | bin_of (Const (@{type_syntax num1}, _)) = [1]
+ | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
+ | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
+ | bin_of t = raise TERM ("bin_of", [t]);
-fun bit_tr' b [t] =
- let
- val rev_digs = b :: bin_of t handle TERM _ => raise Match
- val i = int_of rev_digs;
- val num = string_of_int (abs i);
- in
- Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
- end
- | bit_tr' b _ = raise Match;
+ fun bit_tr' b [t] =
+ let
+ val rev_digs = b :: bin_of t handle TERM _ => raise Match
+ val i = int_of rev_digs;
+ val num = string_of_int (abs i);
+ in
+ Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
+ end
+ | bit_tr' b _ = raise Match;
in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
*}
--- a/src/HOL/Tools/float_syntax.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/HOL/Tools/float_syntax.ML Mon Jan 16 21:50:15 2012 +0100
@@ -35,8 +35,9 @@
in
-fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
- | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
+fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
+ | float_tr [t as Const (str, _)] = mk_frac str
+ | float_tr ts = raise TERM ("float_tr", ts);
end;
--- a/src/HOL/Tools/numeral_syntax.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Mon Jan 16 21:50:15 2012 +0100
@@ -26,9 +26,9 @@
in
-fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
- Syntax.const @{const_syntax Int.number_of} $ mk_bin num
- | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
+fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u
+ | numeral_tr [t as Const (num, _)] = Syntax.const @{const_syntax Int.number_of} $ mk_bin num
+ | numeral_tr ts = raise TERM ("numeral_tr", ts);
end;
--- a/src/HOL/ex/Binary.thy Mon Jan 16 20:32:33 2012 +0100
+++ b/src/HOL/ex/Binary.thy Mon Jan 16 21:50:15 2012 +0100
@@ -193,7 +193,8 @@
val syntax_consts =
map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
- fun binary_tr [Const (num, _)] =
+ fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
+ | binary_tr [Const (num, _)] =
let
val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
--- a/src/Pure/Syntax/syntax.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Jan 16 21:50:15 2012 +0100
@@ -542,8 +542,9 @@
val basic_nonterms =
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
- "any", "prop'", "num_const", "float_const", "xnum_const", "index", "struct",
- "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
+ "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
+ "float_position", "xnum_position", "index", "struct", "id_position",
+ "longid_position", "xstr_position", "type_name", "class_name"]);
--- a/src/Pure/Syntax/syntax_trans.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Mon Jan 16 21:50:15 2012 +0100
@@ -93,7 +93,9 @@
(* constify *)
-fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
+fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
+ Ast.Appl [c, constify_ast_tr [ast1], ast2]
+ | constify_ast_tr [Ast.Variable c] = Ast.Constant c
| constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
--- a/src/Pure/pure_thy.ML Mon Jan 16 20:32:33 2012 +0100
+++ b/src/Pure/pure_thy.ML Mon Jan 16 21:50:15 2012 +0100
@@ -125,9 +125,12 @@
("", typ "var => logic", Delimfix "_"),
("_DDDOT", typ "logic", Delimfix "..."),
("_strip_positions", typ "'a", NoSyn),
- ("_constify", typ "num_token => num_const", Delimfix "_"),
- ("_constify", typ "float_token => float_const", Delimfix "_"),
- ("_constify", typ "xnum_token => xnum_const", Delimfix "_"),
+ ("_position", typ "num_token => num_position", Delimfix "_"),
+ ("_position", typ "float_token => float_position", Delimfix "_"),
+ ("_position", typ "xnum_token => xnum_position", Delimfix "_"),
+ ("_constify", typ "num_position => num_const", Delimfix "_"),
+ ("_constify", typ "float_position => float_const", Delimfix "_"),
+ ("_constify", typ "xnum_position => xnum_const", Delimfix "_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
("_indexvar", typ "index", Delimfix "'\\<index>"),