# HG changeset patch # User wenzelm # Date 969279031 -7200 # Node ID 8c16ec5ba62bad329ecd42d54a61e46f19c0d27e # Parent d41ab495ab148ac94f5b2746af0a819fc30646db indicate occurrences of 'handle _'; diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/dcterm.sml --- a/TFL/dcterm.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/dcterm.sml Mon Sep 18 14:10:31 2000 +0200 @@ -163,7 +163,7 @@ let fun dest (p as (ctm,accum)) = let val (M,N) = break ctm in dest (N, M::accum) - end handle _ => p + end handle _ => p (* FIXME do not handle _ !!! *) in dest (tm,[]) end; @@ -188,6 +188,6 @@ | _ => capply prop ctm end; -fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm; +fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm; (* FIXME do not handle _ !!! *) end; diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/post.sml --- a/TFL/post.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/post.sml Mon Sep 18 14:10:31 2000 +0200 @@ -95,7 +95,7 @@ fun id_thm th = let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) in lhs aconv rhs - end handle _ => false + end handle _ => false (* FIXME do not handle _ !!! *) fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); val P_imp_P_iff_True = prover "P --> (P= True)" RS mp; @@ -213,7 +213,7 @@ fun defer_i thy congs fid eqs = let val {rules,R,theory,full_pats_TCs,SV,...} = Prim.lazyR_def thy (Sign.base_name fid) congs eqs - val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) + val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) (* FIXME do not handle _ !!! *) val dummy = message "Proving induction theorem ..."; val induction = Prim.mk_induction theory {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/rules.sml --- a/TFL/rules.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/rules.sml Mon Sep 18 14:10:31 2000 +0200 @@ -114,7 +114,7 @@ val blist' = map (fn (TVar(idx,_), B) => (idx, ctyp_of sign B)) blist in Thm.instantiate (blist',[]) thm end - handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; + handle _ => raise RULES_ERR{func = "INST_TYPE", mesg = ""}; (* FIXME do not handle _ !!! *) (*---------------------------------------------------------------------------- @@ -150,7 +150,7 @@ let val tm = D.mk_prop(#1(D.dest_imp(cconcl (freezeT thm)))) in implies_elim (thm RS mp) (ASSUME tm) end - handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; + handle _ => raise RULES_ERR{func = "UNDISCH", mesg = ""}; (* FIXME do not handle _ !!! *) fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath; @@ -170,7 +170,7 @@ fun CONJUNCT1 thm = (thm RS conjunct1) fun CONJUNCT2 thm = (thm RS conjunct2); fun CONJUNCTS th = (CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th)) - handle _ => [th]; + handle _ => [th]; (* FIXME do not handle _ !!! *) fun LIST_CONJ [] = raise RULES_ERR{func = "LIST_CONJ", mesg = "empty list"} | LIST_CONJ [th] = th @@ -211,7 +211,7 @@ val rdisj_tl = D.list_mk_disj tail in itlist DISJ2 ldisjs (DISJ1 th rdisj_tl) :: blue (ldisjs@[cconcl th]) rst tail - end handle _ => [itlist DISJ2 ldisjs th] + end handle _ => [itlist DISJ2 ldisjs th] (* FIXME do not handle _ !!! *) in blue [] thms (map cconcl thms) end; @@ -450,7 +450,7 @@ *---------------------------------------------------------------------------*) fun SUBS thl = - rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); + rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl); (* FIXME do not handle _ !!! *) local fun rew_conv mss = Thm.rewrite_cterm (true,false,false) mss (K(K None)) in @@ -544,7 +544,7 @@ val names = variantlist (map (#1 o dest_Free) vstrl, add_term_names(body, [])) in get (rst, n+1, (names,n)::L) - end handle _ => get (rst, n+1, L); + end handle _ => get (rst, n+1, L); (* FIXME do not handle _ !!! *) (* Note: rename_params_rule counts from 1, not 0 *) fun rename thm = @@ -589,7 +589,7 @@ * General abstraction handlers, should probably go in USyntax. *---------------------------------------------------------------------------*) fun mk_aabs(vstr,body) = S.mk_abs{Bvar=vstr,Body=body} - handle _ => S.mk_pabs{varstruct = vstr, body = body}; + handle _ => S.mk_pabs{varstruct = vstr, body = body}; (* FIXME do not handle _ !!! *) fun list_mk_aabs (vstrl,tm) = U.itlist (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm; @@ -597,7 +597,7 @@ fun dest_aabs tm = let val {Bvar,Body} = S.dest_abs tm in (Bvar,Body) - end handle _ => let val {varstruct,body} = S.dest_pabs tm + end handle _ => let val {varstruct,body} = S.dest_pabs tm (* FIXME do not handle _ !!! *) in (varstruct,body) end; @@ -606,7 +606,7 @@ val (bvs, core) = strip_aabs body in (vstr::bvs, core) end - handle _ => ([],tm); + handle _ => ([],tm); (* FIXME do not handle _ !!! *) fun dest_combn tm 0 = (tm,[]) | dest_combn tm n = @@ -715,7 +715,7 @@ val lhs = tych(get_lhs eq) val mss' = add_prems(mss, map ASSUME ants) val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs - handle _ => reflexive lhs + handle _ => reflexive lhs (* FIXME do not handle _ !!! *) val dummy = print_thms "proven:" [lhs_eq_lhs1] val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq @@ -737,12 +737,12 @@ val Q1 = #2(D.dest_eq(cconcl QeqQ1)) val mss' = add_prems(mss, map ASSUME ants1) val Q1eeqQ2 = Thm.rewrite_cterm (false,true,false) mss' prover Q1 - handle _ => reflexive Q1 + handle _ => reflexive Q1 (* FIXME do not handle _ !!! *) val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2))) val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl)) val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection) val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2 - val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => + val QeeqQ3 = transitive thA Q2eeqQ3 handle _ => (* FIXME do not handle _ !!! *) ((Q2eeqQ3 RS meta_eq_to_obj_eq) RS ((thA RS meta_eq_to_obj_eq) RS trans)) RS eq_reflection @@ -763,7 +763,7 @@ val mss' = add_prems(mss, map ASSUME ants1) val Q_eeq_Q1 = Thm.rewrite_cterm(false,true,false) mss' prover (tych Q) - handle _ => reflexive (tych Q) + handle _ => reflexive (tych Q) (* FIXME do not handle _ !!! *) val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1 val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq val ant_th = forall_intr_list(map tych vlist)lhs_eq_lhs2 @@ -781,7 +781,7 @@ (* Assume that the leading constant is ==, *) | _ => thm (* if it is not a ==> *) in Some(eliminate (rename thm)) - end handle _ => None + end handle _ => None (* FIXME do not handle _ !!! *) fun restrict_prover mss thm = let val dummy = say "restrict_prover:" @@ -826,7 +826,7 @@ end val th'' = th' RS thm in Some (th'') - end handle _ => None + end handle _ => None (* FIXME do not handle _ !!! *) in (if (is_cong thm) then cong_prover else restrict_prover) mss thm end diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/tfl.sml --- a/TFL/tfl.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/tfl.sml Mon Sep 18 14:10:31 2000 +0200 @@ -162,7 +162,7 @@ U.itlist (fn (row as ((prfx, p::rst), rhs)) => fn (in_group,not_in_group) => let val (pc,args) = S.strip_comb p - in if ((#1(dest_Const pc) = Name) handle _ => false) + in if ((#1(dest_Const pc) = Name) handle _ => false) (* FIXME do not handle _ !!! *) then (((prfx,args@rst), rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]); @@ -328,7 +328,7 @@ in fun mk_functional thy clauses = let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses) - handle _ => raise TFL_ERR + handle _ => raise TFL_ERR (* FIXME do not handle _ !!! *) {func = "mk_functional", mesg = "recursion equations must use the = relation"} val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L) @@ -347,7 +347,7 @@ val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty {path=[a], rows=rows} val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts - handle _ => mk_functional_err "error in pattern-match translation" + handle _ => mk_functional_err "error in pattern-match translation" (* FIXME do not handle _ !!! *) val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1 val finals = map row_of_pat patts2 val originals = map (row_of_pat o #2) rows @@ -736,7 +736,7 @@ | _ => let val imp = S.list_mk_conj cntxt ==> P_y val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs + val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *) in (S.list_mk_forall(locals,imp), (tm,locals)) end end in case TCs @@ -765,7 +765,7 @@ | _ => let val imp = S.list_mk_conj cntxt ==> P_y val lvs = gen_rems (op aconv) (S.free_vars_lr imp, globals) - val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs + val locals = #2(U.pluck (curry (op aconv) P) lvs) handle _ => lvs (* FIXME do not handle _ !!! *) in (S.list_mk_forall(locals,imp), (tm,locals)) end end in case TCs @@ -793,7 +793,7 @@ fun mk_ih ((TC,locals),th2,nested) = R.GENL (map tych locals) (if nested - then R.DISCH (get_cntxt TC) th2 handle _ => th2 + then R.DISCH (get_cntxt TC) th2 handle _ => th2 (* FIXME do not handle _ !!! *) else if S.is_imp(concl TC) then R.IMP_TRANS TC th2 else R.MP th2 TC) @@ -874,7 +874,7 @@ in R.GEN (tych P) (R.DISCH (tych(concl Rinduct_assum)) dc') end -handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"}; +handle _ => raise TFL_ERR{func = "mk_induction", mesg = "failed derivation"}; (* FIXME do not handle _ !!! *) @@ -922,7 +922,7 @@ (hd(#1(R.dest_thm rules)))), wf_tac) in (R.PROVE_HYP thm rules, R.PROVE_HYP thm induction) - end handle _ => (rules,induction) + end handle _ => (rules,induction) (* FIXME do not handle _ !!! *) (*---------------------------------------------------------------------- * The termination condition (tc) is simplified to |- tc = tc' (there @@ -948,12 +948,12 @@ val _ = print_thms "result: " [tc_eq] in elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind) - handle _ => + handle _ => (* FIXME do not handle _ !!! *) (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))), terminator))) (r,ind) - handle _ => + handle _ => (* FIXME do not handle _ !!! *) (R.UNDISCH(R.MATCH_MP (R.MATCH_MP Thms.simp_thm r) tc_eq), simplify_induction theory tc_eq ind)) end @@ -976,11 +976,11 @@ in R.GEN_ALL (R.MATCH_MP Thms.eqT tc_eq - handle _ + handle _ (* FIXME do not handle _ !!! *) => (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq) (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))), terminator)) - handle _ => tc_eq)) + handle _ => tc_eq)) (* FIXME do not handle _ !!! *) end (*------------------------------------------------------------------- diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/usyntax.sml --- a/TFL/usyntax.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/usyntax.sml Mon Sep 18 14:10:31 2000 +0200 @@ -217,7 +217,7 @@ end in mpa(varstruct,body) end - handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""}; + handle _ => raise USYN_ERR{func = "mk_pabs", mesg = ""}; (* FIXME do not handle _ !!! *) end; (* Destruction routines *) @@ -288,7 +288,7 @@ let val {Bvar,Body} = dest_abs tm in {varstruct = Bvar, body = Body} end - handle + handle (* FIXME do not handle _ !!! *) _ => let val {Rator,Rand} = dest_comb tm val _ = ucheck Rator val {varstruct = lv,body} = dest_pabs Rand @@ -392,7 +392,7 @@ if (p tm) then Some tm else case tm of Abs(_,_,body) => find body - | (t$u) => (Some (the (find t)) handle _ => find u) + | (t$u) => (Some (the (find t)) handle _ => find u) (* FIXME do not handle _ !!! *) | _ => None in find end; @@ -402,7 +402,7 @@ then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm in (R,y,x) end handle _ => raise USYN_ERR{func="dest_relation", - mesg="unexpected term structure"} + mesg="unexpected term structure"} (* FIXME do not handle _ !!! *) else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"}; fun is_WFR (Const("WF.wf",_)$_) = true diff -r d41ab495ab14 -r 8c16ec5ba62b TFL/utils.sml --- a/TFL/utils.sml Sun Sep 17 22:51:20 2000 +0200 +++ b/TFL/utils.sml Mon Sep 18 14:10:31 2000 +0200 @@ -83,8 +83,8 @@ | zip3 _ _ _ = raise UTILS_ERR{func="zip3",mesg="different lengths"}; -fun can f x = (f x ; true) handle _ => false; -fun holds P x = P x handle _ => false; +fun can f x = (f x ; true) handle _ => false; (* FIXME do not handle _ !!! *) +fun holds P x = P x handle _ => false; (* FIXME do not handle _ !!! *) fun sort R =