added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
authorwenzelm
Sat Nov 05 15:00:49 2011 +0100 (2011-11-05)
changeset 45344e209da839ff4
parent 45343 873e9c0ca37d
child 45345 2cb00d068e3b
added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
tuned;
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Tools/code_evaluation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/goal.ML
src/Pure/logic.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 10:59:11 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Nov 05 15:00:49 2011 +0100
     1.3 @@ -75,7 +75,7 @@
     1.4          (map mk_partial_term_of (frees ~~ tys))
     1.5          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
     1.6      val insts =
     1.7 -      map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
     1.8 +      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
     1.9          [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
    1.10      val cty = Thm.ctyp_of thy ty;
    1.11    in
    1.12 @@ -93,9 +93,10 @@
    1.13      val cs = (map o apsnd o apsnd o map o map_atyps)
    1.14        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.15      val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    1.16 -    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    1.17 +    val var_insts =
    1.18 +      map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    1.19          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
    1.20 -          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
    1.21 +          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
    1.22      val var_eq =
    1.23        @{thm partial_term_of_anything}
    1.24        |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
     2.1 --- a/src/HOL/Tools/code_evaluation.ML	Sat Nov 05 10:59:11 2011 +0100
     2.2 +++ b/src/HOL/Tools/code_evaluation.ML	Sat Nov 05 15:00:49 2011 +0100
     2.3 @@ -59,8 +59,10 @@
     2.4      val t = list_comb (Const (c, tys ---> ty),
     2.5        map Free (Name.invent_names Name.context "a" tys));
     2.6      val (arg, rhs) =
     2.7 -      pairself (Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
     2.8 -        (t, (map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t) o HOLogic.reflect_term) t)
     2.9 +      pairself (Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    2.10 +        (t,
    2.11 +          map_aterms (fn t as Free (_, ty) => HOLogic.mk_term_of ty t | t => t)
    2.12 +            (HOLogic.reflect_term t));
    2.13      val cty = Thm.ctyp_of thy ty;
    2.14    in
    2.15      @{thm term_of_anything}
     3.1 --- a/src/Pure/Isar/class.ML	Sat Nov 05 10:59:11 2011 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Sat Nov 05 15:00:49 2011 +0100
     3.3 @@ -344,7 +344,7 @@
     3.4      val c' = Sign.full_name thy b;
     3.5      val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
     3.6      val ty' = Term.fastype_of rhs';
     3.7 -    val rhs'' = map_types Logic.varifyT_global rhs';
     3.8 +    val rhs'' = Logic.varify_types_global rhs';
     3.9    in
    3.10      thy
    3.11      |> Sign.add_abbrev (#1 prmode) (b, rhs'')
     4.1 --- a/src/Pure/Isar/code.ML	Sat Nov 05 10:59:11 2011 +0100
     4.2 +++ b/src/Pure/Isar/code.ML	Sat Nov 05 15:00:49 2011 +0100
     4.3 @@ -131,12 +131,14 @@
     4.4    let
     4.5      val c' = AxClass.unoverload_const thy (c, ty);
     4.6      val ty_decl = Sign.the_const_type thy c';
     4.7 -  in if Sign.typ_equiv thy
     4.8 -      (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
     4.9 -    else error ("Type\n" ^ string_of_typ thy ty
    4.10 -      ^ "\nof constant " ^ quote c
    4.11 -      ^ "\nis too specific compared to declared type\n"
    4.12 -      ^ string_of_typ thy ty_decl)
    4.13 +  in
    4.14 +    if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty))
    4.15 +    then c'
    4.16 +    else
    4.17 +      error ("Type\n" ^ string_of_typ thy ty ^
    4.18 +        "\nof constant " ^ quote c ^
    4.19 +        "\nis too specific compared to declared type\n" ^
    4.20 +        string_of_typ thy ty_decl)
    4.21    end; 
    4.22  
    4.23  fun check_const thy = check_unoverload thy o check_bare_const thy;
    4.24 @@ -403,16 +405,18 @@
    4.25    let
    4.26      val _ = Thm.cterm_of thy (Const (c, raw_ty));
    4.27      val ty = subst_signature thy c raw_ty;
    4.28 -    val ty_decl = (Logic.unvarifyT_global o const_typ thy) c;
    4.29 +    val ty_decl = Logic.unvarifyT_global (const_typ thy c);
    4.30      fun last_typ c_ty ty =
    4.31        let
    4.32          val tfrees = Term.add_tfreesT ty [];
    4.33          val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
    4.34            handle TYPE _ => no_constr thy "bad type" c_ty
    4.35          val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
    4.36 -        val _ = if has_duplicates (eq_fst (op =)) vs
    4.37 +        val _ =
    4.38 +          if has_duplicates (eq_fst (op =)) vs
    4.39            then no_constr thy "duplicate type variables in datatype" c_ty else ();
    4.40 -        val _ = if length tfrees <> length vs
    4.41 +        val _ =
    4.42 +          if length tfrees <> length vs
    4.43            then no_constr thy "type variables missing in datatype" c_ty else ();
    4.44        in (tyco, vs) end;
    4.45      val (tyco, _) = last_typ (c, ty) ty_decl;
    4.46 @@ -692,7 +696,8 @@
    4.47      val _ = (fst o dest_Var) param
    4.48        handle TERM _ => bad "Not an abstype certificate";
    4.49      val _ = if param = rhs then () else bad "Not an abstype certificate";
    4.50 -    val ((tyco, sorts), (abs, (vs, ty'))) = analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
    4.51 +    val ((tyco, sorts), (abs, (vs, ty'))) =
    4.52 +      analyze_constructor thy (abs, Logic.unvarifyT_global raw_ty);
    4.53      val ty = domain_type ty';
    4.54      val (vs', _) = logical_typscheme thy (abs, ty');
    4.55    in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
    4.56 @@ -849,7 +854,7 @@
    4.57        let
    4.58          val vs = fst (typscheme_abs thy abs_thm);
    4.59          val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
    4.60 -      in (vs, add_rhss_of_eqn thy (map_types Logic.unvarifyT_global (Thm.prop_of concrete_thm)) []) end;
    4.61 +      in (vs, add_rhss_of_eqn thy (Logic.unvarify_types_global (Thm.prop_of concrete_thm)) []) end;
    4.62  
    4.63  fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
    4.64        let
    4.65 @@ -865,7 +870,7 @@
    4.66        let
    4.67          val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
    4.68          val tyscm = typscheme_projection thy t;
    4.69 -        val t' = map_types Logic.varifyT_global t;
    4.70 +        val t' = Logic.varify_types_global t;
    4.71          fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
    4.72        in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
    4.73    | equations_of_cert thy (Abstract (abs_thm, tyco)) =
    4.74 @@ -882,7 +887,7 @@
    4.75        (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
    4.76           o snd o equations_of_cert thy) cert
    4.77    | pretty_cert thy (Projection (t, _)) =
    4.78 -      [Syntax.pretty_term_global thy (map_types Logic.varifyT_global t)]
    4.79 +      [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
    4.80    | pretty_cert thy (Abstract (abs_thm, _)) =
    4.81        [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
    4.82  
    4.83 @@ -1255,8 +1260,8 @@
    4.84    in
    4.85      thy
    4.86      |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
    4.87 -    |> change_fun_spec false rep ((K o Proj)
    4.88 -        (map_types Logic.varifyT_global (mk_proj tyco vs ty abs rep), tyco))
    4.89 +    |> change_fun_spec false rep
    4.90 +      (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
    4.91      |> Abstype_Interpretation.data (tyco, serial ())
    4.92    end;
    4.93  
     5.1 --- a/src/Pure/goal.ML	Sat Nov 05 10:59:11 2011 +0100
     5.2 +++ b/src/Pure/goal.ML	Sat Nov 05 15:00:49 2011 +0100
     5.3 @@ -168,8 +168,7 @@
     5.4      val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
     5.5  
     5.6      val global_prop =
     5.7 -      cert (Term.map_types Logic.varifyT_global
     5.8 -        (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
     5.9 +      cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
    5.10        |> Thm.weaken_sorts (Variable.sorts_of ctxt);
    5.11      val global_result = result |> Future.map
    5.12        (Drule.flexflex_unique #>
     6.1 --- a/src/Pure/logic.ML	Sat Nov 05 10:59:11 2011 +0100
     6.2 +++ b/src/Pure/logic.ML	Sat Nov 05 15:00:49 2011 +0100
     6.3 @@ -73,6 +73,8 @@
     6.4    val assum_problems: int * term -> (term -> term) * term list * term
     6.5    val varifyT_global: typ -> typ
     6.6    val unvarifyT_global: typ -> typ
     6.7 +  val varify_types_global: term -> term
     6.8 +  val unvarify_types_global: term -> term
     6.9    val varify_global: term -> term
    6.10    val unvarify_global: term -> term
    6.11    val get_goal: term -> int -> term
    6.12 @@ -524,13 +526,20 @@
    6.13  val varifyT_global = Same.commit varifyT_global_same;
    6.14  val unvarifyT_global = Same.commit unvarifyT_global_same;
    6.15  
    6.16 +fun varify_types_global tm = tm
    6.17 +  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
    6.18 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    6.19 +
    6.20 +fun unvarify_types_global tm = tm
    6.21 +  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
    6.22 +  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    6.23 +
    6.24  fun varify_global tm = tm
    6.25    |> Same.commit (Term_Subst.map_aterms_same
    6.26      (fn Free (x, T) => Var ((x, 0), T)
    6.27        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    6.28        | _ => raise Same.SAME))
    6.29 -  |> Same.commit (Term_Subst.map_types_same varifyT_global_same)
    6.30 -  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    6.31 +  |> varify_types_global;
    6.32  
    6.33  fun unvarify_global tm = tm
    6.34    |> Same.commit (Term_Subst.map_aterms_same
    6.35 @@ -538,8 +547,7 @@
    6.36        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    6.37        | Free (x, _) => raise TERM (bad_fixed x, [tm])
    6.38        | _ => raise Same.SAME))
    6.39 -  |> Same.commit (Term_Subst.map_types_same unvarifyT_global_same)
    6.40 -  handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
    6.41 +  |> unvarify_types_global;
    6.42  
    6.43  
    6.44  (* goal states *)