src/Pure/axclass.ML
changeset 25597 34860182b250
parent 25486 b944ef973109
child 25605 35a5f7f4b97b
     1.1 --- a/src/Pure/axclass.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -27,6 +27,16 @@
     1.4    val axiomatize_arity: arity -> theory -> theory
     1.5    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
     1.6    val instance_name: string * class -> string
     1.7 +  val declare_overloaded: string * typ -> theory -> term * theory
     1.8 +  val define_overloaded: string -> string * term -> theory -> thm * theory
     1.9 +  val inst_tyco_of: theory -> string * typ -> string option
    1.10 +  val unoverload: theory -> thm -> thm
    1.11 +  val overload: theory -> thm -> thm
    1.12 +  val unoverload_conv: theory -> conv
    1.13 +  val overload_conv: theory -> conv
    1.14 +  val unoverload_const: theory -> string * typ -> string
    1.15 +  val param_of_inst: theory -> string * string -> string
    1.16 +  val inst_of_param: theory -> string -> (string * string) option
    1.17    type cache
    1.18    val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
    1.19    val cache: cache
    1.20 @@ -88,23 +98,36 @@
    1.21    Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
    1.22  
    1.23  
    1.24 +(* instance parameters *)
    1.25 +
    1.26 +type inst_params =
    1.27 +  (string * thm) Symtab.table Symtab.table
    1.28 +    (*constant name ~> type constructor ~> (constant name, equation)*)
    1.29 +  * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
    1.30 +
    1.31 +fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
    1.32 +  (Symtab.join  (K (Symtab.merge (K true))) (const_param1, const_param2),
    1.33 +    Symtab.merge (K true) (param_const1, param_const2));
    1.34 +
    1.35 +
    1.36  (* setup data *)
    1.37  
    1.38  structure AxClassData = TheoryDataFun
    1.39  (
    1.40 -  type T = axclasses * instances;
    1.41 -  val empty = ((Symtab.empty, []), ([], Symtab.empty));
    1.42 +  type T = axclasses * (instances * inst_params);
    1.43 +  val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
    1.44    val copy = I;
    1.45    val extend = I;
    1.46 -  fun merge pp ((axclasses1, instances1), (axclasses2, instances2)) =
    1.47 -    (merge_axclasses pp (axclasses1, axclasses2), (merge_instances (instances1, instances2)));
    1.48 +  fun merge pp ((axclasses1, (instances1, inst_params1)), (axclasses2, (instances2, inst_params2))) =
    1.49 +    (merge_axclasses pp (axclasses1, axclasses2),
    1.50 +      (merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)));
    1.51  );
    1.52  
    1.53  
    1.54  (* maintain axclasses *)
    1.55  
    1.56  val get_axclasses = #1 o AxClassData.get;
    1.57 -fun map_axclasses f = AxClassData.map (apfst f);
    1.58 +val map_axclasses = AxClassData.map o apfst;
    1.59  
    1.60  val lookup_def = Symtab.lookup o #1 o get_axclasses;
    1.61  
    1.62 @@ -135,8 +158,8 @@
    1.63  
    1.64  fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
    1.65  
    1.66 -val get_instances = #2 o AxClassData.get;
    1.67 -fun map_instances f = AxClassData.map (apsnd f);
    1.68 +val get_instances = #1 o #2 o AxClassData.get;
    1.69 +val map_instances = AxClassData.map o apsnd o apfst;
    1.70  
    1.71  
    1.72  fun the_classrel thy (c1, c2) =
    1.73 @@ -159,6 +182,39 @@
    1.74    (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
    1.75  
    1.76  
    1.77 +(* maintain instance parameters *)
    1.78 +
    1.79 +val get_inst_params = #2 o #2 o AxClassData.get;
    1.80 +val map_inst_params = AxClassData.map o apsnd o apsnd;
    1.81 +
    1.82 +fun get_inst_param thy (c, tyco) =
    1.83 +  (the o Symtab.lookup ((the o Symtab.lookup (fst (get_inst_params thy))) c)) tyco;
    1.84 +
    1.85 +fun add_inst_param (c, tyco) inst = (map_inst_params o apfst
    1.86 +      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
    1.87 +  #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
    1.88 +
    1.89 +val inst_of_param = Symtab.lookup o snd o get_inst_params;
    1.90 +val param_of_inst = fst oo get_inst_param;
    1.91 +
    1.92 +fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
    1.93 +  (get_inst_params thy) [];
    1.94 +
    1.95 +val inst_tyco_of = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
    1.96 +
    1.97 +fun unoverload thy = MetaSimplifier.simplify true (inst_thms thy);
    1.98 +fun overload thy = MetaSimplifier.simplify true (map Thm.symmetric (inst_thms thy));
    1.99 +
   1.100 +fun unoverload_conv thy = MetaSimplifier.rewrite true (inst_thms thy);
   1.101 +fun overload_conv thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
   1.102 +
   1.103 +fun unoverload_const thy (c_ty as (c, _)) =
   1.104 +  case class_of_param thy c
   1.105 +   of SOME class => (case inst_tyco_of thy c_ty
   1.106 +       of SOME tyco => try (param_of_inst thy) (c, tyco) |> the_default c
   1.107 +        | NONE => c)
   1.108 +    | NONE => c;
   1.109 +
   1.110  
   1.111  (** instances **)
   1.112  
   1.113 @@ -200,10 +256,35 @@
   1.114      val prop = Thm.plain_prop_of (Thm.transfer thy th);
   1.115      val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   1.116      val _ = map (Sign.certify_sort thy) Ss = Ss orelse err ();
   1.117 +    (*FIXME turn this into a mere check as soon as "attach" has disappeared*)
   1.118 +    val missing_params = Sign.complete_sort thy [c]
   1.119 +      |> maps (these o Option.map (fn AxClass { params, ... } => params) o lookup_def thy)
   1.120 +      |> filter_out (fn (p, _) => can (get_inst_param thy) (p, t));
   1.121 +    fun declare_missing (p, T0) thy =
   1.122 +      let
   1.123 +        val name_inst = instance_name (t, c) ^ "_inst";
   1.124 +        val p' = NameSpace.base p ^ "_" ^ NameSpace.base t;
   1.125 +        val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy t) []);
   1.126 +        val T = map_atyps (fn _ => Type (t, map TFree vs)) T0;
   1.127 +      in
   1.128 +        thy
   1.129 +        |> Sign.sticky_prefix name_inst
   1.130 +        |> Sign.no_base_names
   1.131 +        |> Sign.declare_const [] (p', T, NoSyn)
   1.132 +        |-> (fn const' as Const (p'', _) => Thm.add_def false true
   1.133 +              (Thm.def_name p', Logic.mk_equals (const', Const (p, T)))
   1.134 +        #>> Thm.varifyT
   1.135 +        #-> (fn thm => add_inst_param (p, t) (p'', Thm.symmetric thm)
   1.136 +        #> PureThy.note Thm.internalK (p', thm)
   1.137 +        #> snd
   1.138 +        #> Sign.restore_naming thy))
   1.139 +      end;
   1.140 +
   1.141    in
   1.142      thy
   1.143      |> Sign.primitive_arity (t, Ss, [c])
   1.144      |> put_arity ((t, Ss, c), Drule.unconstrainTs th)
   1.145 +    |> fold declare_missing missing_params
   1.146    end;
   1.147  
   1.148  
   1.149 @@ -240,6 +321,47 @@
   1.150    end;
   1.151  
   1.152  
   1.153 +(* instance parameters and overloaded definitions *)
   1.154 +
   1.155 +(* declaration and definition of instances of overloaded constants *)
   1.156 +
   1.157 +fun declare_overloaded (c, T) thy =
   1.158 +  let
   1.159 +    val SOME class = class_of_param thy c;
   1.160 +    val SOME tyco = inst_tyco_of thy (c, T);
   1.161 +    val name_inst = instance_name (tyco, class) ^ "_inst";
   1.162 +    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
   1.163 +    val T' = Type.strip_sorts T;
   1.164 +  in
   1.165 +    thy
   1.166 +    |> Sign.sticky_prefix name_inst
   1.167 +    |> Sign.no_base_names
   1.168 +    |> Sign.declare_const [] (c', T', NoSyn)
   1.169 +    |-> (fn const' as Const (c'', _) => Thm.add_def false true
   1.170 +          (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
   1.171 +    #>> Thm.varifyT
   1.172 +    #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
   1.173 +    #> PureThy.note Thm.internalK (c', thm)
   1.174 +    #> snd
   1.175 +    #> Sign.restore_naming thy
   1.176 +    #> pair (Const (c, T))))
   1.177 +  end;
   1.178 +
   1.179 +fun define_overloaded name (c, t) thy =
   1.180 +  let
   1.181 +    val T = Term.fastype_of t;
   1.182 +    val SOME tyco = inst_tyco_of thy (c, T);
   1.183 +    val (c', eq) = get_inst_param thy (c, tyco);
   1.184 +    val prop = Logic.mk_equals (Const (c', T), t);
   1.185 +    val name' = Thm.def_name_optional
   1.186 +      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
   1.187 +  in
   1.188 +    thy
   1.189 +    |> Thm.add_def false false (name', prop)
   1.190 +    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
   1.191 +  end;
   1.192 +
   1.193 +
   1.194  
   1.195  (** class definitions **)
   1.196