--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 12 13:33:05 2014 +0100
@@ -18,9 +18,9 @@
val set_ensure_groundness : code_options -> code_options
val map_limit_predicates : ((string list * int) list -> (string list * int) list)
-> code_options -> code_options
- val code_options_of : theory -> code_options
+ val code_options_of : theory -> code_options
val map_code_options : (code_options -> code_options) -> theory -> theory
-
+
datatype arith_op = Plus | Minus
datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list
| Number of int | ArithOp of arith_op * prol_term list;
@@ -33,20 +33,20 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
type constant_table = (string * string) list
-
+
val generate : Predicate_Compile_Aux.mode option * bool ->
Proof.context -> string -> (logic_program * constant_table)
val write_program : logic_program -> string
val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) ->
string list -> int option -> prol_term list list
-
+
val active : bool Config.T
val test_goals :
Proof.context -> bool -> (string * typ) list -> (term * term list) list ->
Quickcheck.result list
val trace : bool Unsynchronized.ref
-
+
val replace : ((string * string) * string) -> logic_program -> logic_program
end;
@@ -57,11 +57,11 @@
val trace = Unsynchronized.ref false
-fun tracing s = if !trace then Output.tracing s else ()
+fun tracing s = if !trace then Output.tracing s else ()
+
(* code generation options *)
-
type code_options =
{ensure_groundness : bool,
limit_globally : int option,
@@ -79,15 +79,15 @@
fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
- limited_predicates = f limited_predicates, replacing = replacing,
- manual_reorder = manual_reorder}
+ {ensure_groundness = ensure_groundness, limit_globally = limit_globally,
+ limited_types = limited_types, limited_predicates = f limited_predicates,
+ replacing = replacing, manual_reorder = manual_reorder}
fun merge_global_limit (NONE, NONE) = NONE
| merge_global_limit (NONE, SOME n) = SOME n
| merge_global_limit (SOME n, NONE) = SOME n
| merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m)) (* FIXME odd merge *)
-
+
structure Options = Theory_Data
(
type T = code_options
@@ -113,6 +113,7 @@
val map_code_options = Options.map
+
(* system configuration *)
datatype prolog_system = SWI_PROLOG | YAP
@@ -121,7 +122,7 @@
| string_of_system YAP = "yap"
type system_configuration = {timeout : Time.time, prolog_system : prolog_system}
-
+
structure System_Config = Generic_Data
(
type T = system_configuration
@@ -130,11 +131,13 @@
fun merge (a, _) = a
)
+
(* general string functions *)
val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
+
(* internal program representation *)
datatype arith_op = Plus | Minus
@@ -153,7 +156,7 @@
| map_vars f (ArithOp (opr, ts)) = ArithOp (opr, map (map_vars f) ts)
| map_vars f (AppF (fs, ts)) = AppF (fs, map (map_vars f) ts)
| map_vars f t = t
-
+
fun maybe_AppF (c, []) = Cons c
| maybe_AppF (c, xs) = AppF (c, xs)
@@ -167,7 +170,7 @@
fun string_of_prol_term (Var s) = "Var " ^ s
| string_of_prol_term (Cons s) = "Cons " ^ s
- | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
+ | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")"
| string_of_prol_term (Number n) = "Number " ^ string_of_int n
datatype prem = Conj of prem list
@@ -195,11 +198,12 @@
| fold_prem_terms f (ArithEq (l, r)) = f l #> f r
| fold_prem_terms f (NotArithEq (l, r)) = f l #> f r
| fold_prem_terms f (Ground (v, T)) = f (Var v)
-
+
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
-
+
+
(* translation from introduction rules to internal representation *)
fun mk_conform f empty avoid name =
@@ -211,6 +215,7 @@
val name'' = f (if name' = "" then empty else name')
in if member (op =) avoid name'' then singleton (Name.variant_list avoid) name'' else name'' end
+
(** constant table **)
type constant_table = (string * string) list
@@ -227,11 +232,11 @@
in
fold update' consts constant_table
end
-
+
fun translate_const constant_table c =
- case AList.lookup (op =) constant_table c of
+ (case AList.lookup (op =) constant_table c of
SOME c' => c'
- | NONE => error ("No such constant: " ^ c)
+ | NONE => error ("No such constant: " ^ c))
fun inv_lookup _ [] _ = NONE
| inv_lookup eq ((key, value)::xs) value' =
@@ -239,9 +244,10 @@
else inv_lookup eq xs value';
fun restore_const constant_table c =
- case inv_lookup (op =) constant_table c of
+ (case inv_lookup (op =) constant_table c of
SOME c' => c'
- | NONE => error ("No constant corresponding to " ^ c)
+ | NONE => error ("No constant corresponding to " ^ c))
+
(** translation of terms, literals, premises, and clauses **)
@@ -256,52 +262,53 @@
in funpow n (fn t => AppF (Suc, [t])) (Cons zero) end
fun translate_term ctxt constant_table t =
- case try HOLogic.dest_number t of
+ (case try HOLogic.dest_number t of
SOME (@{typ "int"}, n) => Number n
| SOME (@{typ "nat"}, n) => mk_nat_term constant_table n
| NONE =>
(case strip_comb t of
- (Free (v, T), []) => Var v
+ (Free (v, T), []) => Var v
| (Const (c, _), []) => Cons (translate_const constant_table c)
| (Const (c, _), args) =>
- (case translate_arith_const c of
- SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
- | NONE =>
- AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
- | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t))
+ (case translate_arith_const c of
+ SOME aop => ArithOp (aop, map (translate_term ctxt constant_table) args)
+ | NONE =>
+ AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args))
+ | _ => error ("illegal term for translation: " ^ Syntax.string_of_term ctxt t)))
fun translate_literal ctxt constant_table t =
- case strip_comb t of
+ (case strip_comb t of
(Const (@{const_name HOL.eq}, _), [l, r]) =>
let
val l' = translate_term ctxt constant_table l
val r' = translate_term ctxt constant_table r
in
- (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq) (l', r')
+ (if is_Var l' andalso is_arith_term r' andalso not (is_Var r') then ArithEq else Eq)
+ (l', r')
end
| (Const (c, _), args) =>
Rel (translate_const constant_table c, map (translate_term ctxt constant_table) args)
- | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t)
+ | _ => error ("illegal literal for translation: " ^ Syntax.string_of_term ctxt t))
fun NegRel_of (Rel lit) = NotRel lit
| NegRel_of (Eq eq) = NotEq eq
| NegRel_of (ArithEq eq) = NotArithEq eq
fun mk_groundness_prems t = map Ground (Term.add_frees t [])
-
-fun translate_prem ensure_groundness ctxt constant_table t =
- case try HOLogic.dest_not t of
- SOME t =>
- if ensure_groundness then
- Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
- else
- NegRel_of (translate_literal ctxt constant_table t)
- | NONE => translate_literal ctxt constant_table t
-
+
+fun translate_prem ensure_groundness ctxt constant_table t =
+ (case try HOLogic.dest_not t of
+ SOME t =>
+ if ensure_groundness then
+ Conj (mk_groundness_prems t @ [NegRel_of (translate_literal ctxt constant_table t)])
+ else
+ NegRel_of (translate_literal ctxt constant_table t)
+ | NONE => translate_literal ctxt constant_table t)
+
fun imp_prems_conv cv ct =
- case Thm.term_of ct of
+ (case Thm.term_of ct of
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
- | _ => Conv.all_conv ct
+ | _ => Conv.all_conv ct)
fun preprocess_intro thy rule =
Conv.fconv_rule
@@ -330,17 +337,17 @@
fun add_edges edges_of key G =
let
- fun extend' key (G, visited) =
- case try (Graph.get_node G) key of
- SOME v =>
- let
- val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
- val (G', visited') = fold extend'
- (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
- in
- (fold (Graph.add_edge o (pair key)) new_edges G', visited')
- end
- | NONE => (G, visited)
+ fun extend' key (G, visited) =
+ (case try (Graph.get_node G) key of
+ SOME v =>
+ let
+ val new_edges = filter (fn k => is_some (try (Graph.get_node G) k)) (edges_of (key, v))
+ val (G', visited') = fold extend'
+ (subtract (op =) (key :: visited) new_edges) (G, key :: visited)
+ in
+ (fold (Graph.add_edge o (pair key)) new_edges G', visited')
+ end
+ | NONE => (G, visited))
in
fst (extend' key (G, []))
end
@@ -350,6 +357,7 @@
"Constant " ^ const ^ "has intros:\n" ^
cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
+
(* translation of moded predicates *)
(** generating graph of moded predicates **)
@@ -361,15 +369,20 @@
(case fst (strip_comb t) of
Const (c, _) => SOME (c, (pol, Predicate_Compile_Core.head_mode_of derivation))
| _ => NONE)
- fun req (Predicate_Compile_Aux.Prem t, derivation) = req_mode_of polarity (t, derivation)
- | req (Predicate_Compile_Aux.Negprem t, derivation) = req_mode_of (not polarity) (t, derivation)
+ fun req (Predicate_Compile_Aux.Prem t, derivation) =
+ req_mode_of polarity (t, derivation)
+ | req (Predicate_Compile_Aux.Negprem t, derivation) =
+ req_mode_of (not polarity) (t, derivation)
| req _ = NONE
- in
+ in
maps (fn (_, prems) => map_filter req prems) cls
end
-
-structure Mode_Graph = Graph(type key = string * (bool * Predicate_Compile_Aux.mode)
- val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord));
+
+structure Mode_Graph =
+ Graph(
+ type key = string * (bool * Predicate_Compile_Aux.mode)
+ val ord = prod_ord fast_string_ord (prod_ord bool_ord Predicate_Compile_Aux.mode_ord)
+ )
fun mk_moded_clauses_graph ctxt scc gr =
let
@@ -386,14 +399,16 @@
Predicate_Compile_Core.prepare_intrs options ctxt prednames
(maps (Core_Data.intros_of ctxt) prednames)
val ((moded_clauses, random'), _) =
- Mode_Inference.infer_modes mode_analysis_options options
+ Mode_Inference.infer_modes mode_analysis_options options
(lookup_modes, lookup_neg_modes, needs_random) ctxt preds all_modes param_vs clauses
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
val pos_modes' = map (apsnd (map_filter (fn (true, m) => SOME m | _ => NONE))) modes
val neg_modes' = map (apsnd (map_filter (fn (false, m) => SOME m | _ => NONE))) modes
- val _ = tracing ("Inferred modes:\n" ^
- cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
- (fn (p, m) => Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
+ val _ =
+ tracing ("Inferred modes:\n" ^
+ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
+ (fn (p, m) =>
+ Predicate_Compile_Aux.string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
val gr' = gr
|> fold (fn (p, mps) => fold (fn (mode, cls) =>
Mode_Graph.new_node ((p, mode), cls)) mps)
@@ -406,8 +421,8 @@
AList.merge (op =) (op =) (neg_modes, neg_modes'),
AList.merge (op =) (op =) (random, random')))
end
- in
- fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], [])))
+ in
+ fst (fold infer (rev scc) (Mode_Graph.empty, ([], [], [])))
end
fun declare_moded_predicate moded_preds table =
@@ -431,32 +446,34 @@
fun mk_literal pol derivation constant_table' t =
let
val (p, args) = strip_comb t
- val mode = Predicate_Compile_Core.head_mode_of derivation
+ val mode = Predicate_Compile_Core.head_mode_of derivation
val name = fst (dest_Const p)
-
+
val p' = the (AList.lookup (op =) moded_pred_table' (name, (pol, mode)))
val args' = map (translate_term ctxt constant_table') args
in
Rel (p', args')
end
fun mk_prem pol (indprem, derivation) constant_table =
- case indprem of
+ (case indprem of
Predicate_Compile_Aux.Generator (s, T) => (Ground (s, T), constant_table)
| _ =>
- declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) []) constant_table
+ declare_consts (Term.add_const_names (Predicate_Compile_Aux.dest_indprem indprem) [])
+ constant_table
|> (fn constant_table' =>
(case indprem of Predicate_Compile_Aux.Negprem t =>
NegRel_of (mk_literal (not pol) derivation constant_table' t)
| _ =>
- mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem), constant_table'))
+ mk_literal pol derivation constant_table' (Predicate_Compile_Aux.dest_indprem indprem),
+ constant_table')))
fun mk_clause pred_name pol (ts, prems) (prog, constant_table) =
- let
- val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table
- val args = map (translate_term ctxt constant_table') ts
- val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table'
- in
- (((pred_name, args), Conj prems') :: prog, constant_table'')
- end
+ let
+ val constant_table' = declare_consts (fold Term.add_const_names ts []) constant_table
+ val args = map (translate_term ctxt constant_table') ts
+ val (prems', constant_table'') = fold_map (mk_prem pol) prems constant_table'
+ in
+ (((pred_name, args), Conj prems') :: prog, constant_table'')
+ end
fun mk_clauses (pred, mode as (pol, _)) =
let
val clauses = Mode_Graph.get_node moded_gr (pred, mode)
@@ -469,35 +486,37 @@
end
fun generate (use_modes, ensure_groundness) ctxt const =
- let
+ let
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
val gr = Core_Data.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
- val initial_constant_table =
+ val initial_constant_table =
declare_consts [@{const_name "Groups.zero_class.zero"}, @{const_name "Suc"}] []
in
- case use_modes of
+ (case use_modes of
SOME mode =>
let
val moded_gr = mk_moded_clauses_graph ctxt scc gr
val moded_gr' = Mode_Graph.restrict
(member (op =) (Mode_Graph.all_succs moded_gr [(const, (true, mode))])) moded_gr
- val scc = Mode_Graph.strong_conn moded_gr'
+ val scc = Mode_Graph.strong_conn moded_gr'
in
apfst rev (apsnd snd
(fold (mk_program ctxt moded_gr') (rev scc) ([], ([], initial_constant_table))))
end
- | NONE =>
- let
+ | NONE =>
+ let
val _ = print_intros ctxt gr (flat scc)
val constant_table = declare_consts (flat scc) initial_constant_table
in
- apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
- end
+ apfst flat
+ (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
+ end)
end
-
+
+
(* implementation for fully enumerating predicates and
for size-limited predicates for enumerating the values of a datatype upto a specific size *)
@@ -506,7 +525,7 @@
| add_ground_typ _ = I
fun mk_relname (Type (Tcon, Targs)) =
- first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
+ first_lower (Long_Name.base_name Tcon) ^ space_implode "_" (map mk_relname Targs)
| mk_relname _ = raise Fail "unexpected type"
fun mk_lim_relname T = "lim_" ^ mk_relname T
@@ -519,14 +538,15 @@
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
fun is_recursive_constr T (Const (constr_name, T')) = member (op =) (binder_types T') T
-
+
fun mk_ground_impl ctxt limited_types (T as Type (Tcon, Targs)) (seen, constant_table) =
if member (op =) seen T then ([], (seen, constant_table))
else
let
- val (limited, size) = case AList.lookup (op =) limited_types T of
- SOME s => (true, s)
- | NONE => (false, 0)
+ val (limited, size) =
+ (case AList.lookup (op =) limited_types T of
+ SOME s => (true, s)
+ | NONE => (false, 0))
val rel_name = (if limited then mk_lim_relname else mk_relname) T
fun mk_impl (Const (constr_name, cT), recursive) (seen, constant_table) =
let
@@ -537,9 +557,9 @@
val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto (length Ts))
val lim_var =
if limited then
- if recursive then [AppF ("suc", [Var "Lim"])]
+ if recursive then [AppF ("suc", [Var "Lim"])]
else [Var "Lim"]
- else []
+ else []
fun mk_prem v T' =
if limited andalso T' = T then Rel (mk_lim_relname T', [Var "Lim", v])
else Rel (mk_relname T', [v])
@@ -565,18 +585,20 @@
fun replace_ground (Conj prems) = Conj (map replace_ground prems)
| replace_ground (Ground (x, T)) =
- Rel (mk_relname T, [Var x])
+ Rel (mk_relname T, [Var x])
| replace_ground p = p
-
+
fun add_ground_predicates ctxt limited_types (p, constant_table) =
let
val ground_typs = fold (add_ground_typ o snd) p []
- val (grs, (_, constant_table')) = fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
+ val (grs, (_, constant_table')) =
+ fold_map (mk_ground_impl ctxt limited_types) ground_typs ([], constant_table)
val p' = map (apsnd replace_ground) p
in
((flat grs) @ p', constant_table')
end
+
(* make depth-limited version of predicate *)
fun mk_lim_rel_name rel_name = "lim_" ^ rel_name
@@ -600,8 +622,8 @@
fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
fun add_limited_predicates limited_predicates (p, constant_table) =
- let
- fun add (rel_names, limit) p =
+ let
+ fun add (rel_names, limit) p =
let
val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
val clauses' = map (mk_depth_limited rel_names) clauses
@@ -609,7 +631,7 @@
let
val nargs = length (snd (fst
(the (find_first (fn ((rel, _), _) => rel = rel_name) clauses))))
- val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
in
(("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
end
@@ -629,10 +651,12 @@
if rel = from then Rel (to, ts) else r
| replace_prem r = r
in
- map (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem)) p
+ map
+ (fn ((rel, args), prem) => ((rel, args), (if rel = location then replace_prem else I) prem))
+ p
end
-
+
(* reorder manually : reorder premises of ith clause of predicate p by a permutation perm *)
fun reorder_manually reorder p =
@@ -642,14 +666,16 @@
val seen' = AList.map_default (op =) (rel, 0) (fn x => x + 1) seen
val i = the (AList.lookup (op =) seen' rel)
val perm = AList.lookup (op =) reorder (rel, i)
- val prem' = (case perm of
- SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
- | NONE => prem)
+ val prem' =
+ (case perm of
+ SOME p => (case prem of Conj prems => Conj (map (nth prems) p) | _ => prem)
+ | NONE => prem)
in (((rel, args), prem'), seen') end
in
fst (fold_map reorder' p [])
end
+
(* rename variables to prolog-friendly names *)
fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v))
@@ -658,7 +684,7 @@
fun is_prolog_conform v =
forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v)
-
+
fun mk_renaming v renaming =
(v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming
@@ -667,9 +693,10 @@
val vars = fold_prem_terms add_vars prem (fold add_vars args [])
val renaming = fold mk_renaming vars []
in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
-
+
val rename_vars_program = map rename_vars_clause
+
(* limit computation globally by some threshold *)
fun limit_globally ctxt limit const_name (p, constant_table) =
@@ -686,6 +713,7 @@
(entry_clause :: p' @ p'', constant_table)
end
+
(* post processing of generated prolog program *)
fun post_process ctxt options const_name (p, constant_table) =
@@ -703,6 +731,7 @@
|> apfst (reorder_manually (#manual_reorder options))
|> apfst rename_vars_program
+
(* code printer *)
fun write_arith_op Plus = "+"
@@ -710,15 +739,17 @@
fun write_term (Var v) = v
| write_term (Cons c) = c
- | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
- | write_term (ArithOp (oper, [a1, a2])) = write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
+ | write_term (AppF (f, args)) =
+ f ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ | write_term (ArithOp (oper, [a1, a2])) =
+ write_term a1 ^ " " ^ write_arith_op oper ^ " " ^ write_term a2
| write_term (Number n) = string_of_int n
fun write_rel (pred, args) =
- pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
+ pred ^ "(" ^ space_implode ", " (map write_term args) ^ ")"
fun write_prem (Conj prems) = space_implode ", " (map write_prem prems)
- | write_prem (Rel p) = write_rel p
+ | write_prem (Rel p) = write_rel p
| write_prem (NotRel p) = "not(" ^ write_rel p ^ ")"
| write_prem (Eq (l, r)) = write_term l ^ " = " ^ write_term r
| write_prem (NotEq (l, r)) = write_term l ^ " \\= " ^ write_term r
@@ -730,7 +761,8 @@
write_rel head ^ (if prem = Conj [] then "." else " :- " ^ write_prem prem ^ ".")
fun write_program p =
- cat_lines (map write_clause p)
+ cat_lines (map write_clause p)
+
(* query templates *)
@@ -740,7 +772,7 @@
"eval :- once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]).\n"
-
+
fun swi_prolog_query_firstn n (rel, args) vnames =
"eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^
rel ^ "(" ^ space_implode ", " (map write_term args) ^ "), Sols), writelist(Sols).\n" ^
@@ -748,7 +780,7 @@
"writelist([(" ^ space_implode ", " vnames ^ ")|SolutionTail]) :- " ^
"writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
"\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n"
-
+
val swi_prolog_prelude =
":- use_module(library('dialect/ciao/aggregates')).\n" ^
":- style_check(-singleton).\n" ^
@@ -757,6 +789,7 @@
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
"main :- halt(1).\n"
+
(** query and prelude for yap **)
fun yap_query_first (rel, args) vnames =
@@ -767,18 +800,25 @@
val yap_prelude =
":- initialization(eval).\n"
+
(* system-dependent query, prelude and invocation *)
-fun query system nsols =
- case system of
+fun query system nsols =
+ (case system of
SWI_PROLOG =>
- (case nsols of NONE => swi_prolog_query_first | SOME n => swi_prolog_query_firstn n)
+ (case nsols of
+ NONE => swi_prolog_query_first
+ | SOME n => swi_prolog_query_firstn n)
| YAP =>
- case nsols of NONE => yap_query_first | SOME n =>
- error "No support for querying multiple solutions in the prolog system yap"
+ (case nsols of
+ NONE => yap_query_first
+ | SOME n =>
+ error "No support for querying multiple solutions in the prolog system yap"))
fun prelude system =
- case system of SWI_PROLOG => swi_prolog_prelude | YAP => yap_prelude
+ (case system of
+ SWI_PROLOG => swi_prolog_prelude
+ | YAP => yap_prelude)
fun invoke system file =
let
@@ -804,7 +844,8 @@
Scan.many1 Symbol.is_ascii_digit
val scan_atom =
- Scan.many1 (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+ Scan.many1
+ (fn s => Symbol.is_ascii_lower s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
val scan_var =
Scan.many1
@@ -821,7 +862,8 @@
val is_atom_ident = forall Symbol.is_ascii_lower
val is_var_ident =
- forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
+ forall (fn s =>
+ Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)
fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0
@@ -837,23 +879,25 @@
val parse_term = fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
o raw_explode
-
+
fun parse_solutions sol =
let
- fun dest_eq s = case space_explode "=" s of
+ fun dest_eq s =
+ (case space_explode "=" s of
(l :: r :: []) => parse_term (unprefix " " r)
- | _ => raise Fail "unexpected equation in prolog output"
+ | _ => raise Fail "unexpected equation in prolog output")
fun parse_solution s = map dest_eq (space_explode ";" s)
- val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)
+ val sols = (case space_explode "\n" sol of [] => [] | s => fst (split_last s))
in
map parse_solution sols
- end
-
+ end
+
+
(* calling external interpreter and getting results *)
fun run (timeout, system) p (query_rel, args) vnames nsols =
let
- val renaming = fold mk_renaming (fold add_vars args vnames) []
+ val renaming = fold mk_renaming (fold add_vars args vnames) []
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
val args' = map (rename_vars_term renaming) args
val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
@@ -867,26 +911,27 @@
tss
end
+
(* restoring types in terms *)
fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
| restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
- | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number")
+ | restore_term ctxt constant_table (Number n, _) = raise (Fail "unexpected type for number")
| restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
| restore_term ctxt constant_table (AppF (f, args), T) =
- let
- val thy = Proof_Context.theory_of ctxt
- val c = restore_const constant_table f
- val cT = Sign.the_const_type thy c
- val (argsT, resT) = strip_type cT
- val subst = Sign.typ_match thy (resT, T) Vartab.empty
- val argsT' = map (Envir.subst_type subst) argsT
- in
- list_comb (Const (c, Envir.subst_type subst cT),
- map (restore_term ctxt constant_table) (args ~~ argsT'))
- end
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val c = restore_const constant_table f
+ val cT = Sign.the_const_type thy c
+ val (argsT, resT) = strip_type cT
+ val subst = Sign.typ_match thy (resT, T) Vartab.empty
+ val argsT' = map (Envir.subst_type subst) argsT
+ in
+ list_comb (Const (c, Envir.subst_type subst cT),
+ map (restore_term ctxt constant_table) (args ~~ argsT'))
+ end
-
+
(* restore numerals in natural numbers *)
fun restore_nat_numerals t =
@@ -894,9 +939,10 @@
HOLogic.mk_number @{typ nat} (HOLogic.dest_nat t)
else
(case t of
- t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2
- | t => t)
-
+ t1 $ t2 => restore_nat_numerals t1 $ restore_nat_numerals t2
+ | t => t)
+
+
(* values command *)
val preprocess_options = Predicate_Compile_Aux.Options {
@@ -926,17 +972,19 @@
fun values ctxt soln t_compr =
let
val options = code_options_of (Proof_Context.theory_of ctxt)
- val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
- | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
- val (body, Ts, fp) = HOLogic.strip_psplits split;
+ val split =
+ (case t_compr of
+ (Const (@{const_name Collect}, _) $ t) => t
+ | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
+ val (body, Ts, fp) = HOLogic.strip_psplits split
val output_names = Name.variant_list (Term.add_free_names body [])
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val output_frees = rev (map2 (curry Free) output_names Ts)
val body = subst_bounds (output_frees, body)
val (pred as Const (name, T), all_args) =
- case strip_comb body of
+ (case strip_comb body of
(Const (name, T), all_args) => (Const (name, T), all_args)
- | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
+ | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
val _ = tracing "Preprocessing specification..."
val T = Sign.the_const_type (Proof_Context.theory_of ctxt) name
val t = Const (name, T)
@@ -956,7 +1004,7 @@
val _ = tracing "Restoring terms..."
val empty = Const(@{const_name bot}, fastype_of t_compr)
fun mk_insert x S =
- Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S
+ Const (@{const_name "Set.insert"}, fastype_of x --> fastype_of S --> fastype_of S) $ x $ S
fun mk_set_compr in_insert [] xs =
rev ((Free ("dots", fastype_of t_compr)) :: (* FIXME proper name!? *)
(if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
@@ -968,19 +1016,22 @@
mk_set_compr (t :: in_insert) ts xs
else
let
- val uu as (uuN, uuT) = singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
+ val uu as (uuN, uuT) =
+ singleton (Variable.variant_frees ctxt' [t]) ("uu", fastype_of t)
val set_compr =
- HOLogic.mk_Collect (uuN, uuT, fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
- frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
+ HOLogic.mk_Collect (uuN, uuT,
+ fold (fn (s, T) => fn t => HOLogic.mk_exists (s, T, t))
+ frees (HOLogic.mk_conj (HOLogic.mk_eq (Free uu, t), @{term "True"})))
in
mk_set_compr [] ts
- (set_compr :: (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
+ (set_compr ::
+ (if null in_insert then xs else (fold mk_insert in_insert empty) :: xs))
end
end
in
- foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
- (map (fn ts => HOLogic.mk_tuple
- (map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
+ foldl1 (HOLogic.mk_binop @{const_name sup}) (mk_set_compr []
+ (map (fn ts => HOLogic.mk_tuple
+ (map (restore_nat_numerals o restore_term ctxt' constant_table) (ts ~~ Ts))) tss) [])
end
fun values_cmd print_modes soln raw_t state =
@@ -991,30 +1042,31 @@
val ty' = Term.type_of t'
val ctxt' = Variable.auto_fixes t' ctxt
val _ = tracing "Printing terms..."
- val p = Print_Mode.with_modes print_modes (fn () =>
+ in
+ Print_Mode.with_modes print_modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
- in Pretty.writeln p end;
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ()
+ end |> Pretty.writeln p
(* renewing the values command for Prolog queries *)
val opt_print_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val _ =
Outer_Syntax.improper_command @{command_spec "values"}
"enumerate and print comprehensions"
(opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
>> (fn ((print_modes, soln), t) => Toplevel.keep
- (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+ (values_cmd print_modes soln t))) (*FIXME does not preserve the previous functionality*)
(* quickcheck generator *)
(* FIXME: a small clone of Predicate_Compile_Quickcheck - maybe refactor out commons *)
-val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true);
+val active = Attrib.setup_config_bool @{binding quickcheck_prolog_active} (K true)
fun test_term ctxt (t, eval_terms) =
let
@@ -1035,14 +1087,17 @@
p (translate_const constant_table full_constname, map (Var o fst) vs') (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
val counterexample =
- case tss of
+ (case tss of
[ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
- | _ => NONE
+ | _ => NONE)
in
Quickcheck.Result
- {counterexample = Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
- evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
- end;
+ {counterexample =
+ Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
+ evaluation_terms = Option.map (K []) counterexample,
+ timings = [],
+ reports = []}
+ end
fun test_goals ctxt _ insts goals =
let
@@ -1050,6 +1105,5 @@
in
Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
end
-
-
-end;
+
+end
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Feb 12 13:33:05 2014 +0100
@@ -133,14 +133,16 @@
val merge = Graph.merge eq_pred_data;
);
+
(* queries *)
fun lookup_pred_data ctxt name =
Option.map rep_pred_data (try (Graph.get_node (PredData.get (Proof_Context.theory_of ctxt))) name)
-fun the_pred_data ctxt name = case lookup_pred_data ctxt name
- of NONE => error ("No such predicate " ^ quote name)
- | SOME data => data;
+fun the_pred_data ctxt name =
+ (case lookup_pred_data ctxt name of
+ NONE => error ("No such predicate " ^ quote name)
+ | SOME data => data)
val is_registered = is_some oo lookup_pred_data
@@ -150,24 +152,26 @@
val names_of = map fst o #intros oo the_pred_data
-fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
- of NONE => error ("No elimination rule for predicate " ^ quote name)
- | SOME thm => thm
+fun the_elim_of ctxt name =
+ (case #elim (the_pred_data ctxt name) of
+ NONE => error ("No elimination rule for predicate " ^ quote name)
+ | SOME thm => thm)
val has_elim = is_some o #elim oo the_pred_data
fun function_names_of compilation ctxt name =
- case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
- NONE => error ("No " ^ string_of_compilation compilation
- ^ " functions defined for predicate " ^ quote name)
- | SOME fun_names => fun_names
+ (case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
+ NONE =>
+ error ("No " ^ string_of_compilation compilation ^
+ " functions defined for predicate " ^ quote name)
+ | SOME fun_names => fun_names)
fun function_name_of compilation ctxt name mode =
- case AList.lookup eq_mode
- (function_names_of compilation ctxt name) mode of
- NONE => error ("No " ^ string_of_compilation compilation
- ^ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
- | SOME function_name => function_name
+ (case AList.lookup eq_mode (function_names_of compilation ctxt name) mode of
+ NONE =>
+ error ("No " ^ string_of_compilation compilation ^
+ " function defined for mode " ^ string_of_mode mode ^ " of predicate " ^ quote name)
+ | SOME function_name => function_name)
fun modes_of compilation ctxt name = map fst (function_names_of compilation ctxt name)
@@ -177,9 +181,10 @@
val all_random_modes_of = all_modes_of Random
-fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
+fun defined_functions compilation ctxt name =
+ (case lookup_pred_data ctxt name of
NONE => false
- | SOME data => AList.defined (op =) (#function_names data) compilation
+ | SOME data => AList.defined (op =) (#function_names data) compilation)
fun needs_random ctxt s m =
member (op =) (#needs_random (the_pred_data ctxt s)) m
@@ -189,10 +194,11 @@
(AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
fun the_predfun_data ctxt name mode =
- case lookup_predfun_data ctxt name mode of
- NONE => error ("No function defined for mode " ^ string_of_mode mode ^
- " of predicate " ^ name)
- | SOME data => data;
+ (case lookup_predfun_data ctxt name mode of
+ NONE =>
+ error ("No function defined for mode " ^ string_of_mode mode ^
+ " of predicate " ^ name)
+ | SOME data => data)
val predfun_definition_of = #definition ooo the_predfun_data
@@ -221,7 +227,8 @@
val case_th =
rewrite_rule ctxt (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
val prems' = maps (dest_conjunct_prem o rewrite_rule ctxt tuple_rew_rules) prems
- val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
+ val pats =
+ map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
OF (replicate nargs @{thm refl})
val thesis =
@@ -242,6 +249,7 @@
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
end
+
(* updaters *)
(* fetching introduction rules or registering introduction rules *)
@@ -249,7 +257,7 @@
val no_compilation = ([], ([], []))
fun fetch_pred_data ctxt name =
- case try (Inductive.the_inductive ctxt) name of
+ (case try (Inductive.the_inductive ctxt) name of
SOME (info as (_, result)) =>
let
fun is_intro_of intro =
@@ -267,7 +275,7 @@
in
mk_pred_data (((map (pair NONE) intros, SOME elim), true), no_compilation)
end
- | NONE => error ("No such predicate: " ^ quote name)
+ | NONE => error ("No such predicate: " ^ quote name))
fun add_predfun_data name mode data =
let
@@ -294,16 +302,19 @@
let
val (name, _) = dest_Const (fst (strip_intro_concl thm))
fun cons_intro gr =
- case try (Graph.get_node gr) name of
- SOME _ => Graph.map_node name (map_pred_data
- (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
- | NONE => Graph.new_node (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr
+ (case try (Graph.get_node gr) name of
+ SOME _ =>
+ Graph.map_node name (map_pred_data
+ (apfst (apfst (apfst (fn intros => intros @ [(opt_case_name, thm)]))))) gr
+ | NONE =>
+ Graph.new_node
+ (name, mk_pred_data ((([(opt_case_name, thm)], NONE), false), no_compilation)) gr)
in PredData.map cons_intro thy end
fun set_elim thm =
let
- val (name, _) = dest_Const (fst
- (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
+ val (name, _) =
+ dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (hd (prems_of thm)))))
in PredData.map (Graph.map_node name (map_pred_data (apfst (apfst (apsnd (K (SOME thm))))))) end
fun register_predicate (constname, intros, elim) thy =
@@ -356,12 +367,14 @@
fun extend' value_of edges_of key (G, visited) =
let
- val (G', v) = case try (Graph.get_node G) key of
+ val (G', v) =
+ (case try (Graph.get_node G) key of
SOME v => (G, v)
- | NONE => (Graph.new_node (key, value_of key) G, value_of key)
- val (G'', visited') = fold (extend' value_of edges_of)
- (subtract (op =) visited (edges_of (key, v)))
- (G', key :: visited)
+ | NONE => (Graph.new_node (key, value_of key) G, value_of key))
+ val (G'', visited') =
+ fold (extend' value_of edges_of)
+ (subtract (op =) visited (edges_of (key, v)))
+ (G', key :: visited)
in
(fold (Graph.add_edge o (pair key)) (edges_of (key, v)) G'', visited')
end;
@@ -391,14 +404,15 @@
end))))
thy
+
(* registration of alternative function names *)
structure Alt_Compilations_Data = Theory_Data
(
- type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
- val empty = Symtab.empty;
- val extend = I;
- fun merge data : T = Symtab.merge (K true) data;
+ type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data : T = Symtab.merge (K true) data
);
fun alternative_compilation_of_global thy pred_name mode =
@@ -416,19 +430,21 @@
(List.partition (fn (_, (_, random)) => random) compilations)
val non_random_dummys = map (rpair "dummy") non_random_modes
val all_dummys = map (rpair "dummy") modes
- val dummy_function_names = map (rpair all_dummys) Predicate_Compile_Aux.random_compilations
- @ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
+ val dummy_function_names =
+ map (rpair all_dummys) Predicate_Compile_Aux.random_compilations @
+ map (rpair non_random_dummys) Predicate_Compile_Aux.non_random_compilations
val alt_compilations = map (apsnd fst) compilations
in
- PredData.map (Graph.new_node
- (pred_name, mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
+ PredData.map
+ (Graph.new_node
+ (pred_name,
+ mk_pred_data ((([], SOME @{thm refl}), true), (dummy_function_names, ([], needs_random)))))
#> Alt_Compilations_Data.map (Symtab.insert (K false) (pred_name, alt_compilations))
end
fun functional_compilation fun_name mode compfuns T =
let
- val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE))
- mode (binder_types T)
+ val (inpTs, outpTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
val bs = map (pair "x") inpTs
val bounds = map Bound (rev (0 upto (length bs) - 1))
val f = Const (fun_name, inpTs ---> HOLogic.mk_tupleT outpTs)
@@ -443,4 +459,4 @@
(map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
fun_names)
-end;
\ No newline at end of file
+end
\ No newline at end of file
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Wed Feb 12 13:33:05 2014 +0100
@@ -71,8 +71,10 @@
fun mode_of (Context m) = m
| mode_of (Term m) = m
| mode_of (Mode_App (d1, d2)) =
- (case mode_of d1 of Fun (m, m') =>
- (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of: derivation has mismatching modes")
+ (case mode_of d1 of
+ Fun (m, m') =>
+ (if eq_mode (m, mode_of d2) then m'
+ else raise Fail "mode_of: derivation has mismatching modes")
| _ => raise Fail "mode_of: derivation has a non-functional mode")
| mode_of (Mode_Pair (d1, d2)) =
Pair (mode_of d1, mode_of d2)
@@ -109,12 +111,12 @@
(Syntax.string_of_term ctxt (HOLogic.mk_not t)) ^ "(negative premise)"
| string_of_prem ctxt (Sidecond t) =
(Syntax.string_of_term ctxt t) ^ "(sidecondition)"
- | string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
+ | string_of_prem _ _ = raise Fail "string_of_prem: unexpected input"
type mode_analysis_options =
{use_generators : bool,
- reorder_premises : bool,
- infer_pos_and_neg_modes : bool}
+ reorder_premises : bool,
+ infer_pos_and_neg_modes : bool}
(*** check if a type is an equality type (i.e. doesn't contain fun)
FIXME this is only an approximation ***)
@@ -134,7 +136,7 @@
fun error_of p (_, m) is =
" Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
- p ^ " violates mode " ^ string_of_mode m
+ p ^ " violates mode " ^ string_of_mode m
fun is_all_input mode =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Feb 12 13:33:05 2014 +0100
@@ -24,18 +24,20 @@
fun print_intross options thy msg intross =
if show_intermediate_results options then
- tracing (msg ^
- (space_implode "\n" (map
+ tracing (msg ^
+ (space_implode "\n" (map
(fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
commas (map (Display.string_of_thm_global thy) intros)) intross)))
else ()
-
+
fun print_specs options thy specs =
if show_intermediate_results options then
- map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
- ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+ map (fn (c, thms) =>
+ "Constant " ^ c ^ " has specification:\n" ^
+ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
|> space_implode "\n" |> tracing
else ()
+
fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
fun map_specs f specs =
@@ -44,8 +46,12 @@
fun process_specification options specs thy' =
let
val _ = print_step options "Compiling predicates to flat introrules..."
- val specs = map (apsnd (map
- (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs
+ val specs =
+ map
+ (apsnd (map
+ (fn th =>
+ if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th)))
+ specs
val (intross1, thy'') =
apfst flat (fold_map (Predicate_Compile_Pred.preprocess options) specs thy')
val _ = print_intross options thy'' "Flattened introduction rules: " intross1
@@ -53,21 +59,24 @@
val intross2 =
if function_flattening options then
if fail_safe_function_flattening options then
- case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
+ (case try (map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
SOME intross => intross
| NONE =>
(if show_caught_failures options then tracing "Function replacement failed!" else ();
- intross1)
+ intross1))
else map_specs (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
else
intross1
val _ = print_intross options thy'' "Introduction rules with replaced functions: " intross2
- val _ = print_step options "Introducing new constants for abstractions at higher-order argument positions..."
- val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
- val (new_intross, thy'''') =
+ val _ = print_step options
+ "Introducing new constants for abstractions at higher-order argument positions..."
+ val (intross3, (new_defs, thy''')) =
+ Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
+ val (new_intross, thy'''') =
if not (null new_defs) then
let
- val _ = print_step options "Recursively obtaining introduction rules for new definitions..."
+ val _ =
+ print_step options "Recursively obtaining introduction rules for new definitions..."
in process_specification options new_defs thy''' end
else ([], thy''')
in
@@ -75,9 +84,8 @@
end
fun preprocess_strong_conn_constnames options gr ts thy =
- if forall (fn (Const (c, _)) =>
- Core_Data.is_registered (Proof_Context.init_global thy) c) ts then
- thy
+ if forall (fn (Const (c, _)) => Core_Data.is_registered (Proof_Context.init_global thy) c) ts
+ then thy
else
let
fun get_specs ts = map_filter (fn t =>
@@ -94,9 +102,9 @@
val (fun_pred_specs, thy1) =
(if function_flattening options andalso (not (null funnames)) then
if fail_safe_function_flattening options then
- case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
+ (case try (Predicate_Compile_Fun.define_predicates (get_specs funnames)) thy of
SOME (intross, thy) => (intross, thy)
- | NONE => ([], thy)
+ | NONE => ([], thy))
else Predicate_Compile_Fun.define_predicates (get_specs funnames) thy
else ([], thy))
val _ = print_specs options thy1 fun_pred_specs
@@ -111,8 +119,9 @@
map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
val intross7 = map_specs (map (expand_tuples thy2)) intross6
val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
- val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
- val _ = print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
+ val _ = (case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ()))
+ val _ =
+ print_step options ("Looking for specialisations in " ^ commas (map fst intross8) ^ "...")
val (intross9, thy3) =
if specialise options then
Predicate_Compile_Specialisation.find_specialisations [] intross8 thy2
@@ -129,14 +138,17 @@
fun preprocess options t thy =
let
val _ = print_step options "Fetching definitions from theory..."
- val gr = cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
- (fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
+ val gr =
+ cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-obtain graph"
+ (fn () =>
+ Predicate_Compile_Data.obtain_specification_graph options thy t
|> (fn gr => Term_Graph.restrict (member (op =) (Term_Graph.all_succs gr [t])) gr))
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
cond_timeit (Config.get_global thy Quickcheck.timing) "preprocess-process"
- (fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
- (Term_Graph.strong_conn gr) thy))
+ (fn () =>
+ fold_rev (preprocess_strong_conn_constnames options gr)
+ (Term_Graph.strong_conn gr) thy)
end
datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
@@ -145,14 +157,15 @@
fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
let
fun chk s = member (op =) raw_options s
- val proposed_modes = case proposed_modes of
- Single_Pred proposed_modes => [(const, proposed_modes)]
- | Multiple_Preds proposed_modes => map
- (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes
+ val proposed_modes =
+ (case proposed_modes of
+ Single_Pred proposed_modes => [(const, proposed_modes)]
+ | Multiple_Preds proposed_modes =>
+ map (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes)
in
Options {
expected_modes = Option.map (pair const) expected_modes,
- proposed_modes =
+ proposed_modes =
map (apsnd (map fst)) proposed_modes,
proposed_names =
maps (fn (predname, ms) => (map_filter
@@ -190,15 +203,14 @@
let
val lthy' = Local_Theory.background_theory (preprocess options t) lthy
val const =
- case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of
+ (case Predicate_Compile_Fun.pred_of_function (Proof_Context.theory_of lthy') const of
SOME c => c
- | NONE => const
+ | NONE => const)
val _ = print_step options "Starting Predicate Compile Core..."
in
Predicate_Compile_Core.code_pred options const lthy'
end
- else
- Predicate_Compile_Core.code_pred_cmd options raw_const lthy
+ else Predicate_Compile_Core.code_pred_cmd options raw_const lthy
end
val setup = Predicate_Compile_Core.setup
@@ -210,10 +222,11 @@
(Args.$$$ "i" >> K Input || Args.$$$ "o" >> K Output ||
Args.$$$ "bool" >> K Bool || Args.$$$ "(" |-- parse_mode_expr --| Args.$$$ ")") xs
and parse_mode_tuple_expr xs =
- (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr)
- xs
+ (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\<times>") -- parse_mode_tuple_expr >> Pair ||
+ parse_mode_basic_expr) xs
and parse_mode_expr xs =
- (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs
+ (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\<Rightarrow>") -- parse_mode_expr >> Fun ||
+ parse_mode_tuple_expr) xs
val mode_and_opt_proposal = parse_mode_expr --
Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
@@ -230,6 +243,7 @@
Scan.optional (@{keyword "("} |-- Args.$$$ "expected_modes" |-- @{keyword ":"} |--
Parse.enum "," parse_mode_expr --| @{keyword ")"} >> SOME) NONE
+
(* Parser for options *)
val scan_options =
@@ -243,7 +257,7 @@
end
val opt_print_modes =
- Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
+ Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) []
val opt_mode = (Args.$$$ "_" >> K NONE) || (parse_mode_expr >> SOME)
@@ -267,6 +281,7 @@
((NONE, false), (Pred, []))
end
+
(* code_pred command and values command *)
val _ =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Feb 12 13:33:05 2014 +0100
@@ -89,17 +89,17 @@
val funT_of : compilation_funs -> mode -> typ -> typ
(* Different compilations *)
datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
- | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
+ | Pos_Random_DSeq | Neg_Random_DSeq | New_Pos_Random_DSeq | New_Neg_Random_DSeq
| Pos_Generator_DSeq | Neg_Generator_DSeq | Pos_Generator_CPS | Neg_Generator_CPS
val negative_compilation_of : compilation -> compilation
val compilation_for_polarity : bool -> compilation -> compilation
- val is_depth_limited_compilation : compilation -> bool
+ val is_depth_limited_compilation : compilation -> bool
val string_of_compilation : compilation -> string
val compilation_names : (string * compilation) list
val non_random_compilations : compilation list
val random_compilations : compilation list
(* Different options for compiler *)
- datatype options = Options of {
+ datatype options = Options of {
expected_modes : (string * mode list) option,
proposed_modes : (string * mode list) list,
proposed_names : ((string * mode) * string) list,
@@ -161,7 +161,7 @@
val unify_consts : theory -> term list -> term list -> (term list * term list)
val mk_casesrule : Proof.context -> term -> thm list -> term
val preprocess_intro : theory -> thm -> thm
-
+
val define_quickcheck_predicate :
term -> theory -> (((string * typ) * (string * typ) list) * thm) * theory
end;
@@ -211,7 +211,7 @@
| mode_ord (Bool, Bool) = EQUAL
| mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
| mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
-
+
fun list_fun_mode [] = Bool
| list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
@@ -227,7 +227,7 @@
fun dest_tuple_mode (Pair (mode, mode')) = mode :: dest_tuple_mode mode'
| dest_tuple_mode _ = []
-fun all_modes_of_typ' (T as Type ("fun", _)) =
+fun all_modes_of_typ' (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
in
@@ -237,7 +237,7 @@
else
[Input, Output]
end
- | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ | all_modes_of_typ' (Type (@{type_name Product_Type.prod}, [T1, T2])) =
map_product (curry Pair) (all_modes_of_typ' T1) (all_modes_of_typ' T2)
| all_modes_of_typ' _ = [Input, Output]
@@ -258,7 +258,7 @@
fun all_smodes_of_typ (T as Type ("fun", _)) =
let
val (S, U) = strip_type T
- fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ fun all_smodes (Type (@{type_name Product_Type.prod}, [T1, T2])) =
map_product (curry Pair) (all_smodes T1) (all_smodes T2)
| all_smodes _ = [Input, Output]
in
@@ -291,8 +291,9 @@
fun ho_args_of_typ T ts =
let
- fun ho_arg (T as Type("fun", [_,_])) (SOME t) = if body_type T = @{typ bool} then [t] else []
- | ho_arg (Type("fun", [_,_])) NONE = raise Fail "mode and term do not match"
+ fun ho_arg (T as Type ("fun", [_, _])) (SOME t) =
+ if body_type T = @{typ bool} then [t] else []
+ | ho_arg (Type ("fun", [_, _])) NONE = raise Fail "mode and term do not match"
| ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2]))
(SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2)
@@ -306,25 +307,25 @@
fun ho_argsT_of_typ Ts =
let
fun ho_arg (T as Type("fun", [_,_])) = if body_type T = @{typ bool} then [T] else []
- | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) =
+ | ho_arg (Type (@{type_name "Product_Type.prod"}, [T1, T2])) =
ho_arg T1 @ ho_arg T2
| ho_arg _ = []
in
maps ho_arg Ts
end
-
+
(* temporary function should be replaced by unsplit_input or so? *)
fun replace_ho_args mode hoargs ts =
let
fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
| replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs =
- let
- val (t1', hoargs') = replace (m1, t1) hoargs
- val (t2', hoargs'') = replace (m2, t2) hoargs'
- in
- (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
- end
+ let
+ val (t1', hoargs') = replace (m1, t1) hoargs
+ val (t2', hoargs'') = replace (m2, t2) hoargs'
+ in
+ (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
+ end
| replace (_, t) hoargs = (t, hoargs)
in
fst (fold_map replace (strip_fun_mode mode ~~ ts) hoargs)
@@ -333,7 +334,8 @@
fun ho_argsT_of mode Ts =
let
fun ho_arg (Fun _) T = [T]
- | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) = ho_arg m1 T1 @ ho_arg m2 T2
+ | ho_arg (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ ho_arg m1 T1 @ ho_arg m2 T2
| ho_arg _ _ = []
in
flat (map2 ho_arg (strip_fun_mode mode) Ts)
@@ -379,28 +381,28 @@
fun split_mode mode ts = split_map_mode (fn _ => fn _ => (NONE, NONE)) mode ts
fun fold_map_aterms_prodT comb f (Type (@{type_name Product_Type.prod}, [T1, T2])) s =
- let
- val (x1, s') = fold_map_aterms_prodT comb f T1 s
- val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
- in
- (comb x1 x2, s'')
- end
- | fold_map_aterms_prodT comb f T s = f T s
+ let
+ val (x1, s') = fold_map_aterms_prodT comb f T1 s
+ val (x2, s'') = fold_map_aterms_prodT comb f T2 s'
+ in
+ (comb x1 x2, s'')
+ end
+ | fold_map_aterms_prodT _ f T s = f T s
fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
- comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
+ comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
| map_filter_prod f t = f t
-
+
fun split_modeT mode Ts =
let
fun split_arg_mode (Fun _) _ = ([], [])
| split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
- let
- val (i1, o1) = split_arg_mode m1 T1
- val (i2, o2) = split_arg_mode m2 T2
- in
- (i1 @ i2, o1 @ o2)
- end
+ let
+ val (i1, o1) = split_arg_mode m1 T1
+ val (i2, o2) = split_arg_mode m2 T2
+ in
+ (i1 @ i2, o1 @ o2)
+ end
| split_arg_mode Input T = ([T], [])
| split_arg_mode Output T = ([], [T])
| split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
@@ -427,7 +429,7 @@
| ascii_string_of_mode' Bool = "b"
| ascii_string_of_mode' (Pair (m1, m2)) =
"P" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Pair m2
- | ascii_string_of_mode' (Fun (m1, m2)) =
+ | ascii_string_of_mode' (Fun (m1, m2)) =
"F" ^ ascii_string_of_mode' m1 ^ ascii_string_of_mode'_Fun m2 ^ "B"
and ascii_string_of_mode'_Fun (Fun (m1, m2)) =
ascii_string_of_mode' m1 ^ (if m2 = Bool then "" else "_" ^ ascii_string_of_mode'_Fun m2)
@@ -438,10 +440,11 @@
| ascii_string_of_mode'_Pair m = ascii_string_of_mode' m
in ascii_string_of_mode'_Fun mode' end
+
(* premises *)
-datatype indprem = Prem of term | Negprem of term | Sidecond of term
- | Generator of (string * typ);
+datatype indprem =
+ Prem of term | Negprem of term | Sidecond of term | Generator of (string * typ)
fun dest_indprem (Prem t) = t
| dest_indprem (Negprem t) = t
@@ -453,25 +456,28 @@
| map_indprem f (Sidecond t) = Sidecond (f t)
| map_indprem f (Generator (v, T)) = Generator (dest_Free (f (Free (v, T))))
+
(* general syntactic functions *)
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
- | is_equationlike_term (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
+ | is_equationlike_term
+ (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
| is_equationlike_term _ = false
-
-val is_equationlike = is_equationlike_term o prop_of
+
+val is_equationlike = is_equationlike_term o prop_of
fun is_pred_equation_term (Const ("==", _) $ u $ v) =
- (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
+ (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
| is_pred_equation_term _ = false
-
-val is_pred_equation = is_pred_equation_term o prop_of
+
+val is_pred_equation = is_pred_equation_term o prop_of
fun is_intro_term constname t =
- the_default false (try (fn t => case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
- Const (c, _) => c = constname
- | _ => false) t)
-
+ the_default false (try (fn t =>
+ case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
+ Const (c, _) => c = constname
+ | _ => false) t)
+
fun is_intro constname t = is_intro_term constname (prop_of t)
fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
@@ -486,14 +492,17 @@
val cnstrs = flat (maps
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
(Symtab.dest (Datatype.get_all thy)));
- fun check t = (case strip_comb t of
+ fun check t =
+ (case strip_comb t of
(Var _, []) => true
| (Free _, []) => true
- | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
- (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
+ | (Const (s, T), ts) =>
+ (case (AList.lookup (op =) cnstrs s, body_type T) of
+ (SOME (i, Tname), Type (Tname', _)) =>
+ length ts = i andalso Tname = Tname' andalso forall check ts
| _ => false)
| _ => false)
- in check end;
+ in check end
(* returns true if t is an application of an datatype constructor *)
(* which then consequently would be splitted *)
@@ -512,35 +521,37 @@
else false
*)
-val is_constr = Code.is_constr o Proof_Context.theory_of;
+val is_constr = Code.is_constr o Proof_Context.theory_of
fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
- let
- val (xTs, t') = strip_ex t
- in
- ((x, T) :: xTs, t')
- end
+ let
+ val (xTs, t') = strip_ex t
+ in
+ ((x, T) :: xTs, t')
+ end
| strip_ex t = ([], t)
fun focus_ex t nctxt =
let
- val ((xs, Ts), t') = apfst split_list (strip_ex t)
+ val ((xs, Ts), t') = apfst split_list (strip_ex t)
val (xs', nctxt') = fold_map Name.variant xs nctxt;
val ps' = xs' ~~ Ts;
val vs = map Free ps';
val t'' = Term.subst_bounds (rev vs, t');
- in ((ps', t''), nctxt') end;
+ in ((ps', t''), nctxt') end
-val strip_intro_concl = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of)
-
+val strip_intro_concl = strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of
+
+
(* introduction rule combinators *)
-fun map_atoms f intro =
+fun map_atoms f intro =
let
val (literals, head) = Logic.strip_horn intro
- fun appl t = (case t of
+ fun appl t =
+ (case t of
(@{term Not} $ t') => HOLogic.mk_not (f t')
| _ => f t)
in
@@ -551,16 +562,18 @@
fun fold_atoms f intro s =
let
val (literals, _) = Logic.strip_horn intro
- fun appl t s = (case t of
- (@{term Not} $ t') => f t' s
+ fun appl t s =
+ (case t of
+ (@{term Not} $ t') => f t' s
| _ => f t s)
in fold appl (map HOLogic.dest_Trueprop literals) s end
fun fold_map_atoms f intro s =
let
val (literals, head) = Logic.strip_horn intro
- fun appl t s = (case t of
- (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
+ fun appl t s =
+ (case t of
+ (@{term Not} $ t') => apfst HOLogic.mk_not (f t' s)
| _ => f t s)
val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
in
@@ -588,12 +601,14 @@
Logic.list_implies (premises, f head)
end
+
(* combinators to apply a function to all basic parts of nested products *)
fun map_products f (Const (@{const_name Pair}, T) $ t1 $ t2) =
Const (@{const_name Pair}, T) $ map_products f t1 $ map_products f t2
| map_products f t = f t
+
(* split theorems of case expressions *)
fun prepare_split_thm ctxt split_thm =
@@ -602,7 +617,8 @@
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
- | find_split_thm thy _ = NONE
+ | find_split_thm _ _ = NONE
+
(* lifting term operations to theorems *)
@@ -612,10 +628,11 @@
(*
fun equals_conv lhs_cv rhs_cv ct =
case Thm.term_of ct of
- Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
- | _ => error "equals_conv"
+ Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct
+ | _ => error "equals_conv"
*)
+
(* Different compilations *)
datatype compilation = Pred | Depth_Limited | Random | Depth_Limited_Random | DSeq | Annotated
@@ -629,9 +646,9 @@
| negative_compilation_of Pos_Generator_DSeq = Neg_Generator_DSeq
| negative_compilation_of Neg_Generator_DSeq = Pos_Generator_DSeq
| negative_compilation_of Pos_Generator_CPS = Neg_Generator_CPS
- | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS
+ | negative_compilation_of Neg_Generator_CPS = Pos_Generator_CPS
| negative_compilation_of c = c
-
+
fun compilation_for_polarity false Pos_Random_DSeq = Neg_Random_DSeq
| compilation_for_polarity false New_Pos_Random_DSeq = New_Neg_Random_DSeq
| compilation_for_polarity _ c = c
@@ -641,7 +658,7 @@
(c = Pos_Generator_DSeq) orelse (c = Pos_Generator_DSeq)
fun string_of_compilation c =
- case c of
+ (case c of
Pred => ""
| Random => "random"
| Depth_Limited => "depth limited"
@@ -655,9 +672,10 @@
| Pos_Generator_DSeq => "pos_generator_dseq"
| Neg_Generator_DSeq => "neg_generator_dseq"
| Pos_Generator_CPS => "pos_generator_cps"
- | Neg_Generator_CPS => "neg_generator_cps"
-
-val compilation_names = [("pred", Pred),
+ | Neg_Generator_CPS => "neg_generator_cps")
+
+val compilation_names =
+ [("pred", Pred),
("random", Random),
("depth_limited", Depth_Limited),
("depth_limited_random", Depth_Limited_Random),
@@ -675,6 +693,7 @@
Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq,
Pos_Generator_CPS, Neg_Generator_CPS]
+
(* datastructures and setup for generic compilation *)
datatype compilation_funs = CompilationFuns of {
@@ -688,7 +707,7 @@
mk_iterate_upto : typ -> term * term * term -> term,
mk_not : term -> term,
mk_map : typ -> typ -> term -> term -> term
-};
+}
fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
@@ -701,19 +720,22 @@
fun mk_not (CompilationFuns funs) = #mk_not funs
fun mk_map (CompilationFuns funs) = #mk_map funs
+
(** function types and names of different compilations **)
fun funT_of compfuns mode T =
let
val Ts = binder_types T
- val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
+ val (inTs, outTs) =
+ split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
in
inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
- end;
+ end
+
(* Different options for compiler *)
-datatype options = Options of {
+datatype options = Options of {
expected_modes : (string * mode list) option,
proposed_modes : (string * mode list) list,
proposed_names : ((string * mode) * string) list,
@@ -735,7 +757,7 @@
detect_switches : bool,
smart_depth_limiting : bool,
compilation : compilation
-};
+}
fun expected_modes (Options opt) = #expected_modes opt
fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
@@ -798,33 +820,37 @@
fun print_step options s =
if show_steps options then tracing s else ()
+
(* simple transformations *)
(** tuple processing **)
fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
- | rewrite_args (arg::args) (pats, intro_t, ctxt) =
- (case HOLogic.strip_tupleT (fastype_of arg) of
- (_ :: _ :: _) =>
- let
- fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
- (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
- | rewrite_arg' (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
- let
- val thy = Proof_Context.theory_of ctxt
- val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
- val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
- val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
- val args' = map (Pattern.rewrite_term thy [pat] []) args
- in
- rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
- end
- | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
- val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
- (args, (pats, intro_t, ctxt))
- in
- rewrite_args args' (pats, intro_t', ctxt')
- end
+ | rewrite_args (arg::args) (pats, intro_t, ctxt) =
+ (case HOLogic.strip_tupleT (fastype_of arg) of
+ (_ :: _ :: _) =>
+ let
+ fun rewrite_arg'
+ (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name Product_Type.prod}, [_, T2]))
+ (args, (pats, intro_t, ctxt)) =
+ rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
+ | rewrite_arg'
+ (t, Type (@{type_name Product_Type.prod}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
+ val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
+ val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
+ val args' = map (Pattern.rewrite_term thy [pat] []) args
+ in
+ rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
+ end
+ | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
+ val (args', (pats, intro_t', ctxt')) =
+ rewrite_arg' (arg, fastype_of arg) (args, (pats, intro_t, ctxt))
+ in
+ rewrite_args args' (pats, intro_t', ctxt')
+ end
| _ => rewrite_args args (pats, intro_t, ctxt))
fun rewrite_prem atom =
@@ -834,23 +860,24 @@
fun split_conjuncts_in_assms ctxt th =
let
- val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
+ val ((_, [fixed_th]), ctxt') = Variable.import false [th] ctxt
fun split_conjs i nprems th =
if i > nprems then th
else
- case try Drule.RSN (@{thm conjI}, (i, th)) of
- SOME th' => split_conjs i (nprems+1) th'
- | NONE => split_conjs (i+1) nprems th
+ (case try Drule.RSN (@{thm conjI}, (i, th)) of
+ SOME th' => split_conjs i (nprems + 1) th'
+ | NONE => split_conjs (i + 1) nprems th)
in
- singleton (Variable.export ctxt' ctxt) (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
+ singleton (Variable.export ctxt' ctxt)
+ (split_conjs 1 (Thm.nprems_of fixed_th) fixed_th)
end
fun dest_conjunct_prem th =
- case HOLogic.dest_Trueprop (prop_of th) of
+ (case HOLogic.dest_Trueprop (prop_of th) of
(Const (@{const_name HOL.conj}, _) $ _ $ _) =>
dest_conjunct_prem (th RS @{thm conjunct1})
@ dest_conjunct_prem (th RS @{thm conjunct2})
- | _ => [th]
+ | _ => [th])
fun expand_tuples thy intro =
let
@@ -877,6 +904,7 @@
intro'''''
end
+
(** making case distributivity rules **)
(*** this should be part of the datatype package ***)
@@ -888,7 +916,7 @@
val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
fun make comb =
let
- val Type ("fun", [T, T']) = fastype_of comb;
+ val Type ("fun", [T, T']) = fastype_of comb
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
@@ -952,12 +980,14 @@
(map (fn th => th RS @{thm eq_reflection}) ths) [] t
end
+
(*** conversions ***)
fun imp_prems_conv cv ct =
- case Thm.term_of ct of
+ (case Thm.term_of ct of
Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
- | _ => Conv.all_conv ct
+ | _ => Conv.all_conv ct)
+
(** eta contract higher-order arguments **)
@@ -968,6 +998,7 @@
map_term thy (map_concl f o map_atoms f) intro
end
+
(** remove equalities **)
fun remove_equalities thy intro =
@@ -978,26 +1009,27 @@
fun remove_eq (prems, concl) =
let
fun removable_eq prem =
- case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
- SOME (lhs, rhs) => (case lhs of
- Var _ => true
+ (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop) prem of
+ SOME (lhs, rhs) =>
+ (case lhs of
+ Var _ => true
| _ => (case rhs of Var _ => true | _ => false))
- | NONE => false
+ | NONE => false)
in
- case find_first removable_eq prems of
+ (case find_first removable_eq prems of
NONE => (prems, concl)
| SOME eq =>
- let
- val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
- val prems' = remove (op =) eq prems
- val subst = (case lhs of
- (v as Var _) =>
- (fn t => if t = v then rhs else t)
- | _ => (case rhs of
- (v as Var _) => (fn t => if t = v then lhs else t)))
- in
- remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
- end
+ let
+ val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
+ val prems' = remove (op =) eq prems
+ val subst =
+ (case lhs of
+ (v as Var _) =>
+ (fn t => if t = v then rhs else t)
+ | _ => (case rhs of (v as Var _) => (fn t => if t = v then lhs else t)))
+ in
+ remove_eq (map (map_aterms subst) prems', map_aterms subst concl)
+ end)
end
in
Logic.list_implies (remove_eq (prems, concl))
@@ -1006,6 +1038,7 @@
map_term thy remove_eqs intro
end
+
(* Some last processing *)
fun remove_pointless_clauses intro =
@@ -1013,6 +1046,7 @@
[]
else [intro]
+
(* some peephole optimisations *)
fun peephole_optimisation thy intro =
@@ -1021,7 +1055,8 @@
val process =
rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
fun process_False intro_t =
- if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
+ if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
+ then NONE else SOME intro_t
fun process_True intro_t =
map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
in
@@ -1033,60 +1068,65 @@
(* importing introduction rules *)
fun import_intros inp_pred [] ctxt =
- let
- val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
- val T = fastype_of outp_pred
- val paramTs = ho_argsT_of_typ (binder_types T)
- val (param_names, _) = Variable.variant_fixes
- (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
- val params = map2 (curry Free) param_names paramTs
- in
- (((outp_pred, params), []), ctxt')
- end
+ let
+ val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
+ val T = fastype_of outp_pred
+ val paramTs = ho_argsT_of_typ (binder_types T)
+ val (param_names, _) = Variable.variant_fixes
+ (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
+ val params = map2 (curry Free) param_names paramTs
+ in
+ (((outp_pred, params), []), ctxt')
+ end
| import_intros inp_pred (th :: ths) ctxt =
- let
- val ((_, [th']), ctxt') = Variable.import true [th] ctxt
- val thy = Proof_Context.theory_of ctxt'
- val (pred, args) = strip_intro_concl th'
- val T = fastype_of pred
- val ho_args = ho_args_of_typ T args
- fun subst_of (pred', pred) =
- let
- val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
- handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
- ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
- ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
- ^ " in " ^ Display.string_of_thm ctxt th)
- in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
- fun instantiate_typ th =
- let
- val (pred', _) = strip_intro_concl th
- val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then
- raise Fail "Trying to instantiate another predicate" else ()
- in Thm.certify_instantiate (subst_of (pred', pred), []) th end;
- fun instantiate_ho_args th =
- let
- val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
- val ho_args' = map dest_Var (ho_args_of_typ T args')
- in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
- val outp_pred =
- Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
- val ((_, ths'), ctxt1) =
- Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
- in
- (((outp_pred, ho_args), th' :: ths'), ctxt1)
- end
-
+ let
+ val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val thy = Proof_Context.theory_of ctxt'
+ val (pred, args) = strip_intro_concl th'
+ val T = fastype_of pred
+ val ho_args = ho_args_of_typ T args
+ fun subst_of (pred', pred) =
+ let
+ val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
+ handle Type.TYPE_MATCH =>
+ error ("Type mismatch of predicate " ^ fst (dest_Const pred) ^
+ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') ^
+ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" ^
+ " in " ^ Display.string_of_thm ctxt th)
+ in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
+ fun instantiate_typ th =
+ let
+ val (pred', _) = strip_intro_concl th
+ val _ =
+ if not (fst (dest_Const pred) = fst (dest_Const pred')) then
+ raise Fail "Trying to instantiate another predicate"
+ else ()
+ in Thm.certify_instantiate (subst_of (pred', pred), []) th end
+ fun instantiate_ho_args th =
+ let
+ val (_, args') =
+ (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
+ val ho_args' = map dest_Var (ho_args_of_typ T args')
+ in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
+ val outp_pred =
+ Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+ val ((_, ths'), ctxt1) =
+ Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
+ in
+ (((outp_pred, ho_args), th' :: ths'), ctxt1)
+ end
+
+
(* generation of case rules from user-given introduction rules *)
fun mk_args2 (Type (@{type_name Product_Type.prod}, [T1, T2])) st =
- let
- val (t1, st') = mk_args2 T1 st
- val (t2, st'') = mk_args2 T2 st'
- in
- (HOLogic.mk_prod (t1, t2), st'')
- end
- (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
+ let
+ val (t1, st') = mk_args2 T1 st
+ val (t2, st'') = mk_args2 T2 st'
+ in
+ (HOLogic.mk_prod (t1, t2), st'')
+ end
+ (*| mk_args2 (T as Type ("fun", _)) (params, ctxt) =
let
val (S, U) = strip_type T
in
@@ -1100,11 +1140,11 @@
end
end*)
| mk_args2 T (params, ctxt) =
- let
- val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
- in
- (Free (x, T), (params, ctxt'))
- end
+ let
+ val ([x], ctxt') = Variable.variant_fixes ["x"] ctxt
+ in
+ (Free (x, T), (params, ctxt'))
+ end
fun mk_casesrule ctxt pred introrules =
let
@@ -1129,28 +1169,29 @@
val assm = HOLogic.mk_Trueprop (list_comb (pred, argvs))
val cases = map mk_case intros
in Logic.list_implies (assm :: cases, prop) end;
-
+
(* unifying constants to have the same type variables *)
fun unify_consts thy cs intr_ts =
- (let
+ let
val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
fun varify (t, (i, ts)) =
let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
- in (maxidx_of_term t', t'::ts) end;
- val (i, cs') = List.foldr varify (~1, []) cs;
- val (i', intr_ts') = List.foldr varify (i, []) intr_ts;
- val rec_consts = fold add_term_consts_2 cs' [];
- val intr_consts = fold add_term_consts_2 intr_ts' [];
+ in (maxidx_of_term t', t' :: ts) end
+ val (i, cs') = List.foldr varify (~1, []) cs
+ val (i', intr_ts') = List.foldr varify (i, []) intr_ts
+ val rec_consts = fold add_term_consts_2 cs' []
+ val intr_consts = fold add_term_consts_2 intr_ts' []
fun unify (cname, cT) =
let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
- in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
- val (env, _) = fold unify rec_consts (Vartab.empty, i');
+ in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end
+ val (env, _) = fold unify rec_consts (Vartab.empty, i')
val subst = map_types (Envir.norm_type env)
in (map subst cs', map subst intr_ts')
- end) handle Type.TUNIFY =>
- (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
+ end handle Type.TUNIFY =>
+ (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts))
+
(* preprocessing rules *)
@@ -1163,6 +1204,7 @@
fun preprocess_intro thy = expand_tuples thy #> preprocess_equality thy
+
(* defining a quickcheck predicate *)
fun strip_imp_prems (Const(@{const_name HOL.implies}, _) $ A $ B) = A :: strip_imp_prems B
@@ -1171,7 +1213,7 @@
fun strip_imp_concl (Const(@{const_name HOL.implies}, _) $ _ $ B) = strip_imp_concl B
| strip_imp_concl A = A;
-fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+fun strip_horn A = (strip_imp_prems A, strip_imp_concl A)
fun define_quickcheck_predicate t thy =
let
@@ -1184,9 +1226,10 @@
val constT = map snd vs' ---> @{typ bool}
val thy1 = Sign.add_consts_i [(Binding.name constname, constT, NoSyn)] thy
val const = Const (full_constname, constT)
- val t = Logic.list_implies
- (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
- HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
+ val t =
+ Logic.list_implies
+ (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
+ HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
val intro =
Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
(fn _ => ALLGOALS Skip_Proof.cheat_tac)
@@ -1194,4 +1237,4 @@
((((full_constname, constT), vs'), intro), thy1)
end
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Wed Feb 12 13:33:05 2014 +0100
@@ -4,30 +4,30 @@
Structures for different compilations of the predicate compiler.
*)
-structure Predicate_Comp_Funs =
+structure Predicate_Comp_Funs = (* FIXME proper signature *)
struct
fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
- | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
+ | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
-fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T)
fun mk_single t =
let val T = fastype_of t
- in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end;
+ in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
-val mk_plus = HOLogic.mk_binop @{const_name sup};
+val mk_plus = HOLogic.mk_binop @{const_name sup}
fun mk_if cond = Const (@{const_name Predicate.if_pred},
- HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+ HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
fun mk_iterate_upto T (f, from, to) =
list_comb (Const (@{const_name Predicate.iterate_upto},
@@ -50,44 +50,48 @@
val T = dest_monadT (fastype_of f)
in
Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
- end;
+ end
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
- (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp;
+ (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
- mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
+ mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-end;
+end
-structure CPS_Comp_Funs =
+
+structure CPS_Comp_Funs = (* FIXME proper signature *)
struct
-fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
+fun mk_monadT T =
+ (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
-fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
+fun dest_monadT
+ (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
| dest_monadT T = raise TYPE ("dest_monadT", [T], []);
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T)
fun mk_single t =
let val T = fastype_of t
- in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end;
+ in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
- HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+ HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = error "not implemented yet"
@@ -104,14 +108,16 @@
fun mk_map _ _ _ _ = error "not implemented"
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
-end;
+end
-structure Pos_Bounded_CPS_Comp_Funs =
+
+structure Pos_Bounded_CPS_Comp_Funs = (* FIXME proper signature *)
struct
val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
@@ -119,13 +125,13 @@
fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
@{typ "natural => (bool * term list) option"}])) = T
- | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
+ | dest_monadT T = raise TYPE ("dest_monadT", [T], [])
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T)
fun mk_single t =
let val T = fastype_of t
- in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end;
+ in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
@@ -133,10 +139,11 @@
Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}
-fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
- HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+fun mk_if cond =
+ Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
+ HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = error "not implemented yet"
@@ -156,14 +163,16 @@
fun mk_map _ _ _ _ = error "not implemented"
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
-end;
+end
-structure Neg_Bounded_CPS_Comp_Funs =
+
+structure Neg_Bounded_CPS_Comp_Funs = (* FIXME proper signature *)
struct
fun mk_monadT T =
@@ -171,16 +180,17 @@
--> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
--> @{typ "natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
-fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
- @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
- @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
+fun dest_monadT
+ (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
+ @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
+ @{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = T
| dest_monadT T = raise TYPE ("dest_monadT", [T], []);
-fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T);
+fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T)
fun mk_single t =
let val T = fastype_of t
- in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end;
+ in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end
fun mk_bind (x, f) =
let val T as Type ("fun", [_, U]) = fastype_of f
@@ -188,10 +198,10 @@
Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
end;
-val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
+val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
- HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
+ HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = error "not implemented"
@@ -210,7 +220,8 @@
fun mk_map _ _ _ _ = error "not implemented"
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
@@ -218,7 +229,7 @@
end;
-structure RandomPredCompFuns =
+structure RandomPredCompFuns = (* FIXME proper signature *)
struct
fun mk_randompredT T =
@@ -226,7 +237,7 @@
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
[Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = T
- | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
+ | dest_randompredT T = raise TYPE ("dest_randompredT", [T], [])
fun mk_empty T = Const(@{const_name Random_Pred.empty}, mk_randompredT T)
@@ -235,7 +246,7 @@
val T = fastype_of t
in
Const (@{const_name Random_Pred.single}, T --> mk_randompredT T) $ t
- end;
+ end
fun mk_bind (x, f) =
let
@@ -262,14 +273,16 @@
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map},
(T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
-end;
+end
-structure DSequence_CompFuns =
+
+structure DSequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_dseqT T = Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool},
@@ -304,48 +317,51 @@
fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map},
(T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
end;
-structure New_Pos_DSequence_CompFuns =
+
+structure New_Pos_DSequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_pos_dseqT T =
- @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
+ @{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
-fun dest_pos_dseqT (Type ("fun", [@{typ natural},
- Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
- | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
+fun dest_pos_dseqT
+ (Type ("fun", [@{typ natural}, Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
+ | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], [])
-fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, mk_pos_dseqT T)
fun mk_single t =
let
val T = fastype_of t
- in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end;
+ in Const(@{const_name Limited_Sequence.pos_single}, T --> mk_pos_dseqT T) $ t end
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Limited_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
fun mk_decr_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union}
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union};
-
-fun mk_if cond = Const (@{const_name Limited_Sequence.pos_if_seq},
- HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+ Const (@{const_name Limited_Sequence.pos_if_seq},
+ HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -357,56 +373,63 @@
[Type (@{type_name Option.option}, [@{typ unit}])])
in Const (@{const_name Limited_Sequence.pos_not_seq}, nT --> pT) $ t end
-fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.pos_map},
- (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+ Const (@{const_name Limited_Sequence.pos_map},
+ (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-end;
+end
-structure New_Neg_DSequence_CompFuns =
+
+structure New_Neg_DSequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_neg_dseqT T = @{typ natural} -->
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
-fun dest_neg_dseqT (Type ("fun", [@{typ natural},
- Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
- | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
+fun dest_neg_dseqT
+ (Type ("fun", [@{typ natural},
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) =
+ T
+ | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], [])
-fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T);
+fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, mk_neg_dseqT T)
fun mk_single t =
let
val T = fastype_of t
- in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end;
+ in Const(@{const_name Limited_Sequence.neg_single}, T --> mk_neg_dseqT T) $ t end
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Limited_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
fun mk_decr_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
+
+val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union}
-val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name Limited_Sequence.neg_if_seq},
- HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+ Const (@{const_name Limited_Sequence.neg_if_seq},
+ HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -418,53 +441,58 @@
[@{typ unit}])
in Const (@{const_name Limited_Sequence.neg_not_seq}, pT --> nT) $ t end
-fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.neg_map},
- (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+ Const (@{const_name Limited_Sequence.neg_map},
+ (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-end;
+end
-structure New_Pos_Random_Sequence_CompFuns =
+
+structure New_Pos_Random_Sequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_pos_random_dseqT T =
@{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
-fun dest_pos_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
- Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
- Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
- | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_pos_random_dseqT
+ (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
+ Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
+ | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
-fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, mk_pos_random_dseqT T)
fun mk_single t =
let
val T = fastype_of t
- in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
+ in Const(@{const_name Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
fun mk_decr_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union};
@@ -486,59 +514,66 @@
in Const (@{const_name Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.pos_map},
- (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+ Const (@{const_name Random_Sequence.pos_map},
+ (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
+
end;
-structure New_Neg_Random_Sequence_CompFuns =
+
+structure New_Neg_Random_Sequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_neg_random_dseqT T =
- @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
+ @{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
@{typ natural} -->
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
-fun dest_neg_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
- Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
- Type (@{type_name Lazy_Sequence.lazy_sequence},
- [Type (@{type_name Option.option}, [T])])])])])])) = T
- | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_neg_random_dseqT
+ (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+ Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural},
+ Type (@{type_name Lazy_Sequence.lazy_sequence},
+ [Type (@{type_name Option.option}, [T])])])])])])) = T
+ | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
-fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, mk_neg_random_dseqT T)
fun mk_single t =
let
val T = fastype_of t
- in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
+ in Const(@{const_name Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
fun mk_decr_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union}
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union};
-
-fun mk_if cond = Const (@{const_name Random_Sequence.neg_if_random_dseq},
- HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+ Const (@{const_name Random_Sequence.neg_if_random_dseq},
+ HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond
fun mk_iterate_upto T (f, from, to) =
list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto},
@@ -553,51 +588,58 @@
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
in Const (@{const_name Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
-fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.neg_map},
- (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
+fun mk_map T1 T2 tf tp =
+ Const (@{const_name Random_Sequence.neg_map},
+ (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
-val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_limited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
+val depth_unlimited_compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-end;
+end
-structure Random_Sequence_CompFuns =
+
+structure Random_Sequence_CompFuns = (* FIXME proper signature *)
struct
fun mk_random_dseqT T =
@{typ natural} --> @{typ natural} --> @{typ Random.seed} -->
HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
-fun dest_random_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
- Type ("fun", [@{typ Random.seed},
- Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
- | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
+fun dest_random_dseqT
+ (Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural},
+ Type ("fun", [@{typ Random.seed},
+ Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) =
+ DSequence_CompFuns.dest_dseqT T
+ | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], [])
-fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
+fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T)
fun mk_single t =
let
val T = fastype_of t
- in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
+ in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end
fun mk_bind (x, f) =
let
val T as Type ("fun", [_, U]) = fastype_of f
in
Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
- end;
+ end
+
+val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union}
-val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union};
-
-fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
- HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
+fun mk_if cond =
+ Const (@{const_name Random_Sequence.if_random_dseq},
+ HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond
fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
@@ -609,10 +651,11 @@
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
(T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
-val compfuns = Predicate_Compile_Aux.CompilationFuns
+val compfuns =
+ Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT,
mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 12 13:33:05 2014 +0100
@@ -11,15 +11,15 @@
type options = Predicate_Compile_Aux.options
type compilation = Predicate_Compile_Aux.compilation
type compilation_funs = Predicate_Compile_Aux.compilation_funs
-
+
val setup : theory -> theory
val code_pred : options -> string -> Proof.context -> Proof.state
val code_pred_cmd : options -> string -> Proof.context -> Proof.state
- val values_cmd : string list -> mode option list option
- -> ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
+ val values_cmd : string list -> mode option list option ->
+ ((string option * bool) * (compilation * int list)) -> int -> string -> Toplevel.state -> unit
val values_timeout : real Config.T
-
+
val print_stored_rules : Proof.context -> unit
val print_all_modes : compilation -> Proof.context -> unit
@@ -27,19 +27,23 @@
val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
Proof.context -> Proof.context
val put_dseq_result : (unit -> term Limited_Sequence.dseq) -> Proof.context -> Proof.context
- val put_dseq_random_result : (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed) ->
+ val put_dseq_random_result :
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ term Limited_Sequence.dseq * seed) ->
Proof.context -> Proof.context
val put_new_dseq_result : (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val put_lseq_random_result :
- (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) ->
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+ term Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val put_lseq_random_stats_result :
- (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+ (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val code_pred_intro_attrib : attribute
- (* used by Quickcheck_Generator *)
+ (* used by Quickcheck_Generator *)
(* temporary for testing of the compilation *)
val add_equations : options -> string list -> theory -> theory
val add_depth_limited_random_equations : options -> string list -> theory -> theory
@@ -54,7 +58,7 @@
type mode_analysis_options =
{use_generators : bool,
reorder_premises : bool,
- infer_pos_and_neg_modes : bool}
+ infer_pos_and_neg_modes : bool}
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
| Mode_Pair of mode_derivation * mode_derivation | Term of mode
val head_mode_of : mode_derivation -> mode
@@ -90,12 +94,14 @@
Const(@{const_name Code_Evaluation.tracing},
@{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
+
(* representation of inferred clauses with modes *)
type moded_clause = term list * (indprem * mode_derivation) list
type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
+
(* diagnostic display functions *)
fun print_modes options modes =
@@ -152,50 +158,53 @@
(* validity checks *)
fun check_expected_modes options _ modes =
- case expected_modes options of
- SOME (s, ms) => (case AList.lookup (op =) modes s of
- SOME modes =>
- let
- val modes' = map snd modes
- in
- if not (eq_set eq_mode (ms, modes')) then
- error ("expected modes were not inferred:\n"
- ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
- ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
- else ()
- end
- | NONE => ())
- | NONE => ()
+ (case expected_modes options of
+ SOME (s, ms) =>
+ (case AList.lookup (op =) modes s of
+ SOME modes =>
+ let
+ val modes' = map snd modes
+ in
+ if not (eq_set eq_mode (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ())
fun check_proposed_modes options preds modes errors =
- map (fn (s, _) => case proposed_modes options s of
- SOME ms => (case AList.lookup (op =) modes s of
- SOME inferred_ms =>
- let
- val preds_without_modes = map fst (filter (null o snd) modes)
- val modes' = map snd inferred_ms
- in
- if not (eq_set eq_mode (ms, modes')) then
- error ("expected modes were not inferred:\n"
- ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
- ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
- ^ (if show_invalid_clauses options then
- ("For the following clauses, the following modes could not be inferred: " ^ "\n"
- ^ cat_lines errors) else "") ^
- (if not (null preds_without_modes) then
- "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
- else ""))
- else ()
- end
- | NONE => ())
- | NONE => ()) preds
+ map (fn (s, _) =>
+ case proposed_modes options s of
+ SOME ms =>
+ (case AList.lookup (op =) modes s of
+ SOME inferred_ms =>
+ let
+ val preds_without_modes = map fst (filter (null o snd) modes)
+ val modes' = map snd inferred_ms
+ in
+ if not (eq_set eq_mode (ms, modes')) then
+ error ("expected modes were not inferred:\n"
+ ^ " inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes') ^ "\n"
+ ^ " expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
+ ^ (if show_invalid_clauses options then
+ ("For the following clauses, the following modes could not be inferred: " ^ "\n"
+ ^ cat_lines errors) else "") ^
+ (if not (null preds_without_modes) then
+ "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
+ else ""))
+ else ()
+ end
+ | NONE => ())
+ | NONE => ()) preds
fun check_matches_type ctxt predname T ms =
let
fun check (Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
| check m (Type("fun", _)) = (m = Input orelse m = Output)
| check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
- check m1 T1 andalso check m2 T2
+ check m1 T1 andalso check m2 T2
| check Input _ = true
| check Output _ = true
| check Bool @{typ bool} = true
@@ -203,30 +212,32 @@
fun check_consistent_modes ms =
if forall (fn Fun _ => true | _ => false) ms then
pairself check_consistent_modes (split_list (map (fn Fun (m1, m2) => (m1, m2)) ms))
- |> (fn (res1, res2) => res1 andalso res2)
+ |> (fn (res1, res2) => res1 andalso res2)
else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
true
else if forall (fn Bool => true | _ => false) ms then
true
else
false
- val _ = map
- (fn mode =>
+ val _ =
+ map (fn mode =>
if length (strip_fun_mode mode) = length (binder_types T)
andalso (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
- else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T
- ^ " at predicate " ^ predname)) ms
+ else
+ error (string_of_mode mode ^ " is not a valid mode for " ^
+ Syntax.string_of_typ ctxt T ^ " at predicate " ^ predname)) ms
val _ =
- if check_consistent_modes ms then ()
- else error (commas (map string_of_mode ms) ^
- " are inconsistent modes for predicate " ^ predname)
+ if check_consistent_modes ms then ()
+ else
+ error (commas (map string_of_mode ms) ^ " are inconsistent modes for predicate " ^ predname)
in
ms
end
+
(* compilation modifiers *)
-structure Comp_Mod =
+structure Comp_Mod = (* FIXME proper signature *)
struct
datatype comp_modifiers = Comp_Modifiers of
@@ -263,29 +274,29 @@
additional_arguments = additional_arguments, wrap_compilation = wrap_compilation,
transform_additional_arguments = transform_additional_arguments})
-end;
+end
fun unlimited_compfuns_of true New_Pos_Random_DSeq =
- New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
+ New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
| unlimited_compfuns_of false New_Pos_Random_DSeq =
- New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
+ New_Neg_Random_Sequence_CompFuns.depth_unlimited_compfuns
| unlimited_compfuns_of true Pos_Generator_DSeq =
- New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
+ New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
| unlimited_compfuns_of false Pos_Generator_DSeq =
- New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
+ New_Neg_DSequence_CompFuns.depth_unlimited_compfuns
| unlimited_compfuns_of _ c =
- raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
+ raise Fail ("No unlimited compfuns for compilation " ^ string_of_compilation c)
fun limited_compfuns_of true Predicate_Compile_Aux.New_Pos_Random_DSeq =
- New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+ New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
| limited_compfuns_of false Predicate_Compile_Aux.New_Pos_Random_DSeq =
- New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
+ New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
| limited_compfuns_of true Pos_Generator_DSeq =
- New_Pos_DSequence_CompFuns.depth_limited_compfuns
+ New_Pos_DSequence_CompFuns.depth_limited_compfuns
| limited_compfuns_of false Pos_Generator_DSeq =
- New_Neg_DSequence_CompFuns.depth_limited_compfuns
+ New_Neg_DSequence_CompFuns.depth_limited_compfuns
| limited_compfuns_of _ c =
- raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
+ raise Fail ("No limited compfuns for compilation " ^ string_of_compilation c)
val depth_limited_comp_modifiers = Comp_Mod.Comp_Modifiers
{
@@ -328,7 +339,7 @@
compfuns = Predicate_Comp_Funs.compfuns,
mk_random = (fn T => fn additional_arguments =>
list_comb (Const(@{const_name Random_Pred.iter},
- [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
+ [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
modify_funT = (fn T =>
let
@@ -354,7 +365,7 @@
compfuns = Predicate_Comp_Funs.compfuns,
mk_random = (fn T => fn additional_arguments =>
list_comb (Const(@{const_name Random_Pred.iter},
- [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
+ [@{typ natural}, @{typ natural}, @{typ Random.seed}] --->
Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
modify_funT = (fn T =>
let
@@ -505,7 +516,7 @@
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-
+
val neg_generator_dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
{
compilation = Neg_Generator_DSeq,
@@ -534,7 +545,7 @@
wrap_compilation = K (K (K (K (K I))))
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
+ }
val neg_generator_cps_comp_modifiers = Comp_Mod.Comp_Modifiers
{
@@ -548,30 +559,32 @@
: (compilation_funs -> string -> typ -> mode -> term list -> term -> term),
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-
+
fun negative_comp_modifiers_of comp_modifiers =
- (case Comp_Mod.compilation comp_modifiers of
- Pos_Random_DSeq => neg_random_dseq_comp_modifiers
- | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
- | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
- | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
- | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
- | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
- | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
- | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
- | _ => comp_modifiers)
+ (case Comp_Mod.compilation comp_modifiers of
+ Pos_Random_DSeq => neg_random_dseq_comp_modifiers
+ | Neg_Random_DSeq => pos_random_dseq_comp_modifiers
+ | New_Pos_Random_DSeq => new_neg_random_dseq_comp_modifiers
+ | New_Neg_Random_DSeq => new_pos_random_dseq_comp_modifiers
+ | Pos_Generator_DSeq => neg_generator_dseq_comp_modifiers
+ | Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
+ | Pos_Generator_CPS => neg_generator_cps_comp_modifiers
+ | Neg_Generator_CPS => pos_generator_cps_comp_modifiers
+ | _ => comp_modifiers)
+
(* term construction *)
-fun mk_v (names, vs) s T = (case AList.lookup (op =) vs s of
- NONE => (Free (s, T), (names, (s, [])::vs))
- | SOME xs =>
- let
- val s' = singleton (Name.variant_list names) s;
- val v = Free (s', T)
- in
- (v, (s'::names, AList.update (op =) (s, v::xs) vs))
- end);
+fun mk_v (names, vs) s T =
+ (case AList.lookup (op =) vs s of
+ NONE => (Free (s, T), (names, (s, [])::vs))
+ | SOME xs =>
+ let
+ val s' = singleton (Name.variant_list names) s;
+ val v = Free (s', T)
+ in
+ (v, (s'::names, AList.update (op =) (s, v::xs) vs))
+ end);
fun distinct_v (Free (s, T)) nvs = mk_v nvs s T
| distinct_v (t $ u) nvs =
@@ -587,7 +600,7 @@
let
fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
let
- val (bs2, i') = mk_bounds T2 i
+ val (bs2, i') = mk_bounds T2 i
val (bs1, i'') = mk_bounds T1 i'
in
(HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
@@ -608,17 +621,17 @@
fold_rev mk_split_abs (binder_types T) inner_term
end
-fun compile_arg compilation_modifiers _ _ param_modes arg =
+fun compile_arg compilation_modifiers _ _ param_modes arg =
let
fun map_params (t as Free (f, T)) =
- (case (AList.lookup (op =) param_modes f) of
- SOME mode =>
- let
- val T' = Comp_Mod.funT_of compilation_modifiers mode T
- in
- mk_Eval_of (Free (f, T'), T) mode
- end
- | NONE => t)
+ (case (AList.lookup (op =) param_modes f) of
+ SOME mode =>
+ let
+ val T' = Comp_Mod.funT_of compilation_modifiers mode T
+ in
+ mk_Eval_of (Free (f, T'), T) mode
+ end
+ | NONE => t)
| map_params t = t
in
map_aterms map_params arg
@@ -654,39 +667,40 @@
val compfuns = Comp_Mod.compfuns compilation_modifiers
fun expr_of (t, deriv) =
(case (t, deriv) of
- (t, Term Input) => SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
+ (t, Term Input) =>
+ SOME (compile_arg compilation_modifiers additional_arguments ctxt param_modes t)
| (_, Term Output) => NONE
| (Const (name, T), Context mode) =>
- (case alternative_compilation_of ctxt name mode of
- SOME alt_comp => SOME (alt_comp compfuns T)
- | NONE =>
- SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
- ctxt name mode,
- Comp_Mod.funT_of compilation_modifiers mode T)))
+ (case alternative_compilation_of ctxt name mode of
+ SOME alt_comp => SOME (alt_comp compfuns T)
+ | NONE =>
+ SOME (Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
+ ctxt name mode,
+ Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
- (case (AList.lookup (op =) param_modes s) of
- SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
- | NONE =>
- let
- val bs = map (pair "x") (binder_types (fastype_of t))
- val bounds = map Bound (rev (0 upto (length bs) - 1))
- in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
+ (case (AList.lookup (op =) param_modes s) of
+ SOME _ => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ | NONE =>
+ let
+ val bs = map (pair "x") (binder_types (fastype_of t))
+ val bounds = map Bound (rev (0 upto (length bs) - 1))
+ in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end)
| (t, Context _) =>
- let
- val bs = map (pair "x") (binder_types (fastype_of t))
- val bounds = map Bound (rev (0 upto (length bs) - 1))
- in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
+ let
+ val bs = map (pair "x") (binder_types (fastype_of t))
+ val bounds = map Bound (rev (0 upto (length bs) - 1))
+ in SOME (fold_rev Term.abs bs (mk_if compfuns (list_comb (t, bounds)))) end
| (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
- (case (expr_of (t1, d1), expr_of (t2, d2)) of
- (NONE, NONE) => NONE
- | (NONE, SOME t) => SOME t
- | (SOME t, NONE) => SOME t
- | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
+ (case (expr_of (t1, d1), expr_of (t2, d2)) of
+ (NONE, NONE) => NONE
+ | (NONE, SOME t) => SOME t
+ | (SOME t, NONE) => SOME t
+ | (SOME t1, SOME t2) => SOME (HOLogic.mk_prod (t1, t2)))
| (t1 $ t2, Mode_App (deriv1, deriv2)) =>
- (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
- (SOME t, NONE) => SOME t
- | (SOME t, SOME u) => SOME (t $ u)
- | _ => error "something went wrong here!"))
+ (case (expr_of (t1, deriv1), expr_of (t2, deriv2)) of
+ (SOME t, NONE) => SOME t
+ | (SOME t, SOME u) => SOME (t $ u)
+ | _ => error "something went wrong here!"))
in
list_comb (the (expr_of (t, deriv)), additional_arguments)
end
@@ -721,51 +735,56 @@
val mode = head_mode_of deriv
val additional_arguments' =
Comp_Mod.transform_additional_arguments compilation_modifiers p additional_arguments
- val (compiled_clause, rest) = case p of
- Prem t =>
- let
- val u =
- compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments'
- val (_, out_ts''') = split_mode mode (snd (strip_comb t))
- val rest = compile_prems out_ts''' vs' names'' ps
- in
- (u, rest)
- end
- | Negprem t =>
- let
- val neg_compilation_modifiers =
- negative_comp_modifiers_of compilation_modifiers
- val u = mk_not compfuns
- (compile_expr neg_compilation_modifiers ctxt (t, deriv) param_modes additional_arguments')
- val (_, out_ts''') = split_mode mode (snd (strip_comb t))
- val rest = compile_prems out_ts''' vs' names'' ps
- in
- (u, rest)
- end
- | Sidecond t =>
- let
- val t = compile_arg compilation_modifiers additional_arguments
- ctxt param_modes t
- val rest = compile_prems [] vs' names'' ps;
- in
- (mk_if compfuns t, rest)
- end
- | Generator (v, T) =>
- let
- val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
- val rest = compile_prems [Free (v, T)] vs' names'' ps;
- in
- (u, rest)
- end
+ val (compiled_clause, rest) =
+ (case p of
+ Prem t =>
+ let
+ val u =
+ compile_expr compilation_modifiers ctxt (t, deriv)
+ param_modes additional_arguments'
+ val (_, out_ts''') = split_mode mode (snd (strip_comb t))
+ val rest = compile_prems out_ts''' vs' names'' ps
+ in
+ (u, rest)
+ end
+ | Negprem t =>
+ let
+ val neg_compilation_modifiers =
+ negative_comp_modifiers_of compilation_modifiers
+ val u =
+ mk_not compfuns
+ (compile_expr neg_compilation_modifiers ctxt (t, deriv)
+ param_modes additional_arguments')
+ val (_, out_ts''') = split_mode mode (snd (strip_comb t))
+ val rest = compile_prems out_ts''' vs' names'' ps
+ in
+ (u, rest)
+ end
+ | Sidecond t =>
+ let
+ val t = compile_arg compilation_modifiers additional_arguments
+ ctxt param_modes t
+ val rest = compile_prems [] vs' names'' ps;
+ in
+ (mk_if compfuns t, rest)
+ end
+ | Generator (v, T) =>
+ let
+ val u = Comp_Mod.mk_random compilation_modifiers T additional_arguments
+ val rest = compile_prems [Free (v, T)] vs' names'' ps;
+ in
+ (u, rest)
+ end)
in
compile_match constr_vs' eqs out_ts''
(mk_bind compfuns (compiled_clause, rest))
end
- val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps;
+ val prem_t = compile_prems in_ts' (map fst param_modes) all_vs' moded_ps
in
mk_bind compfuns (mk_single compfuns inp, prem_t)
end
+
(* switch detection *)
(** argument position of an inductive predicates and the executable functions **)
@@ -776,23 +795,25 @@
| input_positions_pair Output = []
| input_positions_pair (Fun _) = []
| input_positions_pair (Pair (m1, m2)) =
- map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
+ map (cons 1) (input_positions_pair m1) @ map (cons 2) (input_positions_pair m2)
-fun input_positions_of_mode mode = flat (map_index
- (fn (i, Input) => [(i, [])]
- | (_, Output) => []
- | (_, Fun _) => []
- | (i, m as Pair _) => map (pair i) (input_positions_pair m))
- (Predicate_Compile_Aux.strip_fun_mode mode))
+fun input_positions_of_mode mode =
+ flat
+ (map_index
+ (fn (i, Input) => [(i, [])]
+ | (_, Output) => []
+ | (_, Fun _) => []
+ | (i, m as Pair _) => map (pair i) (input_positions_pair m))
+ (Predicate_Compile_Aux.strip_fun_mode mode))
fun argument_position_pair _ [] = []
| argument_position_pair (Pair (Fun _, m2)) (2 :: is) = argument_position_pair m2 is
| argument_position_pair (Pair (m1, m2)) (i :: is) =
- (if eq_mode (m1, Output) andalso i = 2 then
- argument_position_pair m2 is
- else if eq_mode (m2, Output) andalso i = 1 then
- argument_position_pair m1 is
- else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
+ (if eq_mode (m1, Output) andalso i = 2 then
+ argument_position_pair m2 is
+ else if eq_mode (m2, Output) andalso i = 1 then
+ argument_position_pair m1 is
+ else (i :: argument_position_pair (if i = 1 then m1 else m2) is))
fun argument_position_of mode (i, is) =
(i - (length (filter (fn Output => true | Fun _ => true | _ => false)
@@ -804,6 +825,7 @@
| nth_pair (2 :: is) (Const (@{const_name Pair}, _) $ _ $ t2) = nth_pair is t2
| nth_pair _ _ = raise Fail "unexpected input for nth_tuple"
+
(** switch detection analysis **)
fun find_switch_test ctxt (i, is) (ts, _) =
@@ -811,25 +833,25 @@
val t = nth_pair is (nth ts i)
val T = fastype_of t
in
- case T of
+ (case T of
TFree _ => NONE
| Type (Tcon, _) =>
- (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
- NONE => NONE
- | SOME cs =>
- (case strip_comb t of
- (Var _, []) => NONE
- | (Free _, []) => NONE
- | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE))
+ (case Datatype.get_constrs (Proof_Context.theory_of ctxt) Tcon of
+ NONE => NONE
+ | SOME cs =>
+ (case strip_comb t of
+ (Var _, []) => NONE
+ | (Free _, []) => NONE
+ | (Const (c, T), _) => if AList.defined (op =) cs c then SOME (c, T) else NONE)))
end
fun partition_clause ctxt pos moded_clauses =
let
fun insert_list eq (key, value) = AList.map_default eq (key, []) (cons value)
fun find_switch_test' moded_clause (cases, left) =
- case find_switch_test ctxt pos moded_clause of
+ (case find_switch_test ctxt pos moded_clause of
SOME (c, T) => (insert_list (op =) ((c, T), moded_clause) cases, left)
- | NONE => (cases, moded_clause :: left)
+ | NONE => (cases, moded_clause :: left))
in
fold find_switch_test' moded_clauses ([], [])
end
@@ -845,34 +867,36 @@
val partition = partition_clause ctxt input_position moded_clauses
val switch = if (length (fst partition) > 1) then SOME (input_position, partition) else NONE
in
- case ord (switch, best_switch) of LESS => best_switch
- | EQUAL => best_switch | GREATER => switch
+ (case ord (switch, best_switch) of
+ LESS => best_switch
+ | EQUAL => best_switch
+ | GREATER => switch)
end
fun detect_switches moded_clauses =
- case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
+ (case fold (select_best_switch moded_clauses) (input_positions_of_mode mode) NONE of
SOME (best_pos, (switched_on, left_clauses)) =>
Node ((best_pos, map (apsnd detect_switches) switched_on),
detect_switches left_clauses)
- | NONE => Atom moded_clauses
+ | NONE => Atom moded_clauses)
in
detect_switches moded_clauses
end
+
(** compilation of detected switches **)
fun destruct_constructor_pattern (pat, obj) =
(case strip_comb pat of
- (Free _, []) => cons (pat, obj)
+ (Free _, []) => cons (pat, obj)
| (Const (c, T), pat_args) =>
- (case strip_comb obj of
- (Const (c', T'), obj_args) =>
- (if c = c' andalso T = T' then
- fold destruct_constructor_pattern (pat_args ~~ obj_args)
- else raise Fail "pattern and object mismatch")
- | _ => raise Fail "unexpected object")
+ (case strip_comb obj of
+ (Const (c', T'), obj_args) =>
+ (if c = c' andalso T = T' then
+ fold destruct_constructor_pattern (pat_args ~~ obj_args)
+ else raise Fail "pattern and object mismatch")
+ | _ => raise Fail "unexpected object")
| _ => raise Fail "unexpected pattern")
-
fun compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
in_ts' outTs switch_tree =
let
@@ -920,48 +944,55 @@
((map compile_single_case switched_clauses) @
[(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
in
- case compile_switch_tree all_vs ctxt_eqs left_clauses of
+ (case compile_switch_tree all_vs ctxt_eqs left_clauses of
NONE => SOME switch
- | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp))
+ | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp)))
end
in
compile_switch_tree all_vs [] switch_tree
end
+
(* compilation of predicates *)
fun compile_pred options compilation_modifiers ctxt all_vs param_vs s T (pol, mode) moded_cls =
let
- val is_terminating = false (* FIXME: requires an termination analysis *)
+ val is_terminating = false (* FIXME: requires an termination analysis *)
val compilation_modifiers =
(if pol then compilation_modifiers else
negative_comp_modifiers_of compilation_modifiers)
|> (if is_depth_limited_compilation (Comp_Mod.compilation compilation_modifiers) then
(if is_terminating then
- (Comp_Mod.set_compfuns (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
- else
- (Comp_Mod.set_compfuns (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
- else I)
- val additional_arguments = Comp_Mod.additional_arguments compilation_modifiers
- (all_vs @ param_vs)
+ (Comp_Mod.set_compfuns
+ (unlimited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers)))
+ else
+ (Comp_Mod.set_compfuns
+ (limited_compfuns_of pol (Comp_Mod.compilation compilation_modifiers))))
+ else I)
+ val additional_arguments =
+ Comp_Mod.additional_arguments compilation_modifiers (all_vs @ param_vs)
val compfuns = Comp_Mod.compfuns compilation_modifiers
fun is_param_type (T as Type ("fun",[_ , T'])) =
- is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
+ is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
| is_param_type T = is_some (try (dest_monadT compfuns) T)
- val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
- (binder_types T)
+ val (inpTs, outTs) =
+ split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
+ (binder_types T)
val funT = Comp_Mod.funT_of compilation_modifiers mode T
- val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
- (fn T => fn (param_vs, names) =>
- if is_param_type T then
- (Free (hd param_vs, T), (tl param_vs, names))
- else
- let
- val new = singleton (Name.variant_list names) "x"
- in (Free (new, T), (param_vs, new :: names)) end)) inpTs
+ val (in_ts, _) =
+ fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
+ (fn T => fn (param_vs, names) =>
+ if is_param_type T then
+ (Free (hd param_vs, T), (tl param_vs, names))
+ else
+ let
+ val new = singleton (Name.variant_list names) "x"
+ in (Free (new, T), (param_vs, new :: names)) end)) inpTs
(param_vs, (all_vs @ param_vs))
- val in_ts' = map_filter (map_filter_prod
- (fn t as Free (x, _) => if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
+ val in_ts' =
+ map_filter (map_filter_prod
+ (fn t as Free (x, _) =>
+ if member (op =) param_vs x then NONE else SOME t | t => SOME t)) in_ts
val param_modes = param_vs ~~ ho_arg_modes_of mode
val compilation =
if detect_switches options then
@@ -971,9 +1002,9 @@
else
let
val cl_ts =
- map (fn (ts, moded_prems) =>
+ map (fn (ts, moded_prems) =>
compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
- (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls;
+ (HOLogic.mk_tuple in_ts') (split_mode mode ts) moded_prems) moded_cls
in
Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
(if null cl_ts then
@@ -982,12 +1013,12 @@
foldr1 (mk_plus compfuns) cl_ts)
end
val fun_const =
- Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
- ctxt s mode, funT)
+ Const (function_name_of (Comp_Mod.compilation compilation_modifiers) ctxt s mode, funT)
in
HOLogic.mk_Trueprop
(HOLogic.mk_eq (list_comb (fun_const, in_ts @ additional_arguments), compilation))
- end;
+ end
+
(* Definition of executable functions and their intro and elim rules *)
@@ -996,36 +1027,36 @@
| strip_split_abs t = t
fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name Product_Type.prod}, [T1, T2])) names =
- if eq_mode (m, Input) orelse eq_mode (m, Output) then
+ if eq_mode (m, Input) orelse eq_mode (m, Output) then
+ let
+ val x = singleton (Name.variant_list names) "x"
+ in
+ (Free (x, T), x :: names)
+ end
+ else
+ let
+ val (t1, names') = mk_args is_eval (m1, T1) names
+ val (t2, names'') = mk_args is_eval (m2, T2) names'
+ in
+ (HOLogic.mk_prod (t1, t2), names'')
+ end
+ | mk_args is_eval ((m as Fun _), T) names =
+ let
+ val funT = funT_of Predicate_Comp_Funs.compfuns m T
+ val x = singleton (Name.variant_list names) "x"
+ val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
+ val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
+ val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
+ (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
+ in
+ (if is_eval then t else Free (x, funT), x :: names)
+ end
+ | mk_args _ (_, T) names =
let
val x = singleton (Name.variant_list names) "x"
in
(Free (x, T), x :: names)
end
- else
- let
- val (t1, names') = mk_args is_eval (m1, T1) names
- val (t2, names'') = mk_args is_eval (m2, T2) names'
- in
- (HOLogic.mk_prod (t1, t2), names'')
- end
- | mk_args is_eval ((m as Fun _), T) names =
- let
- val funT = funT_of Predicate_Comp_Funs.compfuns m T
- val x = singleton (Name.variant_list names) "x"
- val (args, _) = fold_map (mk_args is_eval) (strip_fun_mode m ~~ binder_types T) (x :: names)
- val (inargs, outargs) = split_map_mode (fn _ => fn t => (SOME t, NONE)) m args
- val t = fold_rev HOLogic.tupled_lambda args (Predicate_Comp_Funs.mk_Eval
- (list_comb (Free (x, funT), inargs), HOLogic.mk_tuple outargs))
- in
- (if is_eval then t else Free (x, funT), x :: names)
- end
- | mk_args is_eval (_, T) names =
- let
- val x = singleton (Name.variant_list names) "x"
- in
- (Free (x, T), x :: names)
- end
fun create_intro_elim_rule ctxt mode defthm mode_id funT pred =
let
@@ -1052,8 +1083,9 @@
val funpropI = HOLogic.mk_Trueprop (Predicate_Comp_Funs.mk_Eval (list_comb (funtrm, inargs),
HOLogic.mk_tuple outargs))
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
- val simprules = [defthm, @{thm eval_pred},
- @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
+ val simprules =
+ [defthm, @{thm eval_pred},
+ @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
val unfolddef_tac =
Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
val introthm = Goal.prove ctxt
@@ -1082,14 +1114,13 @@
((introthm, elimthm), opt_neg_introthm)
end
-fun create_constname_of_mode options thy prefix name _ mode =
+fun create_constname_of_mode options thy prefix name _ mode =
let
- val system_proposal = prefix ^ (Long_Name.base_name name)
- ^ "_" ^ ascii_string_of_mode mode
+ val system_proposal = prefix ^ (Long_Name.base_name name) ^ "_" ^ ascii_string_of_mode mode
val name = the_default system_proposal (proposed_names options name mode)
in
Sign.full_bname thy name
- end;
+ end
fun create_definitions options preds (name, modes) thy =
let
@@ -1181,13 +1212,14 @@
fun dest_prem ctxt params t =
(case strip_comb t of
(v as Free _, _) => if member (op =) params v then Prem t else Sidecond t
- | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem ctxt params t of
- Prem t => Negprem t
- | Negprem _ => error ("Double negation not allowed in premise: " ^
- Syntax.string_of_term ctxt (c $ t))
- | Sidecond t => Sidecond (c $ t))
+ | (c as Const (@{const_name Not}, _), [t]) =>
+ (case dest_prem ctxt params t of
+ Prem t => Negprem t
+ | Negprem _ => error ("Double negation not allowed in premise: " ^
+ Syntax.string_of_term ctxt (c $ t))
+ | Sidecond t => Sidecond (c $ t))
| (Const (s, _), _) =>
- if is_registered ctxt s then Prem t else Sidecond t
+ if is_registered ctxt s then Prem t else Sidecond t
| _ => Sidecond t)
fun prepare_intrs options ctxt prednames intros =
@@ -1204,13 +1236,14 @@
all_smodes_of_typ T
else
all_modes_of_typ T
- val all_modes =
+ val all_modes =
map (fn (s, T) =>
- (s, case proposed_modes options s of
+ (s,
+ (case proposed_modes options s of
SOME ms => check_matches_type ctxt s T ms
- | NONE => generate_modes s T)) preds
+ | NONE => generate_modes s T))) preds
val params =
- case intrs of
+ (case intrs of
[] =>
let
val T = snd (hd preds)
@@ -1223,25 +1256,28 @@
map2 (curry Free) param_names paramTs
end
| (intr :: _) =>
- let
- val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
- val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
- in
- ho_args_of one_mode args
- end
+ let
+ val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+ val one_mode = hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))
+ in
+ ho_args_of one_mode args
+ end)
val param_vs = map (fst o dest_Free) params
fun add_clause intr clauses =
let
- val (Const (name, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
- val prems = map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
+ val (Const (name, _), ts) =
+ strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr))
+ val prems =
+ map (dest_prem ctxt params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intr)
in
- AList.update op = (name, these (AList.lookup op = clauses name) @
- [(ts, prems)]) clauses
+ AList.update op =
+ (name, these (AList.lookup op = clauses name) @ [(ts, prems)])
+ clauses
end;
val clauses = fold add_clause intrs []
in
(preds, all_vs, param_vs, all_modes, clauses)
- end;
+ end
(* sanity check of introduction rules *)
(* TODO: rethink check with new modes *)
@@ -1258,7 +1294,7 @@
else
error ("Format of introduction rule is invalid: tuples must be expanded:"
^ (Syntax.string_of_term_global thy arg) ^ " in " ^
- (Display.string_of_thm_global thy intro))
+ (Display.string_of_thm_global thy intro))
| _ => true
val prems = Logic.strip_imp_prems (prop_of intro)
fun check_prem (Prem t) = forall check_arg args
@@ -1288,6 +1324,7 @@
in forall check prednames end
*)
+
(* create code equation *)
fun add_code_equations ctxt preds result_thmss =
@@ -1321,6 +1358,7 @@
map2 add_code_equation preds result_thmss
end
+
(** main function of predicate compiler **)
datatype steps = Steps of
@@ -1340,11 +1378,12 @@
fun dest_steps (Steps s) = s
val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
val ctxt = Proof_Context.init_global thy
- val _ = print_step options
- ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
- ^ ") for predicates " ^ commas prednames ^ "...")
- (*val _ = check_intros_elim_match thy prednames*)
- (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
+ val _ =
+ print_step options
+ ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation ^
+ ") for predicates " ^ commas prednames ^ "...")
+ (*val _ = check_intros_elim_match thy prednames*)
+ (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
val _ =
if show_intermediate_results options then
tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
@@ -1391,7 +1430,7 @@
in
thy'''
end
-
+
fun gen_add_equations steps options names thy =
let
fun dest_steps (Steps s) = s
@@ -1498,14 +1537,17 @@
(Steps {
define_functions =
fn options => fn preds => fn (s, modes) =>
- let
- val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
- val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
- in define_functions new_pos_random_dseq_comp_modifiers New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
- options preds (s, pos_modes)
- #> define_functions new_neg_random_dseq_comp_modifiers New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
- options preds (s, neg_modes)
- end,
+ let
+ val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+ val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+ in
+ define_functions new_pos_random_dseq_comp_modifiers
+ New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns
+ options preds (s, pos_modes) #>
+ define_functions new_neg_random_dseq_comp_modifiers
+ New_Neg_Random_Sequence_CompFuns.depth_limited_compfuns
+ options preds (s, neg_modes)
+ end,
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = new_pos_random_dseq_comp_modifiers,
@@ -1515,16 +1557,16 @@
val add_generator_dseq_equations = gen_add_equations
(Steps {
define_functions =
- fn options => fn preds => fn (s, modes) =>
- let
- val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
- val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
- in
- define_functions pos_generator_dseq_comp_modifiers New_Pos_DSequence_CompFuns.depth_limited_compfuns
- options preds (s, pos_modes)
- #> define_functions neg_generator_dseq_comp_modifiers New_Neg_DSequence_CompFuns.depth_limited_compfuns
- options preds (s, neg_modes)
- end,
+ fn options => fn preds => fn (s, modes) =>
+ let
+ val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+ val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+ in
+ define_functions pos_generator_dseq_comp_modifiers
+ New_Pos_DSequence_CompFuns.depth_limited_compfuns options preds (s, pos_modes) #>
+ define_functions neg_generator_dseq_comp_modifiers
+ New_Neg_DSequence_CompFuns.depth_limited_compfuns options preds (s, neg_modes)
+ end,
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = pos_generator_dseq_comp_modifiers,
@@ -1534,23 +1576,23 @@
val add_generator_cps_equations = gen_add_equations
(Steps {
define_functions =
- fn options => fn preds => fn (s, modes) =>
- let
- val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
- val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
- in
- define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
- options preds (s, pos_modes)
- #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
- options preds (s, neg_modes)
- end,
+ fn options => fn preds => fn (s, modes) =>
+ let
+ val pos_modes = map_filter (fn (true, m) => SOME m | _ => NONE) modes
+ val neg_modes = map_filter (fn (false, m) => SOME m | _ => NONE) modes
+ in
+ define_functions pos_generator_cps_comp_modifiers Pos_Bounded_CPS_Comp_Funs.compfuns
+ options preds (s, pos_modes)
+ #> define_functions neg_generator_cps_comp_modifiers Neg_Bounded_CPS_Comp_Funs.compfuns
+ options preds (s, neg_modes)
+ end,
prove = prove_by_skip,
add_code_equations = K (K I),
comp_modifiers = pos_generator_cps_comp_modifiers,
use_generators = true,
qname = "generator_cps_equation"})
-
-
+
+
(** user interface **)
(* code_pred_intro attribute *)
@@ -1568,9 +1610,11 @@
val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
-val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
+val values_timeout =
+ Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
-val setup = PredData.put (Graph.empty) #>
+val setup =
+ PredData.put (Graph.empty) #>
Attrib.setup @{binding code_pred_intro} (Scan.lift (Scan.option Args.name) >> attrib' add_intro)
"adding alternative introduction rules for code generation of inductive predicates"
@@ -1592,7 +1636,7 @@
val T = Sign.the_const_type thy' const
val pred = Const (const, T)
val intros = intros_of ctxt' const
- in mk_casesrule lthy' pred intros end
+ in mk_casesrule lthy' pred intros end
val cases_rules = map mk_cases preds
val cases =
map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
@@ -1633,6 +1677,7 @@
val code_pred = generic_code_pred (K I);
val code_pred_cmd = generic_code_pred Code.read_const
+
(* transformation for code generation *)
(* FIXME just one data slot (record) per program unit *)
@@ -1695,13 +1740,16 @@
fun dest_special_compr t =
let
- val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
- | _ => raise TERM ("dest_special_compr", [t])
+ val (inner_t, T_compr) =
+ (case t of
+ (Const (@{const_name Collect}, _) $ Abs (_, T, t)) => (t, T)
+ | _ => raise TERM ("dest_special_compr", [t]))
val (Ts, conj) = apfst (map snd) (Predicate_Compile_Aux.strip_ex inner_t)
val [eq, body] = HOLogic.dest_conj conj
- val rhs = case HOLogic.dest_eq eq of
+ val rhs =
+ (case HOLogic.dest_eq eq of
(Bound i, rhs) => if i = length Ts then rhs else raise TERM ("dest_special_compr", [t])
- | _ => raise TERM ("dest_special_compr", [t])
+ | _ => raise TERM ("dest_special_compr", [t]))
val output_names = Name.variant_list (fold Term.add_free_names [rhs, body] [])
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
val output_frees = map2 (curry Free) output_names (rev Ts)
@@ -1712,9 +1760,11 @@
end
fun dest_general_compr ctxt t_compr =
- let
- val inner_t = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
- | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr);
+ let
+ val inner_t =
+ (case t_compr of
+ (Const (@{const_name Collect}, _) $ t) => t
+ | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
val output_names = Name.variant_list (Term.add_free_names body [])
(map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
@@ -1733,24 +1783,28 @@
val compfuns = Comp_Mod.compfuns comp_modifiers
val all_modes_of = all_modes_of compilation
val (((body, output), T_compr), output_names) =
- case try dest_special_compr t_compr of SOME r => r | NONE => dest_general_compr ctxt t_compr
+ (case try dest_special_compr t_compr of
+ SOME r => r
+ | NONE => dest_general_compr ctxt t_compr)
val (Const (name, _), all_args) =
- case strip_comb body of
+ (case strip_comb body of
(Const (name, T), all_args) => (Const (name, T), all_args)
- | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head)
+ | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head))
in
if defined_functions compilation ctxt name then
let
- fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
- | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
+ fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) =
+ Pair (extract_mode t1, extract_mode t2)
+ | extract_mode (Free (x, _)) =
+ if member (op =) output_names x then Output else Input
| extract_mode _ = Input
val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
fun valid modes1 modes2 =
- case int_ord (length modes1, length modes2) of
+ (case int_ord (length modes1, length modes2) of
GREATER => error "Not enough mode annotations"
| LESS => error "Too many mode annotations"
- | EQUAL => forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
- (modes1 ~~ modes2)
+ | EQUAL =>
+ forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2)) (modes1 ~~ modes2))
fun mode_instance_of (m1, m2) =
let
fun instance_of (Fun _, Input) = true
@@ -1778,12 +1832,14 @@
the_default true (Option.map (valid modes) param_user_modes)
end)
|> map fst
- val deriv = case derivs of
- [] => error ("No mode possible for comprehension "
- ^ Syntax.string_of_term ctxt t_compr)
+ val deriv =
+ (case derivs of
+ [] =>
+ error ("No mode possible for comprehension " ^ Syntax.string_of_term ctxt t_compr)
| [d] => d
- | d :: _ :: _ => (warning ("Multiple modes possible for comprehension "
- ^ Syntax.string_of_term ctxt t_compr); d);
+ | d :: _ :: _ =>
+ (warning ("Multiple modes possible for comprehension " ^
+ Syntax.string_of_term ctxt t_compr); d))
val (_, outargs) = split_mode (head_mode_of deriv) all_args
val t_pred = compile_expr comp_modifiers ctxt
(body, deriv) [] additional_arguments;
@@ -1805,32 +1861,35 @@
in count' 0 xs end
fun accumulate xs = (map (fn x => (x, count xs x)) o sort int_ord o distinct (op =)) xs;
val comp_modifiers =
- case compilation of
- Pred => predicate_comp_modifiers
- | Random => random_comp_modifiers
- | Depth_Limited => depth_limited_comp_modifiers
- | Depth_Limited_Random => depth_limited_random_comp_modifiers
- (*| Annotated => annotated_comp_modifiers*)
- | DSeq => dseq_comp_modifiers
- | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
- | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
- | Pos_Generator_DSeq => pos_generator_dseq_comp_modifiers
+ (case compilation of
+ Pred => predicate_comp_modifiers
+ | Random => random_comp_modifiers
+ | Depth_Limited => depth_limited_comp_modifiers
+ | Depth_Limited_Random => depth_limited_random_comp_modifiers
+ (*| Annotated => annotated_comp_modifiers*)
+ | DSeq => dseq_comp_modifiers
+ | Pos_Random_DSeq => pos_random_dseq_comp_modifiers
+ | New_Pos_Random_DSeq => new_pos_random_dseq_comp_modifiers
+ | Pos_Generator_DSeq => pos_generator_dseq_comp_modifiers)
val compfuns = Comp_Mod.compfuns comp_modifiers
val additional_arguments =
- case compilation of
+ (case compilation of
Pred => []
- | Random => map (HOLogic.mk_number @{typ "natural"}) arguments @
- [@{term "(1, 1) :: natural * natural"}]
+ | Random =>
+ map (HOLogic.mk_number @{typ "natural"}) arguments @
+ [@{term "(1, 1) :: natural * natural"}]
| Annotated => []
| Depth_Limited => [HOLogic.mk_number @{typ "natural"} (hd arguments)]
- | Depth_Limited_Random => map (HOLogic.mk_number @{typ "natural"}) arguments @
- [@{term "(1, 1) :: natural * natural"}]
+ | Depth_Limited_Random =>
+ map (HOLogic.mk_number @{typ "natural"}) arguments @
+ [@{term "(1, 1) :: natural * natural"}]
| DSeq => []
| Pos_Random_DSeq => []
| New_Pos_Random_DSeq => []
- | Pos_Generator_DSeq => []
- val t = analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr;
- val T = dest_monadT compfuns (fastype_of t);
+ | Pos_Generator_DSeq => [])
+ val t =
+ analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr
+ val T = dest_monadT compfuns (fastype_of t)
val t' =
if stats andalso compilation = New_Pos_Random_DSeq then
mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ natural}))
@@ -1890,7 +1949,7 @@
(TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
- thy NONE
+ thy NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.map proc)
t' [] nrandom size seed depth))) ())
@@ -1908,20 +1967,21 @@
val setT = HOLogic.mk_setT T
val elems = HOLogic.mk_set T ts
val ([dots], ctxt') =
- Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
+ Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
(* check expected values *)
val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
val () =
- case raw_expected of
+ (case raw_expected of
NONE => ()
| SOME s =>
if eq_set (op =) (HOLogic.dest_set (Syntax.read_term ctxt s), ts) then ()
else
error ("expected and computed values do not match:\n" ^
"expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
- "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
+ "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n"))
in
- ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics), ctxt')
+ ((if k = ~1 orelse length ts < k then elems else union $ elems $ Free (dots, setT), statistics),
+ ctxt')
end;
fun values_cmd print_modes param_user_modes options k raw_t state =
@@ -1932,9 +1992,9 @@
val ty' = Term.type_of t'
val ctxt'' = Variable.auto_fixes t' ctxt'
val pretty_stat =
- case stats of
- NONE => []
- | SOME xs =>
+ (case stats of
+ NONE => []
+ | SOME xs =>
let
val total = fold (curry (op +)) (map snd xs) 0
fun pretty_entry (s, n) =
@@ -1943,13 +2003,14 @@
Pretty.str (string_of_int n), Pretty.fbrk]
in
[Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
- Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
- @ maps pretty_entry xs
- end
- val p = Print_Mode.with_modes print_modes (fn () =>
+ Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk] @
+ maps pretty_entry xs
+ end)
+ in
+ Print_Mode.with_modes print_modes (fn () =>
Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt'' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt'' ty')]
- @ pretty_stat)) ();
- in Pretty.writeln p end;
+ @ pretty_stat)) ()
+ end |> Pretty.writeln
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 13:33:05 2014 +0100
@@ -11,11 +11,11 @@
val keep_function : theory -> string -> bool
val processed_specs : theory -> string -> (string * thm list) list option
val store_processed_specs : (string * (string * thm list) list) -> theory -> theory
-
+
val get_specification : Predicate_Compile_Aux.options -> theory -> term -> thm list
val obtain_specification_graph :
Predicate_Compile_Aux.options -> theory -> term -> thm list Term_Graph.T
-
+
val present_graph : thm list Term_Graph.T -> unit
val normalize_equation : theory -> thm -> thm
end;
@@ -66,7 +66,7 @@
let
val _ $ u = Logic.strip_imp_concl t
in fst (strip_comb u) end
-(*
+(*
in case pred of
Const (c, T) => c
| _ => raise TERM ("defining_const_of_introrule_term failed: Not a constant", [t])
@@ -75,9 +75,9 @@
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
fun defining_const_of_introrule th =
- case defining_term_of_introrule th
- of Const (c, _) => c
- | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+ (case defining_term_of_introrule th of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th]))
(*TODO*)
fun is_introlike_term _ = true
@@ -85,29 +85,29 @@
val is_introlike = is_introlike_term o prop_of
fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
- (case strip_comb u of
- (Const (_, T), args) =>
- if (length (binder_types T) = length args) then
- true
- else
- raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
- | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
+ (case strip_comb u of
+ (Const (_, T), args) =>
+ if (length (binder_types T) = length args) then
+ true
+ else
+ raise TERM ("check_equation_format_term failed: Number of arguments mismatch", [t])
+ | _ => raise TERM ("check_equation_format_term failed: Not a constant", [t]))
| check_equation_format_term t =
- raise TERM ("check_equation_format_term failed: Not an equation", [t])
+ raise TERM ("check_equation_format_term failed: Not an equation", [t])
val check_equation_format = check_equation_format_term o prop_of
fun defining_term_of_equation_term (Const ("==", _) $ u $ _) = fst (strip_comb u)
| defining_term_of_equation_term t =
- raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
+ raise TERM ("defining_const_of_equation_term failed: Not an equation", [t])
val defining_term_of_equation = defining_term_of_equation_term o prop_of
fun defining_const_of_equation th =
- case defining_term_of_equation th
- of Const (c, _) => c
- | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th])
+ (case defining_term_of_equation th of
+ Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_equation failed: Not a constant", [prop_of th]))
@@ -115,9 +115,10 @@
(* Normalizing equations *)
fun mk_meta_equation th =
- case prop_of th of
- Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) => th RS @{thm eq_reflection}
- | _ => th
+ (case prop_of th of
+ Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _) =>
+ th RS @{thm eq_reflection}
+ | _ => th)
val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
@@ -131,13 +132,13 @@
let
val res = Name.invent_names ctxt s xs
in (res, fold Name.declare (map fst res) ctxt) end
-
+
fun split_all_pairs thy th =
let
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val ((_, [th']), _) = Variable.import true [th] ctxt
val t = prop_of th'
- val frees = Term.add_frees t []
+ val frees = Term.add_frees t []
val freenames = Term.add_free_names t []
val nctxt = Name.make_context freenames
fun mk_tuple_rewrites (x, T) nctxt =
@@ -146,7 +147,7 @@
val (xTs, nctxt') = declare_names x Ts nctxt
val paths = HOLogic.flat_tupleT_paths T
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
- val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
+ val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
val t' = Pattern.rewrite_term thy rewr [] t
val th'' =
Goal.prove ctxt (Term.add_free_names t' []) [] t'
@@ -162,7 +163,7 @@
val ctxt = Proof_Context.init_global thy
val inline_defs = Predicate_Compile_Inline_Defs.get ctxt
val th' = (Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs)) th
- (*val _ = print_step options
+ (*val _ = print_step options
("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
@@ -206,11 +207,13 @@
else
NONE
fun filter_defs ths = map_filter filtering (map (normalize thy o Thm.transfer thy) ths)
- val spec = case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
- [] => (case Spec_Rules.retrieve ctxt t of
- [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
- | ((_, (_, ths)) :: _) => filter_defs ths)
- | ths => rev ths
+ val spec =
+ (case filter_defs (Predicate_Compile_Alternative_Defs.get ctxt) of
+ [] =>
+ (case Spec_Rules.retrieve ctxt t of
+ [] => error ("No specification for " ^ Syntax.string_of_term_global thy t)
+ | ((_, (_, ths)) :: _) => filter_defs ths)
+ | ths => rev ths)
val _ =
if show_intermediate_results options then
tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
@@ -221,38 +224,38 @@
end
val logic_operator_names =
- [@{const_name "=="},
+ [@{const_name "=="},
@{const_name "==>"},
@{const_name Trueprop},
@{const_name Not},
@{const_name HOL.eq},
@{const_name HOL.implies},
@{const_name All},
- @{const_name Ex},
+ @{const_name Ex},
@{const_name HOL.conj},
@{const_name HOL.disj}]
-fun special_cases (c, _) = member (op =) [
- @{const_name Product_Type.Unity},
- @{const_name False},
- @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
- @{const_name Nat.one_nat_inst.one_nat},
- @{const_name Orderings.less}, @{const_name Orderings.less_eq},
- @{const_name Groups.zero},
- @{const_name Groups.one}, @{const_name Groups.plus},
- @{const_name Nat.ord_nat_inst.less_eq_nat},
- @{const_name Nat.ord_nat_inst.less_nat},
-(* FIXME
- @{const_name number_nat_inst.number_of_nat},
-*)
- @{const_name Num.Bit0},
- @{const_name Num.Bit1},
- @{const_name Num.One},
- @{const_name Int.zero_int_inst.zero_int},
- @{const_name List.filter},
- @{const_name HOL.If},
- @{const_name Groups.minus}
- ] c
+fun special_cases (c, _) =
+ member (op =)
+ [@{const_name Product_Type.Unity},
+ @{const_name False},
+ @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
+ @{const_name Nat.one_nat_inst.one_nat},
+ @{const_name Orderings.less}, @{const_name Orderings.less_eq},
+ @{const_name Groups.zero},
+ @{const_name Groups.one}, @{const_name Groups.plus},
+ @{const_name Nat.ord_nat_inst.less_eq_nat},
+ @{const_name Nat.ord_nat_inst.less_nat},
+ (* FIXME
+ @{const_name number_nat_inst.number_of_nat},
+ *)
+ @{const_name Num.Bit0},
+ @{const_name Num.Bit1},
+ @{const_name Num.One},
+ @{const_name Int.zero_int_inst.zero_int},
+ @{const_name List.filter},
+ @{const_name HOL.If},
+ @{const_name Groups.minus}] c
fun obtain_specification_graph options thy t =
@@ -306,13 +309,12 @@
|> map (the o Termtab.lookup mapping)
|> distinct (eq_list eq_cname);
val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-
+
fun namify consts = map string_of_const consts
|> commas;
val prgr = map (fn (consts, constss) =>
- { name = namify consts, ID = namify consts, dir = "", unfold = true,
- path = "", parents = map namify constss, content = [] }) conn;
- in Graph_Display.display_graph prgr end;
+ {name = namify consts, ID = namify consts, dir = "", unfold = true,
+ path = "", parents = map namify constss, content = [] }) conn
+ in Graph_Display.display_graph prgr end
-
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Feb 12 13:33:05 2014 +0100
@@ -32,16 +32,16 @@
SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
handle Pattern.MATCH => NONE) (Item_Net.retrieve net t)
in
- case poss_preds of
+ (case poss_preds of
[p] => SOME p
- | _ => NONE
+ | _ => NONE)
end
fun pred_of_function thy name =
- case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
+ (case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
[] => NONE
| [(_, p)] => SOME (fst (dest_Const p))
- | _ => error ("Multiple matches possible for lookup of constant " ^ name)
+ | _ => error ("Multiple matches possible for lookup of constant " ^ name))
fun defined_const thy name = is_some (pred_of_function thy name)
@@ -49,18 +49,18 @@
Fun_Pred.map (Item_Net.update (f, p))
fun transform_ho_typ (T as Type ("fun", _)) =
- let
- val (Ts, T') = strip_type T
- in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
-| transform_ho_typ t = t
+ let
+ val (Ts, T') = strip_type T
+ in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
+ | transform_ho_typ t = t
-fun transform_ho_arg arg =
- case (fastype_of arg) of
+fun transform_ho_arg arg =
+ (case (fastype_of arg) of
(T as Type ("fun", _)) =>
(case arg of
Free (name, _) => Free (name, transform_ho_typ T)
| _ => raise Fail "A non-variable term at a higher-order position")
- | _ => arg
+ | _ => arg)
fun pred_type T =
let
@@ -88,43 +88,43 @@
end;
fun keep_functions thy t =
- case try dest_Const (fst (strip_comb t)) of
+ (case try dest_Const (fst (strip_comb t)) of
SOME (c, _) => Predicate_Compile_Data.keep_function thy c
- | _ => false
+ | _ => false)
fun flatten thy lookup_pred t (names, prems) =
let
fun lift t (names, prems) =
- case lookup_pred (Envir.eta_contract t) of
+ (case lookup_pred (Envir.eta_contract t) of
SOME pred => [(pred, (names, prems))]
| NONE =>
- let
- val (vars, body) = strip_abs t
- val _ = @{assert} (fastype_of body = body_type (fastype_of body))
- val absnames = Name.variant_list names (map fst vars)
- val frees = map2 (curry Free) absnames (map snd vars)
- val body' = subst_bounds (rev frees, body)
- val resname = singleton (Name.variant_list (absnames @ names)) "res"
- val resvar = Free (resname, fastype_of body)
- val t = flatten' body' ([], [])
- |> map (fn (res, (inner_names, inner_prems)) =>
- let
- fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
- val vTs =
- fold Term.add_frees inner_prems []
- |> filter (fn (x, _) => member (op =) inner_names x)
- val t =
- fold mk_exists vTs
- (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
- map HOLogic.dest_Trueprop inner_prems))
- in
- t
- end)
- |> foldr1 HOLogic.mk_disj
- |> fold lambda (resvar :: rev frees)
- in
- [(t, (names, prems))]
- end
+ let
+ val (vars, body) = strip_abs t
+ val _ = @{assert} (fastype_of body = body_type (fastype_of body))
+ val absnames = Name.variant_list names (map fst vars)
+ val frees = map2 (curry Free) absnames (map snd vars)
+ val body' = subst_bounds (rev frees, body)
+ val resname = singleton (Name.variant_list (absnames @ names)) "res"
+ val resvar = Free (resname, fastype_of body)
+ val t = flatten' body' ([], [])
+ |> map (fn (res, (inner_names, inner_prems)) =>
+ let
+ fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
+ val vTs =
+ fold Term.add_frees inner_prems []
+ |> filter (fn (x, _) => member (op =) inner_names x)
+ val t =
+ fold mk_exists vTs
+ (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
+ map HOLogic.dest_Trueprop inner_prems))
+ in
+ t
+ end)
+ |> foldr1 HOLogic.mk_disj
+ |> fold lambda (resvar :: rev frees)
+ in
+ [(t, (names, prems))]
+ end)
and flatten_or_lift (t, T) (names, prems) =
if fastype_of t = T then
flatten' t (names, prems)
@@ -134,7 +134,7 @@
lift t (names, prems)
else
error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
- ", " ^ Syntax.string_of_typ_global thy T)
+ ", " ^ Syntax.string_of_typ_global thy T)
and flatten' (t as Const _) (names, prems) = [(t, (names, prems))]
| flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
| flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
@@ -156,7 +156,7 @@
(* in general unsound! *)
(res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems)))))
end)
- | Const (@{const_name "Let"}, _) =>
+ | Const (@{const_name "Let"}, _) =>
(let
val (_, [f, g]) = strip_comb t
in
@@ -199,9 +199,10 @@
val args = map (Envir.eta_long []) args
val _ = @{assert} (fastype_of t = body_type (fastype_of t))
val f' = lookup_pred f
- val Ts = case f' of
- SOME pred => (fst (split_last (binder_types (fastype_of pred))))
- | NONE => binder_types (fastype_of f)
+ val Ts =
+ (case f' of
+ SOME pred => (fst (split_last (binder_types (fastype_of pred))))
+ | NONE => binder_types (fastype_of f))
in
folds_map flatten_or_lift (args ~~ Ts) (names, prems) |>
(case f' of
@@ -272,7 +273,8 @@
fun mk_intros ((func, pred), (args, rhs)) =
if (body_type (fastype_of func) = @{typ bool}) then
(* TODO: preprocess predicate definition of rhs *)
- [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
+ [Logic.list_implies
+ ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
else
let
val names = Term.add_free_names rhs []
@@ -316,9 +318,10 @@
let
(*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
val t = HOLogic.dest_Trueprop prem
- val (lit, mk_lit) = case try HOLogic.dest_not t of
+ val (lit, mk_lit) =
+ (case try HOLogic.dest_not t of
SOME t => (t, HOLogic.mk_not)
- | NONE => (t, I)
+ | NONE => (t, I))
val (P, args) = strip_comb lit
in
folds_map (flatten thy lookup_pred) args (names, [])
@@ -342,4 +345,4 @@
map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
end
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Feb 12 13:33:05 2014 +0100
@@ -20,15 +20,15 @@
open Predicate_Compile_Aux
fun is_compound ((Const (@{const_name Not}, _)) $ _) =
- error "is_compound: Negation should not occur; preprocessing is defect"
+ error "is_compound: Negation should not occur; preprocessing is defect"
| is_compound ((Const (@{const_name Ex}, _)) $ _) = true
| is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
| is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
- error "is_compound: Conjunction should not occur; preprocessing is defect"
+ error "is_compound: Conjunction should not occur; preprocessing is defect"
| is_compound _ = false
fun try_destruct_case thy names atom =
- case find_split_thm thy (fst (strip_comb atom)) of
+ (case find_split_thm thy (fst (strip_comb atom)) of
NONE => NONE
| SOME raw_split_thm =>
let
@@ -48,17 +48,17 @@
val vars = map Free (var_names ~~ (map snd vTs))
val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
fun partition_prem_subst prem =
- case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
+ (case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
(Free (x, T), r) => (NONE, SOME ((x, T), r))
- | _ => (SOME prem, NONE)
+ | _ => (SOME prem, NONE))
fun partition f xs =
let
fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
| partition' acc1 acc2 (x :: xs) =
let
val (y, z) = f x
- val acc1' = case y of NONE => acc1 | SOME y' => y' :: acc1
- val acc2' = case z of NONE => acc2 | SOME z' => z' :: acc2
+ val acc1' = (case y of NONE => acc1 | SOME y' => y' :: acc1)
+ val acc2' = (case z of NONE => acc2 | SOME z' => z' :: acc2)
in partition' acc1' acc2' xs end
in partition' [] [] xs end
val (prems'', subst) = partition partition_prem_subst prems'
@@ -67,18 +67,19 @@
fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
val rhs = Envir.expand_term_frees subst pre_rhs
in
- case try_destruct_case thy (var_names @ names') rhs of
+ (case try_destruct_case thy (var_names @ names') rhs of
NONE => [(subst, rhs)]
- | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs
+ | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs)
end
- in SOME (atom', maps mk_subst_rhs assms) end
+ in SOME (atom', maps mk_subst_rhs assms) end)
fun flatten constname atom (defs, thy) =
if is_compound atom then
let
val atom = Envir.beta_norm (Envir.eta_long [] atom)
- val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
- ((Long_Name.base_name constname) ^ "_aux")
+ val constname =
+ singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
+ ((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
val (params, args) = List.partition (is_predT o fastype_of)
(map Free (Term.add_frees atom []))
@@ -92,7 +93,7 @@
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
else
- case (fst (strip_comb atom)) of
+ (case (fst (strip_comb atom)) of
(Const (@{const_name If}, _)) =>
let
val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
@@ -103,28 +104,28 @@
flatten constname atom' (defs, thy)
end
| _ =>
- case try_destruct_case thy [] atom of
- NONE => (atom, (defs, thy))
- | SOME (atom', srs) =>
- let
- val frees = map Free (Term.add_frees atom' [])
- val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
- ((Long_Name.base_name constname) ^ "_aux")
- val full_constname = Sign.full_bname thy constname
- val constT = map fastype_of frees ---> HOLogic.boolT
- val lhs = list_comb (Const (full_constname, constT), frees)
- fun mk_def (subst, rhs) =
- Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
- val new_defs = map mk_def srs
- val (definition, thy') = thy
- |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> fold_map Specification.axiom (* FIXME !?!?!?! *)
- (map_index (fn (i, t) =>
- ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
- in
- (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
- end
-
+ (case try_destruct_case thy [] atom of
+ NONE => (atom, (defs, thy))
+ | SOME (atom', srs) =>
+ let
+ val frees = map Free (Term.add_frees atom' [])
+ val constname =
+ singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
+ ((Long_Name.base_name constname) ^ "_aux")
+ val full_constname = Sign.full_bname thy constname
+ val constT = map fastype_of frees ---> HOLogic.boolT
+ val lhs = list_comb (Const (full_constname, constT), frees)
+ fun mk_def (subst, rhs) =
+ Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+ val new_defs = map mk_def srs
+ val (definition, thy') = thy
+ |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
+ |> fold_map Specification.axiom (* FIXME !?!?!?! *)
+ (map_index (fn (i, t) =>
+ ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
+ in
+ (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
+ end))
fun flatten_intros constname intros thy =
let
@@ -143,7 +144,7 @@
(* TODO: same function occurs in inductive package *)
fun select_disj 1 1 = []
| select_disj _ 1 = [rtac @{thm disjI1}]
- | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1));
+ | select_disj n i = (rtac @{thm disjI2})::(select_disj (n - 1) (i - 1))
fun introrulify thy ths =
let
@@ -258,8 +259,9 @@
|> process constname t1
||>> process constname t2
|>> HOLogic.mk_prod
- | NONE => (warning ("Replacing higher order arguments " ^
- "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
+ | NONE =>
+ (warning ("Replacing higher order arguments " ^
+ "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
else if (is_predT (fastype_of arg)) then
process constname arg (new_defs, thy)
else
@@ -274,7 +276,8 @@
let
val constname = fst (dest_Const (fst (strip_comb
(HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
- val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
+ val (intro_ts, (new_defs, thy)) =
+ fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
val th = Skip_Proof.make_thm thy intro_ts
in
(th, (new_defs, thy))
@@ -290,4 +293,4 @@
(intross', (new_defs, thy'))
end
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 13:33:05 2014 +0100
@@ -22,28 +22,34 @@
open Core_Data;
open Mode_Inference;
+
(* debug stuff *)
fun print_tac options s =
if show_proof_trace options then Tactical.print_tac s else Seq.single;
+
(** auxiliary **)
datatype assertion = Max_number_of_subgoals of int
+
fun assert_tac (Max_number_of_subgoals i) st =
if (nprems_of st <= i) then Seq.single st
- else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :"
- ^ "\n" ^ Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals_without_context st)));
+ else
+ raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :\n" ^
+ Pretty.string_of (Pretty.chunks
+ (Goal_Display.pretty_goals_without_context st)))
(** special setup for simpset **)
+
val HOL_basic_ss' =
simpset_of (put_simpset HOL_basic_ss @{context}
addsimps @{thms simp_thms Pair_eq}
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
+
(* auxillary functions *)
fun is_Type (Type _) = true
@@ -53,15 +59,18 @@
(* which then consequently would be splitted *)
(* else false *)
fun is_constructor thy t =
- if (is_Type (fastype_of t)) then
+ if is_Type (fastype_of t) then
(case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of
NONE => false
- | SOME info => (let
- val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
- val (c, _) = strip_comb t
- in (case c of
- Const (name, _) => member (op =) constr_consts name
- | _ => false) end))
+ | SOME info =>
+ let
+ val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
+ val (c, _) = strip_comb t
+ in
+ (case c of
+ Const (name, _) => member (op =) constr_consts name
+ | _ => false)
+ end)
else false
(* MAJOR FIXME: prove_params should be simple
@@ -73,19 +82,20 @@
val mode = head_mode_of deriv
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
- val f_tac = case f of
- Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm eval_pred}, predfun_definition_of ctxt name mode,
- @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
- @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
- | Free _ =>
- Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
- let
- val prems' = maps dest_conjunct_prem (take nargs prems)
- in
- rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
- end) ctxt 1
- | Abs _ => raise Fail "prove_param: No valid parameter term"
+ val f_tac =
+ (case f of
+ Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+ [@{thm eval_pred}, predfun_definition_of ctxt name mode,
+ @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
+ @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+ | Free _ =>
+ Subgoal.FOCUS_PREMS (fn {context = ctxt', params = params, prems, asms, concl, schematics} =>
+ let
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ in
+ rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end) ctxt 1
+ | Abs _ => raise Fail "prove_param: No valid parameter term")
in
REPEAT_DETERM (rtac @{thm ext} 1)
THEN print_tac options "prove_param"
@@ -97,7 +107,7 @@
end
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
- case strip_comb t of
+ (case strip_comb t of
(Const (name, _), args) =>
let
val mode = head_mode_of deriv
@@ -117,25 +127,25 @@
THEN (REPEAT_DETERM (atac 1))
end
| (Free _, _) =>
- print_tac options "proving parameter call.."
- THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
- let
- val param_prem = nth prems premposition
- val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
- val prems' = maps dest_conjunct_prem (take nargs prems)
- fun param_rewrite prem =
- param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
- val SOME rew_eq = find_first param_rewrite prems'
- val param_prem' = rewrite_rule ctxt'
- (map (fn th => th RS @{thm eq_reflection})
- [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
- param_prem
- in
- rtac param_prem' 1
- end) ctxt 1
- THEN print_tac options "after prove parameter call"
+ print_tac options "proving parameter call.."
+ THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', params, prems, asms, concl, schematics} =>
+ let
+ val param_prem = nth prems premposition
+ val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
+ val prems' = maps dest_conjunct_prem (take nargs prems)
+ fun param_rewrite prem =
+ param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
+ val SOME rew_eq = find_first param_rewrite prems'
+ val param_prem' = rewrite_rule ctxt'
+ (map (fn th => th RS @{thm eq_reflection})
+ [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
+ param_prem
+ in
+ rtac param_prem' 1
+ end) ctxt 1
+ THEN print_tac options "after prove parameter call")
-fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
+fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st
fun prove_match options ctxt nargs out_ts =
let
@@ -154,7 +164,7 @@
(fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
in
- (* make this simpset better! *)
+ (* make this simpset better! *)
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
THEN print_tac options "after prove_match:"
THEN (DETERM (TRY
@@ -176,15 +186,17 @@
THEN print_tac options "after if simplification"
end;
+
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
fun prove_sidecond ctxt t =
let
- fun preds_of t nameTs = case strip_comb t of
- (Const (name, T), args) =>
- if is_registered ctxt name then (name, T) :: nameTs
- else fold preds_of args nameTs
- | _ => nameTs
+ fun preds_of t nameTs =
+ (case strip_comb t of
+ (Const (name, T), args) =>
+ if is_registered ctxt name then (name, T) :: nameTs
+ else fold preds_of args nameTs
+ | _ => nameTs)
val preds = preds_of t []
val defs = map
(fn (pred, T) => predfun_definition_of ctxt pred
@@ -200,88 +212,88 @@
let
val (in_ts, clause_out_ts) = split_mode mode ts;
fun prove_prems out_ts [] =
- (prove_match options ctxt nargs out_ts)
- THEN print_tac options "before simplifying assumptions"
- THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
- THEN print_tac options "before single intro rule"
- THEN Subgoal.FOCUS_PREMS
- (fn {context = ctxt', params, prems, asms, concl, schematics} =>
- let
- val prems' = maps dest_conjunct_prem (take nargs prems)
- in
- rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
- end) ctxt 1
- THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
- | prove_prems out_ts ((p, deriv) :: ps) =
- let
- val premposition = (find_index (equal p) clauses) + nargs
- val mode = head_mode_of deriv
- val rest_tac =
- rtac @{thm bindI} 1
- THEN (case p of Prem t =>
- let
- val (_, us) = strip_comb t
- val (_, out_ts''') = split_mode mode us
- val rec_tac = prove_prems out_ts''' ps
- in
- print_tac options "before clause:"
- (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
- THEN print_tac options "before prove_expr:"
- THEN prove_expr options ctxt nargs premposition (t, deriv)
- THEN print_tac options "after prove_expr:"
- THEN rec_tac
- end
- | Negprem t =>
+ (prove_match options ctxt nargs out_ts)
+ THEN print_tac options "before simplifying assumptions"
+ THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
+ THEN print_tac options "before single intro rule"
+ THEN Subgoal.FOCUS_PREMS
+ (fn {context = ctxt', params, prems, asms, concl, schematics} =>
let
- val (t, args) = strip_comb t
- val (_, out_ts''') = split_mode mode args
- val rec_tac = prove_prems out_ts''' ps
- val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
- val neg_intro_rule =
- Option.map (fn name =>
- the (predfun_neg_intro_of ctxt name mode)) name
- val param_derivations = param_derivations_of deriv
- val params = ho_args_of mode args
+ val prems' = maps dest_conjunct_prem (take nargs prems)
in
- print_tac options "before prove_neg_expr:"
- THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
- @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
- THEN (if (is_some name) then
- print_tac options "before applying not introduction rule"
- THEN Subgoal.FOCUS_PREMS
- (fn {context, params = params, prems, asms, concl, schematics} =>
- rtac (the neg_intro_rule) 1
- THEN rtac (nth prems premposition) 1) ctxt 1
- THEN print_tac options "after applying not introduction rule"
- THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
- THEN (REPEAT_DETERM (atac 1))
- else
- rtac @{thm not_predI'} 1
- (* test: *)
- THEN dtac @{thm sym} 1
- THEN asm_full_simp_tac
- (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
- THEN simp_tac
- (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
- THEN rec_tac
- end
- | Sidecond t =>
- rtac @{thm if_predI} 1
- THEN print_tac options "before sidecond:"
- THEN prove_sidecond ctxt t
- THEN print_tac options "after sidecond:"
- THEN prove_prems [] ps)
- in (prove_match options ctxt nargs out_ts)
- THEN rest_tac
- end;
+ rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+ end) ctxt 1
+ THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
+ | prove_prems out_ts ((p, deriv) :: ps) =
+ let
+ val premposition = (find_index (equal p) clauses) + nargs
+ val mode = head_mode_of deriv
+ val rest_tac =
+ rtac @{thm bindI} 1
+ THEN (case p of Prem t =>
+ let
+ val (_, us) = strip_comb t
+ val (_, out_ts''') = split_mode mode us
+ val rec_tac = prove_prems out_ts''' ps
+ in
+ print_tac options "before clause:"
+ (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
+ THEN print_tac options "before prove_expr:"
+ THEN prove_expr options ctxt nargs premposition (t, deriv)
+ THEN print_tac options "after prove_expr:"
+ THEN rec_tac
+ end
+ | Negprem t =>
+ let
+ val (t, args) = strip_comb t
+ val (_, out_ts''') = split_mode mode args
+ val rec_tac = prove_prems out_ts''' ps
+ val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
+ val neg_intro_rule =
+ Option.map (fn name =>
+ the (predfun_neg_intro_of ctxt name mode)) name
+ val param_derivations = param_derivations_of deriv
+ val params = ho_args_of mode args
+ in
+ print_tac options "before prove_neg_expr:"
+ THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+ [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
+ @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
+ THEN (if (is_some name) then
+ print_tac options "before applying not introduction rule"
+ THEN Subgoal.FOCUS_PREMS
+ (fn {context, params = params, prems, asms, concl, schematics} =>
+ rtac (the neg_intro_rule) 1
+ THEN rtac (nth prems premposition) 1) ctxt 1
+ THEN print_tac options "after applying not introduction rule"
+ THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
+ THEN (REPEAT_DETERM (atac 1))
+ else
+ rtac @{thm not_predI'} 1
+ (* test: *)
+ THEN dtac @{thm sym} 1
+ THEN asm_full_simp_tac
+ (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
+ THEN simp_tac
+ (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+ THEN rec_tac
+ end
+ | Sidecond t =>
+ rtac @{thm if_predI} 1
+ THEN print_tac options "before sidecond:"
+ THEN prove_sidecond ctxt t
+ THEN print_tac options "after sidecond:"
+ THEN prove_prems [] ps)
+ in (prove_match options ctxt nargs out_ts)
+ THEN rest_tac
+ end
val prems_tac = prove_prems in_ts moded_ps
in
print_tac options "Proving clause..."
THEN rtac @{thm bindI} 1
THEN rtac @{thm singleI} 1
THEN prems_tac
- end;
+ end
fun select_sup 1 1 = []
| select_sup _ 1 = [rtac @{thm supI1}]
@@ -303,7 +315,8 @@
(1 upto (length moded_clauses))))
THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
THEN print_tac options "proved one direction"
- end;
+ end
+
(** Proof in the other direction **)
@@ -348,12 +361,13 @@
val mode = head_mode_of deriv
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
- val f_tac = case f of
+ val f_tac =
+ (case f of
Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
(@{thm eval_pred}::(predfun_definition_of ctxt name mode)
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
- | _ => error "prove_param2: illegal parameter term"
+ | _ => error "prove_param2: illegal parameter term")
in
print_tac options "before simplification in prove_args:"
THEN f_tac
@@ -379,23 +393,25 @@
end
| _ => etac @{thm bindE} 1)
-fun prove_sidecond2 options ctxt t = let
- fun preds_of t nameTs = case strip_comb t of
- (Const (name, T), args) =>
- if is_registered ctxt name then (name, T) :: nameTs
- else fold preds_of args nameTs
- | _ => nameTs
- val preds = preds_of t []
- val defs = map
- (fn (pred, T) => predfun_definition_of ctxt pred
- (all_input_of T))
- preds
+fun prove_sidecond2 options ctxt t =
+ let
+ fun preds_of t nameTs =
+ (case strip_comb t of
+ (Const (name, T), args) =>
+ if is_registered ctxt name then (name, T) :: nameTs
+ else fold preds_of args nameTs
+ | _ => nameTs)
+ val preds = preds_of t []
+ val defs = map
+ (fn (pred, T) => predfun_definition_of ctxt pred
+ (all_input_of T))
+ preds
in
- (* only simplify the one assumption *)
- full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
- (* need better control here! *)
- THEN print_tac options "after sidecond2 simplification"
- end
+ (* only simplify the one assumption *)
+ full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
+ (* need better control here! *)
+ THEN print_tac options "after sidecond2 simplification"
+ end
fun prove_clause2 options ctxt pred mode (ts, ps) i =
let
@@ -426,46 +442,48 @@
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
val mode = head_mode_of deriv
- val rest_tac = (case p of
- Prem t =>
- let
- val (_, us) = strip_comb t
- val (_, out_ts''') = split_mode mode us
- val rec_tac = prove_prems2 out_ts''' ps
- in
- (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
- end
- | Negprem t =>
- let
- val (_, args) = strip_comb t
- val (_, out_ts''') = split_mode mode args
- val rec_tac = prove_prems2 out_ts''' ps
- val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
- val param_derivations = param_derivations_of deriv
- val ho_args = ho_args_of mode args
- in
- print_tac options "before neg prem 2"
- THEN etac @{thm bindE} 1
- THEN (if is_some name then
- full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
- [predfun_definition_of ctxt (the name) mode]) 1
- THEN etac @{thm not_predE} 1
- THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
- THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
- else
- etac @{thm not_predE'} 1)
- THEN rec_tac
- end
- | Sidecond t =>
- etac @{thm bindE} 1
- THEN etac @{thm if_predE} 1
- THEN prove_sidecond2 options ctxt t
- THEN prove_prems2 [] ps)
- in print_tac options "before prove_match2:"
- THEN prove_match2 options ctxt out_ts
- THEN print_tac options "after prove_match2:"
- THEN rest_tac
- end;
+ val rest_tac =
+ (case p of
+ Prem t =>
+ let
+ val (_, us) = strip_comb t
+ val (_, out_ts''') = split_mode mode us
+ val rec_tac = prove_prems2 out_ts''' ps
+ in
+ (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
+ end
+ | Negprem t =>
+ let
+ val (_, args) = strip_comb t
+ val (_, out_ts''') = split_mode mode args
+ val rec_tac = prove_prems2 out_ts''' ps
+ val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
+ val param_derivations = param_derivations_of deriv
+ val ho_args = ho_args_of mode args
+ in
+ print_tac options "before neg prem 2"
+ THEN etac @{thm bindE} 1
+ THEN (if is_some name then
+ full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
+ [predfun_definition_of ctxt (the name) mode]) 1
+ THEN etac @{thm not_predE} 1
+ THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
+ THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
+ else
+ etac @{thm not_predE'} 1)
+ THEN rec_tac
+ end
+ | Sidecond t =>
+ etac @{thm bindE} 1
+ THEN etac @{thm if_predE} 1
+ THEN prove_sidecond2 options ctxt t
+ THEN prove_prems2 [] ps)
+ in
+ print_tac options "before prove_match2:"
+ THEN prove_match2 options ctxt out_ts
+ THEN print_tac options "after prove_match2:"
+ THEN rest_tac
+ end
val prems_tac = prove_prems2 in_ts ps
in
print_tac options "starting prove_clause2"
@@ -489,14 +507,15 @@
THEN (
if null moded_clauses then etac @{thm botE} 1
else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
- end;
+ end
+
(** proof procedure **)
fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
let
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
- val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
+ val clauses = (case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [])
in
Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
(if not (skip_proof options) then
@@ -508,6 +527,6 @@
THEN prove_other_direction options ctxt pred mode moded_clauses
THEN print_tac options "proved other direction")
else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
- end;
+ end
-end;
\ No newline at end of file
+end
\ No newline at end of file
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 12 13:33:05 2014 +0100
@@ -9,24 +9,28 @@
type seed = Random_Engine.seed
(*val quickcheck : Proof.context -> term -> int -> term list option*)
val put_pred_result :
- (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred) ->
- Proof.context -> Proof.context;
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ term list Predicate.pred) ->
+ Proof.context -> Proof.context
val put_dseq_result :
- (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed) ->
- Proof.context -> Proof.context;
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+ term list Limited_Sequence.dseq * seed) ->
+ Proof.context -> Proof.context
val put_lseq_result :
- (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
- Proof.context -> Proof.context;
- val put_new_dseq_result : (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
+ (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural ->
+ term list Lazy_Sequence.lazy_sequence) ->
+ Proof.context -> Proof.context
+ val put_new_dseq_result :
+ (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
Proof.context -> Proof.context
val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) ->
Proof.context -> Proof.context
val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
- Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
- -> Quickcheck.result list
- val nrandom : int Unsynchronized.ref;
- val debug : bool Unsynchronized.ref;
- val no_higher_order_predicate : string list Unsynchronized.ref;
+ Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list ->
+ Quickcheck.result list
+ val nrandom : int Unsynchronized.ref
+ val debug : bool Unsynchronized.ref
+ val no_higher_order_predicate : string list Unsynchronized.ref
val setup : theory -> theory
end;
@@ -44,48 +48,48 @@
type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Predicate.pred
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Pred_Result"
-);
-val put_pred_result = Pred_Result.put;
+)
+val put_pred_result = Pred_Result.put
structure Dseq_Result = Proof_Data
(
type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term list Limited_Sequence.dseq * seed
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Dseq_Result"
-);
-val put_dseq_result = Dseq_Result.put;
+)
+val put_dseq_result = Dseq_Result.put
structure Lseq_Result = Proof_Data
(
type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
(* FIXME avoid user error with non-user text *)
fun init _ () = error "Lseq_Result"
-);
-val put_lseq_result = Lseq_Result.put;
+)
+val put_lseq_result = Lseq_Result.put
structure New_Dseq_Result = Proof_Data
(
type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
(* FIXME avoid user error with non-user text *)
fun init _ () = error "New_Dseq_Random_Result"
-);
-val put_new_dseq_result = New_Dseq_Result.put;
+)
+val put_new_dseq_result = New_Dseq_Result.put
structure CPS_Result = Proof_Data
(
type T = unit -> Code_Numeral.natural -> (bool * term list) option
(* FIXME avoid user error with non-user text *)
fun init _ () = error "CPS_Result"
-);
-val put_cps_result = CPS_Result.put;
+)
+val put_cps_result = CPS_Result.put
val target = "Quickcheck"
-val nrandom = Unsynchronized.ref 3;
+val nrandom = Unsynchronized.ref 3
-val debug = Unsynchronized.ref false;
+val debug = Unsynchronized.ref false
-val no_higher_order_predicate = Unsynchronized.ref ([] : string list);
+val no_higher_order_predicate = Unsynchronized.ref ([] : string list)
val options = Options {
expected_modes = NONE,
@@ -98,7 +102,7 @@
show_mode_inference = false,
show_compilation = false,
show_caught_failures = false,
- show_invalid_clauses = false,
+ show_invalid_clauses = false,
skip_proof = false,
compilation = Random,
inductify = true,
@@ -141,7 +145,7 @@
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
show_invalid_clauses = s_ic, skip_proof = s_p,
- compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = _,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -157,7 +161,7 @@
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
show_invalid_clauses = s_ic, skip_proof = s_p,
- compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = _, no_higher_order_predicate = no_ho,
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -173,7 +177,7 @@
show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
show_invalid_clauses = s_ic, skip_proof = s_p,
- compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
+ compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
fail_safe_function_flattening = fs_ff, no_higher_order_predicate = _,
smart_depth_limiting = sm_dl, no_topmost_reordering = re}) =
(Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
@@ -185,7 +189,7 @@
smart_depth_limiting = sm_dl, no_topmost_reordering = re})
-fun get_options () =
+fun get_options () =
set_no_higher_order_predicate (!no_higher_order_predicate)
(if !debug then debug_options else options)
@@ -210,7 +214,7 @@
Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
val mk_gen_bind =
Predicate_Compile_Aux.mk_bind New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
-
+
val mk_cpsT =
Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns
@@ -251,41 +255,41 @@
if member eq_mode modes output_mode then
let
val name = Core_Data.function_name_of compilation ctxt4 full_constname output_mode
- val T =
- case compilation of
+ val T =
+ (case compilation of
Pos_Random_DSeq => mk_randompredT (HOLogic.mk_tupleT (map snd vs'))
| New_Pos_Random_DSeq => mk_new_randompredT (HOLogic.mk_tupleT (map snd vs'))
| Pos_Generator_DSeq => mk_new_dseqT (HOLogic.mk_tupleT (map snd vs'))
| Depth_Limited_Random =>
- [@{typ natural}, @{typ natural}, @{typ natural},
- @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
- | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs'))
+ [@{typ natural}, @{typ natural}, @{typ natural},
+ @{typ Random.seed}] ---> mk_predT (HOLogic.mk_tupleT (map snd vs'))
+ | Pos_Generator_CPS => mk_cpsT (HOLogic.mk_tupleT (map snd vs')))
in
Const (name, T)
end
else error ("Predicate Compile Quickcheck failed: " ^ commas (map string_of_mode modes))
fun mk_Some T = Const (@{const_name "Option.Some"}, T --> Type (@{type_name "Option.option"}, [T]))
val qc_term =
- case compilation of
- Pos_Random_DSeq => mk_bind (prog,
- mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
- | New_Pos_Random_DSeq => mk_new_bind (prog,
- mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
- | Pos_Generator_DSeq => mk_gen_bind (prog,
- mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
- | Pos_Generator_CPS => prog $
- mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
- HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))
- | Depth_Limited_Random => fold_rev absdummy
- [@{typ natural}, @{typ natural}, @{typ natural},
- @{typ Random.seed}]
- (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
- mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
- (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))))
+ (case compilation of
+ Pos_Random_DSeq => mk_bind (prog,
+ mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ | New_Pos_Random_DSeq => mk_new_bind (prog,
+ mk_split_lambda (map Free vs') (mk_new_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ | Pos_Generator_DSeq => mk_gen_bind (prog,
+ mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
+ | Pos_Generator_CPS => prog $
+ mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
+ HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))
+ | Depth_Limited_Random => fold_rev absdummy
+ [@{typ natural}, @{typ natural}, @{typ natural},
+ @{typ Random.seed}]
+ (mk_bind' (list_comb (prog, map Bound (3 downto 0)),
+ mk_split_lambda (map Free vs') (mk_return' (HOLogic.mk_list @{typ term}
+ (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))))
val prog =
case compilation of
Pos_Random_DSeq =>
@@ -310,7 +314,7 @@
g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
qc_term []
in
- fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
+ fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield
(
let
val seed = Random_Engine.next_seed ()
@@ -346,7 +350,7 @@
g depth nrandom size seed |> (Predicate.map o map) proc)
qc_term []
in
- fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
+ fn size => fn nrandom => fn depth => Option.map fst (Predicate.yield
(compiled_term depth nrandom size (Random_Engine.run (fn s => (s, s)))))
end
in
@@ -368,14 +372,14 @@
val _ = if Config.get ctxt Quickcheck.timing then
message (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
in
- case result of NONE => try' (i + 1) | SOME q => SOME q
+ (case result of NONE => try' (i + 1) | SOME q => SOME q)
end
- else
- NONE
+ else NONE
in
try' 0
end
+
(* quickcheck interface functions *)
fun compile_term' compilation options ctxt (t, _) =
@@ -386,7 +390,8 @@
(Code_Numeral.natural_of_integer (!nrandom)) o Code_Numeral.natural_of_integer)
in
Quickcheck.Result
- {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
+ {counterexample =
+ Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
end
@@ -412,14 +417,16 @@
(maps (map snd) correct_inst_goals) []
end
-val smart_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true);
-val smart_slow_exhaustive_active = Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false);
+val smart_exhaustive_active =
+ Attrib.setup_config_bool @{binding quickcheck_smart_exhaustive_active} (K true)
+val smart_slow_exhaustive_active =
+ Attrib.setup_config_bool @{binding quickcheck_slow_smart_exhaustive_active} (K false)
val setup =
- Exhaustive_Generators.setup_exhaustive_datatype_interpretation
+ Exhaustive_Generators.setup_exhaustive_datatype_interpretation
#> Context.theory_map (Quickcheck.add_tester ("smart_exhaustive",
(smart_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_CPS, false))))
#> Context.theory_map (Quickcheck.add_tester ("smart_slow_exhaustive",
(smart_slow_exhaustive_active, test_goals (Predicate_Compile_Aux.Pos_Generator_DSeq, false))))
-end;
+end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Feb 12 13:31:18 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Feb 12 13:33:05 2014 +0100
@@ -6,7 +6,8 @@
signature PREDICATE_COMPILE_SPECIALISATION =
sig
- val find_specialisations : string list -> (string * thm list) list -> theory -> (string * thm list) list * theory
+ val find_specialisations : string list -> (string * thm list) list ->
+ theory -> (string * thm list) list * theory
end;
structure Predicate_Compile_Specialisation : PREDICATE_COMPILE_SPECIALISATION =
@@ -17,10 +18,10 @@
(* table of specialisations *)
structure Specialisations = Theory_Data
(
- type T = (term * term) Item_Net.T;
- val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
- val extend = I;
- val merge = Item_Net.merge;
+ type T = (term * term) Item_Net.T
+ val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst)
+ val extend = I
+ val merge = Item_Net.merge
)
fun specialisation_of thy atom =
@@ -29,7 +30,8 @@
fun import (_, intros) args ctxt =
let
val ((_, intros'), ctxt') = Variable.importT intros ctxt
- val pred' = fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
+ val pred' =
+ fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intros')))))
val Ts = binder_types (fastype_of pred')
val argTs = map fastype_of args
val Tsubst = Type.raw_matches (argTs, Ts) Vartab.empty
@@ -44,17 +46,19 @@
val cnstrs = flat (maps
(map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
(Symtab.dest (Datatype.get_all thy)));
- fun check t = (case strip_comb t of
+ fun check t =
+ (case strip_comb t of
(Var _, []) => (true, true)
| (Free _, []) => (true, true)
| (Const (@{const_name Pair}, _), ts) =>
pairself (forall I) (split_list (map check ts))
- | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
+ | (Const (s, T), ts) =>
+ (case (AList.lookup (op =) cnstrs s, body_type T) of
(SOME (i, Tname), Type (Tname', _)) => (false,
length ts = i andalso Tname = Tname' andalso forall (snd o check) ts)
| _ => (false, false))
| _ => (false, false))
- in check t = (false, true) end;
+ in check t = (false, true) end
fun specialise_intros black_list (pred, intros) pats thy =
let
@@ -91,7 +95,8 @@
SOME intro
end handle Pattern.Unif => NONE)
val specialised_intros_t = map_filter I (map specialise_intro intros)
- val thy' = Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
+ val thy' =
+ Sign.add_consts_i [(Binding.name (Long_Name.base_name constname), constT, NoSyn)] thy
val specialised_intros = map (Skip_Proof.make_thm thy') specialised_intros_t
val exported_intros = Variable.exportT ctxt' ctxt specialised_intros
val [t, specialised_t] = Variable.exportT_terms ctxt' ctxt
@@ -124,29 +129,31 @@
end
and restrict_pattern' thy [] free_names = ([], free_names)
| restrict_pattern' thy ((T, Free (x, _)) :: Tts) free_names =
- let
- val (ts', free_names') = restrict_pattern' thy Tts free_names
- in
- (Free (x, T) :: ts', free_names')
- end
+ let
+ val (ts', free_names') = restrict_pattern' thy Tts free_names
+ in
+ (Free (x, T) :: ts', free_names')
+ end
| restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
- replace_term_and_restrict thy T t Tts free_names
+ replace_term_and_restrict thy T t Tts free_names
| restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
- case Datatype.get_constrs thy Tcon of
- NONE => replace_term_and_restrict thy T t Tts free_names
- | SOME constrs => (case strip_comb t of
- (Const (s, _), ats) => (case AList.lookup (op =) constrs s of
- SOME constr_T =>
- let
- val (Ts', T') = strip_type constr_T
- val Tsubst = Type.raw_match (T', T) Vartab.empty
- val Ts = map (Envir.subst_type Tsubst) Ts'
- val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
- val (ats', ts') = chop (length ats) bts'
- in
- (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
- end
- | NONE => replace_term_and_restrict thy T t Tts free_names))
+ (case Datatype.get_constrs thy Tcon of
+ NONE => replace_term_and_restrict thy T t Tts free_names
+ | SOME constrs =>
+ (case strip_comb t of
+ (Const (s, _), ats) =>
+ (case AList.lookup (op =) constrs s of
+ SOME constr_T =>
+ let
+ val (Ts', T') = strip_type constr_T
+ val Tsubst = Type.raw_match (T', T) Vartab.empty
+ val Ts = map (Envir.subst_type Tsubst) Ts'
+ val (bts', free_names') = restrict_pattern' thy ((Ts ~~ ats) @ Tts) free_names
+ val (ats', ts') = chop (length ats) bts'
+ in
+ (list_comb (Const (s, map fastype_of ats' ---> T), ats') :: ts', free_names')
+ end
+ | NONE => replace_term_and_restrict thy T t Tts free_names)))
fun restrict_pattern thy Ts args =
let
val args = map Logic.unvarify_global args
@@ -155,42 +162,42 @@
val (pat, _) = restrict_pattern' thy (Ts ~~ args) free_names
in map Logic.varify_global pat end
fun detect' atom thy =
- case strip_comb atom of
+ (case strip_comb atom of
(pred as Const (pred_name, _), args) =>
let
- val Ts = binder_types (Sign.the_const_type thy pred_name)
- val pats = restrict_pattern thy Ts args
- in
- if (exists (is_nontrivial_constrt thy) pats)
- orelse (has_duplicates (op =) (fold add_vars pats [])) then
- let
- val thy' =
- case specialisation_of thy atom of
- [] =>
- if member (op =) ((map fst specs) @ black_list) pred_name then
- thy
- else
- (case try (Core_Data.intros_of (Proof_Context.init_global thy)) pred_name of
- NONE => thy
- | SOME [] => thy
- | SOME intros =>
- specialise_intros ((map fst specs) @ (pred_name :: black_list))
- (pred, intros) pats thy)
- | _ :: _ => thy
+ val Ts = binder_types (Sign.the_const_type thy pred_name)
+ val pats = restrict_pattern thy Ts args
+ in
+ if (exists (is_nontrivial_constrt thy) pats)
+ orelse (has_duplicates (op =) (fold add_vars pats [])) then
+ let
+ val thy' =
+ (case specialisation_of thy atom of
+ [] =>
+ if member (op =) ((map fst specs) @ black_list) pred_name then
+ thy
+ else
+ (case try (Core_Data.intros_of (Proof_Context.init_global thy)) pred_name of
+ NONE => thy
+ | SOME [] => thy
+ | SOME intros =>
+ specialise_intros ((map fst specs) @ (pred_name :: black_list))
+ (pred, intros) pats thy)
+ | _ :: _ => thy)
val atom' =
- case specialisation_of thy' atom of
+ (case specialisation_of thy' atom of
[] => atom
| (t, specialised_t) :: _ =>
let
val subst = Pattern.match thy' (t, atom) (Vartab.empty, Vartab.empty)
- in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom
- (*FIXME: this exception could be caught earlier in specialisation_of *)
- in
- (atom', thy')
- end
- else (atom, thy)
- end
- | _ => (atom, thy)
+ in Envir.subst_term subst specialised_t end handle Pattern.MATCH => atom)
+ (*FIXME: this exception could be handled earlier in specialisation_of *)
+ in
+ (atom', thy')
+ end
+ else (atom, thy)
+ end
+ | _ => (atom, thy))
fun specialise' (constname, intros) thy =
let
(* FIXME: only necessary because of sloppy Logic.unvarify in restrict_pattern *)