1.1 --- a/src/Tools/isac/Interpret/appl.sml Wed Mar 14 17:12:43 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Sat Mar 17 11:06:46 2012 +0100
1.3 @@ -362,37 +362,31 @@
1.4 | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str))
1.5 | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve')
1.6
1.7 - | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) =
1.8 - if member op = [Pbl,Met] p_
1.9 + | applicable_in (p, p_) pt (m as Rewrite_Inst (subs, thm')) =
1.10 + if member op = [Pbl, Met] p_
1.11 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.12 - else
1.13 - let
1.14 - val pp = par_pblobj pt p;
1.15 - val thy' = (get_obj g_domID pt pp):theory';
1.16 - val thy = assoc_thy thy';
1.17 - val {rew_ord'=ro',erls=erls,...} =
1.18 - get_met (get_obj g_metID pt pp);
1.19 - val (f,p) = case p_ of (*p 12.4.00 unnecessary*)
1.20 - Frm => (get_obj g_form pt p, p)
1.21 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.22 - | _ => error ("applicable_in: call by "^
1.23 - (pos'2str (p,p_)));
1.24 - in
1.25 - let val subst = subs2subst thy subs;
1.26 - val subs' = subst2subs' subst;
1.27 - in case rewrite_inst_ thy (assoc_rew_ord ro') erls
1.28 - (*put_asm*)false subst (assoc_thm' thy thm') f of
1.29 - SOME (f',asm) => Appl (
1.30 - Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm',
1.31 - (*term_of o the o (parse (assoc_thy thy'))*) f,
1.32 - (*(term_of o the o (parse (assoc_thy thy'))*) (f',
1.33 - (*map (term_of o the o (parse (assoc_thy thy')))*) asm)))
1.34 - | NONE => Notappl ((fst thm')^" not applicable") end
1.35 - handle _ => Notappl ("syntax error in "^(subs2str subs)) end
1.36 + else
1.37 + let
1.38 + val pp = par_pblobj pt p;
1.39 + val thy' = (get_obj g_domID pt pp): theory';
1.40 + val thy = assoc_thy thy';
1.41 + val {rew_ord' = ro', erls = erls, ...} = get_met (get_obj g_metID pt pp);
1.42 + val (f, p) = case p_ of (*p 12.4.00 unnecessary*)
1.43 + Frm => (get_obj g_form pt p, p)
1.44 + | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
1.45 + | _ => error ("applicable_in: call by " ^ pos'2str (p,p_));
1.46 + in
1.47 + let
1.48 + val subst = subs2subst thy subs;
1.49 + val subs' = subst2subs' subst;
1.50 + in case rewrite_inst_ thy (assoc_rew_ord ro') erls false subst (assoc_thm' thy thm') f of
1.51 + SOME (f',asm) =>
1.52 + Appl (Rewrite_Inst' (thy', ro', erls, false, subst, thm', f, (f', asm)))
1.53 + | NONE => Notappl ((fst thm')^" not applicable")
1.54 + end
1.55 + handle _ => Notappl ("syntax error in "^(subs2str subs))
1.56 + end
1.57
1.58 -(* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m);
1.59 - val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac);
1.60 - *)
1.61 | applicable_in (p,p_) pt (m as Rewrite thm') =
1.62 if member op = [Pbl,Met] p_
1.63 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.64 @@ -638,65 +632,41 @@
1.65 | applicable_in (p,p_) pt (End_Trans) =
1.66 let val thy' = get_obj g_domID pt (par_pblobj pt p);
1.67 in if p_ = Res
1.68 - then Appl (End_Trans' (get_obj g_result pt p))
1.69 - else Notappl "'End_Trans' is not applicable at \
1.70 - \the beginning of a transitive sequence"
1.71 - (*TODO: check parent branches*)
1.72 + then Appl (End_Trans' (get_obj g_result pt p))
1.73 + else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
1.74 + (*TODO: check parent branches*)
1.75 end
1.76 + | applicable_in p pt (Begin_Sequ) =
1.77 + error ("applicable_in: not impl. for " ^ tac2str (Begin_Sequ))
1.78 + | applicable_in p pt (End_Sequ) =
1.79 + error ("applicable_in: not impl. for " ^ tac2str (End_Sequ))
1.80 + | applicable_in p pt (Split_Intersect) =
1.81 + error ("applicable_in: not impl. for " ^ tac2str (Split_Intersect))
1.82 + | applicable_in p pt (End_Intersect) =
1.83 + error ("applicable_in: not impl. for " ^ tac2str (End_Intersect))
1.84
1.85 - | applicable_in p pt (Begin_Sequ) =
1.86 - error ("applicable_in: not impl. for "^
1.87 - (tac2str (Begin_Sequ)))
1.88 - | applicable_in p pt (End_Sequ) =
1.89 - error ("applicable_in: not impl. for "^
1.90 - (tac2str (End_Sequ)))
1.91 - | applicable_in p pt (Split_Intersect) =
1.92 - error ("applicable_in: not impl. for "^
1.93 - (tac2str (Split_Intersect)))
1.94 - | applicable_in p pt (End_Intersect) =
1.95 - error ("applicable_in: not impl. for "^
1.96 - (tac2str (End_Intersect)))
1.97 -(* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it;
1.98 - val (vvv,ppp) = vp;
1.99 -
1.100 - val Check_elementwise pred = m;
1.101 -
1.102 - val ((p,p_), Check_elementwise pred) = (p, m);
1.103 - *)
1.104 | applicable_in (p,p_) pt (m as Check_elementwise pred) =
1.105 - if member op = [Pbl,Met] p_
1.106 + if member op = [Pbl,Met] p_
1.107 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
1.108 - else
1.109 - let
1.110 - val pp = par_pblobj pt p;
1.111 - val thy' = (get_obj g_domID pt pp):theory';
1.112 - val thy = assoc_thy thy'
1.113 - val metID = (get_obj g_metID pt pp)
1.114 - val {crls,...} = get_met metID
1.115 - (*val _=tracing("### applicable_in Check_elementwise: crls= "^crls)
1.116 - val _=tracing("### applicable_in Check_elementwise: pred= "^pred)*)
1.117 - (*val erl = the (assoc'(!ruleset',crls))*)
1.118 - val (f,asm) = case p_ of
1.119 - Frm => (get_obj g_form pt p , [])
1.120 - | Res => get_obj g_result pt p;
1.121 - (*val _= tracing("### applicable_in Check_elementwise: f= "^f);*)
1.122 - val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
1.123 - (*val (v,p)=vp;val _=tracing("### applicable_in Check_elementwise: vp= "^
1.124 - pair2str(term2str v,term2str p))*)
1.125 - in case f of
1.126 - Const ("List.list.Cons",_) $ _ $ _ =>
1.127 - Appl (Check_elementwise'
1.128 - (f, pred,
1.129 - ((*tracing("### applicable_in Check_elementwise: --> "^
1.130 - (res2str (check_elementwise thy crls f vp)));*)
1.131 - check_elementwise thy crls f vp)))
1.132 - | Const ("Tools.UniversalList",_) =>
1.133 - Appl (Check_elementwise' (f, pred, (f,asm)))
1.134 - | Const ("List.list.Nil",_) =>
1.135 - (*Notappl "not applicable to empty list" 3.6.03*)
1.136 - Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*))))
1.137 - | _ => Notappl ("not applicable: "^(term2str f)^" should be constants")
1.138 - end
1.139 + else
1.140 + let
1.141 + val pp = par_pblobj pt p;
1.142 + val thy' = (get_obj g_domID pt pp):theory';
1.143 + val thy = assoc_thy thy'
1.144 + val metID = (get_obj g_metID pt pp)
1.145 + val {crls,...} = get_met metID
1.146 + val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
1.147 + | Res => get_obj g_result pt p;
1.148 + val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
1.149 + in case f of
1.150 + Const ("List.list.Cons",_) $ _ $ _ =>
1.151 + Appl (Check_elementwise' (f, pred, check_elementwise thy crls f vp))
1.152 + | Const ("Tools.UniversalList",_) =>
1.153 + Appl (Check_elementwise' (f, pred, (f,asm)))
1.154 + | Const ("List.list.Nil",_) =>
1.155 + Appl (Check_elementwise' (f, pred, (f, asm)))
1.156 + | _ => Notappl ("Check_elementwise not applicable: "^(term2str f)^" should be constants")
1.157 + end
1.158
1.159 | applicable_in (p,p_) pt Or_to_List =
1.160 if member op = [Pbl,Met] p_