moved instantiation target formally to class_target.ML
authorhaftmann
Wed Aug 11 14:31:43 2010 +0200 (2010-08-11)
changeset 38348cf7b2121ad9d
parent 38347 19000bb11ff5
child 38349 ed50e21e715a
moved instantiation target formally to class_target.ML
src/HOL/Code_Evaluation.thy
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/typecopy.ML
src/HOL/Typerep.thy
src/HOLCF/Tools/pcpodef.ML
src/HOLCF/Tools/repdef.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:40 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:43 2010 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4          o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     1.5      in
     1.6        thy
     1.7 -      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
     1.8 +      |> Class.instantiation ([tyco], vs, @{sort term_of})
     1.9        |> `(fn lthy => Syntax.check_term lthy eq)
    1.10        |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    1.11        |> snd
     2.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:40 2010 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:43 2010 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4        #> snd
     2.5    in
     2.6      thy
     2.7 -    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
     2.8 +    |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
     2.9      |> fold_map add_def dtcos
    2.10      |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
    2.11           (fn _ => fn def_thms => tac def_thms) def_thms)
     3.1 --- a/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:40 2010 +0200
     3.2 +++ b/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:43 2010 +0200
     3.3 @@ -145,7 +145,7 @@
     3.4        |> PureThy.add_defs false
     3.5          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
     3.6             (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
     3.7 -      ||> Theory_Target.instantiation
     3.8 +      ||> Class.instantiation
     3.9             (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
    3.10        ||>> fold_map define_overloaded
    3.11          (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
     4.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:40 2010 +0200
     4.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:43 2010 +0200
     4.3 @@ -86,7 +86,7 @@
     4.4      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     4.5    in   
     4.6      thy
     4.7 -    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
     4.8 +    |> Class.instantiation ([tyco], vs, @{sort random})
     4.9      |> `(fn lthy => Syntax.check_term lthy eq)
    4.10      |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
    4.11      |> snd
    4.12 @@ -304,7 +304,7 @@
    4.13        (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
    4.14    in
    4.15      thy
    4.16 -    |> Theory_Target.instantiation (tycos, vs, @{sort random})
    4.17 +    |> Class.instantiation (tycos, vs, @{sort random})
    4.18      |> random_aux_specification prfx random_auxN auxs_eqs
    4.19      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    4.20      |-> (fn random_defs' => fold_map (fn random_def =>
     5.1 --- a/src/HOL/Tools/typecopy.ML	Wed Aug 11 14:31:40 2010 +0200
     5.2 +++ b/src/HOL/Tools/typecopy.ML	Wed Aug 11 14:31:43 2010 +0200
     5.3 @@ -116,7 +116,7 @@
     5.4      thy
     5.5      |> Code.add_datatype [constr]
     5.6      |> Code.add_eqn proj_constr
     5.7 -    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
     5.8 +    |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
     5.9      |> `(fn lthy => Syntax.check_term lthy eq)
    5.10      |-> (fn eq => Specification.definition
    5.11           (NONE, (Attrib.empty_binding, eq)))
     6.1 --- a/src/HOL/Typerep.thy	Wed Aug 11 14:31:40 2010 +0200
     6.2 +++ b/src/HOL/Typerep.thy	Wed Aug 11 14:31:43 2010 +0200
     6.3 @@ -56,7 +56,7 @@
     6.4      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     6.5    in
     6.6      thy
     6.7 -    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     6.8 +    |> Class.instantiation ([tyco], vs, @{sort typerep})
     6.9      |> `(fn lthy => Syntax.check_term lthy eq)
    6.10      |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    6.11      |> snd
     7.1 --- a/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 14:31:40 2010 +0200
     7.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 14:31:43 2010 +0200
     7.3 @@ -203,7 +203,7 @@
     7.4      val below_eqn = Logic.mk_equals (below_const newT,
     7.5        Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
     7.6      val lthy3 = thy2
     7.7 -      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
     7.8 +      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
     7.9      val ((_, (_, below_ldef)), lthy4) = lthy3
    7.10        |> Specification.definition (NONE,
    7.11            ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
     8.1 --- a/src/HOLCF/Tools/repdef.ML	Wed Aug 11 14:31:40 2010 +0200
     8.2 +++ b/src/HOLCF/Tools/repdef.ML	Wed Aug 11 14:31:43 2010 +0200
     8.3 @@ -112,7 +112,7 @@
     8.4  
     8.5      (*instantiate class rep*)
     8.6      val lthy = thy
     8.7 -      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
     8.8 +      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep});
     8.9      val ((_, (_, emb_ldef)), lthy) =
    8.10          Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
    8.11      val ((_, (_, prj_ldef)), lthy) =
     9.1 --- a/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:40 2010 +0200
     9.2 +++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:43 2010 +0200
     9.3 @@ -47,6 +47,8 @@
     9.4    val read_multi_arity: theory -> xstring list * xstring list * xstring
     9.5      -> string list * (string * sort) list * sort
     9.6    val type_name: string -> string
     9.7 +  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     9.8 +  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
     9.9  
    9.10    (*subclasses*)
    9.11    val register_subclass: class * class -> morphism option -> Element.witness option
    9.12 @@ -580,6 +582,35 @@
    9.13        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
    9.14    end;
    9.15  
    9.16 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    9.17 +
    9.18 +fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    9.19 +  case instantiation_param lthy b
    9.20 +   of SOME c => if mx <> NoSyn then syntax_error c
    9.21 +        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
    9.22 +            ##>> AxClass.define_overloaded b_def (c, rhs))
    9.23 +          ||> confirm_declaration b
    9.24 +    | NONE => lthy |>
    9.25 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    9.26 +
    9.27 +fun instantiation arities thy =
    9.28 +  thy
    9.29 +  |> init_instantiation arities
    9.30 +  |> Local_Theory.init NONE ""
    9.31 +     {define = Generic_Target.define instantiation_foundation,
    9.32 +      notes = Generic_Target.notes
    9.33 +        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
    9.34 +      abbrev = Generic_Target.abbrev
    9.35 +        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
    9.36 +      declaration = K Generic_Target.theory_declaration,
    9.37 +      syntax_declaration = K Generic_Target.theory_declaration,
    9.38 +      pretty = single o pretty_instantiation,
    9.39 +      reinit = instantiation arities o ProofContext.theory_of,
    9.40 +      exit = Local_Theory.target_of o conclude_instantiation};
    9.41 +
    9.42 +fun instantiation_cmd arities thy =
    9.43 +  instantiation (read_multi_arity thy arities) thy;
    9.44 +
    9.45  
    9.46  (* simplified instantiation interface with no class parameter *)
    9.47  
    10.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:40 2010 +0200
    10.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:43 2010 +0200
    10.3 @@ -472,7 +472,7 @@
    10.4    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
    10.5     (Parse.multi_arity --| Parse.begin
    10.6       >> (fn arities => Toplevel.print o
    10.7 -         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
    10.8 +         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
    10.9  
   10.10  val _ =
   10.11    Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
    11.1 --- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:31:40 2010 +0200
    11.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:31:43 2010 +0200
    11.3 @@ -10,8 +10,6 @@
    11.4    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
    11.5    val init: string option -> theory -> local_theory
    11.6    val context_cmd: xstring -> theory -> local_theory
    11.7 -  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
    11.8 -  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    11.9  end;
   11.10  
   11.11  structure Theory_Target: THEORY_TARGET =
   11.12 @@ -89,8 +87,6 @@
   11.13  
   11.14  (* define *)
   11.15  
   11.16 -fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   11.17 -
   11.18  fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   11.19    Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   11.20    #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
   11.21 @@ -103,14 +99,7 @@
   11.22      #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
   11.23      #> pair (lhs, def))
   11.24  
   11.25 -fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   11.26 -  case Class_Target.instantiation_param lthy b
   11.27 -   of SOME c => if mx <> NoSyn then syntax_error c
   11.28 -        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
   11.29 -            ##>> AxClass.define_overloaded b_def (c, rhs))
   11.30 -          ||> Class_Target.confirm_declaration b
   11.31 -    | NONE => lthy |>
   11.32 -        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
   11.33 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   11.34  
   11.35  fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   11.36    if not is_locale then (NoSyn, NoSyn, mx)
   11.37 @@ -253,24 +242,6 @@
   11.38  fun context_cmd "-" thy = init NONE thy
   11.39    | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
   11.40  
   11.41 -fun instantiation arities thy =
   11.42 -  thy
   11.43 -  |> Class_Target.init_instantiation arities
   11.44 -  |> Local_Theory.init NONE ""
   11.45 -     {define = Generic_Target.define instantiation_foundation,
   11.46 -      notes = Generic_Target.notes
   11.47 -        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
   11.48 -      abbrev = Generic_Target.abbrev
   11.49 -        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
   11.50 -      declaration = K Generic_Target.theory_declaration,
   11.51 -      syntax_declaration = K Generic_Target.theory_declaration,
   11.52 -      pretty = single o Class_Target.pretty_instantiation,
   11.53 -      reinit = instantiation arities o ProofContext.theory_of,
   11.54 -      exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
   11.55 -
   11.56 -fun instantiation_cmd arities thy =
   11.57 -  instantiation (Class_Target.read_multi_arity thy arities) thy;
   11.58 -
   11.59  end;
   11.60  
   11.61  end;