# HG changeset patch # User wenzelm # Date 1392211965 -3600 # Node ID 721b4561007a8ec3eb6ef343bd7728e57afdc12d # Parent 0ab52bf7b5e6c9b250e1ca8b5431af97f39a1a04# Parent db691cc7928900ab16a54e48b982310959d64dd7 merged, resolving some conflicts; diff -r 0ab52bf7b5e6 -r 721b4561007a Admin/PLATFORMS --- a/Admin/PLATFORMS Wed Feb 12 10:59:25 2014 +0100 +++ b/Admin/PLATFORMS Wed Feb 12 14:32:45 2014 +0100 @@ -122,3 +122,6 @@ identifies the JVM platform. Since a particular Java version is always bundled with Isabelle, the resulting settings also provide some clues about its platform, without running it. + +* Common Unix tools like /bin/sh, /bin/kill, sed, ulimit are + notoriously non-portable an should be avoided. \ No newline at end of file diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Divides.thy --- a/src/HOL/Divides.thy Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Divides.thy Wed Feb 12 14:32:45 2014 +0100 @@ -1968,13 +1968,13 @@ lemma [simp]: shows div_one_bit0: "1 div numeral (Num.Bit0 v) = (0 :: int)" and mod_one_bit0: "1 mod numeral (Num.Bit0 v) = (1 :: int)" - and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)" - and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)" - and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)" - and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v" + and div_one_bit1: "1 div numeral (Num.Bit1 v) = (0 :: int)" + and mod_one_bit1: "1 mod numeral (Num.Bit1 v) = (1 :: int)" + and div_one_neg_numeral: "1 div - numeral v = (- 1 :: int)" + and mod_one_neg_numeral: "1 mod - numeral v = (1 :: int) - numeral v" by (simp_all del: arith_special add: div_pos_pos mod_pos_pos div_pos_neg mod_pos_neg posDivAlg_eqn) - + lemma [simp]: shows div_neg_one_numeral: "- 1 div numeral v = (- 1 :: int)" and mod_neg_one_numeral: "- 1 mod numeral v = numeral v - (1 :: int)" diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Wed Feb 12 14:32:45 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,20 +525,21 @@ | 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 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 @@ -530,9 +550,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]) @@ -558,18 +578,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 @@ -593,8 +615,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 @@ -602,7 +624,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 @@ -622,10 +644,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 = @@ -635,14 +659,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)) @@ -651,7 +677,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 @@ -660,9 +686,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) = @@ -679,6 +706,7 @@ (entry_clause :: p' @ p'', constant_table) end + (* post processing of generated prolog program *) fun post_process ctxt options const_name (p, constant_table) = @@ -696,6 +724,7 @@ |> apfst (reorder_manually (#manual_reorder options)) |> apfst rename_vars_program + (* code printer *) fun write_arith_op Plus = "+" @@ -703,15 +732,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 @@ -723,7 +754,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 *) @@ -733,7 +765,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" ^ @@ -741,7 +773,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" ^ @@ -750,6 +782,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 = @@ -760,18 +793,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 @@ -797,7 +837,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 @@ -814,7 +855,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 @@ -830,23 +872,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 @@ -860,26 +904,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 = @@ -887,9 +932,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 { @@ -919,17 +965,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) @@ -949,7 +997,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)) @@ -961,19 +1009,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 = @@ -984,30 +1035,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 @@ -1028,14 +1080,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 @@ -1043,6 +1098,5 @@ in Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) [] end - - -end; + +end diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Feb 12 14:32:45 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.$$$ "\") -- parse_mode_tuple_expr >> Pair || parse_mode_basic_expr) - xs + (parse_mode_basic_expr --| (Args.$$$ "*" || Args.$$$ "\") -- parse_mode_tuple_expr >> Pair || + parse_mode_basic_expr) xs and parse_mode_expr xs = - (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\") -- parse_mode_expr >> Fun || parse_mode_tuple_expr) xs + (parse_mode_tuple_expr --| (Args.$$$ "=>" || Args.$$$ "\") -- 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 _ = diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Feb 12 14:32:45 2014 +0100 @@ -90,17 +90,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, @@ -162,10 +162,10 @@ 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; +end structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX = struct @@ -212,7 +212,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) @@ -228,7 +228,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 @@ -238,7 +238,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] @@ -259,7 +259,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 @@ -292,8 +292,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) @@ -307,25 +308,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) @@ -334,7 +335,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) @@ -380,28 +382,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" @@ -428,7 +430,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) @@ -439,10 +441,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 @@ -454,25 +457,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}) @@ -494,44 +500,49 @@ fun is_constrt thy = let val cnstrs = get_constrs 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 -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 @@ -542,16 +553,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 @@ -579,12 +592,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 = @@ -594,7 +609,8 @@ fun find_split_thm thy (Const (name, _)) = Option.map #split (Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) name) - | find_split_thm thy _ = NONE + | find_split_thm _ _ = NONE + (* lifting term operations to theorems *) @@ -604,10 +620,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 @@ -621,9 +638,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 @@ -633,7 +650,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" @@ -647,9 +664,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), @@ -667,6 +685,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 { @@ -680,7 +699,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 @@ -693,19 +712,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, @@ -727,7 +749,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) @@ -790,33 +812,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 = @@ -826,23 +852,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 @@ -869,6 +896,7 @@ intro''''' end + (** making case distributivity rules **) (*** this should be part of the datatype package ***) @@ -940,12 +968,14 @@ Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] 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 **) @@ -956,6 +986,7 @@ map_term thy (map_concl f o map_atoms f) intro end + (** remove equalities **) fun remove_equalities thy intro = @@ -966,26 +997,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)) @@ -994,6 +1026,7 @@ map_term thy remove_eqs intro end + (* Some last processing *) fun remove_pointless_clauses intro = @@ -1001,6 +1034,7 @@ [] else [intro] + (* some peephole optimisations *) fun peephole_optimisation thy intro = @@ -1009,7 +1043,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 @@ -1021,60 +1056,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 @@ -1088,11 +1128,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 @@ -1117,28 +1157,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 *) @@ -1151,6 +1192,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 @@ -1159,7 +1201,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 @@ -1172,9 +1214,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) @@ -1182,4 +1225,4 @@ ((((full_constname, constT), vs'), intro), thy1) end -end; +end diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Feb 12 14:32:45 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,26 +833,27 @@ 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 Ctr_Sugar.ctr_sugar_of ctxt Tcon of - NONE => NONE - | SOME {ctrs, ...} => - (case strip_comb t of - (Var _, []) => NONE - | (Free _, []) => NONE - | (Const (c, T), _) => - if AList.defined (op =) (map_filter (try dest_Const) ctrs) c then SOME (c, T) else NONE)) + (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of + NONE => NONE + | SOME {ctrs, ...} => + (case strip_comb t of + (Var _, []) => NONE + | (Free _, []) => NONE + | (Const (c, T), _) => + if AList.defined (op =) (map_filter (try dest_Const) ctrs) 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 @@ -846,34 +869,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 @@ -921,48 +946,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 @@ -972,9 +1004,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 @@ -983,12 +1015,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 *) @@ -997,36 +1029,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 @@ -1053,8 +1085,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 @@ -1083,14 +1116,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 @@ -1182,13 +1214,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 = @@ -1205,13 +1238,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) @@ -1224,25 +1258,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 *) @@ -1259,7 +1296,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 @@ -1289,6 +1326,7 @@ in forall check prednames end *) + (* create code equation *) fun add_code_equations ctxt preds result_thmss = @@ -1322,6 +1360,7 @@ map2 add_code_equation preds result_thmss end + (** main function of predicate compiler **) datatype steps = Steps of @@ -1341,11 +1380,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))) @@ -1392,7 +1432,7 @@ in thy''' end - + fun gen_add_equations steps options names thy = let fun dest_steps (Steps s) = s @@ -1499,14 +1539,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, @@ -1516,16 +1559,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, @@ -1535,23 +1578,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 *) @@ -1569,9 +1612,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" @@ -1593,7 +1638,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 = [], @@ -1634,6 +1679,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 *) @@ -1696,13 +1742,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) @@ -1713,9 +1762,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)) @@ -1734,24 +1785,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 @@ -1779,12 +1834,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; @@ -1806,32 +1863,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})) @@ -1891,7 +1951,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))) ()) @@ -1909,20 +1969,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 = @@ -1933,9 +1994,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) = @@ -1944,13 +2005,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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Feb 12 14:32:45 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 = @@ -309,13 +312,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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Wed Feb 12 14:32:45 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 *) (* returns true if t is an application of a datatype constructor *) @@ -51,7 +57,7 @@ fun is_constructor ctxt t = (case fastype_of t of Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t - | _ => false); + | _ => false) (* MAJOR FIXME: prove_params should be simple - different form of introrule for parameters ? *) @@ -62,19 +68,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" @@ -86,7 +93,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 @@ -106,25 +113,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 @@ -142,7 +149,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 @@ -164,15 +171,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 @@ -188,88 +197,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}] @@ -291,7 +300,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 **) @@ -335,12 +345,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 @@ -366,23 +377,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 @@ -413,46 +426,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" @@ -476,14 +491,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 @@ -495,6 +511,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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Wed Feb 12 14:32:45 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 diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Wed Feb 12 14:32:45 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 @@ -42,17 +44,19 @@ fun is_nontrivial_constrt thy t = let val cnstrs = get_constrs 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 @@ -89,7 +93,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 @@ -123,30 +128,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 Ctr_Sugar.ctr_sugar_of ctxt Tcon of NONE => replace_term_and_restrict thy T t Tts free_names - | SOME {ctrs, ...} => (case strip_comb t of - (Const (s, _), ats) => - (case AList.lookup (op =) (map_filter (try dest_Const) ctrs) 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)) + | SOME {ctrs, ...} => + (case strip_comb t of + (Const (s, _), ats) => + (case AList.lookup (op =) (map_filter (try dest_Const) ctrs) 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 +161,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 *) @@ -203,4 +209,4 @@ fold_map specialise' specs thy end -end; \ No newline at end of file +end \ No newline at end of file diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/prop_logic.ML --- a/src/HOL/Tools/prop_logic.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/prop_logic.ML Wed Feb 12 14:32:45 2014 +0100 @@ -258,12 +258,9 @@ let val fm' = nnf fm (* 'new' specifies the next index that is available to introduce an auxiliary variable *) - (* int ref *) val new = Unsynchronized.ref (maxidx fm' + 1) - (* unit -> int *) fun new_idx () = let val idx = !new in new := idx+1; idx end (* replaces 'And' by an auxiliary variable (and its definition) *) - (* prop_formula -> prop_formula * prop_formula list *) fun defcnf_or (And x) = let val i = new_idx () @@ -279,7 +276,6 @@ (Or (fm1', fm2'), defs1 @ defs2) end | defcnf_or fm = (fm, []) - (* prop_formula -> prop_formula *) fun defcnf_from_nnf True = True | defcnf_from_nnf False = False | defcnf_from_nnf (BoolVar i) = BoolVar i diff -r 0ab52bf7b5e6 -r 721b4561007a src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/HOL/Tools/sat_solver.ML Wed Feb 12 14:32:45 2014 +0100 @@ -108,11 +108,8 @@ (* Note: 'fm' must be given in CNF. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) - fun write_dimacs_cnf_file path fm = let - (* prop_formula -> prop_formula *) fun cnf_True_False_elim True = Or (BoolVar 1, Not (BoolVar 1)) | cnf_True_False_elim False = @@ -120,15 +117,12 @@ | cnf_True_False_elim fm = fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) - (* prop_formula -> int *) fun cnf_number_of_clauses (And (fm1, fm2)) = (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) | cnf_number_of_clauses _ = 1 - (* TextIO.outstream -> unit *) fun write_cnf_file out = let - (* prop_formula -> unit *) fun write_formula True = error "formula is not in CNF" | write_formula False = @@ -170,14 +164,10 @@ (* Note: 'fm' must not contain a variable index less than 1. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> prop_formula -> unit *) - fun write_dimacs_sat_file path fm = let - (* TextIO.outstream -> unit *) fun write_sat_file out = let - (* prop_formula -> unit *) fun write_formula True = TextIO.output (out, "*()") | write_formula False = @@ -243,21 +233,16 @@ (* value of i is taken to be unspecified. *) (* ------------------------------------------------------------------------- *) - (* Path.T -> string * string * string -> result *) - fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = let - (* string -> int list *) fun int_list_from_string s = map_filter Int.fromString (space_explode " " s) - (* int list -> assignment *) fun assignment_from_list [] i = NONE (* the SAT solver didn't provide a value for this variable *) | assignment_from_list (x::xs) i = if x=i then (SOME true) else if x=(~i) then (SOME false) else assignment_from_list xs i - (* int list -> string list -> assignment *) fun parse_assignment xs [] = assignment_from_list xs | parse_assignment xs (line::lines) = @@ -265,7 +250,6 @@ parse_assignment (xs @ int_list_from_string line) lines else assignment_from_list xs - (* string -> string -> bool *) fun is_substring needle haystack = let val length1 = String.size needle @@ -277,7 +261,6 @@ true else is_substring needle (String.substring (haystack, 1, length2-1)) end - (* string list -> result *) fun parse_lines [] = UNKNOWN | parse_lines (line::lines) = @@ -305,7 +288,6 @@ fun read_dimacs_cnf_file path = let - (* string list -> string list *) fun filter_preamble [] = error "problem line not found in DIMACS CNF file" | filter_preamble (line::lines) = @@ -319,12 +301,10 @@ lines else error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" - (* string -> int *) fun int_from_string s = case Int.fromString s of SOME i => i | NONE => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number") - (* int list -> int list list *) fun clauses xs = let val (xs1, xs2) = take_prefix (fn i => i <> 0) xs @@ -377,8 +357,6 @@ (* add_solver: updates 'solvers' by adding a new solver *) (* ------------------------------------------------------------------------- *) - (* string * solver -> unit *) - fun add_solver (name, new_solver) = CRITICAL (fn () => let val the_solvers = !solvers; @@ -393,8 +371,6 @@ (* raised. *) (* ------------------------------------------------------------------------- *) - (* string -> solver *) - fun invoke_solver name = (the o AList.lookup (op =) (!solvers)) name; @@ -413,9 +389,7 @@ let fun enum_solver fm = let - (* int list *) val indices = Prop_Logic.indices fm - (* int list -> int list -> int list option *) (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) fun next_list _ ([]:int list) = NONE @@ -428,10 +402,8 @@ else (* set the lowest bit that wasn't set before, keep the higher bits *) SOME (y::x::xs) - (* int list -> int -> bool *) fun assignment_from_list xs i = member (op =) xs i - (* int list -> SatSolver.result *) fun solver_loop xs = if Prop_Logic.eval (assignment_from_list xs) fm then SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) @@ -463,19 +435,15 @@ (* but that sometimes leads to worse performance due to the *) (* introduction of additional variables. *) val fm' = Prop_Logic.nnf fm - (* int list *) val indices = Prop_Logic.indices fm' - (* int list -> int -> prop_formula *) fun partial_var_eval [] i = BoolVar i | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i - (* int list -> prop_formula -> prop_formula *) fun partial_eval xs True = True | partial_eval xs False = False | partial_eval xs (BoolVar i) = partial_var_eval xs i | partial_eval xs (Not fm) = SNot (partial_eval xs fm) | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) - (* prop_formula -> int list *) fun forced_vars True = [] | forced_vars False = [] | forced_vars (BoolVar i) = [i] @@ -485,7 +453,6 @@ (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) (* precedence, and the next partial evaluation of the formula returns 'False'. *) | forced_vars _ = error "formula is not in negation normal form" - (* int list -> prop_formula -> (int list * prop_formula) *) fun eval_and_force xs fm = let val fm' = partial_eval xs fm @@ -497,10 +464,8 @@ eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) (* the same effect as 'union_int' *) end - (* int list -> int option *) fun fresh_var xs = find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices - (* int list -> prop_formula -> int list option *) (* partial assignment 'xs' *) fun dpll xs fm = let @@ -518,7 +483,6 @@ | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) end end - (* int list -> assignment *) fun assignment_from_list [] i = NONE (* the DPLL procedure didn't provide a value for this variable *) | assignment_from_list (x::xs) i = @@ -603,11 +567,9 @@ in case result of SatSolver.UNSATISFIABLE NONE => (let - (* string list *) val proof_lines = (split_lines o File.read) proofpath handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" (* representation of clauses as ordered lists of literals (with duplicates removed) *) - (* prop_formula -> int list *) fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) = Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) | clause_to_lit_list (Prop_Logic.BoolVar i) = @@ -616,7 +578,6 @@ [~i] | clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." - (* prop_formula -> int *) fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = @@ -625,7 +586,6 @@ (* int list array *) val clauses = Array.array (number_of_clauses, []) (* initialize the 'clauses' array *) - (* prop_formula * int -> int *) fun init_array (Prop_Logic.And (fm1, fm2), n) = init_array (fm2, init_array (fm1, n)) | init_array (fm, n) = @@ -636,7 +596,6 @@ val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1) (* search the 'clauses' array for the given list of literals 'lits', *) (* starting at index '!last_ref_clause + 1' *) - (* int list -> int option *) fun original_clause_id lits = let fun original_clause_id_from index = @@ -658,12 +617,10 @@ in original_clause_id_from (!last_ref_clause + 1) end - (* string -> int *) - fun int_from_string s = ( - case Int.fromString s of + fun int_from_string s = + (case Int.fromString s of SOME i => i - | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") - ) + | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")) (* parse the proof file *) val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 @@ -676,7 +633,6 @@ | NONE => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.") ) val next_id = Unsynchronized.ref (number_of_clauses - 1) - (* string list -> unit *) fun process_tokens [] = () | process_tokens (tok::toks) = @@ -749,7 +705,6 @@ raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." ) else raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") - (* string list -> unit *) fun process_lines [] = () | process_lines (l::ls) = ( @@ -812,14 +767,12 @@ case SatSolver.invoke_solver "zchaff" fm of SatSolver.UNSATISFIABLE NONE => (let - (* string list *) (* FIXME File.tmp_path (!?) *) val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 | cnf_number_of_clauses _ = 1 - (* string -> int *) fun int_from_string s = ( case Int.fromString s of SOME i => i @@ -829,7 +782,6 @@ val clause_offset = Unsynchronized.ref ~1 val clause_table = Unsynchronized.ref (Inttab.empty : int list Inttab.table) val empty_id = Unsynchronized.ref ~1 - (* string list -> unit *) fun process_tokens [] = () | process_tokens (tok::toks) = @@ -910,7 +862,6 @@ raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." ) else raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") - (* string list -> unit *) fun process_lines [] = () | process_lines (l::ls) = ( @@ -1004,16 +955,3 @@ SatSolver.add_solver ("jerusat", jerusat) end; -(* ------------------------------------------------------------------------- *) -(* Add code for other SAT solvers below. *) -(* ------------------------------------------------------------------------- *) - -(* -let - fun mysolver fm = ... -in - SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver -end; - --- the solver is now available as SatSolver.invoke_solver "myname" -*) diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/General/position.scala Wed Feb 12 14:32:45 2014 +0100 @@ -75,11 +75,12 @@ } } - object Id_Range + object Reported { - def unapply(pos: T): Option[(Long, Text.Range)] = + def unapply(pos: T): Option[(Long, String, Text.Range)] = (pos, pos) match { - case (Id(id), Range(range)) => Some((id, range)) + case (Id(id), Range(range)) => + Some((id, File.unapply(pos).getOrElse(""), range)) case _ => None } } diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/General/symbol.scala Wed Feb 12 14:32:45 2014 +0100 @@ -118,8 +118,8 @@ final class Index private(text: CharSequence) { - sealed case class Entry(chr: Int, sym: Int) - val index: Array[Entry] = + private sealed case class Entry(chr: Int, sym: Int) + private val index: Array[Entry] = { val matcher = new Matcher(text) val buf = new mutable.ArrayBuffer[Entry] @@ -133,6 +133,7 @@ } buf.toArray } + def decode(sym1: Int): Int = { val sym = sym1 - 1 diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/PIDE/command.ML Wed Feb 12 14:32:45 2014 +0100 @@ -102,8 +102,14 @@ fun make_file src_path (Exn.Res (_, NONE)) = Exn.interruptible_capture (fn () => read_file master_dir pos src_path) () | make_file src_path (Exn.Res (file, SOME text)) = - let val _ = Position.report pos (Markup.path file) - in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end + let + val _ = Position.report pos (Markup.path file); + val file_pos = + Position.file file (*sic!*) |> + (case Position.get_id (Position.thread_data ()) of + NONE => I + | SOME exec_id => Position.put_id exec_id); + in Exn.Res {src_path = src_path, text = text, pos = file_pos} end | make_file _ (Exn.Exn e) = Exn.Exn e; val src_paths = Keyword.command_files cmd path; diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/PIDE/command.scala Wed Feb 12 14:32:45 2014 +0100 @@ -60,8 +60,13 @@ command: Command, status: List[Markup] = Nil, results: Results = Results.empty, - markup: Markup_Tree = Markup_Tree.empty) + markups: Map[String, Markup_Tree] = Map.empty) { + def get_markup(file_name: String): Markup_Tree = + markups.getOrElse(file_name, Markup_Tree.empty) + + def markup: Markup_Tree = get_markup("") + def markup_to_XML(filter: XML.Elem => Boolean): XML.Body = markup.to_XML(command.range, command.source, filter) @@ -72,10 +77,12 @@ command.source == other.command.source && status == other.status && results == other.results && - markup == other.markup + markups == other.markups private def add_status(st: Markup): State = copy(status = st :: status) - private def add_markup(m: Text.Markup): State = copy(markup = markup + m) + + private def add_markup(file_name: String, m: Text.Markup): State = + copy(markups = markups + (file_name -> (get_markup(file_name) + m))) def + (alt_id: Document_ID.Generic, message: XML.Elem): State = message match { @@ -84,7 +91,7 @@ msg match { case elem @ XML.Elem(markup, Nil) => state.add_status(markup) - .add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!? + .add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!? case _ => java.lang.System.err.println("Ignored status message: " + msg) @@ -93,23 +100,40 @@ case XML.Elem(Markup(Markup.REPORT, _), msgs) => (this /: msgs)((state, msg) => - msg match { - case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args) - if (id == command.id || id == alt_id) && - command.range.contains(command.decode(raw_range)) => - val range = command.decode(raw_range) - val props = Position.purge(atts) - val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(info) - case XML.Elem(Markup(name, atts), args) - if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => - val range = command.proper_range - val props = Position.purge(atts) - val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) - state.add_markup(info) - case _ => - // FIXME java.lang.System.err.println("Ignored report message: " + msg) - state + { + def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg) + + msg match { + case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args) + if id == command.id || id == alt_id => + command.chunks.get(file_name) match { + case Some(chunk) => + val range = chunk.decode(raw_range) + if (chunk.range.contains(range)) { + val props = Position.purge(atts) + val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) + state.add_markup(file_name, info) + } + else { + bad() + state + } + case None => + bad() + state + } + + case XML.Elem(Markup(name, atts), args) + if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) => + val range = command.proper_range + val props = Position.purge(atts) + val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args)) + state.add_markup("", info) + + case _ => + // FIXME bad() + state + } }) case XML.Elem(Markup(name, props), body) => props match { @@ -117,14 +141,15 @@ val message1 = XML.Elem(Markup(Markup.message(name), props), body) val message2 = XML.Elem(Markup(name, props), body) - val st0 = copy(results = results + (i -> message1)) - val st1 = - if (Protocol.is_inlined(message)) - (st0 /: Protocol.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, message2))) - else st0 + var st = copy(results = results + (i -> message1)) + if (Protocol.is_inlined(message)) { + for { + (file_name, chunk) <- command.chunks + range <- Protocol.message_positions(command.id, alt_id, chunk, message) + } st = st.add_markup(file_name, Text.Info(range, message2)) + } + st - st1 case _ => java.lang.System.err.println("Ignored message without serial number: " + message) this @@ -135,7 +160,32 @@ copy( status = other.status ::: status, results = results ++ other.results, - markup = markup ++ other.markup) + markups = + (markups.keySet ++ other.markups.keySet) + .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap + ) + } + + + + /** static content **/ + + /* text chunks */ + + abstract class Chunk + { + def file_name: String + def length: Int + def range: Text.Range + def decode(r: Text.Range): Text.Range + } + + class File(val file_name: String, text: CharSequence) extends Chunk + { + val length = text.length + val range = Text.Range(0, length) + private val symbol_index = Symbol.Index(text) + def decode(r: Text.Range): Text.Range = symbol_index.decode(r) } @@ -144,7 +194,7 @@ def name(span: List[Token]): String = span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" } - type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])] + type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])] def apply( id: Document_ID.Command, @@ -220,6 +270,7 @@ val source: String, val init_results: Command.Results, val init_markup: Markup_Tree) + extends Command.Chunk { /* classification */ @@ -243,11 +294,17 @@ for (Exn.Res((name, _)) <- blobs) yield name def blobs_digests: List[SHA1.Digest] = - for (Exn.Res((_, Some(digest))) <- blobs) yield digest + for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest + + val chunks: Map[String, Command.Chunk] = + (("" -> this) :: + (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap /* source */ + def file_name: String = "" + def length: Int = source.length val range: Text.Range = Text.Range(0, length) @@ -256,7 +313,7 @@ def source(range: Text.Range): String = source.substring(range.start, range.stop) - lazy val symbol_index = Symbol.Index(source) + private lazy val symbol_index = Symbol.Index(source) def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) def decode(r: Text.Range): Text.Range = symbol_index.decode(r) @@ -264,7 +321,7 @@ /* accumulated results */ val init_state: Command.State = - Command.State(this, results = init_results, markup = init_markup) + Command.State(this, results = init_results, markups = Map("" -> init_markup)) val empty_state: Command.State = Command.State(this) } diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/PIDE/document.scala Wed Feb 12 14:32:45 2014 +0100 @@ -47,7 +47,7 @@ type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] - type Blobs = Map[Node.Name, Bytes] + type Blobs = Map[Node.Name, (Bytes, Command.File)] object Node { @@ -192,6 +192,7 @@ } final class Node private( + val is_blob: Boolean = false, val header: Node.Header = Node.bad_header("Bad theory header"), val perspective: Node.Perspective_Command = Node.Perspective(false, Command.Perspective.empty, Node.Overlays.empty), @@ -199,11 +200,13 @@ { def clear: Node = new Node(header = header) + def init_blob: Node = new Node(is_blob = true) + def update_header(new_header: Node.Header): Node = - new Node(new_header, perspective, _commands) + new Node(is_blob, new_header, perspective, _commands) def update_perspective(new_perspective: Node.Perspective_Command): Node = - new Node(header, new_perspective, _commands) + new Node(is_blob, header, new_perspective, _commands) def same_perspective(other_perspective: Node.Perspective_Command): Boolean = perspective.required == other_perspective.required && @@ -215,7 +218,7 @@ def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this - else new Node(header, perspective, Node.Commands(new_commands)) + else new Node(is_blob, header, perspective, Node.Commands(new_commands)) def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.range(i) @@ -361,6 +364,7 @@ val node_name: Node.Name val node: Node + val thy_load_commands: List[Command] def eq_content(other: Snapshot): Boolean def cumulate_markup[A]( range: Text.Range, @@ -608,28 +612,51 @@ val node_name = name val node = version.nodes(name) + val thy_load_commands: List[Command] = + if (node_name.is_theory) Nil + else version.nodes.thy_load_commands(node_name) + def eq_content(other: Snapshot): Boolean = + { + def eq_commands(commands: (Command, Command)): Boolean = + state.command_state(version, commands._1) eq_content + other.state.command_state(other.version, commands._2) + !is_outdated && !other.is_outdated && - node.commands.size == other.node.commands.size && - ((node.commands.iterator zip other.node.commands.iterator) forall { - case (cmd1, cmd2) => - state.command_state(version, cmd1) eq_content - other.state.command_state(other.version, cmd2) - }) + node.commands.size == other.node.commands.size && + (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) && + thy_load_commands.length == other.thy_load_commands.length && + (thy_load_commands zip other.thy_load_commands).forall(eq_commands) + } def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]], result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] = { val former_range = revert(range) - (for { - (command, command_start) <- node.command_range(former_range) - st = state.command_state(version, command) - res = result(st) - Text.Info(r0, a) <- st.markup.cumulate[A]( - (former_range - command_start).restrict(command.range), info, elements, - { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) } - ).iterator - } yield Text.Info(convert(r0 + command_start), a)).toList + thy_load_commands match { + case thy_load_command :: _ => + val file_name = node_name.node + (for { + chunk <- thy_load_command.chunks.get(file_name).iterator + st = state.command_state(version, thy_load_command) + res = result(st) + Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A]( + former_range.restrict(chunk.range), info, elements, + { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) } + ).iterator + } yield Text.Info(convert(r0), a)).toList + + case _ => + (for { + (command, command_start) <- node.command_range(former_range) + st = state.command_state(version, command) + res = result(st) + Text.Info(r0, a) <- st.markup.cumulate[A]( + (former_range - command_start).restrict(command.range), info, elements, + { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) } + ).iterator + } yield Text.Info(convert(r0 + command_start), a)).toList + } } def select_markup[A](range: Text.Range, elements: Option[Set[String]], diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/PIDE/protocol.scala Wed Feb 12 14:32:45 2014 +0100 @@ -274,33 +274,32 @@ private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) - def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = + def message_positions( + command_id: Document_ID.Command, + alt_id: Document_ID.Generic, + chunk: Command.Chunk, + message: XML.Elem): Set[Text.Range] = { - def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body) - : Set[Text.Range] = - { - val range = command.decode(raw_range).restrict(command.range) - body.foldLeft(if (range.is_singularity) set else set + range)(positions) - } + def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = + props match { + case Position.Reported(id, file_name, range) + if (id == command_id || id == alt_id) && file_name == chunk.file_name => + val range1 = chunk.decode(range).restrict(chunk.range) + if (range1.is_singularity) set else set + range1 + case _ => set + } def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = tree match { - case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body) - if include_pos(name) && id == command.id => elem_positions(range, set, body) - - case XML.Elem(Markup(name, Position.Id_Range(id, range)), body) - if include_pos(name) && id == command.id => elem_positions(range, set, body) - - case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions) - - case XML.Elem(_, body) => body.foldLeft(set)(positions) - - case _ => set + case XML.Wrapped_Elem(Markup(name, props), _, body) => + body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions) + case XML.Elem(Markup(name, props), body) => + body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions) + case XML.Text(_) => set } val set = positions(Set.empty, message) - if (set.isEmpty) - set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) + if (set.isEmpty) elem_positions(message.markup.properties, set) else set } } @@ -323,7 +322,7 @@ val encode_blob: T[Command.Blob] = variant(List( { case Exn.Res((a, b)) => - (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) }, + (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) YXML.string_of_body(list(encode_blob)(command.blobs)) } diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/System/session.scala --- a/src/Pure/System/session.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/System/session.scala Wed Feb 12 14:32:45 2014 +0100 @@ -379,7 +379,7 @@ digest <- command.blobs_digests if !global_state().defined_blob(digest) } { - doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match { + doc_blobs.collectFirst({ case (_, (b, _)) if b.sha1_digest == digest => b }) match { case Some(blob) => global_state >> (_.define_blob(digest)) prover.get.define_blob(blob) diff -r 0ab52bf7b5e6 -r 721b4561007a src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Wed Feb 12 14:32:45 2014 +0100 @@ -264,11 +264,16 @@ doc_blobs: Document.Blobs) : List[Command.Blob] = { - span_files(syntax, span).map(file => + span_files(syntax, span).map(file_name => Exn.capture { val name = - Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file))) - (name, doc_blobs.get(name).map(_.sha1_digest)) + Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file_name))) + val blob = + doc_blobs.get(name) match { + case Some((bytes, file)) => Some((bytes.sha1_digest, file)) + case None => None + } + (name, blob) } ) } @@ -402,14 +407,17 @@ edit match { case (_, Document.Node.Clear()) => node.clear - case (_, Document.Node.Blob()) => node + case (_, Document.Node.Blob()) => node.init_blob case (name, Document.Node.Edits(text_edits)) => - val commands0 = node.commands - val commands1 = edit_text(text_edits, commands0) - val commands2 = - recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) - node.update_commands(commands2) + if (node.is_blob) node + else { + val commands0 = node.commands + val commands1 = edit_text(text_edits, commands0) + val commands2 = + recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1) + node.update_commands(commands2) + } case (_, Document.Node.Deps(_)) => node diff -r 0ab52bf7b5e6 -r 721b4561007a src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Wed Feb 12 14:32:45 2014 +0100 @@ -106,10 +106,13 @@ val snapshot = this.snapshot() val document_view_ranges = - for { - doc_view <- PIDE.document_views(buffer) - range <- doc_view.perspective(snapshot).ranges - } yield range + if (is_theory) { + for { + doc_view <- PIDE.document_views(buffer) + range <- doc_view.perspective(snapshot).ranges + } yield range + } + else Nil val thy_load_ranges = for { @@ -131,18 +134,19 @@ /* blob */ - private var _blob: Option[Bytes] = None // owned by Swing thread + private var _blob: Option[(Bytes, Command.File)] = None // owned by Swing thread private def reset_blob(): Unit = Swing_Thread.require { _blob = None } - def blob(): Bytes = + def blob(): (Bytes, Command.File) = Swing_Thread.require { _blob match { - case Some(b) => b + case Some(x) => x case None => val b = PIDE.thy_load.file_content(buffer) - _blob = Some(b) - b + val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength)) + _blob = Some((b, file)) + (b, file) } } @@ -163,7 +167,8 @@ node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), node_name -> perspective) else - List(node_name -> Document.Node.Blob()) + List(node_name -> Document.Node.Blob(), + node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text)))) } def node_edits( @@ -186,7 +191,8 @@ node_name -> perspective) } else - List(node_name -> Document.Node.Blob()) + List(node_name -> Document.Node.Blob(), + node_name -> Document.Node.Edits(text_edits)) } diff -r 0ab52bf7b5e6 -r 721b4561007a src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Wed Feb 12 14:32:45 2014 +0100 @@ -210,14 +210,18 @@ if (model.buffer == text_area.getBuffer) { val snapshot = model.snapshot() - if (changed.assignment || + val thy_load_changed = + snapshot.thy_load_commands.exists(changed.commands.contains) + + if (changed.assignment || thy_load_changed || (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) Swing_Thread.later { overview.delay_repaint.invoke() } val visible_lines = text_area.getVisibleLines if (visible_lines > 0) { - if (changed.assignment) text_area.invalidateScreenLineRange(0, visible_lines) + if (changed.assignment || thy_load_changed) + text_area.invalidateScreenLineRange(0, visible_lines) else { val visible_range = JEdit_Lib.visible_range(text_area).get val visible_cmds = diff -r 0ab52bf7b5e6 -r 721b4561007a src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Feb 12 14:32:45 2014 +0100 @@ -148,8 +148,9 @@ { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { - Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match { - case Some(snapshot) => + Swing_Thread.now { Document_Model(buffer) } match { + case Some(model) if model.is_theory => + val snapshot = model.snapshot val root = data.root for ((command, command_start) <- snapshot.node.command_range() if !stopped) { Isabelle_Sidekick.swing_markup_tree( @@ -171,7 +172,7 @@ }) } true - case None => false + case _ => false } } } diff -r 0ab52bf7b5e6 -r 721b4561007a src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Feb 12 14:32:45 2014 +0100 @@ -69,7 +69,7 @@ val buffer = view.getBuffer PIDE.document_view(text_area) match { - case Some(doc_view) => + case Some(doc_view) if doc_view.model.is_theory => val node = snapshot.version.nodes(doc_view.model.node_name) val caret = snapshot.revert(text_area.getCaretPosition) if (caret < buffer.getLength) { @@ -81,7 +81,7 @@ else None } else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) - case None => + case _ => PIDE.document_model(buffer) match { case Some(model) if !model.is_theory => snapshot.version.nodes.thy_load_commands(model.node_name) match { diff -r 0ab52bf7b5e6 -r 721b4561007a src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Feb 12 10:59:25 2014 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Wed Feb 12 14:32:45 2014 +0100 @@ -114,12 +114,10 @@ val model = Document_Model.init(session, buffer, node_name) (model.init_edits(), model) } - if (model.is_theory) { - for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) { - if (document_view(text_area).map(_.model) != Some(model)) - Document_View.init(model, text_area) - } - } + for { + text_area <- JEdit_Lib.jedit_text_areas(buffer) + if document_view(text_area).map(_.model) != Some(model) + } Document_View.init(model, text_area) model_edits ::: edits } } @@ -132,8 +130,8 @@ { JEdit_Lib.swing_buffer_lock(buffer) { document_model(buffer) match { - case Some(model) if model.is_theory => Document_View.init(model, text_area) - case _ => + case Some(model) => Document_View.init(model, text_area) + case None => } } }