position constraints for numerals enable PIDE markup;
authorwenzelm
Mon Jan 16 21:50:15 2012 +0100 (2012-01-16)
changeset 46236ae79f2978a67
parent 46235 e4e0b5190f3d
child 46237 99c80c2f841a
position constraints for numerals enable PIDE markup;
NEWS
src/HOL/Library/Numeral_Type.thy
src/HOL/Tools/float_syntax.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/ex/Binary.thy
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Mon Jan 16 20:32:33 2012 +0100
     1.2 +++ b/NEWS	Mon Jan 16 21:50:15 2012 +0100
     1.3 @@ -26,7 +26,8 @@
     1.4  * Renamed inner syntax categories "num" to "num_token" and "xnum" to
     1.5  "xnum_token", in accordance to existing "float_token".  Minor
     1.6  INCOMPATIBILITY.  Note that in practice "num_const" etc. are mainly
     1.7 -used instead.
     1.8 +used instead (which also include position information via
     1.9 +constraints).
    1.10  
    1.11  
    1.12  *** Pure ***
     2.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Jan 16 20:32:33 2012 +0100
     2.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Jan 16 21:50:15 2012 +0100
     2.3 @@ -296,7 +296,7 @@
     2.4  subsection {* Syntax *}
     2.5  
     2.6  syntax
     2.7 -  "_NumeralType" :: "num_const => type"  ("_")
     2.8 +  "_NumeralType" :: "num_token => type"  ("_")
     2.9    "_NumeralType0" :: type ("0")
    2.10    "_NumeralType1" :: type ("1")
    2.11  
    2.12 @@ -306,46 +306,45 @@
    2.13  
    2.14  parse_translation {*
    2.15  let
    2.16 -fun mk_bintype n =
    2.17 -  let
    2.18 -    fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    2.19 -      | mk_bit 1 = Syntax.const @{type_syntax bit1};
    2.20 -    fun bin_of n =
    2.21 -      if n = 1 then Syntax.const @{type_syntax num1}
    2.22 -      else if n = 0 then Syntax.const @{type_syntax num0}
    2.23 -      else if n = ~1 then raise TERM ("negative type numeral", [])
    2.24 -      else
    2.25 -        let val (q, r) = Integer.div_mod n 2;
    2.26 -        in mk_bit r $ bin_of q end;
    2.27 -  in bin_of n end;
    2.28 +  fun mk_bintype n =
    2.29 +    let
    2.30 +      fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    2.31 +        | mk_bit 1 = Syntax.const @{type_syntax bit1};
    2.32 +      fun bin_of n =
    2.33 +        if n = 1 then Syntax.const @{type_syntax num1}
    2.34 +        else if n = 0 then Syntax.const @{type_syntax num0}
    2.35 +        else if n = ~1 then raise TERM ("negative type numeral", [])
    2.36 +        else
    2.37 +          let val (q, r) = Integer.div_mod n 2;
    2.38 +          in mk_bit r $ bin_of q end;
    2.39 +    in bin_of n end;
    2.40  
    2.41 -fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
    2.42 -      mk_bintype (the (Int.fromString str))
    2.43 -  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    2.44 +  fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
    2.45 +    | numeral_tr ts = raise TERM ("numeral_tr", ts);
    2.46  
    2.47  in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
    2.48  *}
    2.49  
    2.50  print_translation {*
    2.51  let
    2.52 -fun int_of [] = 0
    2.53 -  | int_of (b :: bs) = b + 2 * int_of bs;
    2.54 +  fun int_of [] = 0
    2.55 +    | int_of (b :: bs) = b + 2 * int_of bs;
    2.56  
    2.57 -fun bin_of (Const (@{type_syntax num0}, _)) = []
    2.58 -  | bin_of (Const (@{type_syntax num1}, _)) = [1]
    2.59 -  | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    2.60 -  | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    2.61 -  | bin_of t = raise TERM ("bin_of", [t]);
    2.62 +  fun bin_of (Const (@{type_syntax num0}, _)) = []
    2.63 +    | bin_of (Const (@{type_syntax num1}, _)) = [1]
    2.64 +    | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    2.65 +    | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    2.66 +    | bin_of t = raise TERM ("bin_of", [t]);
    2.67  
    2.68 -fun bit_tr' b [t] =
    2.69 -      let
    2.70 -        val rev_digs = b :: bin_of t handle TERM _ => raise Match
    2.71 -        val i = int_of rev_digs;
    2.72 -        val num = string_of_int (abs i);
    2.73 -      in
    2.74 -        Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    2.75 -      end
    2.76 -  | bit_tr' b _ = raise Match;
    2.77 +  fun bit_tr' b [t] =
    2.78 +        let
    2.79 +          val rev_digs = b :: bin_of t handle TERM _ => raise Match
    2.80 +          val i = int_of rev_digs;
    2.81 +          val num = string_of_int (abs i);
    2.82 +        in
    2.83 +          Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    2.84 +        end
    2.85 +    | bit_tr' b _ = raise Match;
    2.86  in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
    2.87  *}
    2.88  
     3.1 --- a/src/HOL/Tools/float_syntax.ML	Mon Jan 16 20:32:33 2012 +0100
     3.2 +++ b/src/HOL/Tools/float_syntax.ML	Mon Jan 16 21:50:15 2012 +0100
     3.3 @@ -35,8 +35,9 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
     3.8 -  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
     3.9 +fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
    3.10 +  | float_tr [t as Const (str, _)] = mk_frac str
    3.11 +  | float_tr ts = raise TERM ("float_tr", ts);
    3.12  
    3.13  end;
    3.14  
     4.1 --- a/src/HOL/Tools/numeral_syntax.ML	Mon Jan 16 20:32:33 2012 +0100
     4.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Mon Jan 16 21:50:15 2012 +0100
     4.3 @@ -26,9 +26,9 @@
     4.4  
     4.5  in
     4.6  
     4.7 -fun numeral_tr (*"_Numeral"*) [t as Const (num, _)] =
     4.8 -      Syntax.const @{const_syntax Int.number_of} $ mk_bin num
     4.9 -  | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
    4.10 +fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u
    4.11 +  | numeral_tr [t as Const (num, _)] = Syntax.const @{const_syntax Int.number_of} $ mk_bin num
    4.12 +  | numeral_tr ts = raise TERM ("numeral_tr", ts);
    4.13  
    4.14  end;
    4.15  
     5.1 --- a/src/HOL/ex/Binary.thy	Mon Jan 16 20:32:33 2012 +0100
     5.2 +++ b/src/HOL/ex/Binary.thy	Mon Jan 16 21:50:15 2012 +0100
     5.3 @@ -193,7 +193,8 @@
     5.4    val syntax_consts =
     5.5      map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
     5.6  
     5.7 -  fun binary_tr [Const (num, _)] =
     5.8 +  fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
     5.9 +    | binary_tr [Const (num, _)] =
    5.10          let
    5.11            val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
    5.12            val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
     6.1 --- a/src/Pure/Syntax/syntax.ML	Mon Jan 16 20:32:33 2012 +0100
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Jan 16 21:50:15 2012 +0100
     6.3 @@ -542,8 +542,9 @@
     6.4  val basic_nonterms =
     6.5    (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
     6.6      "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
     6.7 -    "any", "prop'", "num_const", "float_const", "xnum_const", "index", "struct",
     6.8 -    "id_position", "longid_position", "xstr_position", "type_name", "class_name"]);
     6.9 +    "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
    6.10 +    "float_position", "xnum_position", "index", "struct", "id_position",
    6.11 +    "longid_position", "xstr_position", "type_name", "class_name"]);
    6.12  
    6.13  
    6.14  
     7.1 --- a/src/Pure/Syntax/syntax_trans.ML	Mon Jan 16 20:32:33 2012 +0100
     7.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Mon Jan 16 21:50:15 2012 +0100
     7.3 @@ -93,7 +93,9 @@
     7.4  
     7.5  (* constify *)
     7.6  
     7.7 -fun constify_ast_tr [Ast.Variable c] = Ast.Constant c
     7.8 +fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
     7.9 +      Ast.Appl [c, constify_ast_tr [ast1], ast2]
    7.10 +  | constify_ast_tr [Ast.Variable c] = Ast.Constant c
    7.11    | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
    7.12  
    7.13  
     8.1 --- a/src/Pure/pure_thy.ML	Mon Jan 16 20:32:33 2012 +0100
     8.2 +++ b/src/Pure/pure_thy.ML	Mon Jan 16 21:50:15 2012 +0100
     8.3 @@ -125,9 +125,12 @@
     8.4      ("",            typ "var => logic",                Delimfix "_"),
     8.5      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     8.6      ("_strip_positions", typ "'a", NoSyn),
     8.7 -    ("_constify",   typ "num_token => num_const",      Delimfix "_"),
     8.8 -    ("_constify",   typ "float_token => float_const",  Delimfix "_"),
     8.9 -    ("_constify",   typ "xnum_token => xnum_const",    Delimfix "_"),
    8.10 +    ("_position",   typ "num_token => num_position",   Delimfix "_"),
    8.11 +    ("_position",   typ "float_token => float_position", Delimfix "_"),
    8.12 +    ("_position",   typ "xnum_token => xnum_position", Delimfix "_"),
    8.13 +    ("_constify",   typ "num_position => num_const",   Delimfix "_"),
    8.14 +    ("_constify",   typ "float_position => float_const", Delimfix "_"),
    8.15 +    ("_constify",   typ "xnum_position => xnum_const", Delimfix "_"),
    8.16      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    8.17      ("_indexdefault", typ "index",                     Delimfix ""),
    8.18      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),