dropped Class.prep_spec
authorhaftmann
Tue Dec 11 10:23:10 2007 +0100 (2007-12-11)
changeset 256034b7a58fc168c
parent 25602 137ebc0603f4
child 25604 6c1714b9b805
dropped Class.prep_spec
src/HOL/Library/Eval.thy
src/Pure/Isar/class.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Tue Dec 11 10:23:09 2007 +0100
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Dec 11 10:23:10 2007 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4        val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ})
     1.5          $ Free ("T", Term.itselfT ty);
     1.6        val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty;
     1.7 -      val eq = Class.prep_spec lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
     1.8 +      val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
     1.9      in lthy |> Specification.definition (NONE, (("", []), eq)) end;
    1.10    fun interpretator tyco thy =
    1.11      let
    1.12 @@ -151,7 +151,7 @@
    1.13      end;
    1.14    fun prep' ctxt proto_eqs =
    1.15      let
    1.16 -      val eqs as eq :: _ = map (Class.prep_spec ctxt) proto_eqs;
    1.17 +      val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs;
    1.18        val (Free (v, ty), _) =
    1.19          (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
    1.20      in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end;
     2.1 --- a/src/Pure/Isar/class.ML	Tue Dec 11 10:23:09 2007 +0100
     2.2 +++ b/src/Pure/Isar/class.ML	Tue Dec 11 10:23:10 2007 +0100
     2.3 @@ -14,9 +14,9 @@
     2.4      -> xstring list -> theory -> string * Proof.context
     2.5  
     2.6    val init: class -> theory -> Proof.context
     2.7 -  val logical_const: string -> Markup.property list
     2.8 +  val declare: string -> Markup.property list
     2.9      -> (string * mixfix) * term -> theory -> theory
    2.10 -  val syntactic_const: string -> Syntax.mode -> Markup.property list
    2.11 +  val abbrev: string -> Syntax.mode -> Markup.property list
    2.12      -> (string * mixfix) * term -> theory -> theory
    2.13    val refresh_syntax: class -> Proof.context -> Proof.context
    2.14  
    2.15 @@ -32,12 +32,12 @@
    2.16  
    2.17    (*instances*)
    2.18    val init_instantiation: string list * sort list * sort -> theory -> local_theory
    2.19 -  val prep_spec: local_theory -> term -> term
    2.20    val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    2.21    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    2.22    val conclude_instantiation: local_theory -> local_theory
    2.23 -  val instantiation_param: Proof.context -> string -> string option
    2.24 +  val instantiation_param: local_theory -> string -> string option
    2.25    val confirm_declaration: string -> local_theory -> local_theory
    2.26 +  val pretty_instantiation: local_theory -> Pretty.T
    2.27  
    2.28    (*old axclass layer*)
    2.29    val axclass_cmd: bstring * xstring list
    2.30 @@ -676,7 +676,7 @@
    2.31  
    2.32  (* class target *)
    2.33  
    2.34 -fun logical_const class pos ((c, mx), dict) thy =
    2.35 +fun declare class pos ((c, mx), dict) thy =
    2.36    let
    2.37      val prfx = class_prefix class;
    2.38      val thy' = thy |> Sign.add_path prfx;
    2.39 @@ -699,7 +699,7 @@
    2.40      |> Sign.add_const_constraint (c', SOME ty')
    2.41    end;
    2.42  
    2.43 -fun syntactic_const class prmode pos ((c, mx), rhs) thy =
    2.44 +fun abbrev class prmode pos ((c, mx), rhs) thy =
    2.45    let
    2.46      val prfx = class_prefix class;
    2.47      val thy' = thy |> Sign.add_path prfx;
    2.48 @@ -726,7 +726,7 @@
    2.49  datatype instantiation = Instantiation of {
    2.50    arities: string list * sort list * sort,
    2.51    params: ((string * string) * (string * typ)) list
    2.52 -    (*(instantiation const, type constructor), (local instantiation parameter, typ)*)
    2.53 +    (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
    2.54  }
    2.55  
    2.56  structure Instantiation = ProofDataFun
    2.57 @@ -766,12 +766,6 @@
    2.58        | NONE => t)
    2.59    | t => t);
    2.60  
    2.61 -fun prep_spec lthy =
    2.62 -  let
    2.63 -    val thy = ProofContext.theory_of lthy;
    2.64 -    val params = instantiation_params lthy;
    2.65 -  in subst_param thy params end;
    2.66 -
    2.67  fun inst_term_check ts lthy =
    2.68    let
    2.69      val params = instantiation_params lthy;
    2.70 @@ -826,7 +820,7 @@
    2.71        | type_name "+" = "sum"
    2.72        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
    2.73      fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
    2.74 -      then NONE else SOME ((AxClass.unoverload_const thy (c, ty), tyco),
    2.75 +      then NONE else SOME ((c, tyco),
    2.76          (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
    2.77      val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    2.78    in
    2.79 @@ -871,4 +865,18 @@
    2.80          tycos;
    2.81    in lthy end;
    2.82  
    2.83 +fun pretty_instantiation lthy =
    2.84 +  let
    2.85 +    val { arities, params } = the_instantiation lthy;
    2.86 +    val (tycos, sorts, sort) = arities;
    2.87 +    val thy = ProofContext.theory_of lthy;
    2.88 +    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, sorts, sort);
    2.89 +    fun pr_param ((c, _), (v, ty)) =
    2.90 +      (Pretty.block o Pretty.breaks) [(Pretty.str o Sign.extern_const thy) c, Pretty.str "::",
    2.91 +        Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
    2.92 +  in
    2.93 +    (Pretty.block o Pretty.fbreaks)
    2.94 +      (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
    2.95 +  end;
    2.96 +
    2.97  end;