# HG changeset patch # User blanchet # Date 1385066014 -3600 # Node ID b8d0d8407c3bf8dc656024a2dc378e4fde54e0e4 # Parent 2b0da4c1dd4032664c88cca42fd22ae1dd481674 eliminated Sledgehammer's dependency on old-style datatypes diff -r 2b0da4c1dd40 -r b8d0d8407c3b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 21 21:33:34 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 21 21:33:34 2013 +0100 @@ -335,9 +335,7 @@ (* Readable names for the more common symbolic functions. Do not mess with the table unless you know what you are doing. *) val const_trans_table = - [(@{type_name Product_Type.prod}, "prod"), - (@{type_name Sum_Type.sum}, "sum"), - (@{const_name False}, "False"), + [(@{const_name False}, "False"), (@{const_name True}, "True"), (@{const_name Not}, "Not"), (@{const_name conj}, "conj"), @@ -2738,20 +2736,8 @@ syms [] in (heading, decls) :: problem end -val typ_of_dtyp = Logic.varifyT_global oo Datatype_Aux.typ_of_dtyp - -fun ctrs_of_datatype descr (_, (s, Ds, ctrs)) = - if forall (can Datatype_Aux.dest_DtTFree) Ds then - let val dataT = Type (s, map (typ_of_dtyp descr) Ds) in - SOME (map (fn (s, Ds) => (s, map (typ_of_dtyp descr) Ds ---> dataT)) ctrs) - end - else - NONE - -fun ctrss_of_descr descr = map_filter (ctrs_of_datatype descr) descr - -fun all_ctrss_of_datatypes thy = - Symtab.fold (snd #> #descr #> ctrss_of_descr #> append) (Datatype.get_all thy) [] +fun all_ctrss_of_datatypes ctxt = + map (map_filter (try dest_Const) o #ctrs) (Ctr_Sugar.ctr_sugars_of ctxt) val app_op_and_predicator_threshold = 45 @@ -2780,7 +2766,7 @@ translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts val (_, sym_tab0) = sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish - val ctrss = all_ctrss_of_datatypes thy + val ctrss = all_ctrss_of_datatypes ctxt fun firstorderize in_helper = firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish sym_tab0 diff -r 2b0da4c1dd40 -r b8d0d8407c3b src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Thu Nov 21 21:33:34 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Thu Nov 21 21:33:34 2013 +0100 @@ -29,7 +29,6 @@ val varify_type : Proof.context -> typ -> typ val instantiate_type : theory -> typ -> typ -> typ -> typ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ - val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ val is_type_surely_finite : Proof.context -> typ -> bool val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool val s_not : term -> term @@ -191,24 +190,11 @@ instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) end -fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) = - the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a)) - | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) = - Type (s, map (typ_of_dtyp descr typ_assoc) Us) - | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) = - let val (s, ds, _) = the (AList.lookup (op =) descr i) in - Type (s, map (typ_of_dtyp descr typ_assoc) ds) - end - -fun datatype_constrs thy (T as Type (s, Ts)) = - (case Datatype.get_info thy s of - SOME {index, descr, ...} => - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in - map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T)) - constrs - end - | NONE => []) - | datatype_constrs _ _ = [] +fun free_constructors_of ctxt (Type (s, Ts)) = + (case Ctr_Sugar.ctr_sugar_of ctxt s of + SOME {ctrs, ...} => map_filter (try dest_Const o Ctr_Sugar.mk_ctr Ts) ctrs + | NONE => []) + | free_constructors_of _ _ = [] (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means @@ -239,12 +225,11 @@ | @{typ nat} => 0 (* optimization *) | Type ("Int.int", []) => 0 (* optimization *) | Type (s, _) => - (case datatype_constrs thy T of + (case free_constructors_of ctxt T of constrs as _ :: _ => let val constr_cards = - map (Integer.prod o map (aux slack (T :: avoid)) o binder_types - o snd) constrs + map (Integer.prod o map (aux slack (T :: avoid)) o binder_types o snd) constrs in if exists (curry (op =) 0) constr_cards then 0 else Int.min (max, Integer.sum constr_cards) @@ -270,10 +255,10 @@ else default_card | [] => default_card) + | TFree _ => (* Very slightly unsound: Type variables are assumed not to be constrained to cardinality 1. (In practice, the user would most likely have used "unit" directly anyway.) *) - | TFree _ => if not sound andalso default_card = 1 then 2 else default_card | TVar _ => default_card in Int.min (max, aux false [] T) end diff -r 2b0da4c1dd40 -r b8d0d8407c3b src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Nov 21 21:33:34 2013 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Nov 21 21:33:34 2013 +0100 @@ -269,7 +269,15 @@ | NONE => false) | _ => false -val typ_of_dtyp = ATP_Util.typ_of_dtyp +fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) = + the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a)) + | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) = + Type (s, map (typ_of_dtyp descr typ_assoc) Us) + | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) = + let val (s, ds, _) = the (AList.lookup (op =) descr i) in + Type (s, map (typ_of_dtyp descr typ_assoc) ds) + end + val varify_type = ATP_Util.varify_type val instantiate_type = ATP_Util.instantiate_type val varify_and_instantiate_type = ATP_Util.varify_and_instantiate_type