# HG changeset patch # User wenzelm # Date 1202558172 -3600 # Node ID 8186c03194ed15c8651c1e0e493d8eb34303c262 # Parent f6f264ff2844f98303e1c2676a6956588fde5c7f overloading: reduced code redundancy, no xstrings here; diff -r f6f264ff2844 -r 8186c03194ed src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sat Feb 09 12:56:10 2008 +0100 +++ b/src/Pure/Isar/theory_target.ML Sat Feb 09 12:56:12 2008 +0100 @@ -15,7 +15,7 @@ val context: xstring -> theory -> local_theory val instantiation: string list * (string * sort) list * sort -> theory -> local_theory val overloading: (string * (string * typ) * bool) list -> theory -> local_theory - val overloading_cmd: ((xstring * xstring) * bool) list -> theory -> local_theory + val overloading_cmd: (string * string * bool) list -> theory -> local_theory end; structure TheoryTarget: THEORY_TARGET = @@ -53,7 +53,8 @@ val elems = (if null fixes then [] else [Element.Fixes fixes]) @ (if null assumes then [] else [Element.Assumes assumes]); - in if target = "" then [] + in + if target = "" then [] else if null elems then [Pretty.str target_name] else [Pretty.big_list (target_name ^ " =") (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)] @@ -63,8 +64,8 @@ Pretty.block [Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: (if not (null overloading) then [Overloading.pretty ctxt] - else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt] - else pretty_thy ctxt target is_locale is_class); + else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt] + else pretty_thy ctxt target is_locale is_class); (* target declarations *) @@ -211,15 +212,19 @@ val U = map #2 xs ---> T; val (mx1, mx2, mx3) = fork_mixfix ta mx; fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); - val declare_const = case Class.instantiation_param lthy c - of SOME c' => if mx3 <> NoSyn then syntax_error c' + val declare_const = + (case Class.instantiation_param lthy c of + SOME c' => + if mx3 <> NoSyn then syntax_error c' else LocalTheory.theory_result (AxClass.declare_overloaded (c', U)) ##> Class.confirm_declaration c - | NONE => (case Overloading.operation lthy c - of SOME (c', _) => if mx3 <> NoSyn then syntax_error c' - else LocalTheory.theory_result (Overloading.declare (c', U)) - ##> Overloading.confirm c - | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3))); + | NONE => + (case Overloading.operation lthy c of + SOME (c', _) => + if mx3 <> NoSyn then syntax_error c' + else LocalTheory.theory_result (Overloading.declare (c', U)) + ##> Overloading.confirm c + | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3)))); val (const, lthy') = lthy |> declare_const; val t = Term.list_comb (const, map Free xs); in @@ -281,12 +286,14 @@ val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def); (*def*) - val define_const = case Overloading.operation lthy c - of SOME (_, checked) => + val define_const = + (case Overloading.operation lthy c of + SOME (_, checked) => (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs)) - | NONE => if is_none (Class.instantiation_param lthy c) + | NONE => + if is_none (Class.instantiation_param lthy c) then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq)) - else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)); + else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs))); val (global_def, lthy3) = lthy2 |> LocalTheory.theory_result (define_const name' (lhs', rhs')); val def = LocalDefs.trans_terms lthy3 @@ -332,15 +339,11 @@ local fun init_target _ NONE = global_target - | init_target thy (SOME target) = make_target target true (Class.is_class thy target) - ([], [], []) []; - -fun init_instantiation arities = make_target "" false false arities []; - -fun init_overloading operations = make_target "" false false ([], [], []) operations; + | init_target thy (SOME target) = + make_target target true (Class.is_class thy target) ([], [], []) []; fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) = - if (not o null o #1) instantiation then Class.init_instantiation instantiation + if not (null (#1 instantiation)) then Class.init_instantiation instantiation else if not (null overloading) then Overloading.init overloading else if not is_locale then ProofContext.init else if not is_class then Locale.init target @@ -358,36 +361,31 @@ term_syntax = term_syntax ta, declaration = declaration ta, reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), - exit = (if (not o null o #1) instantiation then Class.conclude_instantiation - else if not (null overloading) then Overloading.conclude - else I) #> LocalTheory.target_of} + exit = LocalTheory.target_of o + (if not (null (#1 instantiation)) then Class.conclude_instantiation + else if not (null overloading) then Overloading.conclude + else I)} and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; +fun gen_overloading prep_const raw_ops thy = + let + val ctxt = ProofContext.init thy; + val ops = raw_ops |> map (fn (name, const, checked) => + (name, Term.dest_Const (prep_const ctxt const), checked)); + in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end; + in fun init target thy = init_lthy_ctxt (init_target thy target) thy; -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) - (SOME target)) ctxt; +fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt; fun context "-" thy = init NONE thy | context target thy = init (SOME (Locale.intern thy target)) thy; -val instantiation = init_lthy_ctxt o init_instantiation; +fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []); -fun gen_overloading prep_operation raw_operations thy = - let - val check_const = dest_Const o Syntax.check_term (ProofContext.init thy); - val operations = raw_operations - |> map (prep_operation thy) - |> map (fn (v, cTt, checked) => (v, check_const cTt, checked)); - in - thy - |> init_lthy_ctxt (init_overloading operations) - end; - -val overloading = gen_overloading (fn _ => fn (v, cT, checked) => (v, Const cT, checked)); -val overloading_cmd = gen_overloading (fn thy => fn ((v, raw_cT), checked) => - (v, Sign.read_term thy raw_cT, checked)); +val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); +val overloading_cmd = gen_overloading Syntax.read_term; end;