Minimal parsing for SML -- fixing integer numerals.
authorwenzelm
Sun Sep 16 14:52:28 2007 +0200 (2007-09-16)
changeset 245946689effe75d1
parent 24593 1547ea587f5a
child 24595 5c290506fbc0
Minimal parsing for SML -- fixing integer numerals.
src/Pure/ML/ml_parse.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/ml_parse.ML	Sun Sep 16 14:52:28 2007 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +(*  Title:      Pure/ML/ml_parse.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Minimal parsing for SML -- fixing integer numerals.
     1.9 +*)
    1.10 +
    1.11 +signature ML_PARSE =
    1.12 +sig
    1.13 +  val fix_ints: string -> string
    1.14 +end;
    1.15 +
    1.16 +structure ML_Parse: ML_PARSE =
    1.17 +struct
    1.18 +
    1.19 +structure T = ML_Lex;
    1.20 +
    1.21 +
    1.22 +(** error handling **)
    1.23 +
    1.24 +fun !!! scan =
    1.25 +  let
    1.26 +    fun get_pos [] = " (past end-of-file!)"
    1.27 +      | get_pos (tok :: _) = T.pos_of tok;
    1.28 +
    1.29 +    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
    1.30 +      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
    1.31 +  in Scan.!! err scan end;
    1.32 +
    1.33 +fun bad_input x =
    1.34 +  (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
    1.35 +    (fn msg => Scan.fail_with (K msg))) x;
    1.36 +
    1.37 +
    1.38 +(** basic parsers **)
    1.39 +
    1.40 +fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
    1.41 +val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
    1.42 +
    1.43 +val regular = Scan.one T.is_regular >> T.val_of;
    1.44 +val improper = Scan.one T.is_improper >> T.val_of;
    1.45 +
    1.46 +val blanks = Scan.repeat improper >> implode;
    1.47 +
    1.48 +
    1.49 +(* fix_ints *)
    1.50 +
    1.51 +(*approximation only -- corrupts numeric record field patterns *)
    1.52 +val fix_int =
    1.53 +  $$$ "#" ^^ blanks ^^ int ||
    1.54 +  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
    1.55 +  int >> (fn x => "(" ^ x ^ ":int)") ||
    1.56 +  regular ||
    1.57 +  bad_input;
    1.58 +
    1.59 +fun do_fix_ints s =
    1.60 +  Source.of_string s
    1.61 +  |> T.source
    1.62 +  |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
    1.63 +  |> Source.exhaust
    1.64 +  |> implode;
    1.65 +
    1.66 +val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
    1.67 +
    1.68 +end;