infixr || (more efficient);
authorwenzelm
Tue Jul 10 16:45:01 2007 +0200 (2007-07-10)
changeset 236995a4527f3ac79
parent 23698 af84f2f13d4d
child 23700 fb1102e98cd4
infixr || (more efficient);
tuned signature;
removed unused trace';
moved source cascading from scan.ML to source.ML;
tuned;
src/Pure/General/scan.ML
     1.1 --- a/src/Pure/General/scan.ML	Tue Jul 10 16:45:00 2007 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Tue Jul 10 16:45:01 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  infix 5 -- :-- |-- --| ^^;
     1.6  infix 3 >>;
     1.7 -infix 0 ||;
     1.8 +infixr 0 ||;
     1.9  
    1.10  signature BASIC_SCAN =
    1.11  sig
    1.12 @@ -35,6 +35,9 @@
    1.13  signature SCAN =
    1.14  sig
    1.15    include BASIC_SCAN
    1.16 +  val prompt: string -> ('a -> 'b) -> 'a -> 'b
    1.17 +  val error: ('a -> 'b) -> 'a -> 'b
    1.18 +  val catch: ('a -> 'b) -> 'a -> 'b    (*exception Fail*)
    1.19    val fail: 'a -> 'b
    1.20    val fail_with: ('a -> string) -> 'a -> 'b
    1.21    val succeed: 'a -> 'b -> 'a * 'b
    1.22 @@ -48,6 +51,8 @@
    1.23    val option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a
    1.24    val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.25    val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.26 +  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.27 +  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.28    val max: ('a * 'a -> bool) -> ('b -> 'a * 'b) -> ('b -> 'a * 'b) -> 'b -> 'a * 'b
    1.29    val ahead: ('a -> 'b * 'c) -> 'a -> 'b * 'a
    1.30    val unless: ('a -> 'b * 'a) -> ('a -> 'c * 'd) -> 'a -> 'c * 'd
    1.31 @@ -57,24 +62,14 @@
    1.32    val peek: ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd)
    1.33    val pass: 'a -> ('a * 'b -> 'c * ('d * 'e)) -> 'b -> 'c * 'e
    1.34    val lift: ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c)
    1.35 -  val trace': ('a * 'b list -> 'c * ('d * 'e list)) -> 'a * 'b list ->
    1.36 -    ('c * 'b list) * ('d * 'e list)
    1.37 +  val unlift: (unit * 'a -> 'b * ('c * 'd)) -> 'a -> 'b * 'd
    1.38    val trace: ('a list -> 'b * 'c list) -> 'a list -> ('b * 'a list) * 'c list
    1.39 -  val prompt: string -> ('a -> 'b) -> 'a -> 'b
    1.40    val finite': 'a * ('a -> bool) -> ('b * 'a list -> 'c * ('d * 'a list))
    1.41      -> 'b * 'a list -> 'c * ('d * 'a list)
    1.42    val finite: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b * 'a list
    1.43    val read: 'a * ('a -> bool) -> ('a list -> 'b * 'a list) -> 'a list -> 'b option
    1.44 -  val error: ('a -> 'b) -> 'a -> 'b
    1.45 -  val source': string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    1.46 -    'b * ('b -> bool) -> ('d * 'b list -> 'e list * ('d * 'b list)) ->
    1.47 -    (bool * (string -> 'd * 'b list -> 'e list * ('d * 'b list))) option ->
    1.48 -    'd * 'a -> 'e list * ('d * 'c)
    1.49 -  val source: string -> (string -> 'a -> 'b list * 'a) -> ('b list * 'a -> 'c) ->
    1.50 -    'b * ('b -> bool) -> ('b list -> 'd list * 'b list) ->
    1.51 -    (bool * (string -> 'b list -> 'd list * 'b list)) option -> 'a -> 'd list * 'c
    1.52 -  val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.53 -  val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
    1.54 +  val drain: string -> (string -> 'a -> 'b list * 'a) -> 'b * ('b -> bool) ->
    1.55 +    ('c * 'b list -> 'd * ('e * 'b list)) -> ('c * 'b list) * 'a -> ('d * ('e * 'b list)) * 'a
    1.56    type lexicon
    1.57    val dest_lexicon: lexicon -> string list
    1.58    val make_lexicon: string list list -> lexicon
    1.59 @@ -91,10 +86,22 @@
    1.60  
    1.61  (** scanners **)
    1.62  
    1.63 +(* exceptions *)
    1.64 +
    1.65  exception MORE of string option;        (*need more input (prompt)*)
    1.66  exception FAIL of string option;        (*try alternatives (reason of failure)*)
    1.67  exception ABORT of string;              (*dead end*)
    1.68  
    1.69 +fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
    1.70 +fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
    1.71 +fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
    1.72 +fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
    1.73 +fun error scan xs = scan xs handle ABORT msg => Library.error msg;
    1.74 +
    1.75 +fun catch scan xs = scan xs
    1.76 +  handle ABORT msg => raise Fail msg
    1.77 +    | FAIL msg => raise Fail (the_default "Syntax error." msg);
    1.78 +
    1.79  
    1.80  (* scanner combinators *)
    1.81  
    1.82 @@ -161,6 +168,9 @@
    1.83  
    1.84  fun repeat1 scan = scan -- repeat scan >> op ::;
    1.85  
    1.86 +fun single scan = scan >> (fn x => [x]);
    1.87 +fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
    1.88 +
    1.89  fun max leq scan1 scan2 xs =
    1.90    (case (option scan1 xs, option scan2 xs) of
    1.91      ((NONE, _), (NONE, _)) => raise FAIL NONE           (*looses FAIL msg!*)
    1.92 @@ -201,21 +211,9 @@
    1.93  
    1.94  (* trace input *)
    1.95  
    1.96 -fun trace' scan (st, xs) =
    1.97 -  let val (y, (st', xs')) = scan (st, xs)
    1.98 -  in ((y, Library.take (length xs - length xs', xs)), (st', xs')) end;
    1.99 -
   1.100 -fun trace scan = unlift (trace' (lift scan));
   1.101 -
   1.102 -
   1.103 -(* exception handling *)
   1.104 -
   1.105 -fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg));
   1.106 -fun permissive scan xs = scan xs handle MORE _ => raise FAIL NONE | ABORT _ => raise FAIL NONE;
   1.107 -fun strict scan xs = scan xs handle MORE _ => raise FAIL NONE;
   1.108 -fun prompt str scan xs = scan xs handle MORE NONE => raise MORE (SOME str);
   1.109 -fun catch scan xs = scan xs handle ABORT msg => raise FAIL (SOME msg);
   1.110 -fun error scan xs = scan xs handle ABORT msg => Library.error msg;
   1.111 +fun trace scan xs =
   1.112 +  let val (y, xs') = scan xs
   1.113 +  in ((y, Library.take (length xs - length xs', xs)), xs') end;
   1.114  
   1.115  
   1.116  (* finite scans *)
   1.117 @@ -244,36 +242,11 @@
   1.118  
   1.119  (* infinite scans -- draining state-based source *)
   1.120  
   1.121 -fun drain def_prmpt get stopper scan ((state, xs), src) =
   1.122 -  (scan (state, xs), src) handle MORE prmpt =>
   1.123 -    (case get (the_default def_prmpt prmpt) src of
   1.124 +fun drain def_prompt get stopper scan ((state, xs), src) =
   1.125 +  (scan (state, xs), src) handle MORE prompt =>
   1.126 +    (case get (the_default def_prompt prompt) src of
   1.127        ([], _) => (finite' stopper scan (state, xs), src)
   1.128 -    | (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src'));
   1.129 -
   1.130 -fun source' def_prmpt get unget stopper scanner opt_recover (state, src) =
   1.131 -  let
   1.132 -    val draining = drain def_prmpt get stopper;
   1.133 -    val (xs, s) = get def_prmpt src;
   1.134 -    val inp = ((state, xs), s);
   1.135 -    val ((ys, (state', xs')), src') =
   1.136 -      if null xs then (([], (state, [])), s)
   1.137 -      else
   1.138 -        (case opt_recover of
   1.139 -          NONE => draining (error scanner) inp
   1.140 -        | SOME (interactive, recover) =>
   1.141 -            (draining (catch scanner) inp handle FAIL msg =>
   1.142 -              let val err = the_default "Syntax error." msg in
   1.143 -                if interactive then Output.error_msg err else ();
   1.144 -                draining (unless (lift (one (#2 stopper))) (recover err)) inp
   1.145 -              end));
   1.146 -  in (ys, (state', unget (xs', src'))) end;
   1.147 -
   1.148 -fun source def_prmpt get unget stopper scan opt_recover =
   1.149 -  unlift (source' def_prmpt get unget stopper (lift scan)
   1.150 -    (Option.map (fn (int, r) => (int, lift o r)) opt_recover));
   1.151 -
   1.152 -fun single scan = scan >> (fn x => [x]);
   1.153 -fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
   1.154 +    | (xs', src') => drain def_prompt get stopper scan ((state, xs @ xs'), src'));
   1.155  
   1.156  
   1.157