# HG changeset patch # User wenzelm # Date 1255892020 -7200 # Node ID ccc07fbbfefd54f147c2b605e620f387cd7a1b63 # Parent 078c1f7fa8beb0f97f299c6fbfa1ddc4810050ec removed some unreferenced material; tuned; diff -r 078c1f7fa8be -r ccc07fbbfefd src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Sun Oct 18 18:08:04 2009 +0200 +++ b/src/HOL/Tools/metis_tools.ML Sun Oct 18 20:53:40 2009 +0200 @@ -81,11 +81,11 @@ | (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v | _ => error "hol_term_to_fol_FO"; -fun hol_term_to_fol_HO (ResHolClause.CombVar(a, ty)) = Metis.Term.Var a - | hol_term_to_fol_HO (ResHolClause.CombConst(a, ty, tylist)) = - Metis.Term.Fn(fn_isa_to_met a, map hol_type_to_fol tylist) - | hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) = - Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]); +fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a + | hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) = + Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) + | hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) = + Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); @@ -122,8 +122,8 @@ fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; -fun default_sort ctxt (TVar _) = false - | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), [])); +fun default_sort _ (TVar _) = false + | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), [])); fun metis_of_tfree tf = Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf)); @@ -162,7 +162,7 @@ fun m_classrel_cls subclass superclass = [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; -fun classrel_cls (ResClause.ClassrelClause {axiom_name,subclass,superclass,...}) = +fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) = (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); (* ------------------------------------------------------------------------- *) @@ -176,10 +176,10 @@ | terms_of (Type _ :: tts) = terms_of tts; fun types_of [] = [] - | types_of (Term (Term.Var((a,idx), T)) :: tts) = + | types_of (Term (Term.Var ((a,idx), _)) :: tts) = if String.isPrefix "_" a then (*Variable generated by Metis, which might have been a type variable.*) - TVar(("'" ^ a, idx), HOLogic.typeS) :: types_of tts + TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts else types_of tts | types_of (Term _ :: tts) = types_of tts | types_of (Type T :: tts) = T :: types_of tts; @@ -210,7 +210,7 @@ fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t | strip_happ args x = (x, args); -fun fol_type_to_isa ctxt (Metis.Term.Var v) = +fun fol_type_to_isa _ (Metis.Term.Var v) = (case Recon.strip_prefix ResClause.tvar_prefix v of SOME w => Recon.make_tvar w | NONE => Recon.make_tvar v) @@ -281,11 +281,11 @@ (*Maps fully-typed metis terms to isabelle terms*) fun fol_term_to_hol_FT ctxt fol_tm = let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) - fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) = + fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = (case Recon.strip_prefix ResClause.schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) - | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) = + | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = (case Recon.strip_prefix ResClause.const_prefix x of @@ -356,7 +356,7 @@ in cterm_instantiate substs th end; (* INFERENCE RULE: AXIOM *) -fun axiom_inf ctxt thpairs th = incr_indexes 1 (lookth thpairs th); +fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th); (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) (* INFERENCE RULE: ASSUME *) @@ -418,7 +418,6 @@ fun resolve_inf ctxt mode thpairs atm th1 th2 = let - val thy = ProofContext.theory_of ctxt val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) @@ -451,17 +450,17 @@ val c_t = cterm_incr_types thy refl_idx i_t in cterm_instantiate [(refl_x, c_t)] REFL_THM end; -fun get_ty_arg_size thy (Const("op =",_)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const(c,_)) = (Recon.num_typargs thy c handle TYPE _ => 0) - | get_ty_arg_size thy _ = 0; +fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) + | get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) -fun equality_inf ctxt mode thpairs (pos,atm) fp fr = +fun equality_inf ctxt mode (pos, atm) fp fr = let val thy = ProofContext.theory_of ctxt val m_tm = Metis.Term.Fn atm val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr] val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) - fun replace_item_list lx 0 (l::ls) = lx::ls + fun replace_item_list lx 0 (_::ls) = lx::ls | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls fun path_finder_FO tm [] = (tm, Term.Bound 0) | path_finder_FO tm (p::ps) = @@ -479,13 +478,13 @@ end fun path_finder_HO tm [] = (tm, Term.Bound 0) | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) - | path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) + | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) fun path_finder_FT tm [] _ = (tm, Term.Bound 0) - | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) = + | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = path_finder_FT tm ps t1 - | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) = + | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) - | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) = + | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ space_implode " " (map Int.toString ps) ^ @@ -496,7 +495,7 @@ (*equality: not curried, as other predicates are*) if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) else path_finder_HO tm (p::ps) (*1 selects second operand*) - | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = + | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) (Metis.Term.Fn ("=", [t1,t2])) = @@ -507,7 +506,7 @@ else path_finder_FT tm (p::ps) (Metis.Term.Fn (".", [metis_eq,t2])) (*1 selects second operand*) - | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 + | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 (*if not equality, ignore head to skip the hBOOL predicate*) | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = @@ -528,22 +527,19 @@ val factor = Seq.hd o distinct_subgoals_tac; -fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _) = - factor (axiom_inf ctxt thpairs fol_th) - | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm) = - assume_inf ctxt mode f_atm - | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) = +fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th) + | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm + | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) = factor (inst_inf ctxt mode thpairs f_subst f_th1) - | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = + | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) - | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm) = - refl_inf ctxt mode f_tm - | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) = - equality_inf ctxt mode thpairs f_lit f_p f_r; + | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm + | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = + equality_inf ctxt mode f_lit f_p f_r; -fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c); +fun real_literal (_, (c, _)) = not (String.isPrefix ResClause.class_prefix c); -fun translate mode _ thpairs [] = thpairs +fun translate _ _ thpairs [] = thpairs | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = let val _ = trace_msg (fn () => "=============================================") val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) @@ -551,7 +547,8 @@ val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf)) val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) val _ = trace_msg (fn () => "=============================================") - val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) + val n_metis_lits = + length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) in if nprems_of th = n_metis_lits then () else error "Metis: proof reconstruction has gone wrong"; @@ -560,7 +557,7 @@ (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) - | used_axioms axioms _ = NONE; + | used_axioms _ _ = NONE; (* ------------------------------------------------------------------------- *) (* Translation of HO Clauses *) @@ -581,8 +578,7 @@ let val subs = ResAtp.tfree_classes_of_terms tms val supers = ResAtp.tvar_classes_of_terms tms and tycons = ResAtp.type_consts_of_terms thy tms - val arity_clauses = ResClause.make_arity_clauses thy tycons supers - val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers + val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' in map classrel_cls classrel_clauses @ map arity_cls arity_clauses end; @@ -595,12 +591,12 @@ {axioms : (Metis.Thm.thm * Thm.thm) list, tfrees : ResClause.type_literal list}; -fun const_in_metis c (pol,(pred,tm_list)) = +fun const_in_metis c (pred, tm_list) = let - fun in_mterm (Metis.Term.Var nm) = false + fun in_mterm (Metis.Term.Var _) = false | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list - in c=pred orelse exists in_mterm tm_list end; + in c = pred orelse exists in_mterm tm_list end; (*Extract TFree constraints from context to include as conjecture clauses*) fun init_tfrees ctxt = @@ -641,7 +637,7 @@ {axioms = [], tfrees = init_tfrees ctxt} cls val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) - fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists + fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists (*Now check for the existence of certain combinators*) val thI = if used "c_COMBI" then [comb_I] else [] val thK = if used "c_COMBK" then [comb_K] else [] @@ -697,7 +693,7 @@ and used = map_filter (used_axioms axioms) proof val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used - val unused = filter (fn (a,cls) => not (common_thm used cls)) th_cls_pairs + val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs in if null unused then () else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused)); diff -r 078c1f7fa8be -r ccc07fbbfefd src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sun Oct 18 18:08:04 2009 +0200 +++ b/src/HOL/Tools/res_atp.ML Sun Oct 18 20:53:40 2009 +0200 @@ -112,7 +112,7 @@ | add_term_consts_typs_rm thy (t $ u, tab) = add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab)) | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab) - | add_term_consts_typs_rm thy (_, tab) = tab; + | add_term_consts_typs_rm _ (_, tab) = tab; (*The empty list here indicates that the constant is being ignored*) fun add_standard_const (s,tab) = Symtab.update (s,[]) tab; @@ -208,7 +208,7 @@ | dest_ConstFree _ = raise ConstFree; (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*) -fun defines thy (thm,(name,n)) gctypes = +fun defines thy thm gctypes = let val tm = prop_of thm fun defs lhs rhs = let val (rator,args) = strip_comb lhs @@ -262,7 +262,7 @@ | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = let val weight = clause_weight ctab rel_consts consts_typs in - if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts) + if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) then (ResAxioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight)); relevant ((ax,weight)::newrels, rejects) axs) @@ -403,7 +403,7 @@ fun check_named ("", th) = (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false) - | check_named (_, th) = true; + | check_named _ = true; (* get lemmas from claset, simpset, atpset and extra supplied rules *) fun get_clasimp_atp_lemmas ctxt = @@ -440,7 +440,7 @@ (*fold type constructors*) fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x)) - | fold_type_consts f T x = x; + | fold_type_consts _ _ x = x; val add_type_consts_in_type = fold_type_consts setinsert; @@ -448,7 +448,7 @@ fun add_type_consts_in_term thy = let val const_typargs = Sign.const_typargs thy fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x - | add_tcs (Abs (_, T, u)) x = add_tcs u x + | add_tcs (Abs (_, _, u)) x = add_tcs u x | add_tcs (t $ u) x = add_tcs t (add_tcs u x) | add_tcs _ x = x in add_tcs end diff -r 078c1f7fa8be -r ccc07fbbfefd src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sun Oct 18 18:08:04 2009 +0200 +++ b/src/HOL/Tools/res_axioms.ML Sun Oct 18 20:53:40 2009 +0200 @@ -91,7 +91,7 @@ val thy'' = Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy' val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef) in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end - | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx = + | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p, [])) a in dec_sko (subst_bound (Free (fname, T), p)) thx end @@ -119,7 +119,7 @@ in dec_sko (subst_bound (list_comb(c,args), p)) (def :: defs) end - | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs = + | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs = (*Universal quant: insert a free variable into body and continue*) let val fname = Name.variant (OldTerm.add_term_names (p,[])) a in dec_sko (subst_bound (Free(fname,T), p)) defs end @@ -158,8 +158,6 @@ val lambda_free = not o Term.has_abs; -val monomorphic = not o Term.exists_type (Term.exists_subtype Term.is_TVar); - val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B})); val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C})); val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S})); @@ -216,14 +214,14 @@ else case term_of ct of Abs _ => - let val (cv,cta) = Thm.dest_abs NONE ct - val (v,Tv) = (dest_Free o term_of) cv + let val (cv, cta) = Thm.dest_abs NONE ct + val (v, _) = dest_Free (term_of cv) val u_th = combinators_aux cta val cu = Thm.rhs_of u_th val comb_eq = abstract (Thm.cabs cv cu) in transitive (abstract_rule v cv u_th) comb_eq end - | t1 $ t2 => - let val (ct1,ct2) = Thm.dest_comb ct + | _ $ _ => + let val (ct1, ct2) = Thm.dest_comb ct in combination (combinators_aux ct1) (combinators_aux ct2) end; fun combinators th = @@ -286,11 +284,6 @@ fun assume_skolem_of_def s th = map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); -fun assert_lambda_free ths msg = - case filter (not o lambda_free o prop_of) ths of - [] => () - | ths' => error (cat_lines (msg :: map Display.string_of_thm_without_context ths')); - (*** Blacklisting (duplicated in ResAtp?) ***) @@ -343,10 +336,6 @@ if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) else gensym "unknown_thm_"; -fun name_or_string th = - if Thm.has_name_hint th then Thm.get_name_hint th - else Display.string_of_thm_without_context th; - (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm (s, th) = if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then [] diff -r 078c1f7fa8be -r ccc07fbbfefd src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Sun Oct 18 18:08:04 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Sun Oct 18 20:53:40 2009 +0200 @@ -119,9 +119,9 @@ fun type_of dfg (Type (a, Ts)) = let val (folTypes,ts) = types_of dfg Ts in (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts) end - | type_of dfg (tp as (TFree(a,s))) = + | type_of _ (tp as TFree (a, _)) = (RC.AtomF (RC.make_fixed_type_var a), [tp]) - | type_of dfg (tp as (TVar(v,s))) = + | type_of _ (tp as TVar (v, _)) = (RC.AtomV (RC.make_schematic_type_var v), [tp]) and types_of dfg Ts = let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) @@ -130,8 +130,8 @@ (* same as above, but no gathering of sort information *) fun simp_type_of dfg (Type (a, Ts)) = RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) - | simp_type_of dfg (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a) - | simp_type_of dfg (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v); + | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a) + | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v); fun const_type_of dfg thy (c,t) = @@ -143,11 +143,11 @@ let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list) in (c',ts) end - | combterm_of dfg thy (Free(v,t)) = + | combterm_of dfg _ (Free(v,t)) = let val (tp,ts) = type_of dfg t val v' = CombConst(RC.make_fixed_var v, tp, []) in (v',ts) end - | combterm_of dfg thy (Var(v,t)) = + | combterm_of dfg _ (Var(v,t)) = let val (tp,ts) = type_of dfg t val v' = CombVar(RC.make_schematic_var v,tp) in (v',ts) end @@ -155,7 +155,7 @@ let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q in (CombApp(P',Q'), tsP union tsQ) end - | combterm_of _ thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t); + | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t); fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); @@ -195,7 +195,7 @@ fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) []; -fun make_conjecture_clauses_aux dfg _ _ [] = [] +fun make_conjecture_clauses_aux _ _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = make_clause dfg thy (n,"conjecture", RC.Conjecture, th) :: make_conjecture_clauses_aux dfg thy (n+1) ths; @@ -213,9 +213,9 @@ fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 | result_type _ = error "result_type" -fun type_of_combterm (CombConst(c,tp,_)) = tp - | type_of_combterm (CombVar(v,tp)) = tp - | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1); +fun type_of_combterm (CombConst (_, tp, _)) = tp + | type_of_combterm (CombVar (_, tp)) = tp + | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1); (*gets the head of a combinator application, along with the list of arguments*) fun strip_comb u = @@ -226,7 +226,7 @@ val type_wrapper = "ti"; fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c - | head_needs_hBOOL const_needs_hBOOL _ = true; + | head_needs_hBOOL _ _ = true; fun wrap_type t_full (s, tp) = if t_full then @@ -242,7 +242,7 @@ (*Apply an operator to the argument strings, using either the "apply" operator or direct function application.*) -fun string_of_applic t_full cma (CombConst(c,tp,tvars), args) = +fun string_of_applic t_full cma (CombConst (c, _, tvars), args) = let val c = if c = "equal" then "c_fequal" else c val nargs = min_arity_of cma c val args1 = List.take(args, nargs) @@ -255,7 +255,7 @@ in string_apply (c ^ RC.paren_pack (args1@targs), args2) end - | string_of_applic _ cma (CombVar(v,tp), args) = string_apply (v, args) + | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) | string_of_applic _ _ _ = error "string_of_applic"; fun wrap_type_if t_full cnh (head, s, tp) = @@ -282,12 +282,6 @@ CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t | _ => boolify params t; -fun string_of_clausename (cls_id,ax_name) = - RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id; - -fun string_of_type_clsname (cls_id,ax_name,idx) = - string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx); - (*** tptp format ***) @@ -306,7 +300,7 @@ (map (tptp_literal params) literals, map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts)); -fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = +fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) = let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls in (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) @@ -342,7 +336,7 @@ fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars; -fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) = +fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = if c = "equal" then (addtypes tvars funcs, preds) else let val arity = min_arity_of cma c @@ -394,10 +388,10 @@ ("c_COMBB", 0), ("c_COMBC", 0), ("c_COMBS", 0)]; -fun count_combterm (CombConst(c,tp,_), ct) = +fun count_combterm (CombConst (c, _, _), ct) = (case Symtab.lookup ct c of NONE => ct (*no counter*) | SOME n => Symtab.update (c,n+1) ct) - | count_combterm (CombVar(v,tp), ct) = ct + | count_combterm (CombVar _, ct) = ct | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct)); fun count_literal (Literal(_,t), ct) = count_combterm(t,ct); @@ -448,7 +442,7 @@ if toplev then (const_min_arity, const_needs_hBOOL) else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL)) end - | ts => (const_min_arity, const_needs_hBOOL) + | _ => (const_min_arity, const_needs_hBOOL) end; (*A literal is a top-level term*) diff -r 078c1f7fa8be -r ccc07fbbfefd src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Sun Oct 18 18:08:04 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Sun Oct 18 20:53:40 2009 +0200 @@ -216,7 +216,7 @@ | xs => foldr1 HOLogic.mk_disj (rev xs); (*Accumulate sort constraints in vt, with "real" literals in lits.*) -fun lits_of_strees ctxt (vt, lits) [] = (vt, finish lits) +fun lits_of_strees _ (vt, lits) [] = (vt, finish lits) | lits_of_strees ctxt (vt, lits) (t::ts) = lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts handle STREE _ => @@ -303,7 +303,7 @@ | match_literal (Free(a1,_)) (Free(a2,_)) env = if a1=a2 then env else raise MATCH_LITERAL | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env - | match_literal _ _ env = raise MATCH_LITERAL; + | match_literal _ _ _ = raise MATCH_LITERAL; (*Checking that all variable associations are unique. The list env contains no repetitions, but does it contain say (x,y) and (y,y)? *) @@ -337,7 +337,7 @@ then SOME ctm else perm ctms in perm end; -fun have_or_show "show " lname = "show \"" +fun have_or_show "show " _ = "show \"" | have_or_show have lname = have ^ lname ^ ": \"" (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the @@ -345,7 +345,7 @@ fun isar_lines ctxt ctms = let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term) val _ = trace ("\n\nisar_lines: start\n") - fun doline have (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*) + fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*) (case permuted_clause t ctms of SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n" | NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*) @@ -374,17 +374,17 @@ else (case take_prefix (notequal t) lines of (_,[]) => lines (*no repetition of proof line*) - | (pre, (lno',t',deps')::post) => (*repetition: replace later line by earlier one*) + | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) pre @ map (replace_deps (lno', [lno])) post) - | add_prfline ((lno, role, t, []), lines) = (*no deps: conjecture clause*) + | add_prfline ((lno, _, t, []), lines) = (*no deps: conjecture clause*) (lno, t, []) :: lines - | add_prfline ((lno, role, t, deps), lines) = + | add_prfline ((lno, _, t, deps), lines) = if eq_types t then (lno, t, deps) :: lines (*Type information will be deleted later; skip repetition test.*) else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) case take_prefix (notequal t) lines of (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) - | (pre, (lno',t',deps')::post) => + | (pre, (lno', t', _) :: post) => (lno, t', deps) :: (*repetition: replace later line by earlier one*) (pre @ map (replace_deps (lno', [lno])) post);