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