src/Pure/General/scan.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23699 5a4527f3ac79
child 24025 77e3e5781a99
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/scan.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
     4 
     5 Generic scanners (for potentially infinite input).
     6 *)
     7 
     8 infix 5 -- :-- |-- --| ^^;
     9 infix 3 >>;
    10 infixr 0 ||;
    11 
    12 signature BASIC_SCAN =
    13 sig
    14   (*error msg handler*)
    15   val !! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b
    16   (*apply function*)
    17   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    18   (*alternative*)
    19   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
    20   (*sequential pairing*)
    21   val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    22   (*dependent pairing*)
    23   val :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e
    24   (*forget fst*)
    25   val |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e
    26   (*forget snd*)
    27   val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
    28   (*concatenation*)
    29   val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
    30   (*one element literal*)
    31   val $$ : string -> string list -> string * string list
    32   val ~$$ : string -> string list -> string * string list
    33 end;
    34 
    35 signature SCAN =
    36 sig
    37   include BASIC_SCAN
    38   val prompt: string -> ('a -> 'b) -> 'a -> 'b
    39   val error: ('a -> 'b) -> 'a -> 'b
    40   val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
    41   val fail: 'a -> 'b
    42   val fail_with: ('a -> string) -> 'a -> 'b
    43   val succeed: 'a -> 'b -> 'a * 'b
    44   val some: ('a -> 'b option) -> 'a list -> 'b * 'a list
    45   val one: ('a -> bool) -> 'a list -> 'a * 'a list
    46   val this: string list -> string list -> string list * string list
    47   val this_string: string -> string list -> string * string list
    48   val many: ('a -> bool) -> 'a list -> 'a list * 'a list
    49   val many1: ('a -> bool) -> 'a list -> 'a list * 'a list
    50   val optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a
    51   val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    52   val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    53   val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    54   val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    55   val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    56   val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
    57   val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
    58   val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
    59   val first: ('a -> 'b) list -> 'a -> 'b
    60   val state: 'a * 'b -> 'a * ('a * 'b)
    61   val depend: ('a -> 'b -> ('c * 'd) * 'e) -> 'a * 'b -> 'd * ('c * 'e)
    62   val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
    63   val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    64   val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    65   val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
    66   val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
    67   val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    68     -> 'b * 'a list -> 'c * ('d * 'a list)
    69   val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    70   val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    71   val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b * ('b -> bool) ->
    72     ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
    73   type lexicon
    74   val dest_lexicon: lexicon -> string list
    75   val make_lexicon: string list list -> lexicon
    76   val empty_lexicon: lexicon
    77   val extend_lexicon: string list list -> lexicon -> lexicon
    78   val merge_lexicons: lexicon -> lexicon -> lexicon
    79   val is_literal: lexicon -> string list -> bool
    80   val literal: lexicon -> string list -> string list * string list
    81 end;
    82 
    83 structure Scan: SCAN =
    84 struct
    85 
    86 
    87 (** scanners **)
    88 
    89 (* exceptions *)
    90 
    91 exception MORE of string option;        (*need more input (prompt)*)
    92 exception FAIL of string option;        (*try alternatives (reason of failure)*)
    93 exception ABORT of string;              (*dead end*)
    94 
    95 fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    96 fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    97 fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    98 fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    99 fun error scan xs = scan xs handle ABORT msg => Library.error msg;
   100 
   101 fun catch scan xs = scan xs
   102   handle ABORT msg => raise Fail msg
   103     | FAIL msg => raise Fail (the_default "Syntax error." msg);
   104 
   105 
   106 (* scanner combinators *)
   107 
   108 fun (scan >> f) xs = scan xs |>> f;
   109 
   110 fun (scan1 || scan2) xs = scan1 xs handle FAIL _ => scan2 xs;
   111 
   112 fun (scan1 :-- scan2) xs =
   113   let
   114     val (x, ys) = scan1 xs;
   115     val (y, zs) = scan2 x ys;
   116   in ((x, y), zs) end;
   117 
   118 fun (scan1 -- scan2) = scan1 :-- (fn _ => scan2);
   119 fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
   120 fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
   121 fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
   122 
   123 
   124 (* generic scanners *)
   125 
   126 fun fail _ = raise FAIL NONE;
   127 fun fail_with msg_of xs = raise FAIL (SOME (msg_of xs));
   128 fun succeed y xs = (y, xs);
   129 
   130 fun some _ [] = raise MORE NONE
   131   | some f (x :: xs) =
   132       (case f x of SOME y => (y, xs) | _ => raise FAIL NONE);
   133 
   134 fun one _ [] = raise MORE NONE
   135   | one pred (x :: xs) =
   136       if pred x then (x, xs) else raise FAIL NONE;
   137 
   138 fun $$ a = one (fn s: string => s = a);
   139 fun ~$$ a = one (fn s: string => s <> a);
   140 
   141 fun this ys xs =
   142   let
   143     fun drop_prefix [] xs = xs
   144       | drop_prefix (_ :: _) [] = raise MORE NONE
   145       | drop_prefix (y :: ys) (x :: xs) =
   146           if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
   147   in (ys, drop_prefix ys xs) end;
   148 
   149 fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
   150 
   151 fun many _ [] = raise MORE NONE
   152   | many pred (lst as x :: xs) =
   153       if pred x then apfst (cons x) (many pred xs)
   154       else ([], lst);
   155 
   156 fun many1 pred = one pred -- many pred >> op ::;
   157 
   158 fun optional scan def = scan || succeed def;
   159 fun option scan = (scan >> SOME) || succeed NONE;
   160 
   161 fun repeat scan =
   162   let
   163     fun rep ys xs =
   164       (case (SOME (scan xs) handle FAIL _ => NONE) of
   165         NONE => (rev ys, xs)
   166       | SOME (y, xs') => rep (y :: ys) xs');
   167   in rep [] end;
   168 
   169 fun repeat1 scan = scan -- repeat scan >> op ::;
   170 
   171 fun single scan = scan >> (fn x => [x]);
   172 fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
   173 
   174 fun max leq scan1 scan2 xs =
   175   (case (option scan1 xs, option scan2 xs) of
   176     ((NONE, _), (NONE, _)) => raise FAIL NONE           (*looses FAIL msg!*)
   177   | ((SOME tok1, xs'), (NONE, _)) => (tok1, xs')
   178   | ((NONE, _), (SOME tok2, xs')) => (tok2, xs')
   179   | ((SOME tok1, xs1'), (SOME tok2, xs2')) =>
   180       if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2'));
   181 
   182 fun ahead scan xs = (fst (scan xs), xs);
   183 
   184 fun unless test scan =
   185   ahead (option test) :-- (fn NONE => scan | _ => fail) >> #2;
   186 
   187 fun first [] = fail
   188   | first (scan :: scans) = scan || first scans;
   189 
   190 
   191 (* state based scanners *)
   192 
   193 fun state (st, xs) = (st, (st, xs));
   194 
   195 fun depend scan (st, xs) =
   196   let val ((st', y), xs') = scan st xs
   197   in (y, (st', xs')) end;
   198 
   199 fun peek scan = depend (fn st => scan st >> pair st);
   200 
   201 fun pass st scan xs =
   202   let val (y, (_, xs')) = scan (st, xs)
   203   in (y, xs') end;
   204 
   205 fun lift scan (st, xs) =
   206   let val (y, xs') = scan xs
   207   in (y, (st, xs')) end;
   208 
   209 fun unlift scan = pass () scan;
   210 
   211 
   212 (* trace input *)
   213 
   214 fun trace scan xs =
   215   let val (y, xs') = scan xs
   216   in ((y, Library.take (length xs - length xs', xs)), xs') end;
   217 
   218 
   219 (* finite scans *)
   220 
   221 fun finite' (stopper, is_stopper) scan (state, input) =
   222   let
   223     fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!";
   224 
   225     fun stop [] = lost ()
   226       | stop lst =
   227           let val (xs, x) = split_last lst
   228           in if is_stopper x then ((), xs) else lost () end;
   229   in
   230     if exists is_stopper input then
   231       raise ABORT "Stopper may not occur in input of finite scan!"
   232     else (strict scan --| lift stop) (state, input @ [stopper])
   233   end;
   234 
   235 fun finite stopper scan = unlift (finite' stopper (lift scan));
   236 
   237 fun read stopper scan xs =
   238   (case error (finite stopper (option scan)) xs of
   239     (y as SOME _, []) => y
   240   | _ => NONE);
   241 
   242 
   243 (* infinite scans -- draining state-based source *)
   244 
   245 fun drain def_prompt get stopper scan ((state, xs), src) =
   246   (scan (state, xs), src) handle MORE prompt =>
   247     (case get (the_default def_prompt prompt) src of
   248       ([], _) => (finite' stopper scan (state, xs), src)
   249     | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src'));
   250 
   251 
   252 
   253 (** datatype lexicon **)
   254 
   255 datatype lexicon =
   256   Empty |
   257   Branch of string * string list * lexicon * lexicon * lexicon;
   258 
   259 val no_literal = [];
   260 
   261 
   262 (* dest_lexicon *)
   263 
   264 fun dest_lex Empty = []
   265   | dest_lex (Branch (_, [], lt, eq, gt)) =
   266       dest_lex lt @ dest_lex eq @ dest_lex gt
   267   | dest_lex (Branch (_, cs, lt, eq, gt)) =
   268       dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt;
   269 
   270 val dest_lexicon = map implode o dest_lex;
   271 
   272 
   273 (* empty, extend, make, merge lexicons *)
   274 
   275 val empty_lexicon = Empty;
   276 
   277 fun extend_lexicon [] lexicon = lexicon
   278   | extend_lexicon chrss lexicon =
   279       let
   280         fun ext chrs lex =
   281           let
   282             fun add (chs as c :: cs) (Branch (d, a, lt, eq, gt)) =
   283                   (case fast_string_ord (c, d) of
   284                     LESS => Branch (d, a, add chs lt, eq, gt)
   285                   | EQUAL => Branch (d, if null cs then chrs else a, lt, add cs eq, gt)
   286                   | GREATER => Branch (d, a, lt, eq, add chs gt))
   287               | add [c] Empty = Branch (c, chrs, Empty, Empty, Empty)
   288               | add (c :: cs) Empty = Branch (c, no_literal, Empty, add cs Empty, Empty)
   289               | add [] lex = lex;
   290           in add chrs lex end;
   291       in lexicon |> fold ext (chrss |> subtract (op =) (dest_lex lexicon)) end;
   292 
   293 fun make_lexicon chrss = extend_lexicon chrss empty_lexicon;
   294 
   295 fun merge_lexicons lex1 lex2 =
   296   let
   297     val chss1 = dest_lex lex1;
   298     val chss2 = dest_lex lex2;
   299   in
   300     if chss2 subset chss1 then lex1
   301     else if chss1 subset chss2 then lex2
   302     else extend_lexicon chss2 lex1
   303   end;
   304 
   305 
   306 (* is_literal *)
   307 
   308 fun is_literal Empty _ = false
   309   | is_literal _ [] = false
   310   | is_literal (Branch (d, a, lt, eq, gt)) (chs as c :: cs) =
   311       (case fast_string_ord (c, d) of
   312         LESS => is_literal lt chs
   313       | EQUAL => a <> no_literal andalso null cs orelse is_literal eq cs
   314       | GREATER => is_literal gt chs);
   315 
   316 
   317 (* scan literal *)
   318 
   319 fun literal lex chrs =
   320   let
   321     fun lit Empty res _ = res
   322       | lit (Branch _) _ [] = raise MORE NONE
   323       | lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) =
   324           (case fast_string_ord (c, d) of
   325             LESS => lit lt res chs
   326           | EQUAL => lit eq (if a = no_literal then res else SOME (a, cs)) cs
   327           | GREATER => lit gt res chs);
   328   in
   329     (case lit lex NONE chrs of
   330       NONE => raise FAIL NONE
   331     | SOME res => res)
   332   end;
   333 
   334 end;
   335 
   336 structure BasicScan: BASIC_SCAN = Scan;
   337 open BasicScan;