src/Pure/Isar/args.ML
author ballarin
Fri Aug 29 15:19:02 2003 +0200 (2003-08-29)
changeset 14174 f3cafd2929d5
parent 11503 4c25eef6f325
child 14563 4bf2d10461f3
permissions -rw-r--r--
Methods rule_tac etc support static (Isar) contexts.
wenzelm@5822
     1
(*  Title:      Pure/Isar/args.ML
wenzelm@5822
     2
    ID:         $Id$
wenzelm@5822
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8803
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5822
     5
wenzelm@5878
     6
Concrete argument syntax (of attributes and methods).
wenzelm@5822
     7
*)
wenzelm@5822
     8
wenzelm@5822
     9
signature ARGS =
wenzelm@5822
    10
sig
wenzelm@5822
    11
  type T
wenzelm@5822
    12
  val val_of: T -> string
wenzelm@5878
    13
  val pos_of: T -> Position.T
wenzelm@5878
    14
  val str_of: T -> string
wenzelm@9748
    15
  val string_of: T -> string
wenzelm@5878
    16
  val ident: string * Position.T -> T
wenzelm@5878
    17
  val string: string * Position.T -> T
wenzelm@5878
    18
  val keyword: string * Position.T -> T
wenzelm@5822
    19
  val stopper: T * (T -> bool)
wenzelm@5822
    20
  val not_eof: T -> bool
wenzelm@5878
    21
  val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
