| 
24594
 | 
     1  | 
(*  Title:      Pure/ML/ml_parse.ML
  | 
| 
 | 
     2  | 
    ID:         $Id$
  | 
| 
 | 
     3  | 
    Author:     Makarius
  | 
| 
 | 
     4  | 
  | 
| 
 | 
     5  | 
Minimal parsing for SML -- fixing integer numerals.
  | 
| 
 | 
     6  | 
*)
  | 
| 
 | 
     7  | 
  | 
| 
 | 
     8  | 
signature ML_PARSE =
  | 
| 
 | 
     9  | 
sig
  | 
| 
 | 
    10  | 
  val fix_ints: string -> string
  | 
| 
 | 
    11  | 
end;
  | 
| 
 | 
    12  | 
  | 
| 
 | 
    13  | 
structure ML_Parse: ML_PARSE =
  | 
| 
 | 
    14  | 
struct
  | 
| 
 | 
    15  | 
  | 
| 
 | 
    16  | 
structure T = ML_Lex;
  | 
| 
 | 
    17  | 
  | 
| 
 | 
    18  | 
  | 
| 
 | 
    19  | 
(** error handling **)
  | 
| 
 | 
    20  | 
  | 
| 
 | 
    21  | 
fun !!! scan =
  | 
| 
 | 
    22  | 
  let
  | 
| 
 | 
    23  | 
    fun get_pos [] = " (past end-of-file!)"
  | 
| 
 | 
    24  | 
      | get_pos (tok :: _) = T.pos_of tok;
  | 
| 
 | 
    25  | 
  | 
| 
 | 
    26  | 
    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
  | 
| 
 | 
    27  | 
      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
  | 
| 
 | 
    28  | 
  in Scan.!! err scan end;
  | 
| 
 | 
    29  | 
  | 
| 
 | 
    30  | 
fun bad_input x =
  | 
| 
 | 
    31  | 
  (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
  | 
| 
 | 
    32  | 
    (fn msg => Scan.fail_with (K msg))) x;
  | 
| 
 | 
    33  | 
  | 
| 
 | 
    34  | 
  | 
| 
 | 
    35  | 
(** basic parsers **)
  | 
| 
 | 
    36  | 
  | 
| 
 | 
    37  | 
fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
  | 
| 
 | 
    38  | 
val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
  | 
| 
 | 
    39  | 
  | 
| 
 | 
    40  | 
val regular = Scan.one T.is_regular >> T.val_of;
  | 
| 
 | 
    41  | 
val improper = Scan.one T.is_improper >> T.val_of;
  | 
| 
 | 
    42  | 
  | 
| 
 | 
    43  | 
val blanks = Scan.repeat improper >> implode;
  | 
| 
 | 
    44  | 
  | 
| 
 | 
    45  | 
  | 
| 
 | 
    46  | 
(* fix_ints *)
  | 
| 
 | 
    47  | 
  | 
| 
 | 
    48  | 
(*approximation only -- corrupts numeric record field patterns *)
  | 
| 
 | 
    49  | 
val fix_int =
  | 
| 
 | 
    50  | 
  $$$ "#" ^^ blanks ^^ int ||
  | 
| 
 | 
    51  | 
  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
  | 
| 
 | 
    52  | 
  int >> (fn x => "(" ^ x ^ ":int)") ||
 | 
| 
 | 
    53  | 
  regular ||
  | 
| 
 | 
    54  | 
  bad_input;
  | 
| 
 | 
    55  | 
  | 
| 
 | 
    56  | 
fun do_fix_ints s =
  | 
| 
 | 
    57  | 
  Source.of_string s
  | 
| 
 | 
    58  | 
  |> T.source
  | 
| 
 | 
    59  | 
  |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
  | 
| 
 | 
    60  | 
  |> Source.exhaust
  | 
| 
 | 
    61  | 
  |> implode;
  | 
| 
 | 
    62  | 
  | 
| 
 | 
    63  | 
val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
  | 
| 
 | 
    64  | 
  | 
| 
 | 
    65  | 
end;
  |