src/Pure/Isar/class.ML
changeset 25864 11f531354852
parent 25829 4b44d945702f
child 25999 f8bcd311d501
     1.1 --- a/src/Pure/Isar/class.ML	Tue Jan 08 11:37:29 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Jan 08 11:37:30 2008 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4    val print_classes: theory -> unit
     1.5  
     1.6    (*instances*)
     1.7 -  val init_instantiation: string list * sort list * sort -> theory -> local_theory
     1.8 +  val init_instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     1.9    val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state
    1.10    val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory
    1.11    val conclude_instantiation: local_theory -> local_theory
    1.12 @@ -681,7 +681,7 @@
    1.13  (* bookkeeping *)
    1.14  
    1.15  datatype instantiation = Instantiation of {
    1.16 -  arities: string list * sort list * sort,
    1.17 +  arities: string list * (string * sort) list * sort,
    1.18    params: ((string * string) * (string * typ)) list
    1.19      (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
    1.20  }
    1.21 @@ -768,25 +768,24 @@
    1.22      explode #> scan_valids #> implode
    1.23    end;
    1.24  
    1.25 -fun init_instantiation (tycos, sorts, sort) thy =
    1.26 +fun init_instantiation (tycos, vs, sort) thy =
    1.27    let
    1.28      val _ = if null tycos then error "At least one arity must be given" else ();
    1.29      val _ = map (the_class_data thy) sort;
    1.30 -    val vs = map TFree (Name.names Name.context Name.aT sorts);
    1.31      fun type_name "*" = "prod"
    1.32        | type_name "+" = "sum"
    1.33        | type_name s = sanatize_name (NameSpace.base s); (*FIXME*)
    1.34      fun get_param tyco (param, (c, ty)) = if can (AxClass.param_of_inst thy) (c, tyco)
    1.35        then NONE else SOME ((c, tyco),
    1.36 -        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty));
    1.37 +        (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
    1.38      val params = map_product get_param tycos (these_params thy sort) |> map_filter I;
    1.39    in
    1.40      thy
    1.41      |> ProofContext.init
    1.42 -    |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params))
    1.43 -    |> fold (Variable.declare_term o Logic.mk_type) vs
    1.44 +    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.45 +    |> fold (Variable.declare_term o Logic.mk_type o TFree) vs
    1.46      |> fold (Variable.declare_names o Free o snd) params
    1.47 -    |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos
    1.48 +    |> fold (fn tyco => ProofContext.add_arity (tyco, map snd vs, sort)) tycos
    1.49      |> Context.proof_map (
    1.50          Syntax.add_term_check 0 "instance" inst_term_check
    1.51          #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck)
    1.52 @@ -794,8 +793,8 @@
    1.53  
    1.54  fun gen_instantiation_instance do_proof after_qed lthy =
    1.55    let
    1.56 -    val (tycos, sorts, sort) = (#arities o the_instantiation) lthy;
    1.57 -    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.58 +    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    1.59 +    val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    1.60      fun after_qed' results =
    1.61        LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
    1.62        #> after_qed;
    1.63 @@ -814,10 +813,10 @@
    1.64  fun conclude_instantiation lthy =
    1.65    let
    1.66      val { arities, params } = the_instantiation lthy;
    1.67 -    val (tycos, sorts, sort) = arities;
    1.68 +    val (tycos, vs, sort) = arities;
    1.69      val thy = ProofContext.theory_of lthy;
    1.70      val _ = map (fn tyco => if Sign.of_sort thy
    1.71 -        (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
    1.72 +        (Type (tyco, map TFree vs), sort)
    1.73        then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
    1.74          tycos;
    1.75      (*this checkpoint should move to AxClass as soon as "attach" has disappeared*)
    1.76 @@ -830,12 +829,12 @@
    1.77  fun pretty_instantiation lthy =
    1.78    let
    1.79      val { arities, params } = the_instantiation lthy;
    1.80 -    val (tycos, sorts, sort) = arities;
    1.81 +    val (tycos, vs, sort) = arities;
    1.82      val thy = ProofContext.theory_of lthy;
    1.83 -    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, sorts, sort);
    1.84 +    fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    1.85      fun pr_param ((c, _), (v, ty)) =
    1.86 -      (Pretty.block o Pretty.breaks) [(Pretty.str o Sign.extern_const thy) c, Pretty.str "::",
    1.87 -        Sign.pretty_typ thy ty, Pretty.str "as", Pretty.str v];
    1.88 +      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    1.89 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
    1.90    in
    1.91      (Pretty.block o Pretty.fbreaks)
    1.92        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)