# HG changeset patch # User blanchet # Date 1265287012 -3600 # Node ID 5e492a862b344e01b46c669113eab37fa04eadd4 # Parent 7cc8726aa8a72795980d8c4f151e7c44ee8b048e 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" diff -r 7cc8726aa8a7 -r 5e492a862b34 doc-src/Nitpick/nitpick.tex --- 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}).} diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/kodkod.ML --- 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:\ diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/kodkod_sat.ML --- 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 ^ ".") diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/nitpick.ML --- 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 ())) diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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))) diff -r 7cc8726aa8a7 -r 5e492a862b34 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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