src/Pure/Isar/args.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7553 af3a1fe87c42
child 8089 8efec140c5e4
permissions -rw-r--r--
removed extra shyps error;
wenzelm@5822
     1
(*  Title:      Pure/Isar/args.ML
wenzelm@5822
     2
    ID:         $Id$
wenzelm@5822
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5822
     4
wenzelm@5878
     5
Concrete argument syntax (of attributes and methods).
wenzelm@5822
     6
*)
wenzelm@5822
     7
wenzelm@5822
     8
signature ARGS =
wenzelm@5822
     9
sig
wenzelm@5822
    10
  type T
wenzelm@5822
    11
  val val_of: T -> string
wenzelm@5878
    12
  val pos_of: T -> Position.T
wenzelm@5878
    13
  val str_of: T -> string
wenzelm@5878
    14
  val ident: string * Position.T -> T
wenzelm@5878
    15
  val string: string * Position.T -> T
wenzelm@5878
    16
  val keyword: string * Position.T -> T
wenzelm@5822
    17
  val stopper: T * (T -> bool)
wenzelm@5822
    18
  val not_eof: T -> bool
wenzelm@5878
    19
  val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
wenzelm@5878
    20
  val !!! : (T list -> 'a) -> T list -> 'a
wenzelm@5822
    21
  val $$$ : string -> T list -> string * T list
wenzelm@5822
    22
  val name: T list -> string * T list
wenzelm@5878
    23
  val nat: T list -> int * T list
wenzelm@5878
    24
  val var: T list -> indexname * T list
wenzelm@6447
    25
  val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    26
  val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    27
  val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    28
  val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@5878
    29
  val global_typ: theory * T list -> typ * (theory * T list)
wenzelm@5878
    30
  val global_term: theory * T list -> term * (theory * T list)
wenzelm@5878
    31
  val global_prop: theory * T list -> term * (theory * T list)
wenzelm@5934
    32
  val global_term_pat: theory * T list -> term * (theory * T list)
wenzelm@5934
    33
  val global_prop_pat: theory * T list -> term * (theory * T list)
wenzelm@5878
    34
  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
wenzelm@5878
    35
  val local_term: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@5878
    36
  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@5934
    37
  val local_term_pat: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@5934
    38
  val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@7553
    39
  val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
wenzelm@5822
    40
  type src
wenzelm@5878
    41
  val src: (string * T list) * Position.T -> src
wenzelm@5878
    42
  val dest_src: src -> (string * T list) * Position.T
wenzelm@5878
    43
  val attribs: T list -> src list * T list
wenzelm@5878
    44
  val opt_attribs: T list -> src list * T list
wenzelm@5878
    45
  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> 'a -> src -> 'a * 'b
wenzelm@5822
    46
end;
wenzelm@5822
    47
wenzelm@5822
    48
structure Args: ARGS =
wenzelm@5822
    49
struct
wenzelm@5822
    50
wenzelm@5822
    51
wenzelm@5822
    52
(** datatype T **)
wenzelm@5822
    53
wenzelm@5822
    54
datatype kind = Ident | String | Keyword | EOF;
wenzelm@5878
    55
datatype T = Arg of kind * (string * Position.T);
wenzelm@5822
    56
wenzelm@5878
    57
fun val_of (Arg (_, (x, _))) = x;
wenzelm@5878
    58
fun pos_of (Arg (_, (_, pos))) = pos;
wenzelm@5822
    59
wenzelm@5878
    60
fun str_of (Arg (Ident, (x, _))) = enclose "'" "'" x
wenzelm@5878
    61
  | str_of (Arg (String, (x, _))) = quote x
wenzelm@5878
    62
  | str_of (Arg (Keyword, (x, _))) = x
wenzelm@5878
    63
  | str_of (Arg (EOF, _)) = "end-of-text";
wenzelm@5822
    64
wenzelm@5878
    65
fun arg kind x_pos = Arg (kind, x_pos);
wenzelm@5822
    66
val ident = arg Ident;
wenzelm@5822
    67
val string = arg String;
wenzelm@5822
    68
val keyword = arg Keyword;
wenzelm@5822
    69
wenzelm@5822
    70
wenzelm@5822
    71
(* eof *)
wenzelm@5822
    72
wenzelm@5878
    73
val eof = arg EOF ("", Position.none);
wenzelm@5822
    74
wenzelm@5822
    75
fun is_eof (Arg (EOF, _)) = true
wenzelm@5822
    76
  | is_eof _ = false;
wenzelm@5822
    77
wenzelm@5822
    78
val stopper = (eof, is_eof);
wenzelm@5822
    79
val not_eof = not o is_eof;
wenzelm@5822
    80
wenzelm@5822
    81
wenzelm@5822
    82
wenzelm@5822
    83
(** scanners **)
wenzelm@5822
    84
wenzelm@5878
    85
(* position *)
wenzelm@5878
    86
wenzelm@5878
    87
fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
wenzelm@5878
    88
wenzelm@5878
    89
wenzelm@5878
    90
(* cut *)
wenzelm@5878
    91
wenzelm@5878
    92
fun !!! scan =
wenzelm@5878
    93
  let
wenzelm@5878
    94
    fun get_pos [] = " (past end-of-text!)"
wenzelm@5878
    95
      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
wenzelm@5878
    96
wenzelm@5878
    97
    fun err (args, None) = "Argument syntax error" ^ get_pos args
wenzelm@5878
    98
      | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
wenzelm@5878
    99
  in Scan.!! err scan end;
wenzelm@5878
   100
wenzelm@5878
   101
wenzelm@5822
   102
(* basic *)
wenzelm@5822
   103
wenzelm@5878
   104
fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
wenzelm@5878
   105
fun $$$ x = $$$$ x >> val_of;
wenzelm@5878
   106
wenzelm@5878
   107
val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
wenzelm@5878
   108
wenzelm@5878
   109
fun kind f = Scan.one (K true) :--
wenzelm@5878
   110
  (fn Arg (Ident, (x, _)) =>
wenzelm@5878
   111
    (case f x of Some y => Scan.succeed y | _ => Scan.fail)
wenzelm@5878
   112
  | _ => Scan.fail) >> #2;
wenzelm@5878
   113
wenzelm@5878
   114
val nat = kind Syntax.read_nat;
wenzelm@5878
   115
val var = kind (apsome #1 o try Term.dest_Var o Syntax.read_var);
wenzelm@5822
   116
wenzelm@5822
   117
wenzelm@5878
   118
(* enumerations *)
wenzelm@5878
   119
wenzelm@6447
   120
fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
wenzelm@5878
   121
fun enum sep scan = enum1 sep scan || Scan.succeed [];
wenzelm@5878
   122
wenzelm@6447
   123
fun and_list1 scan = enum1 "and" scan;
wenzelm@6447
   124
fun and_list scan = enum "and" scan;
wenzelm@5878
   125
wenzelm@5822
   126
wenzelm@5878
   127
(* terms and types *)
wenzelm@5878
   128
wenzelm@5878
   129
fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
wenzelm@5878
   130
wenzelm@5878
   131
val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
wenzelm@5878
   132
val global_term = gen_item (ProofContext.read_term o ProofContext.init);
wenzelm@5878
   133
val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
wenzelm@5934
   134
val global_term_pat = gen_item (ProofContext.read_term_pat o ProofContext.init);
wenzelm@5934
   135
val global_prop_pat = gen_item (ProofContext.read_prop_pat o ProofContext.init);
wenzelm@5822
   136
wenzelm@5878
   137
val local_typ = gen_item ProofContext.read_typ;
wenzelm@5878
   138
val local_term = gen_item ProofContext.read_term;
wenzelm@5878
   139
val local_prop = gen_item ProofContext.read_prop;
wenzelm@5934
   140
val local_term_pat = gen_item ProofContext.read_term_pat;
wenzelm@5934
   141
val local_prop_pat = gen_item ProofContext.read_prop_pat;
wenzelm@5878
   142
wenzelm@5878
   143
wenzelm@7553
   144
(* bang facts *)
wenzelm@7553
   145
wenzelm@7553
   146
val bang_facts = Scan.depend (fn ctxt =>
wenzelm@7553
   147
  ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
wenzelm@7553
   148
wenzelm@7553
   149
wenzelm@5878
   150
(* args *)
wenzelm@5878
   151
wenzelm@5878
   152
val exclude = explode "(){}[],";
wenzelm@5822
   153
wenzelm@5878
   154
fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
wenzelm@5878
   155
  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
wenzelm@5878
   156
wenzelm@5878
   157
fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
wenzelm@5878
   158
  >> (fn (x, (ys, z)) => x :: ys @ [z]);
wenzelm@5822
   159
wenzelm@5878
   160
fun args blk x = Scan.optional (args1 blk) [] x
wenzelm@5878
   161
and args1 blk x =
wenzelm@5878
   162
  ((Scan.repeat1
wenzelm@5878
   163
    (Scan.repeat1 (atom_arg blk) ||
wenzelm@5878
   164
      paren_args "(" ")" args ||
wenzelm@5878
   165
      paren_args "{" "}" args ||
wenzelm@5878
   166
      paren_args "[" "]" args)) >> flat) x;
wenzelm@5822
   167
wenzelm@5822
   168
wenzelm@5822
   169
wenzelm@5822
   170
(** type src **)
wenzelm@5822
   171
wenzelm@5878
   172
datatype src = Src of (string * T list) * Position.T;
wenzelm@5822
   173
wenzelm@5878
   174
val src = Src;
wenzelm@5878
   175
fun dest_src (Src src) = src;
wenzelm@5878
   176
wenzelm@5878
   177
fun err_in_src kind msg (Src ((s, args), pos)) =
wenzelm@5878
   178
  error (kind ^ " " ^ s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
wenzelm@5878
   179
    space_implode " " (map str_of args));
wenzelm@5822
   180
wenzelm@5822
   181
wenzelm@5822
   182
(* argument syntax *)
wenzelm@5822
   183
wenzelm@5878
   184
fun syntax kind scan st (src as Src ((s, args), pos)) =
wenzelm@5878
   185
  (case handle_error (Scan.error (Scan.finite' stopper (Scan.option scan))) (st, args) of
wenzelm@5878
   186
    OK (Some x, (st', [])) => (st', x)
wenzelm@5878
   187
  | OK (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos))
wenzelm@5911
   188
  | Error msg => err_in_src kind ("\n" ^ msg) src);
wenzelm@5878
   189
wenzelm@5878
   190
wenzelm@5878
   191
(* attribs *)
wenzelm@5878
   192
wenzelm@6447
   193
fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
wenzelm@6447
   194
fun list scan = list1 scan || Scan.succeed [];
wenzelm@6447
   195
wenzelm@5878
   196
val attrib = position (name -- !!! (args false)) >> src;
wenzelm@5878
   197
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
wenzelm@5878
   198
val opt_attribs = Scan.optional attribs [];
wenzelm@5822
   199
wenzelm@5822
   200
wenzelm@5822
   201
end;