# HG changeset patch # User haftmann # Date 1233004459 -3600 # Node ID c3d576157244effffbc8001d14187f4e19921a6a # Parent 3aa049e5f15672582e5838969b8be17b963c9e0c fixed reading of class specs: declare class operations in context diff -r 3aa049e5f156 -r c3d576157244 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Mon Jan 26 22:14:18 2009 +0100 +++ b/src/Pure/Isar/class.ML Mon Jan 26 22:14:19 2009 +0100 @@ -91,20 +91,32 @@ in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; +val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) => + if v = Name.aT then T + else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification") + | T => T); + +fun singleton_fixate thy algebra Ts = + let + fun extract f = (fold o fold_atyps) f Ts []; + val tfrees = extract + (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I); + val inferred_sort = extract + (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I); + val fixate_sort = if null tfrees then inferred_sort + else let val a_sort = (snd o the_single) tfrees + in if Sorts.sort_le algebra (a_sort, inferred_sort) + then Sorts.inter_sort algebra (a_sort, inferred_sort) + else error ("Type inference imposes additional sort constraint " + ^ Syntax.string_of_sort_global thy inferred_sort + ^ " of type parameter " ^ Name.aT ^ " of sort " + ^ Syntax.string_of_sort_global thy a_sort) + end + 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)); -val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) => - if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort) - else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi) - (*FIXME does not occur*) - | T as TFree (v, sort) => - if v = Name.aT then T - else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")); - -val singleton_fixate = (map o map_atyps) (fn TVar (vi, sort) - => TFree (Name.aT, sort) | T => T); - fun add_tfrees_of_element (Element.Fixes fxs) = fold (fn (_, SOME T, _) => Term.add_tfreesT T | _ => I) fxs | add_tfrees_of_element (Element.Constrains cnstrs) = fold (Term.add_tfreesT o snd) cnstrs @@ -142,8 +154,9 @@ (these_operations thy sups); val ((_, _, inferred_elems), _) = ProofContext.init thy |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints - |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param - |> add_typ_check ~2 "singleton_fixate" singleton_fixate + |> 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)) |> prep_decl supexpr raw_elems; (*FIXME check for *all* side conditions here, extra check function for elements, less side-condition checks in check phase*) diff -r 3aa049e5f156 -r c3d576157244 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Mon Jan 26 22:14:18 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Mon Jan 26 22:14:19 2009 +0100 @@ -29,6 +29,7 @@ -> (string * mixfix) * term -> theory -> theory val class_prefix: string -> string val refresh_syntax: class -> Proof.context -> Proof.context + val redeclare_operations: theory -> sort -> Proof.context -> Proof.context (*instances*) val init_instantiation: string list * (string * sort) list * sort @@ -298,6 +299,10 @@ fun these_unchecks thy = map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy; +fun redeclare_const thy c = + let val b = Sign.base_name c + in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; + fun synchronize_class_syntax sort base_sort ctxt = let val thy = ProofContext.theory_of ctxt; @@ -308,9 +313,6 @@ (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 declare_const (c, _) = - let val b = Sign.base_name c - in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; 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) @@ -326,7 +328,7 @@ val unchecks = these_unchecks thy sort; in ctxt - |> fold declare_const primary_constraints + |> fold (redeclare_const thy o fst) primary_constraints |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints), (((improve, subst), true), unchecks)), false)) |> Overloading.set_primary_constraints @@ -338,6 +340,9 @@ val base_sort = base_sort thy class; in synchronize_class_syntax [class] base_sort ctxt end; +fun redeclare_operations thy sort = + fold (redeclare_const thy o fst) (these_operations thy sort); + fun begin sort base_sort ctxt = ctxt |> Variable.declare_term @@ -489,7 +494,8 @@ let val _ = if null tycos then error "At least one arity must be given" else (); val params = these_params thy sort; - fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco) + fun get_param tyco (param, (_, (c, ty))) = + if can (AxClass.param_of_inst thy) (c, tyco) then NONE else SOME ((c, tyco), (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); val inst_params = map_product get_param tycos params |> map_filter I;