src/Pure/Tools/rail.ML
changeset 58465 bd06c6479748
parent 56165 dd89ce51d2c8
child 58903 38c72f5f6c2e
     1.1 --- a/src/Pure/Tools/rail.ML	Fri Sep 26 15:05:11 2014 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Fri Sep 26 15:10:02 2014 +0200
     1.3 @@ -36,6 +36,11 @@
     1.4  fun pos_of (Token ((pos, _), _)) = pos;
     1.5  fun end_pos_of (Token ((_, pos), _)) = pos;
     1.6  
     1.7 +fun range_of (toks as tok :: _) =
     1.8 +      let val pos' = end_pos_of (List.last toks)
     1.9 +      in Position.range (pos_of tok) pos' end
    1.10 +  | range_of [] = Position.no_range;
    1.11 +
    1.12  fun kind_of (Token (_, (k, _))) = k;
    1.13  fun content_of (Token (_, (_, x))) = x;
    1.14  
    1.15 @@ -80,6 +85,9 @@
    1.16  
    1.17  fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
    1.18  
    1.19 +fun antiq_token (antiq as (ss, {range, ...})) =
    1.20 +  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
    1.21 +
    1.22  val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    1.23  
    1.24  val scan_keyword =
    1.25 @@ -89,7 +97,7 @@
    1.26  
    1.27  val scan_token =
    1.28    scan_space >> K [] ||
    1.29 -  Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
    1.30 +  Antiquote.scan_antiq >> antiq_token ||
    1.31    scan_keyword >> (token Keyword o single) ||
    1.32    Lexicon.scan_id >> token Ident ||
    1.33    Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
    1.34 @@ -110,6 +118,8 @@
    1.35  
    1.36  (** parsing **)
    1.37  
    1.38 +(* parser combinators *)
    1.39 +
    1.40  fun !!! scan =
    1.41    let
    1.42      val prefix = "Rail syntax error";
    1.43 @@ -140,6 +150,78 @@
    1.44  
    1.45  val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
    1.46  
    1.47 +fun RANGE scan = Scan.trace scan >> apsnd range_of;
    1.48 +fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
    1.49 +
    1.50 +
    1.51 +(* parse trees *)
    1.52 +
    1.53 +datatype trees =
    1.54 +  CAT of tree list * Position.range
    1.55 +and tree =
    1.56 +  BAR of trees list * Position.range |
    1.57 +  STAR of (trees * trees) * Position.range |
    1.58 +  PLUS of (trees * trees) * Position.range |
    1.59 +  MAYBE of tree * Position.range |
    1.60 +  NEWLINE of Position.range |
    1.61 +  NONTERMINAL of string * Position.range |
    1.62 +  TERMINAL of (bool * string) * Position.range |
    1.63 +  ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
    1.64 +
    1.65 +fun reports_of_tree ctxt =
    1.66 +  if Context_Position.is_visible ctxt then
    1.67 +    let
    1.68 +      fun reports r =
    1.69 +        if r = Position.no_range then []
    1.70 +        else [(Position.set_range r, Markup.expression)];
    1.71 +      fun trees (CAT (ts, r)) = reports r @ maps tree ts
    1.72 +      and tree (BAR (Ts, r)) = reports r @ maps trees Ts
    1.73 +        | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
    1.74 +        | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
    1.75 +        | tree (MAYBE (t, r)) = reports r @ tree t
    1.76 +        | tree (NEWLINE r) = reports r
    1.77 +        | tree (NONTERMINAL (_, r)) = reports r
    1.78 +        | tree (TERMINAL (_, r)) = reports r
    1.79 +        | tree (ANTIQUOTE (_, r)) = reports r;
    1.80 +    in distinct (op =) o tree end
    1.81 +  else K [];
    1.82 +
    1.83 +local
    1.84 +
    1.85 +val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
    1.86 +
    1.87 +fun body x = (RANGE (enum1 "|" body1) >> BAR) x
    1.88 +and body0 x = (RANGE (enum "|" body1) >> BAR) x
    1.89 +and body1 x =
    1.90 + (RANGE_APP (body2 :|-- (fn a =>
    1.91 +   $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
    1.92 +   $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
    1.93 +   Scan.succeed (K a)))) x
    1.94 +and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
    1.95 +and body3 x =
    1.96 + (RANGE_APP (body4 :|-- (fn a =>
    1.97 +   $$$ "?" >> K (curry MAYBE a) ||
    1.98 +   Scan.succeed (K a)))) x
    1.99 +and body4 x =
   1.100 + ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   1.101 +  RANGE_APP
   1.102 +   ($$$ "\<newline>" >> K NEWLINE ||
   1.103 +    ident >> curry NONTERMINAL ||
   1.104 +    at_mode -- string >> curry TERMINAL ||
   1.105 +    at_mode -- antiq >> curry ANTIQUOTE)) x
   1.106 +and body4e x =
   1.107 +  (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
   1.108 +
   1.109 +val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
   1.110 +val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
   1.111 +val rules = enum1 ";" (Scan.option rule) >> map_filter I;
   1.112 +
   1.113 +in
   1.114 +
   1.115 +fun parse_rules toks =
   1.116 +  #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
   1.117 +
   1.118 +end;
   1.119  
   1.120  
   1.121  (** rail expressions **)
   1.122 @@ -156,68 +238,58 @@
   1.123    Terminal of bool * string |
   1.124    Antiquote of bool * Antiquote.antiq;
   1.125  
   1.126 -fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
   1.127 -and reverse (Bar cats) = Bar (map reverse_cat cats)
   1.128 -  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   1.129 -  | reverse x = x;
   1.130 +fun is_newline (Newline _) = true | is_newline _ = false;
   1.131 +
   1.132 +
   1.133 +(* prepare *)
   1.134 +
   1.135 +local
   1.136  
   1.137  fun cat rails = Cat (0, rails);
   1.138  
   1.139  val empty = cat [];
   1.140  fun is_empty (Cat (_, [])) = true | is_empty _ = false;
   1.141  
   1.142 -fun is_newline (Newline _) = true | is_newline _ = false;
   1.143 -
   1.144  fun bar [Cat (_, [rail])] = rail
   1.145    | bar cats = Bar cats;
   1.146  
   1.147 -fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
   1.148 +fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
   1.149 +and reverse (Bar cats) = Bar (map reverse_cat cats)
   1.150 +  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   1.151 +  | reverse x = x;
   1.152 +
   1.153 +fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
   1.154 +
   1.155 +in
   1.156  
   1.157 -fun star cat1 cat2 =
   1.158 -  if is_empty cat2 then plus empty cat1
   1.159 -  else bar [empty, cat [plus cat1 cat2]];
   1.160 +fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
   1.161 +and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
   1.162 +  | prepare_tree (STAR (Ts, _)) =
   1.163 +      let val (cat1, cat2) = pairself prepare_trees Ts in
   1.164 +        if is_empty cat2 then plus (empty, cat1)
   1.165 +        else bar [empty, cat [plus (cat1, cat2)]]
   1.166 +      end
   1.167 +  | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts)
   1.168 +  | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
   1.169 +  | prepare_tree (NEWLINE _) = Newline 0
   1.170 +  | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
   1.171 +  | prepare_tree (TERMINAL (a, _)) = Terminal a
   1.172 +  | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
   1.173  
   1.174 -fun maybe rail = bar [empty, cat [rail]];
   1.175 +end;
   1.176  
   1.177  
   1.178  (* read *)
   1.179  
   1.180 -local
   1.181 -
   1.182 -val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
   1.183 -
   1.184 -fun body x = (enum1 "|" body1 >> bar) x
   1.185 -and body0 x = (enum "|" body1 >> bar) x
   1.186 -and body1 x =
   1.187 - (body2 :|-- (fn a =>
   1.188 -   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
   1.189 -   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
   1.190 -   Scan.succeed a)) x
   1.191 -and body2 x = (Scan.repeat1 body3 >> cat) x
   1.192 -and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
   1.193 -and body4 x =
   1.194 - ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   1.195 -  $$$ "\<newline>" >> K (Newline 0) ||
   1.196 -  ident >> Nonterminal ||
   1.197 -  at_mode -- string >> Terminal ||
   1.198 -  at_mode -- antiq >> Antiquote) x
   1.199 -and body4e x = (Scan.option body4 >> (cat o the_list)) x;
   1.200 -
   1.201 -val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
   1.202 -val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
   1.203 -val rules = enum1 ";" (Scan.option rule) >> map_filter I;
   1.204 -
   1.205 -in
   1.206 -
   1.207  fun read ctxt (source: Symbol_Pos.source) =
   1.208    let
   1.209      val {text, pos, ...} = source;
   1.210      val _ = Context_Position.report ctxt pos Markup.language_rail;
   1.211      val toks = tokenize (Symbol_Pos.explode (text, pos));
   1.212      val _ = Context_Position.reports ctxt (maps reports_of_token toks);
   1.213 -  in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
   1.214 -
   1.215 -end;
   1.216 +    val rules = parse_rules toks;
   1.217 +    val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);
   1.218 +  in map (apsnd prepare_tree) rules end;
   1.219  
   1.220  
   1.221  (* latex output *)