clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
authorwenzelm
Thu Feb 25 22:06:43 2010 +0100 (2010-02-25)
changeset 35360df2b2168e43a
parent 35359 3ec03a3cd9d0
child 35361 4c7c849b70aa
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/Pure/Isar/args.ML
src/Pure/Isar/proof_context.ML
src/Tools/Code/code_eval.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:05:34 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:06:43 2010 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  fun setup_generate_fresh x =
     1.7 -  (Args.goal_spec -- Args.tyname >>
     1.8 +  (Args.goal_spec -- Args.type_name 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/Datatype/datatype_data.ML	Thu Feb 25 22:05:34 2010 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Feb 25 22:06:43 2010 +0100
     2.3 @@ -236,7 +236,7 @@
     2.4  
     2.5  (** document antiquotation **)
     2.6  
     2.7 -val _ = ThyOutput.antiquotation "datatype" Args.tyname
     2.8 +val _ = ThyOutput.antiquotation "datatype" (Args.type_name true)
     2.9    (fn {source = src, context = ctxt, ...} => fn dtco =>
    2.10      let
    2.11        val thy = ProofContext.theory_of ctxt;
     3.1 --- a/src/Pure/Isar/args.ML	Thu Feb 25 22:05:34 2010 +0100
     3.2 +++ b/src/Pure/Isar/args.ML	Thu Feb 25 22:06:43 2010 +0100
     3.3 @@ -54,7 +54,7 @@
     3.4    val term: term context_parser
     3.5    val term_abbrev: term context_parser
     3.6    val prop: term context_parser
     3.7 -  val tyname: string context_parser
     3.8 +  val type_name: bool -> string context_parser
     3.9    val const: string context_parser
    3.10    val const_proper: string context_parser
    3.11    val bang_facts: thm list context_parser
    3.12 @@ -209,7 +209,8 @@
    3.13  
    3.14  (* type and constant names *)
    3.15  
    3.16 -val tyname = Scan.peek (named_typ o ProofContext.read_tyname o Context.proof_of)
    3.17 +fun type_name strict =
    3.18 +  Scan.peek (fn ctxt => named_typ (ProofContext.read_type_name (Context.proof_of ctxt) strict))
    3.19    >> (fn Type (c, _) => c | TFree (a, _) => a | _ => "");
    3.20  
    3.21  val const = Scan.peek (named_term o ProofContext.read_const o Context.proof_of)
     4.1 --- a/src/Pure/Isar/proof_context.ML	Thu Feb 25 22:05:34 2010 +0100
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Feb 25 22:06:43 2010 +0100
     4.3 @@ -52,7 +52,7 @@
     4.4    val infer_type: Proof.context -> string -> typ
     4.5    val inferred_param: string -> Proof.context -> typ * Proof.context
     4.6    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
     4.7 -  val read_tyname: Proof.context -> string -> typ
     4.8 +  val read_type_name: Proof.context -> bool -> string -> typ
     4.9    val read_const_proper: Proof.context -> string -> term
    4.10    val read_const: Proof.context -> string -> term
    4.11    val allow_dummies: Proof.context -> Proof.context
    4.12 @@ -414,7 +414,7 @@
    4.13  
    4.14  in
    4.15  
    4.16 -fun read_tyname ctxt str =
    4.17 +fun read_type_name ctxt strict str =
    4.18    let
    4.19      val thy = theory_of ctxt;
    4.20      val (c, pos) = token_content str;
    4.21 @@ -425,8 +425,15 @@
    4.22      else
    4.23        let
    4.24          val d = Sign.intern_type thy c;
    4.25 +        val decl = Sign.the_type_decl thy d;
    4.26          val _ = Position.report (Markup.tycon d) pos;
    4.27 -      in Type (d, replicate (Sign.arity_number thy d) dummyT) end
    4.28 +        fun err () = error ("Bad type name: " ^ quote d);
    4.29 +        val args =
    4.30 +          (case decl of
    4.31 +            Type.LogicalType n => n
    4.32 +          | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
    4.33 +          | Type.Nonterminal => if strict then err () else 0);
    4.34 +      in Type (d, replicate args dummyT) end
    4.35    end;
    4.36  
    4.37  fun read_const_proper ctxt = prep_const_proper ctxt o token_content;
     5.1 --- a/src/Tools/Code/code_eval.ML	Thu Feb 25 22:05:34 2010 +0100
     5.2 +++ b/src/Tools/Code/code_eval.ML	Thu Feb 25 22:06:43 2010 +0100
     5.3 @@ -144,7 +144,7 @@
     5.4  
     5.5  val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
     5.6  val _ = ML_Context.add_antiq "code_datatype" (fn _ =>
     5.7 -  (Args.tyname --| Scan.lift (Args.$$$ "=")
     5.8 +  (Args.type_name true --| Scan.lift (Args.$$$ "=")
     5.9      -- (Args.term ::: Scan.repeat (Scan.lift (Args.$$$ "|") |-- Args.term)))
    5.10        >> ml_code_datatype_antiq);
    5.11  
     6.1 --- a/src/Tools/induct.ML	Thu Feb 25 22:05:34 2010 +0100
     6.2 +++ b/src/Tools/induct.ML	Thu Feb 25 22:06:43 2010 +0100
     6.3 @@ -345,7 +345,7 @@
     6.4    Scan.lift (Args.$$$ k) >> K "";
     6.5  
     6.6  fun attrib add_type add_pred del =
     6.7 -  spec typeN Args.tyname >> add_type ||
     6.8 +  spec typeN (Args.type_name true) >> add_type ||
     6.9    spec predN Args.const >> add_pred ||
    6.10    spec setN Args.const >> add_pred ||
    6.11    Scan.lift Args.del >> K del;
    6.12 @@ -856,7 +856,7 @@
    6.13        | NONE => error ("No rule for " ^ k ^ " " ^ quote name))))));
    6.14  
    6.15  fun rule get_type get_pred =
    6.16 -  named_rule typeN Args.tyname get_type ||
    6.17 +  named_rule typeN (Args.type_name true) get_type ||
    6.18    named_rule predN Args.const get_pred ||
    6.19    named_rule setN Args.const get_pred ||
    6.20    Scan.lift (Args.$$$ ruleN -- Args.colon) |-- Attrib.thms;