--- 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;
--- 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}
--- 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
--- 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
(*-------------------------------------------------------------------
--- 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
--- 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 =