setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
authorwenzelm
Fri Dec 03 17:59:13 2010 +0100 (2010-12-03)
changeset 409392c150063cd4d
parent 40938 e258f6817add
child 40940 ff805bb109d8
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
NEWS
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/RealDef.thy
src/Tools/subtyping.ML
     1.1 --- a/NEWS	Thu Dec 02 21:48:36 2010 +0100
     1.2 +++ b/NEWS	Fri Dec 03 17:59:13 2010 +0100
     1.3 @@ -101,29 +101,32 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* Quickcheck now by default uses exhaustive testing instead of random testing.
     1.8 -Random testing can be invoked by quickcheck[random],
     1.9 +* Quickcheck now by default uses exhaustive testing instead of random
    1.10 +testing.  Random testing can be invoked by quickcheck[random],
    1.11  exhaustive testing by quickcheck[exhaustive].
    1.12  
    1.13 -* Quickcheck instantiates polymorphic types with small finite datatypes
    1.14 -by default. This enables a simple execution mechanism to handle
    1.15 -quantifiers and function equality over the finite datatypes.   
    1.16 -
    1.17 -* Functions can be declared as coercions and type inference will add them
    1.18 -as necessary upon input of a term. In Complex_Main, real :: nat => real
    1.19 -and real :: int => real are declared as coercions. A new coercion function
    1.20 -f is declared like this:
    1.21 -
    1.22 -declare [[coercion f]]
    1.23 +* Quickcheck instantiates polymorphic types with small finite
    1.24 +datatypes by default. This enables a simple execution mechanism to
    1.25 +handle quantifiers and function equality over the finite datatypes.
    1.26 +
    1.27 +* Functions can be declared as coercions and type inference will add
    1.28 +them as necessary upon input of a term. In theory Complex_Main,
    1.29 +real :: nat => real and real :: int => real are declared as
    1.30 +coercions. A new coercion function f is declared like this:
    1.31 +
    1.32 +  declare [[coercion f]]
    1.33  
    1.34  To lift coercions through type constructors (eg from nat => real to
    1.35  nat list => real list), map functions can be declared, e.g.
    1.36  
    1.37 -declare [[coercion_map map]]
    1.38 -
    1.39 -Currently coercion inference is activated only in theories including real
    1.40 -numbers, i.e. descendants of Complex_Main. In other theories it needs to be
    1.41 -loaded explicitly: uses "~~/src/Tools/subtyping.ML"
    1.42 +  declare [[coercion_map map]]
    1.43 +
    1.44 +Currently coercion inference is activated only in theories including
    1.45 +real numbers, i.e. descendants of Complex_Main.  This is controlled by
    1.46 +the configuration option "infer_coercions", e.g. it can be enabled in
    1.47 +other theories like this:
    1.48 +
    1.49 +  declare [[coercion_enabled]]
    1.50  
    1.51  * Abandoned locales equiv, congruent and congruent2 for equivalence relations.
    1.52  INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).
     2.1 --- a/src/HOL/HOL.thy	Thu Dec 02 21:48:36 2010 +0100
     2.2 +++ b/src/HOL/HOL.thy	Fri Dec 03 17:59:13 2010 +0100
     2.3 @@ -33,9 +33,11 @@
     2.4    "Tools/try.ML"
     2.5    ("Tools/cnf_funcs.ML")
     2.6    ("Tools/type_mapper.ML")
     2.7 +  "~~/src/Tools/subtyping.ML"
     2.8  begin
     2.9  
    2.10  setup {* Intuitionistic.method_setup @{binding iprover} *}
    2.11 +setup Subtyping.setup
    2.12  
    2.13  
    2.14  subsection {* Primitive logic *}
     3.1 --- a/src/HOL/IsaMakefile	Thu Dec 02 21:48:36 2010 +0100
     3.2 +++ b/src/HOL/IsaMakefile	Fri Dec 03 17:59:13 2010 +0100
     3.3 @@ -156,6 +156,14 @@
     3.4  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
     3.5  
     3.6  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
     3.7 +  $(SRC)/Provers/Arith/cancel_div_mod.ML \
     3.8 +  $(SRC)/Provers/Arith/cancel_sums.ML \
     3.9 +  $(SRC)/Provers/Arith/fast_lin_arith.ML \
    3.10 +  $(SRC)/Provers/order.ML \
    3.11 +  $(SRC)/Provers/trancl.ML \
    3.12 +  $(SRC)/Tools/Metis/metis.ML \
    3.13 +  $(SRC)/Tools/rat.ML \
    3.14 +  $(SRC)/Tools/subtyping.ML \
    3.15    Complete_Lattice.thy \
    3.16    Complete_Partial_Order.thy \
    3.17    Datatype.thy \
    3.18 @@ -182,10 +190,7 @@
    3.19    SAT.thy \
    3.20    Set.thy \
    3.21    Sum_Type.thy \
    3.22 -  Tools/abel_cancel.ML \
    3.23 -  Tools/arith_data.ML \
    3.24 -  Tools/async_manager.ML \
    3.25 -  Tools/cnf_funcs.ML \
    3.26 +  Tools/Datatype/datatype.ML \
    3.27    Tools/Datatype/datatype_abs_proofs.ML \
    3.28    Tools/Datatype/datatype_aux.ML \
    3.29    Tools/Datatype/datatype_case.ML \
    3.30 @@ -193,14 +198,12 @@
    3.31    Tools/Datatype/datatype_data.ML \
    3.32    Tools/Datatype/datatype_prop.ML \
    3.33    Tools/Datatype/datatype_realizer.ML \
    3.34 -  Tools/Datatype/datatype.ML \
    3.35 -  Tools/dseq.ML \
    3.36    Tools/Function/context_tree.ML \
    3.37 +  Tools/Function/fun.ML \
    3.38 +  Tools/Function/function.ML \
    3.39    Tools/Function/function_common.ML \
    3.40    Tools/Function/function_core.ML \
    3.41    Tools/Function/function_lib.ML \
    3.42 -  Tools/Function/function.ML \
    3.43 -  Tools/Function/fun.ML \
    3.44    Tools/Function/induction_schema.ML \
    3.45    Tools/Function/lexicographic_order.ML \
    3.46    Tools/Function/measure_functions.ML \
    3.47 @@ -214,17 +217,22 @@
    3.48    Tools/Function/size.ML \
    3.49    Tools/Function/sum_tree.ML \
    3.50    Tools/Function/termination.ML \
    3.51 -  Tools/inductive_codegen.ML \
    3.52 -  Tools/inductive.ML \
    3.53 -  Tools/inductive_realizer.ML \
    3.54 -  Tools/inductive_set.ML \
    3.55 -  Tools/lin_arith.ML \
    3.56    Tools/Meson/meson.ML \
    3.57    Tools/Meson/meson_clausify.ML \
    3.58    Tools/Meson/meson_tactic.ML \
    3.59    Tools/Metis/metis_reconstruct.ML \
    3.60 +  Tools/Metis/metis_tactics.ML \
    3.61    Tools/Metis/metis_translate.ML \
    3.62 -  Tools/Metis/metis_tactics.ML \
    3.63 +  Tools/abel_cancel.ML \
    3.64 +  Tools/arith_data.ML \
    3.65 +  Tools/async_manager.ML \
    3.66 +  Tools/cnf_funcs.ML \
    3.67 +  Tools/dseq.ML \
    3.68 +  Tools/inductive.ML \
    3.69 +  Tools/inductive_codegen.ML \
    3.70 +  Tools/inductive_realizer.ML \
    3.71 +  Tools/inductive_set.ML \
    3.72 +  Tools/lin_arith.ML \
    3.73    Tools/nat_arith.ML \
    3.74    Tools/primrec.ML \
    3.75    Tools/prop_logic.ML \
    3.76 @@ -237,14 +245,7 @@
    3.77    Tools/typedef.ML \
    3.78    Transitive_Closure.thy \
    3.79    Typedef.thy \
    3.80 -  Wellfounded.thy \
    3.81 -  $(SRC)/Provers/Arith/cancel_div_mod.ML \
    3.82 -  $(SRC)/Provers/Arith/cancel_sums.ML \
    3.83 -  $(SRC)/Provers/Arith/fast_lin_arith.ML \
    3.84 -  $(SRC)/Provers/order.ML \
    3.85 -  $(SRC)/Provers/trancl.ML \
    3.86 -  $(SRC)/Tools/Metis/metis.ML \
    3.87 -  $(SRC)/Tools/rat.ML
    3.88 +  Wellfounded.thy
    3.89  
    3.90  $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
    3.91  	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
    3.92 @@ -385,7 +386,6 @@
    3.93  	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
    3.94  
    3.95  HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
    3.96 -  $(SRC)/Tools/subtyping.ML \
    3.97    Archimedean_Field.thy \
    3.98    Complex.thy \
    3.99    Complex_Main.thy \
     4.1 --- a/src/HOL/RealDef.thy	Thu Dec 02 21:48:36 2010 +0100
     4.2 +++ b/src/HOL/RealDef.thy	Fri Dec 03 17:59:13 2010 +0100
     4.3 @@ -9,7 +9,6 @@
     4.4  
     4.5  theory RealDef
     4.6  imports Rat
     4.7 -uses "~~/src/Tools/subtyping.ML"
     4.8  begin
     4.9  
    4.10  text {*
    4.11 @@ -1110,8 +1109,7 @@
    4.12    real_of_nat_def [code_unfold]: "real == real_of_nat"
    4.13    real_of_int_def [code_unfold]: "real == real_of_int"
    4.14  
    4.15 -setup Subtyping.setup
    4.16 -
    4.17 +declare [[coercion_enabled]]
    4.18  declare [[coercion "real::nat\<Rightarrow>real"]]
    4.19  declare [[coercion "real::int\<Rightarrow>real"]]
    4.20  
     5.1 --- a/src/Tools/subtyping.ML	Thu Dec 02 21:48:36 2010 +0100
     5.2 +++ b/src/Tools/subtyping.ML	Fri Dec 03 17:59:13 2010 +0100
     5.3 @@ -7,6 +7,7 @@
     5.4  signature SUBTYPING =
     5.5  sig
     5.6    datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT
     5.7 +  val coercion_enabled: bool Config.T
     5.8    val infer_types: Proof.context -> (string -> typ option) -> (indexname -> typ option) ->
     5.9      term list -> term list
    5.10    val add_type_map: term -> Context.generic -> Context.generic
    5.11 @@ -716,11 +717,15 @@
    5.12      (try (Consts.the_constraint (ProofContext.consts_of ctxt)))
    5.13      (ProofContext.def_type ctxt);
    5.14  
    5.15 +val (coercion_enabled, coercion_enabled_setup) = Attrib.config_bool "coercion_enabled" (K false);
    5.16 +
    5.17  val add_term_check =
    5.18    Syntax.add_term_check ~100 "coercions"
    5.19      (fn xs => fn ctxt =>
    5.20 -      let val xs' = coercion_infer_types ctxt xs
    5.21 -      in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end);
    5.22 +      if Config.get ctxt coercion_enabled then
    5.23 +        let val xs' = coercion_infer_types ctxt xs
    5.24 +        in if eq_list (op aconv) (xs, xs') then NONE else SOME (xs', ctxt) end
    5.25 +      else NONE);
    5.26  
    5.27  
    5.28  (* declarations *)
    5.29 @@ -821,6 +826,7 @@
    5.30  (* theory setup *)
    5.31  
    5.32  val setup =
    5.33 +  coercion_enabled_setup #>
    5.34    Context.theory_map add_term_check #>
    5.35    Attrib.setup @{binding coercion}
    5.36      (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))