optimized code generated for datatype cases + more;
more = lazy creation of debugging messages in mono code
+ use of "let" when performing some beta-applications (to avoid exponential blowup)
+ removal of some set constructs, to simplify the code and increase precision in some cases (and decrease it in others, but this can be regained)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 21 09:38:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Jun 21 11:15:21 2010 +0200
@@ -64,6 +64,10 @@
val iter_var_prefix : string
val strip_first_name_sep : string -> string * string
val original_name : string -> string
+ val abs_var : indexname * typ -> term -> term
+ val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
+ val s_betapply : typ list -> term * term -> term
+ val s_betapplys : typ list -> term * term list -> term
val s_conj : term * term -> term
val s_disj : term * term -> term
val strip_any_connective : term -> term list * term
@@ -162,7 +166,6 @@
val is_finite_type : hol_context -> typ -> bool
val is_small_finite_type : hol_context -> typ -> bool
val special_bounds : term list -> (indexname * typ) list
- val abs_var : indexname * typ -> term -> term
val is_funky_typedef : theory -> typ -> bool
val all_axioms_of :
Proof.context -> (term * term) list -> term list * term list * term list
@@ -302,10 +305,55 @@
else
s
-fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
- | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
- | s_betapply p = betapply p
-val s_betapplys = Library.foldl s_betapply
+fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
+
+fun let_var s = (nitpick_prefix ^ s, 999)
+val let_inline_threshold = 20
+
+fun s_let s n abs_T body_T f t =
+ if (n - 1) * (size_of_term t - 1) <= let_inline_threshold then
+ f t
+ else
+ let val z = (let_var s, abs_T) in
+ Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
+ $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
+ end
+
+fun loose_bvar1_count (Bound i, k) = if i = k then 1 else 0
+ | loose_bvar1_count (t1 $ t2, k) =
+ loose_bvar1_count (t1, k) + loose_bvar1_count (t2, k)
+ | loose_bvar1_count (Abs (_, _, t), k) = loose_bvar1_count (t, k + 1)
+ | loose_bvar1_count _ = 0
+
+fun s_betapply _ (Const (@{const_name If}, _) $ @{const True} $ t1', _) = t1'
+ | s_betapply _ (Const (@{const_name If}, _) $ @{const False} $ _, t2) = t2
+ | s_betapply Ts (Const (@{const_name Let},
+ Type (_, [bound_T, Type (_, [_, body_T])]))
+ $ t12 $ Abs (s, T, t13'), t2) =
+ let val body_T' = range_type body_T in
+ Const (@{const_name Let}, bound_T --> (bound_T --> body_T') --> body_T')
+ $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
+ end
+ | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
+ (s_let s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
+ (curry betapply t1) t2
+ handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
+ | s_betapply _ (t1, t2) = t1 $ t2
+fun s_betapplys Ts = Library.foldl (s_betapply Ts)
+
+fun s_beta_norm Ts t =
+ let
+ fun aux _ (Var _) = raise Same.SAME
+ | aux Ts (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) t')
+ | aux Ts ((t1 as Abs _) $ t2) =
+ Same.commit (aux Ts) (s_betapply Ts (t1, t2))
+ | aux Ts (t1 $ t2) =
+ ((case aux Ts t1 of
+ t1 as Abs _ => Same.commit (aux Ts) (s_betapply Ts (t1, t2))
+ | t1 => t1 $ Same.commit (aux Ts) t2)
+ handle Same.SAME => t1 $ aux Ts t2)
+ | aux _ _ = raise Same.SAME
+ in aux Ts t handle Same.SAME => t end
fun s_conj (t1, @{const True}) = t1
| s_conj (@{const True}, t2) = t2
@@ -344,7 +392,7 @@
(@{const_name True}, 0),
(@{const_name All}, 1),
(@{const_name Ex}, 1),
- (@{const_name "op ="}, 2),
+ (@{const_name "op ="}, 1),
(@{const_name "op &"}, 2),
(@{const_name "op |"}, 2),
(@{const_name "op -->"}, 2),
@@ -355,7 +403,6 @@
(@{const_name fst}, 1),
(@{const_name snd}, 1),
(@{const_name Id}, 0),
- (@{const_name insert}, 2),
(@{const_name converse}, 1),
(@{const_name trancl}, 1),
(@{const_name rel_comp}, 2),
@@ -396,10 +443,7 @@
((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
((@{const_name of_nat}, nat_T --> int_T), 0)]
val built_in_set_consts =
- [(@{const_name semilattice_inf_class.inf}, 2),
- (@{const_name semilattice_sup_class.sup}, 2),
- (@{const_name minus_class.minus}, 2),
- (@{const_name ord_class.less_eq}, 2)]
+ [(@{const_name ord_class.less_eq}, 2)]
fun unarize_type @{typ "unsigned_bit word"} = nat_T
| unarize_type @{typ "signed_bit word"} = int_T
@@ -924,8 +968,8 @@
Const x' =>
if x = x' then @{const True}
else if is_constr_like ctxt x' then @{const False}
- else betapply (discr_term_for_constr hol_ctxt x, t)
- | _ => betapply (discr_term_for_constr hol_ctxt x, t)
+ else s_betapply [] (discr_term_for_constr hol_ctxt x, t)
+ | _ => s_betapply [] (discr_term_for_constr hol_ctxt x, t)
fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
let val (arg_Ts, dataT) = strip_type T in
@@ -955,7 +999,8 @@
else if is_constr_like ctxt x' then Const (@{const_name unknown}, res_T)
else raise SAME ()
| _ => raise SAME())
- handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
+ handle SAME () =>
+ s_betapply [] (nth_arg_sel_term_for_constr thy stds x n, t)
end
fun construct_value _ _ x [] = Const x
@@ -1150,8 +1195,6 @@
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
-fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
-
fun is_funky_typedef_name thy s =
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
@{type_name int}] s orelse
@@ -1309,7 +1352,8 @@
original_name s <> s then
NONE
else
- x |> def_props_for_const thy [(NONE, false)] false table |> List.last
+ x |> def_props_for_const thy [(NONE, false)] false table
+ |> List.last
|> normalized_rhs_of |> Option.map (prefix_abs_vars s)
handle List.Empty => NONE
@@ -1458,25 +1502,44 @@
(** Constant unfolding **)
-fun constr_case_body ctxt stds (j, (x as (_, T))) =
+fun constr_case_body ctxt stds (func_t, (x as (_, T))) =
let val arg_Ts = binder_types T in
- list_comb (Bound j, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
- (index_seq 0 (length arg_Ts)) arg_Ts)
+ s_betapplys [] (func_t, map2 (select_nth_constr_arg ctxt stds x (Bound 0))
+ (index_seq 0 (length arg_Ts)) arg_Ts)
end
-fun add_constr_case (hol_ctxt as {ctxt, stds, ...}) res_T (j, x) res_t =
- Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
- $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body ctxt stds (j, x)
- $ res_t
-fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T =
+fun add_constr_case res_T (body_t, guard_t) res_t =
+ if res_T = bool_T then
+ s_conj (HOLogic.mk_imp (guard_t, body_t), res_t)
+ else
+ Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
+ $ guard_t $ body_t $ res_t
+fun optimized_case_def (hol_ctxt as {ctxt, stds, ...}) dataT res_T func_ts =
let
val xs = datatype_constrs hol_ctxt dataT
- val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
- val (xs', x) = split_last xs
+ val cases =
+ func_ts ~~ xs
+ |> map (fn (func_t, x) =>
+ (constr_case_body ctxt stds (incr_boundvars 1 func_t, x),
+ discriminate_value hol_ctxt x (Bound 0)))
+ |> AList.group (op aconv)
+ |> map (apsnd (List.foldl s_disj @{const False}))
+ |> sort (int_ord o pairself (size_of_term o fst))
+ |> rev
in
- constr_case_body ctxt stds (1, x)
- |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
- |> fold_rev (curry absdummy) (func_Ts @ [dataT])
+ if res_T = bool_T then
+ if forall (member (op =) [@{const False}, @{const True}] o fst) cases then
+ case cases of
+ [(body_t, _)] => body_t
+ | [_, (@{const True}, head_t2)] => head_t2
+ | [_, (@{const False}, head_t2)] => @{const Not} $ head_t2
+ | _ => raise BAD ("Nitpick_HOL.optimized_case_def", "impossible cases")
+ else
+ @{const True} |> fold_rev (add_constr_case res_T) cases
+ else
+ fst (hd cases) |> fold_rev (add_constr_case res_T) (tl cases)
end
+ |> curry absdummy dataT
+
fun optimized_record_get (hol_ctxt as {thy, ctxt, stds, ...}) s rec_T res_T t =
let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
case no_of_record_field thy s rec_T of
@@ -1504,7 +1567,7 @@
map2 (fn j => fn T =>
let val t = select_nth_constr_arg ctxt stds constr_x rec_t j T in
if j = special_j then
- betapply (fun_t, t)
+ s_betapply [] (fun_t, t)
else if j = n - 1 andalso special_j = ~1 then
optimized_record_update hol_ctxt s
(rec_T |> dest_Type |> snd |> List.last) fun_t t
@@ -1542,12 +1605,13 @@
handle TERM _ => raise SAME ()
else
raise SAME ())
- handle SAME () => betapply (do_term depth Ts t0, do_term depth Ts t1))
+ handle SAME () =>
+ s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
| Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
| (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
- betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
- map (do_term depth Ts) [t1, t2])
+ s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
+ map (do_term depth Ts) [t1, t2])
| Const (x as (@{const_name distinct},
Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
$ (t1 as _ $ _) =>
@@ -1560,11 +1624,11 @@
do_term depth Ts t2
else
do_const depth Ts t x [t1, t2, t3]
- | Const x $ t1 $ t2 $ t3 => do_const depth Ts t x [t1, t2, t3]
- | Const x $ t1 $ t2 => do_const depth Ts t x [t1, t2]
- | Const x $ t1 => do_const depth Ts t x [t1]
| Const x => do_const depth Ts t x []
- | t1 $ t2 => betapply (do_term depth Ts t1, do_term depth Ts t2)
+ | t1 $ t2 =>
+ (case strip_comb t of
+ (Const x, ts) => do_const depth Ts t x ts
+ | _ => s_betapply [] (do_term depth Ts t1, do_term depth Ts t2))
| Free _ => t
| Var _ => t
| Bound _ => t
@@ -1585,13 +1649,17 @@
(Const x, ts)
else case AList.lookup (op =) case_names s of
SOME n =>
- let
- val (dataT, res_T) = nth_range_type n T
- |> pairf domain_type range_type
- in
- (optimized_case_def hol_ctxt dataT res_T
- |> do_term (depth + 1) Ts, ts)
- end
+ if length ts < n then
+ (do_term depth Ts (eta_expand Ts t (n - length ts)), [])
+ else
+ let
+ val (dataT, res_T) = nth_range_type n T
+ |> pairf domain_type range_type
+ in
+ (optimized_case_def hol_ctxt dataT res_T
+ (map (do_term depth Ts) (take n ts)),
+ drop n ts)
+ end
| _ =>
if is_constr ctxt stds x then
(Const x, ts)
@@ -1645,11 +1713,14 @@
string_of_int depth ^ ") while expanding " ^
quote s)
else if s = @{const_name wfrec'} then
- (do_term (depth + 1) Ts (betapplys (def, ts)), [])
+ (do_term (depth + 1) Ts (s_betapplys Ts (def, ts)), [])
else
(do_term (depth + 1) Ts def, ts)
| NONE => (Const x, ts)
- in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end
+ in
+ s_betapplys Ts (const, map (do_term depth Ts) ts)
+ |> s_beta_norm Ts
+ end
in do_term 0 [] end
(** Axiom extraction/generation **)
@@ -1796,8 +1867,9 @@
in
[HOLogic.eq_const bool_T $ (bisim_const $ n_var $ x_var $ y_var)
$ (@{term "op |"} $ (HOLogic.eq_const iter_T $ n_var $ zero_const iter_T)
- $ (betapplys (optimized_case_def hol_ctxt T bool_T,
- map case_func xs @ [x_var]))),
+ $ (s_betapply []
+ (optimized_case_def hol_ctxt T bool_T (map case_func xs),
+ x_var))),
HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
$ (Const (@{const_name insert}, T --> set_T --> set_T)
$ x_var $ Const (@{const_name bot_class.bot}, set_T))]
@@ -2036,11 +2108,12 @@
val outer_bounds = map Bound (length outer - 1 downto 0)
val cur = Var ((iter_var_prefix, j + 1), iter_T)
val next = suc_const iter_T $ cur
- val rhs = case fp_app of
- Const _ $ t =>
- betapply (t, list_comb (Const x', next :: outer_bounds))
- | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_\
- \const", [fp_app])
+ val rhs =
+ case fp_app of
+ Const _ $ t =>
+ s_betapply [] (t, list_comb (Const x', next :: outer_bounds))
+ | _ => raise TERM ("Nitpick_HOL.unrolled_inductive_pred_const",
+ [fp_app])
val (inner, naked_rhs) = strip_abs rhs
val all = outer @ inner
val bounds = map Bound (length all - 1 downto 0)
@@ -2056,10 +2129,10 @@
val def = the (def_of_const thy def_table x)
val (outer, fp_app) = strip_abs def
val outer_bounds = map Bound (length outer - 1 downto 0)
- val rhs = case fp_app of
- Const _ $ t => betapply (t, list_comb (Const x, outer_bounds))
- | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom",
- [fp_app])
+ val rhs =
+ case fp_app of
+ Const _ $ t => s_betapply [] (t, list_comb (Const x, outer_bounds))
+ | _ => raise TERM ("Nitpick_HOL.raw_inductive_pred_axiom", [fp_app])
val (inner, naked_rhs) = strip_abs rhs
val all = outer @ inner
val bounds = map Bound (length all - 1 downto 0)
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Jun 21 09:38:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Jun 21 11:15:21 2010 +0200
@@ -866,24 +866,8 @@
| _ => kk_rel_eq r (KK.Atom (j0 + 1))
val formula_from_atom = formula_from_opt_atom Pos
- fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
- val kk_or3 =
- double_rel_rel_let kk
- (fn r1 => fn r2 =>
- kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom
- (kk_intersect r1 r2))
- val kk_and3 =
- double_rel_rel_let kk
- (fn r1 => fn r2 =>
- kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom
- (kk_intersect r1 r2))
- fun kk_notimplies3 r1 r2 = kk_and3 r1 (kk_not3 r2)
-
val unpack_formulas =
map (formula_from_atom bool_j0) oo unpack_vect_in_chunks kk 1
- fun kk_vect_set_op connective k r1 r2 =
- fold1 kk_product (map2 (atom_from_formula kk bool_j0 oo connective)
- (unpack_formulas k r1) (unpack_formulas k r2))
fun kk_vect_set_bool_op connective k r1 r2 =
fold1 kk_and (map2 connective (unpack_formulas k r1)
(unpack_formulas k r2))
@@ -1369,14 +1353,6 @@
kk_union (kk_rel_if f1 true_atom KK.None)
(kk_rel_if f2 KK.None false_atom)
end
- | Op2 (Union, _, R, u1, u2) =>
- to_set_op kk_or kk_or3 kk_union kk_union kk_intersect false R u1 u2
- | Op2 (SetDifference, _, R, u1, u2) =>
- to_set_op kk_notimplies kk_notimplies3 kk_difference kk_intersect
- kk_union true R u1 u2
- | Op2 (Intersect, _, R, u1, u2) =>
- to_set_op kk_and kk_and3 kk_intersect kk_intersect kk_union false R
- u1 u2
| Op2 (Composition, _, R, u1, u2) =>
let
val (a_T, b_T) = HOLogic.dest_prodT (domain_type (type_of u1))
@@ -1644,37 +1620,6 @@
(kk_join r2 true_atom)
| _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
end
- and to_set_op connective connective3 set_oper true_set_oper false_set_oper
- neg_second R u1 u2 =
- let
- val min_R = min_rep (rep_of u1) (rep_of u2)
- val r1 = to_rep min_R u1
- val r2 = to_rep min_R u2
- val unopt_R = unopt_rep R
- in
- rel_expr_from_rel_expr kk unopt_R (unopt_rep min_R)
- (case min_R of
- Opt (Vect (k, Atom _)) => kk_vect_set_op connective k r1 r2
- | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2
- | Func (_, Formula Neut) => set_oper r1 r2
- | Func (Unit, _) => connective3 r1 r2
- | Func _ =>
- double_rel_rel_let kk
- (fn r1 => fn r2 =>
- kk_union
- (kk_product
- (true_set_oper (kk_join r1 true_atom)
- (kk_join r2 (atom_for_bool bool_j0
- (not neg_second))))
- true_atom)
- (kk_product
- (false_set_oper (kk_join r1 false_atom)
- (kk_join r2 (atom_for_bool bool_j0
- neg_second)))
- false_atom))
- r1 r2
- | _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
- end
and to_bit_word_unary_op T R oper =
let
val Ts = strip_type T ||> single |> op @
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Jun 21 09:38:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Jun 21 11:15:21 2010 +0200
@@ -54,8 +54,9 @@
exception MTYPE of string * mtyp list * typ list
exception MTERM of string * mterm list
-fun print_g (_ : string) = ()
-(* val print_g = tracing *)
+val debug_mono = false
+
+fun print_g f = () |> debug_mono ? tracing o f
val string_for_var = signed_string_of_int
fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
@@ -401,10 +402,10 @@
[M1, M2], [])
fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
- (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
- " " ^ string_for_mtype M2);
+ (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
+ string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
- NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
+ NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
| SOME (lits, comps) => (lits, comps, sexps))
val add_mtypes_equal = add_mtype_comp Eq
@@ -446,10 +447,11 @@
raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
- (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
- (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
+ (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
+ (case sn of Minus => "concrete" | Plus => "complete") ^
+ ".");
case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
- NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
+ NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
| SOME (lits, sexps) => (lits, comps, sexps))
val add_mtype_is_concrete = add_notin_mtype_fv Minus
@@ -491,15 +493,16 @@
subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
fun print_problem lits comps sexps =
- print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
- map string_for_comp comps @
- map string_for_sign_expr sexps))
+ print_g (fn () => "*** Problem:\n" ^
+ cat_lines (map string_for_literal lits @
+ map string_for_comp comps @
+ map string_for_sign_expr sexps))
fun print_solution lits =
let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
- print_g ("*** Solution:\n" ^
- "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
- "-: " ^ commas (map (string_for_var o fst) neg))
+ print_g (fn () => "*** Solution:\n" ^
+ "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
+ "-: " ^ commas (map (string_for_var o fst) neg))
end
fun solve max_var (lits, comps, sexps) =
@@ -550,6 +553,12 @@
def_table, ...},
alpha_T, max_fresh, ...}) =
let
+ fun is_enough_eta_expanded t =
+ case strip_comb t of
+ (Const x, ts) =>
+ the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
+ <= length ts
+ | _ => true
val mtype_for = fresh_mtype_for_type mdata false
fun plus_set_mtype_for_dom M =
MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
@@ -640,8 +649,10 @@
|>> mtype_of_mterm
end
| @{const_name "op ="} => do_equals T accum
- | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ())
- | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ())
+ | @{const_name The} =>
+ (print_g (K "*** The"); raise UNSOLVABLE ())
+ | @{const_name Eps} =>
+ (print_g (K "*** Eps"); raise UNSOLVABLE ())
| @{const_name If} =>
do_robust_set_operation (range_type T) accum
|>> curry3 MFun bool_M (S Minus)
@@ -650,19 +661,6 @@
| @{const_name snd} => do_nth_pair_sel 1 T accum
| @{const_name Id} =>
(MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
- | @{const_name insert} =>
- let
- val set_T = domain_type (range_type T)
- val M1 = mtype_for (domain_type set_T)
- val M1' = plus_set_mtype_for_dom M1
- val M2 = mtype_for set_T
- val M3 = mtype_for set_T
- in
- (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
- (gamma, cset |> add_mtype_is_concrete M1
- |> add_is_sub_mtype M1' M3
- |> add_is_sub_mtype M2 M3))
- end
| @{const_name converse} =>
let
val x = Unsynchronized.inc max_fresh
@@ -720,25 +718,9 @@
val a_set_M = mtype_for (domain_type T)
val a_M = dest_MFun a_set_M |> #1
in (MFun (a_set_M, S Minus, a_M), accum) end
- else if s = @{const_name minus_class.minus} andalso
- is_set_type (domain_type T) then
- let
- val set_T = domain_type T
- val left_set_M = mtype_for set_T
- val right_set_M = mtype_for set_T
- in
- (MFun (left_set_M, S Minus,
- MFun (right_set_M, S Minus, left_set_M)),
- (gamma, cset |> add_mtype_is_concrete right_set_M
- |> add_is_sub_mtype right_set_M left_set_M))
- end
else if s = @{const_name ord_class.less_eq} andalso
is_set_type (domain_type T) then
do_fragile_set_operation T accum
- else if (s = @{const_name semilattice_inf_class.inf} orelse
- s = @{const_name semilattice_sup_class.sup}) andalso
- is_set_type (domain_type T) then
- do_robust_set_operation T accum
else if is_sel s then
(mtype_for_sel mdata x, accum)
else if is_constr ctxt stds x then
@@ -758,7 +740,7 @@
(M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
frees = (x, M) :: frees, consts = consts}, cset))
end) |>> curry MRaw t
- | Var _ => (print_g "*** Var"; raise UNSOLVABLE ())
+ | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ())
| Bound j => (MRaw (t, nth bound_Ms j), accum)
| Abs (s, T, t') =>
(case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
@@ -771,10 +753,16 @@
| NONE =>
((case t' of
t1' $ Bound 0 =>
- if not (loose_bvar1 (t1', 0)) then
+ if not (loose_bvar1 (t1', 0)) andalso
+ is_enough_eta_expanded t1' then
do_term (incr_boundvars ~1 t1') accum
else
raise SAME ()
+ | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
+ if not (loose_bvar1 (t13, 0)) then
+ do_term (incr_boundvars ~1 (t11 $ t13)) accum
+ else
+ raise SAME ()
| _ => raise SAME ())
handle SAME () =>
let
@@ -803,8 +791,8 @@
val M2 = mtype_of_mterm m2
in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
end)
- |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^
- string_for_mterm ctxt m))
+ |> tap (fn (m, _) => print_g (fn () => " \<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m))
in do_term end
fun force_minus_funs 0 _ = I
@@ -902,9 +890,9 @@
| _ => do_term t accum
end
|> tap (fn (m, _) =>
- print_g ("\<Gamma> \<turnstile> " ^
- string_for_mterm ctxt m ^ " : o\<^sup>" ^
- string_for_sign sn))
+ print_g (fn () => "\<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m ^ " : o\<^sup>" ^
+ string_for_sign sn))
in do_formula end
(* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -987,9 +975,10 @@
Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
- map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
- map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
- |> cat_lines |> print_g
+ print_g (fn () =>
+ map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
+ map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
+ |> cat_lines)
fun amass f t (ms, accum) =
let val (m, accum) = f t accum in (m :: ms, accum) end
@@ -997,9 +986,9 @@
fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
(nondef_ts, def_ts) =
let
- val _ = print_g ("****** " ^ which ^ " analysis: " ^
- string_for_mtype MAlpha ^ " is " ^
- Syntax.string_of_typ ctxt alpha_T)
+ val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^
+ string_for_mtype MAlpha ^ " is " ^
+ Syntax.string_of_typ ctxt alpha_T)
val mdata as {max_fresh, constr_mcache, ...} =
initial_mdata hol_ctxt binarize no_harmless alpha_T
val accum = (initial_gamma, ([], [], []))
@@ -1064,26 +1053,21 @@
in
case t of
Const (x as (s, _)) =>
- if s = @{const_name insert} then
- case nth_range_type 2 T' of
- set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
- Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
- Const (@{const_name If},
- bool_T --> set_T' --> set_T' --> set_T')
- $ (Const (@{const_name is_unknown},
- elem_T' --> bool_T) $ Bound 1)
- $ (Const (@{const_name unknown}, set_T'))
- $ (coerce_term hol_ctxt new_Ts T' T (Const x)
- $ Bound 1 $ Bound 0)))
- | _ => Const (s, T')
- else if s = @{const_name finite} then
+ if s = @{const_name finite} then
case domain_type T' of
set_T' as Type (@{type_name fin_fun}, _) =>
Abs (Name.uu, set_T', @{const True})
| _ => Const (s, T')
else if s = @{const_name "=="} orelse
s = @{const_name "op ="} then
- Const (s, T')
+ let
+ val T =
+ case T' of
+ Type (_, [T1, Type (_, [T2, T3])]) =>
+ T1 --> T2 --> T3
+ | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
+ \term_from_mterm", [T, T'], [])
+ in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
else if is_built_in_const thy stds fast_descrs x then
coerce_term hol_ctxt new_Ts T' T t
else if is_constr ctxt stds x then
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 09:38:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 11:15:21 2010 +0200
@@ -56,9 +56,6 @@
The |
Eps |
Triad |
- Union |
- SetDifference |
- Intersect |
Composition |
Product |
Image |
@@ -176,9 +173,6 @@
The |
Eps |
Triad |
- Union |
- SetDifference |
- Intersect |
Composition |
Product |
Image |
@@ -247,9 +241,6 @@
| string_for_op2 The = "The"
| string_for_op2 Eps = "Eps"
| string_for_op2 Triad = "Triad"
- | string_for_op2 Union = "Union"
- | string_for_op2 SetDifference = "SetDifference"
- | string_for_op2 Intersect = "Intersect"
| string_for_op2 Composition = "Composition"
| string_for_op2 Product = "Product"
| string_for_op2 Image = "Image"
@@ -525,6 +516,8 @@
do_description_operator The @{const_name undefined_fast_The} x t1
| (Const (x as (@{const_name Eps}, _)), [t1]) =>
do_description_operator Eps @{const_name undefined_fast_Eps} x t1
+ | (Const (@{const_name "op ="}, T), [t1]) =>
+ Op1 (SingletonSet, range_type T, Any, sub t1)
| (Const (@{const_name "op ="}, T), [t1, t2]) => sub_equals T t1 t2
| (Const (@{const_name "op &"}, _), [t1, t2]) =>
Op2 (And, bool_T, Any, sub' t1, sub' t2)
@@ -547,13 +540,6 @@
| (Const (@{const_name snd}, T), [t1]) =>
Op1 (Second, range_type T, Any, sub t1)
| (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
- | (Const (@{const_name insert}, T), [t1, t2]) =>
- (case t2 of
- Abs (_, _, @{const False}) =>
- Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1)
- | _ =>
- Op2 (Union, nth_range_type 2 T, Any,
- Op1 (SingletonSet, nth_range_type 2 T, Any, sub t1), sub t2))
| (Const (@{const_name converse}, T), [t1]) =>
Op1 (Converse, range_type T, Any, sub t1)
| (Const (@{const_name trancl}, T), [t1]) =>
@@ -585,11 +571,6 @@
| (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Add, T, Any)
else ConstName (s, T, Any)
- | (Const (@{const_name minus_class.minus},
- Type (@{type_name fun},
- [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
- [t1, t2]) =>
- Op2 (SetDifference, T1, Any, sub t1, sub t2)
| (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
else ConstName (s, T, Any)
@@ -643,16 +624,6 @@
| (Const (@{const_name of_nat},
T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
Cst (NatToInt, T, Any)
- | (Const (@{const_name semilattice_inf_class.inf},
- Type (@{type_name fun},
- [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
- [t1, t2]) =>
- Op2 (Intersect, T1, Any, sub t1, sub t2)
- | (Const (@{const_name semilattice_sup_class.sup},
- Type (@{type_name fun},
- [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
- [t1, t2]) =>
- Op2 (Union, T1, Any, sub t1, sub t2)
| (t0 as Const (x as (s, T)), ts) =>
if is_constr ctxt stds x then
do_construct x ts
@@ -685,15 +656,14 @@
| Op1 (SingletonSet, _, _, _) => true
| Op1 (Converse, _, _, u1) => is_fully_representable_set u1
| Op2 (oper, _, _, u1, u2) =>
- if oper = Union orelse oper = SetDifference orelse oper = Intersect then
- forall is_fully_representable_set [u1, u2]
- else if oper = Apply then
+ if oper = Apply then
case u1 of
ConstName (s, _, _) =>
is_sel_like_and_no_discr s orelse s = @{const_name set}
| _ => false
else
false
+ | Op2 (Lambda, _, _, _, Cst (False, _, _)) => true
| _ => false
fun rep_for_abs_fun scope T =
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 21 09:38:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Jun 21 11:15:21 2010 +0200
@@ -91,7 +91,7 @@
fun uncurry_term table t =
let
fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
- | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
+ | aux (Abs (s, T, t')) args = s_betapplys [] (Abs (s, T, aux t' []), args)
| aux (t as Const (s, T)) args =
(case Termtab.lookup table t of
SOME n =>
@@ -111,17 +111,18 @@
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
in
if n - j < 2 then
- betapplys (t, args)
+ s_betapplys [] (t, args)
else
- betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
- before_arg_Ts ---> tuple_T --> rest_T),
- before_args @ [mk_flat_tuple tuple_T tuple_args] @
- after_args)
+ s_betapplys []
+ (Const (uncurry_prefix_for (n - j) j ^ s,
+ before_arg_Ts ---> tuple_T --> rest_T),
+ before_args @ [mk_flat_tuple tuple_T tuple_args] @
+ after_args)
end
else
- betapplys (t, args)
- | NONE => betapplys (t, args))
- | aux t args = betapplys (t, args)
+ s_betapplys [] (t, args)
+ | NONE => s_betapplys [] (t, args))
+ | aux t args = s_betapplys [] (t, args)
in aux t [] end
(** Boxing **)
@@ -248,13 +249,13 @@
val T2 = fastype_of1 (new_Ts, t2)
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
- betapply (if s1 = @{type_name fun} then
- t1
- else
- select_nth_constr_arg ctxt stds
- (@{const_name FunBox},
- Type (@{type_name fun}, Ts1) --> T1) t1 0
- (Type (@{type_name fun}, Ts1)), t2)
+ s_betapply new_Ts (if s1 = @{type_name fun} then
+ t1
+ else
+ select_nth_constr_arg ctxt stds
+ (@{const_name FunBox},
+ Type (@{type_name fun}, Ts1) --> T1) t1 0
+ (Type (@{type_name fun}, Ts1)), t2)
end
| t1 $ t2 =>
let
@@ -265,13 +266,13 @@
val T2 = fastype_of1 (new_Ts, t2)
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
- betapply (if s1 = @{type_name fun} then
- t1
- else
- select_nth_constr_arg ctxt stds
- (@{const_name FunBox},
- Type (@{type_name fun}, Ts1) --> T1) t1 0
- (Type (@{type_name fun}, Ts1)), t2)
+ s_betapply new_Ts (if s1 = @{type_name fun} then
+ t1
+ else
+ select_nth_constr_arg ctxt stds
+ (@{const_name FunBox},
+ Type (@{type_name fun}, Ts1) --> T1) t1 0
+ (Type (@{type_name fun}, Ts1)), t2)
end
| Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
| Var (z as (x, T)) =>
@@ -388,18 +389,6 @@
(list_comb (t, args), seen)
in aux [] 0 t [] [] |> fst end
-val let_var_prefix = nitpick_prefix ^ "l"
-val let_inline_threshold = 32
-
-fun hol_let n abs_T body_T f t =
- if n * size_of_term t <= let_inline_threshold then
- f t
- else
- let val z = ((let_var_prefix, 0), abs_T) in
- Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
- $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
- end
-
fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
let
val num_occs_of_var =
@@ -439,10 +428,10 @@
x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- hol_let (n + 1) dataT bool_T
- (fn t1 => discriminate_value hol_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
- |> foldr1 s_conj) t1
+ s_let "l" (n + 1) dataT bool_T
+ (fn t1 => discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
+ |> foldr1 s_conj) t1
else
raise SAME ()
end
@@ -572,7 +561,7 @@
map Bound (rev js))
val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
in
- if null js then betapply (abs_t, sko_t)
+ if null js then s_betapply Ts (abs_t, sko_t)
else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
end
else
@@ -602,11 +591,9 @@
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
do_quantifier s0 T0 s1 T1 t1
| @{const "op &"} $ t1 $ t2 =>
- @{const "op &"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
+ s_conj (pairself (aux ss Ts js depth polar) (t1, t2))
| @{const "op |"} $ t1 $ t2 =>
- @{const "op |"} $ aux ss Ts js depth polar t1
- $ aux ss Ts js depth polar t2
+ s_disj (pairself (aux ss Ts js depth polar) (t1, t2))
| @{const "op -->"} $ t1 $ t2 =>
@{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
$ aux ss Ts js depth polar t2
@@ -617,42 +604,30 @@
not (is_well_founded_inductive_pred hol_ctxt x) then
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val (pref, connective, set_oper) =
- if gfp then
- (lbfp_prefix, @{const "op |"},
- @{const_name semilattice_sup_class.sup})
- else
- (ubfp_prefix, @{const "op &"},
- @{const_name semilattice_inf_class.inf})
+ val (pref, connective) =
+ if gfp then (lbfp_prefix, @{const "op |"})
+ else (ubfp_prefix, @{const "op &"})
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
|> aux ss Ts js depth polar
fun neg () = Const (pref ^ s, T)
in
- (case polar |> gfp ? flip_polarity of
- Pos => pos ()
- | Neg => neg ()
- | Neut =>
- if is_fun_type T then
- let
- val ((trunk_arg_Ts, rump_arg_T), body_T) =
- T |> strip_type |>> split_last
- val set_T = rump_arg_T --> body_T
- fun app f =
- list_comb (f (),
- map Bound (length trunk_arg_Ts - 1 downto 0))
- in
- List.foldr absdummy
- (Const (set_oper, set_T --> set_T --> set_T)
- $ app pos $ app neg) trunk_arg_Ts
- end
- else
- connective $ pos () $ neg ())
+ case polar |> gfp ? flip_polarity of
+ Pos => pos ()
+ | Neg => neg ()
+ | Neut =>
+ let
+ val arg_Ts = binder_types T
+ fun app f =
+ list_comb (f (), map Bound (length arg_Ts - 1 downto 0))
+ in
+ List.foldr absdummy (connective $ app pos $ app neg) arg_Ts
+ end
end
else
Const x
| t1 $ t2 =>
- betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
- aux ss Ts [] depth Neut t2)
+ s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1,
+ aux ss Ts [] depth Neut t2)
| Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
| _ => t
end
@@ -1064,10 +1039,10 @@
| _ => raise SAME ()
else
raise SAME ())
- handle SAME () => betapplys (t, args))
+ handle SAME () => s_betapplys [] (t, args))
| do_term (Abs (s, T, t')) args =
- betapplys (Abs (s, T, do_term t' []), args)
- | do_term t args = betapplys (t, args)
+ s_betapplys [] (Abs (s, T, do_term t' []), args)
+ | do_term t args = s_betapplys [] (t, args)
in do_term t [] end
(** Quantifier massaging: Distributing quantifiers **)
@@ -1223,15 +1198,20 @@
fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
(nondef_ts, def_ts) =
- let
- val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
- |> filter_out (fn Type (@{type_name fun_box}, _) => true
- | @{typ signed_bit} => true
- | @{typ unsigned_bit} => true
- | T => is_small_finite_type hol_ctxt T orelse
- triple_lookup (type_match thy) monos T
- = SOME (SOME false))
- in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
+ if forall (curry (op =) (SOME false) o snd) finitizes then
+ (nondef_ts, def_ts)
+ else
+ let
+ val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
+ |> filter_out (fn Type (@{type_name fun_box}, _) => true
+ | @{typ signed_bit} => true
+ | @{typ unsigned_bit} => true
+ | T => is_small_finite_type hol_ctxt T orelse
+ triple_lookup (type_match thy) monos T
+ = SOME (SOME false))
+ in
+ fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
+ end
(** Preprocessor entry point **)