four changes to Nitpick:
1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems
2. do eta-contraction in the monotonicity check
3. improved quantifier massaging algorithms using ideas from Paradox
4. repaired "check_potential" and "check_genuine"
--- a/doc-src/Nitpick/nitpick.tex Tue Feb 02 23:38:41 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Thu Feb 04 13:36:52 2010 +0100
@@ -1888,7 +1888,9 @@
Specifies whether Nitpick should put its temporary files in
\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER}, which is useful for
debugging Nitpick but also unsafe if several instances of the tool are run
-simultaneously.
+simultaneously. The files are identified by the extensions
+\texttt{.kki}, \texttt{.cnf}, \texttt{.out}, and
+\texttt{.err}; you may safely remove them after Nitpick has run.
\nopagebreak
{\small See also \textit{debug} (\S\ref{output-format}).}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Feb 04 13:36:52 2010 +0100
@@ -505,6 +505,19 @@
filter (is_relevant_setting o fst) (#settings p1)
= filter (is_relevant_setting o fst) (#settings p2)
+val created_temp_dir = Unsynchronized.ref false
+
+(* bool -> string * string *)
+fun serial_string_and_temporary_dir_for_overlord overlord =
+ if overlord then
+ ("", getenv "ISABELLE_HOME_USER")
+ else
+ let
+ val dir = getenv "ISABELLE_TMP"
+ val _ = if !created_temp_dir then ()
+ else (created_temp_dir := true; File.mkdir (Path.explode dir))
+ in (serial_string (), dir) end
+
(* int -> string *)
fun base_name j =
if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
@@ -1012,20 +1025,17 @@
Normal ([], triv_js)
else
let
- val (serial_str, tmp_path) =
- if overlord then
- ("", Path.append (Path.variable "ISABELLE_HOME_USER") o Path.base)
- else
- (serial_string (), File.tmp_path)
- (* string -> string -> Path.T *)
- fun path_for base suf =
- tmp_path (Path.explode (base ^ serial_str ^ "." ^ suf))
- val in_path = path_for "isabelle" "kki"
+ val (serial_str, temp_dir) =
+ serial_string_and_temporary_dir_for_overlord overlord
+ (* string -> Path.T *)
+ fun path_for suf =
+ Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
+ val in_path = path_for "kki"
val in_buf = Unsynchronized.ref Buffer.empty
(* string -> unit *)
fun out s = Unsynchronized.change in_buf (Buffer.add s)
- val out_path = path_for "kodkodi" "out"
- val err_path = path_for "kodkodi" "err"
+ val out_path = path_for "out"
+ val err_path = path_for "err"
val _ = write_problem_file out (map snd indexed_problems)
val _ = File.write_buffer in_path (!in_buf)
(* unit -> unit *)
@@ -1043,7 +1053,8 @@
val outcome =
let
val code =
- system ("env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
+ system ("cd " ^ temp_dir ^ ";\n" ^
+ "env CLASSPATH=\"$KODKODI_CLASSPATH:$CLASSPATH\" \
\JAVA_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
\$JAVA_LIBRARY_PATH\" \
\LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Thu Feb 04 13:36:52 2010 +0100
@@ -9,12 +9,14 @@
sig
val configured_sat_solvers : bool -> string list
val smart_sat_solver_name : bool -> string
- val sat_solver_spec : string -> string * string list
+ val sat_solver_spec : bool -> string -> string * string list
end;
structure Kodkod_SAT : KODKOD_SAT =
struct
+open Kodkod
+
datatype sink = ToStdout | ToFile
datatype availability = Java | JNI
datatype mode = Batch | Incremental
@@ -49,34 +51,34 @@
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
-val created_temp_dir = Unsynchronized.ref false
-
-(* string -> sink -> string -> string -> string list -> string list
+(* bool -> string -> sink -> string -> string -> string list -> string list
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_external name dev home exec args markers =
+fun dynamic_entry_for_external overlord name dev home exec args markers =
case getenv home of
"" => NONE
- | dir => SOME (name, fn () =>
- let
- val temp_dir = getenv "ISABELLE_TMP"
- val _ = if !created_temp_dir then
- ()
- else
- (created_temp_dir := true;
- File.mkdir (Path.explode temp_dir))
- val temp = temp_dir ^ "/" ^ name ^ serial_string ()
- val out_file = temp ^ ".out"
- in
- [if null markers then "External" else "ExternalV2",
- dir ^ "/" ^ exec, temp ^ ".cnf",
- if dev = ToFile then out_file else ""] @ markers @
- (if dev = ToFile then [out_file] else []) @ args
- end)
-(* bool -> string * sat_solver_info
+ | dir =>
+ SOME (name, fn () =>
+ let
+ val serial_str = if overlord then "" else serial_string ()
+ val base = name ^ serial_str
+ val out_file = base ^ ".out"
+ val dir_sep =
+ if String.isSubstring "\\" dir andalso
+ not (String.isSubstring "/" dir) then
+ "\\"
+ else
+ "/"
+ in
+ [if null markers then "External" else "ExternalV2",
+ dir ^ dir_sep ^ exec, base ^ ".cnf",
+ if dev = ToFile then out_file else ""] @ markers @
+ (if dev = ToFile then [out_file] else []) @ args
+ end)
+(* bool -> bool -> string * sat_solver_info
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
+fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
- | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
+ | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) =
if incremental andalso mode = Batch then
NONE
else
@@ -90,33 +92,36 @@
else
NONE
end
- | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
- dynamic_entry_for_external name dev home exec args []
- | dynamic_entry_for_info false (name, ExternalV2 (dev, home, exec, args,
- m1, m2, m3)) =
- dynamic_entry_for_external name dev home exec args [m1, m2, m3]
- | dynamic_entry_for_info true _ = NONE
-(* bool -> (string * (unit -> string list)) list *)
-fun dynamic_list incremental =
- map_filter (dynamic_entry_for_info incremental) static_list
+ | dynamic_entry_for_info overlord false
+ (name, External (dev, home, exec, args)) =
+ dynamic_entry_for_external overlord name dev home exec args []
+ | dynamic_entry_for_info overlord false
+ (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
+ dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3]
+ | dynamic_entry_for_info _ true _ = NONE
+(* bool -> bool -> (string * (unit -> string list)) list *)
+fun dynamic_list overlord incremental =
+ map_filter (dynamic_entry_for_info overlord incremental) static_list
(* bool -> string list *)
-val configured_sat_solvers = map fst o dynamic_list
-
+val configured_sat_solvers = map fst o dynamic_list false
(* bool -> string *)
-val smart_sat_solver_name = dynamic_list #> hd #> fst
+val smart_sat_solver_name = fst o hd o dynamic_list false
-(* (string * 'a) list -> string *)
-fun enum_solvers xs = commas (map (quote o fst) xs |> distinct (op =))
-(* string -> string * string list *)
-fun sat_solver_spec name =
- let val dynamic_list = dynamic_list false in
- (name, the (AList.lookup (op =) dynamic_list name) ())
+(* bool -> string -> string * string list *)
+fun sat_solver_spec overlord name =
+ let
+ val dyn_list = dynamic_list overlord false
+ (* (string * 'a) list -> string *)
+ fun enum_solvers solvers =
+ commas (distinct (op =) (map (quote o fst) solvers))
+ in
+ (name, the (AList.lookup (op =) dyn_list name) ())
handle Option.Option =>
error (if AList.defined (op =) static_list name then
"The SAT solver " ^ quote name ^ " is not configured. The \
\following solvers are configured:\n" ^
- enum_solvers dynamic_list ^ "."
+ enum_solvers dyn_list ^ "."
else
"Unknown SAT solver " ^ quote name ^ ". The following \
\solvers are supported:\n" ^ enum_solvers static_list ^ ".")
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 04 13:36:52 2010 +0100
@@ -502,8 +502,8 @@
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
PrintMode.setmp [] multiline_string_for_scope scope
- val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
- |> snd
+ val kodkod_sat_solver =
+ Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
val bit_width = if bits = 0 then 16 else bits + 1
val delay = if liberal then
Option.map (fn time => Time.- (time, Time.now ()))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Feb 04 13:36:52 2010 +0100
@@ -51,6 +51,7 @@
val skolem_prefix : string
val eval_prefix : string
val original_name : string -> string
+ val s_conj : term * term -> term
val unbit_and_unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
@@ -204,36 +205,6 @@
{frac_types = AList.merge (op =) (K true) (fs1, fs2),
codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
-(* term * term -> term *)
-fun s_conj (t1, @{const True}) = t1
- | s_conj (@{const True}, t2) = t2
- | s_conj (t1, t2) =
- if t1 = @{const False} orelse t2 = @{const False} then @{const False}
- else HOLogic.mk_conj (t1, t2)
-fun s_disj (t1, @{const False}) = t1
- | s_disj (@{const False}, t2) = t2
- | s_disj (t1, t2) =
- if t1 = @{const True} orelse t2 = @{const True} then @{const True}
- else HOLogic.mk_disj (t1, t2)
-(* term -> term -> term *)
-fun mk_exists v t =
- HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
-
-(* term -> term -> term list *)
-fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
- if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
- | strip_connective _ t = [t]
-(* term -> term list * term *)
-fun strip_any_connective (t as (t0 $ t1 $ t2)) =
- if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
- (strip_connective t0 t, t0)
- else
- ([t], @{const Not})
- | strip_any_connective t = ([t], @{const Not})
-(* term -> term list *)
-val conjuncts = strip_connective @{const "op &"}
-val disjuncts = strip_connective @{const "op |"}
-
val name_sep = "$"
val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
val sel_prefix = nitpick_prefix ^ "sel"
@@ -278,6 +249,36 @@
s
val after_name_sep = snd o strip_first_name_sep
+(* term * term -> term *)
+fun s_conj (t1, @{const True}) = t1
+ | s_conj (@{const True}, t2) = t2
+ | s_conj (t1, t2) =
+ if t1 = @{const False} orelse t2 = @{const False} then @{const False}
+ else HOLogic.mk_conj (t1, t2)
+fun s_disj (t1, @{const False}) = t1
+ | s_disj (@{const False}, t2) = t2
+ | s_disj (t1, t2) =
+ if t1 = @{const True} orelse t2 = @{const True} then @{const True}
+ else HOLogic.mk_disj (t1, t2)
+(* term -> term -> term *)
+fun mk_exists v t =
+ HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
+
+(* term -> term -> term list *)
+fun strip_connective conn_t (t as (t0 $ t1 $ t2)) =
+ if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
+ | strip_connective _ t = [t]
+(* term -> term list * term *)
+fun strip_any_connective (t as (t0 $ t1 $ t2)) =
+ if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
+ (strip_connective t0 t, t0)
+ else
+ ([t], @{const Not})
+ | strip_any_connective t = ([t], @{const Not})
+(* term -> term list *)
+val conjuncts = strip_connective @{const "op &"}
+val disjuncts = strip_connective @{const "op |"}
+
(* When you add constants to these lists, make sure to handle them in
"Nitpick_Nut.nut_from_term", and perhaps in "Nitpick_Mono.consider_term" as
well. *)
@@ -551,6 +552,7 @@
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
+ | is_quot_type _ (Type ("FSet.fset", _)) = true (* FIXME *)
| is_quot_type _ _ = false
fun is_codatatype thy (T as Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
@@ -618,8 +620,10 @@
| is_rep_fun _ _ = false
(* Proof.context -> styp -> bool *)
fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* FIXME *)
+ | is_quot_abs_fun _ ("FSet.abs_fset", _) = true (* FIXME *)
| is_quot_abs_fun _ _ = false
fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* FIXME *)
+ | is_quot_rep_fun _ ("FSet.rep_fset", _) = true (* FIXME *)
| is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
@@ -630,11 +634,17 @@
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
(* theory -> typ -> typ *)
fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
+ | rep_type_for_quot_type _ (Type ("FSet.fset", [T])) =
+ Type (@{type_name list}, [T])
| rep_type_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
(* theory -> typ -> term *)
fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
+ | equiv_relation_for_quot_type _ (Type ("FSet.fset", [T])) =
+ Const ("FSet.list_eq",
+ Type (@{type_name list}, [T]) --> Type (@{type_name list}, [T])
+ --> bool_T)
| equiv_relation_for_quot_type _ T =
raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
@@ -2396,7 +2406,7 @@
Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
| _ => t
-val quantifier_cluster_max_size = 8
+val quantifier_cluster_threshold = 7
(* theory -> term -> term *)
fun push_quantifiers_inward thy =
@@ -2405,7 +2415,7 @@
fun aux quant_s ss Ts t =
(case t of
(t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
- if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
+ if s0 = quant_s then
aux s0 (s1 :: ss) (T1 :: Ts) t1
else if quant_s = "" andalso
(s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
@@ -2432,22 +2442,43 @@
(* int -> int *)
val flip = curry (op -) (num_Ts - 1)
val t_boundss = map (map flip o loose_bnos) ts
- (* (int list * int) list -> int list -> int *)
- fun cost boundss_cum_costs [] =
- map snd boundss_cum_costs |> Integer.sum
- | cost boundss_cum_costs (j :: js) =
+ (* (int list * int) list -> int list
+ -> (int list * int) list *)
+ fun merge costly_boundss [] = costly_boundss
+ | merge costly_boundss (j :: js) =
let
val (yeas, nays) =
List.partition (fn (bounds, _) =>
member (op =) bounds j)
- boundss_cum_costs
+ costly_boundss
val yeas_bounds = big_union fst yeas
val yeas_cost = Integer.sum (map snd yeas)
* nth T_costs j
- in cost ((yeas_bounds, yeas_cost) :: nays) js end
- val js = all_permutations (index_seq 0 num_Ts)
- |> map (`(cost (t_boundss ~~ t_costs)))
- |> sort (int_ord o pairself fst) |> hd |> snd
+ in merge ((yeas_bounds, yeas_cost) :: nays) js end
+ (* (int list * int) list -> int list -> int *)
+ val cost = Integer.sum o map snd oo merge
+ (* Inspired by Claessen & Sörensson's polynomial binary
+ splitting heuristic (p. 5 of their MODEL 2003 paper). *)
+ (* (int list * int) list -> int list -> int list *)
+ fun heuristically_best_permutation _ [] = []
+ | heuristically_best_permutation costly_boundss js =
+ let
+ val (costly_boundss, (j, js)) =
+ js |> map (`(merge costly_boundss o single))
+ |> sort (int_ord
+ o pairself (Integer.sum o map snd o fst))
+ |> split_list |>> hd ||> pairf hd tl
+ in
+ j :: heuristically_best_permutation costly_boundss js
+ end
+ val js =
+ if length Ts <= quantifier_cluster_threshold then
+ all_permutations (index_seq 0 num_Ts)
+ |> map (`(cost (t_boundss ~~ t_costs)))
+ |> sort (int_ord o pairself fst) |> hd |> snd
+ else
+ heuristically_best_permutation (t_boundss ~~ t_costs)
+ (index_seq 0 num_Ts)
val back_js = map (fn j => find_index (curry (op =) j) js)
(index_seq 0 num_Ts)
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
@@ -3515,7 +3546,6 @@
#> simplify_constrs_and_sels thy
#> distribute_quantifiers
#> push_quantifiers_inward thy
- #> Envir.eta_contract
#> not core ? Refute.close_form
#> shorten_abs_vars
in
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Feb 04 13:36:52 2010 +0100
@@ -232,7 +232,8 @@
if T = T' then t
else raise TYPE ("Nitpick_Model.typecast_fun.do_term", [T, T'], [])
in if T1' = T1 andalso T2' = T2 then t else do_fun T1' T2' T1 T2 t end
- | typecast_fun T' _ _ _ = raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
+ | typecast_fun T' _ _ _ =
+ raise TYPE ("Nitpick_Model.typecast_fun", [T'], [])
(* term -> string *)
fun truth_const_sort_key @{const True} = "0"
@@ -341,7 +342,7 @@
(* bool -> typ -> typ -> typ -> term list -> term list -> term *)
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
- |> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
+ |> make_plain_fun maybe_opt T1 T2
|> unbit_and_unbox_term
|> typecast_fun (unbit_and_unbox_type T')
(unbit_and_unbox_type T1)
@@ -523,7 +524,7 @@
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
in
- (not for_auto ? polish_funs []) o unbit_and_unbox_term oooo term_for_rep []
+ polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
end
(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
@@ -723,7 +724,8 @@
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
-> KK.raw_bound list -> term -> bool option *)
-fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns, ...})
+fun prove_hol_model (scope as {ext_ctxt as {thy, ctxt, debug, ...},
+ card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
let
(* typ * int -> term *)
@@ -737,25 +739,29 @@
Const (@{const_name All}, (T --> bool_T) --> bool_T)
$ Abs ("x", T, foldl1 HOLogic.mk_disj eqs)
val distinct_assm = distinctness_formula T (map atom (index_seq 0 k))
- in HOLogic.mk_conj (compreh_assm, distinct_assm) end
+ in s_conj (compreh_assm, distinct_assm) end
(* nut -> term *)
fun free_name_assm name =
HOLogic.mk_eq (Free (nickname_of name, type_of name),
term_for_name scope sel_names rel_table bounds name)
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
val model_assms = map free_name_assm free_names
- val assm = List.foldr HOLogic.mk_conj @{const True}
- (freeT_assms @ model_assms)
+ val assm = foldr1 s_conj (freeT_assms @ model_assms)
(* bool -> bool *)
fun try_out negate =
let
val concl = (negate ? curry (op $) @{const Not})
(ObjectLogic.atomize_term thy prop)
- val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
+ val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
|> map_types (map_type_tfree
- (fn (s, []) => TFree (s, HOLogic.typeS)
- | x => TFree x))
- |> cterm_of thy |> Goal.init
+ (fn (s, []) => TFree (s, HOLogic.typeS)
+ | x => TFree x))
+ val _ = if debug then
+ priority ((if negate then "Genuineness" else "Spuriousness") ^
+ " goal: " ^ Syntax.string_of_term ctxt prop ^ ".")
+ else
+ ()
+ val goal = prop |> cterm_of thy |> Goal.init
in
(goal |> SINGLE (DETERM_TIMEOUT auto_timeout
(auto_tac (clasimpset_of ctxt)))
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Feb 02 23:38:41 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 04 13:36:52 2010 +0100
@@ -766,10 +766,18 @@
| Bound j => (nth bounds j, accum)
| Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
| Abs (s, T, t') =>
- let
- val C = ctype_for T
- val (C', accum) = do_term t' (accum |>> push_bound C)
- in (CFun (C, S Minus, C'), accum |>> pop_bound) end
+ ((case t' of
+ t1' $ Bound 0 =>
+ if not (loose_bvar1 (t1', 0)) then
+ do_term (incr_boundvars ~1 t1') accum
+ else
+ raise SAME ()
+ | _ => raise SAME ())
+ handle SAME () =>
+ let
+ val C = ctype_for T
+ val (C', accum) = do_term t' (accum |>> push_bound C)
+ in (CFun (C, S Minus, C'), accum |>> pop_bound) end)
| Const (@{const_name All}, _)
$ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
do_bounded_quantifier T' t1 t2 accum