overloading: reduced code redundancy, no xstrings here;
authorwenzelm
Sat Feb 09 12:56:12 2008 +0100 (2008-02-09)
changeset 260498186c03194ed
parent 26048 f6f264ff2844
child 26050 88bb26089ef5
overloading: reduced code redundancy, no xstrings here;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Feb 09 12:56:10 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Feb 09 12:56:12 2008 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val context: xstring -> theory -> local_theory
     1.5    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     1.6    val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     1.7 -  val overloading_cmd: ((xstring * xstring) * bool) list -> theory -> local_theory
     1.8 +  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
     1.9  end;
    1.10  
    1.11  structure TheoryTarget: THEORY_TARGET =
    1.12 @@ -53,7 +53,8 @@
    1.13      val elems =
    1.14        (if null fixes then [] else [Element.Fixes fixes]) @
    1.15        (if null assumes then [] else [Element.Assumes assumes]);
    1.16 -  in if target = "" then []
    1.17 +  in
    1.18 +    if target = "" then []
    1.19      else if null elems then [Pretty.str target_name]
    1.20      else [Pretty.big_list (target_name ^ " =")
    1.21        (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)]
    1.22 @@ -63,8 +64,8 @@
    1.23    Pretty.block [Pretty.str "theory", Pretty.brk 1,
    1.24        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    1.25      (if not (null overloading) then [Overloading.pretty ctxt]
    1.26 -    else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt]
    1.27 -    else pretty_thy ctxt target is_locale is_class);
    1.28 +     else if not (null (#1 instantiation)) then [Class.pretty_instantiation ctxt]
    1.29 +     else pretty_thy ctxt target is_locale is_class);
    1.30  
    1.31  
    1.32  (* target declarations *)
    1.33 @@ -211,15 +212,19 @@
    1.34      val U = map #2 xs ---> T;
    1.35      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.36      fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    1.37 -    val declare_const = case Class.instantiation_param lthy c
    1.38 -       of SOME c' => if mx3 <> NoSyn then syntax_error c'
    1.39 +    val declare_const =
    1.40 +      (case Class.instantiation_param lthy c of
    1.41 +        SOME c' =>
    1.42 +          if mx3 <> NoSyn then syntax_error c'
    1.43            else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
    1.44              ##> Class.confirm_declaration c
    1.45 -        | NONE => (case Overloading.operation lthy c
    1.46 -           of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
    1.47 -              else LocalTheory.theory_result (Overloading.declare (c', U))
    1.48 -                ##> Overloading.confirm c
    1.49 -            | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3)));
    1.50 +        | NONE =>
    1.51 +            (case Overloading.operation lthy c of
    1.52 +              SOME (c', _) =>
    1.53 +                if mx3 <> NoSyn then syntax_error c'
    1.54 +                else LocalTheory.theory_result (Overloading.declare (c', U))
    1.55 +                  ##> Overloading.confirm c
    1.56 +            | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3))));
    1.57      val (const, lthy') = lthy |> declare_const;
    1.58      val t = Term.list_comb (const, map Free xs);
    1.59    in
    1.60 @@ -281,12 +286,14 @@
    1.61      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.62  
    1.63      (*def*)
    1.64 -    val define_const = case Overloading.operation lthy c
    1.65 -     of SOME (_, checked) =>
    1.66 +    val define_const =
    1.67 +      (case Overloading.operation lthy c of
    1.68 +        SOME (_, checked) =>
    1.69            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    1.70 -      | NONE => if is_none (Class.instantiation_param lthy c)
    1.71 +      | NONE =>
    1.72 +          if is_none (Class.instantiation_param lthy c)
    1.73            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    1.74 -          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs));
    1.75 +          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
    1.76      val (global_def, lthy3) = lthy2
    1.77        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    1.78      val def = LocalDefs.trans_terms lthy3
    1.79 @@ -332,15 +339,11 @@
    1.80  local
    1.81  
    1.82  fun init_target _ NONE = global_target
    1.83 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target)
    1.84 -      ([], [], []) [];
    1.85 -
    1.86 -fun init_instantiation arities = make_target "" false false arities [];
    1.87 -
    1.88 -fun init_overloading operations = make_target "" false false ([], [], []) operations;
    1.89 +  | init_target thy (SOME target) =
    1.90 +      make_target target true (Class.is_class thy target) ([], [], []) [];
    1.91  
    1.92  fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    1.93 -  if (not o null o #1) instantiation then Class.init_instantiation instantiation
    1.94 +  if not (null (#1 instantiation)) then Class.init_instantiation instantiation
    1.95    else if not (null overloading) then Overloading.init overloading
    1.96    else if not is_locale then ProofContext.init
    1.97    else if not is_class then Locale.init target
    1.98 @@ -358,36 +361,31 @@
    1.99      term_syntax = term_syntax ta,
   1.100      declaration = declaration ta,
   1.101      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
   1.102 -    exit = (if (not o null o #1) instantiation then Class.conclude_instantiation
   1.103 -      else if not (null overloading) then Overloading.conclude
   1.104 -      else I) #> LocalTheory.target_of}
   1.105 +    exit = LocalTheory.target_of o
   1.106 +      (if not (null (#1 instantiation)) then Class.conclude_instantiation
   1.107 +       else if not (null overloading) then Overloading.conclude
   1.108 +       else I)}
   1.109  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
   1.110  
   1.111 +fun gen_overloading prep_const raw_ops thy =
   1.112 +  let
   1.113 +    val ctxt = ProofContext.init thy;
   1.114 +    val ops = raw_ops |> map (fn (name, const, checked) =>
   1.115 +      (name, Term.dest_Const (prep_const ctxt const), checked));
   1.116 +  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
   1.117 +
   1.118  in
   1.119  
   1.120  fun init target thy = init_lthy_ctxt (init_target thy target) thy;
   1.121 -fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt)
   1.122 -  (SOME target)) ctxt;
   1.123 +fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
   1.124  
   1.125  fun context "-" thy = init NONE thy
   1.126    | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.127  
   1.128 -val instantiation = init_lthy_ctxt o init_instantiation;
   1.129 +fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
   1.130  
   1.131 -fun gen_overloading prep_operation raw_operations thy =
   1.132 -  let
   1.133 -    val check_const = dest_Const o Syntax.check_term (ProofContext.init thy);
   1.134 -    val operations = raw_operations
   1.135 -      |> map (prep_operation thy)
   1.136 -      |> map (fn (v, cTt, checked) => (v, check_const cTt, checked));
   1.137 -  in
   1.138 -    thy
   1.139 -    |> init_lthy_ctxt (init_overloading operations)
   1.140 -  end;
   1.141 -
   1.142 -val overloading = gen_overloading (fn _ => fn (v, cT, checked) => (v, Const cT, checked));
   1.143 -val overloading_cmd = gen_overloading (fn thy => fn ((v, raw_cT), checked) =>
   1.144 -  (v, Sign.read_term thy raw_cT, checked));
   1.145 +val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   1.146 +val overloading_cmd = gen_overloading Syntax.read_term;
   1.147  
   1.148  end;
   1.149