explicit accessed to structure Class_Target
authorhaftmann
Wed Aug 11 15:09:30 2010 +0200 (2010-08-11 ago)
changeset 38376dc67291d590b
parent 38375 43a765bc7ff0
child 38377 2dfd8b7b8274
explicit accessed to structure Class_Target
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Aug 11 14:54:10 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 11 15:09:30 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    val subclass_cmd: xstring -> local_theory -> Proof.state
     1.5  end;
     1.6  
     1.7 -structure Class : CLASS =
     1.8 +structure Class: CLASS =
     1.9  struct
    1.10  
    1.11  open Class_Target;
    1.12 @@ -55,7 +55,7 @@
    1.13      (* witness for canonical interpretation *)
    1.14      val prop = try the_single props;
    1.15      val wit = Option.map (fn prop => let
    1.16 -        val sup_axioms = map_filter (fst o rules thy) sups;
    1.17 +        val sup_axioms = map_filter (fst o Class_Target.rules thy) sups;
    1.18          val loc_intro_tac = case Locale.intros_of thy class
    1.19            of (_, NONE) => all_tac
    1.20             | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
    1.21 @@ -66,9 +66,9 @@
    1.22  
    1.23      (* canonical interpretation *)
    1.24      val base_morph = inst_morph
    1.25 -      $> Morphism.binding_morphism (Binding.prefix false (class_prefix class))
    1.26 +      $> Morphism.binding_morphism (Binding.prefix false (Class_Target.class_prefix class))
    1.27        $> Element.satisfy_morphism (the_list wit);
    1.28 -    val eq_morph = Element.eq_morphism thy (these_defs thy sups);
    1.29 +    val eq_morph = Element.eq_morphism thy (Class_Target.these_defs thy sups);
    1.30  
    1.31      (* assm_intro *)
    1.32      fun prove_assm_intro thm =
    1.33 @@ -88,7 +88,7 @@
    1.34      val of_class_prop = case prop of NONE => of_class_prop_concl
    1.35        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    1.36            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
    1.37 -    val sup_of_classes = map (snd o rules thy) sups;
    1.38 +    val sup_of_classes = map (snd o Class_Target.rules thy) sups;
    1.39      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    1.40      val axclass_intro = #intro (AxClass.get_info thy class);
    1.41      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    1.42 @@ -110,10 +110,10 @@
    1.43      val algebra = Sign.classes_of thy;
    1.44      val inter_sort = curry (Sorts.inter_sort algebra);
    1.45      val proto_base_sort = if null sups then Sign.defaultS thy
    1.46 -      else fold inter_sort (map (base_sort thy) sups) [];
    1.47 +      else fold inter_sort (map (Class_Target.base_sort thy) sups) [];
    1.48      val base_constraints = (map o apsnd)
    1.49        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
    1.50 -        (these_operations thy sups);
    1.51 +        (Class_Target.these_operations thy sups);
    1.52      val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
    1.53            if v = Name.aT then T
    1.54            else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.55 @@ -141,7 +141,7 @@
    1.56  
    1.57      (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.58      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.59 -      #> redeclare_operations thy sups
    1.60 +      #> Class_Target.redeclare_operations thy sups
    1.61        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.62        #> add_typ_check ~10 "singleton_fixate" singleton_fixate;
    1.63      val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.64 @@ -181,10 +181,10 @@
    1.65      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
    1.66      val sups = map (prep_class thy) raw_supclasses
    1.67        |> Sign.minimize_sort thy;
    1.68 -    val _ = case filter_out (is_class thy) sups
    1.69 +    val _ = case filter_out (Class_Target.is_class thy) sups
    1.70       of [] => ()
    1.71        | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
    1.72 -    val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    1.73 +    val raw_supparams = (map o apsnd) (snd o snd) (Class_Target.these_params thy sups);
    1.74      val raw_supparam_names = map fst raw_supparams;
    1.75      val _ = if has_duplicates (op =) raw_supparam_names
    1.76        then error ("Duplicate parameter(s) in superclasses: "
    1.77 @@ -197,7 +197,7 @@
    1.78      val sup_sort = inter_sort base_sort sups;
    1.79  
    1.80      (* process elements as class specification *)
    1.81 -    val class_ctxt = begin sups base_sort (ProofContext.init_global thy);
    1.82 +    val class_ctxt = Class_Target.begin sups base_sort (ProofContext.init_global thy);
    1.83      val ((_, _, syntax_elems), _) = class_ctxt
    1.84        |> Expression.cert_declaration supexpr I inferred_elems;
    1.85      fun check_vars e vs = if null vs
    1.86 @@ -229,7 +229,7 @@
    1.87    let
    1.88      (*FIXME simplify*)
    1.89      val supconsts = supparam_names
    1.90 -      |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
    1.91 +      |> AList.make (snd o the o AList.lookup (op =) (Class_Target.these_params thy sups))
    1.92        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
    1.93      val all_params = Locale.params_of thy class;
    1.94      val raw_params = (snd o chop (length supparam_names)) all_params;
    1.95 @@ -249,7 +249,7 @@
    1.96        end;
    1.97    in
    1.98      thy
    1.99 -    |> Sign.add_path (class_prefix class)
   1.100 +    |> Sign.add_path (Class_Target.class_prefix class)
   1.101      |> fold_map add_const raw_params
   1.102      ||> Sign.restore_naming thy
   1.103      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   1.104 @@ -295,7 +295,7 @@
   1.105      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
   1.106         Context.theory_map (Locale.add_registration (class, base_morph)
   1.107           (Option.map (rpair true) eq_morph) export_morph)
   1.108 -    #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
   1.109 +    #> Class_Target.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
   1.110      |> Named_Target.init (SOME class)
   1.111      |> pair class
   1.112    end;
   1.113 @@ -327,7 +327,7 @@
   1.114      val some_prop = try the_single props;
   1.115      val some_dep_morph = try the_single (map snd deps);
   1.116      fun after_qed some_wit =
   1.117 -      ProofContext.theory (register_subclass (sub, sup)
   1.118 +      ProofContext.theory (Class_Target.register_subclass (sub, sup)
   1.119          some_dep_morph some_wit export)
   1.120        #> ProofContext.theory_of #> Named_Target.init (SOME sub);
   1.121    in do_proof after_qed some_prop goal_ctxt end;