tuned signature -- more uniform check_type_name/read_type_name;
authorwenzelm
Thu Mar 06 12:10:19 2014 +0100 (2014-03-06)
changeset 55951c07d184aebe9
parent 55950 3bb5c7179234
child 55952 2f85cc6c27d4
tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Quickcheck/abstract_generators.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/coinduction.ML
src/Pure/Isar/args.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Tools/Code/code_target.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 11:32:16 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:10:19 2014 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  fun setup_generate_fresh x =
     1.7 -  (Args.goal_spec -- Args.type_name true >>
     1.8 +  (Args.goal_spec -- Args.type_name {proper = false, strict = true} >>
     1.9      (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
    1.10  
    1.11  fun setup_fresh_fun_simp x =
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 11:32:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Mar 06 12:10:19 2014 +0100
     2.3 @@ -33,7 +33,8 @@
     2.4        error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
     2.5  
     2.6      val fpT_names =
     2.7 -      map (fst o dest_Type o Proof_Context.read_type_name_proper lthy false) raw_fpT_names;
     2.8 +      map (fst o dest_Type o Proof_Context.read_type_name lthy {proper = true, strict = false})
     2.9 +        raw_fpT_names;
    2.10  
    2.11      fun lfp_sugar_of s =
    2.12        (case fp_sugar_of lthy s of
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 11:32:16 2014 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Mar 06 12:10:19 2014 +0100
     3.3 @@ -234,7 +234,7 @@
     3.4  (** document antiquotation **)
     3.5  
     3.6  val antiq_setup =
     3.7 -  Thy_Output.antiquotation @{binding datatype} (Args.type_name true)
     3.8 +  Thy_Output.antiquotation @{binding datatype} (Args.type_name {proper = false, strict = true})
     3.9      (fn {source = src, context = ctxt, ...} => fn dtco =>
    3.10        let
    3.11          val thy = Proof_Context.theory_of ctxt;
     4.1 --- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 11:32:16 2014 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Thu Mar 06 12:10:19 2014 +0100
     4.3 @@ -61,8 +61,10 @@
     4.4  
     4.5  val quickcheck_generator = gen_quickcheck_generator (K I) (K I)
     4.6    
     4.7 -val quickcheck_generator_cmd = gen_quickcheck_generator
     4.8 -  (fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
     4.9 +val quickcheck_generator_cmd =
    4.10 +  gen_quickcheck_generator
    4.11 +    (fn ctxt => fst o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = false})
    4.12 +    Syntax.read_term
    4.13    
    4.14  val _ =
    4.15    Outer_Syntax.command @{command_spec "quickcheck_generator"}
     5.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 11:32:16 2014 +0100
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Thu Mar 06 12:10:19 2014 +0100
     5.3 @@ -71,7 +71,7 @@
     5.4  
     5.5  val quotmaps_attribute_setup =
     5.6    Attrib.setup @{binding mapQ3}
     5.7 -    ((Args.type_name true --| Scan.lift @{keyword "="}) --
     5.8 +    ((Args.type_name {proper = false, strict = true} --| Scan.lift @{keyword "="}) --
     5.9        (Scan.lift @{keyword "("} |-- Args.const_proper true --| Scan.lift @{keyword ","} --
    5.10          Attrib.thm --| Scan.lift @{keyword ")"}) >>
    5.11        (fn (tyname, (relname, qthm)) =>
     6.1 --- a/src/HOL/Tools/coinduction.ML	Thu Mar 06 11:32:16 2014 +0100
     6.2 +++ b/src/HOL/Tools/coinduction.ML	Thu Mar 06 12:10:19 2014 +0100
     6.3 @@ -129,7 +129,7 @@
     6.4        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
     6.5  
     6.6  fun rule get_type get_pred =
     6.7 -  named_rule Induct.typeN (Args.type_name false) get_type ||
     6.8 +  named_rule Induct.typeN (Args.type_name {proper = false, strict = false}) get_type ||
     6.9    named_rule Induct.predN (Args.const false) get_pred ||
    6.10    named_rule Induct.setN (Args.const false) get_pred ||
    6.11    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;
     7.1 --- a/src/Pure/Isar/args.ML	Thu Mar 06 11:32:16 2014 +0100
     7.2 +++ b/src/Pure/Isar/args.ML	Thu Mar 06 12:10:19 2014 +0100
     7.3 @@ -56,7 +56,7 @@
     7.4    val term_pattern: term context_parser
     7.5    val term_abbrev: term context_parser
     7.6    val prop: term context_parser
     7.7 -  val type_name: bool -> string context_parser
     7.8 +  val type_name: {proper: bool, strict: bool} -> string context_parser
     7.9    val const: bool -> string context_parser
    7.10    val const_proper: bool -> string context_parser
    7.11    val goal_spec: ((int -> tactic) -> tactic) context_parser
    7.12 @@ -208,8 +208,8 @@
    7.13  
    7.14  (* type and constant names *)
    7.15  
    7.16 -fun type_name strict =
    7.17 -  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) strict))
    7.18 +fun type_name flags =
    7.19 +  Scan.peek (fn ctxt => named_typ (Proof_Context.read_type_name (Context.proof_of ctxt) flags))
    7.20    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    7.21  
    7.22  fun const strict =
     8.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 11:32:16 2014 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 12:10:19 2014 +0100
     8.3 @@ -68,12 +68,9 @@
     8.4    val infer_type: Proof.context -> string * typ -> typ
     8.5    val inferred_param: string -> Proof.context -> typ * Proof.context
     8.6    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
     8.7 -  val check_type_name: Proof.context -> bool ->
     8.8 +  val check_type_name: Proof.context -> {proper: bool, strict: bool} ->
     8.9      xstring * Position.T -> typ * Position.report list
    8.10 -  val check_type_name_proper: Proof.context -> bool ->
    8.11 -    xstring * Position.T -> typ * Position.report list
    8.12 -  val read_type_name: Proof.context -> bool -> string -> typ
    8.13 -  val read_type_name_proper: Proof.context -> bool -> string -> typ
    8.14 +  val read_type_name: Proof.context -> {proper: bool, strict: bool} -> string -> typ
    8.15    val check_const_proper: Proof.context -> bool ->
    8.16      xstring * Position.T -> term * Position.report list
    8.17    val read_const_proper: Proof.context -> bool -> string -> term
    8.18 @@ -443,13 +440,15 @@
    8.19  
    8.20  (* type names *)
    8.21  
    8.22 -fun check_type_name ctxt strict (c, pos) =
    8.23 +fun check_type_name ctxt {proper, strict} (c, pos) =
    8.24    if Lexicon.is_tid c then
    8.25 -    let
    8.26 -      val reports =
    8.27 -        if Context_Position.is_reported ctxt pos
    8.28 -        then [(pos, Markup.tfree)] else [];
    8.29 -    in (TFree (c, default_sort ctxt (c, ~1)), reports) end
    8.30 +    if proper then error ("Not a type constructor: " ^ c ^ Position.here pos)
    8.31 +    else
    8.32 +      let
    8.33 +        val reports =
    8.34 +          if Context_Position.is_reported ctxt pos
    8.35 +          then [(pos, Markup.tfree)] else [];
    8.36 +      in (TFree (c, default_sort ctxt (c, ~1)), reports) end
    8.37    else
    8.38      let
    8.39        val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
    8.40 @@ -461,16 +460,12 @@
    8.41          | Type.Nonterminal => if strict then err () else 0);
    8.42      in (Type (d, replicate args dummyT), reports) end;
    8.43  
    8.44 -fun check_type_name_proper ctxt strict arg =
    8.45 -  (case check_type_name ctxt strict arg of
    8.46 -    res as (Type _, _) => res
    8.47 -  | (T, _) => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
    8.48 -
    8.49 -fun read_type_name ctxt strict =
    8.50 -  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name ctxt strict #> #1;
    8.51 -
    8.52 -fun read_type_name_proper ctxt strict =
    8.53 -  Syntax.read_token #> Symbol_Pos.source_content #> check_type_name_proper ctxt strict #> #1;
    8.54 +fun read_type_name ctxt flags text =
    8.55 +  let
    8.56 +    val (T, reports) =
    8.57 +      check_type_name ctxt flags (Symbol_Pos.source_content (Syntax.read_token text));
    8.58 +    val _ = Position.reports reports;
    8.59 +  in T end;
    8.60  
    8.61  
    8.62  (* constant names *)
    8.63 @@ -531,7 +526,8 @@
    8.64  in
    8.65  
    8.66  val read_arity =
    8.67 -  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
    8.68 +  prep_arity (fn ctxt => #1 o dest_Type o read_type_name ctxt {proper = true, strict = true})
    8.69 +    Syntax.read_sort;
    8.70  
    8.71  val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
    8.72  
     9.1 --- a/src/Pure/Isar/specification.ML	Thu Mar 06 11:32:16 2014 +0100
     9.2 +++ b/src/Pure/Isar/specification.ML	Thu Mar 06 12:10:19 2014 +0100
     9.3 @@ -276,7 +276,8 @@
     9.4  in
     9.5  
     9.6  val type_notation = gen_type_notation (K I);
     9.7 -val type_notation_cmd = gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt false);
     9.8 +val type_notation_cmd =
     9.9 +  gen_type_notation (fn ctxt => Proof_Context.read_type_name ctxt {proper = false, strict = false});
    9.10  
    9.11  val notation = gen_notation (K I);
    9.12  val notation_cmd = gen_notation (fn ctxt => Proof_Context.read_const ctxt false dummyT);
    10.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 11:32:16 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 06 12:10:19 2014 +0100
    10.3 @@ -127,7 +127,7 @@
    10.4  fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax)
    10.5    >> (fn (ctxt, (s, pos)) =>
    10.6      let
    10.7 -      val Type (c, _) = Proof_Context.read_type_name_proper ctxt false s;
    10.8 +      val Type (c, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s;
    10.9        val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos);
   10.10        val res =
   10.11          (case try check (c, decl) of
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 11:32:16 2014 +0100
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 12:10:19 2014 +0100
    11.3 @@ -170,7 +170,8 @@
    11.4            let
    11.5              val pos = Lexicon.pos_of_token tok;
    11.6              val (Type (c, _), rs) =
    11.7 -              Proof_Context.check_type_name_proper ctxt false (Lexicon.str_of_token tok, pos);
    11.8 +              Proof_Context.check_type_name ctxt {proper = true, strict = false}
    11.9 +                (Lexicon.str_of_token tok, pos);
   11.10              val _ = Unsynchronized.change reports (append (map (rpair "") rs));
   11.11            in [Ast.Constant (Lexicon.mark_type c)] end
   11.12        | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
    12.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 06 11:32:16 2014 +0100
    12.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 06 12:10:19 2014 +0100
    12.3 @@ -515,7 +515,7 @@
    12.4    Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
    12.5  
    12.6  fun pretty_type ctxt s =
    12.7 -  let val Type (name, _) = Proof_Context.read_type_name_proper ctxt false s
    12.8 +  let val Type (name, _) = Proof_Context.read_type_name ctxt {proper = true, strict = false} s
    12.9    in Pretty.str (Proof_Context.extern_type ctxt name) end;
   12.10  
   12.11  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
    13.1 --- a/src/Tools/Code/code_target.ML	Thu Mar 06 11:32:16 2014 +0100
    13.2 +++ b/src/Tools/Code/code_target.ML	Thu Mar 06 12:10:19 2014 +0100
    13.3 @@ -97,8 +97,8 @@
    13.4        else error ("No such type constructor: " ^ quote tyco);
    13.5    in tyco end;
    13.6  
    13.7 -fun read_tyco ctxt = #1 o dest_Type
    13.8 -  o Proof_Context.read_type_name_proper ctxt true;
    13.9 +fun read_tyco ctxt =
   13.10 +  #1 o dest_Type o Proof_Context.read_type_name ctxt {proper = true, strict = true};
   13.11  
   13.12  fun cert_class ctxt class =
   13.13    let
    14.1 --- a/src/Tools/induct.ML	Thu Mar 06 11:32:16 2014 +0100
    14.2 +++ b/src/Tools/induct.ML	Thu Mar 06 12:10:19 2014 +0100
    14.3 @@ -361,7 +361,7 @@
    14.4    Scan.lift (Args.$$$ k) >> K "";
    14.5  
    14.6  fun attrib add_type add_pred del =
    14.7 -  spec typeN (Args.type_name false) >> add_type ||
    14.8 +  spec typeN (Args.type_name {proper = false, strict = false}) >> add_type ||
    14.9    spec predN (Args.const false) >> add_pred ||
   14.10    spec setN (Args.const false) >> add_pred ||
   14.11    Scan.lift Args.del >> K del;
   14.12 @@ -883,7 +883,7 @@
   14.13        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
   14.14  
   14.15  fun rule get_type get_pred =
   14.16 -  named_rule typeN (Args.type_name false) get_type ||
   14.17 +  named_rule typeN (Args.type_name {proper = false, strict = false}) get_type ||
   14.18    named_rule predN (Args.const false) get_pred ||
   14.19    named_rule setN (Args.const false) get_pred ||
   14.20    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;