merged
authorhaftmann
Wed Aug 11 13:31:29 2010 +0200 (2010-08-11)
changeset 38343e5418eec375c
parent 38326 01d2ef471ffe
parent 38342 09d4a04d5c2e
child 38344 36f179131633
merged
src/Pure/ROOT.ML
     1.1 --- a/src/HOL/Tools/primrec.ML	Wed Aug 11 12:50:33 2010 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 13:31:29 2010 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4  
     1.5  fun add_primrec_overloaded ops fixes specs thy =
     1.6    let
     1.7 -    val lthy = Theory_Target.overloading ops thy;
     1.8 +    val lthy = Overloading.overloading ops thy;
     1.9      val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    1.10      val simps' = ProofContext.export lthy' lthy simps;
    1.11    in ((ts, simps'), Local_Theory.exit_global lthy') end;
     2.1 --- a/src/Pure/Isar/generic_target.ML	Wed Aug 11 12:50:33 2010 +0200
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Aug 11 13:31:29 2010 +0200
     2.3 @@ -21,11 +21,21 @@
     2.4      -> term list -> local_theory -> local_theory)
     2.5      -> string * bool -> (binding * mixfix) * term -> local_theory
     2.6      -> (term * term) * local_theory
     2.7 +
     2.8 +  val theory_declaration: declaration -> local_theory -> local_theory
     2.9 +  val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
    2.10 +    -> term list * term list -> local_theory -> (term * thm) * local_theory
    2.11 +  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
    2.12 +    -> local_theory -> local_theory
    2.13 +  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
    2.14 +    -> local_theory -> local_theory
    2.15  end;
    2.16  
    2.17  structure Generic_Target: GENERIC_TARGET =
    2.18  struct
    2.19  
    2.20 +(** lifting primitive to target operations **)
    2.21 +
    2.22  (* mixfix syntax *)
    2.23  
    2.24  fun check_mixfix ctxt (b, extra_tfrees) mx =
    2.25 @@ -176,4 +186,40 @@
    2.26      |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
    2.27    end;
    2.28  
    2.29 +
    2.30 +(** primitive theory operations **)
    2.31 +
    2.32 +fun theory_declaration decl lthy =
    2.33 +  let
    2.34 +    val global_decl = Morphism.form
    2.35 +      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
    2.36 +  in
    2.37 +    lthy
    2.38 +    |> Local_Theory.theory (Context.theory_map global_decl)
    2.39 +    |> Local_Theory.target (Context.proof_map global_decl)
    2.40 +  end;
    2.41 +
    2.42 +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    2.43 +  let
    2.44 +    val (const, lthy2) = lthy |> Local_Theory.theory_result
    2.45 +      (Sign.declare_const ((b, U), mx));
    2.46 +    val lhs = list_comb (const, type_params @ term_params);
    2.47 +    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
    2.48 +      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
    2.49 +  in ((lhs, def), lthy3) end;
    2.50 +
    2.51 +fun theory_notes kind global_facts lthy =
    2.52 +  let
    2.53 +    val thy = ProofContext.theory_of lthy;
    2.54 +    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
    2.55 +  in
    2.56 +    lthy
    2.57 +    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
    2.58 +    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
    2.59 +  end;
    2.60 +
    2.61 +fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
    2.62 +  (Sign.add_abbrev (#1 prmode) (b, t) #->
    2.63 +    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
    2.64 +
    2.65  end;
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 12:50:33 2010 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 13:31:29 2010 +0200
     3.3 @@ -492,7 +492,7 @@
     3.4        Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
     3.5        >> Parse.triple1) --| Parse.begin
     3.6     >> (fn operations => Toplevel.print o
     3.7 -         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
     3.8 +         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
     3.9  
    3.10  
    3.11  (* code generation *)
     4.1 --- a/src/Pure/Isar/overloading.ML	Wed Aug 11 12:50:33 2010 +0200
     4.2 +++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 13:31:29 2010 +0200
     4.3 @@ -19,6 +19,9 @@
     4.4    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     4.5      -> Proof.context -> Proof.context
     4.6    val set_primary_constraints: Proof.context -> Proof.context
     4.7 +
     4.8 +  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     4.9 +  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    4.10  end;
    4.11  
    4.12  structure Overloading: OVERLOADING =
    4.13 @@ -194,4 +197,40 @@
    4.14        (Pretty.str "overloading" :: map pr_operation overloading)
    4.15    end;
    4.16  
    4.17 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    4.18 +
    4.19 +fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    4.20 +  case operation lthy b
    4.21 +   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
    4.22 +        else lthy |> Local_Theory.theory_result (declare (c, U)
    4.23 +            ##>> define checked b_def (c, rhs))
    4.24 +          ||> confirm b
    4.25 +    | NONE => lthy |>
    4.26 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    4.27 +
    4.28 +fun gen_overloading prep_const raw_ops thy =
    4.29 +  let
    4.30 +    val ctxt = ProofContext.init_global thy;
    4.31 +    val ops = raw_ops |> map (fn (name, const, checked) =>
    4.32 +      (name, Term.dest_Const (prep_const ctxt const), checked));
    4.33 +  in
    4.34 +    thy
    4.35 +    |> init ops
    4.36 +    |> Local_Theory.init NONE ""
    4.37 +       {define = Generic_Target.define overloading_foundation,
    4.38 +        notes = Generic_Target.notes
    4.39 +          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
    4.40 +        abbrev = Generic_Target.abbrev
    4.41 +          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
    4.42 +            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    4.43 +        declaration = K Generic_Target.theory_declaration,
    4.44 +        syntax_declaration = K Generic_Target.theory_declaration,
    4.45 +        pretty = single o pretty,
    4.46 +        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
    4.47 +        exit = Local_Theory.target_of o conclude}
    4.48 +  end;
    4.49 +
    4.50 +val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    4.51 +val overloading_cmd = gen_overloading Syntax.read_term;
    4.52 +
    4.53  end;
     5.1 --- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:50:33 2010 +0200
     5.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 13:31:29 2010 +0200
     5.3 @@ -7,18 +7,11 @@
     5.4  
     5.5  signature THEORY_TARGET =
     5.6  sig
     5.7 -  val peek: local_theory ->
     5.8 -   {target: string,
     5.9 -    is_locale: bool,
    5.10 -    is_class: bool,
    5.11 -    instantiation: string list * (string * sort) list * sort,
    5.12 -    overloading: (string * (string * typ) * bool) list}
    5.13 +  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
    5.14    val init: string option -> theory -> local_theory
    5.15    val context_cmd: xstring -> theory -> local_theory
    5.16    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    5.17    val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    5.18 -  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
    5.19 -  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    5.20  end;
    5.21  
    5.22  structure Theory_Target: THEORY_TARGET =
    5.23 @@ -26,15 +19,12 @@
    5.24  
    5.25  (* context data *)
    5.26  
    5.27 -datatype target = Target of {target: string, is_locale: bool,
    5.28 -  is_class: bool, instantiation: string list * (string * sort) list * sort,
    5.29 -  overloading: (string * (string * typ) * bool) list};
    5.30 +datatype target = Target of {target: string, is_locale: bool, is_class: bool};
    5.31  
    5.32 -fun make_target target is_locale is_class instantiation overloading =
    5.33 -  Target {target = target, is_locale = is_locale,
    5.34 -    is_class = is_class, instantiation = instantiation, overloading = overloading};
    5.35 +fun make_target target is_locale is_class =
    5.36 +  Target {target = target, is_locale = is_locale, is_class = is_class};
    5.37  
    5.38 -val global_target = make_target "" false false ([], [], []) [];
    5.39 +val global_target = make_target "" false false;
    5.40  
    5.41  structure Data = Proof_Data
    5.42  (
    5.43 @@ -47,28 +37,18 @@
    5.44  
    5.45  (* generic declarations *)
    5.46  
    5.47 -fun theory_declaration decl lthy =
    5.48 -  let
    5.49 -    val global_decl = Morphism.form
    5.50 -      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
    5.51 -  in
    5.52 -    lthy
    5.53 -    |> Local_Theory.theory (Context.theory_map global_decl)
    5.54 -    |> Local_Theory.target (Context.proof_map global_decl)
    5.55 -  end;
    5.56 -
    5.57  fun locale_declaration locale { syntax, pervasive } decl lthy =
    5.58    let
    5.59      val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    5.60      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    5.61    in
    5.62      lthy
    5.63 -    |> pervasive ? theory_declaration decl
    5.64 +    |> pervasive ? Generic_Target.theory_declaration decl
    5.65      |> Local_Theory.target (add locale locale_decl)
    5.66    end;
    5.67  
    5.68  fun target_declaration (Target {target, ...}) { syntax, pervasive } =
    5.69 -  if target = "" then theory_declaration
    5.70 +  if target = "" then Generic_Target.theory_declaration
    5.71    else locale_declaration target { syntax = syntax, pervasive = pervasive };
    5.72  
    5.73  
    5.74 @@ -111,23 +91,14 @@
    5.75  
    5.76  fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    5.77  
    5.78 -fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    5.79 -  let
    5.80 -    val (const, lthy2) = lthy |> Local_Theory.theory_result
    5.81 -      (Sign.declare_const ((b, U), mx));
    5.82 -    val lhs = list_comb (const, type_params @ term_params);
    5.83 -    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
    5.84 -      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
    5.85 -  in ((lhs, def), lthy3) end;
    5.86 -
    5.87  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    5.88 -  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    5.89 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    5.90    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
    5.91      #> pair (lhs, def))
    5.92  
    5.93  fun class_foundation (ta as Target {target, ...})
    5.94      (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
    5.95 -  theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    5.96 +  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
    5.97    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
    5.98      #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
    5.99      #> pair (lhs, def))
   5.100 @@ -139,16 +110,7 @@
   5.101              ##>> AxClass.define_overloaded b_def (c, rhs))
   5.102            ||> Class_Target.confirm_declaration b
   5.103      | NONE => lthy |>
   5.104 -        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   5.105 -
   5.106 -fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   5.107 -  case Overloading.operation lthy b
   5.108 -   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
   5.109 -        else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
   5.110 -            ##>> Overloading.define checked b_def (c, rhs))
   5.111 -          ||> Overloading.confirm b
   5.112 -    | NONE => lthy |>
   5.113 -        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   5.114 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   5.115  
   5.116  fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   5.117    if not is_locale then (NoSyn, NoSyn, mx)
   5.118 @@ -192,16 +154,6 @@
   5.119  
   5.120  (* notes *)
   5.121  
   5.122 -fun theory_notes kind global_facts lthy =
   5.123 -  let
   5.124 -    val thy = ProofContext.theory_of lthy;
   5.125 -    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
   5.126 -  in
   5.127 -    lthy
   5.128 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
   5.129 -    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
   5.130 -  end;
   5.131 -
   5.132  fun locale_notes locale kind global_facts local_facts lthy = 
   5.133    let
   5.134      val global_facts' = Attrib.map_facts (K I) global_facts;
   5.135 @@ -215,15 +167,11 @@
   5.136  
   5.137  fun target_notes (ta as Target {target, is_locale, ...}) =
   5.138    if is_locale then locale_notes target
   5.139 -    else fn kind => fn global_facts => fn _ => theory_notes kind global_facts;
   5.140 +    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
   5.141  
   5.142  
   5.143  (* abbrev *)
   5.144  
   5.145 -fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
   5.146 -  (Sign.add_abbrev (#1 prmode) (b, t) #->
   5.147 -    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
   5.148 -
   5.149  fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
   5.150    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
   5.151      (fn (lhs, _) => locale_const_declaration ta prmode
   5.152 @@ -236,7 +184,7 @@
   5.153        |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
   5.154        |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
   5.155      else lthy
   5.156 -      |> theory_abbrev prmode ((b, mx), global_rhs);
   5.157 +      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
   5.158  
   5.159  
   5.160  (* pretty *)
   5.161 @@ -261,26 +209,22 @@
   5.162        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
   5.163    end;
   5.164  
   5.165 -fun pretty (Target {target, is_class, instantiation, overloading, ...}) ctxt =
   5.166 +fun pretty (Target {target, is_class, ...}) ctxt =
   5.167    Pretty.block [Pretty.command "theory", Pretty.brk 1,
   5.168        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
   5.169 -    (if not (null overloading) then [Overloading.pretty ctxt]
   5.170 -     else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
   5.171 -     else pretty_thy ctxt target is_class);
   5.172 +    pretty_thy ctxt target is_class;
   5.173  
   5.174  
   5.175  (* init various targets *)
   5.176  
   5.177  local
   5.178  
   5.179 -fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) =
   5.180 -  if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   5.181 -  else if not (null overloading) then Overloading.init overloading
   5.182 -  else if not is_locale then ProofContext.init_global
   5.183 +fun init_data (Target {target, is_locale, is_class}) =
   5.184 +  if not is_locale then ProofContext.init_global
   5.185    else if not is_class then Locale.init target
   5.186    else Class_Target.init target;
   5.187  
   5.188 -fun init_target (ta as Target {target, instantiation, overloading, ...}) thy =
   5.189 +fun init_target (ta as Target {target, ...}) thy =
   5.190    thy
   5.191    |> init_data ta
   5.192    |> Data.put ta
   5.193 @@ -294,39 +238,14 @@
   5.194          { syntax = true, pervasive = pervasive },
   5.195        pretty = pretty ta,
   5.196        reinit = init_target ta o ProofContext.theory_of,
   5.197 -      exit = Local_Theory.target_of o
   5.198 -        (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
   5.199 -         else if not (null overloading) then Overloading.conclude
   5.200 -         else I)};
   5.201 +      exit = Local_Theory.target_of};
   5.202  
   5.203  fun named_target _ NONE = global_target
   5.204    | named_target thy (SOME target) =
   5.205        if Locale.defined thy target
   5.206 -      then make_target target true (Class_Target.is_class thy target) ([], [], []) []
   5.207 +      then make_target target true (Class_Target.is_class thy target)
   5.208        else error ("No such locale: " ^ quote target);
   5.209  
   5.210 -fun gen_overloading prep_const raw_ops thy =
   5.211 -  let
   5.212 -    val ctxt = ProofContext.init_global thy;
   5.213 -    val ops = raw_ops |> map (fn (name, const, checked) =>
   5.214 -      (name, Term.dest_Const (prep_const ctxt const), checked));
   5.215 -  in
   5.216 -    thy
   5.217 -    |> Overloading.init ops
   5.218 -    |> Local_Theory.init NONE ""
   5.219 -       {define = Generic_Target.define overloading_foundation,
   5.220 -        notes = Generic_Target.notes
   5.221 -          (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
   5.222 -        abbrev = Generic_Target.abbrev
   5.223 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
   5.224 -            theory_abbrev prmode ((b, mx), t)),
   5.225 -        declaration = fn pervasive => theory_declaration,
   5.226 -        syntax_declaration = fn pervasive => theory_declaration,
   5.227 -        pretty = single o Overloading.pretty,
   5.228 -        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
   5.229 -        exit = Local_Theory.target_of o Overloading.conclude}
   5.230 -  end;
   5.231 -
   5.232  in
   5.233  
   5.234  fun init target thy = init_target (named_target thy target) thy;
   5.235 @@ -340,11 +259,11 @@
   5.236    |> Local_Theory.init NONE ""
   5.237       {define = Generic_Target.define instantiation_foundation,
   5.238        notes = Generic_Target.notes
   5.239 -        (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
   5.240 +        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   5.241        abbrev = Generic_Target.abbrev
   5.242 -        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
   5.243 -      declaration = fn pervasive => theory_declaration,
   5.244 -      syntax_declaration = fn pervasive => theory_declaration,
   5.245 +        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
   5.246 +      declaration = K Generic_Target.theory_declaration,
   5.247 +      syntax_declaration = K Generic_Target.theory_declaration,
   5.248        pretty = single o Class_Target.pretty_instantiation,
   5.249        reinit = instantiation arities o ProofContext.theory_of,
   5.250        exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
   5.251 @@ -352,9 +271,6 @@
   5.252  fun instantiation_cmd arities thy =
   5.253    instantiation (Class_Target.read_multi_arity thy arities) thy;
   5.254  
   5.255 -val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   5.256 -val overloading_cmd = gen_overloading Syntax.read_term;
   5.257 -
   5.258  end;
   5.259  
   5.260  end;
     6.1 --- a/src/Pure/ROOT.ML	Wed Aug 11 12:50:33 2010 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Wed Aug 11 13:31:29 2010 +0200
     6.3 @@ -205,9 +205,9 @@
     6.4  
     6.5  (*local theories and targets*)
     6.6  use "Isar/local_theory.ML";
     6.7 +use "Isar/locale.ML";
     6.8  use "Isar/generic_target.ML";
     6.9  use "Isar/overloading.ML";
    6.10 -use "Isar/locale.ML";
    6.11  use "axclass.ML";
    6.12  use "Isar/class_target.ML";
    6.13  use "Isar/theory_target.ML";