# HG changeset patch # User wenzelm # Date 1394104219 -3600 # Node ID c07d184aebe9cce602bbff9bcde48de0ec0fbad8 # Parent 3bb5c717923492f8ffab97048930065d8f3bbf36 tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c); diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 06 12:10:19 2014 +0100 @@ -185,7 +185,7 @@ (Scan.succeed false); fun setup_generate_fresh x = - (Args.goal_spec -- Args.type_name true >> + (Args.goal_spec -- Args.type_name {proper = false, strict = true} >> (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x; fun setup_fresh_fun_simp x = diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Mar 06 12:10:19 2014 +0100 @@ -33,7 +33,8 @@ error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes"); val fpT_names = - map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names; + map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false}) + raw_fpT_names; fun lfp_sugar_of s = (case fp_sugar_of lthy s of diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Mar 06 12:10:19 2014 +0100 @@ -234,7 +234,7 @@ (** document antiquotation **) val antiq_setup = - Thy_Output.antiquotation @{binding datatype} (Args.type_name true) + Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, strict = true}) (fn {source = src, context = ctxt, ...} => fn dtco => let val thy = Proof_Context.theory_of ctxt; diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/Quickcheck/abstract_generators.ML --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Thu Mar 06 12:10:19 2014 +0100 @@ -61,8 +61,10 @@ val quickcheck_generator = gen_quickcheck_generator (K I) (K I) -val quickcheck_generator_cmd = gen_quickcheck_generator - (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term +val quickcheck_generator_cmd = + gen_quickcheck_generator + (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false}) + Syntax.read_term val _ = Outer_Syntax.command @{command_spec "quickcheck_generator"} diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/Quotient/quotient_info.ML --- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Mar 06 12:10:19 2014 +0100 @@ -71,7 +71,7 @@ val quotmaps_attribute_setup = Attrib.setup @{binding mapQ3} - ((Args.type_name true --| Scan.lift @{keyword "="}) -- + ((Args.type_name {proper = false, strict = true} --| Scan.lift @{keyword "="}) -- (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} -- Attrib.thm --| Scan.lift @{keyword ")"}) >> (fn (tyname, (relname, qthm)) => diff -r 3bb5c7179234 -r c07d184aebe9 src/HOL/Tools/coinduction.ML --- a/src/HOL/Tools/coinduction.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/HOL/Tools/coinduction.ML Thu Mar 06 12:10:19 2014 +0100 @@ -129,7 +129,7 @@ | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); fun rule get_type get_pred = - named_rule Induct.typeN (Args.type_name false) get_type || + named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type || named_rule Induct.predN (Args.const false) get_pred || named_rule Induct.setN (Args.const false) get_pred || Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms; diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/Isar/args.ML Thu Mar 06 12:10:19 2014 +0100 @@ -56,7 +56,7 @@ val term_pattern: term context_parser val term_abbrev: term context_parser val prop: term context_parser - val type_name: bool -> string context_parser + val type_name: {proper: bool, strict: bool} -> string context_parser val const: bool -> string context_parser val const_proper: bool -> string context_parser val goal_spec: ((int -> tactic) -> tactic) context_parser @@ -208,8 +208,8 @@ (* type and constant names *) -fun type_name strict = - Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict)) +fun type_name flags = + Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags)) >> (fn Type (c, _) => c | TFree (a, _) => a | _ => ""); fun const strict = diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 06 12:10:19 2014 +0100 @@ -68,12 +68,9 @@ val infer_type: Proof.context -> string * typ -> typ val inferred_param: string -> Proof.context -> typ * Proof.context val inferred_fixes: Proof.context -> (string * typ) list * Proof.context - val check_type_name: Proof.context -> bool -> + val check_type_name: Proof.context -> {proper: bool, strict: bool} -> xstring * Position.T -> typ * Position.report list - val check_type_name_proper: Proof.context -> bool -> - xstring * Position.T -> typ * Position.report list - val read_type_name: Proof.context -> bool -> string -> typ - val read_type_name_proper: Proof.context -> bool -> string -> typ + val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ val check_const_proper: Proof.context -> bool -> xstring * Position.T -> term * Position.report list val read_const_proper: Proof.context -> bool -> string -> term @@ -443,13 +440,15 @@ (* type names *) -fun check_type_name ctxt strict (c, pos) = +fun check_type_name ctxt {proper, strict} (c, pos) = if Lexicon.is_tid c then - let - val reports = - if Context_Position.is_reported ctxt pos - then [(pos, Markup.tfree)] else []; - in (TFree (c, default_sort ctxt (c, ~1)), reports) end + if proper then error ("Not a type constructor: " ^ c ^ Position.here pos) + else + let + val reports = + if Context_Position.is_reported ctxt pos + then [(pos, Markup.tfree)] else []; + in (TFree (c, default_sort ctxt (c, ~1)), reports) end else let val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos); @@ -461,16 +460,12 @@ | Type.Nonterminal => if strict then err () else 0); in (Type (d, replicate args dummyT), reports) end; -fun check_type_name_proper ctxt strict arg = - (case check_type_name ctxt strict arg of - res as (Type _, _) => res - | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T)); - -fun read_type_name ctxt strict = - Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1; - -fun read_type_name_proper ctxt strict = - Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1; +fun read_type_name ctxt flags text = + let + val (T, reports) = + check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text)); + val _ = Position.reports reports; + in T end; (* constant names *) @@ -531,7 +526,8 @@ in val read_arity = - prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort; + prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true}) + Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/Isar/specification.ML Thu Mar 06 12:10:19 2014 +0100 @@ -276,7 +276,8 @@ in val type_notation = gen_type_notation (K I); -val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false); +val type_notation_cmd = + gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = false, strict = false}); val notation = gen_notation (K I); val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT); diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Thu Mar 06 12:10:19 2014 +0100 @@ -127,7 +127,7 @@ fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) >> (fn (ctxt, (s, pos)) => let - val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s; + val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s; val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); val res = (case try check (c, decl) of diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 06 12:10:19 2014 +0100 @@ -170,7 +170,8 @@ let val pos = Lexicon.pos_of_token tok; val (Type (c, _), rs) = - Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos); + Proof_Context.check_type_name ctxt {proper = true, strict = false} + (Lexicon.str_of_token tok, pos); val _ = Unsynchronized.change reports (append (map (rpair "") rs)); in [Ast.Constant (Lexicon.mark_type c)] end | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok diff -r 3bb5c7179234 -r c07d184aebe9 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Mar 06 12:10:19 2014 +0100 @@ -515,7 +515,7 @@ Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt; fun pretty_type ctxt s = - let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s + let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s in Pretty.str (Proof_Context.extern_type ctxt name) end; fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; diff -r 3bb5c7179234 -r c07d184aebe9 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Tools/Code/code_target.ML Thu Mar 06 12:10:19 2014 +0100 @@ -97,8 +97,8 @@ else error ("No such type constructor: " ^ quote tyco); in tyco end; -fun read_tyco ctxt = #1 o dest_Type - o Proof_Context.read_type_name_proper ctxt true; +fun read_tyco ctxt = + #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true}; fun cert_class ctxt class = let diff -r 3bb5c7179234 -r c07d184aebe9 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Mar 06 11:32:16 2014 +0100 +++ b/src/Tools/induct.ML Thu Mar 06 12:10:19 2014 +0100 @@ -361,7 +361,7 @@ Scan.lift (Args.$$$ k) >> K ""; fun attrib add_type add_pred del = - spec typeN (Args.type_name false) >> add_type || + spec typeN (Args.type_name {proper = false, strict = false}) >> add_type || spec predN (Args.const false) >> add_pred || spec setN (Args.const false) >> add_pred || Scan.lift Args.del >> K del; @@ -883,7 +883,7 @@ | NONE => error ("No rule for " ^ k ^ " " ^ quote name)))))); fun rule get_type get_pred = - named_rule typeN (Args.type_name false) get_type || + named_rule typeN (Args.type_name {proper = false, strict = false}) get_type || named_rule predN (Args.const false) get_pred || named_rule setN (Args.const false) get_pred || Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;