replaced Sign.add_consts_authentic by Sign.declare_const;
authorwenzelm
Thu Oct 11 16:05:44 2007 +0200 (2007-10-11)
changeset 24968f9bafc868847
parent 24967 68c5c62bed13
child 24969 b38527eefb3b
replaced Sign.add_consts_authentic by Sign.declare_const;
replaced read_param by Sign.read_const, which is independent of syntax;
added define_class_params (from axclass.ML);
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 11 16:05:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 11 16:05:44 2007 +0200
     1.3 @@ -179,9 +179,11 @@
     1.4    in
     1.5      thy
     1.6      |> Sign.sticky_prefix name_inst
     1.7 -    |> PureThy.simple_def ("", [])
     1.8 -         (((c_inst_base, ty, Syntax.NoSyn), []), Const (c, ty))
     1.9 -    |-> (fn (c_inst, thm) => add_inst (c, tyco) (c_inst, symmetric thm))
    1.10 +    |> Sign.declare_const [] (c_inst_base, ty, Syntax.NoSyn)
    1.11 +    |-> (fn const as Const (c_inst, _) =>
    1.12 +      PureThy.add_defs_i false
    1.13 +        [((Thm.def_name c_inst_base, Logic.mk_equals (const, Const (c, ty))), [])]
    1.14 +      #-> (fn [thm] => add_inst (c, tyco) (c_inst, Thm.symmetric thm)))
    1.15      |> Sign.restore_naming thy
    1.16    end;
    1.17  
    1.18 @@ -245,7 +247,7 @@
    1.19        end;
    1.20      fun get_consts_class tyco ty class =
    1.21        let
    1.22 -        val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
    1.23 +        val cs = (these o try (#params o AxClass.get_info theory)) class;
    1.24          val subst_ty = map_type_tfree (K ty);
    1.25        in
    1.26          map (fn (c, ty) => (c, ((class, tyco), subst_ty ty))) cs
    1.27 @@ -615,14 +617,6 @@
    1.28  
    1.29  local
    1.30  
    1.31 -fun read_param thy raw_t =  (* FIXME ProofContext.read_const (!?) *)
    1.32 -  let
    1.33 -    val t = Syntax.read_term_global thy raw_t
    1.34 -  in case try dest_Const t
    1.35 -   of SOME (c, _) => c
    1.36 -    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    1.37 -  end;
    1.38 -
    1.39  fun gen_class_spec prep_class prep_expr process_expr thy raw_supclasses raw_includes_elems =
    1.40    let
    1.41      val supclasses = map (prep_class thy) raw_supclasses;
    1.42 @@ -652,12 +646,38 @@
    1.43  val read_class_spec = gen_class_spec Sign.intern_class Locale.intern_expr Locale.read_expr;
    1.44  val check_class_spec = gen_class_spec (K I) (K I) Locale.cert_expr;
    1.45  
    1.46 +
    1.47 +fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    1.48 +  let
    1.49 +    val superclasses = map (Sign.certify_class thy) raw_superclasses;
    1.50 +    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
    1.51 +    fun add_const ((c, ty), syn) = Sign.declare_const [] (c, ty, syn) #>> Term.dest_Const;
    1.52 +    fun mk_axioms cs thy =
    1.53 +      raw_dep_axioms thy cs
    1.54 +      |> (map o apsnd o map) (Sign.cert_prop thy)
    1.55 +      |> rpair thy;
    1.56 +    fun add_constraint class (c, ty) =
    1.57 +      Sign.add_const_constraint (c, SOME
    1.58 +        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    1.59 +  in
    1.60 +    thy
    1.61 +    |> Sign.add_path (Logic.const_of_class name)
    1.62 +    |> fold_map add_const consts
    1.63 +    ||> Sign.restore_naming thy
    1.64 +    |-> (fn cs => mk_axioms cs
    1.65 +    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
    1.66 +           (map fst cs @ other_consts) axioms_prop
    1.67 +    #-> (fn class => `(fn thy => AxClass.get_info thy class)
    1.68 +    #-> (fn {axioms, ...} => fold (add_constraint class) cs
    1.69 +    #> pair (class, (cs, axioms))))))
    1.70 +  end;
    1.71 +
    1.72  fun gen_class prep_spec prep_param local_syntax bname
    1.73      raw_supclasses raw_includes_elems raw_other_consts thy =
    1.74    let
    1.75      val (((sups, supconsts), (supsort, local_sort, mergeexpr)), elems) =
    1.76        prep_spec thy raw_supclasses raw_includes_elems;
    1.77 -    val other_consts = map (prep_param thy) raw_other_consts;
    1.78 +    val other_consts = map (tap (Sign.the_const_type thy) o prep_param thy) raw_other_consts;
    1.79      fun mk_instT class = Symtab.empty
    1.80        |> Symtab.update (Name.aT, TFree (Name.aT, [class]));
    1.81      fun mk_inst class param_names cs =
    1.82 @@ -701,7 +721,7 @@
    1.83      |-> (fn name_locale => ProofContext.theory_result (
    1.84        `(fn thy => extract_params thy name_locale)
    1.85        #-> (fn (globals, params) =>
    1.86 -        AxClass.define_class_params (bname, supsort) params
    1.87 +        define_class_params (bname, supsort) params
    1.88            (extract_assumes name_locale params) other_consts
    1.89        #-> (fn (name_axclass, (consts, axioms)) =>
    1.90          `(fn thy => class_intro thy name_locale name_axclass sups)
    1.91 @@ -718,7 +738,7 @@
    1.92  
    1.93  in
    1.94  
    1.95 -val class_cmd = gen_class read_class_spec read_param;
    1.96 +val class_cmd = gen_class read_class_spec ((#1 o Term.dest_Const) oo Sign.read_const);
    1.97  val class = gen_class check_class_spec (K I);
    1.98  
    1.99  end; (*local*)
   1.100 @@ -773,7 +793,7 @@
   1.101    in
   1.102      thy
   1.103      |> Sign.add_path prfx
   1.104 -    |> Sign.add_consts_authentic [] [(c, ty', syn')]
   1.105 +    |> Sign.declare_const [] (c, ty', syn') |> snd
   1.106      |> Sign.parent_path
   1.107      |> Sign.sticky_prefix prfx
   1.108      |> PureThy.add_defs_i false [(def, [])]