added ::: / @@@ scanner combinators;
authorwenzelm
Mon Jan 28 22:27:19 2008 +0100 (2008-01-28)
changeset 25999f8bcd311d501
parent 25998 f38dc602a926
child 26000 b629b4f2026c
added ::: / @@@ scanner combinators;
src/HOL/Statespace/state_space.ML
src/HOL/Tools/res_reconstruct.ML
src/Pure/General/scan.ML
src/Pure/Isar/args.ML
src/Pure/Isar/class.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Syntax/simple_syntax.ML
src/Tools/code/code_name.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Mon Jan 28 18:18:19 2008 +0100
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Mon Jan 28 22:27:19 2008 +0100
     1.3 @@ -701,7 +701,7 @@
     1.4  
     1.5  val comp = P.name -- (P.$$$ "::" |-- P.!!! P.typ);
     1.6  fun plus1_unless test scan =
     1.7 -  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
     1.8 +  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
     1.9  
    1.10  val mapsto = P.$$$ "=";
    1.11  val rename = P.name -- (mapsto |-- P.name);
     2.1 --- a/src/HOL/Tools/res_reconstruct.ML	Mon Jan 28 18:18:19 2008 +0100
     2.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Mon Jan 28 22:27:19 2008 +0100
     2.3 @@ -70,7 +70,7 @@
     2.4  val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
     2.5  
     2.6  (*Generalized FO terms, which include filenames, numbers, etc.*)
     2.7 -fun termlist x = (term -- Scan.repeat ($$"," |-- term) >> op::) x
     2.8 +fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
     2.9  and term x = (quoted >> atom || integer>>Int || truefalse ||
    2.10                Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
    2.11                $$"(" |-- term --| $$")" ||
    2.12 @@ -88,7 +88,7 @@
    2.13  fun literal x = ($$"~" |-- literal >> negate ||
    2.14                   (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x;
    2.15  
    2.16 -val literals = literal -- Scan.repeat ($$"|" |-- literal) >> op:: ;
    2.17 +val literals = literal ::: Scan.repeat ($$"|" |-- literal);
    2.18  
    2.19  (*Clause: a list of literals separated by the disjunction sign*)
    2.20  val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
     3.1 --- a/src/Pure/General/scan.ML	Mon Jan 28 18:18:19 2008 +0100
     3.2 +++ b/src/Pure/General/scan.ML	Mon Jan 28 22:27:19 2008 +0100
     3.3 @@ -6,6 +6,7 @@
     3.4  *)
     3.5  
     3.6  infix 5 -- :-- :|-- |-- --| ^^;
     3.7 +infixr 5 ::: @@@;
     3.8  infix 3 >>;
     3.9  infixr 0 ||;
    3.10  
    3.11 @@ -27,6 +28,8 @@
    3.12    val --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e
    3.13    (*concatenation*)
    3.14    val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c
    3.15 +  val ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd
    3.16 +  val @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd
    3.17    (*one element literal*)
    3.18    val $$ : string -> string list -> string * string list
    3.19    val ~$$ : string -> string list -> string * string list
    3.20 @@ -120,6 +123,8 @@
    3.21  fun (scan1 |-- scan2) = scan1 -- scan2 >> #2;
    3.22  fun (scan1 --| scan2) = scan1 -- scan2 >> #1;
    3.23  fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^;
    3.24 +fun (scan1 ::: scan2) = scan1 -- scan2 >> op ::;
    3.25 +fun (scan1 @@@ scan2) = scan1 -- scan2 >> op @;
    3.26  
    3.27  
    3.28  (* generic scanners *)
    3.29 @@ -154,7 +159,7 @@
    3.30        if pred x then apfst (cons x) (many pred xs)
    3.31        else ([], lst);
    3.32  
    3.33 -fun many1 pred = one pred -- many pred >> op ::;
    3.34 +fun many1 pred = one pred ::: many pred;
    3.35  
    3.36  fun optional scan def = scan || succeed def;
    3.37  fun option scan = (scan >> SOME) || succeed NONE;
    3.38 @@ -167,7 +172,7 @@
    3.39        | SOME (y, xs') => rep (y :: ys) xs');
    3.40    in rep [] end;
    3.41  
    3.42 -fun repeat1 scan = scan -- repeat scan >> op ::;
    3.43 +fun repeat1 scan = scan ::: repeat scan;
    3.44  
    3.45  fun single scan = scan >> (fn x => [x]);
    3.46  fun bulk scan = scan -- repeat (permissive scan) >> (op ::);
     4.1 --- a/src/Pure/Isar/args.ML	Mon Jan 28 18:18:19 2008 +0100
     4.2 +++ b/src/Pure/Isar/args.ML	Mon Jan 28 22:27:19 2008 +0100
     4.3 @@ -288,10 +288,10 @@
     4.4  
     4.5  (* enumerations *)
     4.6  
     4.7 -fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
     4.8 +fun list1 scan = scan ::: Scan.repeat ($$$ "," |-- scan);
     4.9  fun list scan = list1 scan || Scan.succeed [];
    4.10  
    4.11 -fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
    4.12 +fun enum1 sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
    4.13  fun enum sep scan = enum1 sep scan || Scan.succeed [];
    4.14  
    4.15  fun and_list1 scan = enum1 "and" scan;
     5.1 --- a/src/Pure/Isar/class.ML	Mon Jan 28 18:18:19 2008 +0100
     5.2 +++ b/src/Pure/Isar/class.ML	Mon Jan 28 22:27:19 2008 +0100
     5.3 @@ -763,7 +763,7 @@
     5.4        ((junk |--
     5.5          (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
     5.6          --| junk))
     5.7 -      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
     5.8 +      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     5.9    in
    5.10      explode #> scan_valids #> implode
    5.11    end;
     6.1 --- a/src/Pure/Isar/outer_parse.ML	Mon Jan 28 18:18:19 2008 +0100
     6.2 +++ b/src/Pure/Isar/outer_parse.ML	Mon Jan 28 22:27:19 2008 +0100
     6.3 @@ -185,7 +185,7 @@
     6.4  
     6.5  (* enumerations *)
     6.6  
     6.7 -fun enum1 sep scan = scan -- Scan.repeat ($$$ sep |-- !!! scan) >> op ::;
     6.8 +fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
     6.9  fun enum sep scan = enum1 sep scan || Scan.succeed [];
    6.10  
    6.11  fun list1 scan = enum1 "," scan;
     7.1 --- a/src/Pure/Isar/spec_parse.ML	Mon Jan 28 18:18:19 2008 +0100
     7.2 +++ b/src/Pure/Isar/spec_parse.ML	Mon Jan 28 22:27:19 2008 +0100
     7.3 @@ -108,7 +108,7 @@
     7.4      >> (curry Element.Notes "");
     7.5  
     7.6  fun plus1_unless test scan =
     7.7 -  scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::;
     7.8 +  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
     7.9  
    7.10  val rename = P.name -- Scan.option P.mixfix;
    7.11  
     8.1 --- a/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 18:18:19 2008 +0100
     8.2 +++ b/src/Pure/Syntax/simple_syntax.ML	Mon Jan 28 22:27:19 2008 +0100
     8.3 @@ -44,8 +44,8 @@
     8.4  (* basic scanners *)
     8.5  
     8.6  fun $$ s = Scan.some (fn Lexicon.Token s' => if s = s' then SOME s else NONE | _ => NONE);
     8.7 -fun enum1 s scan = scan -- Scan.repeat ($$ s |-- scan) >> op ::;
     8.8 -fun enum2 s scan = scan -- Scan.repeat1 ($$ s |-- scan) >> op ::;
     8.9 +fun enum1 s scan = scan ::: Scan.repeat ($$ s |-- scan);
    8.10 +fun enum2 s scan = scan ::: Scan.repeat1 ($$ s |-- scan);
    8.11  
    8.12  val tfree = Scan.some (fn Lexicon.TFreeSy s => SOME s | _ => NONE);
    8.13  val ident = Scan.some (fn Lexicon.IdentSy s => SOME s | _ => NONE);
     9.1 --- a/src/Tools/code/code_name.ML	Mon Jan 28 18:18:19 2008 +0100
     9.2 +++ b/src/Tools/code/code_name.ML	Mon Jan 28 22:27:19 2008 +0100
     9.3 @@ -49,7 +49,7 @@
     9.4        ((junk |--
     9.5          (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.many is_valid >> implode)
     9.6          --| junk))
     9.7 -      -- Scan.repeat ((Scan.many1 is_valid >> implode) --| junk) >> op ::);
     9.8 +      ::: Scan.repeat ((Scan.many1 is_valid >> implode) --| junk));
     9.9      fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs
    9.10        else if lower then (if forall Symbol.is_ascii_upper cs
    9.11          then map else nth_map 0) Symbol.to_ascii_lower cs