src/Pure/Isar/parse_value.ML
author wenzelm
Wed, 02 Jun 2010 11:09:26 +0200
changeset 37251 72c7e636067b
parent 36951 985c197f2fe9
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36951
985c197f2fe9 renamed structure ValueParse to Parse_Value;
wenzelm
parents: 36950
diff changeset
     1
(*  Title:      Pure/Isar/parse_value.ML
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     3
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     4
Outer syntax parsers for basic ML values.
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     5
*)
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     6
36951
985c197f2fe9 renamed structure ValueParse to Parse_Value;
wenzelm
parents: 36950
diff changeset
     7
signature PARSE_VALUE =
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     8
sig
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
     9
  val comma: 'a parser -> 'a parser
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    10
  val equal: 'a parser -> 'a parser
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    11
  val parens: 'a parser -> 'a parser
32787
4271aab3aa4a actually export unit parser;
wenzelm
parents: 30513
diff changeset
    12
  val unit: unit parser
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    13
  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    14
  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
29458
98d749ae5edc export list;
wenzelm
parents: 29308
diff changeset
    15
  val list: 'a parser -> 'a list parser
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    16
  val properties: Properties.T parser
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    17
end;
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    18
36951
985c197f2fe9 renamed structure ValueParse to Parse_Value;
wenzelm
parents: 36950
diff changeset
    19
structure Parse_Value: PARSE_VALUE =
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    20
struct
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    21
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    22
(* syntax utilities *)
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    23
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    24
fun comma p = Parse.$$$ "," |-- Parse.!!! p;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    25
fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    26
fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    27
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    28
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    29
(* tuples *)
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    30
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    31
val unit = parens (Scan.succeed ());
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    32
fun pair p1 p2 = parens (p1 -- comma p2);
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    33
fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    34
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    35
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    36
(* lists *)
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    37
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    38
fun list p = parens (Parse.enum "," p);
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 32787
diff changeset
    39
val properties = list (Parse.string -- equal Parse.string);
29308
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    40
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    41
end;
ddf7fad4448c added Isar/value_parse.ML: Outer syntax parsers for basic ML values.
wenzelm
parents:
diff changeset
    42