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