src/Pure/Isar/class.ML
changeset 32206 b2e93cda0be8
parent 32113 bafffa63ebfd
child 32713 b8381161adb1
     1.1 --- a/src/Pure/Isar/class.ML	Sat Jul 25 18:44:55 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Jul 25 18:44:55 2009 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  
     1.5  (* reading and processing class specifications *)
     1.6  
     1.7 -fun prep_class_elems prep_decl thy supexpr sups proto_base_sort raw_elems =
     1.8 +fun prep_class_elems prep_decl thy sups proto_base_sort raw_elems =
     1.9    let
    1.10  
    1.11      (* user space type system: only permits 'a type variable, improves towards 'a *)
    1.12 @@ -129,16 +129,19 @@
    1.13                    ^ Syntax.string_of_sort_global thy a_sort ^ ".")
    1.14              | _ => error "Multiple type variables in class specification.";
    1.15        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
    1.16 -    fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
    1.17 -      let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
    1.18 +    fun add_typ_check level name f = Context.proof_map
    1.19 +      (Syntax.add_typ_check level name (fn xs => fn ctxt =>
    1.20 +        let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
    1.21  
    1.22 -    (* preprocessing elements, retrieving base sort from type-checked elements *)
    1.23 +    (* preprocessing elements, retrieving base sort from typechecked elements *)
    1.24      val init_class_body = fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
    1.25        #> redeclare_operations thy sups
    1.26        #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
    1.27        #> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy));
    1.28 -    val ((_, _, inferred_elems), _) = ProofContext.init thy
    1.29 -      |> prep_decl supexpr init_class_body raw_elems;
    1.30 +    val raw_supexpr = (map (fn sup => (sup, (("", false),
    1.31 +      Expression.Positional []))) sups, []);
    1.32 +    val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy
    1.33 +      |> prep_decl raw_supexpr init_class_body raw_elems;
    1.34      fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs
    1.35        | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs
    1.36        | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) =>
    1.37 @@ -151,9 +154,16 @@
    1.38        case (fold o fold_element_types) Term.add_tfreesT inferred_elems []
    1.39         of [] => error "No type variable in class specification"
    1.40          | [(_, sort)] => sort
    1.41 -        | _ => error "Multiple type variables in class specification"
    1.42 +        | _ => error "Multiple type variables in class specification";
    1.43 +    val supparams = map (fn ((c, T), _) =>
    1.44 +      (c, map_atyps (K (TFree (Name.aT, base_sort))) T)) raw_supparams;
    1.45 +    val supparam_names = map fst supparams;
    1.46 +    fun mk_param ((c, _), _) = Free (c, (the o AList.lookup (op =) supparams) c);
    1.47 +    val supexpr = (map (fn sup => (sup, (("", false),
    1.48 +      Expression.Positional (map (SOME o mk_param) (Locale.params_of thy sup))))) sups,
    1.49 +        map (fn (c, T) => (Binding.name c, SOME T, NoSyn)) supparams);
    1.50  
    1.51 -  in (base_sort, inferred_elems) end;
    1.52 +  in (base_sort, supparam_names, supexpr, inferred_elems) end;
    1.53  
    1.54  val cert_class_elems = prep_class_elems Expression.cert_declaration;
    1.55  val read_class_elems = prep_class_elems Expression.cert_read_declaration;
    1.56 @@ -168,23 +178,21 @@
    1.57      val _ = case filter_out (is_class thy) sups
    1.58       of [] => ()
    1.59        | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
    1.60 -    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    1.61 -    val supparam_names = map fst supparams;
    1.62 -    val _ = if has_duplicates (op =) supparam_names
    1.63 +    val raw_supparams = (map o apsnd) (snd o snd) (these_params thy sups);
    1.64 +    val raw_supparam_names = map fst raw_supparams;
    1.65 +    val _ = if has_duplicates (op =) raw_supparam_names
    1.66        then error ("Duplicate parameter(s) in superclasses: "
    1.67 -        ^ (commas o map quote o duplicates (op =)) supparam_names)
    1.68 +        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
    1.69        else ();
    1.70 -    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
    1.71 -      sups, []);
    1.72      val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
    1.73  
    1.74      (* infer types and base sort *)
    1.75 -    val (base_sort, inferred_elems) = prep_class_elems thy supexpr sups
    1.76 -      given_basesort raw_elems;
    1.77 -    val sup_sort = inter_sort base_sort sups
    1.78 +    val (base_sort, supparam_names, supexpr, inferred_elems) =
    1.79 +      prep_class_elems thy sups given_basesort raw_elems;
    1.80 +    val sup_sort = inter_sort base_sort sups;
    1.81  
    1.82      (* process elements as class specification *)
    1.83 -    val class_ctxt = begin sups base_sort (ProofContext.init thy)
    1.84 +    val class_ctxt = begin sups base_sort (ProofContext.init thy);
    1.85      val ((_, _, syntax_elems), _) = class_ctxt
    1.86        |> Expression.cert_declaration supexpr I inferred_elems;
    1.87      fun check_vars e vs = if null vs
    1.88 @@ -204,11 +212,11 @@
    1.89        | fork_syn x = pair x;
    1.90      val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
    1.91      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    1.92 -      (K (TFree (Name.aT, base_sort))) supparams);
    1.93 +      (K (TFree (Name.aT, base_sort))) raw_supparams);
    1.94        (*FIXME perhaps better: control type variable by explicit
    1.95        parameter instantiation of import expression*)
    1.96  
    1.97 -  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
    1.98 +  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), ((*constrain :: *)elems, global_syntax)) end;
    1.99  
   1.100  val cert_class_spec = prep_class_spec (K I) cert_class_elems;
   1.101  val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
   1.102 @@ -216,14 +224,14 @@
   1.103  
   1.104  (* class establishment *)
   1.105  
   1.106 -fun add_consts class base_sort sups supparams global_syntax thy =
   1.107 +fun add_consts class base_sort sups supparam_names global_syntax thy =
   1.108    let
   1.109      (*FIXME simplify*)
   1.110 -    val supconsts = supparams
   1.111 +    val supconsts = supparam_names
   1.112        |> AList.make (snd o the o AList.lookup (op =) (these_params thy sups))
   1.113        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
   1.114      val all_params = Locale.params_of thy class;
   1.115 -    val raw_params = (snd o chop (length supparams)) all_params;
   1.116 +    val raw_params = (snd o chop (length supparam_names)) all_params;
   1.117      fun add_const ((raw_c, raw_ty), _) thy =
   1.118        let
   1.119          val b = Binding.name raw_c;
   1.120 @@ -246,7 +254,7 @@
   1.121      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   1.122    end;
   1.123  
   1.124 -fun adjungate_axclass bname class base_sort sups supsort supparams global_syntax thy =
   1.125 +fun adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax thy =
   1.126    let
   1.127      (*FIXME simplify*)
   1.128      fun globalize param_map = map_aterms
   1.129 @@ -260,7 +268,7 @@
   1.130        | [thm] => SOME thm;
   1.131    in
   1.132      thy
   1.133 -    |> add_consts class base_sort sups supparams global_syntax
   1.134 +    |> add_consts class base_sort sups supparam_names global_syntax
   1.135      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   1.136            (map (fst o snd) params)
   1.137            [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   1.138 @@ -270,16 +278,16 @@
   1.139      #> pair (param_map, params, assm_axiom)))
   1.140    end;
   1.141  
   1.142 -fun gen_class prep_spec bname raw_supclasses raw_elems thy =
   1.143 +fun gen_class prep_class_spec bname raw_supclasses raw_elems thy =
   1.144    let
   1.145      val class = Sign.full_name thy bname;
   1.146 -    val (((sups, supparams), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
   1.147 -      prep_spec thy raw_supclasses raw_elems;
   1.148 +    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
   1.149 +      prep_class_spec thy raw_supclasses raw_elems;
   1.150    in
   1.151      thy
   1.152      |> Expression.add_locale bname Binding.empty supexpr elems
   1.153      |> snd |> LocalTheory.exit_global
   1.154 -    |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
   1.155 +    |> adjungate_axclass bname class base_sort sups supsort supparam_names global_syntax
   1.156      ||> Theory.checkpoint
   1.157      |-> (fn (param_map, params, assm_axiom) =>
   1.158         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)