# HG changeset patch # User wenzelm # Date 1218314633 -7200 # Node ID 44bc67675210a0e93b0db1257bffbdcb20a236d3 # Parent b09f6fcc1f3df65d380d06ed6a6964273ed161e0 unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML); diff -r b09f6fcc1f3d -r 44bc67675210 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Sat Aug 09 22:43:52 2008 +0200 +++ b/src/Pure/Isar/args.ML Sat Aug 09 22:43:53 2008 +0200 @@ -2,29 +2,13 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Concrete argument syntax of attributes, methods etc. -- with special -support for embedded values and static binding. +Parsing with implicit value assigment. Concrete argument syntax of +attributes, methods etc. *) signature ARGS = sig - datatype value = - Text of string | Typ of typ | Term of term | Fact of thm list | - Attribute of morphism -> attribute - type T - val string_of: T -> string - val mk_ident: string * Position.T -> T - val mk_string: string * Position.T -> T - val mk_alt_string: string * Position.T -> T - val mk_keyword: string * Position.T -> T - val mk_text: string -> T - val mk_typ: typ -> T - val mk_term: term -> T - val mk_fact: thm list -> T - val mk_attribute: (morphism -> attribute) -> T - val eof: T - val stopper: T Scan.stopper - val not_eof: T -> bool + type T = OuterLex.token type src val src: (string * T list) * Position.T -> src val dest_src: src -> (string * T list) * Position.T @@ -33,12 +17,9 @@ val morph_values: morphism -> src -> src val maxidx_values: src -> int -> int val assignable: src -> src - val assign: value option -> T -> unit val closure: src -> src val context: Context.generic * T list -> Context.proof * (Context.generic * T list) val theory: Context.generic * T list -> Context.theory * (Context.generic * T list) - val position: (T list -> 'a * 'b) -> T list -> ('a * Position.T) * 'b - val !!! : (T list -> 'a) -> T list -> 'a val $$$ : string -> T list -> string * T list val add: T list -> string * T list val del: T list -> string * T list @@ -51,21 +32,11 @@ val bracks: (T list -> 'a * T list) -> T list -> 'a * T list val mode: string -> 'a * T list -> bool * ('a * T list) val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list - val terminator: T list -> T * T list val name: T list -> string * T list val alt_name: T list -> string * T list val symbol: T list -> string * T list val liberal_name: T list -> string * T list - val nat: T list -> int * T list - val int: T list -> int * T list val var: T list -> indexname * T list - val list: (T list -> 'a * T list) -> T list -> 'a list * T list - val list1: (T list -> 'a * T list) -> T list -> 'a list * T list - val enum: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) - val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) - val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) - val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list) - val ahead: T list -> T * T list val internal_text: T list -> string * T list val internal_typ: T list -> typ * T list val internal_term: T list -> term * T list @@ -85,11 +56,11 @@ val tyname: Context.generic * T list -> string * (Context.generic * T list) val const: Context.generic * T list -> string * (Context.generic * T list) val const_proper: Context.generic * T list -> string * (Context.generic * T list) - val thm_sel: T list -> Facts.interval list * T list val bang_facts: Context.generic * T list -> thm list * (Context.generic * T list) val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list) -> ((int -> tactic) -> tactic) * ('a * T list) - val generic_args1: (string -> bool) -> T list -> T list * T list + val parse: OuterLex.token list -> T list * OuterLex.token list + val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list val attribs: (string -> string) -> T list -> src list * T list val opt_attribs: (string -> string) -> T list -> src list * T list val thm_name: (string -> string) -> string -> T list -> (string * src list) * T list @@ -102,72 +73,15 @@ structure Args: ARGS = struct - -(** datatype T **) - -(*An argument token is a symbol (with raw string value), together with - an optional assigned internal value. Note that an assignable ref - designates an intermediate state of internalization -- it is NOT - meant to persist.*) - -datatype kind = Ident | String | AltString | Keyword | EOF; - -type symbol = kind * string * Position.T; - -datatype value = - Text of string | - Typ of typ | - Term of term | - Fact of thm list | - Attribute of morphism -> attribute; - -datatype slot = - Empty | - Value of value option | - Assignable of value option ref; - -datatype T = Arg of symbol * slot; - -fun string_of (Arg ((Ident, x, _), _)) = x - | string_of (Arg ((String, x, _), _)) = quote x - | string_of (Arg ((AltString, x, _), _)) = enclose "`" "`" x - | string_of (Arg ((Keyword, x, _), _)) = x - | string_of (Arg ((EOF, _, _), _)) = ""; - -fun sym_of (Arg ((_, x, _), _)) = x; -fun pos_of (Arg ((_, _, pos), _)) = pos; - - -(* basic constructors *) - -fun mk_symbol k (x, p) = Arg ((k, x, p), Empty); -fun mk_value k v = Arg ((Keyword, k, Position.none), Value (SOME v)); - -val mk_ident = mk_symbol Ident; -val mk_string = mk_symbol String; -val mk_alt_string = mk_symbol AltString; -val mk_keyword = mk_symbol Keyword; -val mk_text = mk_value "" o Text; -val mk_typ = mk_value "" o Typ; -val mk_term = mk_value "" o Term; -val mk_fact = mk_value "" o Fact; -val mk_attribute = mk_value "" o Attribute; - - -(* eof *) - -val eof = mk_symbol EOF ("", Position.none); - -fun is_eof (Arg ((EOF, _, _), _)) = true - | is_eof _ = false; - -val stopper = Scan.stopper (K eof) is_eof; -val not_eof = not o is_eof; +structure T = OuterLex; +structure P = OuterParse; (** datatype src **) +type T = T.token; + datatype src = Src of (string * T list) * Position.T; val src = Src; @@ -176,12 +90,13 @@ fun pretty_src ctxt src = let val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; - fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s) - | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T - | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t - | prt (Arg (_, Value (SOME (Fact ths)))) = - Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) - | prt arg = Pretty.str (string_of arg); + fun prt arg = + (case T.get_value arg of + SOME (T.Text s) => Pretty.str (quote s) + | SOME (T.Typ T) => Syntax.pretty_typ ctxt T + | SOME (T.Term t) => Syntax.pretty_term ctxt t + | SOME (T.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths)) + | _ => Pretty.str (T.unparse arg)); val (s, args) = #1 (dest_src src); in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end; @@ -191,43 +106,26 @@ (* values *) -fun map_value f (Arg (s, Value (SOME v))) = Arg (s, Value (SOME (f v))) - | map_value _ arg = arg; - -fun morph_values phi = map_args (map_value - (fn Text s => Text s - | Typ T => Typ (Morphism.typ phi T) - | Term t => Term (Morphism.term phi t) - | Fact ths => Fact (Morphism.fact phi ths) - | Attribute att => Attribute (Morphism.transform phi att))); - -fun maxidx_values (Src ((_, args), _)) = args |> fold - (fn (Arg (_, Value (SOME (Typ T)))) => Term.maxidx_typ T - | (Arg (_, Value (SOME (Term t)))) => Term.maxidx_term t - | (Arg (_, Value (SOME (Fact ths)))) => fold Thm.maxidx_thm ths - | _ => I); - +fun morph_values phi = map_args (T.map_value + (fn T.Text s => T.Text s + | T.Typ T => T.Typ (Morphism.typ phi T) + | T.Term t => T.Term (Morphism.term phi t) + | T.Fact ths => T.Fact (Morphism.fact phi ths) + | T.Attribute att => T.Attribute (Morphism.transform phi att))); -(* static binding *) - -(*1st stage: make empty slots assignable*) -val assignable = - map_args (fn Arg (s, Empty) => Arg (s, Assignable (ref NONE)) | arg => arg); +fun maxidx_values (Src ((_, args), _)) = args |> fold (fn arg => + (case T.get_value arg of + SOME (T.Typ T) => Term.maxidx_typ T + | SOME (T.Term t) => Term.maxidx_term t + | SOME (T.Fact ths) => fold Thm.maxidx_thm ths + | _ => I)); -(*2nd stage: assign values as side-effect of scanning*) -fun assign v (arg as Arg (_, Assignable r)) = r := v - | assign _ _ = (); - -val ahead = Scan.ahead (Scan.one not_eof); -fun touch scan = ahead -- scan >> (fn (arg, y) => (assign NONE arg; y)); - -(*3rd stage: static closure of final values*) -val closure = - map_args (fn Arg (s, Assignable (ref v)) => Arg (s, Value v) | arg => arg); +val assignable = map_args T.assignable; +val closure = map_args T.closure; -(** scanners **) +(** argument scanners **) (* context *) @@ -235,44 +133,23 @@ fun theory x = (Scan.state >> Context.theory_of) x; -(* position *) +(* basic *) -fun position scan = - (Scan.ahead (Scan.one not_eof) >> pos_of) -- scan >> Library.swap; - - -(* cut *) +fun token atom = Scan.ahead P.not_eof --| atom; -fun !!! scan = - let - fun get_pos [] = " (past end-of-text!)" - | get_pos (arg :: _) = Position.str_of (pos_of arg); +val ident = token + (P.short_ident || P.long_ident || P.sym_ident || P.term_var || + P.type_ident || P.type_var || P.number); - fun err (args, NONE) = "Argument syntax error" ^ get_pos args - | err (args, SOME msg) = "Argument syntax error" ^ get_pos args ^ ": " ^ msg; - in Scan.!! err scan end; +val string = token (P.string || P.verbatim); +val alt_string = token P.alt_string; +val symbolic = token P.keyword_ident_or_symbolic; + +fun $$$ x = (ident >> T.content_of || P.keyword) + :|-- (fn y => if x = y then Scan.succeed x else Scan.fail); -(* basic *) - -fun some_ident f = - touch (Scan.some (fn Arg ((Ident, x, _), _) => f x | _ => NONE)); - -val named = - touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String)); - -val alt_string = - touch (Scan.one (fn Arg ((k, _, _), _) => k = AltString)); - -val symbolic = - touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x)); - -fun &&& x = - touch (Scan.one (fn Arg ((k, y, _), _) => k = Keyword andalso x = y)); - -fun $$$ x = - touch (Scan.one (fn Arg ((k, y, _), _) => (k = Ident orelse k = Keyword) andalso x = y)) - >> sym_of; +val named = ident || string; val add = $$$ "add"; val del = $$$ "del"; @@ -286,50 +163,35 @@ fun bracks scan = $$$ "[" |-- scan --| $$$ "]"; fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false); fun maybe scan = $$$ "_" >> K NONE || scan >> SOME; -val terminator = Scan.ahead (Scan.one is_eof); -val name = named >> sym_of; -val alt_name = alt_string >> sym_of; -val symbol = symbolic >> sym_of; +val name = named >> T.content_of; +val alt_name = alt_string >> T.content_of; +val symbol = symbolic >> T.content_of; val liberal_name = symbol || name; -val nat = some_ident Lexicon.read_nat; -val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *; -val var = some_ident Lexicon.read_variable; - - -(* enumerations *) - -fun list1 scan = scan ::: Scan.repeat ($$$ "," |-- scan); -fun list scan = list1 scan || Scan.succeed []; - -fun enum1 sep scan = scan ::: Scan.repeat (Scan.lift ($$$ sep) |-- scan); -fun enum sep scan = enum1 sep scan || Scan.succeed []; - -fun and_list1 scan = enum1 "and" scan; -fun and_list scan = enum "and" scan; +val var = (ident >> T.content_of) :|-- (fn x => + (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail)); (* values *) -fun value dest = Scan.some (*no touch here*) - (fn Arg (_, Value (SOME v)) => (SOME (dest v) handle Match => NONE) - | Arg _ => NONE); +fun value dest = Scan.some (fn arg => + (case T.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE)); fun evaluate mk eval arg = - let val x = eval (sym_of arg) in (assign (SOME (mk x)) arg; x) end; + let val x = eval (T.content_of arg) in (T.assign (SOME (mk x)) arg; x) end; -val internal_text = value (fn Text s => s); -val internal_typ = value (fn Typ T => T); -val internal_term = value (fn Term t => t); -val internal_fact = value (fn Fact ths => ths); -val internal_attribute = value (fn Attribute att => att); +val internal_text = value (fn T.Text s => s); +val internal_typ = value (fn T.Typ T => T); +val internal_term = value (fn T.Term t => t); +val internal_fact = value (fn T.Fact ths => ths); +val internal_attribute = value (fn T.Attribute att => att); -fun named_text intern = internal_text || named >> evaluate Text intern; -fun named_typ readT = internal_typ || named >> evaluate Typ readT; -fun named_term read = internal_term || named >> evaluate Term read; -fun named_fact get = internal_fact || (alt_string || named) >> evaluate Fact get; -fun named_attribute att = internal_attribute || named >> evaluate Attribute att; +fun named_text intern = internal_text || named >> evaluate T.Text intern; +fun named_typ readT = internal_typ || named >> evaluate T.Typ readT; +fun named_term read = internal_term || named >> evaluate T.Term read; +fun named_fact get = internal_fact || (alt_string || named) >> evaluate T.Fact get; +fun named_attribute att = internal_attribute || named >> evaluate T.Attribute att; (* terms and types *) @@ -353,38 +215,31 @@ >> (fn Const (c, _) => c | _ => ""); -(* misc *) - -val thm_sel = parens (list1 - (nat --| $$$ "-" -- nat >> Facts.FromTo || - nat --| $$$ "-" >> Facts.From || - nat >> Facts.Single)); +(* improper method arguments *) val bang_facts = Scan.peek (fn context => - $$$ "!" >> (fn _ => (warning "use of prems in proof method"; - Assumption.prems_of (Context.proof_of context))) || Scan.succeed []); - - -(* goal specification *) + P.position ($$$ "!") >> (fn (_, pos) => + (warning ("use of prems in proof method" ^ Position.str_of pos); + Assumption.prems_of (Context.proof_of context))) || Scan.succeed []); val from_to = - nat -- ($$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) || - nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) || - nat >> (fn i => fn tac => tac i) || + P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) || + P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) || + P.nat >> (fn i => fn tac => tac i) || $$$ "!" >> K ALLGOALS; -val goal = $$$ "[" |-- !!! (from_to --| $$$ "]"); +val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]"); fun goal_spec def = Scan.lift (Scan.optional goal def); -(* nested args and attribs *) - -local +(* arguments within outer syntax *) fun parse_args is_symid = let - fun atom blk = touch (Scan.one (fn Arg ((k, x, _), _) => - k <> Keyword orelse is_symid x orelse blk andalso x = ",")); + val keyword_symid = token (P.keyword_with is_symid); + fun atom blk = P.group "argument" + (ident || keyword_symid || string || alt_string || + (if blk then token (P.$$$ ",") else Scan.fail)); fun args blk x = Scan.optional (args1 blk) [] x and args1 blk x = @@ -392,43 +247,41 @@ (Scan.repeat1 (atom blk) || argsp "(" ")" || argsp "[" "]")) >> flat) x - and argsp l r x = - (Scan.trace (&&& l -- !!! (args true -- &&& r)) >> #2) x; + and argsp l r x = (token (P.$$$ l) ::: P.!!! (args true @@@ (token (P.$$$ r) >> single))) x; in (args, args1) end; -in +val parse = #1 (parse_args T.ident_or_symbolic) false; +fun parse1 is_symid = #2 (parse_args is_symid) false; -fun generic_args1 is_symid = #2 (parse_args is_symid) false; -val arguments = #1 (parse_args OuterLex.is_sid) false; + +(* attributes *) fun attribs intern = let - val attrib_name = internal_text || (symbolic || named) >> evaluate Text intern; - val attrib = position (attrib_name -- !!! arguments) >> src; - in $$$ "[" |-- !!! (list attrib --| $$$ "]") end; + val attrib_name = internal_text || (symbolic || named) >> evaluate T.Text intern; + val attrib = P.position (attrib_name -- P.!!! parse) >> src; + in $$$ "[" |-- P.!!! (P.list attrib --| $$$ "]") end; fun opt_attribs intern = Scan.optional (attribs intern) []; -end; - (* theorem specifications *) fun thm_name intern s = name -- opt_attribs intern --| $$$ s; + fun opt_thm_name intern s = Scan.optional ((name -- opt_attribs intern || attribs intern >> pair "") --| $$$ s) ("", []); - (** syntax wrapper **) fun syntax kind scan (src as Src ((s, args), pos)) st = - (case Scan.error (Scan.finite' stopper (Scan.option scan)) (st, args) of + (case Scan.error (Scan.finite' T.stopper (Scan.option scan)) (st, args) of (SOME x, (st', [])) => (x, st') | (_, (_, args')) => error (kind ^ " " ^ quote s ^ Position.str_of pos ^ ": bad arguments\n " ^ - space_implode " " (map string_of args'))); + space_implode " " (map T.unparse args'))); fun context_syntax kind scan src = apsnd Context.the_proof o syntax kind scan src o Context.Proof;