more systematic treatment of data -- avoid slightly odd nested tuples here;
authorwenzelm
Sun Apr 25 22:50:47 2010 +0200 (2010-04-25 ago)
changeset 3632985004134055c
parent 36328 4d9deabf6474
child 36330 0584e203960e
more systematic treatment of data -- avoid slightly odd nested tuples here;
tuned;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Sun Apr 25 21:18:04 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 25 22:50:47 2010 +0200
     1.3 @@ -44,6 +44,18 @@
     1.4  
     1.5  (** theory data **)
     1.6  
     1.7 +(* axclass info *)
     1.8 +
     1.9 +type info =
    1.10 + {def: thm,
    1.11 +  intro: thm,
    1.12 +  axioms: thm list,
    1.13 +  params: (string * typ) list};
    1.14 +
    1.15 +fun make_axclass (def, intro, axioms, params): info =
    1.16 +  {def = def, intro = intro, axioms = axioms, params = params};
    1.17 +
    1.18 +
    1.19  (* class parameters (canonical order) *)
    1.20  
    1.21  type param = string * class;
    1.22 @@ -55,85 +67,109 @@
    1.23        " for " ^ Pretty.string_of_sort pp [c] ^
    1.24        (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
    1.25  
    1.26 -fun merge_params _ ([], qs) = qs
    1.27 -  | merge_params pp (ps, qs) =
    1.28 -      fold_rev (fn q => if member (op =) ps q then I else add_param pp q) qs ps;
    1.29 -
    1.30 -
    1.31 -(* axclass info *)
    1.32 -
    1.33 -type info =
    1.34 - {def: thm,
    1.35 -  intro: thm,
    1.36 -  axioms: thm list,
    1.37 -  params: (string * typ) list};
    1.38 -
    1.39 -type axclasses = info Symtab.table * param list;
    1.40 -
    1.41 -fun make_axclass ((def, intro, axioms), params): info =
    1.42 -  {def = def, intro = intro, axioms = axioms, params = params};
    1.43 -
    1.44 -fun merge_axclasses pp ((tab1, params1), (tab2, params2)) : axclasses =
    1.45 -  (Symtab.merge (K true) (tab1, tab2), merge_params pp (params1, params2));
    1.46 -
    1.47 -
    1.48 -(* instances *)
    1.49 -
    1.50 -val classrel_prefix = "classrel_";
    1.51 -val arity_prefix = "arity_";
    1.52 -
    1.53 -type instances =
    1.54 -  (thm * proof) Symreltab.table *  (*classrel theorems*)
    1.55 -  ((class * sort list) * ((thm * string) * proof)) list Symtab.table;  (*arity theorems with theory name*)
    1.56 -
    1.57 -(*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
    1.58 -fun merge_instances ((classrel1, arities1): instances, (classrel2, arities2)) =
    1.59 - (Symreltab.join (K fst) (classrel1, classrel2),
    1.60 -  Symtab.join (K (merge (eq_fst op =))) (arities1, arities2));
    1.61 -
    1.62 -
    1.63 -(* instance parameters *)
    1.64 -
    1.65 -type inst_params =
    1.66 -  (string * thm) Symtab.table Symtab.table
    1.67 -    (*constant name ~> type constructor ~> (constant name, equation)*)
    1.68 -  * (string * string) Symtab.table; (*constant name ~> (constant name, type constructor)*)
    1.69 -
    1.70 -fun merge_inst_params ((const_param1, param_const1), (const_param2, param_const2)) =
    1.71 -  (Symtab.join  (K (Symtab.merge (K true))) (const_param1, const_param2),
    1.72 -    Symtab.merge (K true) (param_const1, param_const2));
    1.73 -
    1.74  
    1.75  (* setup data *)
    1.76  
    1.77 +datatype data = Data of
    1.78 + {axclasses: info Symtab.table,
    1.79 +  params: param list,
    1.80 +  proven_classrels: (thm * proof) Symreltab.table,
    1.81 +  proven_arities: ((class * sort list) * ((thm * string) * proof)) list Symtab.table,
    1.82 +    (*arity theorems with theory name*)
    1.83 +  inst_params:
    1.84 +    (string * thm) Symtab.table Symtab.table *
    1.85 +      (*constant name ~> type constructor ~> (constant name, equation)*)
    1.86 +    (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
    1.87 +  diff_merge_classrels: (class * class) list};
    1.88 +
    1.89 +fun make_data
    1.90 +    (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
    1.91 +  Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
    1.92 +    proven_arities = proven_arities, inst_params = inst_params,
    1.93 +    diff_merge_classrels = diff_merge_classrels};
    1.94 +
    1.95  structure Data = Theory_Data_PP
    1.96  (
    1.97 -  type T = axclasses * ((instances * inst_params) * (class * class) list);
    1.98 -  val empty = ((Symtab.empty, []), (((Symreltab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)), []));
    1.99 +  type T = data;
   1.100 +  val empty =
   1.101 +    make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty), []);
   1.102    val extend = I;
   1.103 -  fun merge pp ((axclasses1, ((instances1, inst_params1), diff_merge_classrels1)),
   1.104 -    (axclasses2, ((instances2, inst_params2), diff_merge_classrels2))) =
   1.105 +  fun merge pp
   1.106 +      (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
   1.107 +        proven_arities = proven_arities1, inst_params = inst_params1,
   1.108 +        diff_merge_classrels = diff_merge_classrels1},
   1.109 +       Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
   1.110 +        proven_arities = proven_arities2, inst_params = inst_params2,
   1.111 +        diff_merge_classrels = diff_merge_classrels2}) =
   1.112      let
   1.113 -      val (classrels1, classrels2) = pairself (Symreltab.keys o fst) (instances1, instances2);
   1.114 -      val diff_merge_classrels =
   1.115 +      val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
   1.116 +      val params' =
   1.117 +        if null params1 then params2
   1.118 +        else fold_rev (fn q => if member (op =) params1 q then I else add_param pp q) params2 params1;
   1.119 +
   1.120 +      (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
   1.121 +      val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
   1.122 +      val proven_arities' =
   1.123 +        Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
   1.124 +
   1.125 +      val classrels1 = Symreltab.keys proven_classrels1;
   1.126 +      val classrels2 = Symreltab.keys proven_classrels2;
   1.127 +      val diff_merge_classrels' =
   1.128          subtract (op =) classrels1 classrels2 @
   1.129          subtract (op =) classrels2 classrels1 @
   1.130          diff_merge_classrels1 @ diff_merge_classrels2;
   1.131 +
   1.132 +      val inst_params' =
   1.133 +        (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
   1.134 +          Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
   1.135      in
   1.136 -      (merge_axclasses pp (axclasses1, axclasses2),
   1.137 -        ((merge_instances (instances1, instances2), merge_inst_params (inst_params1, inst_params2)),
   1.138 -          diff_merge_classrels))
   1.139 +      make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
   1.140 +        diff_merge_classrels')
   1.141      end;
   1.142  );
   1.143  
   1.144 +fun map_data f =
   1.145 +  Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
   1.146 +    make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
   1.147 +
   1.148 +fun map_axclasses f =
   1.149 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
   1.150 +    (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
   1.151 +
   1.152 +fun map_params f =
   1.153 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
   1.154 +    (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
   1.155 +
   1.156 +fun map_proven_classrels f =
   1.157 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
   1.158 +    (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
   1.159 +
   1.160 +fun map_proven_arities f =
   1.161 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
   1.162 +    (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
   1.163 +
   1.164 +fun map_inst_params f =
   1.165 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
   1.166 +    (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
   1.167 +
   1.168 +val clear_diff_merge_classrels =
   1.169 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
   1.170 +    (axclasses, params, proven_classrels, proven_arities, inst_params, []));
   1.171 +
   1.172 +val rep_data = Data.get #> (fn Data args => args);
   1.173 +
   1.174 +val axclasses_of = #axclasses o rep_data;
   1.175 +val params_of = #params o rep_data;
   1.176 +val proven_classrels_of = #proven_classrels o rep_data;
   1.177 +val proven_arities_of = #proven_arities o rep_data;
   1.178 +val inst_params_of = #inst_params o rep_data;
   1.179 +val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
   1.180 +
   1.181  
   1.182  (* maintain axclasses *)
   1.183  
   1.184 -val get_axclasses = #1 o Data.get;
   1.185 -val map_axclasses = Data.map o apfst;
   1.186 -
   1.187  fun get_info thy c =
   1.188 -  (case Symtab.lookup (#1 (get_axclasses thy)) c of
   1.189 +  (case Symtab.lookup (axclasses_of thy) c of
   1.190      SOME info => info
   1.191    | NONE => error ("No such axclass: " ^ quote c));
   1.192  
   1.193 @@ -143,40 +179,40 @@
   1.194      val classes = Sign.all_classes thy;
   1.195    in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
   1.196  
   1.197 +
   1.198 +(* maintain params *)
   1.199 +
   1.200  fun all_params_of thy S =
   1.201 -  let val params = #2 (get_axclasses thy);
   1.202 +  let val params = params_of thy;
   1.203    in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;
   1.204  
   1.205 -fun class_of_param thy = AList.lookup (op =) (#2 (get_axclasses thy));
   1.206 +fun class_of_param thy = AList.lookup (op =) (params_of thy);
   1.207  
   1.208  
   1.209  (* maintain instances *)
   1.210  
   1.211 -fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
   1.212 +val classrel_prefix = "classrel_";
   1.213 +val arity_prefix = "arity_";
   1.214  
   1.215 -val get_instances = #1 o #1 o #2 o Data.get;
   1.216 -val map_instances = Data.map o apsnd o apfst o apfst;
   1.217 -
   1.218 -val get_diff_merge_classrels = #2 o #2 o Data.get;
   1.219 -val clear_diff_merge_classrels = Data.map (apsnd (apsnd (K [])));
   1.220 +fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
   1.221  
   1.222  
   1.223  fun the_classrel thy (c1, c2) =
   1.224 -  (case Symreltab.lookup (#1 (get_instances thy)) (c1, c2) of
   1.225 +  (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
   1.226      SOME classrel => classrel
   1.227    | NONE => error ("Unproven class relation " ^
   1.228        Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
   1.229  
   1.230 -fun the_classrel_thm thy = Thm.transfer thy o fst o the_classrel thy;
   1.231 -fun the_classrel_prf thy = snd o the_classrel thy;
   1.232 +fun the_classrel_thm thy = Thm.transfer thy o #1 o the_classrel thy;
   1.233 +fun the_classrel_prf thy = #2 o the_classrel thy;
   1.234  
   1.235  fun put_trancl_classrel ((c1, c2), th) thy =
   1.236    let
   1.237      val cert = Thm.cterm_of thy;
   1.238      val certT = Thm.ctyp_of thy;
   1.239  
   1.240 -    val classrels = fst (get_instances thy);
   1.241      val classes = Sorts.classes_of (Sign.classes_of thy);
   1.242 +    val classrels = proven_classrels_of thy;
   1.243  
   1.244      fun reflcl_classrel (c1', c2') =
   1.245        if c1' = c2'
   1.246 @@ -187,7 +223,7 @@
   1.247          val th' = ((reflcl_classrel (c1_pred, c1) RS th) RS reflcl_classrel (c2, c2_succ))
   1.248            |> Drule.instantiate' [SOME (certT (TVar ((Name.aT, 0), [])))] []
   1.249            |> Thm.close_derivation;
   1.250 -        val prf' = th' |> Thm.proof_of;
   1.251 +        val prf' = Thm.proof_of th';
   1.252        in ((c1_pred, c2_succ), (th', prf')) end;
   1.253  
   1.254      val new_classrels =
   1.255 @@ -197,38 +233,36 @@
   1.256      val needed = not (null new_classrels);
   1.257    in
   1.258      (needed,
   1.259 -     if needed then
   1.260 -       thy |> map_instances (fn (classrels, arities) =>
   1.261 -         (classrels |> fold Symreltab.update new_classrels, arities))
   1.262 -     else thy)
   1.263 +      if needed then map_proven_classrels (fold Symreltab.update new_classrels) thy
   1.264 +      else thy)
   1.265    end;
   1.266  
   1.267  fun complete_classrels thy =
   1.268    let
   1.269 -    val diff_merge_classrels = get_diff_merge_classrels thy;
   1.270 -    val classrels = fst (get_instances thy);
   1.271 +    val classrels = proven_classrels_of thy;
   1.272 +    val diff_merge_classrels = diff_merge_classrels_of thy;
   1.273      val (needed, thy') = (false, thy) |>
   1.274        fold (fn c12 => fn (needed, thy) =>
   1.275 -          put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> fst) thy
   1.276 +          put_trancl_classrel (c12, Symreltab.lookup classrels c12 |> the |> #1) thy
   1.277            |>> (fn b => needed orelse b))
   1.278          diff_merge_classrels;
   1.279    in
   1.280      if null diff_merge_classrels then NONE
   1.281 -    else thy' |> clear_diff_merge_classrels |> SOME
   1.282 +    else SOME (clear_diff_merge_classrels thy')
   1.283    end;
   1.284  
   1.285  
   1.286  fun the_arity thy a (c, Ss) =
   1.287 -  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
   1.288 +  (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
   1.289      SOME arity => arity
   1.290    | NONE => error ("Unproven type arity " ^
   1.291        Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
   1.292  
   1.293 -fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> fst |> fst |> Thm.transfer thy;
   1.294 -fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> snd;
   1.295 +fun the_arity_thm thy a c_Ss = the_arity thy a c_Ss |> #1 |> #1 |> Thm.transfer thy;
   1.296 +fun the_arity_prf thy a c_Ss = the_arity thy a c_Ss |> #2;
   1.297  
   1.298  fun thynames_of_arity thy (c, a) =
   1.299 -  Symtab.lookup_list (#2 (get_instances thy)) a
   1.300 +  Symtab.lookup_list (proven_arities_of thy) a
   1.301    |> map_filter (fn ((c', _), ((_, name),_)) => if c = c' then SOME name else NONE)
   1.302    |> rev;
   1.303  
   1.304 @@ -256,34 +290,30 @@
   1.305      val arity' = (t, ((c, Ss), ((th, Context.theory_name thy), Thm.proof_of th)));
   1.306    in
   1.307      thy
   1.308 -    |> map_instances (fn (classrel, arities) => (classrel,
   1.309 -      arities
   1.310 -      |> Symtab.insert_list (eq_fst op =) arity'
   1.311 -      |> insert_arity_completions thy arity'
   1.312 -      |> snd))
   1.313 +    |> map_proven_arities
   1.314 +      (Symtab.insert_list (eq_fst op =) arity' #>
   1.315 +        insert_arity_completions thy arity' #> snd)
   1.316    end;
   1.317  
   1.318  fun complete_arities thy =
   1.319    let
   1.320 -    val arities = snd (get_instances thy);
   1.321 +    val arities = proven_arities_of thy;
   1.322      val (finished, arities') = arities
   1.323        |> fold_map (insert_arity_completions thy) (Symtab.dest_list arities);
   1.324    in
   1.325 -    if forall I finished then NONE
   1.326 -    else SOME (thy |> map_instances (fn (classrel, _) => (classrel, arities')))
   1.327 +    if forall I finished
   1.328 +    then NONE
   1.329 +    else SOME (map_proven_arities (K arities') thy)
   1.330    end;
   1.331  
   1.332  val _ = Context.>> (Context.map_theory
   1.333 -  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities))
   1.334 +  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
   1.335  
   1.336  
   1.337  (* maintain instance parameters *)
   1.338  
   1.339 -val get_inst_params = #2 o #1 o #2 o Data.get;
   1.340 -val map_inst_params = Data.map o apsnd o apfst o apsnd;
   1.341 -
   1.342  fun get_inst_param thy (c, tyco) =
   1.343 -  (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (get_inst_params thy)) c)) tyco of
   1.344 +  (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
   1.345      SOME c' => c'
   1.346    | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
   1.347  
   1.348 @@ -291,11 +321,11 @@
   1.349    (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   1.350    #> (map_inst_params o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   1.351  
   1.352 -val inst_of_param = Symtab.lookup o snd o get_inst_params;
   1.353 +val inst_of_param = Symtab.lookup o #2 o inst_params_of;
   1.354  val param_of_inst = fst oo get_inst_param;
   1.355  
   1.356  fun inst_thms thy =
   1.357 -  (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) (get_inst_params thy) [];
   1.358 +  Symtab.fold (Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of thy)) [];
   1.359  
   1.360  fun get_inst_tyco consts = try (fst o dest_Type o the_single o Consts.typargs consts);
   1.361  
   1.362 @@ -339,8 +369,6 @@
   1.363    cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
   1.364      handle TYPE (msg, _, _) => error msg;
   1.365  
   1.366 -val shyps_topped = forall null o #shyps o Thm.rep_thm;
   1.367 -
   1.368  
   1.369  (* declaration and definition of instances of overloaded constants *)
   1.370  
   1.371 @@ -392,6 +420,8 @@
   1.372  
   1.373  (* primitive rules *)
   1.374  
   1.375 +val shyps_topped = forall null o #shyps o Thm.rep_thm;
   1.376 +
   1.377  fun add_classrel raw_th thy =
   1.378    let
   1.379      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
   1.380 @@ -562,16 +592,15 @@
   1.381  
   1.382      (* result *)
   1.383  
   1.384 -    val axclass = make_axclass ((def, intro, axioms), params);
   1.385 +    val axclass = make_axclass (def, intro, axioms, params);
   1.386      val result_thy =
   1.387        facts_thy
   1.388        |> fold (snd oo put_trancl_classrel) (map (pair class) super ~~ classrel)
   1.389        |> Sign.qualified_path false bconst
   1.390        |> PureThy.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms)) |> snd
   1.391        |> Sign.restore_naming facts_thy
   1.392 -      |> map_axclasses (fn (axclasses, parameters) =>
   1.393 -        (Symtab.update (class, axclass) axclasses,
   1.394 -          fold (fn (x, _) => add_param pp (x, class)) params parameters));
   1.395 +      |> map_axclasses (Symtab.update (class, axclass))
   1.396 +      |> map_params (fold (fn (x, _) => add_param pp (x, class)) params);
   1.397  
   1.398    in (class, result_thy) end;
   1.399