src/Pure/Isar/class_declaration.ML
changeset 45431 924c2f6dcd05
parent 45429 fd58cbf8cae3
child 45432 12cc89f1eb0c
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Nov 09 21:36:18 2011 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Nov 09 21:44:06 2011 +0100
     1.3 @@ -41,7 +41,8 @@
     1.4      val (([raw_props], [(_, raw_inst_morph)], export_morph), _) = empty_ctxt
     1.5        |> Expression.cert_goal_expression ([(class, (("", false),
     1.6             Expression.Named param_map_const))], []);
     1.7 -    val (props, inst_morph) = if null param_map
     1.8 +    val (props, inst_morph) =
     1.9 +      if null param_map
    1.10        then (raw_props |> map (Morphism.term typ_morph),
    1.11          raw_inst_morph $> typ_morph)
    1.12        else (raw_props, raw_inst_morph); (*FIXME proper handling in
    1.13 @@ -49,13 +50,15 @@
    1.14  
    1.15      (* witness for canonical interpretation *)
    1.16      val prop = try the_single props;
    1.17 -    val wit = Option.map (fn prop => let
    1.18 +    val wit = Option.map (fn prop =>
    1.19 +      let
    1.20          val sup_axioms = map_filter (fst o Class.rules thy) sups;
    1.21 -        val loc_intro_tac = case Locale.intros_of thy class
    1.22 -          of (_, NONE) => all_tac
    1.23 -           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
    1.24 +        val loc_intro_tac =
    1.25 +          (case Locale.intros_of thy class of
    1.26 +            (_, NONE) => all_tac
    1.27 +          | (_, SOME intro) => ALLGOALS (Tactic.rtac intro));
    1.28          val tac = loc_intro_tac
    1.29 -          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom))
    1.30 +          THEN ALLGOALS (Proof_Context.fact_tac (sup_axioms @ the_list assm_axiom));
    1.31        in Element.prove_witness empty_ctxt prop tac end) prop;
    1.32      val axiom = Option.map Element.conclude_witness wit;
    1.33  
    1.34 @@ -69,9 +72,10 @@
    1.35      fun prove_assm_intro thm =
    1.36        let
    1.37          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
    1.38 -        val const_eq_morph = case eq_morph
    1.39 -         of SOME eq_morph => const_morph $> eq_morph
    1.40 -          | NONE => const_morph
    1.41 +        val const_eq_morph =
    1.42 +          (case eq_morph of
    1.43 +             SOME eq_morph => const_morph $> eq_morph
    1.44 +          | NONE => const_morph);
    1.45          val thm'' = Morphism.thm const_eq_morph thm';
    1.46          val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
    1.47        in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    1.48 @@ -80,17 +84,19 @@
    1.49  
    1.50      (* of_class *)
    1.51      val of_class_prop_concl = Logic.mk_of_class (aT, class);
    1.52 -    val of_class_prop = case prop of NONE => of_class_prop_concl
    1.53 +    val of_class_prop =
    1.54 +      (case prop of
    1.55 +        NONE => of_class_prop_concl
    1.56        | SOME prop => Logic.mk_implies (Morphism.term const_morph
    1.57 -          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
    1.58 +          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
    1.59      val sup_of_classes = map (snd o Class.rules thy) sups;
    1.60      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    1.61      val axclass_intro = #intro (AxClass.get_info thy class);
    1.62      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
    1.63 -    val tac = REPEAT (SOMEGOAL
    1.64 -      (Tactic.match_tac (axclass_intro :: sup_of_classes
    1.65 -         @ loc_axiom_intros @ base_sort_trivs)
    1.66 -           ORELSE' Tactic.assume_tac));
    1.67 +    val tac =
    1.68 +      REPEAT (SOMEGOAL
    1.69 +        (Tactic.match_tac (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
    1.70 +          ORELSE' Tactic.assume_tac));
    1.71      val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
    1.72  
    1.73    in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
    1.74 @@ -110,8 +116,8 @@
    1.75      val base_constraints = (map o apsnd)
    1.76        (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o snd)
    1.77          (Class.these_operations thy sups);
    1.78 -    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
    1.79 -          if v = Name.aT then T
    1.80 +    val reject_bcd_etc = (map o map_atyps) (fn T as TFree (a, _) =>
    1.81 +          if a = Name.aT then T
    1.82            else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
    1.83        | T => T);
    1.84      fun singleton_fixate Ts =
    1.85 @@ -123,22 +129,26 @@
    1.86            if null tfrees then inferred_sort
    1.87            else
    1.88              (case tfrees of
    1.89 -              [(_, a_sort)] => if Sorts.sort_le algebra (a_sort, inferred_sort)
    1.90 -                then inter_sort a_sort inferred_sort
    1.91 -                else error ("Type inference imposes additional sort constraint "
    1.92 -                  ^ Syntax.string_of_sort_global thy inferred_sort
    1.93 -                  ^ " of type parameter " ^ Name.aT ^ " of sort "
    1.94 -                  ^ Syntax.string_of_sort_global thy a_sort)
    1.95 +              [(_, a_sort)] =>
    1.96 +                if Sorts.sort_le algebra (a_sort, inferred_sort) then
    1.97 +                  inter_sort a_sort inferred_sort
    1.98 +                else
    1.99 +                  error ("Type inference imposes additional sort constraint " ^
   1.100 +                    Syntax.string_of_sort_global thy inferred_sort ^
   1.101 +                    " of type parameter " ^ Name.aT ^ " of sort " ^
   1.102 +                    Syntax.string_of_sort_global thy a_sort)
   1.103              | _ => error "Multiple type variables in class specification");
   1.104        in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
   1.105      fun after_infer_fixate Ts =
   1.106        let
   1.107 -        val sort' = (fold o fold_atyps) (fn T as TFree _ => I | T as TVar (vi, sort) =>
   1.108 -          if Type_Infer.is_param vi then inter_sort sort else I) Ts [];
   1.109 +        val S' =
   1.110 +          (fold o fold_atyps)
   1.111 +            (fn TVar (xi, S) => if Type_Infer.is_param xi then inter_sort S else I | _ => I) Ts [];
   1.112        in
   1.113          (map o map_atyps)
   1.114 -          (fn T as TFree _ => T | T as TVar (vi, _) =>
   1.115 -            if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts
   1.116 +          (fn T as TVar (xi, _) =>
   1.117 +              if Type_Infer.is_param xi then Type_Infer.param 0 (Name.aT, S') else T
   1.118 +            | T => T) Ts
   1.119        end;
   1.120  
   1.121      (* preprocessing elements, retrieving base sort from type-checked elements *)
   1.122 @@ -193,38 +203,39 @@
   1.123  
   1.124      (* prepare import *)
   1.125      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
   1.126 -    val sups = map (prep_class thy) raw_supclasses
   1.127 -      |> Sign.minimize_sort thy;
   1.128 -    val _ = case filter_out (Class.is_class thy) sups
   1.129 -     of [] => ()
   1.130 -      | no_classes => error ("No (proper) classes: " ^ commas (map quote no_classes));
   1.131 +    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
   1.132 +    val _ =
   1.133 +      (case filter_out (Class.is_class thy) sups of
   1.134 +        [] => ()
   1.135 +      | no_classes => error ("No (proper) classes: " ^ commas_quote no_classes));
   1.136      val raw_supparams = (map o apsnd) (snd o snd) (Class.these_params thy sups);
   1.137      val raw_supparam_names = map fst raw_supparams;
   1.138 -    val _ = if has_duplicates (op =) raw_supparam_names
   1.139 -      then error ("Duplicate parameter(s) in superclasses: "
   1.140 -        ^ (commas o map quote o duplicates (op =)) raw_supparam_names)
   1.141 +    val _ =
   1.142 +      if has_duplicates (op =) raw_supparam_names then
   1.143 +        error ("Duplicate parameter(s) in superclasses: " ^
   1.144 +          (commas_quote (duplicates (op =) raw_supparam_names)))
   1.145        else ();
   1.146  
   1.147      (* infer types and base sort *)
   1.148 -    val (base_sort, supparam_names, supexpr, inferred_elems) =
   1.149 -      prep_class_elems thy sups raw_elems;
   1.150 +    val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems;
   1.151      val sup_sort = inter_sort base_sort sups;
   1.152  
   1.153      (* process elements as class specification *)
   1.154      val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
   1.155      val ((_, _, syntax_elems), _) = class_ctxt
   1.156        |> Expression.cert_declaration supexpr I inferred_elems;
   1.157 -    fun check_vars e vs = if null vs
   1.158 -      then error ("No type variable in part of specification element "
   1.159 -        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
   1.160 +    fun check_vars e vs =
   1.161 +      if null vs then
   1.162 +        error ("No type variable in part of specification element " ^
   1.163 +          Pretty.string_of (Pretty.chunks (Element.pretty_ctxt class_ctxt e)))
   1.164        else ();
   1.165      fun check_element (e as Element.Fixes fxs) =
   1.166 -          map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
   1.167 +          List.app (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
   1.168        | check_element (e as Element.Assumes assms) =
   1.169 -          maps (fn (_, ts_pss) => map
   1.170 -            (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
   1.171 -      | check_element e = [()];
   1.172 -    val _ = map check_element syntax_elems;
   1.173 +          List.app (fn (_, ts_pss) =>
   1.174 +            List.app (fn (t, _) => check_vars e (Term.add_tfrees t [])) ts_pss) assms
   1.175 +      | check_element _ = ();
   1.176 +    val _ = List.app check_element syntax_elems;
   1.177      fun fork_syn (Element.Fixes xs) =
   1.178            fold_map (fn (c, ty, syn) => cons (c, syn) #> pair (c, ty, NoSyn)) xs
   1.179            #>> Element.Fixes
   1.180 @@ -278,9 +289,10 @@
   1.181      val raw_pred = Locale.intros_of thy class
   1.182        |> fst
   1.183        |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
   1.184 -    fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
   1.185 -     of [] => NONE
   1.186 -      | [thm] => SOME thm;
   1.187 +    fun get_axiom thy =
   1.188 +      (case #axioms (AxClass.get_info thy class) of
   1.189 +         [] => NONE
   1.190 +      | [thm] => SOME thm);
   1.191    in
   1.192      thy
   1.193      |> add_consts class base_sort sups supparam_names global_syntax
   1.194 @@ -331,9 +343,10 @@
   1.195    let
   1.196      val thy = Proof_Context.theory_of lthy;
   1.197      val proto_sup = prep_class thy raw_sup;
   1.198 -    val proto_sub = case Named_Target.peek lthy
   1.199 -     of SOME {target, is_class = true, ...} => target
   1.200 -      | _ => error "Not in a class target";
   1.201 +    val proto_sub =
   1.202 +      (case Named_Target.peek lthy of
   1.203 +         SOME {target, is_class = true, ...} => target
   1.204 +      | _ => error "Not in a class target");
   1.205      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   1.206  
   1.207      val expr = ([(sup, (("", false), Expression.Positional []))], []);