# HG changeset patch
# User haftmann
# Date 1248540295 -7200
# Node ID b2e93cda0be8de816a3074ecc8ca307a36d96023
# Parent  49db434c157fe4c7b0d1f2a4a0bd6b76b2b8db0c
improved handling of parameter import; tuned

diff -r 49db434c157f -r b2e93cda0be8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Jul 25 18:44:55 2009 +0200
+++ b/src/Pure/Isar/class.ML	Sat Jul 25 18:44:55 2009 +0200
@@ -101,7 +101,7 @@
 
 (* reading and processing class specifications *)
 
-fun prep_class_elems prep_decl thy supexpr sups proto_base_sort raw_elems =
+fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
   let
 
     (* user space type system: only permits 'a type variable, improves towards 'a *)
@@ -129,16 +129,19 @@
                   ^ Syntax.string_of_sort_global thy a_sort ^ ".")
             | _ => error "Multiple type variables in class specification.";
       in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
-    fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
-      let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
+    fun add_typ_check level name f = Context.proof_map
+      (Syntax.add_typ_check level name (fn xs => fn ctxt =>
+        let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
 
-    (* preprocessing elements, retrieving base sort from type-checked elements *)
+    (* preprocessing elements, retrieving base sort from typechecked elements *)
     val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
       #> redeclare_operations thy sups
       #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
       #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
-    val ((_, _, inferred_elems), _) = ProofContext.init thy
-      |> prep_decl supexpr init_class_body raw_elems;
+    val raw_supexpr = (map (fn sup => (sup, (("", false),
+      Expression.Positional []))) sups, []);
+    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
+      |> prep_decl raw_supexpr init_class_body raw_elems;
     fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
       | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
       | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
@@ -151,9 +154,16 @@
       case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
        of [] => error "No type variable in class specification"
         | [(_, sort)] => sort
-        | _ => error "Multiple type variables in class specification"
+        | _ => error "Multiple type variables in class specification";
+    val supparams = map (fn ((c, T), _) =>
+      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
+    val supparam_names = map fst supparams;
+    fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
+    val supexpr = (map (fn sup => (sup, (("", false),
+      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
+        map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
 
-  in (base_sort, inferred_elems) end;
+  in (base_sort, supparam_names, supexpr, inferred_elems) end;
 
 val cert_class_elems = prep_class_elems Expression.cert_declaration;
 val read_class_elems = prep_class_elems Expression.cert_read_declaration;
@@ -168,23 +178,21 @@
     val _ = case filter_out (is_class thy) sups
      of [] => ()
       | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
-    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
-    val supparam_names = map fst supparams;
-    val _ = if has_duplicates (op =) supparam_names
+    val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+    val raw_supparam_names = map fst raw_supparams;
+    val _ = if has_duplicates (op =) raw_supparam_names
       then error ("Duplicate parameter(s) in superclasses: "
-        ^ (commas o map quote o duplicates (op =)) supparam_names)
+        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
       else ();
-    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
-      sups, []);
     val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
 
     (* infer types and base sort *)
-    val (base_sort, inferred_elems) = prep_class_elems thy supexpr sups
-      given_basesort raw_elems;
-    val sup_sort = inter_sort base_sort sups
+    val (base_sort, supparam_names, supexpr, inferred_elems) =
+      prep_class_elems thy sups given_basesort raw_elems;
+    val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = begin sups base_sort (ProofContext.init thy)
+    val class_ctxt = begin sups base_sort (ProofContext.init thy);
     val ((_, _, syntax_elems), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
@@ -204,11 +212,11 @@
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
-      (K (TFree (Name.aT, base_sort))) supparams);
+      (K (TFree (Name.aT, base_sort))) raw_supparams);
       (*FIXME perhaps better: control type variable by explicit
       parameter instantiation of import expression*)
 
-  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
+  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), ((*constrain :: *)elems, global_syntax)) end;
 
 val cert_class_spec = prep_class_spec (K I) cert_class_elems;
 val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
@@ -216,14 +224,14 @@
 
 (* class establishment *)
 
-fun add_consts class base_sort sups supparams global_syntax thy =
+fun add_consts class base_sort sups supparam_names global_syntax thy =
   let
     (*FIXME simplify*)
-    val supconsts = supparams
+    val supconsts = supparam_names
       |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     val all_params = Locale.params_of thy class;
-    val raw_params = (snd o chop (length supparams)) all_params;
+    val raw_params = (snd o chop (length supparam_names)) all_params;
     fun add_const ((raw_c, raw_ty), _) thy =
       let
         val b = Binding.name raw_c;
@@ -246,7 +254,7 @@
     |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   end;
 
-fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
+fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
   let
     (*FIXME simplify*)
     fun globalize param_map = map_aterms
@@ -260,7 +268,7 @@
       | [thm] => SOME thm;
   in
     thy
-    |> add_consts class base_sort sups supparams global_syntax
+    |> add_consts class base_sort sups supparam_names global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
           [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
@@ -270,16 +278,16 @@
     #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_spec bname raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy bname;
-    val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
-      prep_spec thy raw_supclasses raw_elems;
+    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
+      prep_class_spec thy raw_supclasses raw_elems;
   in
     thy
     |> Expression.add_locale bname Binding.empty supexpr elems
     |> snd |> LocalTheory.exit_global
-    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
+    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
     ||> Theory.checkpoint
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)