--- a/src/Pure/Isar/class.ML Wed Aug 11 17:19:27 2010 +0200
+++ b/src/Pure/Isar/class.ML Wed Aug 11 17:59:32 2010 +0200
@@ -441,6 +441,19 @@
(((primary_constraints, []), (((improve, subst), false), unchecks)), false))
end;
+fun resort_terms pp algebra consts constraints ts =
+ let
+ fun matchings (Const (c_ty as (c, _))) = (case constraints c
+ of NONE => I
+ | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
+ (Consts.typargs consts c_ty) sorts)
+ | matchings _ = I
+ val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
+ handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
+ val inst = map_type_tvar
+ (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
+ in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
+
(* target *)
@@ -461,20 +474,39 @@
val type_name = sanitize_name o Long_Name.base_name;
-fun resort_terms pp algebra consts constraints ts =
+fun define_overloaded (c, U) v (b_def, rhs) = Local_Theory.theory_result
+ (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);
+
+fun pretty lthy =
let
- fun matchings (Const (c_ty as (c, _))) = (case constraints c
- of NONE => I
- | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
- (Consts.typargs consts c_ty) sorts)
- | matchings _ = I
- val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
- handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
- val inst = map_type_tvar
- (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
- in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
+ val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
+ val thy = ProofContext.theory_of lthy;
+ fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
+ fun pr_param ((c, _), (v, ty)) =
+ (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
+ (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
+ in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
-fun init_instantiation (tycos, vs, sort) thy =
+fun conclude lthy =
+ let
+ val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
+ val thy = ProofContext.theory_of lthy;
+ val _ = map (fn tyco => if Sign.of_sort thy
+ (Type (tyco, map TFree vs), sort)
+ then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
+ tycos;
+ in lthy end;
+
+fun instantiation (tycos, vs, sort) thy =
let
val _ = if null tycos then error "At least one arity must be given" else ();
val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
@@ -512,11 +544,20 @@
|> Overloading.add_improvable_syntax
|> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
|> synchronize_inst_syntax
+ |> Local_Theory.init NONE ""
+ {define = Generic_Target.define foundation,
+ notes = Generic_Target.notes
+ (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+ abbrev = Generic_Target.abbrev
+ (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+ declaration = K Generic_Target.theory_declaration,
+ syntax_declaration = K Generic_Target.theory_declaration,
+ pretty = pretty,
+ exit = Local_Theory.target_of o conclude}
end;
-fun confirm_declaration b = (map_instantiation o apsnd)
- (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
- #> Local_Theory.target synchronize_inst_syntax
+fun instantiation_cmd arities thy =
+ instantiation (read_multi_arity thy arities) thy;
fun gen_instantiation_instance do_proof after_qed lthy =
let
@@ -551,57 +592,6 @@
|> pair y
end;
-fun conclude_instantiation lthy =
- let
- val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
- val thy = ProofContext.theory_of lthy;
- val _ = map (fn tyco => if Sign.of_sort thy
- (Type (tyco, map TFree vs), sort)
- then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
- tycos;
- in lthy end;
-
-fun pretty_instantiation lthy =
- let
- val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
- val thy = ProofContext.theory_of lthy;
- fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
- fun pr_param ((c, _), (v, ty)) =
- (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
- (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
- in
- (Pretty.block o Pretty.fbreaks)
- (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
- end;
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
-fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case instantiation_param lthy b
- of SOME c => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
- ##>> AxClass.define_overloaded b_def (c, rhs))
- ||> confirm_declaration b
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun instantiation arities thy =
- thy
- |> init_instantiation arities
- |> Local_Theory.init NONE ""
- {define = Generic_Target.define instantiation_foundation,
- notes = Generic_Target.notes
- (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
- abbrev = Generic_Target.abbrev
- (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
- declaration = K Generic_Target.theory_declaration,
- syntax_declaration = K Generic_Target.theory_declaration,
- pretty = single o pretty_instantiation,
- exit = Local_Theory.target_of o conclude_instantiation};
-
-fun instantiation_cmd arities thy =
- instantiation (read_multi_arity thy arities) thy;
-
(* simplified instantiation interface with no class parameter *)
--- a/src/Pure/Isar/overloading.ML Wed Aug 11 17:19:27 2010 +0200
+++ b/src/Pure/Isar/overloading.ML Wed Aug 11 17:59:32 2010 +0200
@@ -113,27 +113,22 @@
(** overloading target **)
-(* bookkeeping *)
-
-structure OverloadingData = Proof_Data
+structure Data = Proof_Data
(
type T = ((string * typ) * (string * bool)) list;
fun init _ = [];
);
-val get_overloading = OverloadingData.get o Local_Theory.target_of;
-val map_overloading = Local_Theory.target o OverloadingData.map;
+val get_overloading = Data.get o Local_Theory.target_of;
+val map_overloading = Local_Theory.target o Data.map;
fun operation lthy b = get_overloading lthy
|> get_first (fn ((c, _), (v, checked)) =>
- if Binding.name_of b = v then SOME (c, checked) else NONE);
-
-
-(* target *)
+ if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
fun synchronize_syntax ctxt =
let
- val overloading = OverloadingData.get ctxt;
+ val overloading = Data.get ctxt;
fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty)
of SOME (v, _) => SOME (ty, Free (v, ty))
| NONE => NONE;
@@ -144,38 +139,20 @@
|> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
end
-fun init raw_overloading thy =
- let
- val _ = if null raw_overloading then error "At least one parameter must be given" else ();
- val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading;
- in
- thy
- |> Theory.checkpoint
- |> ProofContext.init_global
- |> OverloadingData.put overloading
- |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
- |> add_improvable_syntax
- |> synchronize_syntax
- end;
-
-fun declare c_ty = pair (Const c_ty);
+fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
+ Local_Theory.theory_result
+ (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+ ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
+ ##> Local_Theory.target synchronize_syntax
+ #-> (fn (_, def) => pair (Const (c, U), def))
-fun define checked b (c, t) =
- Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
- #>> snd;
-
-fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
- #> Local_Theory.target synchronize_syntax
-
-fun conclude lthy =
- let
- val overloading = get_overloading lthy;
- val _ = if null overloading then () else
- error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
- o Syntax.string_of_term lthy o Const o fst) overloading));
- in
- lthy
- end;
+fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+ case operation lthy b
+ of SOME (c, (v, checked)) => if mx <> NoSyn
+ then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
+ else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
+ | NONE => lthy |>
+ Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
fun pretty lthy =
let
@@ -184,32 +161,32 @@
fun pr_operation ((c, ty), (v, _)) =
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
- in
- (Pretty.block o Pretty.fbreaks)
- (Pretty.str "overloading" :: map pr_operation overloading)
- end;
-
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+ in Pretty.str "overloading" :: map pr_operation overloading end;
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
- case operation lthy b
- of SOME (c, checked) => if mx <> NoSyn then syntax_error c
- else lthy |> Local_Theory.theory_result (declare (c, U)
- ##>> define checked b_def (c, rhs))
- ||> confirm b
- | NONE => lthy |>
- Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+fun conclude lthy =
+ let
+ val overloading = get_overloading lthy;
+ val _ = if null overloading then () else
+ error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+ o Syntax.string_of_term lthy o Const o fst) overloading));
+ in lthy end;
-fun gen_overloading prep_const raw_ops thy =
+fun gen_overloading prep_const raw_overloading thy =
let
val ctxt = ProofContext.init_global thy;
- val ops = raw_ops |> map (fn (name, const, checked) =>
- (name, Term.dest_Const (prep_const ctxt const), checked));
+ val _ = if null raw_overloading then error "At least one parameter must be given" else ();
+ val overloading = raw_overloading |> map (fn (v, const, checked) =>
+ (Term.dest_Const (prep_const ctxt const), (v, checked)));
in
thy
- |> init ops
+ |> Theory.checkpoint
+ |> ProofContext.init_global
+ |> Data.put overloading
+ |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+ |> add_improvable_syntax
+ |> synchronize_syntax
|> Local_Theory.init NONE ""
- {define = Generic_Target.define overloading_foundation,
+ {define = Generic_Target.define foundation,
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
abbrev = Generic_Target.abbrev
@@ -217,7 +194,7 @@
Generic_Target.theory_abbrev prmode ((b, mx), t)),
declaration = K Generic_Target.theory_declaration,
syntax_declaration = K Generic_Target.theory_declaration,
- pretty = single o pretty,
+ pretty = pretty,
exit = Local_Theory.target_of o conclude}
end;