src/Pure/Isar/class.ML

 structure Class: CLASS =
 struct
 
 (** class data **)
 
-datatype class_data = ClassData of {
+datatype class_data = Class_Data of {
 
   (* static part *)
   consts: (string * string) list
     (*locale parameter ~> constant name*),
   base_sort: sort,

 
 };
 
 fun make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)) =
-  ClassData { consts = consts, base_sort = base_sort,
+  Class_Data {consts = consts, base_sort = base_sort,
     base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
-    of_class = of_class, axiom = axiom, defs = defs, operations = operations };
-fun map_class_data f (ClassData { consts, base_sort, base_morph, export_morph, assm_intro,
-    of_class, axiom, defs, operations }) =
+    of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
+    of_class, axiom, defs, operations}) =
   make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)));
-fun merge_class_data _ (ClassData { consts = consts,
+fun merge_class_data _ (Class_Data {consts = consts,
     base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
-    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1 },
-  ClassData { consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
-    of_class = _, axiom = _, defs = defs2, operations = operations2 }) =
+    of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},
+  Class_Data {consts = _, base_sort = _, base_morph = _, export_morph = _, assm_intro = _,
+    of_class = _, axiom = _, defs = defs2, operations = operations2}) =
   make_class_data ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
-structure ClassData = Theory_Data
+structure Class_Data = Theory_Data
 (
   type T = class_data Graph.T
   val empty = Graph.empty;
   val extend = I;
   val merge = Graph.join merge_class_data;
 );
 
 
 (* queries *)
 
-fun lookup_class_data thy class = case try (Graph.get_node (ClassData.get thy)) class
- of SOME (ClassData data) => SOME data
-  | NONE => NONE;
-
-fun the_class_data thy class = case lookup_class_data thy class
- of NONE => error ("Undeclared class " ^ quote class)
-  | SOME data => data;
+fun lookup_class_data thy class =
+  (case try (Graph.get_node (Class_Data.get thy)) class of
+    SOME (Class_Data data) => SOME data
+  | NONE => NONE);
+
+fun the_class_data thy class =
+  (case lookup_class_data thy class of
+    NONE => error ("Undeclared class " ^ quote class)
+  | SOME data => data);
 
 val is_class = is_some oo lookup_class_data;
 
-val ancestry = Graph.all_succs o ClassData.get;
-val heritage = Graph.all_preds o ClassData.get;
+val ancestry = Graph.all_succs o Class_Data.get;
+val heritage = Graph.all_preds o Class_Data.get;
 
 fun these_params thy =
   let
     fun params class =
       let

   in maps params o ancestry thy end;
 
 val base_sort = #base_sort oo the_class_data;
 
 fun rules thy class =
-  let val { axiom, of_class, ... } = the_class_data thy class
+  let val {axiom, of_class, ...} = the_class_data thy class
   in (axiom, of_class) end;
 
 fun all_assm_intros thy =
-  Graph.fold (fn (_, (ClassData { assm_intro, ... }, _)) => fold (insert Thm.eq_thm)
-    (the_list assm_intro)) (ClassData.get thy) [];
+  Graph.fold (fn (_, (Class_Data {assm_intro, ...}, _)) => fold (insert Thm.eq_thm)
+    (the_list assm_intro)) (Class_Data.get thy) [];
 
 fun these_defs thy = maps (#defs o the_class_data thy) o ancestry thy;
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
 val base_morphism = #base_morph oo the_class_data;
-fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
- of SOME eq_morph => base_morphism thy class $> eq_morph
-  | NONE => base_morphism thy class;
+fun morphism thy class =
+  (case Element.eq_morphism thy (these_defs thy [class]) of
+    SOME eq_morph => base_morphism thy class $> eq_morph
+  | NONE => base_morphism thy class);
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;

       (c, (class, (ty, Free v_ty)))) params;
     val add_class = Graph.new_node (class,
         make_class_data (((map o pairself) fst params, base_sort,
           base_morph, export_morph, assm_intro, of_class, axiom), ([], operations)))
       #> fold (curry Graph.add_edge class) sups;
