neuper@37906: (* interpreter for scripts neuper@37906: (c) Walther Neuper 2000 neuper@37906: neuper@37906: use"ME/script.sml"; neuper@37906: use"script.sml"; neuper@37906: *) neuper@37906: signature INTERPRETER = neuper@37906: sig neuper@37906: (*type ets (list of executed tactics) see sequent.sml*) neuper@37906: neuper@37906: datatype locate neuper@37906: = NotLocatable neuper@37906: | Steps of (tac_ * mout * ptree * pos' * cid * safe (* ets*)) list neuper@37906: (* | ToDo of ets 28.4.02*) neuper@37906: neuper@37906: (*diss: next-tactic-function*) neuper@37906: val next_tac : theory' -> ptree * pos' -> metID -> scr -> ets -> tac_ neuper@37906: (*diss: locate-function*) neuper@37906: val locate_gen : theory' neuper@37906: -> tac_ neuper@37906: -> ptree * pos' -> scr * rls -> ets -> loc_ -> locate neuper@37906: neuper@37906: val sel_rules : ptree -> pos' -> tac list neuper@37906: val init_form : scr -> ets -> loc_ * term option (*FIXME not up to date*) neuper@37906: val formal_args : term -> term list neuper@37906: neuper@37906: (*shift to library ...*) neuper@37906: val inst_abs : theory' -> term -> term neuper@37906: val itms2args : metID -> itm list -> term list neuper@37906: val user_interrupt : loc_ * (tac_ * env * env * term * term * safe) neuper@37906: (*val empty : term*) neuper@37906: end neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* neuper@37906: structure Interpreter : INTERPRETER = neuper@37906: struct neuper@37906: *) neuper@37906: neuper@37906: (*.traces the leaves (ie. non-tactical nodes) of the script neuper@37906: found by next_tac. neuper@37906: a leaf is either a tactic or an 'exp' in 'let v = expr' neuper@37906: where 'exp' does not contain a tactic.*) neuper@38006: val trace_script = Unsynchronized.ref false; neuper@37906: neuper@37906: type step = (*data for creating a new node in the ptree; neuper@37906: designed for use: neuper@37906: fun ass* scrstate steps = neuper@37906: ... case ass* scrstate steps of neuper@37906: Assoc (scrstate, steps) => ... ass* scrstate steps*) neuper@37906: tac_ (*transformed from associated tac*) neuper@37906: * mout (*result with indentation etc.*) neuper@37906: * ptree (*containing node created by tac_ + resp. scrstate*) neuper@37906: * pos' (*position in ptree; ptree * pos' is the proofstate*) neuper@37906: * pos' list; (*of ptree-nodes probably cut (by fst tac_)*) neuper@37906: val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step; neuper@37906: neuper@37906: fun rule2thm' (Thm (id, thm)) = (id, string_of_thmI thm):thm' neuper@38031: | rule2thm' r = error ("rule2thm': not defined for "^(rule2str r)); neuper@37906: fun rule2rls' (Rls_ rls) = id_rls rls neuper@38031: | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r)); neuper@37906: neuper@37906: (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve; neuper@37906: complicated with current t in rrlsstate.*) neuper@37906: fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] = neuper@41996: let neuper@41996: val thy = assoc_thy thy' neuper@41996: val ctxt = get_ctxt pt p |> insert_assumptions am neuper@41996: val m = Rewrite' (thy', ro, er, pa, rule2thm' r, f, (f', am)) neuper@41996: val is = RrlsState (f', f'', rss, rts) neuper@41996: val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res) neuper@41996: val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt neuper@41996: in (is, (m, mout, pt', p', cid) :: steps) end neuper@41996: | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) ((r, (f', am))::rts') = neuper@41996: let neuper@41996: val thy = assoc_thy thy' neuper@41996: val ctxt = get_ctxt pt p |> insert_assumptions am neuper@41996: val m = Rewrite' (thy',ro,er,pa, rule2thm' r, f, (f', am)) neuper@41996: val is = RrlsState (f',f'',rss,rts) neuper@41996: val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res) neuper@41996: val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt neuper@41996: in rts2steps ((m, mout, pt', p', cid)::steps) neuper@41996: ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end; neuper@37906: neuper@37906: (*. functions for the environment stack .*) neuper@37906: fun accessenv id es = the (assoc((top es):env, id)) neuper@37906: handle _ => error ("accessenv: "^(free2str id)^" not in env"); neuper@37906: fun updateenv id vl (es:env stack) = neuper@37906: (push (overwrite(top es, (id, vl))) (pop es)):env stack; neuper@37906: fun pushenv id vl (es:env stack) = neuper@37906: (push (overwrite(top es, (id, vl))) es):env stack; neuper@37906: val popenv = pop:env stack -> env stack; neuper@37906: neuper@37906: neuper@37906: neuper@37906: fun de_esc_underscore str = neuper@37906: let fun scan [] = [] neuper@37906: | scan (s::ss) = if s = "'" then (scan ss) neuper@37906: else (s::(scan ss)) neuper@40836: in (implode o scan o Symbol.explode) str end; neuper@37906: (* neuper@37906: > val str = "Rewrite_Set_Inst"; neuper@37906: > val esc = esc_underscore str; neuper@37906: val it = "Rewrite'_Set'_Inst" : string neuper@37906: > val des = de_esc_underscore esc; neuper@37906: val des = de_esc_underscore esc;*) neuper@37906: neuper@37906: (*go at a location in a script and fetch the contents*) neuper@37906: fun go [] t = t neuper@37906: | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0 neuper@37906: | go (L::p) (t1 $ t2) = go p t1 neuper@37906: | go (R::p) (t1 $ t2) = go p t2 neuper@38031: | go l _ = error ("go: no "^(loc_2str l)); neuper@37906: (* neuper@37906: > val t = (term_of o the o (parse thy)) "a+b"; neuper@37906: val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term neuper@37906: > val plus_a = go [L] t; neuper@37906: > val b = go [R] t; neuper@37906: > val plus = go [L,L] t; neuper@37906: > val a = go [L,R] t; neuper@37906: neuper@37906: > val t = (term_of o the o (parse thy)) "a+b+c"; neuper@37906: val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term neuper@37906: > val pl_pl_a_b = go [L] t; neuper@37906: > val c = go [R] t; neuper@37906: > val a = go [L,R,L,R] t; neuper@37906: > val b = go [L,R,R] t; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (* get a subterm t with test t, and record location *) neuper@37906: fun get l test (t as Const (s,T)) = neuper@37926: if test t then SOME (l,t) else NONE neuper@37906: | get l test (t as Free (s,T)) = neuper@37926: if test t then SOME (l,t) else NONE neuper@37906: | get l test (t as Bound n) = neuper@37926: if test t then SOME (l,t) else NONE neuper@37906: | get l test (t as Var (s,T)) = neuper@37926: if test t then SOME (l,t) else NONE neuper@37906: | get l test (t as Abs (s,T,body)) = neuper@37926: if test t then SOME (l:loc_,t) else get ((l@[D]):loc_) test body neuper@37906: | get l test (t as t1 $ t2) = neuper@37926: if test t then SOME (l,t) neuper@37906: else case get (l@[L]) test t1 of neuper@37926: NONE => get (l@[R]) test t2 neuper@37926: | SOME (l',t') => SOME (l',t'); neuper@37906: (*18.6.00 neuper@37906: > val sss = ((term_of o the o (parse thy)) neuper@37906: "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ neuper@37906: \ (let e_ = Try (Rewrite square_equation_left True eq_) \ neuper@37906: \ in [e_])"); neuper@37906: ______ compares head_of !! neuper@41968: > get [] (eq_str "HOL.Let") sss; [R] neuper@37906: > get [] (eq_str "Script.Try") sss; [R,L,R] neuper@37906: > get [] (eq_str "Script.Rewrite") sss; [R,L,R,R] neuper@41928: > get [] (eq_str "HOL.True") sss; [R,L,R,R,L,R] neuper@37906: > get [] (eq_str "e_") sss; [R,R] neuper@37906: *) neuper@37906: neuper@37930: fun test_negotiable t = neuper@37937: member op = (!negotiable) neuper@40836: ((strip_thy o (term_str (Thy_Info.get_theory "Script")) o head_of) t); neuper@37906: neuper@37906: (*.get argument of first stactic in a script for init_form.*) neuper@37906: fun get_stac thy (h $ body) = neuper@37906: let neuper@37906: fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = neuper@37926: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@37906: | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = neuper@37926: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@37906: | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a neuper@37906: | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a neuper@37906: | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a neuper@37906: | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a neuper@37906: | get_t y (Const ("Script.Or",_) $e1 $ e2) a = neuper@37926: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@37906: | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ = neuper@37926: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@37906: | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a neuper@37906: | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a neuper@37906: | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a = neuper@37926: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@41968: (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a = neuper@41999: (case get_t y e1 a of NONE => get_t y e2 a | la => la) neuper@37906: | get_t y (Abs (_,_,e)) a = get_t y e a*) neuper@41968: | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a = neuper@37906: get_t y e1 a (*don't go deeper without evaluation !*) neuper@37926: | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE neuper@37926: (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*) neuper@37906: neuper@37926: | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a neuper@37926: | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a neuper@37926: | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a neuper@37926: | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a neuper@37906: neuper@37926: | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a neuper@37926: | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a neuper@37906: neuper@37926: | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE neuper@37906: neuper@37906: | get_t y x _ = neuper@38015: ((*tracing ("### get_t yac: list-expr "^(term2str x));*) neuper@37926: NONE) neuper@37906: in get_t thy body e_term end; neuper@37906: neuper@37906: (*FIXME: get 1st stac by next_stac [] instead of ... ?? 29.7.02*) neuper@37906: (* val Script sc = scr; neuper@37906: *) neuper@37906: fun init_form thy (Script sc) env = neuper@37906: (case get_stac thy sc of neuper@38053: NONE => NONE neuper@38053: (*error ("init_form: no 1st stac in "^ neuper@38053: (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) sc))*) neuper@37926: | SOME stac => SOME (subst_atomic env stac)) neuper@38031: | init_form _ _ _ = error "init_form: no match"; neuper@37906: neuper@37906: (* use"ME/script.sml"; neuper@37906: use"script.sml"; neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*the 'iteration-argument' of a stac (args not eval)*) neuper@37906: fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v neuper@37906: | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v neuper@37906: | itr_arg _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ v) = v neuper@37906: | itr_arg _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ v) = v neuper@37906: | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v neuper@37906: | itr_arg _ (Const ("Script.Check'_elementwise",_) $ consts $ _) = consts neuper@37906: | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term neuper@37906: | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term neuper@37906: | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term neuper@38031: | itr_arg thy t = error neuper@38053: ("itr_arg not impl. for " ^ neuper@38053: (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt (assoc_thy thy))) t)); neuper@37906: (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_"; neuper@38058: > itr_arg "Script" t; neuper@37906: val it = Free ("e_","RealDef.real") : term neuper@37906: > val t = (term_of o the o (parse thy))"xxx"; neuper@38058: > itr_arg "Script" t; neuper@37906: *** itr_arg not impl. for xxx neuper@37906: uncaught exception ERROR neuper@37906: raised at: library.ML:1114.35-1114.40*) neuper@37906: neuper@37906: neuper@37906: (*.get the arguments of the script out of the scripts parsetree.*) neuper@37906: fun formal_args scr = (fst o split_last o snd o strip_comb) scr; neuper@37906: (* neuper@37906: > formal_args scr; neuper@37906: [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"), neuper@37906: Free ("eqs_","bool List.list")] : term list neuper@37906: *) neuper@37906: neuper@37906: (*.get the identifier of the script out of the scripts parsetree.*) neuper@37906: fun id_of_scr sc = (id_of o fst o strip_comb) sc; neuper@37906: neuper@37906: (*WN020526: not clear, when a is available in ass_up for eva-_true*) neuper@37926: (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS neuper@37906: curried Rewrite) for CURRENT value (which may be different from PREVIOUS); neuper@37926: thus "NONE" must be set at the end of currying (ill designed anyway)*) neuper@37926: fun upd_env_opt env (SOME a, v) = upd_env env (a,v) neuper@37926: | upd_env_opt env (NONE, v) = neuper@41996: (tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")"); env); neuper@37906: neuper@37906: type dsc = typ; (*<-> nam..unknow in Descript.thy*) neuper@37906: fun typ_str (Type (s,_)) = s neuper@37906: | typ_str (TFree(s,_)) = s neuper@41996: | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i); neuper@37906: neuper@37906: (*get the _result_-type of a description*) neuper@37906: fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T; neuper@37906: (*> val t = (term_of o the o (parse thy)) "equality"; neuper@37906: > val T = type_of t; neuper@37906: val T = "bool => Tools.una" : typ neuper@37906: > val dsc = dsc_valT t; neuper@37906: val dsc = "una" : string neuper@37906: neuper@37906: > val t = (term_of o the o (parse thy)) "fixedValues"; neuper@37906: > val T = type_of t; neuper@37906: val T = "bool List.list => Tools.nam" : typ neuper@37906: > val dsc = dsc_valT t; neuper@37906: val dsc = "nam" : string*) neuper@37906: neuper@37906: (*.from penv in itm_ make args for script depending on type of description.*) neuper@37906: (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv neuper@37906: 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*) neuper@38053: fun mk_arg thy d [] = neuper@38053: error ("mk_arg: no data for " ^ neuper@38053: (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) d)) neuper@37906: | mk_arg thy d [t] = neuper@37906: (case dsc_valT d of neuper@37906: "una" => [t] neuper@37906: | "nam" => neuper@37906: [case t of neuper@41922: r as (Const ("HOL.eq",_) $ _ $ _) => r neuper@38053: | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality "^ neuper@38053: (Print_Mode.setmp [] (Syntax.string_of_term neuper@38053: (thy2ctxt thy)) t))] neuper@38031: | s => error ("mk_arg: not impl. for "^s)) neuper@37906: neuper@37906: | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts); neuper@37906: (* neuper@37906: val d = d_in itm_; neuper@37906: val [t] = ts_in itm_; neuper@37906: mk_arg thy neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (*.create the actual parameters (args) of script: their order neuper@37906: is given by the order in met.pat .*) neuper@37906: (*WN.5.5.03: ?: does this allow for different descriptions ??? neuper@37906: ?: why not taken from formal args of script ??? neuper@37906: !: FIXXXME penv: push it here in itms2args into script-evaluation*) neuper@37906: (* val (thy, mI, itms) = (thy, metID, itms); neuper@37906: *) neuper@37906: fun itms2args thy mI (itms:itm list) = neuper@37906: let val mvat = max_vt itms neuper@37935: fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b neuper@37906: val itms = filter (okv mvat) itms neuper@37906: fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_) neuper@37906: fun itm2arg itms (_,(d,_)) = neuper@37906: case find_first (test_dsc d) itms of neuper@37926: NONE => neuper@38031: error ("itms2args: '"^term2str d^"' not in itms") neuper@37926: (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_); neuper@37906: penv postponed; presently penv holds already env for script*) neuper@37926: | SOME (_,_,_,_,itm_) => penvval_in itm_ neuper@37906: fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find") neuper@37906: val pats = (#ppc o get_met) mI neuper@37906: in (flat o (map (itm2arg itms))) pats end; neuper@37906: (* neuper@37906: > val sc = ... Solve_root_equation ... neuper@38058: > val mI = ("Script","sqrt-equ-test"); neuper@37906: > val PblObj{meth={ppc=itms,...},...} = get_obj I pt []; neuper@37906: > val ts = itms2args thy mI itms; neuper@38053: > map (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))) ts; neuper@37906: ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list neuper@37906: *) neuper@37906: neuper@37906: neuper@37984: (*["BOOL (1+x=2)","REAL x"] --match_ags--> oris neuper@37906: --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"]*) neuper@37906: fun oris2fmz_vals oris = neuper@37906: let fun ori2fmz_vals ((_,_,_,dsc,ts):ori) = neuper@37906: ((term2str o comp_dts') (dsc, ts), last_elem ts) neuper@38031: handle _ => error ("ori2fmz_env called with "^terms2str ts) neuper@37906: in (split_list o (map ori2fmz_vals)) oris end; neuper@37906: neuper@37906: (*detour necessary, because generate1 delivers a string-result*) neuper@37906: fun mout2term thy (Form' (FormKF (_,_,_,_,res))) = neuper@37906: (term_of o the o (parse (assoc_thy thy))) res neuper@37906: | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl neuper@37906: at time of detection in script*) neuper@37906: neuper@37906: (*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac, neuper@37906: then convert to a 'tac_' (as required in appy). neuper@37906: arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*) neuper@37906: fun stac2tac_ pt thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ f) = neuper@41984: let neuper@41984: val tid = (de_esc_underscore o strip_thy) thmID neuper@41984: in (Rewrite (tid, (string_of_thmI o (assoc_thm' thy)) (tid,"")), Empty_Tac_) neuper@41984: end neuper@37906: neuper@41984: | stac2tac_ pt thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ f) = neuper@41984: let neuper@41984: val subML = ((map isapair2pair) o isalist2list) sub neuper@41984: val subStr = subst2subs subML neuper@41984: val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*) neuper@41984: in (Rewrite_Inst (subStr, (tid, (string_of_thmI o (assoc_thm' thy)) (tid,""))), Empty_Tac_) neuper@41984: end neuper@37906: neuper@41984: | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) = neuper@41984: (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_) neuper@37906: neuper@41984: | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ sub $ Free (rls,_) $ _ $ f) = neuper@41984: let neuper@41984: val subML = ((map isapair2pair) o isalist2list) sub; neuper@41984: val subStr = subst2subs subML; neuper@41984: in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end neuper@37906: neuper@37906: | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) = neuper@41984: (Calculate op_, Empty_Tac_) neuper@37906: neuper@37906: | stac2tac_ pt thy (Const ("Script.Take",_) $ t) = neuper@41984: (Take (term2str t), Empty_Tac_) neuper@37906: neuper@37906: | stac2tac_ pt thy (Const ("Script.Substitute",_) $ isasub $ arg) = neuper@41984: (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_) neuper@37906: neuper@37906: | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ neuper@41984: (set as Const ("Collect",_) $ Abs (_,_,pred))) = neuper@41984: (Check_elementwise (Print_Mode.setmp [] (Syntax.string_of_term neuper@41984: (thy2ctxt thy)) pred), (*set*)Empty_Tac_) neuper@37906: neuper@37906: | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = neuper@41984: (Or_to_List, Empty_Tac_) neuper@37906: neuper@41984: (*12.1.01.for subproblem_equation_dummy in root-equation *) neuper@37906: | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) = neuper@41984: (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_) neuper@37906: neuper@41990: (*compare "| assod _ (Subproblem'"*) neuper@37906: | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $ neuper@41983: (Const ("Product_Type.Pair",_) $Free (dI',_) $ neuper@41983: (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = neuper@41983: let neuper@41983: val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*); neuper@37906: val thy = maxthy (assoc_thy dI) (rootthy pt); neuper@41983: val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; neuper@41983: val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; neuper@41983: val ags = isalist2list ags'; neuper@41983: val (pI, pors, mI) = neuper@41983: if mI = ["no_met"] neuper@41983: then neuper@41983: let neuper@41983: val pors = (match_ags thy ((#ppc o get_pbt) pI) ags) neuper@41983: handle ERROR "actual args do not match formal args" neuper@41983: => (match_ags_msg pI stac ags(*raise exn*); []) neuper@41983: val pI' = refine_ori' pors pI; neuper@41983: in (pI', pors (*refinement over models with diff.prec only*), neuper@41983: (hd o #met o get_pbt) pI') end neuper@41983: else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags) neuper@41983: handle ERROR "actual args do not match formal args" neuper@41983: => (match_ags_msg pI stac ags(*raise exn*); []), mI); neuper@37906: val (fmz_, vals) = oris2fmz_vals pors; neuper@41983: val {cas,ppc,thy,...} = get_pbt pI neuper@41983: val dI = theory2theory' thy (*.take dI from _refined_ pbl.*) neuper@41983: val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt)); neuper@41992: val ctxt = ProofContext.init_global neuper@41992: val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global neuper@41992: |> declare_constraints' vals neuper@41983: val hdl = neuper@41983: case cas of neuper@41983: NONE => pblterm dI pI neuper@41983: | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t neuper@37906: val f = subpbl (strip_thy dI) pI neuper@41990: in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f)) neuper@41983: end neuper@37906: neuper@38031: | stac2tac_ pt thy t = error neuper@38053: ("stac2tac_ TODO: no match for " ^ neuper@38053: (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t)); neuper@37906: neuper@37906: fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t; neuper@37906: neuper@37906: (*test a term for being a _list_ (set ?) of constants; could be more rigorous*) neuper@37906: fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true neuper@37906: | list_of_consts (Const ("List.list.Nil",_)) = true neuper@37906: | list_of_consts _ = false; neuper@37906: (*val ttt = (term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]"; neuper@37906: > list_of_consts ttt; neuper@37906: val it = true : bool neuper@37906: > val ttt = (term_of o the o (parse thy)) "[]"; neuper@37906: > list_of_consts ttt; neuper@37906: val it = true : bool*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: datatype ass = neuper@41983: Ass of neuper@41983: tac_ * (* SubProblem gets args instantiated in assod *) neuper@41983: term (* for itr_arg, result in ets *) neuper@41983: | AssWeak of neuper@41983: tac_ * neuper@41983: term (*for itr_arg,result in ets*) neuper@41983: | NotAss; neuper@37906: neuper@37906: (*.assod: tac_ associated with stac w.r.t. d neuper@37906: args neuper@37906: pt:ptree for pushing the thy specified in rootpbl into subpbls neuper@37906: returns neuper@37906: Ass : associated: e.g. thmID in stac = thmID in m neuper@37906: +++ arg in stac = arg in m neuper@37906: AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg// neuper@37906: NotAss : e.g. thmID in stac/=/thmID in m (not =) neuper@37906: 8.01: neuper@37906: tac_ SubProblem with args completed from script neuper@37906: .*) neuper@37906: fun assod pt d (m as Rewrite_Inst' (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) stac = neuper@41983: (case stac of neuper@41983: (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) => neuper@41983: if thmID = thmID_ neuper@41983: then neuper@41983: if f = f_ neuper@41983: then ((*tracing"3### assod ..Ass";*)Ass (m,f')) neuper@41983: else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f')) neuper@41983: else ((*tracing"3### assod ..NotAss";*)NotAss) neuper@41983: | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) => neuper@41983: if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: | _ => NotAss) neuper@37906: neuper@37906: | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) stac = neuper@41983: (case stac of neuper@41983: (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) => neuper@41983: ((*tracing ("3### assod: stac = " ^ ter2str t); neuper@41983: tracing ("3### assod: f(m)= " ^ term2str f);*) neuper@41983: if thmID = thmID_ neuper@41983: then neuper@41983: if f = f_ neuper@41983: then ((*tracing"3### assod ..Ass";*)Ass (m,f')) neuper@41983: else neuper@41983: ((*tracing"### assod ..AssWeak"; neuper@41983: tracing("### assod: f(m) = " ^ term2str f); neuper@41983: tracing("### assod: f(stac)= " ^ term2str f_)*) neuper@41983: AssWeak (m,f')) neuper@41983: else ((*tracing"3### assod ..NotAss";*)NotAss)) neuper@37906: | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) => neuper@41983: if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls_) neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: | _ => NotAss) neuper@37906: neuper@37906: | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm))) neuper@41983: (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) = neuper@41983: if id_rls rls = rls_ neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: neuper@37906: | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm))) neuper@41983: (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) = neuper@41983: if id_rls rls = rls_ neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: neuper@37906: | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm))) neuper@41983: (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) = neuper@41983: if id_rls rls = rls_ neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: neuper@37906: | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm))) neuper@41983: (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) = neuper@41983: if id_rls rls = rls_ neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: neuper@37906: | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac = neuper@41983: (case stac of neuper@41983: (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) => neuper@41983: if op_ = op__ neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@41983: | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) => neuper@41983: if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_) neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) => neuper@41983: if contains_rule (Calc (snd (assoc1 (!calclist', op_)))) (assoc_rls rls_) neuper@41983: then neuper@41983: if f = f_ then Ass (m,f') else AssWeak (m,f') neuper@41983: else NotAss neuper@37906: | _ => NotAss) neuper@37906: neuper@37906: | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_))) neuper@37906: (Const ("Script.Check'_elementwise",_) $ consts' $ _) = neuper@41983: ((*tracing("### assod Check'_elementwise: consts= "^(term2str consts)^ neuper@37906: ", consts'= "^(term2str consts')); neuper@41983: atomty consts; atomty consts';*) neuper@41983: if consts = consts' neuper@41983: then ((*tracing"### assod Check'_elementwise: Ass";*) Ass (m, consts_chkd)) neuper@41983: else ((*tracing"### assod Check'_elementwise: NotAss";*) NotAss)) neuper@37906: neuper@41983: | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) = neuper@41983: Ass (m, list) neuper@37906: neuper@41983: | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) = neuper@41983: Ass (m, term) neuper@37906: neuper@41983: | assod pt _ (m as Substitute' (_, _, res)) (Const ("Script.Substitute",_) $ _ $ _) = neuper@41983: Ass (m, res) neuper@37906: neuper@41983: | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) = neuper@41983: if id = id' neuper@41983: then Ass (m, ((term_of o the o (parse thy)) f')) neuper@41983: else NotAss neuper@37906: neuper@41990: (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*) neuper@41983: | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f)) neuper@41983: (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $ neuper@41983: Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = neuper@41983: let neuper@41983: val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*); neuper@37906: val thy = maxthy (assoc_thy dI) (rootthy pt); neuper@41983: val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI'; neuper@41983: val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI'; neuper@41983: val ags = isalist2list ags'; neuper@41983: val (pI, pors, mI) = neuper@41983: if mI = ["no_met"] neuper@41983: then neuper@41983: let neuper@41983: val pors = (match_ags thy ((#ppc o get_pbt) pI) ags) neuper@41983: handle ERROR "actual args do not match formal args" neuper@41983: => (match_ags_msg pI stac ags(*raise exn*);[]); neuper@41983: val pI' = refine_ori' pors pI; neuper@41983: in (pI', pors (*refinement over models with diff.prec only*), neuper@41983: (hd o #met o get_pbt) pI') neuper@41983: end neuper@41983: else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags) neuper@41983: handle ERROR "actual args do not match formal args" neuper@41983: => (match_ags_msg pI stac ags(*raise exn*);[]), mI); neuper@37906: val (fmz_, vals) = oris2fmz_vals pors; neuper@41983: val {cas, ppc, thy,...} = get_pbt pI neuper@41983: val dI = theory2theory' thy (*take dI from _refined_ pbl*) neuper@41983: val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt)) neuper@41992: val ctxt = dI |> Thy_Info.get_theory |> ProofContext.init_global neuper@41992: |> declare_constraints' vals neuper@41983: val hdl = neuper@41983: case cas of neuper@41983: NONE => pblterm dI pI neuper@41983: | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t neuper@37906: val f = subpbl (strip_thy dI) pI neuper@41983: in neuper@41983: if domID = dI andalso pblID = pI neuper@41990: then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f) neuper@41983: else NotAss neuper@41983: end neuper@37906: neuper@37906: | assod pt d m t = neuper@41983: (if (!trace_script) neuper@41983: then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^ neuper@41983: "@@@ tac_ = "^(tac_2str m)) neuper@41983: else (); neuper@41983: NotAss); neuper@37906: neuper@37906: fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI neuper@37906: | tac_2tac (Model_Problem' (pI,_,_)) = Model_Problem neuper@37906: | tac_2tac (Add_Given' (t,_)) = Add_Given t neuper@37906: | tac_2tac (Add_Find' (t,_)) = Add_Find t neuper@37906: | tac_2tac (Add_Relation' (t,_)) = Add_Relation t neuper@37906: neuper@37906: | tac_2tac (Specify_Theory' dI) = Specify_Theory dI neuper@37906: | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI neuper@37906: | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI neuper@37906: neuper@37906: | tac_2tac (Rewrite' (thy,rod,erls,put,(thmID,thm),f,(f',asm))) = neuper@37906: Rewrite (thmID,thm) neuper@37906: neuper@37906: | tac_2tac (Rewrite_Inst' (thy,rod,erls,put,sub,(thmID,thm),f,(f',asm)))= neuper@37906: Rewrite_Inst (subst2subs sub,(thmID,thm)) neuper@37906: neuper@37906: | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = neuper@37906: Rewrite_Set (id_rls rls) neuper@37906: neuper@37906: | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = neuper@37906: Detail_Set (id_rls rls) neuper@37906: neuper@37906: | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = neuper@37906: Rewrite_Set_Inst (subst2subs sub,id_rls rls) neuper@37906: neuper@37906: | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) = neuper@37906: Detail_Set_Inst (subst2subs sub,id_rls rls) neuper@37906: neuper@37906: | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_) neuper@37906: neuper@37906: | tac_2tac (Check_elementwise' (consts,pred,consts')) = neuper@37906: Check_elementwise pred neuper@37906: neuper@37906: | tac_2tac (Or_to_List' _) = Or_to_List neuper@37906: | tac_2tac (Take' term) = Take (term2str term) neuper@37906: | tac_2tac (Substitute' (subte, t, res)) = Substitute (subte2sube subte) neuper@37906: neuper@37906: | tac_2tac (Tac_ (_,f,id,f')) = Tac id neuper@37906: neuper@41983: | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = neuper@37906: Subproblem (domID, pblID) neuper@37906: | tac_2tac (Check_Postcond' (pblID, _)) = neuper@37906: Check_Postcond pblID neuper@37906: | tac_2tac Empty_Tac_ = Empty_Tac neuper@37906: neuper@37906: | tac_2tac m = neuper@38031: error ("tac_2tac: not impl. for "^(tac_2str m)); neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (** decompose tac_ to a rule and to (lhs,rhs) neuper@41956: unly needed --- **) neuper@37906: neuper@37906: val idT = Type ("Script.ID",[]); neuper@37906: (*val tt = (term_of o the o (parse thy)) "square_equation_left::ID"; neuper@37906: type_of tt = idT; neuper@37906: val it = true : bool neuper@37906: *) neuper@37938: neuper@37906: fun make_rule thy t = neuper@37938: let val ct = cterm_of thy (Trueprop $ t) neuper@38053: in Thm (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) neuper@38053: (term_of ct), make_thm ct) end; neuper@37906: neuper@37906: (* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m; neuper@37906: *) neuper@37906: (*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete! neuper@37906: NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!! neuper@37906: WN0508 only use in tac_2res, which uses only last return-value*) neuper@37906: fun rep_tac_ (Rewrite_Inst' neuper@37906: (thy',rod,rls,put,subs,(thmID,thm),f,(f',asm))) = neuper@37906: let val fT = type_of f; neuper@37906: val b = if put then HOLogic.true_const else HOLogic.false_const; neuper@37906: val sT = (type_of o fst o hd) subs; neuper@37906: val subs' = list2isalist (HOLogic.mk_prodT (sT, sT)) neuper@37906: (map HOLogic.mk_prod subs); neuper@37906: val sT' = type_of subs'; neuper@37906: val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT) neuper@37906: $ subs' $ Free (thmID,idT) $ b $ f; neuper@37906: in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end neuper@37906: (*Fehlersuche 25.4.01 neuper@37906: (a)----- als String zusammensetzen: neuper@38053: ML> term2str f; neuper@37906: val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string neuper@38053: ML> term2str f'; neuper@37906: val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string neuper@37906: ML> subs; neuper@37906: val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst neuper@37906: > val tt = (term_of o the o (parse thy)) neuper@37906: "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))"; neuper@37906: > atomty tt; neuper@38053: ML> tracing (term2str tt); neuper@37906: (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) = neuper@37906: #0 + d_d x (x ^^^ #2 + #3 * x) neuper@37906: neuper@37906: (b)----- laut rep_tac_: neuper@37906: > val ttt=HOLogic.mk_eq (lhs,f'); neuper@37906: > atomty ttt; neuper@37906: neuper@37906: neuper@37906: (*Fehlersuche 1-2Monate vor 4.01:*) neuper@37906: > val tt = (term_of o the o (parse thy)) neuper@37906: "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)"; neuper@37906: > atomty tt; neuper@37906: neuper@37906: > val f = (term_of o the o (parse thy)) "x=#1+#2"; neuper@37906: > val f' = (term_of o the o (parse thy)) "x=#3"; neuper@37906: > val subs = [((term_of o the o (parse thy)) "bdv", neuper@37906: (term_of o the o (parse thy)) "x")]; neuper@37906: > val sT = (type_of o fst o hd) subs; neuper@37906: > val subs' = list2isalist (HOLogic.mk_prodT (sT, sT)) neuper@37906: (map HOLogic.mk_prod subs); neuper@37906: > val sT' = type_of subs'; neuper@37906: > val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT) neuper@37906: $ subs' $ Free (thmID,idT) $ HOLogic.true_const $ f; neuper@37906: > lhs = tt; neuper@37906: val it = true : bool neuper@37906: > rep_tac_ (Rewrite_Inst' neuper@38058: ("Script","tless_true","eval_rls",false,subs, neuper@37906: ("square_equation_left",""),f,(f',[]))); neuper@37906: *) neuper@37906: | rep_tac_ (Rewrite' (thy',rod,rls,put,(thmID,thm),f,(f',asm)))= neuper@37906: let neuper@37906: val fT = type_of f; neuper@37906: val b = if put then HOLogic.true_const else HOLogic.false_const; neuper@37906: val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT) neuper@37906: $ Free (thmID,idT) $ b $ f; neuper@37906: in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end neuper@37906: (* neuper@37906: > val tt = (term_of o the o (parse thy)) (*____ ____..test*) neuper@37906: "Rewrite square_equation_left True (x=#1+#2) = (x=#3)"; neuper@37906: neuper@37906: > val f = (term_of o the o (parse thy)) "x=#1+#2"; neuper@37906: > val f' = (term_of o the o (parse thy)) "x=#3"; neuper@37906: > val Thm (id,thm) = neuper@37906: rep_tac_ (Rewrite' neuper@38058: ("Script","tless_true","eval_rls",false, neuper@37906: ("square_equation_left",""),f,(f',[]))); neuper@37926: > val SOME ct = parse thy neuper@37906: "Rewrite square_equation_left True (x=#1+#2)"; neuper@37906: > rewrite_ Script.thy tless_true eval_rls true thm ct; neuper@37926: val it = SOME ("x = #3",[]) : (cterm * cterm list) option neuper@37906: *) neuper@37906: | rep_tac_ (Rewrite_Set_Inst' neuper@37906: (thy',put,subs,rls,f,(f',asm))) = neuper@37906: (e_rule, (e_term, f')) neuper@37906: (*WN050824: type error ... neuper@37906: let val fT = type_of f; neuper@37906: val sT = (type_of o fst o hd) subs; neuper@37906: val subs' = list2isalist (HOLogic.mk_prodT (sT, sT)) neuper@37906: (map HOLogic.mk_prod subs); neuper@37906: val sT' = type_of subs'; neuper@37906: val b = if put then HOLogic.true_const else HOLogic.false_const neuper@37906: val lhs = Const ("Script.Rewrite'_Set'_Inst", neuper@37906: [sT',idT,fT,fT] ---> fT) neuper@37906: $ subs' $ Free (id_rls rls,idT) $ b $ f; neuper@37906: in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*) neuper@37906: (* ... vals from Rewrite_Inst' ... neuper@37906: > rep_tac_ (Rewrite_Set_Inst' neuper@38058: ("Script",false,subs, neuper@37906: "isolate_bdv",f,(f',[]))); neuper@37906: *) neuper@37906: (* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m; neuper@37906: *) neuper@37906: | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))= neuper@37906: let val fT = type_of f; neuper@37906: val b = if put then HOLogic.true_const else HOLogic.false_const; neuper@37906: val lhs = Const ("Script.Rewrite'_Set",[idT,bool,fT] ---> fT) neuper@37906: $ Free (id_rls rls,idT) $ b $ f; neuper@37906: in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end neuper@37906: (* 13.3.01: neuper@37906: val thy = assoc_thy thy'; neuper@37906: val t = HOLogic.mk_eq (lhs,f'); neuper@37906: make_rule thy t; neuper@37906: -------------------------------------------------- neuper@37906: val lll = (term_of o the o (parse thy)) neuper@37906: "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)"; neuper@37906: neuper@37906: -------------------------------------------------- neuper@37906: > val f = (term_of o the o (parse thy)) "x=#1+#2"; neuper@37906: > val f' = (term_of o the o (parse thy)) "x=#3"; neuper@37906: > val Thm (id,thm) = neuper@37906: rep_tac_ (Rewrite_Set' neuper@38058: ("Script",false,"SqRoot_simplify",f,(f',[]))); neuper@37906: val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string neuper@37906: val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm neuper@37906: *) neuper@37906: | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))= neuper@37906: let val fT = type_of f; neuper@37906: val lhs = Const ("Script.Calculate",[idT,fT] ---> fT) neuper@37906: $ Free (op_,idT) $ f neuper@37906: in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end neuper@37906: (* neuper@37906: > val lhs'=(term_of o the o (parse thy))"Calculate plus (#1+#2)"; neuper@37906: ... test-root-equ.sml: calculate ... neuper@37922: > val Appl m'=applicable_in p pt (Calculate "PLUS"); neuper@37906: > val (lhs,_)=tac_2etac m'; neuper@37906: > lhs'=lhs; neuper@37906: val it = true : bool*) neuper@37906: | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t')) neuper@41983: | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t')) neuper@37906: | rep_tac_ (Take' (t')) = (Erule, (e_term, t')) neuper@37906: | rep_tac_ (Substitute' (subst,t,t')) = (Erule, (t, t')) neuper@37906: | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t')) neuper@38031: | rep_tac_ m = error ("rep_tac_: not impl.for "^ neuper@37906: (tac_2str m)); neuper@37906: neuper@37906: (*"N.3.6.03------ neuper@37906: fun tac_2rule m = (fst o rep_tac_) m; neuper@37906: fun tac_2etac m = (snd o rep_tac_) m; neuper@37906: fun tac_2tac m = (fst o snd o rep_tac_) m;*) neuper@37906: fun tac_2res m = (snd o snd o rep_tac_) m;(*ONLYuse of rep_tac_ neuper@37906: FIXXXXME: simplify rep_tac_*) neuper@37906: neuper@37906: neuper@41996: (* handle a leaf at the end of recursive descent: neuper@37906: a leaf is either a tactic or an 'exp' in 'let v = expr' neuper@37906: where 'exp' does not contain a tactic. neuper@37906: handling a leaf comprises neuper@37906: (1) 'subst_stacexpr' substitute env and complete curried tactic neuper@37906: (2) rewrite the leaf by 'srls' neuper@41996: *) neuper@37906: fun handle_leaf call thy srls E a v t = neuper@41996: (*WN050916 'upd_env_opt' is a blind copy from previous version*) neuper@41996: case subst_stacexpr E a v t of neuper@41996: (a', STac stac) => (*script-tactic*) neuper@41996: let val stac' = neuper@41996: eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac) neuper@41996: in neuper@41996: (if (!trace_script) neuper@41996: then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'") neuper@41996: else (); neuper@41996: (a', STac stac')) neuper@41996: end neuper@41996: | (a', Expr lexpr) => (*leaf-expression*) neuper@41996: let val lexpr' = neuper@41996: eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr) neuper@41996: in neuper@41996: (if (!trace_script) neuper@41996: then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'") neuper@41996: else (); neuper@41996: (a', Expr lexpr')) neuper@41996: end; neuper@37906: neuper@37906: neuper@37906: (** locate an applicable stactic in a script **) neuper@37906: neuper@37906: datatype assoc = (*ExprVal in the sense of denotational semantics*) neuper@37906: Assoc of (*the stac is associated, strongly or weakly*) neuper@37906: scrstate * (*the current; returned for next_tac etc. outside ass* *) neuper@37906: (step list) (*list of steps done until associated stac found; neuper@37906: initiated with the data for doing the 1st step, neuper@37906: thus the head holds these data further on, neuper@37906: while the tail holds steps finished (incl.scrstate in ptree)*) neuper@37906: | NasApp of (*stac not associated, but applicable, ptree-node generated*) neuper@37906: scrstate * (step list) neuper@37906: | NasNap of (*stac not associated, not applicable, nothing generated; neuper@37906: for distinction in Or, for leaving iterations, leaving Seq, neuper@37906: evaluate scriptexpressions*) neuper@37906: term * env; neuper@37906: fun assoc2str (Assoc _) = "Assoc" neuper@37906: | assoc2str (NasNap _) = "NasNap" neuper@37906: | assoc2str (NasApp _) = "NasApp"; neuper@37906: neuper@37906: neuper@37906: datatype asap = (*arg. of assy _only_ for distinction w.r.t. Or*) neuper@37906: Aundef (*undefined: set only by (topmost) Or*) neuper@37906: | AssOnly (*do not execute appl stacs - there could be an associated neuper@37906: in parallel Or-branch*) neuper@37906: | AssGen; (*no Ass(Weak) found within Or, thus neuper@37906: search for _applicable_ stacs, execute and generate pt*) neuper@37906: (*this constructions doesnt allow arbitrary nesting of Or !!!*) neuper@37906: neuper@37906: neuper@37906: (*assy, ass_up, astep_up scanning for locate_gen at stactic in a script. neuper@37906: search is clearly separated into (1)-(2): neuper@37906: (1) assy is recursive descent; neuper@37906: (2) ass_up resumes interpretation at a location somewhere in the script; neuper@37906: astep_up does only get to the parentnode of the scriptexpr. neuper@37906: consequence: neuper@37906: * call of (2) means _always_ that in this branch below neuper@41996: there was an appl.stac (Repeat, Or e1, ...) found by the previous step. neuper@37906: *) neuper@41996: fun assy ya (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) = neuper@41996: (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of neuper@41996: NasApp ((E',l,a,v,S,bb),ss) => neuper@41996: let neuper@41996: val id' = mk_Free (id, T); neuper@41996: val E' = upd_env E' (id', v); neuper@41996: in assy ya ((E', l@[R,D], a,v,S,b),ss) body end neuper@41996: | NasNap (v,E) => neuper@41996: let neuper@41996: val id' = mk_Free (id, T); neuper@41996: val E' = upd_env E (id', v); neuper@41996: in assy ya ((E', l@[R,D], a,v,S,b),ss) body end neuper@41996: | ay => ay) neuper@37906: neuper@41996: | assy (ya as (((thy,srls),_),_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) = neuper@41996: (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c) neuper@41996: then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e neuper@41996: else NasNap (v, E)) neuper@41996: | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) = neuper@41996: (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c) neuper@41996: then assy ya ((E, l@[R], a,v,S,b),ss) e neuper@41996: else NasNap (v, E)) neuper@37906: neuper@41996: | assy (ya as (((thy,srls),_),_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) = neuper@41996: (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c) neuper@41996: then assy ya ((E, l@[L,R], a,v,S,b),ss) e1 neuper@41996: else assy ya ((E, l@[ R], a,v,S,b),ss) e2) neuper@37906: neuper@37906: | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) = neuper@41996: (case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of neuper@41996: ay => ay) neuper@41996: | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) = neuper@41996: (case assy ya ((E, l@[R], a,v,S,b),ss) e of neuper@41996: ay => ay) neuper@37906: neuper@37906: | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) = neuper@41996: (case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of neuper@41996: NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2 neuper@41996: | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2 neuper@37906: | ay => ay) neuper@37906: | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) = neuper@41996: (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of neuper@41996: NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2 neuper@41996: | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[R], a,v,S,b),ss) e2 neuper@37906: | ay => ay) neuper@37906: neuper@37906: | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) = neuper@41996: assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e neuper@41996: | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) = neuper@41996: assy ya ((E,(l@[R]),a,v,S,b),ss) e neuper@37906: neuper@37906: | assy (y, Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) = neuper@41996: (case assy (y, AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of neuper@37906: NasNap (v, E) => neuper@41996: (case assy (y, AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of neuper@41996: NasNap (v, E) => neuper@41996: (case assy (y, AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of neuper@41996: NasNap (v, E) => neuper@41996: assy (y, AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2 neuper@41996: | ay => ay) neuper@41996: | ay =>(ay)) neuper@38031: | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///") neuper@37906: | ay => (ay)) neuper@37906: | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) = neuper@41996: (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of neuper@41996: NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2 neuper@37906: | ay => (ay)) neuper@37906: neuper@37906: | assy (((thy',sr),d),ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t = neuper@41996: (case handle_leaf "locate" thy' sr E a v t of neuper@41996: (a', Expr s) => neuper@41996: (NasNap (eval_listexpr_ (assoc_thy thy') sr neuper@41996: (subst_atomic (upd_env_opt E (a',v)) t), E)) neuper@41996: | (a', STac stac) => neuper@41996: let neuper@41996: val ctxt = get_ctxt pt (p,p_) neuper@41996: val p' = neuper@41996: case p_ of Frm => p neuper@41996: | Res => lev_on p neuper@41996: | _ => error ("assy: call by " ^ pos'2str (p,p_)); neuper@41996: in neuper@41996: case assod pt d m stac of neuper@41996: Ass (m,v') => neuper@41996: let val (p'',c',f',pt') = neuper@41996: generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt; neuper@41996: in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end neuper@41996: | AssWeak (m,v') => neuper@41996: let val (p'',c',f',pt') = neuper@41996: generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt; neuper@41996: in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end neuper@41996: | NotAss => neuper@41996: (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*) neuper@41996: AssOnly => (NasNap (v, E)) neuper@41996: | gen => neuper@41996: (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of neuper@41996: Appl m' => neuper@41996: let neuper@41996: val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*)) neuper@41996: val (p'',c',f',pt') = neuper@41996: generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt; neuper@41996: in NasApp (is,(m,f',pt',p'',c @ c')::ss) end neuper@41996: | Notappl _ => (NasNap (v, E)) neuper@41996: ) neuper@41996: ) neuper@41996: end); neuper@37906: neuper@37906: fun ass_up (ys as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) neuper@41968: (Const ("HOL.Let",_) $ _) = neuper@38015: let (*val _= tracing("### ass_up1 Let$e: is=") neuper@38015: val _= tracing(istate2str (ScrState is))*) neuper@37906: val l = drop_last l; (*comes from e, goes to Abs*) neuper@41968: val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc; neuper@37906: val i = mk_Free (i, T); neuper@37906: val E = upd_env E (i, v); neuper@38015: (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*) neuper@37906: in case assy (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body of neuper@37906: Assoc iss => Assoc iss neuper@37906: | NasApp iss => astep_up ys iss neuper@37906: | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end neuper@37906: neuper@37906: | ass_up ys (iss as (is,_)) (Abs (_,_,_)) = neuper@38015: ((*tracing("### ass_up Abs: is="); neuper@38015: tracing(istate2str (ScrState is));*) neuper@37906: astep_up ys iss) (*TODO 5.9.00: env ?*) neuper@37906: neuper@41968: | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))= neuper@38015: ((*tracing("### ass_up Let $ e $ Abs: is="); neuper@38015: tracing(istate2str (ScrState is));*) neuper@37906: astep_up ys iss) (*TODO 5.9.00: env ?*) neuper@37906: neuper@37906: (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) = neuper@37906: (ys, ((E,up,a,v,S,b),ss), (go up sc)); neuper@37906: *) neuper@37906: | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) = neuper@37906: astep_up ysa iss (*all has been done in (*2*) below*) neuper@37906: neuper@37906: | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) = neuper@37906: (* val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _)) = neuper@37906: (ys, ((E,up,a,v,S,b),ss), (go up sc)); neuper@37906: *) neuper@37906: astep_up ysa iss (*2*: comes from e2*) neuper@37906: neuper@37906: | ass_up (ysa as (y,s,Script sc,d)) (is as (E,l,a,v,S,b),ss) neuper@37906: (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*) neuper@37906: (* val ((ysa as (y,s,Script sc,d)), (is as (E,l,a,v,S,b),ss), neuper@37906: (Const ("Script.Seq",_) $ _ )) = neuper@37906: (ys, ((E,up,a,v,S,b),ss), (go up sc)); neuper@37906: *) neuper@37906: let val up = drop_last l; neuper@37906: val Const ("Script.Seq",_) $ _ $ e2 = go up sc neuper@38015: (*val _= tracing("### ass_up Seq$e: is=") neuper@38015: val _= tracing(istate2str (ScrState is))*) neuper@37906: in case assy (((y,s),d),Aundef) ((E, up@[R], a,v,S,b),ss) e2 of neuper@37906: NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss) neuper@37906: | NasApp iss => astep_up ysa iss neuper@37906: | ay => ay end neuper@37906: neuper@37906: (* val (ysa, iss, (Const ("Script.Try",_) $ e $ _)) = neuper@37906: (ys, ((E,up,a,v,S,b),ss), (go up sc)); neuper@37906: *) neuper@37906: | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) = neuper@37906: astep_up ysa iss neuper@37906: neuper@37906: (* val (ysa, iss, (Const ("Script.Try",_) $ e)) = neuper@37906: (ys, ((E,up,a,v,S,b),ss), (go up sc)); neuper@37906: *) neuper@37906: | ass_up ysa iss (Const ("Script.Try",_) $ e) = neuper@38015: ((*tracing("### ass_up Try $ e");*) neuper@37906: astep_up ysa iss) neuper@37906: neuper@37906: | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss) neuper@37906: (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*) neuper@37906: (t as Const ("Script.While",_) $ c $ e $ a) = neuper@38015: ((*tracing("### ass_up: While c= "^ neuper@37906: (term2str (subst_atomic (upd_env E (a,v)) c)));*) neuper@37906: if eval_true_ y s (subst_atomic (upd_env E (a,v)) c) neuper@37926: then (case assy (((y,s),d),Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of neuper@37926: NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss) neuper@37906: | NasApp ((E',l,a,v,S,b),ss) => neuper@37906: ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*) neuper@37906: | ay => ay) neuper@37926: else astep_up ys ((E,l, SOME a,v,S,b),ss) neuper@37906: ) neuper@37906: neuper@37906: | ass_up (ys as (y,s,_,d)) ((E,l,a,v,S,b),ss) neuper@37906: (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*) neuper@37906: (t as Const ("Script.While",_) $ c $ e) = neuper@37906: if eval_true_ y s (subst_atomic (upd_env_opt E (a,v)) c) neuper@37906: then (case assy (((y,s),d),Aundef) ((E, l@[R], a,v,S,b),ss) e of neuper@37906: NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss) neuper@37906: | NasApp ((E',l,a,v,S,b),ss) => neuper@37906: ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*) neuper@37906: | ay => ay) neuper@37906: else astep_up ys ((E,l, a,v,S,b),ss) neuper@37906: neuper@37906: | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss neuper@37906: neuper@37906: | ass_up (ys as (y,s,_,d)) ((E,l,_,v,S,b),ss) neuper@37906: (t as Const ("Script.Repeat",_) $ e $ a) = neuper@37926: (case assy (((y,s),d), Aundef) ((E, (l@[L,R]), SOME a,v,S,b),ss) e of neuper@37926: NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss) neuper@37906: | NasApp ((E',l,a,v,S,b),ss) => neuper@37906: ass_up ys ((E',l,a,v,S,b),ss) t neuper@37906: | ay => ay) neuper@37906: neuper@37906: | ass_up (ys as (y,s,_,d)) (is as ((E,l,a,v,S,b),ss)) neuper@37906: (t as Const ("Script.Repeat",_) $ e) = neuper@37906: (case assy (((y,s),d), Aundef) ((E, (l@[R]), a,v,S,b),ss) e of neuper@37906: NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss) neuper@37906: | NasApp ((E',l,a,v',S,bb),ss) => neuper@37906: ass_up ys ((E',l,a,v',S,b),ss) t neuper@37906: | ay => ay) neuper@37906: neuper@37906: | ass_up y iss (Const ("Script.Or",_) $ _ $ _ $ _) = astep_up y iss neuper@37906: neuper@37906: | ass_up y iss (Const ("Script.Or",_) $ _ $ _) = astep_up y iss neuper@37906: neuper@37906: | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) = neuper@37906: astep_up y ((E, (drop_last l), a,v,S,b),ss) neuper@37906: neuper@37906: | ass_up y iss t = neuper@38031: error ("ass_up not impl for t= "^(term2str t)) neuper@37906: (* 9.6.03 neuper@37906: val (ys as (_,_,Script sc,_), ss) = neuper@37906: ((thy',srls,scr,d), [(m,EmptyMout,pt,p,[])]:step list); neuper@37906: astep_up ys ((E,l,a,v,S,b),ss); neuper@37906: val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) = neuper@37906: (ysa, iss); neuper@37906: val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) = neuper@37906: ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])])); neuper@37906: *) neuper@37906: and astep_up (ys as (_,_,Script sc,_)) ((E,l,a,v,S,b),ss) = neuper@37906: if 1 < length l neuper@37906: then neuper@37906: let val up = drop_last l; neuper@38015: (*val _= tracing("### astep_up: E= "^env2str E);*) neuper@37906: in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end neuper@37906: else (NasNap (v, E)) neuper@37906: ; neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* use"ME/script.sml"; neuper@37906: use"script.sml"; neuper@37906: term2str (go up sc); neuper@37906: neuper@37906: *) neuper@37906: neuper@37906: (*check if there are tacs for rewriting only*) neuper@37906: fun rew_only ([]:step list) = true neuper@37906: | rew_only (((Rewrite' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((Rewrite_Inst' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((Rewrite_Set' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((Calculate' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only (((End_Trans' _ ,_,_,_,_))::ss) = rew_only ss neuper@37906: | rew_only _ = false; neuper@37906: neuper@37906: neuper@37906: datatype locate = neuper@37906: Steps of istate (*producing hd of step list (which was latest) neuper@37906: for next_tac, for reporting Safe|Unsafe to DG*) neuper@37906: * step (*(scrstate producing this step is in ptree !)*) neuper@37906: list (*locate_gen may produce intermediate steps*) neuper@37906: | NotLocatable; (*no (m Ass m') or (m AssWeak m') found*) neuper@37906: neuper@37906: neuper@37906: neuper@37906: (* locate_gen tries to locate an input tac m in the script. neuper@37906: pursuing this goal the script is executed until an (m' equiv m) is found, neuper@37906: or the end of the script neuper@37906: args neuper@37906: m : input by the user, already checked by applicable_in, neuper@37906: (to be searched within Or; and _not_ an m doing the step on ptree !) neuper@37906: p,pt: (incl ets) at the time of input neuper@37906: scr : the script neuper@37906: d : canonical simplifier for locating Take, Substitute, Subproblems etc. neuper@37906: ets : ets at the time of input neuper@37906: l : the location (in scr) of the stac which generated the current formula neuper@37906: returns neuper@37906: Steps: pt,p (incl. ets) with m done neuper@37906: pos' list of proofobjs cut (from generate) neuper@37906: safe: implied from last proofobj neuper@37906: ets: neuper@37906: ///ToDo : ets contains a list of tacs to be done before m can be done neuper@37906: NOT IMPL. -- "error: do other step before" neuper@37906: NotLocatable: thus generate_hard neuper@37906: *) neuper@37906: (* val (Rewrite'(_,ro,er,pa,(id,str),f,_), p, Rfuns {locate_rule=lo,...}, neuper@37906: RrlsState (_,f'',rss,rts)) = (m, (p,p_), sc, is); neuper@37906: *) neuper@37906: fun locate_gen (thy',_) (Rewrite'(_,ro,er,pa,(id,str),f,_)) (pt,p) bonzai@41948: (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) = neuper@37906: (case lo rss f (Thm (id, mk_thm (assoc_thy thy') str)) of neuper@37906: [] => NotLocatable neuper@37906: | rts' => neuper@37906: Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts')) neuper@37906: neuper@37906: | locate_gen (ts as (thy',srls)) (m:tac_) ((pt,p):ptree * pos') bonzai@41948: (scr as Script (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) = neuper@38015: let (*val _= tracing("### locate_gen-----------------: is="); neuper@38015: val _= tracing( istate2str (ScrState (E,l,a,v,S,b))); neuper@38015: val _= tracing("### locate_gen: l= "^loc_2str l^", p= "^pos'2str p)*) neuper@37906: val thy = assoc_thy thy'; neuper@37906: in case if l=[] orelse ((*init.in solve..Apply_Method...*) neuper@37906: (last_elem o fst) p = 0 andalso snd p = Res) neuper@37906: then (assy ((ts,d),Aundef) ((E,[R],a,v,S,b), neuper@37906: [(m,EmptyMout,pt,p,[])]) body) neuper@37906: (* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) = neuper@37906: (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b),[(m,EmptyMout,pt,p,[])])); neuper@37906: (assy ((ts,d),Aundef) ((E,[R],a,v,S,b),[(m,EmptyMout,pt,p,[])]) body); neuper@37906: *) neuper@37906: else (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), neuper@37906: [(m,EmptyMout,pt,p,[])]) ) of neuper@37906: Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) => neuper@37906: (* val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) = neuper@37906: (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), neuper@37906: [(m,EmptyMout,pt,p,[])]) ); neuper@37906: *) neuper@38015: ((*tracing("### locate_gen Assoc: p'="^(pos'2str p'));*) neuper@37906: if bb then Steps (ScrState is, ss) neuper@37906: else if rew_only ss (*andalso 'not bb'= associated weakly*) neuper@37906: then let val (po,p_) = p neuper@37906: val po' = case p_ of Frm => po | Res => lev_on po neuper@37906: (*WN.12.03: noticed, that pos is also updated in assy !?! neuper@37906: instead take p' from Assoc ?????????????????????????????*) neuper@37906: val (p'',c'',f'',pt'') = bonzai@41951: generate1 thy m (ScrState is, ctxt) (po',p_) pt; neuper@38015: (*val _=tracing("### locate_gen, aft g1: p''="^(pos'2str p''));*) neuper@37906: (*drop the intermediate steps !*) neuper@37906: in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end neuper@37906: else Steps (ScrState is, ss)) neuper@37906: neuper@37906: | NasApp _ (*[((E,l,a,v,S,bb),(m',f',pt',p',c'))] => neuper@38031: error ("locate_gen: should not have got NasApp, ets =")*) neuper@37906: => NotLocatable neuper@37906: | NasNap (_,_) => neuper@37906: if l=[] then NotLocatable neuper@37906: else (*scan from begin of script for rew_only*) neuper@37906: (case assy ((ts,d),Aundef) ((E,[R],a,v,Unsafe,b), neuper@37906: [(m,EmptyMout,pt,p,[])]) body of neuper@37906: Assoc (iss as (is as (_,_,_,_,_,bb), neuper@37906: ss as ((m',f',pt',p',c')::_))) => neuper@38015: ((*tracing"4### locate_gen Assoc after Fini";*) neuper@37906: if rew_only ss neuper@37906: then let val(p'',c'',f'',pt'') = bonzai@41951: generate1 thy m (ScrState is, ctxt) p' pt; neuper@37906: (*drop the intermediate steps !*) neuper@37906: in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end neuper@37906: else NotLocatable) neuper@38015: | _ => ((*tracing ("#### locate_gen: after Fini");*) neuper@37906: NotLocatable)) neuper@37906: end bonzai@41951: | locate_gen _ m _ (sc,_) (is, _) = neuper@38031: error ("locate_gen: wrong arguments,\n tac= "^(tac_2str m)^ neuper@37906: ",\n scr= "^(scr2str sc)^",\n istate= "^(istate2str is)); neuper@37906: neuper@37906: neuper@37906: neuper@37906: (** find the next stactic in a script **) neuper@37906: neuper@37906: datatype appy = (*ExprVal in the sense of denotational semantics*) neuper@37906: Appy of (*applicable stac found, search stalled*) neuper@37906: tac_ * (*tac_ associated (fun assod) with stac*) neuper@37906: scrstate (*after determination of stac WN.18.8.03*) neuper@37906: | Napp of (*stac found was not applicable; neuper@37906: this mode may become Skip in Repeat, Try and Or*) neuper@37906: env (*stack*) (*popped while nxt_up*) neuper@37906: | Skip of (*for restart after Appy, for leaving iterations, neuper@37906: for passing the value of scriptexpressions, neuper@37906: and for finishing the script successfully*) neuper@37906: term * env (*stack*); neuper@37906: neuper@37906: (*appy, nxt_up, nstep_up scanning for next_tac. neuper@37906: search is clearly separated into (1)-(2): neuper@37906: (1) appy is recursive descent; neuper@37906: (2) nxt_up resumes interpretation at a location somewhere in the script; neuper@37906: nstep_up does only get to the parentnode of the scriptexpr. neuper@37906: consequence: neuper@37906: * call of (2) means _always_ that in this branch below neuper@37906: there was an applicable stac (Repeat, Or e1, ...) neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: datatype appy_ = (*as argument in nxt_up, nstep_up, from appy*) neuper@37906: (* Appy is only (final) returnvalue, not argument during search neuper@37906: |*) Napp_ (*ev. detects 'script is not appropriate for this example'*) neuper@37906: | Skip_; (*detects 'script successfully finished' neuper@37906: also used as init-value for resuming; this works, neuper@37906: because 'nxt_up Or e1' treats as Appy*) neuper@37906: neuper@37906: fun appy thy ptp E l neuper@41968: (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v = neuper@41968: (* val (thy, ptp, E, l, t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b)),a, v)= neuper@37906: (thy, ptp, E, up@[R,D], body, a, v); neuper@37906: appy thy ptp E l t a v; neuper@37906: *) neuper@38015: ((*tracing("### appy Let$e$Abs: is="); neuper@38015: tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*) neuper@37906: case appy thy ptp E (l@[L,R]) e a v of neuper@37906: Skip (res, E) => neuper@38015: let (*val _= tracing("### appy Let "^(term2str t)); neuper@38015: val _= tracing("### appy Let: Skip res ="^(term2str res));*) neuper@37906: (*val (i',b') = variant_abs (i,T,b); WN.15.5.03 neuper@37906: val i = mk_Free(i',T); WN.15.5.03 *) neuper@37906: val E' = upd_env E (Free (i,T), res); neuper@37906: in appy thy ptp E' (l@[R,D]) b a v end neuper@37906: | ay => ay) neuper@37906: neuper@37906: | appy (thy as (th,sr)) ptp E l neuper@37906: (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v = (*ohne n. 28.9.00*) neuper@38015: ((*tracing("### appy While $ c $ e $ a, upd_env= "^ neuper@37906: (subst2str (upd_env E (a,v))));*) neuper@37906: if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c) neuper@37926: then appy thy ptp E (l@[L,R]) e (SOME a) v neuper@37906: else Skip (v, E)) neuper@37906: neuper@37906: | appy (thy as (th,sr)) ptp E l neuper@37906: (t as Const ("Script.While"(*2*),_) $ c $ e) a v =(*ohne nachdenken 28.9.00*) neuper@38015: ((*tracing("### appy While $ c $ e, upd_env= "^ neuper@37906: (subst2str (upd_env_opt E (a,v))));*) neuper@37906: if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c) neuper@37906: then appy thy ptp E (l@[R]) e a v neuper@37906: else Skip (v, E)) neuper@37906: neuper@37906: | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v = neuper@38015: ((*tracing("### appy If: t= "^(term2str t)); neuper@38015: tracing("### appy If: c= "^(term2str(subst_atomic(upd_env_opt E(a,v))c))); neuper@38015: tracing("### appy If: thy= "^(fst thy));*) neuper@37906: if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c) neuper@38015: then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v) neuper@38015: else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v)) neuper@37906: (* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e $ a), _, v) = neuper@37906: (thy, ptp, E, (l@[R]), e, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E (*env*) l neuper@37906: (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v = neuper@38015: ((*tracing("### appy Repeat a: ");*) neuper@37926: appy thy ptp E (*env*) (l@[L,R]) e (SOME a) v) neuper@37906: (* val (thy, ptp, E, l, (Const ("Script.Repeat",_) $ e), _, v) = neuper@37906: (thy, ptp, E, (l@[R]), e, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E (*env*) l neuper@37906: (Const ("Script.Repeat"(*2*),_) $ e) a v = neuper@38053: ((*tracing("3### appy Repeat: a= " ^ term2str a);*) neuper@37906: appy thy ptp E (*env*) (l@[R]) e a v) neuper@37906: (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e $ a), _, v)= neuper@37906: (thy, ptp, E, (l@[R]), e2, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E l neuper@37906: (t as Const ("Script.Try",_) $ e $ a) _ v = neuper@37926: (case appy thy ptp E (l@[L,R]) e (SOME a) v of neuper@38053: Napp E => ((*tracing("### appy Try " ^ term2str t);*) neuper@37906: Skip (v, E)) neuper@37906: | ay => ay) neuper@37906: (* val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)= neuper@37906: (thy, ptp, E, (l@[R]), e2, a, v); neuper@37906: val (thy, ptp, E, l, (t as Const ("Script.Try",_) $ e), _, v)= neuper@37906: (thy, ptp, E, (l@[L,R]), e1, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E l neuper@37906: (t as Const ("Script.Try",_) $ e) a v = neuper@37906: (case appy thy ptp E (l@[R]) e a v of neuper@38053: Napp E => ((*tracing("### appy Try " ^ term2str t);*) neuper@37906: Skip (v, E)) neuper@37906: | ay => ay) neuper@37906: neuper@37906: neuper@37906: | appy thy ptp E l neuper@37906: (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v = neuper@37926: (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of neuper@37906: Appy lme => Appy lme neuper@37926: | _ => appy thy ptp E (*env*) (l@[L,R]) e2 (SOME a) v) neuper@37906: neuper@37906: | appy thy ptp E l neuper@37906: (Const ("Script.Or"(*2*),_) $e1 $ e2) a v = neuper@37906: (case appy thy ptp E (l@[L,R]) e1 a v of neuper@37906: Appy lme => Appy lme neuper@37906: | _ => appy thy ptp E (l@[R]) e2 a v) neuper@37906: neuper@37906: (* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)= neuper@37906: (thy, ptp, E,(up@[R]),e2, a, v); neuper@37906: val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2 $ a), _, v)= neuper@37906: (thy, ptp, E,(up@[R,D]),body, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E l neuper@37906: (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v = neuper@38015: ((*tracing("### appy Seq $ e1 $ e2 $ a, upd_env= "^ neuper@37906: (subst2str (upd_env E (a,v))));*) neuper@37926: case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of neuper@37926: Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v neuper@37906: | ay => ay) neuper@37906: neuper@37906: (* val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)= neuper@37906: (thy, ptp, E,(up@[R]),e2, a, v); neuper@37906: val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)= neuper@37906: (thy, ptp, E,(l@[R]), e2, a, v); neuper@37906: val (thy, ptp, E, l, (Const ("Script.Seq",_) $ e1 $ e2), _, v)= neuper@37906: (thy, ptp, E,(up@[R,D]),body, a, v); neuper@37906: *) neuper@37906: | appy thy ptp E l neuper@37906: (Const ("Script.Seq",_) $ e1 $ e2) a v = neuper@37906: (case appy thy ptp E (l@[L,R]) e1 a v of neuper@37906: Skip (v,E) => appy thy ptp E (l@[R]) e2 a v neuper@37906: | ay => ay) neuper@37906: neuper@37906: (*.a leaf has been found*) neuper@37906: | appy (thy as (th,sr)) (pt, p) E l t a v = neuper@37906: (* val (thy as (th,sr),(pt, p),E, l, t, a, v) = neuper@37906: (thy, ptp, E, up@[R,D], body, a, v); neuper@37906: val (thy as (th,sr),(pt, p),E, l, t, a, v) = neuper@37906: (thy, ptp, E, l@[L,R], e, a, v); neuper@37906: val (thy as (th,sr),(pt, p),E, l, t, a, v) = neuper@37906: (thy, ptp, E,(l@[R]), e, a, v); neuper@37906: *) neuper@37906: (case handle_leaf "next " th sr E a v t of neuper@37906: (* val (a', Expr s) = handle_leaf "next " th sr E a v t; neuper@37906: *) neuper@37906: (a', Expr s) => Skip (s, E) neuper@37906: (* val (a', STac stac) = handle_leaf "next " th sr E a v t; neuper@37906: *) neuper@37906: | (a', STac stac) => neuper@37906: let neuper@38015: (*val _= tracing("### appy t, vor stac2tac_ is="); neuper@38015: val _= tracing(istate2str (ScrState (E,l,a',v,Sundef,false)));*) neuper@37906: val (m,m') = stac2tac_ pt (assoc_thy th) stac neuper@37906: in case m of neuper@37906: Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false)) neuper@37906: | _ => (case applicable_in p pt m of neuper@37906: (* val Appl m' = applicable_in p pt m; neuper@37906: *) neuper@37906: Appl m' => neuper@38015: ((*tracing("### appy: Appy");*) neuper@37906: Appy (m', (E,l,a',tac_2res m',Sundef,false))) neuper@38015: | _ => ((*tracing("### appy: Napp");*)Napp E)) neuper@37906: end); neuper@37906: neuper@37906: neuper@41968: (* val (scr as Script sc, l, t as Const ("HOL.Let",_) $ _) = neuper@37906: (Script sc, up, go up sc); neuper@37906: nxt_up thy ptp (Script sc) E l ay t a v; neuper@37906: neuper@41968: val (thy,ptp,scr as (Script sc),E,l, ay, t as Const ("HOL.Let",_) $ _, a, v)= neuper@37906: (thy,ptp,Script sc, E,up,ay, go up sc, a, v); neuper@37906: nxt_up thy ptp scr E l ay t a v; neuper@37906: *) neuper@37906: fun nxt_up thy ptp (scr as (Script sc)) E l ay neuper@41968: (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*) neuper@38015: ((*tracing("### nxt_up1 Let$e: is="); neuper@38015: tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*) neuper@37906: if ay = Napp_ neuper@37906: then nstep_up thy ptp scr E (drop_last l) Napp_ a v neuper@37906: else (*Skip_*) neuper@37906: let val up = drop_last l; neuper@41968: val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; neuper@37906: val i = mk_Free (i, T); neuper@37906: val E = upd_env E (i, v); neuper@38015: (*val _= tracing("### nxt_up2 Let$e: is="); neuper@38015: val _= tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*) neuper@37906: in case appy thy ptp (E) (up@[R,D]) body a v of neuper@37906: Appy lre => Appy lre neuper@37906: | Napp E => nstep_up thy ptp scr E up Napp_ a v neuper@37906: | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end) neuper@37906: neuper@37906: | nxt_up thy ptp scr E l ay neuper@37906: (t as Abs (_,_,_)) a v = neuper@38053: ((*tracing("### nxt_up Abs: " ^ term2str t);*) neuper@37906: nstep_up thy ptp scr E (*enr*) l ay a v) neuper@37906: neuper@37906: | nxt_up thy ptp scr E l ay neuper@41968: (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v = neuper@38015: ((*tracing("### nxt_up Let$e$Abs: is="); neuper@38015: tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*) neuper@38053: (*tracing("### nxt_up Let e Abs: " ^ term2str t);*) neuper@37906: nstep_up thy ptp scr (*upd_env*) E (*a,v)*) neuper@37906: (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v) neuper@37906: neuper@37906: (*no appy_: never causes Napp -> Helpless*) neuper@37906: | nxt_up (thy as (th,sr)) ptp scr E l _ neuper@37906: (Const ("Script.While"(*1*),_) $ c $ e $ _) a v = neuper@37906: if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c) neuper@37906: then case appy thy ptp E (l@[L,R]) e a v of neuper@37906: Appy lr => Appy lr neuper@37906: | Napp E => nstep_up thy ptp scr E l Skip_ a v neuper@37906: | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v neuper@37906: else nstep_up thy ptp scr E l Skip_ a v neuper@37906: neuper@37906: (*no appy_: never causes Napp - Helpless*) neuper@37906: | nxt_up (thy as (th,sr)) ptp scr E l _ neuper@37906: (Const ("Script.While"(*2*),_) $ c $ e) a v = neuper@37906: if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c) neuper@37906: then case appy thy ptp E (l@[R]) e a v of neuper@37906: Appy lr => Appy lr neuper@37906: | Napp E => nstep_up thy ptp scr E l Skip_ a v neuper@37906: | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v neuper@37906: else nstep_up thy ptp scr E l Skip_ a v neuper@37906: neuper@37906: (* val (scr, l) = (Script sc, up); neuper@37906: *) neuper@37906: | nxt_up thy ptp scr E l ay (Const ("If",_) $ _ $ _ $ _) a v = neuper@37906: nstep_up thy ptp scr E l ay a v neuper@37906: neuper@37906: | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*) neuper@37906: (Const ("Script.Repeat"(*1*),T) $ e $ _) a v = neuper@37906: (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[L,R]):loc_) e a v of neuper@37906: Appy lr => Appy lr neuper@38015: | Napp E => ((*tracing("### nxt_up Repeat a: ");*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v) neuper@38015: | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^ neuper@37906: (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v)) neuper@37906: neuper@37906: | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*) neuper@37906: (Const ("Script.Repeat"(*2*),T) $ e) a v = neuper@37906: (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[R]):loc_) e a v of neuper@37906: Appy lr => Appy lr neuper@38015: | Napp E => ((*tracing("### nxt_up Repeat a: ");*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v) neuper@38015: | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^ neuper@37906: (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v)) neuper@37906: (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e $ _), a, v) = neuper@37906: (thy, ptp, (Script sc), neuper@37906: E, up, ay,(go up sc), a, v); neuper@37906: *) neuper@37906: | nxt_up thy ptp scr E l _ (*makes Napp to Skip*) neuper@37906: (t as Const ("Script.Try",_) $ e $ _) a v = neuper@38053: ((*tracing("### nxt_up Try " ^ term2str t);*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v ) neuper@37906: (* val (thy, ptp, scr, E, l, _,(t as Const ("Script.Try",_) $ e), a, v) = neuper@37906: (thy, ptp, (Script sc), neuper@37906: E, up, ay,(go up sc), a, v); neuper@37906: *) neuper@37906: | nxt_up thy ptp scr E l _ (*makes Napp to Skip*) neuper@37906: (t as Const ("Script.Try"(*2*),_) $ e) a v = neuper@38053: ((*tracing("### nxt_up Try " ^ term2str t);*) neuper@37906: nstep_up thy ptp scr E l Skip_ a v) neuper@37906: neuper@37906: neuper@37906: | nxt_up thy ptp scr E l ay neuper@37906: (Const ("Script.Or",_) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v neuper@37906: neuper@37906: | nxt_up thy ptp scr E l ay neuper@37906: (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v neuper@37906: neuper@37906: | nxt_up thy ptp scr E l ay neuper@37906: (Const ("Script.Or",_) $ _ ) a v = neuper@37906: nstep_up thy ptp scr E (drop_last l) ay a v neuper@37906: (* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ _ $ _), a, v) = neuper@37906: (thy, ptp, (Script sc), neuper@37906: E, up, ay,(go up sc), a, v); neuper@37906: *) neuper@37906: | nxt_up thy ptp scr E l ay (*all has been done in (*2*) below*) neuper@37906: (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v = neuper@37906: nstep_up thy ptp scr E l ay a v neuper@37906: (* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _ $ e2), a, v) = neuper@37906: (thy, ptp, (Script sc), neuper@37906: E, up, ay,(go up sc), a, v); neuper@37906: *) neuper@37906: | nxt_up thy ptp scr E l ay (*comes from e2*) neuper@37906: (Const ("Script.Seq"(*2*),_) $ _ $ e2) a v = neuper@37906: nstep_up thy ptp scr E l ay a v neuper@37906: (* val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq",_) $ _), a, v) = neuper@37906: (thy, ptp, (Script sc), neuper@37906: E, up, ay,(go up sc), a, v); neuper@37906: *) neuper@37906: | nxt_up thy ptp (scr as Script sc) E l ay (*comes from e1*) neuper@37906: (Const ("Script.Seq",_) $ _) a v = neuper@37906: if ay = Napp_ neuper@37906: then nstep_up thy ptp scr E (drop_last l) Napp_ a v neuper@37906: else (*Skip_*) neuper@37906: let val up = drop_last l; neuper@37906: val Const ("Script.Seq"(*2*),_) $ _ $ e2 = go up sc; neuper@37906: in case appy thy ptp E (up@[R]) e2 a v of neuper@37906: Appy lr => Appy lr neuper@37906: | Napp E => nstep_up thy ptp scr E up Napp_ a v neuper@37906: | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end neuper@37906: neuper@37906: | nxt_up (thy,_) ptp scr E l ay t a v = neuper@38053: error ("nxt_up not impl for " ^ term2str t) neuper@37906: neuper@37906: (* val (thy, ptp, (Script sc), E, l, ay, a, v)= neuper@37906: (thy, ptp, scr, E, l, Skip_, a, v); neuper@37906: val (thy, ptp, (Script sc), E, l, ay, a, v)= neuper@37906: (thy, ptp, sc, E, l, Skip_, a, v); neuper@37906: *) neuper@37906: and nstep_up thy ptp (Script sc) E l ay a v = neuper@38053: ((*tracing ("### nstep_up from: " ^ (loc_2str l)); neuper@38053: tracing ("### nstep_up from: " ^ term2str (go l sc));*) neuper@37906: if 1 < length l neuper@37906: then neuper@37906: let neuper@37906: val up = drop_last l; neuper@38053: in ((*tracing("### nstep_up to: " ^ term2str (go up sc));*) neuper@37906: nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end neuper@37906: else (*interpreted to end*) neuper@37906: if ay = Skip_ then Skip (v, E) else Napp E neuper@37906: ); neuper@37906: neuper@37906: (* decide for the next applicable stac in the script; neuper@37906: returns (stactic, value) - the value in case the script is finished neuper@37906: 12.8.02: ~~~~~ and no assumptions ??? FIXME ??? neuper@37906: 20.8.02: must return p in case of finished, because the next script neuper@37906: consulted need not be the calling script: neuper@37906: in case of detail ie. _inserted_ PrfObjs, the next stac neuper@37906: has to searched in a script with PblObj.status<>Complete ! neuper@37906: (.. not true for other details ..PrfObj ?????????????????? neuper@37906: 20.8.02: do NOT return safe (is only changed in locate !!!) neuper@37906: *) neuper@41996: fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) = neuper@41996: let val ctxt = get_ctxt pt p neuper@41996: in neuper@41996: if f = f' neuper@41996: then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt), neuper@41996: (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*) neuper@41996: else neuper@41996: (case next_rule rss f of neuper@41996: NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*) neuper@41996: | SOME (Thm (id,thm))(*8.6.03: muss auch f' liefern ?!!*) => neuper@41996: (Rewrite' (thy, "e_rew_ord", e_rls,(*!?!8.6.03*) false, neuper@41996: (id, string_of_thmI thm), f,(e_term,[(*!?!8.6.03*)])), neuper@41996: (Uistate, ctxt), (e_term, Sundef))) (*next stac*) neuper@41996: end neuper@41999: neuper@41996: | next_tac thy (ptp as (pt,pos as (p,_)):ptree * pos') (sc as Script (h $ body)) neuper@41996: (ScrState (E,l,a,v,s,b), ctxt) = neuper@41996: let val ctxt = get_ctxt pt pos neuper@41996: in neuper@41996: (case if l = [] neuper@41996: then appy thy ptp E [R] body NONE v neuper@41996: else nstep_up thy ptp sc E l Skip_ a v of neuper@41996: Skip (v, _) => (*finished*) neuper@41996: (case par_pbl_det pt p of neuper@41996: (true, p', _) => neuper@41996: let val (_,pblID,_) = get_obj g_spec pt p'; neuper@41996: in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])), neuper@41996: (e_istate, ctxt), (v,s)) neuper@41996: end neuper@41996: | (_, p', rls') => neuper@41996: (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s))) neuper@41996: | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*) neuper@41996: | Appy (m', scrst as (_,_,_,v,_,_)) => neuper@41996: (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*) neuper@41996: end neuper@41999: neuper@41972: | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is)); neuper@37906: neuper@37906: neuper@37906: (*.create the initial interpreter state from the items of the guard.*) neuper@41999: fun init_scrstate thy itms metID =(*FIXME.WN170511: delete ctxt from value*) neuper@41996: let neuper@41996: val actuals = itms2args thy metID itms; neuper@41996: val scr as Script sc = (#scr o get_met) metID; neuper@41996: val formals = formal_args sc neuper@41996: (*expects same sequence of (actual) args in itms and (formal) args in met*) neuper@41996: fun relate_args env [] [] = env neuper@41996: | relate_args env _ [] = neuper@41996: error ("ERROR in creating the environment for '" ^ neuper@41996: id_of_scr sc ^ "' from \nthe items of the guard of " ^ neuper@41996: metID2str metID ^ ",\n" ^ neuper@41996: "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^ neuper@41996: (string_of_int o length) formals ^ neuper@41996: " formals: " ^ terms2str formals ^ "\n" ^ neuper@41996: (string_of_int o length) actuals ^ neuper@41996: " actuals: " ^ terms2str actuals) neuper@41996: | relate_args env [] actual_finds = env (*may drop Find!*) neuper@41996: | relate_args env (a::aa) (f::ff) = neuper@41996: if type_of a = type_of f neuper@41996: then relate_args (env @ [(a, f)]) aa ff neuper@41996: else neuper@41996: error ("ERROR in creating the environment for '" ^ neuper@41996: id_of_scr sc ^ "' from \nthe items of the guard of " ^ neuper@41996: metID2str metID ^ ",\n" ^ neuper@41996: "different types of formal arg, from the script, " ^ neuper@41996: "and actual arg, from the guards env:'\n" ^ neuper@41996: "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^ neuper@41996: "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^ neuper@41996: "in\n" ^ neuper@41996: "formals: " ^ terms2str formals ^ "\n" ^ neuper@41996: "actuals: " ^ terms2str actuals) neuper@41996: val env = relate_args [] formals actuals; neuper@41997: in (ScrState (env,[],NONE,e_term,Safe,true), (*FIXME.WN170511 remove*)e_ctxt, scr):istate * Proof.context * scr end; neuper@37906: neuper@41996: (* decide, where to get script/istate from: neuper@37906: (*1*) from PblObj.env: at begin of script if no init_form neuper@37906: (*2*) from PblObj/PrfObj: if stac is in the middle of the script neuper@41996: (*3*) from rls/PrfObj: in case of detail a ruleset *) neuper@37906: fun from_pblobj_or_detail' thy' (p,p_) pt = neuper@41996: let val ctxt = get_ctxt pt (p,p_) neuper@41996: in neuper@37935: if member op = [Pbl,Met] p_ neuper@37906: then case get_obj g_env pt p of neuper@41996: NONE => error "from_pblobj_or_detail': no istate" neuper@41996: | SOME is => neuper@41996: let neuper@41996: val metID = get_obj g_metID pt p neuper@41996: val {srls,...} = get_met metID neuper@41996: in (srls, is, (#scr o get_met) metID) end neuper@37906: else neuper@41996: let val (pbl,p',rls') = par_pbl_det pt p neuper@41996: in if pbl neuper@41996: then (*2*) neuper@41996: let neuper@41996: val thy = assoc_thy thy' neuper@41996: val PblObj{meth=itms,...} = get_obj I pt p' neuper@41996: val metID = get_obj g_metID pt p' neuper@41996: val {srls,...} = get_met metID neuper@41996: in (*if last_elem p = 0 nothing written to pt yet*) neuper@41996: (srls, get_loc pt (p,p_), (#scr o get_met) metID) neuper@41996: end neuper@41996: else (*3*) neuper@41996: (e_rls, (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) neuper@41996: get_loc pt (p,p_), neuper@41996: case rls' of neuper@41996: Rls {scr=scr,...} => scr neuper@41996: | Seq {scr=scr,...} => scr neuper@41996: | Rrls {scr=rfuns,...} => rfuns) neuper@41996: end neuper@41996: end; neuper@37906: neuper@41996: (*.get script and istate from PblObj, see (*1*) above.*) bonzai@41948: fun from_pblobj' thy' (p,p_) pt = neuper@42001: let neuper@42001: val p' = par_pblobj pt p neuper@42001: val thy = assoc_thy thy' neuper@42001: val PblObj {meth=itms, ctxt, ...} = get_obj I pt p' neuper@42001: val metID = get_obj g_metID pt p' neuper@42001: val {srls,scr,...} = get_met metID neuper@42001: in neuper@42001: if last_elem p = 0 (*nothing written to pt yet*) neuper@42001: then neuper@42001: let val (is, _, scr) = init_scrstate thy itms metID neuper@42001: in (srls, (is, ctxt), scr) end bonzai@41953: else (srls, get_loc pt (p,p_), scr) neuper@37906: end; neuper@37906: neuper@37906: (*.get the stactics and problems of a script as tacs neuper@37906: instantiated with the current environment; neuper@37906: l is the location which generated the given formula.*) neuper@37906: (*WN.12.5.03: quick-and-dirty repair for listexpressions*) neuper@37906: fun is_spec_pos Pbl = true neuper@37906: | is_spec_pos Met = true neuper@37906: | is_spec_pos _ = false; neuper@37906: neuper@37906: (*. fetch _all_ tactics from script .*) neuper@37906: fun sel_rules _ (([],Res):pos') = neuper@37906: raise PTREE "no tactics applicable at the end of a calculation" neuper@37906: | sel_rules pt (p,p_) = neuper@37906: if is_spec_pos p_ neuper@37906: then [get_obj g_tac pt 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 thy = assoc_thy thy'; neuper@37906: val metID = get_obj g_metID pt pp; neuper@37906: val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp) neuper@37906: else metID neuper@37906: val {scr=Script sc,srls,...} = get_met metID' bonzai@41953: val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_); neuper@37906: in map ((stac2tac pt thy) o rep_stacexpr o #2 o neuper@37906: (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end; neuper@37906: (* neuper@38058: > val Script sc = (#scr o get_met) ("SqRoot","sqrt-equ-test"); neuper@40836: > val env = [((term_of o the o (parse (Thy_Info.get_theory "Isac"))) "bdv", neuper@40836: (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "x")]; neuper@37926: > map ((stac2tac pt thy) o #2 o(subst_stacexpr env NONE e_term)) (stacpbls sc); neuper@37906: *) neuper@37906: neuper@37906: neuper@37906: (*. fetch tactics from script and filter _applicable_ tactics; neuper@37906: in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*) neuper@37906: fun sel_appl_atomic_tacs _ (([],Res):pos') = neuper@37906: raise PTREE "no tactics applicable at the end of a calculation" neuper@37906: | sel_appl_atomic_tacs pt (p,p_) = neuper@37906: if is_spec_pos p_ neuper@37906: then [get_obj g_tac pt 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 thy = assoc_thy thy' neuper@37906: val metID = get_obj g_metID pt pp neuper@37906: val metID' =if metID = e_metID neuper@37906: then (thd3 o snd3) (get_obj g_origin pt pp) neuper@37906: else metID neuper@37906: val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID' bonzai@41953: val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_) neuper@37906: val alltacs = (*we expect at least 1 stac in a script*) neuper@37906: map ((stac2tac pt thy) o rep_stacexpr o #2 o neuper@37906: (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) 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: (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*) neuper@37906: in (distinct o flat o neuper@37906: (map (atomic_appl_tacs thy ro erls f))) alltacs end; neuper@37906: neuper@37906: neuper@37906: (* neuper@37906: end neuper@37906: open Interpreter; neuper@37906: *) neuper@37906: neuper@37906: (* use"ME/script.sml"; neuper@37906: use"script.sml"; neuper@37906: *)