1(* Title: Pure/Isar/args.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Quasi-inner syntax based on outer tokens: concrete argument syntax of 5attributes, methods etc. 6*) 7 8signature ARGS = 9sig 10 val context: Proof.context context_parser 11 val theory: theory context_parser 12 val symbolic: Token.T parser 13 val $$$ : string -> string parser 14 val add: string parser 15 val del: string parser 16 val colon: string parser 17 val query: string parser 18 val bang: string parser 19 val query_colon: string parser 20 val bang_colon: string parser 21 val parens: 'a parser -> 'a parser 22 val bracks: 'a parser -> 'a parser 23 val mode: string -> bool parser 24 val maybe: 'a parser -> 'a option parser 25 val name_token: Token.T parser 26 val name: string parser 27 val name_position: (string * Position.T) parser 28 val cartouche_inner_syntax: string parser 29 val cartouche_input: Input.source parser 30 val text_token: Token.T parser 31 val embedded_token: Token.T parser 32 val embedded_inner_syntax: string parser 33 val embedded_input: Input.source parser 34 val embedded: string parser 35 val embedded_position: (string * Position.T) parser 36 val text_input: Input.source parser 37 val text: string parser 38 val binding: binding parser 39 val alt_name: string parser 40 val liberal_name: string parser 41 val var: indexname parser 42 val internal_source: Token.src parser 43 val internal_name: Token.name_value parser 44 val internal_typ: typ parser 45 val internal_term: term parser 46 val internal_fact: thm list parser 47 val internal_attribute: (morphism -> attribute) parser 48 val internal_declaration: declaration parser 49 val named_source: (Token.T -> Token.src) -> Token.src parser 50 val named_typ: (string -> typ) -> typ parser 51 val named_term: (string -> term) -> term parser 52 val named_fact: (string -> string option * thm list) -> thm list parser 53 val named_attribute: (string * Position.T -> morphism -> attribute) -> 54 (morphism -> attribute) parser 55 val text_declaration: (Input.source -> declaration) -> declaration parser 56 val cartouche_declaration: (Input.source -> declaration) -> declaration parser 57 val typ_abbrev: typ context_parser 58 val typ: typ context_parser 59 val term: term context_parser 60 val term_pattern: term context_parser 61 val term_abbrev: term context_parser 62 val prop: term context_parser 63 val type_name: {proper: bool, strict: bool} -> string context_parser 64 val const: {proper: bool, strict: bool} -> string context_parser 65 val goal_spec: ((int -> tactic) -> tactic) context_parser 66end; 67 68structure Args: ARGS = 69struct 70 71(** argument scanners **) 72 73(* context *) 74 75fun context x = (Scan.state >> Context.proof_of) x; 76fun theory x = (Scan.state >> Context.theory_of) x; 77 78 79(* basic *) 80 81val ident = Parse.token 82 (Parse.short_ident || Parse.long_ident || Parse.sym_ident || Parse.term_var || 83 Parse.type_ident || Parse.type_var || Parse.number); 84 85val string = Parse.token Parse.string; 86val alt_string = Parse.token (Parse.alt_string || Parse.cartouche); 87val symbolic = Parse.token (Parse.keyword_with Token.ident_or_symbolic); 88 89fun $$$ x = 90 (ident || Parse.token Parse.keyword) :|-- (fn tok => 91 let val y = Token.content_of tok in 92 if x = y 93 then (Token.assign (SOME (Token.Literal (false, Markup.quasi_keyword))) tok; Scan.succeed x) 94 else Scan.fail 95 end); 96 97val add = $$$ "add"; 98val del = $$$ "del"; 99val colon = $$$ ":"; 100val query = $$$ "?"; 101val bang = $$$ "!"; 102val query_colon = $$$ "?" ^^ $$$ ":"; 103val bang_colon = $$$ "!" ^^ $$$ ":"; 104 105fun parens scan = $$$ "(" |-- scan --| $$$ ")"; 106fun bracks scan = $$$ "[" |-- scan --| $$$ "]"; 107fun mode s = Scan.optional (parens ($$$ s) >> K true) false; 108fun maybe scan = $$$ "_" >> K NONE || scan >> SOME; 109 110val name_token = ident || string; 111val name = name_token >> Token.content_of; 112val name_position = name_token >> (Input.source_content o Token.input_of); 113 114val cartouche = Parse.token Parse.cartouche; 115val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of; 116val cartouche_input = cartouche >> Token.input_of; 117 118val embedded_token = ident || string || cartouche; 119val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of; 120val embedded_input = embedded_token >> Token.input_of; 121val embedded = embedded_token >> Token.content_of; 122val embedded_position = embedded_input >> Input.source_content; 123 124val text_token = embedded_token || Parse.token Parse.verbatim; 125val text_input = text_token >> Token.input_of; 126val text = text_token >> Token.content_of; 127 128val binding = Parse.input name >> (Binding.make o Input.source_content); 129val alt_name = alt_string >> Token.content_of; 130val liberal_name = (symbolic >> Token.content_of) || name; 131 132val var = 133 (ident >> Token.content_of) :|-- (fn x => 134 (case Lexicon.read_variable x of SOME v => Scan.succeed v | NONE => Scan.fail)); 135 136 137(* values *) 138 139fun value dest = Scan.some (fn arg => 140 (case Token.get_value arg of SOME v => (SOME (dest v) handle Match => NONE) | NONE => NONE)); 141 142val internal_source = value (fn Token.Source src => src); 143val internal_name = value (fn Token.Name (a, _) => a); 144val internal_typ = value (fn Token.Typ T => T); 145val internal_term = value (fn Token.Term t => t); 146val internal_fact = value (fn Token.Fact (_, ths) => ths); 147val internal_attribute = value (fn Token.Attribute att => att); 148val internal_declaration = value (fn Token.Declaration decl => decl); 149 150fun named_source read = 151 internal_source || name_token >> Token.evaluate Token.Source read; 152 153fun named_typ read = 154 internal_typ || embedded_token >> Token.evaluate Token.Typ (read o Token.inner_syntax_of); 155 156fun named_term read = 157 internal_term || embedded_token >> Token.evaluate Token.Term (read o Token.inner_syntax_of); 158 159fun named_fact get = 160 internal_fact || 161 name_token >> Token.evaluate Token.Fact (get o Token.content_of) >> #2 || 162 alt_string >> Token.evaluate Token.Fact (get o Token.inner_syntax_of) >> #2; 163 164fun named_attribute att = 165 internal_attribute || 166 name_token >> 167 Token.evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok)); 168 169fun text_declaration read = 170 internal_declaration || text_token >> Token.evaluate Token.Declaration (read o Token.input_of); 171 172fun cartouche_declaration read = 173 internal_declaration || cartouche >> Token.evaluate Token.Declaration (read o Token.input_of); 174 175 176(* terms and types *) 177 178val typ_abbrev = Scan.peek (named_typ o Proof_Context.read_typ_abbrev o Context.proof_of); 179val typ = Scan.peek (named_typ o Syntax.read_typ o Context.proof_of); 180val term = Scan.peek (named_term o Syntax.read_term o Context.proof_of); 181val term_pattern = Scan.peek (named_term o Proof_Context.read_term_pattern o Context.proof_of); 182val term_abbrev = Scan.peek (named_term o Proof_Context.read_term_abbrev o Context.proof_of); 183val prop = Scan.peek (named_term o Syntax.read_prop o Context.proof_of); 184 185 186(* type and constant names *) 187 188fun type_name flags = 189 Scan.peek (named_typ o Proof_Context.read_type_name flags o Context.proof_of) 190 >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); 191 192fun const flags = 193 Scan.peek (named_term o Proof_Context.read_const flags o Context.proof_of) 194 >> (fn Const (c, _) => c | Free (x, _) => x | _ => ""); 195 196 197(* improper method arguments *) 198 199val from_to = 200 Parse.nat -- ($$$ "-" |-- Parse.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) || 201 Parse.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) || 202 Parse.nat >> (fn i => fn tac => tac i) || 203 $$$ "!" >> K ALLGOALS; 204 205val goal = Parse.keyword_improper "[" |-- Parse.!!! (from_to --| Parse.keyword_improper "]"); 206fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x; 207 208end; 209