diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Interpret/appl.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/Interpret/appl.sml Wed Aug 25 16:20:07 2010 +0200 @@ -0,0 +1,782 @@ +(* use"ME/appl.sml"; + use"appl.sml"; + +12345678901234567890123456789012345678901234567890123456789012345678901234567890 + 10 20 30 40 50 60 70 80 +*) +val e_cterm' = empty_cterm'; + + +fun rew_info (Rls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = + (rew_ord':rew_ord',erls,ca) + | rew_info (Seq {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = + (rew_ord',erls,ca) + | rew_info (Rrls {erls,rew_ord=(rew_ord',_),calc=ca, ...}) = + (rew_ord',erls, ca) + | rew_info rls = raise error ("rew_info called with '"^rls2str rls^"'"); + +(*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*) +fun from_pblobj_or_detail_thm thm' p pt = + let val (pbl,p',rls') = par_pbl_det pt p + in if pbl + then let (*val _= writeln("### from_pblobj_or_detail_thm: pbl=true")*) + val thy' = get_obj g_domID pt p' + val {rew_ord',erls,(*asm_thm,*)...} = + get_met (get_obj g_metID pt p') + (*val _= writeln("### from_pblobj_or_detail_thm: metID= "^ + (metID2str(get_obj g_metID pt p'))) + val _= writeln("### from_pblobj_or_detail_thm: erls= "^erls)*) + in ("OK",thy',rew_ord',erls,(*put_asm*)false) + end + else ((*writeln("### from_pblobj_or_detail_thm: pbl=false");*) + (*case assoc(!ruleset', rls') of !!!FIXME.3.4.03:re-organize !!! + NONE => ("unknown ruleset '"^rls'^"'","","",Erls,false) + | SOME rls =>*) + let val thy' = get_obj g_domID pt (par_pblobj pt p) + val (rew_ord',erls,(*asm_thm,*)_) = rew_info rls' + in ("OK",thy',rew_ord',erls,false) end) + end; +(*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*) +fun from_pblobj_or_detail_calc scrop p pt = +(* val (scrop, p, pt) = (op_, p, pt); + *) + let val (pbl,p',rls') = par_pbl_det pt p + in if pbl + then let val thy' = get_obj g_domID pt p' + val {calc = scr_isa_fns,...} = + get_met (get_obj g_metID pt p') + val opt = assoc (scr_isa_fns, scrop) + in case opt of + SOME isa_fn => ("OK",thy',isa_fn) + | NONE => ("applicable_in Calculate: unknown '"^scrop^"'", + "",("",e_evalfn)) end + else (*case assoc(!ruleset', rls') of + NONE => ("unknown ruleset '"^rls'^"'","",("",e_evalfn)) + | SOME rls => !!!FIXME.3.4.03:re-organize from_pblobj_or_detai*) + (* val SOME rls = assoc(!ruleset', rls'); + *) + let val thy' = get_obj g_domID pt (par_pblobj pt p); + val (_,_,(*_,*)scr_isa_fns) = rew_info rls'(*rls*) + in case assoc (scr_isa_fns, scrop) of + SOME isa_fn => ("OK",thy',isa_fn) + | NONE => ("applicable_in Calculate: unknown '"^scrop^"'", + "",("",e_evalfn)) end + end; +(*------------------------------------------------------------------*) + +val op_and = Const ("op &", [bool, bool] ---> bool); +(*> (cterm_of thy) (op_and $ Free("a",bool) $ Free("b",bool)); +val it = "a & b" : cterm +*) +fun mk_and a b = op_and $ a $ b; +(*> (cterm_of thy) + (mk_and (Free("a",bool)) (Free("b",bool))); +val it = "a & b" : cterm*) + +fun mk_and [] = HOLogic.true_const + | mk_and (t::[]) = t + | mk_and (t::ts) = + let fun mk t' (t::[]) = op_and $ t' $ t + | mk t' (t::ts) = mk (op_and $ t' $ t) ts + in mk t ts end; +(*> val pred = map (term_of o the o (parse thy)) + ["#0 <= #9 + #4 * x","#0 <= sqrt x + sqrt (#-3 + x)"]; +> (cterm_of thy) (mk_and pred); +val it = "#0 <= #9 + #4 * x & #0 <= sqrt x + sqrt (#-3 + x)" : cterm*) + + + + +(*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*) +fun mk_set thy pt p (Const ("List.list.Nil",_)) pred = (e_term, []) + + | mk_set thy pt p (Const ("Tools.UniversalList",_)) pred = + (e_term, if pred <> Const ("Script.Assumptions",bool) + then [pred] + else (map fst) (get_assumptions_ pt (p,Res))) + +(* val pred = (term_of o the o (parse thy)) pred; + val consts as Const ("List.list.Cons",_) $ eq $ _ = ft; + mk_set thy pt p consts pred; + *) + | mk_set thy pt p (consts as Const ("List.list.Cons",_) $ eq $ _) pred = + let val (bdv,_) = HOLogic.dest_eq eq; + val pred = if pred <> Const ("Script.Assumptions",bool) + then [pred] + else (map fst) (get_assumptions_ pt (p,Res)) + in (bdv, pred) end + + | mk_set thy _ _ l _ = + raise error ("check_elementwise: no set "^ + (Syntax.string_of_term (thy2ctxt thy) l)); +(*> val consts = str2term "[x=#4]"; +> val pred = str2term "Assumptions"; +> val pt = union_asm pt p + [("#0 <= sqrt x + sqrt (#5 + x)",[11]),("#0 <= #9 + #4 * x",[22]), + ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])]; +> val p = []; +> val (sss,ttt) = mk_set thy pt p consts pred; +> (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt); +val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ... + + val consts = str2term "UniversalList"; + val pred = str2term "Assumptions"; + +*) + + + +(*check a list (/set) of constants [c_1,..,c_n] for c_i:set (: in)*) +(* val (erls,consts,(bdv,pred)) = (erl,ft,vp); + val (consts,(bdv,pred)) = (ft,vp); + *) +fun check_elementwise thy erls all_results (bdv, asm) = + let (*bdv extracted from ~~~~~~~~~~~ in mk_set already*) + fun check sub = + let val inst_ = map (subst_atomic [sub]) asm + in case eval__true thy 1 inst_ [] erls of + (asm', true) => ([HOLogic.mk_eq sub], asm') + | (_, false) => ([],[]) + end; + (*val _= writeln("### check_elementwise: res= "^(term2str all_results)^ + ", bdv= "^(term2str bdv)^", asm= "^(terms2str asm));*) + val c' = isalist2list all_results + val c'' = map (snd o HOLogic.dest_eq) c' (*assumes [x=1,x=2,..]*) + val subs = map (pair bdv) c'' + in if asm = [] then (all_results, []) + else ((apfst ((list2isalist bool) o flat)) o + (apsnd flat) o split_list o (map check)) subs end; +(* 20.5.03 +> val all_results = str2term "[x=a+b,x=b,x=3]"; +> val bdv = str2term "x"; +> val asm = str2term "(x ~= a) & (x ~= b)"; +> val erls = e_rls; +> val (t, ts) = check_elementwise thy erls all_results (bdv, asm); +> term2str t; writeln(terms2str ts); +val it = "[x = a + b, x = b, x = c]" : string +["a + b ~= a & a + b ~= b","b ~= a & b ~= b","c ~= a & c ~= b"] +... with appropriate erls this should be: +val it = "[x = a + b, x = c]" : string +["b ~= 0 & a ~= 0", "3 ~= a & 3 ~= b"] + ////// because b ~= b False*) + + + +(*before 5.03----- +> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\ + \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4"; +> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct; +val ct' = "True" : cterm' + +> val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\ + \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4"; +> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct; +val ct' = "True" : cterm' + + +> val const = (term_of o the o (parse thy)) "(#3::real)"; +> val pred' = subst_atomic [(bdv,const)] pred; + + +> val consts = (term_of o the o (parse thy)) "[x = #-3, x = #3]"; +> val bdv = (term_of o the o (parse thy)) "(x::real)"; +> val pred = (term_of o the o (parse thy)) + "((#0 <= #18 & #0 <= sqrt (#5 + x) + sqrt (#5 - x)) & #0 <= #25 + #-1 * x ^^^ #2) & #0 <= #4"; +> val ttt = check_elementwise thy consts (bdv, pred); +> (cterm_of thy) ttt; +val it = "[x = #-3, x = #3]" : cterm + +> val consts = (term_of o the o (parse thy)) "[x = #4]"; +> val bdv = (term_of o the o (parse thy)) "(x::real)"; +> val pred = (term_of o the o (parse thy)) + "#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #5 * x & #0 <= #2 + x"; +> val ttt = check_elementwise thy consts (bdv,pred); +> (cterm_of thy) ttt; +val it = "[x = #4]" : cterm + +> val consts = (term_of o the o (parse thy)) "[x = #-12 // #5]"; +> val bdv = (term_of o the o (parse thy)) "(x::real)"; +> val pred = (term_of o the o (parse thy)) + " #0 <= sqrt x + sqrt (#-3 + x) & #0 <= #9 + #4 * x & #0 <= x ^^^ #2 + #-3 * x & #0 <= #6 + x"; +> val ttt = check_elementwise thy consts (bdv,pred); +> (cterm_of thy) ttt; +val it = "[]" : cterm*) + + +(* 14.1.01: for Tac-dummies in root-equ only: skip str until "("*) +fun split_dummy str = +let fun scan s' [] = (implode s', "") + | scan s' (s::ss) = if s=" " then (implode s', implode ss) + else scan (s'@[s]) ss; +in ((scan []) o explode) str end; +(* split_dummy "subproblem_equation_dummy (x=-#5//#12)"; +val it = ("subproblem_equation_dummy","(x=-#5//#12)") : string * string +> split_dummy "x=-#5//#12"; +val it = ("x=-#5//#12","") : string * string*) + + + + +(*.applicability of a tacic wrt. a calc-state (ptree,pos'). + additionally used by next_tac in the script-interpreter for sequence-tacs. + tests for applicability are so expensive, that results (rewrites!) + are kept in the return-value of 'type tac_'. +.*) +fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = + Appl (Init_Proof' (ct', spec)) + + | applicable_in (p,p_) pt Model_Problem = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str Model_Problem)^ + " not for pos "^(pos'2str (p,p_))) + else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p + val {ppc,...} = get_pbt pI' + val pbl = init_pbl ppc + in Appl (Model_Problem' (pI', pbl, [])) end +(* val Refine_Tacitly pI = m; + *) + | applicable_in (p,p_) pt (Refine_Tacitly pI) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Refine_Tacitly pI))^ + " not for pos "^(pos'2str (p,p_))) + else (* val Refine_Tacitly pI = m; + *) + let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p; + val opt = refine_ori oris pI; + in case opt of + SOME pblID => + Appl (Refine_Tacitly' (pI, pblID, + e_domID, e_metID, [](*filled in specify*))) + | NONE => Notappl ((tac2str (Refine_Tacitly pI))^ + " not applicable") end +(* val (p,p_) = ip; + val Refine_Problem pI = m; + *) + | applicable_in (p,p_) pt (Refine_Problem pI) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Refine_Problem pI))^ + " not for pos "^(pos'2str (p,p_))) + else + let val (PblObj {origin=(_,(dI,_,_),_),spec=(dI',_,_), + probl=itms, ...}) = get_obj I pt p; + val thy = if dI' = e_domID then dI else dI'; + val rfopt = refine_pbl (assoc_thy thy) pI itms; + in case rfopt of + NONE => Notappl ((tac2str (Refine_Problem pI))^" not applicable") + | SOME (rf as (pI',_)) => +(* val SOME (rf as (pI',_)) = rfopt; + *) + if pI' = pI + then Notappl ((tac2str (Refine_Problem pI))^" not applicable") + else Appl (Refine_Problem' rf) + end + + (*the specify-tacs have cterm' instead term: + parse+error here!!!: see appl_add*) + | applicable_in (p,p_) pt (Add_Given ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Add_Given ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Add_Given' (ct', [(*filled in specify_additem*)])) + (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*) + + | applicable_in (p,p_) pt (Del_Given ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Del_Given ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Del_Given' ct') + + | applicable_in (p,p_) pt (Add_Find ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Add_Find ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Add_Find' (ct', [(*filled in specify_additem*)])) + + | applicable_in (p,p_) pt (Del_Find ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Del_Find ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Del_Find' ct') + + | applicable_in (p,p_) pt (Add_Relation ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Add_Relation ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Add_Relation' (ct', [(*filled in specify_additem*)])) + + | applicable_in (p,p_) pt (Del_Relation ct') = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Del_Relation ct'))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Del_Relation' ct') + + | applicable_in (p,p_) pt (Specify_Theory dI) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Specify_Theory dI))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Specify_Theory' dI) +(* val (p,p_) = p; val Specify_Problem pID = m; + val Specify_Problem pID = m; + *) + | applicable_in (p,p_) pt (Specify_Problem pID) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Specify_Problem pID))^ + " not for pos "^(pos'2str (p,p_))) + else + let val (PblObj {origin=(oris,(dI,pI,_),_),spec=(dI',pI',_), + probl=itms, ...}) = get_obj I pt p; + val thy = assoc_thy (if dI' = e_domID then dI else dI'); + val {ppc,where_,prls,...} = get_pbt pID; + val pbl = if pI'=e_pblID andalso pI=e_pblID + then (false, (init_pbl ppc, [])) + else match_itms_oris thy itms (ppc,where_,prls) oris; + in Appl (Specify_Problem' (pID, pbl)) end +(* val Specify_Method mID = nxt; val (p,p_) = p; + *) + | applicable_in (p,p_) pt (Specify_Method mID) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Specify_Method mID))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Specify_Method' (mID,[(*filled in specify*)], + [(*filled in specify*)])) + + | applicable_in (p,p_) pt (Apply_Method mI) = + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res + then Notappl ((tac2str (Apply_Method mI))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Apply_Method' (mI, NONE, e_istate (*filled in solve*))) + + | applicable_in (p,p_) pt (Check_Postcond pI) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str (Check_Postcond pI))^ + " not for pos "^(pos'2str (p,p_))) + else Appl (Check_Postcond' + (pI,(e_term,[(*asm in solve*)]))) + (* in solve -"- ^^^^^^ gets returnvalue of scr*) + + (*these are always applicable*) + | applicable_in (p,p_) _ (Take str) = Appl (Take' (str2term str)) + | applicable_in (p,p_) _ (Free_Solve) = Appl (Free_Solve') + +(* val m as Rewrite_Inst (subs, thm') = m; + *) + | applicable_in (p,p_) pt (m as Rewrite_Inst (subs, thm')) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val {rew_ord'=ro',erls=erls,...} = + get_met (get_obj g_metID pt pp); + val (f,p) = case p_ of (*p 12.4.00 unnecessary*) + Frm => (get_obj g_form pt p, p) + | Res => ((fst o (get_obj g_result pt)) p, lev_on p) + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in + let val subst = subs2subst thy subs; + val subs' = subst2subs' subst; + in case rewrite_inst_ thy (assoc_rew_ord ro') erls + (*put_asm*)false subst (assoc_thm' thy thm') f of + SOME (f',asm) => Appl ( + Rewrite_Inst' (thy',ro',erls,(*put_asm*)false,subst,thm', + (*term_of o the o (parse (assoc_thy thy'))*) f, + (*(term_of o the o (parse (assoc_thy thy'))*) (f', + (*map (term_of o the o (parse (assoc_thy thy')))*) asm))) + | NONE => Notappl ((fst thm')^" not applicable") end + handle _ => Notappl ("syntax error in "^(subs2str subs)) end + +(* val ((p,p_), pt, m as Rewrite thm') = (p, pt, m); + val ((p,p_), pt, m as Rewrite thm') = (pos, pt, tac); + *) +| applicable_in (p,p_) pt (m as Rewrite thm') = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let val (msg,thy',ro,rls',(*put_asm*)_)= from_pblobj_or_detail_thm thm' p pt; + val thy = assoc_thy thy'; + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + | _ => raise error ("applicable_in Rewrite: call by "^ + (pos'2str (p,p_))); + in if msg = "OK" + then + ((*writeln("### applicable_in rls'= "^rls');*) + (* val SOME (f',asm)=rewrite thy' ro (id_rls rls') put_asm thm' f; + *) + case rewrite_ thy (assoc_rew_ord ro) + rls' false (assoc_thm' thy thm') f of + SOME (f',asm) => Appl ( + Rewrite' (thy',ro,rls',(*put_asm*)false,thm', f, (f', asm))) + | NONE => Notappl ("'"^(fst thm')^"' not applicable") ) + else Notappl msg + end + +| applicable_in (p,p_) pt (m as Rewrite_Asm thm') = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val {rew_ord'=ro',erls=erls,...} = + get_met (get_obj g_metID pt pp); + (*val put_asm = true;*) + val (f,p) = case p_ of (*p 12.4.00 unnecessary*) + Frm => (get_obj g_form pt p, p) + | Res => ((fst o (get_obj g_result pt)) p, lev_on p) + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in case rewrite_ thy (assoc_rew_ord ro') erls + (*put_asm*)false (assoc_thm' thy thm') f of + SOME (f',asm) => Appl ( + Rewrite' (thy',ro',erls,(*put_asm*)false,thm', f, (f', asm))) + | NONE => Notappl ("'"^(fst thm')^"' not applicable") end + + | applicable_in (p,p_) pt (m as Detail_Set_Inst (subs, rls)) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val {rew_ord'=ro',...} = get_met (get_obj g_metID pt pp); + val f = case p_ of Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in + let val subst = subs2subst thy subs + val subs' = subst2subs' subst + in case rewrite_set_inst_ thy false subst (assoc_rls rls) f of + SOME (f',asm) => Appl ( + Detail_Set_Inst' (thy',false,subst,assoc_rls rls, f, (f', asm))) + | NONE => Notappl (rls^" not applicable") end + handle _ => Notappl ("syntax error in "^(subs2str subs)) end + + | applicable_in (p,p_) pt (m as Rewrite_Set_Inst (subs, rls)) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val {rew_ord'=ro',(*asm_rls=asm_rls,*)...} = + get_met (get_obj g_metID pt pp); + val (f,p) = case p_ of (*p 12.4.00 unnecessary*) + Frm => (get_obj g_form pt p, p) + | Res => ((fst o (get_obj g_result pt)) p, lev_on p) + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in + let val subst = subs2subst thy subs; + val subs' = subst2subs' subst; + in case rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of + SOME (f',asm) => Appl ( + Rewrite_Set_Inst' (thy',(*put_asm*)false,subst,assoc_rls rls, f, (f', asm))) + | NONE => Notappl (rls^" not applicable") end + handle _ => Notappl ("syntax error in "^(subs2str subs)) end + + | applicable_in (p,p_) pt (m as Rewrite_Set rls) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val (f,p) = case p_ of (*p 12.4.00 unnecessary*) + Frm => (get_obj g_form pt p, p) + | Res => ((fst o (get_obj g_result pt)) p, lev_on p) + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of + SOME (f',asm) => + ((*writeln("#.# applicable_in Rewrite_Set,2f'= "^f');*) + Appl (Rewrite_Set' (thy',(*put_asm*)false,assoc_rls rls, f, (f', asm))) + ) + | NONE => Notappl (rls^" not applicable") end + + | applicable_in (p,p_) pt (m as Detail_Set rls) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let val pp = par_pblobj pt p + val thy' = (get_obj g_domID pt pp):theory' + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + in case rewrite_set_ (assoc_thy thy') false (assoc_rls rls) f of + SOME (f',asm) => + Appl (Detail_Set' (thy',false,assoc_rls rls, f, (f',asm))) + | NONE => Notappl (rls^" not applicable") end + + + | applicable_in p pt (End_Ruleset) = + raise error ("applicable_in: not impl. for "^ + (tac2str End_Ruleset)) + +(* val ((p,p_), pt, (m as Calculate op_)) = (p, pt, m); + *) +| applicable_in (p,p_) pt (m as Calculate op_) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt; + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + in if msg = "OK" then + case calculate_ (assoc_thy thy') isa_fn f of + SOME (f', (id, thm)) => + Appl (Calculate' (thy',op_, f, (f', (id, string_of_thmI thm)))) + | NONE => Notappl ("'calculate "^op_^"' not applicable") + else Notappl msg + end + +(*Substitute combines two different kind of "substitution": + (1) subst_atomic: for ?a..?z + (2) Pattern.match: for solving equational systems + (which raises exn for ?a..?z)*) + | applicable_in (p,p_) pt (m as Substitute sube) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else let val pp = par_pblobj pt p + val thy = assoc_thy (get_obj g_domID pt pp) + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp) + val subte = sube2subte sube + val subst = sube2subst thy sube + in if foldl and_ (true, map contains_Var subte) + (*1*) + then let val f' = subst_atomic subst f + in if f = f' then Notappl (sube2str sube^" not applicable") + else Appl (Substitute' (subte, f, f')) + end + (*2*) + else case rewrite_terms_ thy (assoc_rew_ord rew_ord') + erls subte f of + SOME (f', _) => Appl (Substitute' (subte, f, f')) + | NONE => Notappl (sube2str sube^" not applicable") + end +(*-------WN08114 interrupted with error in polyminus.sml "11 = 11" + | applicable_in (p,p_) pt (m as Substitute sube) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else let val pp = par_pblobj pt p + val thy = assoc_thy (get_obj g_domID pt pp) + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p + val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp) + val subte = sube2subte sube + in case rewrite_terms_ thy (assoc_rew_ord rew_ord') erls subte f of + SOME (f', _) => Appl (Substitute' (subte, f, f')) + | NONE => Notappl (sube2str sube^" not applicable") + end +------------------*) + + | applicable_in p pt (Apply_Assumption cts') = + (raise error ("applicable_in: not impl. for "^ + (tac2str (Apply_Assumption cts')))) + + (*'logical' applicability wrt. script in locate: Inconsistent?*) + | applicable_in (p,p_) pt (m as Take ct') = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let val thy' = get_obj g_domID pt (par_pblobj pt p); + in (case parse (assoc_thy thy') ct' of + SOME ct => Appl (Take' (term_of ct)) + | NONE => Notappl ("syntax error in "^ct')) + end + + | applicable_in p pt (Take_Inst ct') = + raise error ("applicable_in: not impl. for "^ + (tac2str (Take_Inst ct'))) + + | applicable_in p pt (Group (con, ints)) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Group (con, ints)))) + + | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = + if member op = [Pbl,Met] p_ + then (*maybe Apply_Method has already been done*) + case get_obj g_env pt p of + SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], + e_term, [], subpbl domID pblID)) + | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else (*somewhere later in the script*) + Appl (Subproblem' ((domID, pblID, e_metID), [], + e_term, [], subpbl domID pblID)) + + | applicable_in p pt (End_Subproblem) = + raise error ("applicable_in: not impl. for "^ + (tac2str (End_Subproblem))) + + | applicable_in p pt (CAScmd ct') = + raise error ("applicable_in: not impl. for "^ + (tac2str (CAScmd ct'))) + + | applicable_in p pt (Split_And) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Split_And))) + | applicable_in p pt (Conclude_And) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Conclude_And))) + | applicable_in p pt (Split_Or) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Split_Or))) + | applicable_in p pt (Conclude_Or) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Conclude_Or))) + + | applicable_in (p,p_) pt (Begin_Trans) = + let + val (f,p) = case p_ of (*p 12.4.00 unnecessary*) + (*_____ implizit Take in gen*) + Frm => (get_obj g_form pt p, (lev_on o lev_dn) p) + | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p) + | _ => raise error ("applicable_in: call by "^ + (pos'2str (p,p_))); + val thy' = get_obj g_domID pt (par_pblobj pt p); + in (Appl (Begin_Trans' f)) + handle _ => raise error ("applicable_in: Begin_Trans finds \ + \syntaxerror in '"^(term2str f)^"'") end + + (*TODO: check parent branches*) + | applicable_in (p,p_) pt (End_Trans) = + let val thy' = get_obj g_domID pt (par_pblobj pt p); + in if p_ = Res + then Appl (End_Trans' (get_obj g_result pt p)) + else Notappl "'End_Trans' is not applicable at \ + \the beginning of a transitive sequence" + (*TODO: check parent branches*) + end + + | applicable_in p pt (Begin_Sequ) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Begin_Sequ))) + | applicable_in p pt (End_Sequ) = + raise error ("applicable_in: not impl. for "^ + (tac2str (End_Sequ))) + | applicable_in p pt (Split_Intersect) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Split_Intersect))) + | applicable_in p pt (End_Intersect) = + raise error ("applicable_in: not impl. for "^ + (tac2str (End_Intersect))) +(* val Appl (Check_elementwse'(t1,"Assumptions",t2)) = it; + val (vvv,ppp) = vp; + + val Check_elementwise pred = m; + + val ((p,p_), Check_elementwise pred) = (p, m); + *) + | applicable_in (p,p_) pt (m as Check_elementwise pred) = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy' + val metID = (get_obj g_metID pt pp) + val {crls,...} = get_met metID + (*val _=writeln("### applicable_in Check_elementwise: crls= "^crls) + val _=writeln("### applicable_in Check_elementwise: pred= "^pred)*) + (*val erl = the (assoc'(!ruleset',crls))*) + val (f,asm) = case p_ of + Frm => (get_obj g_form pt p , []) + | Res => get_obj g_result pt p; + (*val _= writeln("### applicable_in Check_elementwise: f= "^f);*) + val vp = mk_set thy pt p f ((term_of o the o (parse thy)) pred); + (*val (v,p)=vp;val _=writeln("### applicable_in Check_elementwise: vp= "^ + pair2str(term2str v,term2str p))*) + in case f of + Const ("List.list.Cons",_) $ _ $ _ => + Appl (Check_elementwise' + (f, pred, + ((*writeln("### applicable_in Check_elementwise: --> "^ + (res2str (check_elementwise thy crls f vp)));*) + check_elementwise thy crls f vp))) + | Const ("Tools.UniversalList",_) => + Appl (Check_elementwise' (f, pred, (f,asm))) + | Const ("List.list.Nil",_) => + (*Notappl "not applicable to empty list" 3.6.03*) + Appl (Check_elementwise' (f, pred, (f,asm(*[] 11.6.03???*)))) + | _ => Notappl ("not applicable: "^(term2str f)^" should be constants") + end + + | applicable_in (p,p_) pt Or_to_List = + if member op = [Pbl,Met] p_ + then Notappl ((tac2str Or_to_List)^" not for pos "^(pos'2str (p,p_))) + else + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p; + in (let val ls = or2list f + in Appl (Or_to_List' (f, ls)) end) + handle _ => Notappl ("'Or_to_List' not applicable to "^(term2str f)) + end + + | applicable_in p pt (Collect_Trues) = + raise error ("applicable_in: not impl. for "^ + (tac2str (Collect_Trues))) + + | applicable_in p pt (Empty_Tac) = + Notappl "Empty_Tac is not applicable" + + | applicable_in (p,p_) pt (Tac id) = + let + val pp = par_pblobj pt p; + val thy' = (get_obj g_domID pt pp):theory'; + val thy = assoc_thy thy'; + val f = case p_ of + Frm => get_obj g_form pt p + | Res => (fst o (get_obj g_result pt)) p; + in case id of + "subproblem_equation_dummy" => + if is_expliceq f + then Appl (Tac_ (thy, term2str f, id, + "subproblem_equation_dummy ("^(term2str f)^")")) + else Notappl "applicable only to equations made explicit" + | "solve_equation_dummy" => + let (*val _= writeln("### applicable_in: solve_equation_dummy: f= " + ^f);*) + val (id',f') = split_dummy (term2str f); + (*val _= writeln("### applicable_in: f'= "^f');*) + (*val _= (term_of o the o (parse thy)) f';*) + (*val _= writeln"### applicable_in: solve_equation_dummy";*) + in if id' <> "subproblem_equation_dummy" then Notappl "no subproblem" + else if is_expliceq ((term_of o the o (parse thy)) f') + then Appl (Tac_ (thy, term2str f, id, "[" ^ f' ^ "]")) + else error ("applicable_in: f= " ^ f') end + | _ => Appl (Tac_ (thy, term2str f, id, term2str f)) end + + | applicable_in p pt End_Proof' = Appl End_Proof'' + + | applicable_in _ _ m = + raise error ("applicable_in called for "^(tac2str m)); + +(*WN060614 unused*) +fun tac2tac_ pt p m = + case applicable_in p pt m of + Appl (m') => m' + | Notappl _ => raise error ("tac2mstp': fails with"^ + (tac2str m)); +