1.1 --- a/src/Pure/Isar/args.ML Sat Aug 09 22:43:52 2008 +0200
1.2 +++ b/src/Pure/Isar/args.ML Sat Aug 09 22:43:53 2008 +0200
1.3 @@ -2,29 +2,13 @@
1.4 ID: $Id$
1.5 Author: Markus Wenzel, TU Muenchen
1.6
1.7 -Concrete argument syntax of attributes, methods etc. -- with special
1.8 -support for embedded values and static binding.
1.9 +Parsing with implicit value assigment. Concrete argument syntax of
1.10 +attributes, methods etc.
1.11 *)
1.12
1.13 signature ARGS =
1.14 sig
1.15 - datatype value =
1.16 - Text of string | Typ of typ | Term of term | Fact of thm list |
1.17 - Attribute of morphism -> attribute
1.18 - type T
1.19 - val string_of: T -> string
1.20 - val mk_ident: string * Position.T -> T
1.21 - val mk_string: string * Position.T -> T
1.22 - val mk_alt_string: string * Position.T -> T
1.23 - val mk_keyword: string * Position.T -> T
1.24 - val mk_text: string -> T
1.25 - val mk_typ: typ -> T
1.26 - val mk_term: term -> T
1.27 - val mk_fact: thm list -> T
1.28 - val mk_attribute: (morphism -> attribute) -> T
1.29 - val eof: T
1.30 - val stopper: T Scan.stopper
1.31 - val not_eof: T -> bool
1.32 + type T = OuterLex.token
1.33 type src
1.34 val src: (string * T list) * Position.T -> src
1.35 val dest_src: src -> (string * T list) * Position.T
1.36 @@ -33,12 +17,9 @@
1.37 val morph_values: morphism -> src -> src
1.38 val maxidx_values: src -> int -> int
1.39 val assignable: src -> src
1.40 - val assign: value option -> T -> unit
1.41 val closure: src -> src
1.42 val context: Context.generic * T list -> Context.proof * (Context.generic * T list)
1.43 val theory: Context.generic * T list -> Context.theory * (Context.generic * T list)
1.44 - val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b
1.45 - val !!! : (T list -> 'a) -> T list -> 'a
1.46 val $$$ : string -> T list -> string * T list
1.47 val add: T list -> string * T list
1.48 val del: T list -> string * T list
1.49 @@ -51,21 +32,11 @@
1.50 val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
1.51 val mode: string -> 'a * T list -> bool * ('a * T list)
1.52 val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
1.53 - val terminator: T list -> T * T list
1.54 val name: T list -> string * T list
1.55 val alt_name: T list -> string * T list
1.56 val symbol: T list -> string * T list
1.57 val liberal_name: T list -> string * T list
1.58 - val nat: T list -> int * T list
1.59 - val int: T list -> int * T list
1.60 val var: T list -> indexname * T list
1.61 - val list: (T list -> 'a * T list) -> T list -> 'a list * T list
1.62 - val list1: (T list -> 'a * T list) -> T list -> 'a list * T list
1.63 - val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
1.64 - val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
1.65 - val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
1.66 - val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
1.67 - val ahead: T list -> T * T list
1.68 val internal_text: T list -> string * T list
1.69 val internal_typ: T list -> typ * T list
1.70 val internal_term: T list -> term * T list
1.71 @@ -85,11 +56,11 @@
1.72 val tyname: Context.generic * T list -> string * (Context.generic * T list)
1.73 val const: Context.generic * T list -> string * (Context.generic * T list)
1.74 val const_proper: Context.generic * T list -> string * (Context.generic * T list)
1.75 - val thm_sel: T list -> Facts.interval list * T list
1.76 val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list)
1.77 val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
1.78 -> ((int -> tactic) -> tactic) * ('a * T list)
1.79 - val generic_args1: (string -> bool) -> T list -> T list * T list
1.80 + val parse: OuterLex.token list -> T list * OuterLex.token list
1.81 + val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
1.82 val attribs: (string -> string) -> T list -> src list * T list
1.83 val opt_attribs: (string -> string) -> T list -> src list * T list
1.84 val thm_name: (string -> string) -> string -> T list -> (string * src list) * T list
1.85 @@ -102,72 +73,15 @@
1.86 structure Args: ARGS =
1.87 struct
1.88
1.89 -
1.90 -(** datatype T **)
1.91 -
1.92 -(*An argument token is a symbol (with raw string value), together with
1.93 - an optional assigned internal value. Note that an assignable ref
1.94 - designates an intermediate state of internalization -- it is NOT
1.95 - meant to persist.*)
1.96 -
1.97 -datatype kind = Ident | String | AltString | Keyword | EOF;
1.98 -
1.99 -type symbol = kind * string * Position.T;
1.100 -
1.101 -datatype value =
1.102 - Text of string |
1.103 - Typ of typ |
1.104 - Term of term |
1.105 - Fact of thm list |
1.106 - Attribute of morphism -> attribute;
1.107 -
1.108 -datatype slot =
1.109 - Empty |
1.110 - Value of value option |
1.111 - Assignable of value option ref;
1.112 -
1.113 -datatype T = Arg of symbol * slot;
1.114 -
1.115 -fun string_of (Arg ((Ident, x, _), _)) = x
1.116 - | string_of (Arg ((String, x, _), _)) = quote x
1.117 - | string_of (Arg ((AltString, x, _), _)) = enclose "`" "`" x
1.118 - | string_of (Arg ((Keyword, x, _), _)) = x
1.119 - | string_of (Arg ((EOF, _, _), _)) = "";
1.120 -
1.121 -fun sym_of (Arg ((_, x, _), _)) = x;
1.122 -fun pos_of (Arg ((_, _, pos), _)) = pos;
1.123 -
1.124 -
1.125 -(* basic constructors *)
1.126 -
1.127 -fun mk_symbol k (x, p) = Arg ((k, x, p), Empty);
1.128 -fun mk_value k v = Arg ((Keyword, k, Position.none), Value (SOME v));
1.129 -
1.130 -val mk_ident = mk_symbol Ident;
1.131 -val mk_string = mk_symbol String;
1.132 -val mk_alt_string = mk_symbol AltString;
1.133 -val mk_keyword = mk_symbol Keyword;
1.134 -val mk_text = mk_value "<text>" o Text;
1.135 -val mk_typ = mk_value "<typ>" o Typ;
1.136 -val mk_term = mk_value "<term>" o Term;
1.137 -val mk_fact = mk_value "<fact>" o Fact;
1.138 -val mk_attribute = mk_value "<attribute>" o Attribute;
1.139 -
1.140 -
1.141 -(* eof *)
1.142 -
1.143 -val eof = mk_symbol EOF ("", Position.none);
1.144 -
1.145 -fun is_eof (Arg ((EOF, _, _), _)) = true
1.146 - | is_eof _ = false;
1.147 -
1.148 -val stopper = Scan.stopper (K eof) is_eof;
1.149 -val not_eof = not o is_eof;
1.150 +structure T = OuterLex;
1.151 +structure P = OuterParse;
1.152
1.153
1.154
1.155 (** datatype src **)
1.156
1.157 +type T = T.token;
1.158 +
1.159 datatype src = Src of (string * T list) * Position.T;
1.160
1.161 val src = Src;
1.162 @@ -176,12 +90,13 @@
1.163 fun pretty_src ctxt src =
1.164 let
1.165 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
1.166 - fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s)
1.167 - | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T
1.168 - | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t
1.169 - | prt (Arg (_, Value (SOME (Fact ths)))) =
1.170 - Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
1.171 - | prt arg = Pretty.str (string_of arg);
1.172 + fun prt arg =
1.173 + (case T.get_value arg of
1.174 + SOME (T.Text s) => Pretty.str (quote s)
1.175 + | SOME (T.Typ T) => Syntax.pretty_typ ctxt T
1.176 + | SOME (T.Term t) => Syntax.pretty_term ctxt t
1.177 + | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
1.178 + | _ => Pretty.str (T.unparse arg));
1.179 val (s, args) = #1 (dest_src src);
1.180 in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
1.181
1.182 @@ -191,43 +106,26 @@
1.183
1.184 (* values *)
1.185
1.186 -fun map_value f (Arg (s, Value (SOME v))) = Arg (s, Value (SOME (f v)))
1.187 - | map_value _ arg = arg;
1.188 +fun morph_values phi = map_args (T.map_value
1.189 + (fn T.Text s => T.Text s
1.190 + | T.Typ T => T.Typ (Morphism.typ phi T)
1.191 + | T.Term t => T.Term (Morphism.term phi t)
1.192 + | T.Fact ths => T.Fact (Morphism.fact phi ths)
1.193 + | T.Attribute att => T.Attribute (Morphism.transform phi att)));
1.194
1.195 -fun morph_values phi = map_args (map_value
1.196 - (fn Text s => Text s
1.197 - | Typ T => Typ (Morphism.typ phi T)
1.198 - | Term t => Term (Morphism.term phi t)
1.199 - | Fact ths => Fact (Morphism.fact phi ths)
1.200 - | Attribute att => Attribute (Morphism.transform phi att)));
1.201 +fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg =>
1.202 + (case T.get_value arg of
1.203 + SOME (T.Typ T) => Term.maxidx_typ T
1.204 + | SOME (T.Term t) => Term.maxidx_term t
1.205 + | SOME (T.Fact ths) => fold Thm.maxidx_thm ths
1.206 + | _ => I));
1.207
1.208 -fun maxidx_values (Src ((_, args), _)) = args |> fold
1.209 - (fn (Arg (_, Value (SOME (Typ T)))) => Term.maxidx_typ T
1.210 - | (Arg (_, Value (SOME (Term t)))) => Term.maxidx_term t
1.211 - | (Arg (_, Value (SOME (Fact ths)))) => fold Thm.maxidx_thm ths
1.212 - | _ => I);
1.213 +val assignable = map_args T.assignable;
1.214 +val closure = map_args T.closure;
1.215
1.216
1.217 -(* static binding *)
1.218
1.219 -(*1st stage: make empty slots assignable*)
1.220 -val assignable =
1.221 - map_args (fn Arg (s, Empty) => Arg (s, Assignable (ref NONE)) | arg => arg);
1.222 -
1.223 -(*2nd stage: assign values as side-effect of scanning*)
1.224 -fun assign v (arg as Arg (_, Assignable r)) = r := v
1.225 - | assign _ _ = ();
1.226 -
1.227 -val ahead = Scan.ahead (Scan.one not_eof);
1.228 -fun touch scan = ahead -- scan >> (fn (arg, y) => (assign NONE arg; y));
1.229 -
1.230 -(*3rd stage: static closure of final values*)
1.231 -val closure =
1.232 - map_args (fn Arg (s, Assignable (ref v)) => Arg (s, Value v) | arg => arg);
1.233 -
1.234 -
1.235 -
1.236 -(** scanners **)
1.237 +(** argument scanners **)
1.238
1.239 (* context *)
1.240
1.241 @@ -235,44 +133,23 @@
1.242 fun theory x = (Scan.state >> Context.theory_of) x;
1.243
1.244
1.245 -(* position *)
1.246 -
1.247 -fun position scan =
1.248 - (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap;
1.249 -
1.250 -
1.251 -(* cut *)
1.252 -
1.253 -fun !!! scan =
1.254 - let
1.255 - fun get_pos [] = " (past end-of-text!)"
1.256 - | get_pos (arg :: _) = Position.str_of (pos_of arg);
1.257 -
1.258 - fun err (args, NONE) = "Argument syntax error" ^ get_pos args
1.259 - | err (args, SOME msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg;
1.260 - in Scan.!! err scan end;
1.261 -
1.262 -
1.263 (* basic *)
1.264
1.265 -fun some_ident f =
1.266 - touch (Scan.some (fn Arg ((Ident, x, _), _) => f x | _ => NONE));
1.267 +fun token atom = Scan.ahead P.not_eof --| atom;
1.268
1.269 -val named =
1.270 - touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String));
1.271 +val ident = token
1.272 + (P.short_ident || P.long_ident || P.sym_ident || P.term_var ||
1.273 + P.type_ident || P.type_var || P.number);
1.274
1.275 -val alt_string =
1.276 - touch (Scan.one (fn Arg ((k, _, _), _) => k = AltString));
1.277 +val string = token (P.string || P.verbatim);
1.278 +val alt_string = token P.alt_string;
1.279 +val symbolic = token P.keyword_ident_or_symbolic;
1.280
1.281 -val symbolic =
1.282 - touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x));
1.283 +fun $$$ x = (ident >> T.content_of || P.keyword)
1.284 + :|-- (fn y => if x = y then Scan.succeed x else Scan.fail);
1.285
1.286 -fun &&& x =
1.287 - touch (Scan.one (fn Arg ((k, y, _), _) => k = Keyword andalso x = y));
1.288
1.289 -fun $$$ x =
1.290 - touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y))
1.291 - >> sym_of;
1.292 +val named = ident || string;
1.293
1.294 val add = $$$ "add";
1.295 val del = $$$ "del";
1.296 @@ -286,50 +163,35 @@
1.297 fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
1.298 fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
1.299 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
1.300 -val terminator = Scan.ahead (Scan.one is_eof);
1.301
1.302 -val name = named >> sym_of;
1.303 -val alt_name = alt_string >> sym_of;
1.304 -val symbol = symbolic >> sym_of;
1.305 +val name = named >> T.content_of;
1.306 +val alt_name = alt_string >> T.content_of;
1.307 +val symbol = symbolic >> T.content_of;
1.308 val liberal_name = symbol || name;
1.309
1.310 -val nat = some_ident Lexicon.read_nat;
1.311 -val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
1.312 -val var = some_ident Lexicon.read_variable;
1.313 -
1.314 -
1.315 -(* enumerations *)
1.316 -
1.317 -fun list1 scan = scan ::: Scan.repeat ($$$ "," |-- scan);
1.318 -fun list scan = list1 scan || Scan.succeed [];
1.319 -
1.320 -fun enum1 sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan);
1.321 -fun enum sep scan = enum1 sep scan || Scan.succeed [];
1.322 -
1.323 -fun and_list1 scan = enum1 "and" scan;
1.324 -fun and_list scan = enum "and" scan;
1.325 +val var = (ident >> T.content_of) :|-- (fn x =>
1.326 + (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail));
1.327
1.328
1.329 (* values *)
1.330
1.331 -fun value dest = Scan.some (*no touch here*)
1.332 - (fn Arg (_, Value (SOME v)) => (SOME (dest v) handle Match => NONE)
1.333 - | Arg _ => NONE);
1.334 +fun value dest = Scan.some (fn arg =>
1.335 + (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE));
1.336
1.337 fun evaluate mk eval arg =
1.338 - let val x = eval (sym_of arg) in (assign (SOME (mk x)) arg; x) end;
1.339 + let val x = eval (T.content_of arg) in (T.assign (SOME (mk x)) arg; x) end;
1.340
1.341 -val internal_text = value (fn Text s => s);
1.342 -val internal_typ = value (fn Typ T => T);
1.343 -val internal_term = value (fn Term t => t);
1.344 -val internal_fact = value (fn Fact ths => ths);
1.345 -val internal_attribute = value (fn Attribute att => att);
1.346 +val internal_text = value (fn T.Text s => s);
1.347 +val internal_typ = value (fn T.Typ T => T);
1.348 +val internal_term = value (fn T.Term t => t);
1.349 +val internal_fact = value (fn T.Fact ths => ths);
1.350 +val internal_attribute = value (fn T.Attribute att => att);
1.351
1.352 -fun named_text intern = internal_text || named >> evaluate Text intern;
1.353 -fun named_typ readT = internal_typ || named >> evaluate Typ readT;
1.354 -fun named_term read = internal_term || named >> evaluate Term read;
1.355 -fun named_fact get = internal_fact || (alt_string || named) >> evaluate Fact get;
1.356 -fun named_attribute att = internal_attribute || named >> evaluate Attribute att;
1.357 +fun named_text intern = internal_text || named >> evaluate T.Text intern;
1.358 +fun named_typ readT = internal_typ || named >> evaluate T.Typ readT;
1.359 +fun named_term read = internal_term || named >> evaluate T.Term read;
1.360 +fun named_fact get = internal_fact || (alt_string || named) >> evaluate T.Fact get;
1.361 +fun named_attribute att = internal_attribute || named >> evaluate T.Attribute att;
1.362
1.363
1.364 (* terms and types *)
1.365 @@ -353,38 +215,31 @@
1.366 >> (fn Const (c, _) => c | _ => "");
1.367
1.368
1.369 -(* misc *)
1.370 -
1.371 -val thm_sel = parens (list1
1.372 - (nat --| $$$ "-" -- nat >> Facts.FromTo ||
1.373 - nat --| $$$ "-" >> Facts.From ||
1.374 - nat >> Facts.Single));
1.375 +(* improper method arguments *)
1.376
1.377 val bang_facts = Scan.peek (fn context =>
1.378 - $$$ "!" >> (fn _ => (warning "use of prems in proof method";
1.379 - Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
1.380 -
1.381 -
1.382 -(* goal specification *)
1.383 + P.position ($$$ "!") >> (fn (_, pos) =>
1.384 + (warning ("use of prems in proof method" ^ Position.str_of pos);
1.385 + Assumption.prems_of (Context.proof_of context))) || Scan.succeed []);
1.386
1.387 val from_to =
1.388 - nat -- ($$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
1.389 - nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
1.390 - nat >> (fn i => fn tac => tac i) ||
1.391 + P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
1.392 + P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
1.393 + P.nat >> (fn i => fn tac => tac i) ||
1.394 $$$ "!" >> K ALLGOALS;
1.395
1.396 -val goal = $$$ "[" |-- !!! (from_to --| $$$ "]");
1.397 +val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
1.398 fun goal_spec def = Scan.lift (Scan.optional goal def);
1.399
1.400
1.401 -(* nested args and attribs *)
1.402 -
1.403 -local
1.404 +(* arguments within outer syntax *)
1.405
1.406 fun parse_args is_symid =
1.407 let
1.408 - fun atom blk = touch (Scan.one (fn Arg ((k, x, _), _) =>
1.409 - k <> Keyword orelse is_symid x orelse blk andalso x = ","));
1.410 + val keyword_symid = token (P.keyword_with is_symid);
1.411 + fun atom blk = P.group "argument"
1.412 + (ident || keyword_symid || string || alt_string ||
1.413 + (if blk then token (P.$$$ ",") else Scan.fail));
1.414
1.415 fun args blk x = Scan.optional (args1 blk) [] x
1.416 and args1 blk x =
1.417 @@ -392,43 +247,41 @@
1.418 (Scan.repeat1 (atom blk) ||
1.419 argsp "(" ")" ||
1.420 argsp "[" "]")) >> flat) x
1.421 - and argsp l r x =
1.422 - (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x;
1.423 + and argsp l r x = (token (P.$$$ l) ::: P.!!! (args true @@@ (token (P.$$$ r) >> single))) x;
1.424 in (args, args1) end;
1.425
1.426 -in
1.427 +val parse = #1 (parse_args T.ident_or_symbolic) false;
1.428 +fun parse1 is_symid = #2 (parse_args is_symid) false;
1.429
1.430 -fun generic_args1 is_symid = #2 (parse_args is_symid) false;
1.431 -val arguments = #1 (parse_args OuterLex.is_sid) false;
1.432 +
1.433 +(* attributes *)
1.434
1.435 fun attribs intern =
1.436 let
1.437 - val attrib_name = internal_text || (symbolic || named) >> evaluate Text intern;
1.438 - val attrib = position (attrib_name -- !!! arguments) >> src;
1.439 - in $$$ "[" |-- !!! (list attrib --| $$$ "]") end;
1.440 + val attrib_name = internal_text || (symbolic || named) >> evaluate T.Text intern;
1.441 + val attrib = P.position (attrib_name -- P.!!! parse) >> src;
1.442 + in $$$ "[" |-- P.!!! (P.list attrib --| $$$ "]") end;
1.443
1.444 fun opt_attribs intern = Scan.optional (attribs intern) [];
1.445
1.446 -end;
1.447 -
1.448
1.449 (* theorem specifications *)
1.450
1.451 fun thm_name intern s = name -- opt_attribs intern --| $$$ s;
1.452 +
1.453 fun opt_thm_name intern s =
1.454 Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []);
1.455
1.456
1.457
1.458 -
1.459 (** syntax wrapper **)
1.460
1.461 fun syntax kind scan (src as Src ((s, args), pos)) st =
1.462 - (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of
1.463 + (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of
1.464 (SOME x, (st', [])) => (x, st')
1.465 | (_, (_, args')) =>
1.466 error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^
1.467 - space_implode " " (map string_of args')));
1.468 + space_implode " " (map T.unparse args')));
1.469
1.470 fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;
1.471