overloading target
authorhaftmann
Mon Dec 03 16:04:17 2007 +0100 (2007-12-03)
changeset 255198570745cb40b
parent 25518 00d5cc16e891
child 25520 e123c81257a5
overloading target
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/ROOT.ML	Mon Dec 03 16:04:16 2007 +0100
     1.2 +++ b/src/Pure/Isar/ROOT.ML	Mon Dec 03 16:04:17 2007 +0100
     1.3 @@ -47,6 +47,7 @@
     1.4  
     1.5  (*local theories and target primitives*)
     1.6  use "local_theory.ML";
     1.7 +use "overloading.ML";
     1.8  use "locale.ML";
     1.9  use "class.ML";
    1.10  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Dec 03 16:04:16 2007 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Dec 03 16:04:17 2007 +0100
     2.3 @@ -445,7 +445,7 @@
     2.4        Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class)));
     2.5  
     2.6  val _ =
     2.7 -  OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
     2.8 +  OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
     2.9     (P.and_list1 P.arity --| P.begin
    2.10       >> (fn arities => Toplevel.print o
    2.11           Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
    2.12 @@ -459,6 +459,17 @@
    2.13    || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
    2.14  
    2.15  
    2.16 +(* arbitrary overloading *)
    2.17 +
    2.18 +val _ =
    2.19 +  OuterSyntax.command "overloading" "overloaded definitions" K.thy_decl
    2.20 +   (Scan.repeat1 (P.xname --| P.$$$ "::" -- P.typ --| P.$$$ "is" -- P.name --
    2.21 +      Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true)
    2.22 +        --| P.begin
    2.23 +   >> (fn operations => Toplevel.print o
    2.24 +         Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
    2.25 +
    2.26 +
    2.27  (* code generation *)
    2.28  
    2.29  val _ =
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/overloading.ML	Mon Dec 03 16:04:17 2007 +0100
     3.3 @@ -0,0 +1,94 @@
     3.4 +(*  Title:      Pure/Isar/overloading.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Haftmann, TU Muenchen
     3.7 +
     3.8 +Overloaded definitions without any discipline.
     3.9 +*)
    3.10 +
    3.11 +signature OVERLOADING =
    3.12 +sig
    3.13 +  val init: ((string * typ) * (string * bool)) list -> theory -> local_theory
    3.14 +  val conclude: local_theory -> local_theory
    3.15 +  val declare: string * typ -> theory -> term * theory
    3.16 +  val confirm: string -> local_theory -> local_theory
    3.17 +  val define: bool -> string -> string * term -> theory -> thm * theory
    3.18 +  val operation: Proof.context -> string -> (string * bool) option
    3.19 +end;
    3.20 +
    3.21 +structure Overloading: OVERLOADING =
    3.22 +struct
    3.23 +
    3.24 +(* bookkeeping *)
    3.25 +
    3.26 +structure OverloadingData = ProofDataFun
    3.27 +(
    3.28 +  type T = ((string * typ) * (string * bool)) list;
    3.29 +  fun init _ = [];
    3.30 +);
    3.31 +
    3.32 +val get_overloading = OverloadingData.get o LocalTheory.target_of;
    3.33 +val map_overloading = LocalTheory.target o OverloadingData.map;
    3.34 +
    3.35 +fun operation lthy v = get_overloading lthy
    3.36 +  |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE);
    3.37 +
    3.38 +fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c));
    3.39 +
    3.40 +
    3.41 +(* overloaded declarations and definitions *)
    3.42 +
    3.43 +fun declare c_ty = pair (Const c_ty);
    3.44 +
    3.45 +fun define checked name (c, t) =
    3.46 +  Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t));
    3.47 +
    3.48 +
    3.49 +(* syntax *)
    3.50 +
    3.51 +fun term_check ts lthy =
    3.52 +  let
    3.53 +    val overloading = get_overloading lthy;
    3.54 +    fun subst (t as Const (c, ty)) = (case AList.lookup (op =) overloading (c, ty)
    3.55 +         of SOME (v, _) => Free (v, ty)
    3.56 +          | NONE => t)
    3.57 +      | subst t = t;
    3.58 +    val ts' = (map o map_aterms) subst ts;
    3.59 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
    3.60 +
    3.61 +fun term_uncheck ts lthy =
    3.62 +  let
    3.63 +    val overloading = get_overloading lthy;
    3.64 +    fun subst (t as Free (v, ty)) = (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) overloading
    3.65 +         of SOME c => Const (c, ty)
    3.66 +          | NONE => t)
    3.67 +      | subst t = t;
    3.68 +    val ts' = (map o map_aterms) subst ts;
    3.69 +  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end;
    3.70 +
    3.71 +
    3.72 +(* target *)
    3.73 +
    3.74 +fun init overloading thy =
    3.75 +  let
    3.76 +    val _ = if null overloading then error "At least one parameter must be given" else ();
    3.77 +  in
    3.78 +    thy
    3.79 +    |> ProofContext.init
    3.80 +    |> OverloadingData.put overloading
    3.81 +    |> fold (Variable.declare_term o Logic.mk_type o snd o fst) overloading
    3.82 +    |> Context.proof_map (
    3.83 +        Syntax.add_term_check 0 "overloading" term_check
    3.84 +        #> Syntax.add_term_uncheck 0 "overloading" term_uncheck)
    3.85 +  end;
    3.86 +
    3.87 +fun conclude lthy =
    3.88 +  let
    3.89 +    val overloading = get_overloading lthy;
    3.90 +    val _ = if null overloading then () else
    3.91 +      error ("Missing definition(s) for parameters " ^ commas (map (quote
    3.92 +        o Syntax.string_of_term lthy o Const o fst) overloading));
    3.93 +  in
    3.94 +    lthy
    3.95 +  end;
    3.96 +
    3.97 +end;
     4.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 03 16:04:16 2007 +0100
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 03 16:04:17 2007 +0100
     4.3 @@ -8,11 +8,14 @@
     4.4  signature THEORY_TARGET =
     4.5  sig
     4.6    val peek: local_theory -> {target: string, is_locale: bool,
     4.7 -    is_class: bool, instantiation: arity list}
     4.8 +    is_class: bool, instantiation: arity list,
     4.9 +    overloading: ((string * typ) * (string * bool)) list}
    4.10    val init: string option -> theory -> local_theory
    4.11    val begin: string -> Proof.context -> local_theory
    4.12    val context: xstring -> theory -> local_theory
    4.13    val instantiation: arity list -> theory -> local_theory
    4.14 +  val overloading: ((string * typ) * (string * bool)) list -> theory -> local_theory
    4.15 +  val overloading_cmd: (((xstring * xstring) * string) * bool) list -> theory -> local_theory
    4.16  end;
    4.17  
    4.18  structure TheoryTarget: THEORY_TARGET =
    4.19 @@ -21,13 +24,13 @@
    4.20  (* context data *)
    4.21  
    4.22  datatype target = Target of {target: string, is_locale: bool,
    4.23 -  is_class: bool, instantiation: arity list};
    4.24 +  is_class: bool, instantiation: arity list, overloading: ((string * typ) * (string * bool)) list};
    4.25  
    4.26 -fun make_target target is_locale is_class instantiation =
    4.27 +fun make_target target is_locale is_class instantiation overloading =
    4.28    Target {target = target, is_locale = is_locale,
    4.29 -    is_class = is_class, instantiation = instantiation};
    4.30 +    is_class = is_class, instantiation = instantiation, overloading = overloading};
    4.31  
    4.32 -val global_target = make_target "" false false [];
    4.33 +val global_target = make_target "" false false [] [];
    4.34  
    4.35  structure Data = ProofDataFun
    4.36  (
    4.37 @@ -40,7 +43,7 @@
    4.38  
    4.39  (* pretty *)
    4.40  
    4.41 -fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
    4.42 +fun pretty (Target {target, is_locale, is_class, instantiation, overloading}) ctxt =
    4.43    let
    4.44      val thy = ProofContext.theory_of ctxt;
    4.45      val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    4.46 @@ -196,10 +199,16 @@
    4.47      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    4.48      val U = map #2 xs ---> T;
    4.49      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    4.50 +    fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    4.51      val declare_const = case Class.instantiation_param lthy c
    4.52 -       of SOME c' => LocalTheory.theory_result (Class.overloaded_const (c', U, mx3))
    4.53 +       of SOME c' => if mx3 <> NoSyn then syntax_error c'
    4.54 +          else LocalTheory.theory_result (Class.overloaded_const (c', U))
    4.55              ##> Class.confirm_declaration c
    4.56 -        | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
    4.57 +        | NONE => (case Overloading.operation lthy c
    4.58 +           of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
    4.59 +              else LocalTheory.theory_result (Overloading.declare (c', U))
    4.60 +                ##> Overloading.confirm c
    4.61 +            | NONE => LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3)));
    4.62      val (const, lthy') = lthy |> declare_const;
    4.63      val t = Term.list_comb (const, map Free xs);
    4.64    in
    4.65 @@ -261,9 +270,12 @@
    4.66      val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
    4.67  
    4.68      (*def*)
    4.69 -    val define_const = if is_none (Class.instantiation_param lthy c)
    4.70 -      then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
    4.71 -      else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    4.72 +    val define_const = case Overloading.operation lthy c
    4.73 +     of SOME (_, checked) =>
    4.74 +          (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    4.75 +      | NONE => if is_none (Class.instantiation_param lthy c)
    4.76 +          then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    4.77 +          else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    4.78      val (global_def, lthy3) = lthy2
    4.79        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    4.80      val def = LocalDefs.trans_terms lthy3
    4.81 @@ -309,12 +321,15 @@
    4.82  local
    4.83  
    4.84  fun init_target _ NONE = global_target
    4.85 -  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
    4.86 +  | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [] [];
    4.87 +
    4.88 +fun init_instantiation arities = make_target "" false false arities [];
    4.89  
    4.90 -fun init_instantiaton arities = make_target "" false false arities
    4.91 +fun init_overloading operations = make_target "" false false [] operations;
    4.92  
    4.93 -fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
    4.94 +fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    4.95    if not (null instantiation) then Class.init_instantiation instantiation
    4.96 +  else if not (null overloading) then Overloading.init overloading
    4.97    else if not is_locale then ProofContext.init
    4.98    else if not is_class then Locale.init target
    4.99    else Class.init target;
   4.100 @@ -343,8 +358,15 @@
   4.101  fun context "-" thy = init NONE thy
   4.102    | context target thy = init (SOME (Locale.intern thy target)) thy;
   4.103  
   4.104 -fun instantiation arities thy =
   4.105 -  init_lthy_ctxt (init_instantiaton arities) thy;
   4.106 +val instantiation = init_lthy_ctxt o init_instantiation;
   4.107 +
   4.108 +fun gen_overloading prep_operation operations thy =
   4.109 +  thy
   4.110 +  |> init_lthy_ctxt (init_overloading (map (prep_operation thy) operations));
   4.111 +
   4.112 +val overloading = gen_overloading (K I);
   4.113 +val overloading_cmd = gen_overloading (fn thy => fn (((raw_c, rawT), v), checked) =>
   4.114 +  ((Sign.intern_const thy raw_c, Sign.read_typ thy rawT), (v, checked)));
   4.115  
   4.116  end;
   4.117