src/Pure/Isar/theory_target.ML
changeset 25519 8570745cb40b
parent 25514 4b508bb31a6c
child 25542 ced4104f6c1f
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 03 16:04:16 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 03 16:04:17 2007 +0100
     1.3 @@ -8,11 +8,14 @@
     1.4  signature THEORY_TARGET =
     1.5  sig
     1.6    val peek: local_theory -> {target: string, is_locale: bool,
     1.7 -    is_class: bool, instantiation: arity list}
     1.8 +    is_class: bool, instantiation: arity list,
     1.9 +    overloading: ((string * typ) * (string * bool)) list}
    1.10    val init: string option -> theory -> local_theory
    1.11    val begin: string -> Proof.context -> local_theory
    1.12    val context: xstring -> theory -> local_theory
    1.13    val instantiation: arity list -> theory -> local_theory
    1.14 +  val overloading: ((string * typ) * (string * bool)) list -> theory -> local_theory
    1.15 +  val overloading_cmd: (((xstring * xstring) * string) * bool) list -> theory -> local_theory
    1.16  end;
    1.17  
    1.18  structure TheoryTarget: THEORY_TARGET =
    1.19 @@ -21,13 +24,13 @@
    1.20  (* context data *)
    1.21  
    1.22  datatype target = Target of {target: string, is_locale: bool,
    1.23 -  is_class: bool, instantiation: arity list};
    1.24 +  is_class: bool, instantiation: arity list, overloading: ((string * typ) * (string * bool)) list};
    1.25  
    1.26 -fun make_target target is_locale is_class instantiation =
    1.27 +fun make_target target is_locale is_class instantiation overloading =
    1.28    Target {target = target, is_locale = is_locale,
    1.29 -    is_class = is_class, instantiation = instantiation};
    1.30 +    is_class = is_class, instantiation = instantiation, overloading = overloading};
    1.31  
    1.32 -val global_target = make_target "" false false [];
    1.33 +val global_target = make_target "" false false [] [];
    1.34  
    1.35  structure Data = ProofDataFun
    1.36  (
    1.37 @@ -40,7 +43,7 @@
    1.38  
    1.39  (* pretty *)
    1.40  
    1.41 -fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
    1.42 +fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
    1.43    let
    1.44      val thy = ProofContext.theory_of ctxt;
    1.45      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.46 @@ -196,10 +199,16 @@
    1.47      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.48      val U = map #2 xs ---> T;
    1.49      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.50 +    fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    1.51      val declare_const = case Class.instantiation_param lthy c
    1.52 -       of SOME c' => LocalTheory.theory_result (Class.overloaded_const (c', U, mx3))
    1.53 +       of SOME c' => if mx3 <> NoSyn then syntax_error c'
    1.54 +          else LocalTheory.theory_result (Class.overloaded_const (c', U))
    1.55              ##> Class.confirm_declaration c
    1.56 -        | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    1.57 +        | NONE => (case Overloading.operation lthy c
    1.58 +           of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
    1.59 +              else LocalTheory.theory_result (Overloading.declare (c', U))
    1.60 +                ##> Overloading.confirm c
    1.61 +            | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3)));
    1.62      val (const, lthy') = lthy |> declare_const;
    1.63      val t = Term.list_comb (const, map Free xs);
    1.64    in
    1.65 @@ -261,9 +270,12 @@
    1.66      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    1.67  
    1.68      (*def*)
    1.69 -    val define_const = if is_none (Class.instantiation_param lthy c)
    1.70 -      then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    1.71 -      else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    1.72 +    val define_const = case Overloading.operation lthy c
    1.73 +     of SOME (_, checked) =>
    1.74 +          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    1.75 +      | NONE => if is_none (Class.instantiation_param lthy c)
    1.76 +          then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    1.77 +          else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    1.78      val (global_def, lthy3) = lthy2
    1.79        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    1.80      val def = LocalDefs.trans_terms lthy3
    1.81 @@ -309,12 +321,15 @@
    1.82  local
    1.83  
    1.84  fun init_target _ NONE = global_target
    1.85 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
    1.86 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [] [];
    1.87 +
    1.88 +fun init_instantiation arities = make_target "" false false arities [];
    1.89  
    1.90 -fun init_instantiaton arities = make_target "" false false arities
    1.91 +fun init_overloading operations = make_target "" false false [] operations;
    1.92  
    1.93 -fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
    1.94 +fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    1.95    if not (null instantiation) then Class.init_instantiation instantiation
    1.96 +  else if not (null overloading) then Overloading.init overloading
    1.97    else if not is_locale then ProofContext.init
    1.98    else if not is_class then Locale.init target
    1.99    else Class.init target;
   1.100 @@ -343,8 +358,15 @@
   1.101  fun context "-" thy = init NONE thy
   1.102    | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.103  
   1.104 -fun instantiation arities thy =
   1.105 -  init_lthy_ctxt (init_instantiaton arities) thy;
   1.106 +val instantiation = init_lthy_ctxt o init_instantiation;
   1.107 +
   1.108 +fun gen_overloading prep_operation operations thy =
   1.109 +  thy
   1.110 +  |> init_lthy_ctxt (init_overloading (map (prep_operation thy) operations));
   1.111 +
   1.112 +val overloading = gen_overloading (K I);
   1.113 +val overloading_cmd = gen_overloading (fn thy => fn (((raw_c, rawT), v), checked) =>
   1.114 +  ((Sign.intern_const thy raw_c, Sign.read_typ thy rawT), (v, checked)));
   1.115  
   1.116  end;
   1.117