--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Nov 12 23:24:40 2012 +0100
@@ -212,8 +212,7 @@
fun PEEK f dependent_tactic st = dependent_tactic (f st) st
fun meta_eq_of th = th RS @{thm eq_reflection}
val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]
- fun instantiate i n {context = ctxt, params = p, prems = prems,
- asms = a, concl = cl, schematics = s} =
+ fun instantiate i n {context, params, prems, asms, concl, schematics} =
let
fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t)
fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
@@ -293,10 +292,10 @@
fun add_intro (opt_case_name, thm) thy =
let
- val (name, T) = dest_Const (fst (strip_intro_concl thm))
+ val (name, _) = dest_Const (fst (strip_intro_concl thm))
fun cons_intro gr =
case try (Graph.get_node gr) name of
- SOME pred_data => Graph.map_node name (map_pred_data
+ 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
@@ -386,9 +385,6 @@
val pred = Const (name, Sign.the_const_type thy name)
val ctxt = Proof_Context.init_global thy
val elim_t = mk_casesrule ctxt pred (map snd named_intros')
- val nparams = (case try (Inductive.the_inductive ctxt) name of
- SOME (_, result) => length (Inductive.params_of (#raw_induct result))
- | NONE => 0)
val elim' = prove_casesrule ctxt (pred, (elim, 0)) elim_t
in
((named_intros', SOME elim'), true)
@@ -417,7 +413,7 @@
(* thm refl is a dummy thm *)
val modes = map fst compilations
val (needs_random, non_random_modes) = pairself (map fst)
- (List.partition (fn (m, (fun_name, random)) => random) compilations)
+ (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
--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Mon Nov 12 23:24:40 2012 +0100
@@ -60,13 +60,6 @@
datatype mode_derivation = Mode_App of mode_derivation * mode_derivation | Context of mode
| Mode_Pair of mode_derivation * mode_derivation | Term of mode
-fun string_of_derivation (Mode_App (m1, m2)) =
- "App (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
- | string_of_derivation (Mode_Pair (m1, m2)) =
- "Pair (" ^ string_of_derivation m1 ^ ", " ^ string_of_derivation m2 ^ ")"
- | string_of_derivation (Term m) = "Term (" ^ string_of_mode m ^ ")"
- | string_of_derivation (Context m) = "Context (" ^ string_of_mode m ^ ")"
-
fun strip_mode_derivation deriv =
let
fun strip (Mode_App (deriv1, deriv2)) ds = strip deriv1 (deriv2 :: ds)
@@ -118,43 +111,20 @@
(Syntax.string_of_term ctxt t) ^ "(sidecondition)"
| string_of_prem ctxt _ = raise Fail "string_of_prem: unexpected input"
-fun string_of_clause ctxt pred (ts, prems) =
- (space_implode " --> "
- (map (string_of_prem ctxt) prems)) ^ " --> " ^ pred ^ " "
- ^ (space_implode " " (map (Syntax.string_of_term ctxt) ts))
-
type mode_analysis_options =
{use_generators : bool,
reorder_premises : bool,
infer_pos_and_neg_modes : bool}
-fun is_constrt thy =
- let
- val cnstrs = flat (maps
- (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
- (Symtab.dest (Datatype.get_all thy)));
- fun check t = (case strip_comb t of
- (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
- | _ => false)
- | _ => false)
- in check end;
-
(*** check if a type is an equality type (i.e. doesn't contain fun)
FIXME this is only an approximation ***)
fun is_eqT (Type (s, Ts)) = s <> "fun" andalso forall is_eqT Ts
| is_eqT _ = true;
-fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
+fun term_vs tm = fold_aterms (fn Free (x, _) => cons x | _ => I) tm [];
val terms_vs = distinct (op =) o maps term_vs;
-(** collect all Frees in a term (with duplicates!) **)
-fun term_vTs tm =
- fold_aterms (fn Free xT => cons xT | _ => I) tm [];
-
-fun print_failed_mode options thy modes p (pol, m) rs is =
+fun print_failed_mode options p (_, m) is =
if show_mode_inference options then
let
val _ = tracing ("Clauses " ^ commas (map (fn i => string_of_int (i + 1)) is) ^ " of " ^
@@ -162,7 +132,7 @@
in () end
else ()
-fun error_of p (pol, m) is =
+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
@@ -195,27 +165,10 @@
fold find' xs NONE
end
-fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
-val terms_vs = distinct (op =) o maps term_vs;
-
-fun input_mode T =
- let
- val (Ts, U) = strip_type T
- in
- fold_rev (curry Fun) (map (K Input) Ts) Input
- end
-
-fun output_mode T =
- let
- val (Ts, U) = strip_type T
- in
- fold_rev (curry Fun) (map (K Output) Ts) Output
- end
-
fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f
| is_invertible_function ctxt _ = false
-fun non_invertible_subterms ctxt (t as Free _) = []
+fun non_invertible_subterms ctxt (Free _) = []
| non_invertible_subterms ctxt t =
let
val (f, args) = strip_comb t
@@ -281,7 +234,7 @@
| output_terms (t, Term Output) = [t]
| output_terms _ = []
-fun lookup_mode modes (Const (s, T)) =
+fun lookup_mode modes (Const (s, _)) =
(case (AList.lookup (op =) modes s) of
SOME ms => SOME (map (fn m => (Context m, [])) ms)
| NONE => NONE)
@@ -312,7 +265,7 @@
end*)
(case try (all_derivations_of ctxt modes vs) t of
SOME derivs =>
- filter (fn (d, mvars) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
+ filter (fn (d, _) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs
| NONE => (if is_all_input m then [(Context m, [])] else []))
| derivations_of ctxt modes vs t m =
if eq_mode (m, Input) then
@@ -353,7 +306,7 @@
SOME (s, _) =>
(case AList.lookup (op =) modes s of
SOME ms =>
- (case AList.lookup (op =) (map (fn ((p, m), r) => (m, r)) ms) (head_mode_of deriv) of
+ (case AList.lookup (op =) (map (fn ((_, m), r) => (m, r)) ms) (head_mode_of deriv) of
SOME r => r
| NONE => false)
| NONE => false)
@@ -370,21 +323,16 @@
length (filter contains_output args)
end
-fun lex_ord ord1 ord2 (x, x') =
- case ord1 (x, x') of
- EQUAL => ord2 (x, x')
- | ord => ord
-
fun lexl_ord [] (x, x') = EQUAL
| lexl_ord (ord :: ords') (x, x') =
case ord (x, x') of
EQUAL => lexl_ord ords' (x, x')
| ord => ord
-fun deriv_ord' ctxt pol pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
+fun deriv_ord' ctxt _ pred modes t1 t2 ((deriv1, mvars1), (deriv2, mvars2)) =
let
(* prefer functional modes if it is a function *)
- fun fun_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ fun fun_ord ((t1, deriv1, _), (t2, deriv2, _)) =
let
fun is_functional t mode =
case try (fst o dest_Const o fst o strip_comb) t of
@@ -398,20 +346,20 @@
| (false, false) => EQUAL
end
(* prefer modes without requirement for generating random values *)
- fun mvars_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ fun mvars_ord ((_, _, mvars1), (_, _, mvars2)) =
int_ord (length mvars1, length mvars2)
(* prefer non-random modes *)
- fun random_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ fun random_mode_ord ((t1, deriv1, _), (t2, deriv2, _)) =
int_ord (if random_mode_in_deriv modes t1 deriv1 then 1 else 0,
if random_mode_in_deriv modes t2 deriv2 then 1 else 0)
(* prefer modes with more input and less output *)
- fun output_mode_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ fun output_mode_ord ((_, deriv1, _), (_, deriv2, _)) =
int_ord (number_of_output_positions (head_mode_of deriv1),
number_of_output_positions (head_mode_of deriv2))
(* prefer recursive calls *)
fun is_rec_premise t =
- case fst (strip_comb t) of Const (c, T) => c = pred | _ => false
- fun recursive_ord ((t1, deriv1, mvars1), (t2, deriv2, mvars2)) =
+ case fst (strip_comb t) of Const (c, _) => c = pred | _ => false
+ fun recursive_ord ((t1, _, _), (t2, deriv2, _)) =
int_ord (if is_rec_premise t1 then 0 else 1,
if is_rec_premise t2 then 0 else 1)
val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord]
@@ -424,10 +372,6 @@
fun premise_ord thy pol pred modes ((prem1, a1), (prem2, a2)) =
rev_option_ord (deriv_ord' thy pol pred modes (dest_indprem prem1) (dest_indprem prem2)) (a1, a2)
-fun print_mode_list modes =
- tracing ("modes: " ^ (commas (map (fn (s, ms) => s ^ ": " ^
- commas (map (fn (m, r) => string_of_mode m ^ (if r then " random " else " not ")) ms)) modes)))
-
fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
pol (modes, (pos_modes, neg_modes)) vs ps =
let
@@ -435,7 +379,7 @@
find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
| choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
| choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
- (filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
+ (filter (fn (d, _) => is_all_input (head_mode_of d))
(all_derivations_of ctxt neg_modes vs t))
| choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
in
@@ -451,17 +395,16 @@
val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts []))
val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode))
fun retrieve_modes_of_pol pol = map (fn (s, ms) =>
- (s, map_filter (fn ((p, m), r) => if p = pol then SOME m else NONE | _ => NONE) ms))
+ (s, map_filter (fn ((p, m), _) => if p = pol then SOME m else NONE | _ => NONE) ms))
val (pos_modes', neg_modes') =
if #infer_pos_and_neg_modes mode_analysis_options then
(retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes')
else
let
- val modes = map (fn (s, ms) => (s, map (fn ((p, m), r) => m) ms)) modes'
+ val modes = map (fn (s, ms) => (s, map (fn ((_, m), _) => m) ms)) modes'
in (modes, modes) end
val (in_ts, out_ts) = split_mode mode ts
val in_vs = union (op =) param_vs (maps (vars_of_destructable_term ctxt) in_ts)
- val out_vs = terms_vs out_ts
fun known_vs_after p vs = (case p of
Prem t => union (op =) vs (term_vs t)
| Sidecond t => union (op =) vs (term_vs t)
@@ -480,7 +423,7 @@
(distinct (op =) missing_vars))
@ acc_ps) true (known_vs_after p vs) (filter_out (equal p) ps)
else NONE
- | SOME (p, NONE) => NONE
+ | SOME (_, NONE) => NONE
| NONE => NONE)
in
case check_mode_prems [] false in_vs ps of
@@ -508,7 +451,7 @@
fun split xs =
let
fun split' [] (ys, zs) = (rev ys, rev zs)
- | split' ((m, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
+ | split' ((_, Error z) :: xs) (ys, zs) = split' xs (ys, z :: zs)
| split' (((m : bool * mode), Success rnd) :: xs) (ys, zs) = split' xs ((m, rnd) :: ys, zs)
in
split' xs ([], [])
@@ -522,7 +465,7 @@
cond_timeit false "aux part of check_mode for one mode" (fn _ =>
case find_indices is_none res of
[] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
- | is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
+ | is => (print_failed_mode options p m is; Error (error_of p m is)))
end
val _ = if show_mode_inference options then
tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
@@ -537,9 +480,9 @@
let
val rs = these (AList.lookup (op =) clauses p)
in
- (p, map (fn (m, rnd) =>
+ (p, map (fn (m, _) =>
(m, map
- ((fn (ts, ps, rnd) => (ts, ps)) o the o
+ ((fn (ts, ps, _) => (ts, ps)) o the o
check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)) ms)
end;
@@ -567,18 +510,12 @@
fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
preds all_modes param_vs clauses =
let
- fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
fun add_needs_random s (false, m) = ((false, m), false)
| add_needs_random s (true, m) = ((true, m), needs_random s m)
fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
val prednames = map fst preds
(* extramodes contains all modes of all constants, should we only use the necessary ones
- what is the impact on performance? *)
- fun predname_of (Prem t) =
- (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
- | predname_of (Negprem t) =
- (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
- | predname_of _ = I
val relevant_prednames = fold (fn (_, clauses') =>
fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
|> filter_out (fn name => member (op =) prednames name)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Mon Nov 12 23:24:40 2012 +0100
@@ -157,7 +157,7 @@
map (apsnd (map fst)) proposed_modes,
proposed_names =
maps (fn (predname, ms) => (map_filter
- (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
+ (fn (_, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
show_steps = chk "show_steps",
show_intermediate_results = chk "show_intermediate_results",
show_proof_trace = chk "show_proof_trace",
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Nov 12 23:24:40 2012 +0100
@@ -931,7 +931,7 @@
let
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
- val ([tname, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
+ val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
val T' = TFree (tname', HOLogic.typeS)
val U = TFree (uname, HOLogic.typeS)
val y = Free (yname, U)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML Mon Nov 12 23:24:40 2012 +0100
@@ -89,20 +89,20 @@
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+fun mk_iterate_upto _ _ = error "not implemented yet"
fun mk_not t =
let
val T = mk_monadT HOLogic.unitT
in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _ = error "not implemented"
val compfuns = Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -138,7 +138,7 @@
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
+fun mk_iterate_upto _ _ = error "not implemented yet"
fun mk_not t =
let
@@ -148,13 +148,13 @@
val T = mk_monadT HOLogic.unitT
in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _ = error "not implemented"
val compfuns = Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -193,7 +193,7 @@
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = error "not implemented"
+fun mk_iterate_upto _ _ = error "not implemented"
fun mk_not t =
let
@@ -202,13 +202,13 @@
--> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"}
in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
-fun mk_Enum f = error "not implemented"
+fun mk_Enum _ = error "not implemented"
-fun mk_Eval (f, x) = error "not implemented"
+fun mk_Eval _ = error "not implemented"
-fun dest_Eval t = error "not implemented"
+fun dest_Eval _ = error "not implemented"
-fun mk_map T1 T2 tf tp = error "not implemented"
+fun mk_map _ _ _ _ = error "not implemented"
val compfuns = Predicate_Compile_Aux.CompilationFuns
{mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
@@ -296,7 +296,7 @@
fun mk_if cond = Const (@{const_name DSequence.if_seq},
HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
fun mk_not t = let val T = mk_dseqT HOLogic.unitT
in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
@@ -347,7 +347,7 @@
fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
fun mk_not t =
let
@@ -408,7 +408,7 @@
fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
fun mk_not t =
let
@@ -599,7 +599,7 @@
fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
-fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation"
+fun mk_iterate_upto _ _ = raise Fail "No iterate_upto compilation"
fun mk_not t =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Nov 12 23:24:40 2012 +0100
@@ -80,20 +80,6 @@
HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
in mk_eqs x xs end;
-fun mk_scomp (t, u) =
- let
- val T = fastype_of t
- val U = fastype_of u
- val [A] = binder_types T
- val D = body_type U
- in
- Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
- end;
-
-fun dest_randomT (Type ("fun", [@{typ Random.seed},
- Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
- | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
-
fun mk_tracing s t =
Const(@{const_name Code_Evaluation.tracing},
@{typ String.literal} --> (fastype_of t) --> (fastype_of t)) $ (HOLogic.mk_literal s) $ t
@@ -115,7 +101,7 @@
fun print_pred_mode_table string_of_entry pred_mode_table =
let
- fun print_mode pred ((pol, mode), entry) = "mode : " ^ string_of_mode mode
+ fun print_mode pred ((_, mode), entry) = "mode : " ^ string_of_mode mode
^ string_of_entry pred mode entry
fun print_pred (pred, modes) =
"predicate " ^ pred ^ ": " ^ cat_lines (map (print_mode pred) modes)
@@ -133,7 +119,7 @@
fun print pred () = let
val _ = writeln ("predicate: " ^ pred)
val _ = writeln ("introrules: ")
- val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
+ val _ = fold (fn thm => fn _ => writeln (Display.string_of_thm ctxt thm))
(rev (intros_of ctxt pred)) ()
in
if (has_elim ctxt pred) then
@@ -159,7 +145,7 @@
(* validity checks *)
-fun check_expected_modes options preds modes =
+fun check_expected_modes options _ modes =
case expected_modes options of
SOME (s, ms) => (case AList.lookup (op =) modes s of
SOME modes =>
@@ -200,16 +186,16 @@
fun check_matches_type ctxt predname T ms =
let
- fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
- | check m (T as Type("fun", _)) = (m = Input orelse m = Output)
+ 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 Input T = true
- | check Output T = true
+ | check Input _ = true
+ | check Output _ = true
| check Bool @{typ bool} = true
| check _ _ = false
fun check_consistent_modes ms =
- if forall (fn Fun (m1', m2') => true | _ => false) ms then
+ 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)
else if forall (fn Input => true | Output => true | Pair _ => true | _ => false) ms then
@@ -320,7 +306,7 @@
$ compilation
end,
transform_additional_arguments =
- fn prem => fn additional_arguments =>
+ fn _ => fn additional_arguments =>
let
val [depth] = additional_arguments
val depth' =
@@ -378,7 +364,7 @@
Free (size, @{typ code_numeral}), Free (seed, @{typ "code_numeral * code_numeral"})]
end),
wrap_compilation =
- fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
+ fn compfuns => fn _ => fn T => fn mode => fn additional_arguments => fn compilation =>
let
val depth = hd (additional_arguments)
val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
@@ -391,7 +377,7 @@
$ compilation
end,
transform_additional_arguments =
- fn prem => fn additional_arguments =>
+ fn _ => fn additional_arguments =>
let
val [depth, nrandom, size, seed] = additional_arguments
val depth' =
@@ -413,21 +399,6 @@
transform_additional_arguments = K I : (indprem -> term list -> term list)
}
-val annotated_comp_modifiers = Comp_Mod.Comp_Modifiers
- {
- compilation = Annotated,
- function_name_prefix = "annotated_",
- compfuns = Predicate_Comp_Funs.compfuns,
- mk_random = (fn _ => error "no random generation"),
- modify_funT = I,
- additional_arguments = K [],
- wrap_compilation =
- fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
- mk_tracing ("calling predicate " ^ s ^
- " with mode " ^ string_of_mode mode) compilation,
- transform_additional_arguments = K I : (indprem -> term list -> term list)
- }
-
val dseq_comp_modifiers = Comp_Mod.Comp_Modifiers
{
compilation = DSeq,
@@ -446,7 +417,7 @@
compilation = Pos_Random_DSeq,
function_name_prefix = "random_dseq_",
compfuns = Random_Sequence_CompFuns.compfuns,
- mk_random = (fn T => fn additional_arguments =>
+ mk_random = (fn T => fn _ =>
let
val random = Const ("Quickcheck.random_class.random",
@{typ code_numeral} --> @{typ Random.seed} -->
@@ -483,7 +454,7 @@
compilation = New_Pos_Random_DSeq,
function_name_prefix = "new_random_dseq_",
compfuns = New_Pos_Random_Sequence_CompFuns.depth_limited_compfuns,
- mk_random = (fn T => fn additional_arguments =>
+ mk_random = (fn T => fn _ =>
let
val random = Const ("Quickcheck.random_class.random",
@{typ code_numeral} --> @{typ Random.seed} -->
@@ -519,7 +490,7 @@
function_name_prefix = "generator_dseq_",
compfuns = New_Pos_DSequence_CompFuns.depth_limited_compfuns,
mk_random =
- (fn T => fn additional_arguments =>
+ (fn T => fn _ =>
Const (@{const_name "Lazy_Sequence.small_lazy_class.small_lazy"},
@{typ "Code_Numeral.code_numeral"} --> Type (@{type_name "Lazy_Sequence.lazy_sequence"}, [T]))),
modify_funT = I,
@@ -548,7 +519,7 @@
function_name_prefix = "generator_cps_pos_",
compfuns = Pos_Bounded_CPS_Comp_Funs.compfuns,
mk_random =
- (fn T => fn additional_arguments =>
+ (fn T => fn _ =>
Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
(T --> @{typ "(bool * term list) option"}) -->
@{typ "code_numeral => (bool * term list) option"})),
@@ -582,7 +553,7 @@
| Neg_Generator_DSeq => pos_generator_dseq_comp_modifiers
| Pos_Generator_CPS => neg_generator_cps_comp_modifiers
| Neg_Generator_CPS => pos_generator_cps_comp_modifiers
- | c => comp_modifiers)
+ | _ => comp_modifiers)
(* term construction *)
@@ -606,7 +577,7 @@
(** specific rpred functions -- move them to the correct place in this file *)
-fun mk_Eval_of (P as (Free (f, _)), T) mode =
+fun mk_Eval_of (P as (Free _), T) mode =
let
fun mk_bounds (Type (@{type_name Product_Type.prod}, [T1, T2])) i =
let
@@ -615,7 +586,7 @@
in
(HOLogic.pair_const T1 T2 $ bs1 $ bs2, i'' + 1)
end
- | mk_bounds T i = (Bound i, i + 1)
+ | mk_bounds _ i = (Bound i, i + 1)
fun mk_prod ((t1, T1), (t2, T2)) = (HOLogic.pair_const T1 T2 $ t1 $ t2, HOLogic.mk_prodT (T1, T2))
fun mk_tuple [] = (HOLogic.unit, HOLogic.unitT)
| mk_tuple tTs = foldr1 mk_prod tTs
@@ -625,13 +596,13 @@
| mk_split_abs T t = absdummy T t
val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
val (inargs, outargs) = split_mode mode args
- val (inTs, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
+ val (_, outTs) = split_map_modeT (fn _ => fn T => (SOME T, NONE)) mode (binder_types T)
val inner_term = Predicate_Comp_Funs.mk_Eval (list_comb (P, inargs), fst (mk_tuple (outargs ~~ outTs)))
in
fold_rev mk_split_abs (binder_types T) inner_term
end
-fun compile_arg compilation_modifiers additional_arguments ctxt 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
@@ -672,23 +643,13 @@
(v', mk_empty compfuns U')])
end;
-fun string_of_tderiv ctxt (t, deriv) =
- (case (t, deriv) of
- (t1 $ t2, Mode_App (deriv1, deriv2)) =>
- string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
- | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
- "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
- | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
- | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
- | (t, Context m) => Syntax.string_of_term ctxt t ^ "[" ^ string_of_mode m ^ "]")
-
fun compile_expr compilation_modifiers ctxt (t, deriv) param_modes additional_arguments =
let
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 Output) => NONE
+ | (_, Term Output) => NONE
| (Const (name, T), Context mode) =>
(case alternative_compilation_of ctxt name mode of
SOME alt_comp => SOME (alt_comp compfuns T)
@@ -698,13 +659,13 @@
Comp_Mod.funT_of compilation_modifiers mode T)))
| (Free (s, T), Context m) =>
(case (AList.lookup (op =) param_modes s) of
- SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+ 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 m) =>
+ | (t, Context _) =>
let
val bs = map (pair "x") (binder_types (fastype_of t))
val bounds = map Bound (rev (0 upto (length bs) - 1))
@@ -736,7 +697,7 @@
let
val (out_ts'', (names', eqs')) =
fold_map (collect_non_invertible_subterms ctxt) out_ts' (names, []);
- val (out_ts''', (names'', constr_vs)) = fold_map distinct_v
+ val (out_ts''', (_, constr_vs)) = fold_map distinct_v
out_ts'' (names', map (rpair []) vs);
val processed_out_ts = map (compile_arg compilation_modifiers additional_arguments
ctxt param_modes) out_ts
@@ -815,10 +776,10 @@
(fn (i, Input) => [(i, [])]
| (_, Output) => []
| (_, Fun _) => []
- | (i, m as Pair (m1, m2)) => map (pair i) (input_positions_pair m))
+ | (i, m as Pair _) => map (pair i) (input_positions_pair m))
(Predicate_Compile_Aux.strip_fun_mode mode))
-fun argument_position_pair 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
@@ -839,7 +800,7 @@
(** switch detection analysis **)
-fun find_switch_test ctxt (i, is) (ts, prems) =
+fun find_switch_test ctxt (i, is) (ts, _) =
let
val t = nth_pair is (nth ts i)
val T = fastype_of t
@@ -895,7 +856,7 @@
fun destruct_constructor_pattern (pat, obj) =
(case strip_comb pat of
- (f as Free _, []) => cons (pat, obj)
+ (Free _, []) => cons (pat, obj)
| (Const (c, T), pat_args) =>
(case strip_comb obj of
(Const (c', T'), obj_args) =>
@@ -1024,12 +985,6 @@
(* Definition of executable functions and their intro and elim rules *)
-fun print_arities arities = tracing ("Arities:\n" ^
- cat_lines (map (fn (s, (ks, k)) => s ^ ": " ^
- space_implode " -> " (map
- (fn NONE => "X" | SOME k' => string_of_int k')
- (ks @ [SOME k]))) arities));
-
fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
@@ -1120,7 +1075,7 @@
((introthm, elimthm), opt_neg_introthm)
end
-fun create_constname_of_mode options thy prefix name T 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
@@ -1139,7 +1094,7 @@
val mode_cbasename = Long_Name.base_name mode_cname
val funT = funT_of compfuns mode T
val (args, _) = fold_map (mk_args true) ((strip_fun_mode mode) ~~ (binder_types T)) []
- fun strip_eval m t =
+ fun strip_eval _ t =
let
val t' = strip_split_abs t
val (r, _) = Predicate_Comp_Funs.dest_Eval t'
@@ -1167,7 +1122,7 @@
thy |> defined_function_of Pred name |> fold create_definition modes
end;
-fun define_functions comp_modifiers compfuns options preds (name, modes) thy =
+fun define_functions comp_modifiers _ options preds (name, modes) thy =
let
val T = AList.lookup (op =) preds name |> the
fun create_definition mode thy =
@@ -1200,7 +1155,7 @@
fun maps_modes preds_modes_table =
map (fn (pred, modes) =>
- (pred, map (fn (mode, value) => value) modes)) preds_modes_table
+ (pred, map (fn (_, value) => value) modes)) preds_modes_table
fun compile_preds options comp_modifiers ctxt all_vs param_vs preds moded_clauses =
map_preds_modes (fn pred => compile_pred options comp_modifiers ctxt all_vs param_vs pred
@@ -1210,21 +1165,21 @@
map_preds_modes (prove_pred options thy clauses preds)
(join_preds_modes moded_clauses compiled_terms)
-fun prove_by_skip options thy _ _ _ compiled_terms =
+fun prove_by_skip _ thy _ _ _ compiled_terms =
map_preds_modes
- (fn pred => fn mode => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
+ (fn _ => fn _ => fn t => Drule.export_without_context (Skip_Proof.make_thm thy t))
compiled_terms
(* preparation of introduction rules into special datastructures *)
fun dest_prem ctxt params t =
(case strip_comb t of
- (v as Free _, ts) => if member (op =) params v then Prem t else Sidecond t
+ (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 (s, _), ts) =>
+ | (Const (s, _), _) =>
if is_registered ctxt s then Prem t else Sidecond t
| _ => Sidecond t)
@@ -1270,7 +1225,7 @@
val param_vs = map (fst o dest_Free) params
fun add_clause intr clauses =
let
- val (Const (name, T), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl 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) @
@@ -1479,18 +1434,6 @@
use_generators = false,
qname = "depth_limited_equation"})
-val add_annotated_equations = gen_add_equations
- (Steps {
- define_functions =
- fn options => fn preds => fn (s, modes) =>
- define_functions annotated_comp_modifiers Predicate_Comp_Funs.compfuns options preds
- (s, map_filter (fn (true, m) => SOME m | _ => NONE) modes),
- prove = prove_by_skip,
- add_code_equations = K (K I),
- comp_modifiers = annotated_comp_modifiers,
- use_generators = false,
- qname = "annotated_equation"})
-
val add_random_equations = gen_add_equations
(Steps {
define_functions =
@@ -1668,7 +1611,7 @@
| New_Pos_Random_DSeq => add_new_random_dseq_equations
| Pos_Generator_DSeq => add_generator_dseq_equations
| Pos_Generator_CPS => add_generator_cps_equations
- | compilation => error ("Compilation not supported")
+ | _ => error ("Compilation not supported")
) options [const]))
end
in
@@ -1740,7 +1683,7 @@
fun dest_special_compr t =
let
- val (inner_t, T_compr) = case t of (Const (@{const_name Collect}, _) $ Abs (x, T, t)) => (t, 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
@@ -1773,13 +1716,13 @@
(*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
fun analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes
- (compilation, arguments) t_compr =
+ (compilation, _) t_compr =
let
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
- val (pred as Const (name, T), all_args) =
+ val (Const (name, _), all_args) =
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)
@@ -1794,7 +1737,7 @@
case int_ord (length modes1, length modes2) of
GREATER => error "Not enough mode annotations"
| LESS => error "Too many mode annotations"
- | EQUAL => forall (fn (m, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
+ | EQUAL => forall (fn (_, NONE) => true | (m, SOME m2) => eq_mode (m, m2))
(modes1 ~~ modes2)
fun mode_instance_of (m1, m2) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Nov 12 23:24:40 2012 +0100
@@ -80,13 +80,13 @@
| _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
(*TODO*)
-fun is_introlike_term t = true
+fun is_introlike_term _ = true
val is_introlike = is_introlike_term o prop_of
-fun check_equation_format_term (t as (Const ("==", _) $ u $ v)) =
+fun check_equation_format_term (t as (Const ("==", _) $ u $ _)) =
(case strip_comb u of
- (Const (c, T), args) =>
+ (Const (_, T), args) =>
if (length (binder_types T) = length args) then
true
else
@@ -98,7 +98,7 @@
val check_equation_format = check_equation_format_term o prop_of
-fun defining_term_of_equation_term (t as (Const ("==", _) $ u $ v)) = fst (strip_comb u)
+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])
@@ -135,7 +135,7 @@
fun split_all_pairs thy th =
let
val ctxt = Proof_Context.init_global thy
- val ((_, [th']), ctxt') = Variable.import true [th] ctxt
+ val ((_, [th']), _) = Variable.import true [th] ctxt
val t = prop_of th'
val frees = Term.add_frees t []
val freenames = Term.add_free_names t []
@@ -230,7 +230,7 @@
@{const_name HOL.conj},
@{const_name HOL.disj}]
-fun special_cases (c, T) = member (op =) [
+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},
@@ -253,18 +253,12 @@
] c
-fun print_specification options thy constname specs =
- if show_intermediate_results options then
- tracing ("Specification of " ^ constname ^ ":\n" ^
- cat_lines (map (Display.string_of_thm_global thy) specs))
- else ()
-
fun obtain_specification_graph options thy t =
let
val ctxt = Proof_Context.init_global thy
- fun is_nondefining_const (c, T) = member (op =) logic_operator_names c
- fun has_code_pred_intros (c, T) = can (Core_Data.intros_of ctxt) c
- fun case_consts (c, T) = is_some (Datatype.info_of_case thy c)
+ fun is_nondefining_const (c, _) = member (op =) logic_operator_names c
+ fun has_code_pred_intros (c, _) = can (Core_Data.intros_of ctxt) c
+ fun case_consts (c, _) = is_some (Datatype.info_of_case thy c)
fun is_datatype_constructor (c, T) = is_some (Datatype.info_of_constr thy (c, T))
fun defiants_of specs =
fold (Term.add_consts o prop_of) specs []
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Nov 12 23:24:40 2012 +0100
@@ -40,7 +40,7 @@
fun pred_of_function thy name =
case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
[] => NONE
- | [(f, p)] => SOME (fst (dest_Const p))
+ | [(_, p)] => SOME (fst (dest_Const p))
| _ => error ("Multiple matches possible for lookup of constant " ^ name)
fun defined_const thy name = is_some (pred_of_function thy name)
@@ -78,20 +78,6 @@
val (func, args) = strip_comb lhs
in ((func, args), rhs) end;
-(* TODO: does not work with higher order functions yet *)
-fun mk_rewr_eq (func, pred) =
- let
- val (argTs, resT) = strip_type (fastype_of func)
- val nctxt =
- Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
- val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
- val (resname, nctxt'') = Name.variant "r" nctxt'
- val args = map Free (argnames ~~ argTs)
- val res = Free (resname, resT)
- in Logic.mk_equals
- (HOLogic.mk_eq (res, list_comb (func, args)), list_comb (pred, args @ [res]))
- end;
-
fun folds_map f xs y =
let
fun folds_map' acc [] y = [(rev acc, y)]
@@ -126,7 +112,7 @@
fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
val vTs =
fold Term.add_frees inner_prems []
- |> filter (fn (x, T) => member (op =) inner_names x)
+ |> filter (fn (x, _) => member (op =) inner_names x)
val t =
fold mk_exists vTs
(foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
@@ -149,8 +135,8 @@
else
error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
", " ^ Syntax.string_of_typ_global thy T)
- and flatten' (t as Const (name, T)) (names, prems) = [(t, (names, prems))]
- | flatten' (t as Free (f, T)) (names, prems) = [(t, (names, prems))]
+ 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))]
| flatten' (t as _ $ _) (names, prems) =
if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
@@ -182,10 +168,9 @@
case find_split_thm thy (fst (strip_comb t)) of
SOME raw_split_thm =>
let
- val (f, args) = strip_comb t
val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val t' = case_betapply thy t
val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
fun flatten_of_assm assm =
@@ -267,7 +252,6 @@
([], thy)
else
let
- val consts = map fst specs
val eqns = maps snd specs
(* create prednames *)
val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
@@ -293,10 +277,9 @@
let
val names = Term.add_free_names rhs []
in flatten thy lookup_pred rhs (names, [])
- |> map (fn (resultt, (names', prems)) =>
+ |> map (fn (resultt, (_, prems)) =>
Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
end
- fun mk_rewr_thm (func, pred) = @{thm refl}
val intr_ts = maps mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
val (intrs, thy') = thy
|> Sign.add_consts_i
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Nov 12 23:24:40 2012 +0100
@@ -19,7 +19,7 @@
open Predicate_Compile_Aux
-fun is_compound ((Const (@{const_name Not}, _)) $ t) =
+fun is_compound ((Const (@{const_name Not}, _)) $ _) =
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
@@ -37,7 +37,7 @@
(*val ((_, [isplit_thm]), _) =
Variable.import true [split_thm] (Proof_Context.init_global thy)*)
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
- val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
+ val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val atom' = case_betapply thy atom
val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
val names' = Term.add_free_names atom' names
@@ -156,7 +156,7 @@
val nctxt = Name.make_context frees
fun mk_introrule t =
let
- val ((ps, t'), nctxt') = focus_ex t nctxt
+ val ((ps, t'), _) = focus_ex t nctxt
val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
in
(ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
@@ -224,11 +224,6 @@
(full_spec, thy'')
end;
-fun preprocess_term t thy = error "preprocess_pred_term: to implement"
-
-fun is_Abs (Abs _) = true
- | is_Abs _ = false
-
fun flat_higher_order_arguments (intross, thy) =
let
fun process constname atom (new_defs, thy) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Mon Nov 12 23:24:40 2012 +0100
@@ -72,12 +72,12 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
val f_tac = case f of
- Const (name, T) => simp_tac (HOL_basic_ss addsimps
+ Const (name, _) => simp_tac (HOL_basic_ss 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} =>
+ Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
@@ -97,7 +97,7 @@
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
case strip_comb t of
- (Const (name, T), args) =>
+ (Const (name, _), args) =>
let
val mode = head_mode_of deriv
val introrule = predfun_intro_of ctxt name mode
@@ -117,7 +117,7 @@
end
| (Free _, _) =>
print_tac options "proving parameter call.."
- THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+ THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} =>
let
val param_prem = nth prems premposition
val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem))
@@ -136,23 +136,6 @@
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
-fun SOLVEDALL tac st = FILTER (fn st' => nprems_of st' = 0) tac st
-
-fun check_format ctxt st =
- let
- val concl' = Logic.strip_assums_concl (hd (prems_of st))
- val concl = HOLogic.dest_Trueprop concl'
- val expr = fst (strip_comb (fst (Predicate_Comp_Funs.dest_Eval concl)))
- fun valid_expr (Const (@{const_name Predicate.bind}, _)) = true
- | valid_expr (Const (@{const_name Predicate.single}, _)) = true
- | valid_expr _ = false
- in
- if valid_expr expr then
- ((*tracing "expression is valid";*) Seq.single st)
- else
- ((*tracing "expression is not valid";*) Seq.empty) (* error "check_format: wrong format" *)
- end
-
fun prove_match options ctxt nargs out_ts =
let
val thy = Proof_Context.theory_of ctxt
@@ -175,7 +158,7 @@
THEN print_tac options "after prove_match:"
THEN (DETERM (TRY
(rtac eval_if_P 1
- THEN (SUBPROOF (fn {context = ctxt, params, prems, asms, concl, schematics} =>
+ THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} =>
(REPEAT_DETERM (rtac @{thm conjI} 1
THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
THEN print_tac options "if condition to be solved:"
@@ -197,7 +180,7 @@
fun prove_sidecond ctxt t =
let
fun preds_of t nameTs = case strip_comb t of
- (f as Const (name, T), args) =>
+ (Const (name, T), args) =>
if is_registered ctxt name then (name, T) :: nameTs
else fold preds_of args nameTs
| _ => nameTs
@@ -221,7 +204,7 @@
THEN asm_full_simp_tac HOL_basic_ss' 1
THEN print_tac options "before single intro rule"
THEN Subgoal.FOCUS_PREMS
- (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+ (fn {context, params, prems, asms, concl, schematics} =>
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
@@ -267,7 +250,7 @@
THEN (if (is_some name) then
print_tac options "before applying not introduction rule"
THEN Subgoal.FOCUS_PREMS
- (fn {context = ctxt, params = params, prems, asms, concl, schematics} =>
+ (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"
@@ -364,7 +347,7 @@
val param_derivations = param_derivations_of deriv
val ho_args = ho_args_of mode args
val f_tac = case f of
- Const (name, T) => full_simp_tac (HOL_basic_ss addsimps
+ Const (name, _) => full_simp_tac (HOL_basic_ss addsimps
(@{thm eval_pred}::(predfun_definition_of ctxt name mode)
:: @{thm "Product_Type.split_conv"}::[])) 1
| Free _ => all_tac
@@ -378,7 +361,7 @@
fun prove_expr2 options ctxt (t, deriv) =
(case strip_comb t of
- (Const (name, T), args) =>
+ (Const (name, _), args) =>
let
val mode = head_mode_of deriv
val param_derivations = param_derivations_of deriv
@@ -396,7 +379,7 @@
fun prove_sidecond2 options ctxt t = let
fun preds_of t nameTs = case strip_comb t of
- (f as Const (name, T), args) =>
+ (Const (name, T), args) =>
if is_registered ctxt name then (name, T) :: nameTs
else fold preds_of args nameTs
| _ => nameTs
@@ -415,7 +398,7 @@
fun prove_clause2 options ctxt pred mode (ts, ps) i =
let
val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
- val (in_ts, clause_out_ts) = split_mode mode ts;
+ val (in_ts, _) = split_mode mode ts;
val split_ss = HOL_basic_ss' addsimps [@{thm split_eta}, @{thm split_beta},
@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
fun prove_prems2 out_ts [] =
@@ -506,7 +489,7 @@
(** proof procedure **)
-fun prove_pred options thy clauses preds pred (pol, mode) (moded_clauses, compiled_term) =
+fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
let
val ctxt = Proof_Context.init_global thy
val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon Nov 12 23:24:40 2012 +0100
@@ -26,15 +26,9 @@
fun specialisation_of thy atom =
Item_Net.retrieve (Specialisations.get thy) atom
-fun print_specialisations thy =
- tracing (cat_lines (map (fn (t, spec_t) =>
- Syntax.string_of_term_global thy t ^ " ~~~> " ^ Syntax.string_of_term_global thy spec_t)
- (Item_Net.content (Specialisations.get thy))))
-
-fun import (pred, intros) args ctxt =
+fun import (_, intros) args ctxt =
let
- val thy = Proof_Context.theory_of ctxt
- val ((Tinst, intros'), ctxt') = Variable.importT intros ctxt
+ val ((_, intros'), ctxt') = Variable.importT intros ctxt
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
@@ -68,7 +62,6 @@
val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
- val intros_t = map prop_of intros
val result_pats = map Var (fold_rev Term.add_vars pats [])
fun mk_fresh_name names =
let
@@ -85,9 +78,6 @@
val constname = mk_fresh_name []
val constT = map fastype_of result_pats ---> @{typ bool}
val specialised_const = Const (constname, constT)
- val specialisation =
- [(HOLogic.mk_Trueprop (list_comb (pred, pats)),
- HOLogic.mk_Trueprop (list_comb (specialised_const, result_pats)))]
fun specialise_intro intro =
(let
val (prems, concl) = Logic.strip_horn (prop_of intro)
@@ -141,7 +131,7 @@
end
| restrict_pattern' thy ((T as TFree _, t) :: Tts) free_names =
replace_term_and_restrict thy T t Tts free_names
- | restrict_pattern' thy ((T as Type (Tcon, Ts), t) :: Tts) free_names =
+ | restrict_pattern' thy ((T as Type (Tcon, _), t) :: Tts) free_names =
case Datatype.get_constrs thy Tcon of
NONE => replace_term_and_restrict thy T t Tts free_names
| SOME constrs => (case strip_comb t of
@@ -169,7 +159,6 @@
(pred as Const (pred_name, _), args) =>
let
val Ts = binder_types (Sign.the_const_type thy pred_name)
- val vnames = map fst (fold Term.add_var_names args [])
val pats = restrict_pattern thy Ts args
in
if (exists (is_nontrivial_constrt thy) pats)
@@ -187,7 +176,7 @@
| SOME intros =>
specialise_intros ((map fst specs) @ (pred_name :: black_list))
(pred, intros) pats thy)
- | (t, specialised_t) :: _ => thy
+ | _ :: _ => thy
val atom' =
case specialisation_of thy' atom of
[] => atom