src/Pure/Isar/args.ML
author wenzelm
Mon, 09 Nov 1998 15:32:02 +0100
changeset 5822 3f824514ad88
child 5878 769abc29bb8e
permissions -rw-r--r--
Concrete argument syntax (for attributes, methods etc.).
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5822
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/args.ML
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     4
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     5
Concrete argument syntax (for attributes, methods etc.).
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     6
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     7
TODO:
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     8
  - sectioned: generalize sname to attributed thms;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
     9
*)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    10
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    11
signature ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    12
sig
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    13
  type T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    14
  val val_of: T -> string
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    15
  val ident: string -> T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    16
  val string: string -> T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    17
  val keyword: string -> T
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    18
  val stopper: T * (T -> bool)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    19
  val not_eof: T -> bool
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    20
  val $$$ : string -> T list -> string * T list
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    21
  val name: T list -> string * T list
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    22
  val sectioned: string list -> T list -> (string list * (string * string list) list) * T list
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    23
  type src
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    24
  val syntax: string -> (T list -> 'a * T list) -> ('a -> 'b) -> src -> 'b
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    25
end;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    26
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    27
structure Args: ARGS =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    28
struct
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    29
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    30
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    31
(** datatype T **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    32
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    33
datatype kind = Ident | String | Keyword | EOF;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    34
datatype T = Arg of kind * string;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    35
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    36
fun val_of (Arg (_, x)) = x;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    37
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    38
fun str_of (Arg (Ident, x)) = enclose "'" "'" x
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    39
  | str_of (Arg (String, x)) = quote x
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    40
  | str_of (Arg (Keyword, x)) = x;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    41
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    42
fun arg kind x = Arg (kind, x);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    43
val ident = arg Ident;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    44
val string = arg String;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    45
val keyword = arg Keyword;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    46
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    47
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    48
(* eof *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    49
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    50
val eof = arg EOF "";
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    51
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    52
fun is_eof (Arg (EOF, _)) = true
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    53
  | is_eof _ = false;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    54
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    55
val stopper = (eof, is_eof);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    56
val not_eof = not o is_eof;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    57
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    58
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    59
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    60
(** scanners **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    61
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    62
(* basic *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    63
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    64
fun $$$ x = Scan.one (fn Arg (k, y) => (k = Ident orelse k = Keyword) andalso x = y) >> val_of;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    65
val name = Scan.one (fn (Arg (k, x)) => k = Ident orelse k = String) >> val_of;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    66
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    67
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    68
(* sections *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    69
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    70
val no_colon = Scan.one (fn Arg (k, x) => k = String orelse x <> ":");
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    71
val sname = name --| Scan.ahead no_colon;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    72
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    73
fun sect s = ($$$ s --| $$$ ":") -- Scan.repeat sname;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    74
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    75
fun any_sect [] = Scan.fail
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    76
  | any_sect (s :: ss) = sect s || any_sect ss;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    77
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    78
fun sectioned ss =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    79
  Scan.repeat sname -- Scan.repeat (any_sect ss);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    80
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    81
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    82
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    83
(** type src **)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    84
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    85
type src = (string * T list) * Position.T;
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    86
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    87
fun err_in_src kind msg ((s, args), pos) =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    88
  error (space_implode " " (kind :: s :: map str_of args) ^ Position.str_of pos ^ ": " ^ msg);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    89
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    90
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    91
(* argument syntax *)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    92
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    93
fun syntax kind scan f (src as ((s, args), pos)) =
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    94
  (case handle_error (Scan.error (Scan.finite stopper scan)) args of
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    95
    OK (x, []) => f x
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    96
  | OK (_, args') => err_in_src kind "bad arguments" ((s, args'), pos)
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    97
  | Error msg => err_in_src kind ("\n" ^ msg) src);
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    98
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
    99
3f824514ad88 Concrete argument syntax (for attributes, methods etc.).
wenzelm
parents:
diff changeset
   100
end;