--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:33:23 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:33:51 2016 +0200
@@ -10,37 +10,39 @@
val strip_imp : term -> (term list * term)
val reflect_bool : bool -> term
val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
- -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
+ -> string -> string list -> string list -> typ list -> Proof.context -> Proof.context
val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
val register_predicate : term * string -> Context.generic -> Context.generic
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
- val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
+ val collect_results : ('a -> Quickcheck.result) -> 'a list ->
+ Quickcheck.result list -> Quickcheck.result list
type result = (bool * term list) option * Quickcheck.report option
- type generator = string * ((theory -> typ list -> bool) *
+ type generator = string * ((theory -> typ list -> bool) *
(Proof.context -> (term * term list) list -> bool -> int list -> result))
val generator_test_goal_terms :
generator -> Proof.context -> bool -> (string * typ) list
-> (term * term list) list -> Quickcheck.result list
- type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
- -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+ type instantiation =
+ Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
+ string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
val ensure_sort :
(((sort * sort) * sort) *
((theory -> string list -> Old_Datatype_Aux.descr * (string * sort) list * string list
- * string * (string list * string list) * (typ list * typ list)) * instantiation))
- -> Old_Datatype_Aux.config -> string list -> theory -> theory
- val ensure_common_sort_datatype :
- (sort * instantiation) -> Old_Datatype_Aux.config -> string list -> theory -> theory
+ * string * (string list * string list) * (typ list * typ list)) * instantiation)) ->
+ Old_Datatype_Aux.config -> string list -> theory -> theory
+ val ensure_common_sort_datatype : (sort * instantiation) -> Old_Datatype_Aux.config ->
+ string list -> theory -> theory
val datatype_interpretation : string -> sort * instantiation -> theory -> theory
val gen_mk_parametric_generator_expr :
- (((Proof.context -> term * term list -> term) * term) * typ)
- -> Proof.context -> (term * term list) list -> term
+ (((Proof.context -> term * term list -> term) * term) * typ) ->
+ Proof.context -> (term * term list) list -> term
val mk_fun_upd : typ -> typ -> term * term -> term -> term
val post_process_term : term -> term
val test_term : generator -> Proof.context -> bool -> term * term list -> Quickcheck.result
-end;
+end
structure Quickcheck_Common : QUICKCHECK_COMMON =
struct
@@ -51,27 +53,32 @@
val define_foundationally = false
+
(* HOLogic's term functions *)
-fun strip_imp (Const(@{const_name HOL.implies},_) $ A $ B) = apfst (cons A) (strip_imp B)
+fun strip_imp (Const(@{const_name HOL.implies}, _) $ A $ B) = apfst (cons A) (strip_imp B)
| strip_imp A = ([], A)
-fun reflect_bool b = if b then @{term "True"} else @{term "False"}
+fun reflect_bool b = if b then @{term True} else @{term False}
-fun mk_undefined T = Const(@{const_name undefined}, T)
+fun mk_undefined T = Const (@{const_name undefined}, T)
+
(* testing functions: testing with increasing sizes (and cardinalities) *)
type result = (bool * term list) option * Quickcheck.report option
-type generator = string * ((theory -> typ list -> bool) *
- (Proof.context -> (term * term list) list -> bool -> int list -> result))
+type generator =
+ string * ((theory -> typ list -> bool) *
+ (Proof.context -> (term * term list) list -> bool -> int list -> result))
fun check_test_term t =
let
- val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
- error "Term to be tested contains type variables";
- val _ = null (Term.add_vars t []) orelse
- error "Term to be tested contains schematic variables";
+ val _ =
+ (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
+ error "Term to be tested contains type variables"
+ val _ =
+ null (Term.add_vars t []) orelse
+ error "Term to be tested contains schematic variables"
in () end
fun cpu_time description e =
@@ -85,55 +92,59 @@
val _ = check_test_term t
val names = Term.add_free_names t []
val current_size = Unsynchronized.ref 0
- val current_result = Unsynchronized.ref Quickcheck.empty_result
- val act = if catch_code_errors then try else (fn f => SOME o f)
- val (test_fun, comp_time) = cpu_time "quickcheck compilation"
- (fn () => act (compile ctxt) [(t, eval_terms)]);
+ val current_result = Unsynchronized.ref Quickcheck.empty_result
+ val act = if catch_code_errors then try else (fn f => SOME o f)
+ val (test_fun, comp_time) =
+ cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)])
val _ = Quickcheck.add_timing comp_time current_result
fun with_size test_fun genuine_only k =
- if k > Config.get ctxt Quickcheck.size then
- NONE
+ if k > Config.get ctxt Quickcheck.size then NONE
else
let
- val _ = Quickcheck.verbose_message ctxt
- ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
+ val _ =
+ Quickcheck.verbose_message ctxt
+ ("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
val ((result, report), time) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
- val _ = if Config.get ctxt Quickcheck.timing then
- Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+ val _ =
+ if Config.get ctxt Quickcheck.timing then
+ Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms")
+ else ()
val _ = Quickcheck.add_timing time current_result
val _ = Quickcheck.add_report k report current_result
in
- case result of
+ (case result of
NONE => with_size test_fun genuine_only (k + 1)
| SOME (true, ts) => SOME (true, ts)
| SOME (false, ts) =>
- if abort_potential then SOME (false, ts)
- else
- let
- val (ts1, ts2) = chop (length names) ts
- val (eval_terms', _) = chop (length ts2) eval_terms
- val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
- in
- (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
- Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
- with_size test_fun true k)
- end
- end;
+ if abort_potential then SOME (false, ts)
+ else
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) eval_terms
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ Quickcheck.message ctxt
+ (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
+ with_size test_fun true k
+ end)
+ end
in
case test_fun of
- NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
- !current_result)
+ NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
+ !current_result)
| SOME test_fun =>
- let
- val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
- val (response, exec_time) =
- cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
- val _ = Quickcheck.add_response names eval_terms response current_result
- val _ = Quickcheck.add_timing exec_time current_result
- in !current_result end
- end;
+ let
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
+ val (response, exec_time) =
+ cpu_time "quickcheck execution" (fn () => with_size test_fun genuine_only 1)
+ val _ = Quickcheck.add_response names eval_terms response current_result
+ val _ = Quickcheck.add_timing exec_time current_result
+ in !current_result end
+ end
fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts =
let
@@ -145,105 +156,104 @@
val names = Term.add_free_names (hd ts') []
val Ts = map snd (Term.add_frees (hd ts') [])
val current_result = Unsynchronized.ref Quickcheck.empty_result
- fun test_card_size test_fun genuine_only (card, size) =
- (* FIXME: why decrement size by one? *)
+ fun test_card_size test_fun genuine_only (card, size) = (* FIXME: why decrement size by one? *)
let
val _ =
Quickcheck.verbose_message ctxt ("[Quickcheck-" ^ name ^ "] Test " ^
(if size = 0 then "" else "data size: " ^ string_of_int size ^ " and ") ^
- "cardinality: " ^ string_of_int card)
+ "cardinality: " ^ string_of_int card)
val (ts, timing) =
cpu_time ("size " ^ string_of_int size ^ " and card " ^ string_of_int card)
(fn () => fst (test_fun genuine_only [card, size + 1]))
val _ = Quickcheck.add_timing timing current_result
- in
- Option.map (pair (card, size)) ts
- end
+ in Option.map (pair (card, size)) ts end
val enumeration_card_size =
if size_matters_for thy Ts then
map_product pair (1 upto (length ts)) (1 upto (Config.get ctxt Quickcheck.size))
|> sort (fn ((c1, s1), (c2, s2)) => int_ord ((c1 + s1), (c2 + s2)))
- else
- map (rpair 0) (1 upto (length ts))
+ else map (rpair 0) (1 upto (length ts))
val act = if catch_code_errors then try else (fn f => SOME o f)
val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) ts)
val _ = Quickcheck.add_timing comp_time current_result
in
- case test_fun of
- NONE => (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
- !current_result)
+ (case test_fun of
+ NONE =>
+ (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-" ^ name);
+ !current_result)
| SOME test_fun =>
- let
- val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...");
- fun test genuine_only enum = case get_first (test_card_size test_fun genuine_only) enum of
- SOME ((card, _), (true, ts)) =>
- Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (true, ts)) current_result
- | SOME ((card, size), (false, ts)) =>
- if abort_potential then
- Quickcheck.add_response names (nth eval_terms (card - 1)) (SOME (false, ts)) current_result
- else
- let
- val (ts1, ts2) = chop (length names) ts
- val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
- val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
- in
- (Quickcheck.message ctxt (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
- Quickcheck.message ctxt "Quickcheck continues to find a genuine counterexample...";
- test true (snd (take_prefix (fn x => not (x = (card, size))) enum)))
- end
- | NONE => ()
- in (test genuine_only enumeration_card_size; !current_result) end
+ let
+ val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-" ^ name ^ "...")
+ fun test genuine_only enum =
+ (case get_first (test_card_size test_fun genuine_only) enum of
+ SOME ((card, _), (true, ts)) =>
+ Quickcheck.add_response names (nth eval_terms (card - 1))
+ (SOME (true, ts)) current_result
+ | SOME ((card, size), (false, ts)) =>
+ if abort_potential then
+ Quickcheck.add_response names (nth eval_terms (card - 1))
+ (SOME (false, ts)) current_result
+ else
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) (nth eval_terms (card - 1))
+ val cex = SOME ((false, names ~~ ts1), eval_terms' ~~ ts2)
+ in
+ Quickcheck.message ctxt
+ (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex));
+ Quickcheck.message ctxt
+ "Quickcheck continues to find a genuine counterexample...";
+ test true (snd (take_prefix (fn x => not (x = (card, size))) enum))
+ end
+ | NONE => ())
+ in (test genuine_only enumeration_card_size; !current_result) end)
end
fun get_finite_types ctxt =
fst (chop (Config.get ctxt Quickcheck.finite_type_size)
- [@{typ "Enum.finite_1"}, @{typ "Enum.finite_2"}, @{typ "Enum.finite_3"},
- @{typ "Enum.finite_4"}, @{typ "Enum.finite_5"}])
+ [@{typ Enum.finite_1}, @{typ Enum.finite_2}, @{typ Enum.finite_3},
+ @{typ Enum.finite_4}, @{typ Enum.finite_5}])
exception WELLSORTED of string
fun monomorphic_term thy insts default_T =
let
fun subst (T as TFree (v, S)) =
- let
- val T' = AList.lookup (op =) insts v
- |> the_default default_T
- in if Sign.of_sort thy (T', S) then T'
- else raise (WELLSORTED ("For instantiation with default_type " ^
- Syntax.string_of_typ_global thy default_T ^
- ":\n" ^ Syntax.string_of_typ_global thy T' ^
- " to be substituted for variable " ^
- Syntax.string_of_typ_global thy T ^ " does not have sort " ^
- Syntax.string_of_sort_global thy S))
- end
- | subst T = T;
- in (map_types o map_atyps) subst end;
+ let val T' = AList.lookup (op =) insts v |> the_default default_T in
+ if Sign.of_sort thy (T', S) then T'
+ else raise (WELLSORTED ("For instantiation with default_type " ^
+ Syntax.string_of_typ_global thy default_T ^
+ ":\n" ^ Syntax.string_of_typ_global thy T' ^
+ " to be substituted for variable " ^
+ Syntax.string_of_typ_global thy T ^ " does not have sort " ^
+ Syntax.string_of_sort_global thy S))
+ end
+ | subst T = T
+ in (map_types o map_atyps) subst end
datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list
+
(* minimalistic preprocessing *)
-fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) =
- let
- val (a', t') = strip_all t
- in ((a, T) :: a', t') end
- | strip_all t = ([], t);
+fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) =
+ let val (a', t') = strip_all t
+ in ((a, T) :: a', t') end
+ | strip_all t = ([], t)
fun preprocess ctxt t =
let
val thy = Proof_Context.theory_of ctxt
val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
- val rewrs = map (swap o dest) @{thms all_simps} @
- (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
- @{thm bot_fun_def}, @{thm less_bool_def}])
+ val rewrs =
+ map (swap o dest) @{thms all_simps} @
+ (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
+ @{thm bot_fun_def}, @{thm less_bool_def}])
val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
val (vs, body) = strip_all t'
val vs' = Variable.variant_frees ctxt [t'] vs
- in
- subst_bounds (map Free (rev vs'), body)
- end
+ in subst_bounds (map Free (rev vs'), body) end
-
+
structure Subtype_Predicates = Generic_Data
(
type T = (term * string) list
@@ -257,31 +267,31 @@
fun subtype_preprocess ctxt (T, (t, ts)) =
let
val preds = Subtype_Predicates.get (Context.Proof ctxt)
- fun matches (p $ _) = AList.defined Term.could_unify preds p
+ fun matches (p $ _) = AList.defined Term.could_unify preds p
fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
fun subst_of (tyco, v as Free (x, repT)) =
let
val [(info, _)] = Typedef.get_info ctxt tyco
val repT' = Logic.varifyT_global (#rep_type info)
- val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
+ val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
val (prems, concl) = strip_imp t
val subst = map subst_of (map_filter get_match prems)
val t' = Term.subst_free subst
(fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
- in
- (T, (t', ts))
- end
+ in (T, (t', ts)) end
+
(* instantiation of type variables with concrete types *)
-
+
fun instantiate_goals lthy insts goals =
let
fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms)
val thy = Proof_Context.theory_of lthy
val default_insts =
- if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type
+ if Config.get lthy Quickcheck.finite_types
+ then get_finite_types else Quickcheck.default_type
val inst_goals =
map (fn (check_goal, eval_terms) =>
if not (null (Term.add_tfree_names check_goal [])) then
@@ -289,67 +299,61 @@
(pair (SOME T) o Term o apfst (preprocess lthy))
(map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms))
handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy)
- else
- [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
+ else [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals
val error_msg =
cat_lines
(maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals)
fun is_wellsorted_term (T, Term t) = SOME (T, t)
| is_wellsorted_term (_, Wellsorted_Error _) = NONE
val correct_inst_goals =
- case map (map_filter is_wellsorted_term) inst_goals of
+ (case map (map_filter is_wellsorted_term) inst_goals of
[[]] => error error_msg
- | xs => xs
+ | xs => xs)
val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg
- in
- correct_inst_goals
- end
+ in correct_inst_goals end
+
(* compilation of testing functions *)
fun mk_safe_if genuine_only none (cond, then_t, else_t) genuine =
let
val T = fastype_of then_t
- val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
+ val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
in
- Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $
+ Const (@{const_name "Quickcheck_Random.catch_match"}, T --> T --> T) $
(if_t $ cond $ then_t $ else_t genuine) $
(if_t $ genuine_only $ none $ else_t false)
end
fun collect_results f [] results = results
| collect_results f (t :: ts) results =
- let
- val result = f t
- in
- if Quickcheck.found_counterexample result then
- (result :: results)
- else
- collect_results f ts (result :: results)
- end
+ let val result = f t in
+ if Quickcheck.found_counterexample result then result :: results
+ else collect_results f ts (result :: results)
+ end
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
let
val use_subtype = Config.get ctxt Quickcheck.use_subtype
fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
fun add_equation_eval_terms (t, eval_terms) =
- case try HOLogic.dest_eq (snd (strip_imp t)) of
+ (case try HOLogic.dest_eq (snd (strip_imp t)) of
SOME (lhs, rhs) => (t, add_eval_term lhs (add_eval_term rhs eval_terms))
- | NONE => (t, eval_terms)
+ | NONE => (t, eval_terms))
fun test_term' goal =
- case goal of
+ (case goal of
[(NONE, t)] => test_term generator ctxt catch_code_errors t
- | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
- val goals' = instantiate_goals ctxt insts goals
+ | ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts))
+ val goals' =
+ instantiate_goals ctxt insts goals
|> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then
collect_results test_term' goals' []
- else
- collect_results (test_term generator ctxt catch_code_errors)
- (maps (map snd) goals') []
- end;
+ else collect_results (test_term generator ctxt catch_code_errors) (maps (map snd) goals') []
+ end
+
(* defining functions *)
@@ -388,38 +392,42 @@
(names ~~ eqs) lthy
end)
+
(** ensuring sort constraints **)
-type instantiation = Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list
- -> string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
+type instantiation =
+ Old_Datatype_Aux.config -> Old_Datatype_Aux.descr -> (string * sort) list ->
+ string list -> string -> string list * string list -> typ list * typ list -> theory -> theory
fun perhaps_constrain thy insts raw_vs =
let
- fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy)
- (Logic.varifyT_global T, sort);
+ fun meet (T, sort) = Sorts.meet_sort (Sign.classes_of thy) (Logic.varifyT_global T, sort)
val vtab = Vartab.empty
|> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) raw_vs
- |> fold meet insts;
- in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
- end handle Sorts.CLASS_ERROR _ => NONE;
+ |> fold meet insts
+ in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0))) end
+ handle Sorts.CLASS_ERROR _ => NONE
fun ensure_sort (((sort_vs, aux_sort), sort), (the_descr, instantiate)) config raw_tycos thy =
let
- val algebra = Sign.classes_of thy;
+ val algebra = Sign.classes_of thy
val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = the_descr thy raw_tycos
val vs = (map o apsnd) (curry (Sorts.inter_sort algebra) sort_vs) raw_vs
fun insts_of sort constr = (map (rpair sort) o flat o maps snd o maps snd)
(Old_Datatype_Aux.interpret_construction descr vs constr)
val insts = insts_of sort { atyp = single, dtyp = (K o K o K) [] }
@ insts_of aux_sort { atyp = K [], dtyp = K o K }
- val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos;
- in if has_inst then thy
- else case perhaps_constrain thy insts vs
- of SOME constrain => instantiate config descr
- (map constrain vs) tycos prfx (names, auxnames)
- ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
- | NONE => thy
- end;
+ val has_inst = exists (fn tyco => Sorts.has_instance algebra tyco sort) tycos
+ in
+ if has_inst then thy
+ else
+ (case perhaps_constrain thy insts vs of
+ SOME constrain =>
+ instantiate config descr
+ (map constrain vs) tycos prfx (names, auxnames)
+ ((apply2 o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
+ | NONE => thy)
+ end
fun ensure_common_sort_datatype (sort, instantiate) =
ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
@@ -427,86 +435,89 @@
fun datatype_interpretation name =
BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype
-
+
+
(** generic parametric compilation **)
fun gen_mk_parametric_generator_expr ((mk_generator_expr, out_of_bounds), T) ctxt ts =
let
- val if_t = Const (@{const_name "If"}, @{typ bool} --> T --> T --> T)
- fun mk_if (index, (t, eval_terms)) else_t = if_t $
- (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
+ val if_t = Const (@{const_name If}, @{typ bool} --> T --> T --> T)
+ fun mk_if (index, (t, eval_terms)) else_t =
+ if_t $ (HOLogic.eq_const @{typ natural} $ Bound 0 $ HOLogic.mk_number @{typ natural} index) $
(mk_generator_expr ctxt (t, eval_terms)) $ else_t
- in
- absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds)
- end
+ in absdummy @{typ natural} (fold_rev mk_if (1 upto (length ts) ~~ ts) out_of_bounds) end
+
(** post-processing of function terms **)
fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
| dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
-fun mk_fun_upd T1 T2 (t1, t2) t =
+fun mk_fun_upd T1 T2 (t1, t2) t =
Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2) $ t $ t1 $ t2
fun dest_fun_upds t =
- case try dest_fun_upd t of
+ (case try dest_fun_upd t of
NONE =>
(case t of
- Abs (_, _, _) => ([], t)
+ Abs (_, _, _) => ([], t)
| _ => raise TERM ("dest_fun_upds", [t]))
- | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0)
+ | SOME (t0, (t1, t2)) => apfst (cons (t1, t2)) (dest_fun_upds t0))
fun make_fun_upds T1 T2 (tps, t) = fold_rev (mk_fun_upd T1 T2) tps t
fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
| make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
| make_set T1 ((t1, @{const True}) :: tps) =
- Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
- $ t1 $ (make_set T1 tps)
+ Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $
+ t1 $ (make_set T1 tps)
| make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t])
fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool})
- | make_coset T tps =
+ | make_coset T tps =
let
val U = T --> @{typ bool}
fun invert @{const False} = @{const True}
| invert @{const True} = @{const False}
in
- Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U)
- $ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
+ Const (@{const_name "Groups.minus_class.minus"}, U --> U --> U) $
+ Const (@{const_abbrev UNIV}, U) $ make_set T (map (apsnd invert) tps)
end
fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
| make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
| make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
-
+
fun post_process_term t =
let
fun map_Abs f t =
- case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t])
- fun process_args t = case strip_comb t of
- (c as Const (_, _), ts) => list_comb (c, map post_process_term ts)
+ (case t of
+ Abs (x, T, t') => Abs (x, T, f t')
+ | _ => raise TERM ("map_Abs", [t]))
+ fun process_args t =
+ (case strip_comb t of
+ (c as Const (_, _), ts) => list_comb (c, map post_process_term ts))
in
- case fastype_of t of
+ (case fastype_of t of
Type (@{type_name fun}, [T1, T2]) =>
(case try dest_fun_upds t of
SOME (tps, t) =>
- (map (apply2 post_process_term) tps, map_Abs post_process_term t)
- |> (case T2 of
- @{typ bool} =>
- (case t of
- Abs(_, _, @{const False}) => fst #> rev #> make_set T1
- | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
- | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
- | _ => raise TERM ("post_process_term", [t]))
- | Type (@{type_name option}, _) =>
- (case t of
- Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
- | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
- | _ => make_fun_upds T1 T2)
- | _ => make_fun_upds T1 T2)
+ (map (apply2 post_process_term) tps, map_Abs post_process_term t) |>
+ (case T2 of
+ @{typ bool} =>
+ (case t of
+ Abs(_, _, @{const False}) => fst #> rev #> make_set T1
+ | Abs(_, _, @{const True}) => fst #> rev #> make_coset T1
+ | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> rev #> make_set T1
+ | _ => raise TERM ("post_process_term", [t]))
+ | Type (@{type_name option}, _) =>
+ (case t of
+ Abs(_, _, Const (@{const_name None}, _)) => fst #> make_map T1 T2
+ | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
+ | _ => make_fun_upds T1 T2)
+ | _ => make_fun_upds T1 T2)
| NONE => process_args t)
- | _ => process_args t
+ | _ => process_args t)
end
-end;
+end