-  in ClassData.map add_class thy end;
-
-fun activate_defs class thms thy = case Element.eq_morphism thy thms
- of SOME eq_morph => fold (fn cls => fn thy =>
+  in Class_Data.map add_class thy end;
+
+fun activate_defs class thms thy =
+  (case Element.eq_morphism thy thms of
+    SOME eq_morph => fold (fn cls => fn thy =>
       Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
         (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
-  | NONE => thy;
+  | NONE => thy);
 
 fun register_operation class (c, (t, some_def)) thy =
   let
     val base_sort = base_sort thy class;
     val prep_typ = map_type_tfree

         then TFree (v, base_sort) else TVar ((v, 0), sort));
     val t' = map_types prep_typ t;
     val ty' = Term.fastype_of t';
   in
     thy
-    |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
+    |> (Class_Data.map o Graph.map_node class o map_class_data o apsnd)
       (fn (defs, operations) =>
         (fold cons (the_list some_def) defs,
           (c, (class, (ty', t'))) :: operations))
     |> activate_defs class (the_list some_def)
   end;

     val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
       (K tac);
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
       |> filter (is_class thy);
-    val add_dependency = case some_dep_morph
-     of SOME dep_morph => Locale.add_dependency sub
+    val add_dependency =
+      (case some_dep_morph of
+        SOME dep_morph => Locale.add_dependency sub
           (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) NONE export
-      | NONE => I
+      | NONE => I);
   in
     thy
     |> AxClass.add_classrel classrel
-    |> ClassData.map (Graph.add_edge (sub, sup))
+    |> Class_Data.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
     |> add_dependency
   end;
 
 

     fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
     val primary_constraints =
       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
     val secondary_constraints =
       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
-    fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
-     of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
-         of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
-             of SOME (_, ty' as TVar (vi, sort)) =>
-                  if Type_Infer.is_param vi
-                    andalso Sorts.sort_le algebra (base_sort, sort)
-                      then SOME (ty', TFree (Name.aT, base_sort))
-                      else NONE
+    fun improve (c, ty) =
+      (case AList.lookup (op =) primary_constraints c of
+        SOME ty' =>
+          (case try (Type.raw_match (ty', ty)) Vartab.empty of
+            SOME tyenv =>
+              (case Vartab.lookup tyenv (Name.aT, 0) of
+                SOME (_, ty' as TVar (vi, sort)) =>
+                  if Type_Infer.is_param vi andalso Sorts.sort_le algebra (base_sort, sort)
+                  then SOME (ty', TFree (Name.aT, base_sort))
+                  else NONE
               | _ => NONE)
           | NONE => NONE)
-      | NONE => NONE)
+      | NONE => NONE);
     fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
     val unchecks = these_unchecks thy sort;
   in
     ctxt
     |> fold (redeclare_const thy o fst) primary_constraints

     (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
 }
 
 structure Instantiation = Proof_Data
 (
-  type T = instantiation
-  fun init _ = Instantiation { arities = ([], [], []), params = [] };
+  type T = instantiation;
+  fun init _ = Instantiation {arities = ([], [], []), params = []};
 );
 
 fun mk_instantiation (arities, params) =
-  Instantiation { arities = arities, params = params };
-fun get_instantiation lthy = case Instantiation.get (Local_Theory.target_of lthy)
- of Instantiation data => data;
-fun map_instantiation f = (Local_Theory.target o Instantiation.map)
-  (fn Instantiation { arities, params } => mk_instantiation (f (arities, params)));
-
-fun the_instantiation lthy = case get_instantiation lthy
- of { arities = ([], [], []), ... } => error "No instantiation target"
-  | data => data;
+  Instantiation {arities = arities, params = params};
+
+val get_instantiation =
+  (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of;
+
+fun map_instantiation f =
+  (Local_Theory.target o Instantiation.map)
+    (fn Instantiation {arities, params} => mk_instantiation (f (arities, params)));
+
+fun the_instantiation lthy =
+  (case get_instantiation lthy of
+    {arities = ([], [], []), ...} => error "No instantiation target"
+  | data => data);
 
 val instantiation_params = #params o get_instantiation;
 
 fun instantiation_param lthy b = instantiation_params lthy
   |> find_first (fn (_, (v, _)) => Binding.name_of b = v)

 
 (* syntax *)
 
 fun synchronize_inst_syntax ctxt =
   let
-    val Instantiation { params, ... } = Instantiation.get ctxt;
+    val Instantiation {params, ...} = Instantiation.get ctxt;
 
     val lookup_inst_param = AxClass.lookup_inst_param
       (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
-    fun subst (c, ty) = case lookup_inst_param (c, ty)
-     of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
-      | NONE => NONE;
+    fun subst (c, ty) =
+      (case lookup_inst_param (c, ty) of
+        SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
+      | NONE => NONE);
     val unchecks =
       map (fn ((c, _), v_ty as (_, ty)) => (Free v_ty, Const (c, ty))) params;
   in
     ctxt
     |> Overloading.map_improvable_syntax
-         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
-            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
+      (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
+          (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   end;
 
 fun resort_terms ctxt algebra consts constraints ts =
   let
     fun matchings (Const (c_ty as (c, _))) =

     (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))
   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_inst_syntax;
 
 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case instantiation_param lthy b
-   of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
-        else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+  (case instantiation_param lthy b of
+    SOME c =>
+      if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+      else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
+  | NONE => lthy |>
+      Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
 
 fun pretty lthy =
   let
-    val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
+    val {arities = (tycos, vs, sort), params} = the_instantiation lthy;
     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
     fun pr_param ((c, _), (v, ty)) =
       Pretty.block (Pretty.breaks
         [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
           Pretty.str "::", Syntax.pretty_typ lthy ty]);

 fun conclude lthy =
   let
     val (tycos, vs, sort) = #arities (the_instantiation lthy);
     val thy = Proof_Context.theory_of lthy;
     val _ = tycos |> List.app (fn tyco =>
-      if Sign.of_sort thy
-        (Type (tyco, map TFree vs), sort)
-      then ()
+      if Sign.of_sort thy (Type (tyco, map TFree vs), sort) then ()
       else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
   in lthy end;
 
 fun instantiation (tycos, vs, sort) thy =
   let