New lexical item "float".
authornipkow
Sat Nov 29 13:37:13 2008 +0100 (2008-11-29)
changeset 289043ef9489eeef5
parent 28903 b3fc3a62247a
child 28905 c999579a5166
New lexical item "float".
src/Pure/General/markup.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/General/markup.ML	Fri Nov 28 17:43:06 2008 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Sat Nov 29 13:37:13 2008 +0100
     1.3 @@ -53,6 +53,7 @@
     1.4    val boundN: string val bound: T
     1.5    val varN: string val var: T
     1.6    val numN: string val num: T
     1.7 +  val floatN: string val float: T
     1.8    val xnumN: string val xnum: T
     1.9    val xstrN: string val xstr: T
    1.10    val literalN: string val literal: T
    1.11 @@ -203,6 +204,7 @@
    1.12  val (boundN, bound) = markup_elem "bound";
    1.13  val (varN, var) = markup_elem "var";
    1.14  val (numN, num) = markup_elem "num";
    1.15 +val (floatN, float) = markup_elem "float";
    1.16  val (xnumN, xnum) = markup_elem "xnum";
    1.17  val (xstrN, xstr) = markup_elem "xstr";
    1.18  val (literalN, literal) = markup_elem "literal";
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Nov 28 17:43:06 2008 +0100
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Nov 29 13:37:13 2008 +0100
     2.3 @@ -30,6 +30,7 @@
     2.4    val read_nat: string -> int option
     2.5    val read_int: string -> int option
     2.6    val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
     2.7 +  val read_float: string -> {mant: int, exp: int}
     2.8    val fixedN: string
     2.9    val constN: string
    2.10  end;
    2.11 @@ -40,7 +41,7 @@
    2.12    val is_xid: string -> bool
    2.13    datatype token_kind =
    2.14      Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
    2.15 -    NumSy | XNumSy | StrSy | Space | Comment | EOF
    2.16 +    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
    2.17    datatype token = Token of token_kind * string * Position.range
    2.18    val str_of_token: token -> string
    2.19    val pos_of_token: token -> Position.T
    2.20 @@ -98,6 +99,8 @@
    2.21  
    2.22  val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
    2.23  val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
    2.24 +val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
    2.25 +val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
    2.26  val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
    2.27  val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
    2.28  
    2.29 @@ -111,7 +114,7 @@
    2.30  
    2.31  datatype token_kind =
    2.32    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
    2.33 -  NumSy | XNumSy | StrSy | Space | Comment | EOF;
    2.34 +  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
    2.35  
    2.36  datatype token = Token of token_kind * string * Position.range;
    2.37  
    2.38 @@ -142,7 +145,8 @@
    2.39  val tidT = Type ("tid", []);
    2.40  val tvarT = Type ("tvar", []);
    2.41  
    2.42 -val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"];
    2.43 +val terminals =
    2.44 +  ["id", "longid", "var", "tid", "tvar", "num", "float", "xnum", "xstr"];
    2.45  val is_terminal = member (op =) terminals;
    2.46  
    2.47  
    2.48 @@ -156,6 +160,7 @@
    2.49    | TFreeSy     => Markup.tfree
    2.50    | TVarSy      => Markup.tvar
    2.51    | NumSy       => Markup.num
    2.52 +  | FloatSy     => Markup.float
    2.53    | XNumSy      => Markup.xnum
    2.54    | StrSy       => Markup.xstr
    2.55    | Space       => Markup.none
    2.56 @@ -187,6 +192,7 @@
    2.57    | predef_term "tid" = SOME (Token (TFreeSy, "tid", Position.no_range))
    2.58    | predef_term "tvar" = SOME (Token (TVarSy, "tvar", Position.no_range))
    2.59    | predef_term "num" = SOME (Token (NumSy, "num", Position.no_range))
    2.60 +  | predef_term "float" = SOME (Token (FloatSy, "float", Position.no_range))
    2.61    | predef_term "xnum" = SOME (Token (XNumSy, "xnum", Position.no_range))
    2.62    | predef_term "xstr" = SOME (Token (StrSy, "xstr", Position.no_range))
    2.63    | predef_term _ = NONE;
    2.64 @@ -234,6 +240,7 @@
    2.65        scan_tvar >> token TVarSy ||
    2.66        scan_var >> token VarSy ||
    2.67        scan_tid >> token TFreeSy ||
    2.68 +      scan_float >> token FloatSy ||
    2.69        scan_num >> token NumSy ||
    2.70        $$$ "#" @@@ scan_num >> token XNumSy ||
    2.71        scan_longid >> token LongIdentSy ||
    2.72 @@ -380,4 +387,16 @@
    2.73  
    2.74  end;
    2.75  
    2.76 +fun read_float str =
    2.77 +  let
    2.78 +    val (sign, cs) =
    2.79 +      (case Symbol.explode str of  "-" :: cs => (~1, cs) | cs => (1, cs));
    2.80 +    val (intpart,fracpart) =
    2.81 +      (case take_prefix Symbol.is_digit cs of
    2.82 +        (intpart, "." :: fracpart) => (intpart,fracpart)
    2.83 +      | _ =>  sys_error "read_float")
    2.84 +  in {mant = sign * #1 (Library.read_int (intpart@fracpart)),
    2.85 +      exp = length fracpart}
    2.86 +  end
    2.87 +
    2.88  end;
     3.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Nov 28 17:43:06 2008 +0100
     3.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Nov 29 13:37:13 2008 +0100
     3.3 @@ -387,7 +387,7 @@
     3.4  fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
     3.5  
     3.6  val standard_token_classes =
     3.7 -  ["class", "tfree", "tvar", "free", "bound", "var", "num", "xnum", "xstr"];
     3.8 +  ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
     3.9  
    3.10  val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
    3.11  
     4.1 --- a/src/Pure/Syntax/syntax.ML	Fri Nov 28 17:43:06 2008 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Nov 29 13:37:13 2008 +0100
     4.3 @@ -391,7 +391,8 @@
     4.4  val basic_nonterms =
     4.5    (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
     4.6      SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
     4.7 -    "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]);
     4.8 +    "asms", SynExt.any_, SynExt.sprop, "num_const", "float_const",
     4.9 +    "index", "struct"]);
    4.10  
    4.11  
    4.12  
     5.1 --- a/src/Pure/pure_thy.ML	Fri Nov 28 17:43:06 2008 +0100
     5.2 +++ b/src/Pure/pure_thy.ML	Sat Nov 29 13:37:13 2008 +0100
     5.3 @@ -321,6 +321,7 @@
     5.4      ("",            typ "var => logic",                Delimfix "_"),
     5.5      ("_DDDOT",      typ "logic",                       Delimfix "..."),
     5.6      ("_constify",   typ "num => num_const",            Delimfix "_"),
     5.7 +    ("_constify",   typ "float => float_const",        Delimfix "_"),
     5.8      ("_indexnum",   typ "num_const => index",          Delimfix "\\<^sub>_"),
     5.9      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
    5.10      ("_indexdefault", typ "index",                     Delimfix ""),