src/Pure/Isar/value_parse.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 32787 4271aab3aa4a
child 36950 75b8f26f2f07
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm@29308
     1
(*  Title:      Pure/Isar/value_parse.ML
wenzelm@29308
     2
    Author:     Makarius
wenzelm@29308
     3
wenzelm@29308
     4
Outer syntax parsers for basic ML values.
wenzelm@29308
     5
*)
wenzelm@29308
     6
wenzelm@29308
     7
signature VALUE_PARSE =
wenzelm@29308
     8
sig
wenzelm@29308
     9
  val comma: 'a parser -> 'a parser
wenzelm@29308
    10
  val equal: 'a parser -> 'a parser
wenzelm@29308
    11
  val parens: 'a parser -> 'a parser
wenzelm@32787
    12
  val unit: unit parser
wenzelm@29308
    13
  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
wenzelm@29308
    14
  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
wenzelm@29458
    15
  val list: 'a parser -> 'a list parser
wenzelm@29308
    16
  val properties: Properties.T parser
wenzelm@29308
    17
end;
wenzelm@29308
    18
wenzelm@29308
    19
structure ValueParse: VALUE_PARSE =
wenzelm@29308
    20
struct
wenzelm@29308
    21
wenzelm@29308
    22
structure P = OuterParse;
wenzelm@29308
    23
wenzelm@29308
    24
wenzelm@29308
    25
(* syntax utilities *)
wenzelm@29308
    26
wenzelm@29308
    27
fun comma p = P.$$$ "," |-- P.!!! p;
wenzelm@29308
    28
fun equal p = P.$$$ "=" |-- P.!!! p;
wenzelm@29308
    29
fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
wenzelm@29308
    30
wenzelm@29308
    31
wenzelm@29308
    32
(* tuples *)
wenzelm@29308
    33
wenzelm@29308
    34
val unit = parens (Scan.succeed ());
wenzelm@29308
    35
fun pair p1 p2 = parens (p1 -- comma p2);
wenzelm@29308
    36
fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
wenzelm@29308
    37
wenzelm@29308
    38
wenzelm@29308
    39
(* lists *)
wenzelm@29308
    40
wenzelm@29308
    41
fun list p = parens (P.enum "," p);
wenzelm@29308
    42
val properties = list (P.string -- equal P.string);
wenzelm@29308
    43
wenzelm@29308
    44
end;
wenzelm@29308
    45