src/Pure/Isar/value_parse.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29458 98d749ae5edc
child 30513 1796b8ea88aa
permissions -rw-r--r--
use long names for old-style fold combinators;
     1 (*  Title:      Pure/Isar/value_parse.ML
     2     Author:     Makarius
     3 
     4 Outer syntax parsers for basic ML values.
     5 *)
     6 
     7 signature VALUE_PARSE =
     8 sig
     9   type 'a parser = 'a OuterParse.parser
    10   val comma: 'a parser -> 'a parser
    11   val equal: 'a parser -> 'a parser
    12   val parens: 'a parser -> 'a parser
    13   val pair: 'a parser -> 'b parser -> ('a * 'b) parser
    14   val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
    15   val list: 'a parser -> 'a list parser
    16   val properties: Properties.T parser
    17 end;
    18 
    19 structure ValueParse: VALUE_PARSE =
    20 struct
    21 
    22 structure P = OuterParse;
    23 type 'a parser = 'a P.parser;
    24 
    25 
    26 (* syntax utilities *)
    27 
    28 fun comma p = P.$$$ "," |-- P.!!! p;
    29 fun equal p = P.$$$ "=" |-- P.!!! p;
    30 fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
    31 
    32 
    33 (* tuples *)
    34 
    35 val unit = parens (Scan.succeed ());
    36 fun pair p1 p2 = parens (p1 -- comma p2);
    37 fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
    38 
    39 
    40 (* lists *)
    41 
    42 fun list p = parens (P.enum "," p);
    43 val properties = list (P.string -- equal P.string);
    44 
    45 end;
    46