wenzelm@5878
    22
  val !!! : (T list -> 'a) -> T list -> 'a
wenzelm@5822
    23
  val $$$ : string -> T list -> string * T list
wenzelm@10035
    24
  val add: T list -> string * T list
wenzelm@10035
    25
  val del: T list -> string * T list
wenzelm@8803
    26
  val colon: T list -> string * T list
wenzelm@10035
    27
  val query: T list -> string * T list
wenzelm@10035
    28
  val bang: T list -> string * T list
wenzelm@10035
    29
  val query_colon: T list -> string * T list
wenzelm@10035
    30
  val bang_colon: T list -> string * T list
wenzelm@8803
    31
  val parens: (T list -> 'a * T list) -> T list -> 'a * T list
wenzelm@10150
    32
  val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
wenzelm@9809
    33
  val mode: string -> 'a * T list -> bool * ('a * T list)
wenzelm@5822
    34
  val name: T list -> string * T list
wenzelm@8687
    35
  val name_dummy: T list -> string option * T list
wenzelm@5878
    36
  val nat: T list -> int * T list
wenzelm@9538
    37
  val int: T list -> int * T list
wenzelm@5878
    38
  val var: T list -> indexname * T list
wenzelm@6447
    39
  val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    40
  val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    41
  val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@6447
    42
  val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
wenzelm@9504
    43
  val global_typ_no_norm: theory * T list -> typ * (theory * T list)
wenzelm@5878
    44
  val global_typ: theory * T list -> typ * (theory * T list)
wenzelm@5878
    45
  val global_term: theory * T list -> term * (theory * T list)
wenzelm@5878
    46
  val global_prop: theory * T list -> term * (theory * T list)
wenzelm@9504
    47
  val local_typ_no_norm: Proof.context * T list -> typ * (Proof.context * T list)
wenzelm@5878
    48
  val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
wenzelm@5878
    49
  val local_term: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@5878
    50
  val local_prop: Proof.context * T list -> term * (Proof.context * T list)
wenzelm@7553
    51
  val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
wenzelm@8536
    52
  val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
wenzelm@8536
    53
    -> ((int -> tactic) -> tactic) * ('a * T list)
wenzelm@5822
    54
  type src
wenzelm@5878
    55
  val src: (string * T list) * Position.T -> src
wenzelm@5878
    56
  val dest_src: src -> (string * T list) * Position.T
wenzelm@5878
    57
  val attribs: T list -> src list * T list
wenzelm@5878
    58
  val opt_attribs: T list -> src list * T list
wenzelm@8282
    59
  val syntax: string -> ('a * T list -> 'b * ('a * T list)) -> src -> 'a -> 'a * 'b
wenzelm@5822
    60
end;
wenzelm@5822
    61
wenzelm@5822
    62
structure Args: ARGS =
wenzelm@5822
    63
struct
wenzelm@5822
    64
wenzelm@5822
    65
wenzelm@5822
    66
(** datatype T **)
wenzelm@5822
    67
wenzelm@5822
    68
datatype kind = Ident | String | Keyword | EOF;
wenzelm@5878
    69
datatype T = Arg of kind * (string * Position.T);
wenzelm@5822
    70
wenzelm@5878
    71
fun val_of (Arg (_, (x, _))) = x;
wenzelm@5878
    72
fun pos_of (Arg (_, (_, pos))) = pos;
wenzelm@5822
    73
wenzelm@9901
    74
fun str_of (Arg (Ident, (x, _))) = x
wenzelm@5878
    75
  | str_of (Arg (String, (x, _))) = quote x
wenzelm@5878
    76
  | str_of (Arg (Keyword, (x, _))) = x
wenzelm@5878
    77
  | str_of (Arg (EOF, _)) = "end-of-text";
wenzelm@5822
    78
wenzelm@9748
    79
fun string_of (Arg (Ident, (x, _))) = x
wenzelm@9748
    80
  | string_of (Arg (String, (x, _))) = quote x
wenzelm@9748
    81
  | string_of (Arg (Keyword, (x, _))) = x
wenzelm@9748
    82
  | string_of (Arg (EOF, _)) = "";
wenzelm@9748
    83
wenzelm@5878
    84
fun arg kind x_pos = Arg (kind, x_pos);
wenzelm@5822
    85
val ident = arg Ident;
wenzelm@5822
    86
val string = arg String;
wenzelm@5822
    87
val keyword = arg Keyword;
wenzelm@5822
    88
wenzelm@5822
    89
wenzelm@5822
    90
(* eof *)
wenzelm@5822
    91
wenzelm@5878
    92
val eof = arg EOF ("", Position.none);
wenzelm@5822
    93
wenzelm@5822
    94
fun is_eof (Arg (EOF, _)) = true
wenzelm@5822
    95
  | is_eof _ = false;
wenzelm@5822
    96
wenzelm@5822
    97
val stopper = (eof, is_eof);
wenzelm@5822
    98
val not_eof = not o is_eof;
wenzelm@5822
    99
wenzelm@5822
   100
wenzelm@5822
   101
wenzelm@5822
   102
(** scanners **)
wenzelm@5822
   103
wenzelm@5878
   104
(* position *)
wenzelm@5878
   105
wenzelm@5878
   106
fun position scan = (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
wenzelm@5878
   107
wenzelm@5878
   108
wenzelm@5878
   109
(* cut *)
wenzelm@5878
   110
wenzelm@5878
   111
fun !!! scan =
wenzelm@5878
   112
  let
wenzelm@5878
   113
    fun get_pos [] = " (past end-of-text!)"
wenzelm@5878
   114
      | get_pos (Arg (_, (_, pos)) :: _) = Position.str_of pos;
wenzelm@5878
   115
wenzelm@5878
   116
    fun err (args, None) = "Argument syntax error" ^ get_pos args
wenzelm@5878
   117
      | err (args, Some msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
wenzelm@5878
   118
  in Scan.!! err scan end;
wenzelm@5878
   119
wenzelm@5878
   120
wenzelm@5822
   121
(* basic *)
wenzelm@5822
   122
wenzelm@5878
   123
fun $$$$ x = Scan.one (fn Arg (k, (y, _)) => (k = Ident orelse k = Keyword) andalso x = y);
wenzelm@5878
   124
fun $$$ x = $$$$ x >> val_of;
wenzelm@5878
   125
wenzelm@10035
   126
val add = $$$ "add";
wenzelm@10035
   127
val del = $$$ "del";
wenzelm@8803
   128
val colon = $$$ ":";
wenzelm@10035
   129
val query = $$$ "?";
wenzelm@10035
   130
val bang = $$$ "!";
wenzelm@10035
   131
val query_colon = $$$ "?:";
wenzelm@10035
   132
val bang_colon = $$$ "!:";
wenzelm@10035
   133
wenzelm@8803
   134
fun parens scan = $$$ "(" |-- scan --| $$$ ")";
wenzelm@10150
   135
fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
wenzelm@9809
   136
fun mode s = Scan.lift (Scan.optional (parens ($$$$ s) >> K true) false);
wenzelm@8803
   137
wenzelm@5878
   138
val name = Scan.one (fn Arg (k, (x, _)) => k = Ident orelse k = String) >> val_of;
wenzelm@8687
   139
val name_dummy = $$$ "_" >> K None || name >> Some;
wenzelm@5878
   140
wenzelm@8233
   141
val keyword_symid =
wenzelm@8233
   142
  Scan.one (fn Arg (k, (x, _)) => k = Keyword andalso OuterLex.is_sid x) >> val_of;
wenzelm@8233
   143
wenzelm@5878
   144
fun kind f = Scan.one (K true) :--
ballarin@14174
   145
  ((fn Arg (Ident, (x, _)) =>
wenzelm@5878
   146
    (case f x of Some y => Scan.succeed y | _ => Scan.fail)
ballarin@14174
   147
  | _ => Scan.fail)
ballarin@14174
   148
(* o (fn (t as Arg (i, (s, _))) =>
ballarin@14174
   149
  (warning (
ballarin@14174
   150
    (case i of Ident => "Ident: " | String => "String: "
ballarin@14174
   151
            | Keyword => "Keyword: " | EOF => "EOF: ")
ballarin@14174
   152
    ^ s); t)) *) ) >> #2;
wenzelm@5878
   153
wenzelm@5878
   154
val nat = kind Syntax.read_nat;
wenzelm@9538
   155
val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
wenzelm@5822
   156
ballarin@14174
   157
(* Read variable name.  Leading `?' may be omitted if name contains no dot. *)
ballarin@14174
   158
val var = kind (apsome #1 o
ballarin@14174
   159
      (fn s => (Some (Term.dest_Var (Syntax.read_var s)))
ballarin@14174
   160
         handle _ => (Some (Term.dest_Var (Syntax.read_var ("?" ^ s))))
ballarin@14174
   161
         handle _ => None));
wenzelm@5822
   162
wenzelm@5878
   163
(* enumerations *)
wenzelm@5878
   164
wenzelm@6447
   165
fun enum1 sep scan = scan -- Scan.repeat (Scan.lift ($$$ sep) |-- scan) >> op ::;
wenzelm@5878
   166
fun enum sep scan = enum1 sep scan || Scan.succeed [];
wenzelm@5878
   167
wenzelm@6447
   168
fun and_list1 scan = enum1 "and" scan;
wenzelm@6447
   169
fun and_list scan = enum "and" scan;
wenzelm@5878
   170
wenzelm@5822
   171
wenzelm@5878
   172
(* terms and types *)
wenzelm@5878
   173
wenzelm@5878
   174
fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
wenzelm@5878
   175
wenzelm@9504
   176
val global_typ_no_norm = gen_item (ProofContext.read_typ_no_norm o ProofContext.init);
wenzelm@5878
   177
val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
wenzelm@5878
   178
val global_term = gen_item (ProofContext.read_term o ProofContext.init);
wenzelm@5878
   179
val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
wenzelm@5822
   180
wenzelm@9504
   181
val local_typ_no_norm = gen_item ProofContext.read_typ_no_norm;
wenzelm@5878
   182
val local_typ = gen_item ProofContext.read_typ;
wenzelm@5878
   183
val local_term = gen_item ProofContext.read_term;
wenzelm@5878
   184
val local_prop = gen_item ProofContext.read_prop;
wenzelm@5878
   185
wenzelm@5878
   186
wenzelm@7553
   187
(* bang facts *)
wenzelm@7553
   188
wenzelm@7553
   189
val bang_facts = Scan.depend (fn ctxt =>
wenzelm@7553
   190
  ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
wenzelm@7553
   191
wenzelm@7553
   192
wenzelm@8536
   193
(* goal specification *)
wenzelm@8536
   194
wenzelm@8536
   195
(* range *)
wenzelm@8233
   196
wenzelm@8536
   197
val from_to =
wenzelm@8536
   198
  nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
wenzelm@8536
   199
  nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
wenzelm@8549
   200
  nat >> (fn i => fn tac => tac i) ||
wenzelm@8549
   201
  $$$$ "!" >> K ALLGOALS;
wenzelm@8536
   202
wenzelm@8536
   203
val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
wenzelm@8536
   204
fun goal_spec def = Scan.lift (Scan.optional goal def);
wenzelm@8233
   205
wenzelm@8233
   206
wenzelm@5878
   207
(* args *)
wenzelm@5878
   208
wenzelm@9126
   209
val exclude = explode "()[],";
wenzelm@5822
   210
wenzelm@5878
   211
fun atom_arg blk = Scan.one (fn Arg (k, (x, _)) =>
wenzelm@5878
   212
  k <> Keyword orelse not (x mem exclude) orelse blk andalso x = ",");
wenzelm@5878
   213
wenzelm@5878
   214
fun paren_args l r scan = $$$$ l -- !!! (scan true -- $$$$ r)
wenzelm@5878
   215
  >> (fn (x, (ys, z)) => x :: ys @ [z]);
wenzelm@5822
   216
wenzelm@5878
   217
fun args blk x = Scan.optional (args1 blk) [] x
wenzelm@5878
   218
and args1 blk x =
wenzelm@5878
   219
  ((Scan.repeat1
wenzelm@5878
   220
    (Scan.repeat1 (atom_arg blk) ||
wenzelm@5878
   221
      paren_args "(" ")" args ||
wenzelm@5878
   222
      paren_args "[" "]" args)) >> flat) x;
wenzelm@5822
   223
wenzelm@5822
   224
wenzelm@5822
   225
wenzelm@5822
   226
(** type src **)
wenzelm@5822
   227
wenzelm@5878
   228
datatype src = Src of (string * T list) * Position.T;
wenzelm@5822
   229
wenzelm@5878
   230
val src = Src;
wenzelm@5878
   231
fun dest_src (Src src) = src;
wenzelm@5878
   232
wenzelm@5878
   233
fun err_in_src kind msg (Src ((s, args), pos)) =
wenzelm@11503
   234
  error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": " ^ msg ^ "\n  " ^
wenzelm@5878
   235
    space_implode " " (map str_of args));
wenzelm@5822
   236
wenzelm@5822
   237
wenzelm@5822
   238
(* argument syntax *)
wenzelm@5822
   239
wenzelm@8282
   240
fun syntax kind scan (src as Src ((s, args), pos)) st =
wenzelm@9901
   241
  (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
wenzelm@9901
   242
    (Some x, (st', [])) => (st', x)
wenzelm@9901
   243
  | (_, (_, args')) => err_in_src kind "bad arguments" (Src ((s, args'), pos)));
wenzelm@5878
   244
wenzelm@5878
   245
wenzelm@5878
   246
(* attribs *)
wenzelm@5878
   247
wenzelm@6447
   248
fun list1 scan = scan -- Scan.repeat ($$$ "," |-- scan) >> op ::;
wenzelm@6447
   249
fun list scan = list1 scan || Scan.succeed [];
wenzelm@6447
   250
wenzelm@8233
   251
val attrib = position ((keyword_symid || name) -- !!! (args false)) >> src;
wenzelm@5878
   252
val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]");
wenzelm@5878
   253
val opt_attribs = Scan.optional attribs [];
wenzelm@5822
   254
wenzelm@5822
   255
wenzelm@5822
   256
end;