1.1 --- a/src/Tools/isac/Interpret/script.sml Thu Oct 27 10:48:24 2016 +0200
1.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Nov 12 17:21:43 2016 +0100
1.3 @@ -5,296 +5,166 @@
1.4 10 20 30 40 50 60 70 80
1.5 *)
1.6
1.7 -signature INTERPRETER =
1.8 +signature LUCAS_INTERPRETER =
1.9 sig
1.10 - (*type ets (list of executed tactics) see sequent.sml*)
1.11
1.12 - datatype locate
1.13 - = NotLocatable
1.14 - | Steps of (tac_ * mout * ptree * pos' * cid * safe (* ets*)) list
1.15 -(* | ToDo of ets 28.4.02*)
1.16 -
1.17 - (*diss: next-tactic-function*)
1.18 - val next_tac : theory' -> ptree * pos' -> metID -> scr -> ets -> tac_
1.19 - (*diss: locate-function*)
1.20 - val locate_gen : theory'
1.21 - -> tac_
1.22 - -> ptree * pos' -> scr * rls -> ets -> loc_ -> locate
1.23 -
1.24 - val sel_rules : ptree -> pos' -> tac list
1.25 - val init_form : scr -> ets -> loc_ * term option (*FIXME not up to date*)
1.26 + type step = tac_ * mout * ptree * pos' * pos' list
1.27 + datatype locate = NotLocatable | Steps of istate * step list
1.28 +
1.29 + val next_tac : (*diss: next-tactic-function*)
1.30 + theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe)
1.31 + val locate_gen : (*diss: locate-function*)
1.32 + theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate
1.33 + val sel_rules : ptree -> pos' -> tac list
1.34 + val init_form : 'a -> scr -> (term * term) list -> term option
1.35 val formal_args : term -> term list
1.36
1.37 - (*shift to library ...*)
1.38 - val inst_abs : theory' -> term -> term
1.39 - val itms2args : metID -> itm list -> term list
1.40 - val user_interrupt : loc_ * (tac_ * env * env * term * term * safe)
1.41 - (*val empty : term*)
1.42 + val tac_2tac : tac_ -> tac
1.43 + val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr
1.44 + val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr
1.45 + val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree ->
1.46 + rls * (istate * Proof.context) * scr
1.47 + val rule2thm'' : rule -> thm''
1.48 + val rule2rls' : rule -> string
1.49 +
1.50 + val itms2args : 'a -> metID -> itm list -> term list
1.51 end
1.52
1.53 -
1.54 -
1.55 -
1.56 -(*
1.57 -structure Interpreter : INTERPRETER =
1.58 +(**)
1.59 +structure Lucin: LUCAS_INTERPRETER(**) =
1.60 struct
1.61 -*)
1.62 -
1.63 -(*.traces the leaves (ie. non-tactical nodes) of the script
1.64 - found by next_tac.
1.65 - a leaf is either a tactic or an 'exp' in 'let v = expr'
1.66 - where 'exp' does not contain a tactic.*)
1.67 +(**)
1.68 +(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)
1.69 val trace_script = Unsynchronized.ref false;
1.70
1.71 -type step = (*data for creating a new node in the ptree;
1.72 - designed for use:
1.73 - fun ass* scrstate steps =
1.74 - ... case ass* scrstate steps of
1.75 - Assoc (scrstate, steps) => ... ass* scrstate steps*)
1.76 - tac_ (*transformed from associated tac*)
1.77 - * mout (*result with indentation etc.*)
1.78 - * ptree (*containing node created by tac_ + resp. scrstate*)
1.79 - * pos' (*position in ptree; ptree * pos' is the proofstate*)
1.80 - * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
1.81 -val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
1.82 +(* data for creating a new node in ctree; designed for use as:
1.83 + fun ass* scrstate steps = / ... case ass* scrstate steps of /
1.84 + Assoc (scrstate, steps) => ... ass* scrstate steps *)
1.85 +type step =
1.86 + tac_ (*transformed from associated tac *)
1.87 + * mout (*result with indentation etc. *)
1.88 + * ptree (*containing node created by tac_ + resp. scrstate *)
1.89 + * pos' (*position in ptree; ptree * pos' is the proofstate *)
1.90 + * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
1.91
1.92 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
1.93 - | rule2thm'' r = error ("rule2thm': not defined for "^(rule2str r));
1.94 + | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r);
1.95 fun rule2rls' (Rls_ rls) = id_rls rls
1.96 - | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
1.97 + | rule2rls' r = error ("rule2rls': not defined for " ^ rule2str r);
1.98
1.99 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
1.100 complicated with current t in rrlsstate.*)
1.101 -fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =
1.102 +fun rts2steps steps ((pt, p), (f, f'', rss, rts), (thy', ro, er, pa)) [(r, (f', am))] =
1.103 let
1.104 val thy = assoc_thy thy'
1.105 val ctxt = get_ctxt pt p |> insert_assumptions am
1.106 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.107 val is = RrlsState (f', f'', rss, rts)
1.108 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.109 + val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.110 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.111 in (is, (m, mout, pt', p', cid) :: steps) end
1.112 - | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) ((r, (f', am))::rts') =
1.113 + | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
1.114 let
1.115 val thy = assoc_thy thy'
1.116 val ctxt = get_ctxt pt p |> insert_assumptions am
1.117 - val m = Rewrite' (thy',ro,er,pa, rule2thm'' r, f, (f', am))
1.118 - val is = RrlsState (f',f'',rss,rts)
1.119 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
1.120 + val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
1.121 + val is = RrlsState (f', f'', rss, rts)
1.122 + val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
1.123 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
1.124 in rts2steps ((m, mout, pt', p', cid)::steps)
1.125 - ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
1.126 + ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
1.127 + end
1.128 + | rts2steps _ _ _ = error "rts2steps: uncovered fun-def"
1.129
1.130 -(*. functions for the environment stack .*)
1.131 -fun accessenv id es = the (assoc((top es):env, id))
1.132 - handle _ => error ("accessenv: "^(free2str id)^" not in env");
1.133 -fun updateenv id vl (es:env stack) =
1.134 - (push (overwrite(top es, (id, vl))) (pop es)):env stack;
1.135 -fun pushenv id vl (es:env stack) =
1.136 - (push (overwrite(top es, (id, vl))) es):env stack;
1.137 -val popenv = pop:env stack -> env stack;
1.138 -
1.139 -
1.140 +(* functions for the environment stack: NOT YET IMPLEMENTED
1.141 +fun accessenv id es = the (assoc ((top es) : env, id))
1.142 + handle _ => error ("accessenv: " ^ free2str id ^ " not in env");
1.143 +fun updateenv id vl (es : env stack) =
1.144 + (push (overwrite(top es, (id, vl))) (pop es)) : env stack;
1.145 +fun pushenv id vl (es : env stack) =
1.146 + (push (overwrite(top es, (id, vl))) es) : env stack;
1.147 +val popenv = pop : env stack -> env stack;
1.148 +*)
1.149
1.150 fun de_esc_underscore str =
1.151 - let fun scan [] = []
1.152 - | scan (s::ss) = if s = "'" then (scan ss)
1.153 - else (s::(scan ss))
1.154 + let
1.155 + fun scan [] = []
1.156 + | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
1.157 in (implode o scan o Symbol.explode) str end;
1.158 -(*
1.159 -> val str = "Rewrite_Set_Inst";
1.160 -> val esc = esc_underscore str;
1.161 -val it = "Rewrite'_Set'_Inst" : string
1.162 -> val des = de_esc_underscore esc;
1.163 - val des = de_esc_underscore esc;*)
1.164
1.165 (*go at a location in a script and fetch the contents*)
1.166 fun go [] t = t
1.167 - | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
1.168 - | go (L::p) (t1 $ t2) = go p t1
1.169 - | go (R::p) (t1 $ t2) = go p t2
1.170 - | go l _ = error ("go: no "^(loc_2str l));
1.171 -(*
1.172 -> val t = (Thm.term_of o the o (parse thy)) "a+b";
1.173 -val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
1.174 -> val plus_a = go [L] t;
1.175 -> val b = go [R] t;
1.176 -> val plus = go [L,L] t;
1.177 -> val a = go [L,R] t;
1.178 -
1.179 -> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
1.180 -val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
1.181 -> val pl_pl_a_b = go [L] t;
1.182 -> val c = go [R] t;
1.183 -> val a = go [L,R,L,R] t;
1.184 -> val b = go [L,R,R] t;
1.185 -*)
1.186 -
1.187 -
1.188 -(* get a subterm t with test t, and record location *)
1.189 -fun get l test (t as Const (s,T)) =
1.190 - if test t then SOME (l,t) else NONE
1.191 - | get l test (t as Free (s,T)) =
1.192 - if test t then SOME (l,t) else NONE
1.193 - | get l test (t as Bound n) =
1.194 - if test t then SOME (l,t) else NONE
1.195 - | get l test (t as Var (s,T)) =
1.196 - if test t then SOME (l,t) else NONE
1.197 - | get l test (t as Abs (s,T,body)) =
1.198 - if test t then SOME (l:loc_,t) else get ((l@[D]):loc_) test body
1.199 - | get l test (t as t1 $ t2) =
1.200 - if test t then SOME (l,t)
1.201 - else case get (l@[L]) test t1 of
1.202 - NONE => get (l@[R]) test t2
1.203 - | SOME (l',t') => SOME (l',t');
1.204 -(*18.6.00
1.205 -> val sss = ((Thm.term_of o the o (parse thy))
1.206 - "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
1.207 - \ (let e_ = Try (Rewrite square_equation_left True eq_) \
1.208 - \ in [e_])");
1.209 - ______ compares head_of !!
1.210 -> get [] (eq_str "HOL.Let") sss; [R]
1.211 -> get [] (eq_str "Script.Try") sss; [R,L,R]
1.212 -> get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]
1.213 -> get [] (eq_str "HOL.True") sss; [R,L,R,R,L,R]
1.214 -> get [] (eq_str "e_") sss; [R,R]
1.215 -*)
1.216 + | go (D::p) (Abs(_, _, t0)) = go (p : loc_) t0
1.217 + | go (L::p) (t1 $ _) = go p t1
1.218 + | go (R::p) (_ $ t2) = go p t2
1.219 + | go l _ = error ("go: no " ^ loc_2str l);
1.220
1.221 (*.get argument of first stactic in a script for init_form.*)
1.222 -fun get_stac thy (h $ body) =
1.223 +fun get_stac thy (_ $ body) =
1.224 let
1.225 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
1.226 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.227 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.228 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
1.229 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.230 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.231 | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a
1.232 | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a
1.233 | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
1.234 | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
1.235 | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
1.236 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.237 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.238 | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
1.239 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.240 - | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
1.241 - | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
1.242 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
1.243 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.244 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.245 + | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a
1.246 + | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a
1.247 + | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
1.248 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.249 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.250 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.251 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.252 | get_t y (Abs (_,_,e)) a = get_t y e a*)
1.253 - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.254 + | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
1.255 get_t y e1 a (*don't go deeper without evaluation !*)
1.256 - | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
1.257 + | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
1.258 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
1.259
1.260 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
1.261 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
1.262 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
1.263 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
1.264 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
1.265 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
1.266 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
1.267 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
1.268 - | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
1.269 - | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a
1.270 + | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
1.271 + | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
1.272 + | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
1.273 + | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
1.274 + | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
1.275 + | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
1.276 + | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
1.277 + | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
1.278 + | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
1.279 + | get_t _ (Const ("Script.Calculate",_) $ _ ) a = SOME a
1.280
1.281 - | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
1.282 - | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a
1.283 + | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
1.284 + | get_t _ (Const ("Script.Substitute",_) $ _ ) a = SOME a
1.285
1.286 - | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
1.287 + | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
1.288
1.289 - | get_t y x _ =
1.290 - ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
1.291 - NONE)
1.292 -in get_t thy body e_term end;
1.293 + | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
1.294 + in get_t thy body e_term end
1.295 + | get_stac _ t = error ("get_stac: no fun-def. for " ^ term2str t);
1.296
1.297 fun init_form thy (Prog sc) env =
1.298 - (case get_stac thy sc of
1.299 - NONE => NONE
1.300 - | SOME stac => SOME (subst_atomic env stac))
1.301 + (case get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
1.302 | init_form _ _ _ = error "init_form: no match";
1.303
1.304 -(*the 'iteration-argument' of a stac (args not eval)*)
1.305 -fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v
1.306 - | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v
1.307 - | itr_arg _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ v) = v
1.308 - | itr_arg _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ v) = v
1.309 - | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v
1.310 - | itr_arg _ (Const ("Script.Check'_elementwise",_) $ consts $ _) = consts
1.311 - | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
1.312 - | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
1.313 - | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
1.314 - | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
1.315 -(* val t = (Thm.term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
1.316 -> itr_arg "Script" t;
1.317 -val it = Free ("e_","RealDef.real") : term
1.318 -> val t = (Thm.term_of o the o (parse thy))"xxx";
1.319 -> itr_arg "Script" t;
1.320 -*** itr_arg not impl. for xxx
1.321 -uncaught exception ERROR
1.322 - raised at: library.ML:1114.35-1114.40*)
1.323 +(* get the arguments of the script out of the scripts parsetree *)
1.324 +fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
1.325
1.326 -
1.327 -(*.get the arguments of the script out of the scripts parsetree.*)
1.328 -fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
1.329 -(*
1.330 -> formal_args scr;
1.331 - [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
1.332 - Free ("eqs_","bool List.list")] : term list
1.333 -*)
1.334 -
1.335 -(*.get the identifier of the script out of the scripts parsetree.*)
1.336 +(* get the identifier of the script out of the scripts parsetree *)
1.337 fun id_of_scr sc = (id_of o fst o strip_comb) sc;
1.338
1.339 -(*WN020526: not clear, when a is available in ass_up for eva-_true*)
1.340 +(*WN020526: not clear, when a is available in ass_up for eval_true*)
1.341 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
1.342 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
1.343 thus "NONE" must be set at the end of currying (ill designed anyway)*)
1.344 -fun upd_env_opt env (SOME a, v) = upd_env env (a,v)
1.345 - | upd_env_opt env (NONE, v) =
1.346 - (tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")"); env);
1.347 +fun upd_env_opt env (SOME a, v) = upd_env env (a, v)
1.348 + | upd_env_opt env (NONE, _) =
1.349 + ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);
1.350
1.351 -type dsc = typ; (*<-> nam..unknow in Descript.thy*)
1.352 -fun typ_str (Type (s,_)) = s
1.353 - | typ_str (TFree(s,_)) = s
1.354 - | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i);
1.355 -
1.356 -(*get the _result_-type of a description*)
1.357 -fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
1.358 -(*> val t = (Thm.term_of o the o (parse thy)) "equality";
1.359 -> val T = type_of t;
1.360 -val T = "bool => Tools.una" : typ
1.361 -> val dsc = dsc_valT t;
1.362 -val dsc = "una" : string
1.363 -
1.364 -> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
1.365 -> val T = type_of t;
1.366 -val T = "bool List.list => Tools.nam" : typ
1.367 -> val dsc = dsc_valT t;
1.368 -val dsc = "nam" : string*)
1.369 -
1.370 -(*.from penv in itm_ make args for script depending on type of description.*)
1.371 -(*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
1.372 - 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
1.373 -fun mk_arg thy d [] =
1.374 - error ("mk_arg: no data for " ^ term_to_string''' thy d)
1.375 - | mk_arg thy d [t] =
1.376 - (case dsc_valT d of
1.377 - "una" => [t]
1.378 - | "nam" =>
1.379 - [case t of
1.380 - r as (Const ("HOL.eq",_) $ _ $ _) => r
1.381 - | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality " ^ term_to_string''' thy t)]
1.382 - | s => error ("mk_arg: not impl. for "^s))
1.383 - | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
1.384 -(*
1.385 - val d = d_in itm_;
1.386 - val [t] = ts_in itm_;
1.387 -mk_arg thy
1.388 -*)
1.389 -
1.390 -
1.391 -
1.392 +type dsc = typ; (* <-> nam..unknow in Descript.thy *)
1.393
1.394 (*.create the actual parameters (args) of script: their order
1.395 is given by the order in met.pat .*)
1.396 @@ -303,140 +173,93 @@
1.397 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
1.398 (* val (thy, mI, itms) = (thy, metID, itms);
1.399 *)
1.400 -val errmsg =
1.401 - "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
1.402 -fun itms2args thy mI (itms:itm list) =
1.403 - let val mvat = max_vt itms
1.404 - fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
1.405 - val itms = filter (okv mvat) itms
1.406 - fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_)
1.407 - fun itm2arg itms (_,(d,_)) =
1.408 - case find_first (test_dsc d) itms of
1.409 - NONE =>
1.410 - error ("itms2args: '"^term2str d^"' not in itms")
1.411 - (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
1.412 - penv postponed; presently penv holds already env for script*)
1.413 - | SOME (_,_,_,_,itm_) => penvval_in itm_
1.414 - fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
1.415 - val pats = (#ppc o get_met) mI
1.416 - val _ = if pats = [] then raise ERROR errmsg else ()
1.417 - in (flat o (map (itm2arg itms))) pats end;
1.418 -(*
1.419 -> val sc = ... Solve_root_equation ...
1.420 -> val mI = ("Script","sqrt-equ-test");
1.421 -> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
1.422 -> val ts = itms2args thy mI itms;
1.423 -> map (term_to_string''' thy) ts;
1.424 -["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
1.425 -*)
1.426 +val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
1.427 +fun itms2args _ mI (itms : itm list) =
1.428 + let
1.429 + val mvat = max_vt itms
1.430 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
1.431 + val itms = filter (okv mvat) itms
1.432 + fun test_dsc d (_, _, _, _, itm_) = (d = d_in itm_)
1.433 + fun itm2arg itms (_,(d,_)) =
1.434 + case find_first (test_dsc d) itms of
1.435 + NONE => error ("itms2args: '" ^ term2str d ^ "' not in itms")
1.436 + | SOME (_, _, _, _, itm_) => penvval_in itm_
1.437 + (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
1.438 + penv postponed; presently penv holds already env for script*)
1.439 + val pats = (#ppc o get_met) mI
1.440 + val _ = if pats = [] then raise ERROR errmsg else ()
1.441 + in (flat o (map (itm2arg itms))) pats end;
1.442
1.443 -
1.444 -(*detour necessary, because generate1 delivers a string-result*)
1.445 -fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
1.446 - (Thm.term_of o the o (parse (assoc_thy thy))) res
1.447 - | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl
1.448 - at time of detection in script*)
1.449 -
1.450 -(*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac,
1.451 - then convert to a 'tac_' (as required in appy).
1.452 - arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
1.453 -fun stac2tac_ _ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ _) =
1.454 - let
1.455 - val tid = (de_esc_underscore o strip_thy) thmID
1.456 - in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_)
1.457 - end
1.458 -
1.459 - | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ _) =
1.460 - let
1.461 - val subML = ((map isapair2pair) o isalist2list) sub
1.462 - val subStr = subst2subs subML
1.463 - val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
1.464 - in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
1.465 -
1.466 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
1.467 - (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
1.468 -
1.469 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ sub $ Free (rls,_) $ _ $ f) =
1.470 - let
1.471 - val subML = ((map isapair2pair) o isalist2list) sub;
1.472 - val subStr = subst2subs subML;
1.473 - in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
1.474 -
1.475 - | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =
1.476 - (Calculate op_, Empty_Tac_)
1.477 -
1.478 - | stac2tac_ pt thy (Const ("Script.Take",_) $ t) =
1.479 - (Take (term2str t), Empty_Tac_)
1.480 -
1.481 - | stac2tac_ pt thy (Const ("Script.Substitute",_) $ isasub $ arg) =
1.482 - (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
1.483 -
1.484 - | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $
1.485 - (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) =
1.486 - (Check_elementwise (term_to_string''' thy pred), (*set*)Empty_Tac_)
1.487 -
1.488 - | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) =
1.489 - (Or_to_List, Empty_Tac_)
1.490 -
1.491 - (*12.1.01.for subproblem_equation_dummy in root-equation *)
1.492 - | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) =
1.493 - (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
1.494 +(* convert a script-tac 'stac' to a tactic 'tac';
1.495 + if stac is an initac, then convert to a 'tac_' (as required in appy).
1.496 + arg ptree for pushing the thy specified in rootpbl into subpbls *)
1.497 +fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =
1.498 + let
1.499 + val tid = (de_esc_underscore o strip_thy) thmID
1.500 + in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_) end
1.501 + | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ Free (thmID, _) $ _ $ _) =
1.502 + let
1.503 + val subML = ((map isapair2pair) o isalist2list) sub
1.504 + val subStr = subst2subs subML
1.505 + val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
1.506 + in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
1.507 + | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ Free (rls, _) $ _ $ _) =
1.508 + (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
1.509 + | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ Free (rls, _) $ _ $ _) =
1.510 + let
1.511 + val subML = ((map isapair2pair) o isalist2list) sub;
1.512 + val subStr = subst2subs subML;
1.513 + in (Rewrite_Set_Inst (subStr, rls), Empty_Tac_) end
1.514 + | stac2tac_ _ _ (Const ("Script.Calculate", _) $ Free (op_, _) $ _) = (Calculate op_, Empty_Tac_)
1.515 + | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Take (term2str t), Empty_Tac_)
1.516 + | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =
1.517 + (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
1.518 + | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $
1.519 + (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
1.520 + (Check_elementwise (term_to_string''' thy pred), Empty_Tac_)
1.521 + | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Or_to_List, Empty_Tac_)
1.522 + | stac2tac_ _ _ (Const ("Script.Tac", _) $ Free (str, _)) =
1.523 + (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
1.524
1.525 (*compare "| assod _ (Subproblem'"*)
1.526 - | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
1.527 - (Const ("Product_Type.Pair",_) $Free (dI',_) $
1.528 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.529 - let
1.530 - val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.531 - val thy = maxthy (assoc_thy dI) (rootthy pt);
1.532 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.533 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.534 - val ags = isalist2list ags';
1.535 - val (pI, pors, mI) =
1.536 - if mI = ["no_met"]
1.537 - then
1.538 - let
1.539 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.540 - handle ERROR "actual args do not match formal args"
1.541 - => (match_ags_msg pI stac ags(*raise exn*); [])
1.542 - val pI' = refine_ori' pors pI;
1.543 - in (pI', pors (*refinement over models with diff.prec only*),
1.544 - (hd o #met o get_pbt) pI') end
1.545 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.546 - handle ERROR "actual args do not match formal args"
1.547 - => (match_ags_msg pI stac ags(*raise exn*); []), mI);
1.548 - val (fmz_, vals) = oris2fmz_vals pors;
1.549 - val {cas,ppc,thy,...} = get_pbt pI
1.550 - val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
1.551 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
1.552 - val ctxt = Proof_Context.init_global
1.553 - val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1.554 - |> declare_constraints' vals
1.555 - val hdl =
1.556 - case cas of
1.557 - NONE => pblterm dI pI
1.558 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.559 - val f = subpbl (strip_thy dI) pI
1.560 - in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
1.561 - end
1.562 - | stac2tac_ pt thy t = error
1.563 - ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
1.564 + | stac2tac_ pt _ (stac as Const ("Script.SubProblem",_) $
1.565 + (Const ("Product_Type.Pair",_) $Free (dI', _) $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $
1.566 + ags') =
1.567 + let
1.568 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.569 + val thy = maxthy (assoc_thy dI) (rootthy pt);
1.570 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.571 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.572 + val ags = isalist2list ags';
1.573 + val (pI, pors, mI) =
1.574 + if mI = ["no_met"]
1.575 + then
1.576 + let
1.577 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.578 + handle ERROR "actual args do not match formal args"
1.579 + => (match_ags_msg pI stac ags(*raise exn*); [])
1.580 + val pI' = refine_ori' pors pI;
1.581 + in (pI', pors (* refinement over models with diff.prec only *),
1.582 + (hd o #met o get_pbt) pI') end
1.583 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.584 + handle ERROR "actual args do not match formal args"
1.585 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
1.586 + val (fmz_, vals) = oris2fmz_vals pors;
1.587 + val {cas,ppc,thy,...} = get_pbt pI
1.588 + val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
1.589 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
1.590 + val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
1.591 + val hdl =
1.592 + case cas of
1.593 + NONE => pblterm dI pI
1.594 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.595 + val f = subpbl (strip_thy dI) pI
1.596 + in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
1.597 + end
1.598 + | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
1.599
1.600 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
1.601
1.602 -(*test a term for being a _list_ (set ?) of constants; could be more rigorous*)
1.603 -fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
1.604 - | list_of_consts (Const ("List.list.Nil",_)) = true
1.605 - | list_of_consts _ = false;
1.606 -(*val ttt = (Thm.term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
1.607 -> list_of_consts ttt;
1.608 -val it = true : bool
1.609 -> val ttt = (Thm.term_of o the o (parse thy)) "[]";
1.610 -> list_of_consts ttt;
1.611 -val it = true : bool*)
1.612 -
1.613 -
1.614 -
1.615 datatype ass =
1.616 Ass of
1.617 tac_ * (* SubProblem gets args instantiated in assod *)
1.618 @@ -461,378 +284,227 @@
1.619 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
1.620 NotAss : e.g. thmID in stac/=/thmID in m (not =)
1.621 *)
1.622 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm'' as (thmID, _), f, (f', asm))) stac =
1.623 +fun assod _ _ (m as Rewrite_Inst' (_, _, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.624 (case stac of
1.625 - (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
1.626 - if thmID = thmID_
1.627 - then
1.628 - if f = f_
1.629 - then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.630 - else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
1.631 - else ((*tracing"3### assod ..NotAss";*)NotAss)
1.632 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
1.633 - if contains_rule (Thm thm'') (assoc_rls rls_)
1.634 - then
1.635 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.636 - else NotAss
1.637 - | _ => NotAss)
1.638 - | assod pt d (m as Rewrite' (thy, rod, rls, put, thm'' as (thmID, _), f, (f', asm))) stac =
1.639 + (Const ("Script.Rewrite'_Inst", _) $ _ $ Free (thmID_, _) $ _ $ f_) =>
1.640 + if thmID = thmID_
1.641 + then
1.642 + if f = f_
1.643 + then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
1.644 + else ((*tracing"3### assod ..AssWeak";*) AssWeak(m, f'))
1.645 + else ((*tracing"3### assod ..NotAss";*) NotAss)
1.646 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ Free (rls_, _) $ _ $ f_) =>
1.647 + if contains_rule (Thm thm'') (assoc_rls rls_)
1.648 + then if f = f_ then Ass (m,f') else AssWeak (m,f')
1.649 + else NotAss
1.650 + | _ => NotAss)
1.651 + | assod _ _ (m as Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
1.652 (case stac of
1.653 - (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
1.654 - ((*tracing ("3### assod: stac = " ^ ter2str t);
1.655 - tracing ("3### assod: f(m)= " ^ term2str f);*)
1.656 - if thmID = thmID_
1.657 - then
1.658 - if f = f_
1.659 - then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
1.660 - else
1.661 - ((*tracing"### assod ..AssWeak";
1.662 - tracing("### assod: f(m) = " ^ term2str f);
1.663 - tracing("### assod: f(stac)= " ^ term2str f_)*)
1.664 - AssWeak (m,f'))
1.665 - else ((*tracing"3### assod ..NotAss";*)NotAss))
1.666 - | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
1.667 - if contains_rule (Thm thm'') (assoc_rls rls_)
1.668 - then
1.669 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.670 - else NotAss
1.671 - | _ => NotAss)
1.672 -
1.673 - | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
1.674 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
1.675 - if id_rls rls = rls_
1.676 - then
1.677 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.678 - else NotAss
1.679 -
1.680 - | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
1.681 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
1.682 - if id_rls rls = rls_
1.683 - then
1.684 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.685 - else NotAss
1.686 -
1.687 - | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm)))
1.688 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.689 - if id_rls rls = rls_
1.690 - then
1.691 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.692 - else NotAss
1.693 -
1.694 - | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm)))
1.695 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
1.696 - if id_rls rls = rls_
1.697 - then
1.698 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.699 - else NotAss
1.700 -
1.701 - | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac =
1.702 - (case stac of
1.703 - (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
1.704 - if op_ = op__
1.705 - then
1.706 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.707 - else NotAss
1.708 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
1.709 - let
1.710 - val thy = assoc_thy "Isac";
1.711 - in
1.712 - if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
1.713 - then
1.714 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.715 - else NotAss
1.716 - end
1.717 - | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
1.718 - let
1.719 - val thy = assoc_thy "Isac";
1.720 - in
1.721 - if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
1.722 - then
1.723 - if f = f_ then Ass (m,f') else AssWeak (m,f')
1.724 - else NotAss
1.725 - end
1.726 - | _ => NotAss)
1.727 -
1.728 - | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
1.729 - (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.730 - if consts = consts'
1.731 - then Ass (m, consts_chkd)
1.732 - else NotAss
1.733 -
1.734 - | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
1.735 - Ass (m, list)
1.736 -
1.737 - | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
1.738 - Ass (m, term)
1.739 -
1.740 - | assod pt _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute",_) $ _ $ t) =
1.741 - if f = t then Ass (m, f')
1.742 - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.743 - if foldl and_ (true, map contains_Var subte)
1.744 - then
1.745 - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
1.746 - in if t = t' then error "assod: Substitute' not applicable to val of Expr"
1.747 - else Ass (Substitute' (ro, erls, subte, t, t'), t')
1.748 - end
1.749 - else (case rewrite_terms_ (Isac()) ro erls subte t of
1.750 + (Const ("Script.Rewrite", _) $ Free (thmID_, _) $ _ $ f_) =>
1.751 + ((*tracing ("3### assod: stac = " ^ ter2str t);
1.752 + tracing ("3### assod: f(m)= " ^ term2str f);*)
1.753 + if thmID = thmID_
1.754 + then
1.755 + if f = f_
1.756 + then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
1.757 + else
1.758 + ((*tracing"### assod ..AssWeak";
1.759 + tracing("### assod: f(m) = " ^ term2str f);
1.760 + tracing("### assod: f(stac)= " ^ term2str f_)*)
1.761 + AssWeak (m,f'))
1.762 + else ((*tracing"3### assod ..NotAss";*) NotAss))
1.763 + | (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =>
1.764 + if contains_rule (Thm thm'') (assoc_rls rls_)
1.765 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.766 + else NotAss
1.767 + | _ => NotAss)
1.768 + | assod _ _ (m as Rewrite_Set_Inst' (_, _, _, rls, f, (f', _)))
1.769 + (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) =
1.770 + if id_rls rls = rls_
1.771 + then if f = f_ then Ass (m, f') else AssWeak (m ,f')
1.772 + else NotAss
1.773 + | assod _ _ (m as Detail_Set_Inst' (_, _, _, rls, f, (f',_)))
1.774 + (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) =
1.775 + if id_rls rls = rls_
1.776 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.777 + else NotAss
1.778 + | assod _ _ (m as Rewrite_Set' (_, _, rls, f, (f', _)))
1.779 + (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =
1.780 + if id_rls rls = rls_
1.781 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.782 + else NotAss
1.783 + | assod _ _ (m as Detail_Set' (_, _, rls, f, (f', _)))
1.784 + (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =
1.785 + if id_rls rls = rls_
1.786 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.787 + else NotAss
1.788 + | assod _ _ (m as Calculate' (_, op_, f, (f', _))) stac =
1.789 + (case stac of
1.790 + (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
1.791 + if op_ = op__
1.792 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.793 + else NotAss
1.794 + | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free(rls_,_) $_$f_) =>
1.795 + let val thy = assoc_thy "Isac";
1.796 + in
1.797 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
1.798 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
1.799 + else NotAss
1.800 + end
1.801 + | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
1.802 + let val thy = assoc_thy "Isac";
1.803 + in
1.804 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
1.805 + then if f = f_ then Ass (m,f') else AssWeak (m,f')
1.806 + else NotAss
1.807 + end
1.808 + | _ => NotAss)
1.809 + | assod _ _ (m as Check_elementwise' (consts, _, (consts_chkd, _)))
1.810 + (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
1.811 + if consts = consts'
1.812 + then Ass (m, consts_chkd)
1.813 + else NotAss
1.814 + | assod _ _ (m as Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) = Ass (m, list)
1.815 + | assod _ _ (m as Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term)
1.816 + | assod _ _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =
1.817 + if f = t then Ass (m, f')
1.818 + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
1.819 + if foldl and_ (true, map contains_Var subte)
1.820 + then
1.821 + let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
1.822 + in if t = t' then error "assod: Substitute' not applicable to val of Expr"
1.823 + else Ass (Substitute' (ro, erls, subte, t, t'), t')
1.824 + end
1.825 + else (case rewrite_terms_ (Isac()) ro erls subte t of
1.826 SOME (t', _) => Ass (Substitute' (ro, erls, subte, t, t'), t')
1.827 | NONE => error "assod: Substitute' not applicable to val of Expr")
1.828 -
1.829 - | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
1.830 - if id = id'
1.831 - then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
1.832 - else NotAss
1.833 + | assod _ _ (m as Tac_ (thy, _, id, f')) (Const ("Script.Tac",_) $ Free (id', _)) =
1.834 + if id = id'
1.835 + then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
1.836 + else NotAss
1.837
1.838 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
1.839 - | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
1.840 - (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
1.841 - Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.842 - let
1.843 - val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.844 - val thy = maxthy (assoc_thy dI) (rootthy pt);
1.845 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.846 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.847 - val ags = isalist2list ags';
1.848 - val (pI, pors, mI) =
1.849 - if mI = ["no_met"]
1.850 - then
1.851 - let
1.852 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.853 - handle ERROR "actual args do not match formal args"
1.854 - => (match_ags_msg pI stac ags(*raise exn*);[]);
1.855 - val pI' = refine_ori' pors pI;
1.856 - in (pI', pors (*refinement over models with diff.prec only*),
1.857 - (hd o #met o get_pbt) pI')
1.858 - end
1.859 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.860 - handle ERROR "actual args do not match formal args"
1.861 - => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
1.862 - val (fmz_, vals) = oris2fmz_vals pors;
1.863 - val {cas, ppc, thy,...} = get_pbt pI
1.864 - val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.865 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
1.866 - val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
1.867 - |> declare_constraints' vals
1.868 - val hdl =
1.869 - case cas of
1.870 - NONE => pblterm dI pI
1.871 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.872 - val f = subpbl (strip_thy dI) pI
1.873 - in
1.874 - if domID = dI andalso pblID = pI
1.875 - then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
1.876 - else NotAss
1.877 - end
1.878 + | assod pt _ (Subproblem' ((domID, pblID, _), _, _, _, _, _))
1.879 + (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
1.880 + Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
1.881 + let
1.882 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
1.883 + val thy = maxthy (assoc_thy dI) (rootthy pt);
1.884 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
1.885 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
1.886 + val ags = isalist2list ags';
1.887 + val (pI, pors, mI) =
1.888 + if mI = ["no_met"]
1.889 + then
1.890 + let
1.891 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
1.892 + handle ERROR "actual args do not match formal args"
1.893 + => (match_ags_msg pI stac ags(*raise exn*);[]);
1.894 + val pI' = refine_ori' pors pI;
1.895 + in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o get_pbt) pI')
1.896 + end
1.897 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
1.898 + handle ERROR "actual args do not match formal args"
1.899 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
1.900 + val (fmz_, vals) = oris2fmz_vals pors;
1.901 + val {cas, ppc, thy, ...} = get_pbt pI
1.902 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
1.903 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
1.904 + val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
1.905 + val hdl =
1.906 + case cas of
1.907 + NONE => pblterm dI pI
1.908 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
1.909 + val f = subpbl (strip_thy dI) pI
1.910 + in
1.911 + if domID = dI andalso pblID = pI
1.912 + then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
1.913 + else NotAss
1.914 + end
1.915 + | assod _ _ m _ =
1.916 + (if (!trace_script)
1.917 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
1.918 + ^ "@@@ tac_ = " ^ tac_2str m)
1.919 + else ();
1.920 + NotAss);
1.921
1.922 - | assod pt d m t =
1.923 - (if (!trace_script)
1.924 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
1.925 - "@@@ tac_ = "^(tac_2str m))
1.926 - else ();
1.927 - NotAss);
1.928 -
1.929 -fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI
1.930 - | tac_2tac (Model_Problem' (pI,_,_)) = Model_Problem
1.931 - | tac_2tac (Add_Given' (t,_)) = Add_Given t
1.932 - | tac_2tac (Add_Find' (t,_)) = Add_Find t
1.933 - | tac_2tac (Add_Relation' (t,_)) = Add_Relation t
1.934 +fun tac_2tac (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
1.935 + | tac_2tac (Model_Problem' (_, _, _)) = Model_Problem
1.936 + | tac_2tac (Add_Given' (t, _)) = Add_Given t
1.937 + | tac_2tac (Add_Find' (t, _)) = Add_Find t
1.938 + | tac_2tac (Add_Relation' (t, _)) = Add_Relation t
1.939
1.940 - | tac_2tac (Specify_Theory' dI) = Specify_Theory dI
1.941 - | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
1.942 - | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
1.943 + | tac_2tac (Specify_Theory' dI) = Specify_Theory dI
1.944 + | tac_2tac (Specify_Problem' (dI, _)) = Specify_Problem dI
1.945 + | tac_2tac (Specify_Method' (dI, _, _)) = Specify_Method dI
1.946
1.947 | tac_2tac (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
1.948 | tac_2tac (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (subst2subs sub, thm)
1.949
1.950 - | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
1.951 - | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
1.952 + | tac_2tac (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (id_rls rls)
1.953 + | tac_2tac (Detail_Set' (_, _, rls, _, _)) = Detail_Set (id_rls rls)
1.954
1.955 - | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
1.956 - Rewrite_Set_Inst (subst2subs sub,id_rls rls)
1.957 - | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
1.958 - Detail_Set_Inst (subst2subs sub,id_rls rls)
1.959 + | tac_2tac (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
1.960 + Rewrite_Set_Inst (subst2subs sub,id_rls rls)
1.961 + | tac_2tac (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
1.962 + Detail_Set_Inst (subst2subs sub,id_rls rls)
1.963
1.964 - | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)
1.965 -
1.966 - | tac_2tac (Check_elementwise' (consts,pred,consts')) = Check_elementwise pred
1.967 + | tac_2tac (Calculate' (_, op_, _, _)) = Calculate (op_)
1.968 + | tac_2tac (Check_elementwise' (_, pred, _)) = Check_elementwise pred
1.969
1.970 | tac_2tac (Or_to_List' _) = Or_to_List
1.971 | tac_2tac (Take' term) = Take (term2str term)
1.972 - | tac_2tac (Substitute' (_, _, subte, t, res)) = Substitute (subte2sube subte)
1.973 -
1.974 - | tac_2tac (Tac_ (_,f,id,f')) = Tac id
1.975 + | tac_2tac (Substitute' (_, _, subte, _, _)) = Substitute (subte2sube subte)
1.976 + | tac_2tac (Tac_ (_, _, id, _)) = Tac id
1.977
1.978 | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
1.979 | tac_2tac (Check_Postcond' (pblID, _)) = Check_Postcond pblID
1.980 | tac_2tac Empty_Tac_ = Empty_Tac
1.981 - | tac_2tac m =
1.982 - error ("tac_2tac: not impl. for "^(tac_2str m));
1.983 + | tac_2tac m = error ("tac_2tac: not impl. for "^(tac_2str m));
1.984
1.985 -
1.986 -
1.987 -
1.988 -(** decompose tac_ to a rule and to (lhs,rhs)
1.989 - unly needed --- **)
1.990 -
1.991 -val idT = Type ("Script.ID",[]);
1.992 -(*val tt = (Thm.term_of o the o (parse thy)) "square_equation_left::ID";
1.993 -type_of tt = idT;
1.994 -val it = true : bool
1.995 -*)
1.996 +val idT = Type ("Script.ID", []);
1.997
1.998 fun make_rule thy t =
1.999 let val ct = Thm.global_cterm_of thy (Trueprop $ t)
1.1000 in Thm (term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
1.1001
1.1002 -(* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
1.1003 - *)
1.1004 -(*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
1.1005 - NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!
1.1006 -WN0508 only use in tac_2res, which uses only last return-value*)
1.1007 -fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
1.1008 - let val fT = type_of f;
1.1009 - val b = if put then @{term True} else @{term False};
1.1010 - val sT = (type_of o fst o hd) subs;
1.1011 - val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.1012 - (map HOLogic.mk_prod subs);
1.1013 - val sT' = type_of subs';
1.1014 - val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT)
1.1015 - $ subs' $ Free (thmID, idT) $ b $ f;
1.1016 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1017 -(*Fehlersuche 25.4.01
1.1018 -(a)----- als String zusammensetzen:
1.1019 -ML> term2str f;
1.1020 -val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
1.1021 -ML> term2str f';
1.1022 -val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
1.1023 -ML> subs;
1.1024 -val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
1.1025 -> val tt = (Thm.term_of o the o (parse thy))
1.1026 - "(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))";
1.1027 -> atomty tt;
1.1028 -ML> tracing (term2str tt);
1.1029 -(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
1.1030 - #0 + d_d x (x ^^^ #2 + #3 * x)
1.1031 +fun rep_tac_ (Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _))) =
1.1032 + let val fT = type_of f;
1.1033 + val b = if put then @{term True} else @{term False};
1.1034 + val sT = (type_of o fst o hd) subs;
1.1035 + val subs' = list2isalist (HOLogic.mk_prodT (sT, sT)) (map HOLogic.mk_prod subs);
1.1036 + val sT' = type_of subs';
1.1037 + val lhs = Const ("Script.Rewrite'_Inst", [sT', idT, bool, fT] ---> fT)
1.1038 + $ subs' $ Free (thmID, idT) $ b $ f;
1.1039 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.1040 + | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.1041 + let
1.1042 + val fT = type_of f;
1.1043 + val b = if put then @{term True} else @{term False};
1.1044 + val lhs = Const ("Script.Rewrite", [idT, HOLogic.boolT, fT] ---> fT)
1.1045 + $ Free (thmID, idT) $ b $ f;
1.1046 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.1047 + | rep_tac_ (Rewrite_Set_Inst' (_, _, _, _, _, (f', _))) = (e_rule, (e_term, f'))
1.1048 + | rep_tac_ (Rewrite_Set' (thy', put, rls, f, (f', _))) =
1.1049 + let
1.1050 + val fT = type_of f;
1.1051 + val b = if put then @{term True} else @{term False};
1.1052 + val lhs = Const ("Script.Rewrite'_Set", [idT, bool, fT] ---> fT)
1.1053 + $ Free (id_rls rls, idT) $ b $ f;
1.1054 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1055 + | rep_tac_ (Calculate' (thy', op_, f, (f', _)))=
1.1056 + let
1.1057 + val fT = type_of f;
1.1058 + val lhs = Const ("Script.Calculate",[idT,fT] ---> fT) $ Free (op_,idT) $ f
1.1059 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1060 + | rep_tac_ (Check_elementwise' (_, _, (t', _))) = (Erule, (e_term, t'))
1.1061 + | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
1.1062 + | rep_tac_ (Take' t') = (Erule, (e_term, t'))
1.1063 + | rep_tac_ (Substitute' (_, _, _, t, t')) = (Erule, (t, t'))
1.1064 + | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
1.1065 + | rep_tac_ m = error ("rep_tac_: not impl.for " ^ tac_2str m)
1.1066
1.1067 -(b)----- laut rep_tac_:
1.1068 -> val ttt=HOLogic.mk_eq (lhs,f');
1.1069 -> atomty ttt;
1.1070 -
1.1071 -
1.1072 -(*Fehlersuche 1-2Monate vor 4.01:*)
1.1073 -> val tt = (Thm.term_of o the o (parse thy))
1.1074 - "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
1.1075 -> atomty tt;
1.1076 -
1.1077 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.1078 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.1079 -> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
1.1080 - (Thm.term_of o the o (parse thy)) "x")];
1.1081 -> val sT = (type_of o fst o hd) subs;
1.1082 -> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.1083 - (map HOLogic.mk_prod subs);
1.1084 -> val sT' = type_of subs';
1.1085 -> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
1.1086 - $ subs' $ Free (thmID,idT) $ @{term True} $ f;
1.1087 -> lhs = tt;
1.1088 -val it = true : bool
1.1089 -> rep_tac_ (Rewrite_Inst'
1.1090 - ("Script","tless_true","eval_rls",false,subs,
1.1091 - ("square_equation_left",""),f,(f',[])));
1.1092 -*)
1.1093 - | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.1094 - let
1.1095 - val fT = type_of f;
1.1096 - val b = if put then @{term True} else @{term False};
1.1097 - val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
1.1098 - $ Free (thmID, idT) $ b $ f;
1.1099 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1100 -(*
1.1101 -> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
1.1102 - "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
1.1103 -
1.1104 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.1105 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.1106 -> val Thm (id,thm) =
1.1107 - rep_tac_ (Rewrite'
1.1108 - ("Script","tless_true","eval_rls",false,
1.1109 - ("square_equation_left",""),f,(f',[])));
1.1110 -> val SOME ct = parse thy
1.1111 - "Rewrite square_equation_left True (x=#1+#2)";
1.1112 -> rewrite_ Script.thy tless_true eval_rls true thm ct;
1.1113 -val it = SOME ("x = #3",[]) : (cterm * cterm list) option
1.1114 -*)
1.1115 - | rep_tac_ (Rewrite_Set_Inst'
1.1116 - (thy',put,subs,rls,f,(f',asm))) =
1.1117 - (e_rule, (e_term, f'))
1.1118 -(*WN050824: type error ...
1.1119 - let val fT = type_of f;
1.1120 - val sT = (type_of o fst o hd) subs;
1.1121 - val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.1122 - (map HOLogic.mk_prod subs);
1.1123 - val sT' = type_of subs';
1.1124 - val b = if put then @{term True} else @{term False}
1.1125 - val lhs = Const ("Script.Rewrite'_Set'_Inst",
1.1126 - [sT',idT,fT,fT] ---> fT)
1.1127 - $ subs' $ Free (id_rls rls,idT) $ b $ f;
1.1128 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
1.1129 -(* ... vals from Rewrite_Inst' ...
1.1130 -> rep_tac_ (Rewrite_Set_Inst'
1.1131 - ("Script",false,subs,
1.1132 - "isolate_bdv",f,(f',[])));
1.1133 -*)
1.1134 -(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
1.1135 -*)
1.1136 - | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
1.1137 - let val fT = type_of f;
1.1138 - val b = if put then @{term True} else @{term False};
1.1139 - val lhs = Const ("Script.Rewrite'_Set",[idT,bool,fT] ---> fT)
1.1140 - $ Free (id_rls rls,idT) $ b $ f;
1.1141 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1142 -(* 13.3.01:
1.1143 -val thy = assoc_thy thy';
1.1144 -val t = HOLogic.mk_eq (lhs,f');
1.1145 -make_rule thy t;
1.1146 ---------------------------------------------------
1.1147 -val lll = (Thm.term_of o the o (parse thy))
1.1148 - "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
1.1149 -
1.1150 ---------------------------------------------------
1.1151 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.1152 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.1153 -> val Thm (id,thm) =
1.1154 - rep_tac_ (Rewrite_Set'
1.1155 - ("Script",false,"SqRoot_simplify",f,(f',[])));
1.1156 -val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
1.1157 -val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
1.1158 -*)
1.1159 - | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
1.1160 - let val fT = type_of f;
1.1161 - val lhs = Const ("Script.Calculate",[idT,fT] ---> fT)
1.1162 - $ Free (op_,idT) $ f
1.1163 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
1.1164 -(*
1.1165 -> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
1.1166 - ... test-root-equ.sml: calculate ...
1.1167 -> val Appl m'=applicable_in p pt (Calculate "PLUS");
1.1168 -> val (lhs,_)=tac_2etac m';
1.1169 -> lhs'=lhs;
1.1170 -val it = true : bool*)
1.1171 - | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
1.1172 - | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
1.1173 - | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
1.1174 - | rep_tac_ (Substitute' (_, _, subst,t,t')) = (Erule, (t, t'))
1.1175 - | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
1.1176 - | rep_tac_ m = error ("rep_tac_: not impl.for "^
1.1177 - (tac_2str m));
1.1178 -
1.1179 -(*"N.3.6.03------
1.1180 -fun tac_2rule m = (fst o rep_tac_) m;
1.1181 -fun tac_2etac m = (snd o rep_tac_) m;
1.1182 -fun tac_2tac m = (fst o snd o rep_tac_) m;*)
1.1183 -fun tac_2res m = (snd o snd o rep_tac_) m;(*ONLYuse of rep_tac_
1.1184 - FIXXXXME: simplify rep_tac_*)
1.1185 -
1.1186 +fun tac_2res m = (snd o snd o rep_tac_) m;
1.1187
1.1188 (* handle a leaf at the end of recursive descent:
1.1189 a leaf is either a tactic or an 'expr' in "let v = expr"
1.1190 @@ -843,295 +515,244 @@
1.1191 *)
1.1192 fun handle_leaf call thy srls E a v t =
1.1193 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
1.1194 - case subst_stacexpr E a v t of
1.1195 - (a', STac stac) => (*script-tactic*)
1.1196 - let val stac' =
1.1197 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.1198 - in
1.1199 - (if (!trace_script)
1.1200 - then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
1.1201 - else ();
1.1202 - (a', STac stac'))
1.1203 - end
1.1204 - | (a', Expr lexpr) => (*leaf-expression*)
1.1205 - let val lexpr' =
1.1206 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.1207 - in
1.1208 - (if (!trace_script)
1.1209 - then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
1.1210 - else ();
1.1211 - (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
1.1212 - end;
1.1213 + case subst_stacexpr E a v t of
1.1214 + (a', STac stac) => (*script-tactic*)
1.1215 + let val stac' =
1.1216 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
1.1217 + in
1.1218 + (if (! trace_script)
1.1219 + then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac ^"'")
1.1220 + else ();
1.1221 + (a', STac stac'))
1.1222 + end
1.1223 + | (a', Expr lexpr) => (*leaf-expression*)
1.1224 + let val lexpr' =
1.1225 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
1.1226 + in
1.1227 + (if (! trace_script)
1.1228 + then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
1.1229 + else ();
1.1230 + (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
1.1231 + end;
1.1232
1.1233 -
1.1234 -(** locate an applicable stactic in a script **)
1.1235 -
1.1236 -datatype assoc = (*ExprVal in the sense of denotational semantics*)
1.1237 - Assoc of (*the stac is associated, strongly or weakly*)
1.1238 - scrstate * (*the current; returned for next_tac etc. outside ass* *)
1.1239 - (step list) (*list of steps done until associated stac found;
1.1240 - initiated with the data for doing the 1st step,
1.1241 - thus the head holds these data further on,
1.1242 - while the tail holds steps finished (incl.scrstate in ptree)*)
1.1243 -| NasApp of (*stac not associated, but applicable, ptree-node generated*)
1.1244 +(** locate an applicable stac in a script **)
1.1245 +datatype assoc = (* ExprVal in the sense of denotational semantics *)
1.1246 + Assoc of (* the stac is associated, strongly or weakly *)
1.1247 + scrstate * (* the current; returned for next_tac etc. outside ass* *)
1.1248 + (step list) (* list of steps done until associated stac found;
1.1249 + initiated with the data for doing the 1st step,
1.1250 + thus the head holds these data further on,
1.1251 + while the tail holds steps finished (incl.scrstate in ptree) *)
1.1252 +| NasApp of (* stac not associated, but applicable, ptree-node generated *)
1.1253 scrstate * (step list)
1.1254 -| NasNap of (*stac not associated, not applicable, nothing generated;
1.1255 - for distinction in Or, for leaving iterations, leaving Seq,
1.1256 - evaluate scriptexpressions*)
1.1257 +| NasNap of (* stac not associated, not applicable, nothing generated;
1.1258 + for distinction in Or, for leaving iterations, leaving Seq,
1.1259 + evaluate scriptexpressions *)
1.1260 term * env;
1.1261 -fun assoc2str (Assoc _) = "Assoc"
1.1262 - | assoc2str (NasNap _) = "NasNap"
1.1263 +fun assoc2str (Assoc _) = "Assoc"
1.1264 + | assoc2str (NasNap _) = "NasNap"
1.1265 | assoc2str (NasApp _) = "NasApp";
1.1266
1.1267 +datatype asap = (* arg. of assy _only_ for distinction w.r.t. Or *)
1.1268 + Aundef (* undefined: set only by (topmost) Or *)
1.1269 +| AssOnly (* do not execute appl stacs - there could be an associated
1.1270 + in parallel Or-branch *)
1.1271 +| AssGen; (* no Ass(Weak) found within Or, thus
1.1272 + search for _applicable_ stacs, execute and generate pt *)
1.1273 +(*this constructions doesnt allow arbitrary nesting of Or !!! *)
1.1274
1.1275 -datatype asap = (*arg. of assy _only_ for distinction w.r.t. Or*)
1.1276 - Aundef (*undefined: set only by (topmost) Or*)
1.1277 -| AssOnly (*do not execute appl stacs - there could be an associated
1.1278 - in parallel Or-branch*)
1.1279 -| AssGen; (*no Ass(Weak) found within Or, thus
1.1280 - search for _applicable_ stacs, execute and generate pt*)
1.1281 -(*this constructions doesnt allow arbitrary nesting of Or !!!*)
1.1282 +(* assy, ass_up, astep_up scan for locate_gen in a script.
1.1283 + search is clearly separated into (1)-(2):
1.1284 + (1) assy is recursive descent;
1.1285 + (2) ass_up resumes interpretation at a location somewhere in the script;
1.1286 + astep_up does only get to the parentnode of the scriptexpr.
1.1287 + consequence:
1.1288 + * call of (2) means _always_ that in this branch below
1.1289 + there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
1.1290 +*)
1.1291 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
1.1292 +fun assy ya ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.1293 + (case assy ya ((E , l @ [L, R], a,v,S,b),ss) e of
1.1294 + NasApp ((E',l,a,v,S,_),ss) =>
1.1295 + let
1.1296 + val id' = mk_Free (id, T);
1.1297 + val E' = upd_env E' (id', v);
1.1298 + in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
1.1299 + | NasNap (v,E) =>
1.1300 + let
1.1301 + val id' = mk_Free (id, T);
1.1302 + val E' = upd_env E (id', v);
1.1303 + in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
1.1304 + | ay => ay)
1.1305 + | assy (ya as (thy,_,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
1.1306 + if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
1.1307 + then assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e
1.1308 + else NasNap (v, E)
1.1309 + | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
1.1310 + if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.1311 + then assy ya ((E, l @ [R], a,v,S,b),ss) e
1.1312 + else NasNap (v, E)
1.1313 + | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
1.1314 + if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.1315 + then assy ya ((E, l @ [L, R], a,v,S,b),ss) e1
1.1316 + else assy ya ((E, l @ [R], a,v,S,b),ss) e2
1.1317 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
1.1318 + (case assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e of ay => ay)
1.1319 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
1.1320 + (case assy ya ((E, l @ [R], a,v,S,b),ss) e of ay => ay)
1.1321 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
1.1322 + (case assy ya ((E, l @ [L, L, R], SOME a,v,S,b),ss) e1 of
1.1323 + NasNap (v, E) => assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e2
1.1324 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e2
1.1325 + | ay => ay)
1.1326 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
1.1327 + (case assy ya ((E, l @ [L, R], a,v,S,b),ss) e1 of
1.1328 + NasNap (v, E) => assy ya ((E, l @ [R], a,v,S,b),ss) e2
1.1329 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [R], a,v,S,b),ss) e2
1.1330 + | ay => ay)
1.1331 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
1.1332 + assy ya ((E,(l @ [L, R]),SOME a,v,S,b),ss) e
1.1333 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
1.1334 + assy ya ((E,(l @ [R]),a,v,S,b),ss) e
1.1335 + | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
1.1336 + (case assy (y,x,s,sc,AssOnly) ((E,(l @ [L, L, R]),SOME a,v,S,b),ss) e1 of
1.1337 + NasNap (v, E) =>
1.1338 + (case assy (y,x,s,sc,AssOnly) ((E,(l @ [L, R]),SOME a,v,S,b),ss) e2 of
1.1339 + NasNap (v, E) =>
1.1340 + (case assy (y,x,s,sc,AssGen) ((E,(l @ [L, L, R]),SOME a,v,S,b),ss) e1 of
1.1341 + NasNap (v, E) =>
1.1342 + assy (y,x,s,sc,AssGen) ((E, (l @ [L, R]), SOME a,v,S,b),ss) e2
1.1343 + | ay => ay)
1.1344 + | ay =>ay)
1.1345 + | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
1.1346 + | ay => (ay))
1.1347 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
1.1348 + (case assy ya ((E,(l @ [L, R]),a,v,S,b),ss) e1 of
1.1349 + NasNap (v, E) => assy ya ((E,(l @ [R]),a,v,S,b),ss) e2
1.1350 + | ay => (ay))
1.1351 + (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
1.1352 + | assy (thy',ctxt,sr,d,ap) ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss) t =
1.1353 + (case handle_leaf "locate" thy' sr E a v t of
1.1354 + (a', Expr _) =>
1.1355 + (NasNap (eval_listexpr_ (assoc_thy thy') sr
1.1356 + (subst_atomic (upd_env_opt E (a',v)) t), E))
1.1357 + | (a', STac stac) =>
1.1358 + let
1.1359 + val p' =
1.1360 + case p_ of Frm => p
1.1361 + | Res => lev_on p
1.1362 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
1.1363 + in
1.1364 + case assod pt d m stac of
1.1365 + Ass (m,v') =>
1.1366 + let val (p'',c',f',pt') =
1.1367 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.1368 + in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.1369 + | AssWeak (m,v') =>
1.1370 + let val (p'',c',f',pt') =
1.1371 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
1.1372 + in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.1373 + | NotAss =>
1.1374 + (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.1375 + AssOnly => (NasNap (v, E))
1.1376 + | _ =>
1.1377 + (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
1.1378 + Appl m' =>
1.1379 + let
1.1380 + val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
1.1381 + val (p'',c',f',pt') =
1.1382 + generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
1.1383 + in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.1384 + | Notappl _ => (NasNap (v, E))
1.1385 + )
1.1386 + )
1.1387 + end)
1.1388 + | assy _ (_, []) t = error ("assy: uncovered fun-def with " ^ term2str t);
1.1389
1.1390 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
1.1391 +fun ass_up (ys as (y,ctxt,s,Prog sc,d)) ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.1392 + let
1.1393 + val l = drop_last l; (*comes from e, goes to Abs*)
1.1394 + val (i, T, body) =
1.1395 + (case go l sc of
1.1396 + Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
1.1397 + | t => error ("ass_up..HOL.Let $ _ with " ^ term2str t))
1.1398 + val i = mk_Free (i, T);
1.1399 + val E = upd_env E (i, v);
1.1400 + in case assy (y,ctxt,s,d,Aundef) ((E, l @ [R, D], a,v,S,b),ss) body of
1.1401 + Assoc iss => Assoc iss
1.1402 + | NasApp iss => astep_up ys iss
1.1403 + | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss)
1.1404 + end
1.1405 + | ass_up ys iss (Abs (_,_,_)) = astep_up ys iss (*TODO 5.9.00: env ?*)
1.1406 + | ass_up ys iss (Const ("HOL.Let",_) $ _ $ (Abs _)) = astep_up ys iss (*TODO 5.9.00: env ?*)
1.1407 + | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
1.1408 + astep_up ysa iss (*all has been done in (*2*) below*)
1.1409 + | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.1410 + astep_up ysa iss (*2*: comes from e2*)
1.1411
1.1412 -(*assy, ass_up, astep_up scan for locate_gen in a script.
1.1413 - search is clearly separated into (1)-(2):
1.1414 - (1) assy is recursive descent;
1.1415 - (2) ass_up resumes interpretation at a location somewhere in the script;
1.1416 - astep_up does only get to the parentnode of the scriptexpr.
1.1417 - consequence:
1.1418 - * call of (2) means _always_ that in this branch below
1.1419 - there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
1.1420 -*)
1.1421 -fun assy ya (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
1.1422 - (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
1.1423 - NasApp ((E',l,a,v,S,bb),ss) =>
1.1424 - let
1.1425 - val id' = mk_Free (id, T);
1.1426 - val E' = upd_env E' (id', v);
1.1427 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.1428 - | NasNap (v,E) =>
1.1429 - let
1.1430 - val id' = mk_Free (id, T);
1.1431 - val E' = upd_env E (id', v);
1.1432 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
1.1433 - | ay => ay)
1.1434 -
1.1435 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
1.1436 - (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
1.1437 - then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
1.1438 - else NasNap (v, E))
1.1439 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
1.1440 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.1441 - then assy ya ((E, l@[R], a,v,S,b),ss) e
1.1442 - else NasNap (v, E))
1.1443 -
1.1444 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
1.1445 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
1.1446 - then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
1.1447 - else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
1.1448 -
1.1449 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
1.1450 - (case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.1451 - ay => ay)
1.1452 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
1.1453 - (case assy ya ((E, l@[R], a,v,S,b),ss) e of
1.1454 - ay => ay)
1.1455 -
1.1456 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
1.1457 - (case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
1.1458 - NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.1459 - | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
1.1460 - | ay => ay)
1.1461 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
1.1462 - (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
1.1463 - NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
1.1464 - | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[R], a,v,S,b),ss) e2
1.1465 - | ay => ay)
1.1466 -
1.1467 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
1.1468 - assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
1.1469 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
1.1470 - assy ya ((E,(l@[R]),a,v,S,b),ss) e
1.1471 -
1.1472 - | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
1.1473 - (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.1474 - NasNap (v, E) =>
1.1475 - (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
1.1476 - NasNap (v, E) =>
1.1477 - (case assy (y,x,s,sc,AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
1.1478 - NasNap (v, E) =>
1.1479 - assy (y,x,s,sc,AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
1.1480 - | ay => ay)
1.1481 - | ay =>(ay))
1.1482 - | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
1.1483 - | ay => (ay))
1.1484 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
1.1485 - (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
1.1486 - NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
1.1487 - | ay => (ay))
1.1488 -
1.1489 - (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
1.1490 - | assy (thy',ctxt,sr,d,ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
1.1491 - (case handle_leaf "locate" thy' sr E a v t of
1.1492 - (a', Expr s) =>
1.1493 - (NasNap (eval_listexpr_ (assoc_thy thy') sr
1.1494 - (subst_atomic (upd_env_opt E (a',v)) t), E))
1.1495 - | (a', STac stac) =>
1.1496 - let
1.1497 - val p' =
1.1498 - case p_ of Frm => p
1.1499 - | Res => lev_on p
1.1500 - | _ => error ("assy: call by " ^ pos'2str (p,p_));
1.1501 - in
1.1502 - case assod pt d m stac of
1.1503 - Ass (m,v') =>
1.1504 - let val (p'',c',f',pt') =
1.1505 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
1.1506 - in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
1.1507 - | AssWeak (m,v') =>
1.1508 - let val (p'',c',f',pt') =
1.1509 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
1.1510 - in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
1.1511 - | NotAss =>
1.1512 - (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
1.1513 - AssOnly => (NasNap (v, E))
1.1514 - | gen =>
1.1515 - (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
1.1516 - Appl m' =>
1.1517 - let
1.1518 - val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
1.1519 - val (p'',c',f',pt') =
1.1520 - generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
1.1521 - in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
1.1522 - | Notappl _ => (NasNap (v, E))
1.1523 - )
1.1524 - )
1.1525 - end);
1.1526 -
1.1527 -fun ass_up (ys as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
1.1528 - let
1.1529 - (*val _= tracing("### ass_up1 Let$e: is=")
1.1530 - val _= tracing(istate2str (ScrState is))*)
1.1531 - val l = drop_last l; (*comes from e, goes to Abs*)
1.1532 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
1.1533 - val i = mk_Free (i, T);
1.1534 - val E = upd_env E (i, v);
1.1535 - (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
1.1536 - in case assy (y,ctxt,s,d,Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
1.1537 - Assoc iss => Assoc iss
1.1538 - | NasApp iss => astep_up ys iss
1.1539 - | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
1.1540 -
1.1541 - | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
1.1542 - ((*tracing("### ass_up Abs: is=");
1.1543 - tracing(istate2str (ScrState is));*)
1.1544 - astep_up ys iss) (*TODO 5.9.00: env ?*)
1.1545 -
1.1546 - | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))=
1.1547 - ((*tracing("### ass_up Let $ e $ Abs: is=");
1.1548 - tracing(istate2str (ScrState is));*)
1.1549 - astep_up ys iss) (*TODO 5.9.00: env ?*)
1.1550 -
1.1551 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
1.1552 - astep_up ysa iss (*all has been done in (*2*) below*)
1.1553 -
1.1554 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
1.1555 - astep_up ysa iss (*2*: comes from e2*)
1.1556 -
1.1557 - | ass_up (ysa as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss)
1.1558 - (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
1.1559 - let
1.1560 - val up = drop_last l;
1.1561 - val Const ("Script.Seq",_) $ _ $ e2 = go up sc
1.1562 - (*val _= tracing("### ass_up Seq$e: is=")
1.1563 - val _= tracing(istate2str (ScrState is))*)
1.1564 - in
1.1565 - case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
1.1566 - NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
1.1567 - | NasApp iss => astep_up ysa iss
1.1568 - | ay => ay end
1.1569 -
1.1570 - | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
1.1571 - astep_up ysa iss
1.1572 -
1.1573 - (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
1.1574 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
1.1575 - *)
1.1576 - | ass_up ysa iss (Const ("Script.Try",_) $ e) =
1.1577 - ((*tracing("### ass_up Try $ e");*)
1.1578 - astep_up ysa iss)
1.1579 -
1.1580 + | ass_up (ysa as (y,ctxt,s,Prog sc,d)) ((E,l,a,v,S,b),ss)
1.1581 + (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
1.1582 + let
1.1583 + val up = drop_last l;
1.1584 + val e2 =
1.1585 + (case go up sc of
1.1586 + Const ("Script.Seq",_) $ _ $ e2 => e2
1.1587 + | t => error ("ass_up..Script.Seq $ _ with " ^ term2str t))
1.1588 + in case assy (y,ctxt,s,d,Aundef) ((E, up @ [R], a,v,S,b),ss) e2 of
1.1589 + NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
1.1590 + | NasApp iss => astep_up ysa iss
1.1591 + | ay => ay
1.1592 + end
1.1593 + | ass_up ysa iss (Const ("Script.Try",_) $ _ $ _) = astep_up ysa iss
1.1594 + | ass_up ysa iss (Const ("Script.Try",_) $ _) = astep_up ysa iss
1.1595 | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
1.1596 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
1.1597 - (t as Const ("Script.While",_) $ c $ e $ a) =
1.1598 - ((*tracing("### ass_up: While c= "^
1.1599 - (term2str (subst_atomic (upd_env E (a,v)) c)));*)
1.1600 - if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
1.1601 - then (case assy (y,ctxt,s,d,Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of
1.1602 - NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.1603 - | NasApp ((E',l,a,v,S,b),ss) =>
1.1604 - ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
1.1605 - | ay => ay)
1.1606 + (t as Const ("Script.While",_) $ c $ e $ a) =
1.1607 + if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
1.1608 + then case assy (y,ctxt,s,d,Aundef) ((E, l @ [L, R], SOME a,v,S,b),ss) e of
1.1609 + NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.1610 + | NasApp ((E',l,a,v,S,b),ss) =>
1.1611 + ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
1.1612 + | ay => ay
1.1613 else astep_up ys ((E,l, SOME a,v,S,b),ss)
1.1614 - )
1.1615 -
1.1616 | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
1.1617 (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*)
1.1618 - (t as Const ("Script.While",_) $ c $ e) =
1.1619 + (t as Const ("Script.While",_) $ c $ e) =
1.1620 if eval_true_ y s (subst_atomic (upd_env_opt E (a,v)) c)
1.1621 - then (case assy (y,ctxt,s,d,Aundef) ((E, l@[R], a,v,S,b),ss) e of
1.1622 + then case assy (y,ctxt,s,d,Aundef) ((E, l @ [R], a,v,S,b),ss) e of
1.1623 NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)
1.1624 | NasApp ((E',l,a,v,S,b),ss) =>
1.1625 ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
1.1626 + | ay => ay
1.1627 + else astep_up ys ((E,l, a,v,S,b),ss)
1.1628 + | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
1.1629 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
1.1630 + (t as Const ("Script.Repeat",_) $ e $ a) =
1.1631 + (case assy (y,ctxt,s,d, Aundef) ((E, (l @ [L, R]), SOME a,v,S,b),ss) e of
1.1632 + NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.1633 + | NasApp ((E',l,a,v,S,b),ss) =>
1.1634 + ass_up ys ((E',l,a,v,S,b),ss) t
1.1635 + | ay => ay)
1.1636 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
1.1637 + (t as Const ("Script.Repeat",_) $ e) =
1.1638 + (case assy (y,ctxt,s,d,Aundef) ((E, (l @ [R]), a,v,S,b),ss) e of
1.1639 + NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
1.1640 + | NasApp ((E',l,a,v',S,_),ss) => ass_up ys ((E',l,a,v',S,b),ss) t
1.1641 | ay => ay)
1.1642 - else astep_up ys ((E,l, a,v,S,b),ss)
1.1643 -
1.1644 - | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
1.1645 -
1.1646 - | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
1.1647 - (t as Const ("Script.Repeat",_) $ e $ a) =
1.1648 - (case assy (y,ctxt,s,d, Aundef) ((E, (l@[L,R]), SOME a,v,S,b),ss) e of
1.1649 - NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
1.1650 - | NasApp ((E',l,a,v,S,b),ss) =>
1.1651 - ass_up ys ((E',l,a,v,S,b),ss) t
1.1652 - | ay => ay)
1.1653 -
1.1654 - | ass_up (ys as (y,ctxt,s,_,d)) (is as ((E,l,a,v,S,b),ss))
1.1655 - (t as Const ("Script.Repeat",_) $ e) =
1.1656 - (case assy (y,ctxt,s,d,Aundef) ((E, (l@[R]), a,v,S,b),ss) e of
1.1657 - NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
1.1658 - | NasApp ((E',l,a,v',S,bb),ss) =>
1.1659 - ass_up ys ((E',l,a,v',S,b),ss) t
1.1660 - | ay => ay)
1.1661 -
1.1662 | ass_up y iss (Const ("Script.Or",_) $ _ $ _ $ _) = astep_up y iss
1.1663 -
1.1664 | ass_up y iss (Const ("Script.Or",_) $ _ $ _) = astep_up y iss
1.1665 -
1.1666 | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
1.1667 astep_up y ((E, (drop_last l), a,v,S,b),ss)
1.1668 -
1.1669 - | ass_up y iss t =
1.1670 - error ("ass_up not impl for t= "^(term2str t))
1.1671 -
1.1672 + | ass_up _ _ t =
1.1673 + error ("ass_up not impl for t= " ^ term2str t)
1.1674 and astep_up (ys as (_,_,_,Prog sc,_)) ((E,l,a,v,S,b),ss) =
1.1675 if 1 < length l
1.1676 - then
1.1677 - let val up = drop_last l;
1.1678 - (*val _= tracing("### astep_up: E= "^env2str E);*)
1.1679 - in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
1.1680 + then
1.1681 + let val up = drop_last l;
1.1682 + in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
1.1683 else (NasNap (v, E))
1.1684 -;
1.1685 -
1.1686 -
1.1687 -
1.1688 -
1.1689 -
1.1690 -(* use"ME/script.sml";
1.1691 - use"script.sml";
1.1692 - term2str (go up sc);
1.1693 -
1.1694 - *)
1.1695 + | astep_up _ ((_,l,_,_,_,_),_) = error ("astep_up: uncovered fun-def with " ^ loc_2str l)
1.1696
1.1697 (*check if there are tacs for rewriting only*)
1.1698 fun rew_only ([]:step list) = true
1.1699 @@ -1143,16 +764,13 @@
1.1700 | rew_only (((Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
1.1701 | rew_only (((End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
1.1702 | rew_only _ = false;
1.1703 -
1.1704
1.1705 datatype locate =
1.1706 - Steps of istate (*producing hd of step list (which was latest)
1.1707 - for next_tac, for reporting Safe|Unsafe to DG*)
1.1708 - * step (*(scrstate producing this step is in ptree !)*)
1.1709 - list (*locate_gen may produce intermediate steps*)
1.1710 -| NotLocatable; (*no (m Ass m') or (m AssWeak m') found*)
1.1711 -
1.1712 -
1.1713 + Steps of istate (* producing hd of step list (which was latest)
1.1714 + for next_tac, for reporting Safe|Unsafe to DG *)
1.1715 + * step (* (scrstate producing this step is in ptree !) *)
1.1716 + list (* locate_gen may produce intermediate steps *)
1.1717 +| NotLocatable; (* no (m Ass m') or (m AssWeak m') found *)
1.1718
1.1719 (* locate_gen tries to locate an input tac m in the script.
1.1720 pursuing this goal the script is executed until an (m' equiv m) is found,
1.1721 @@ -1174,57 +792,41 @@
1.1722 NOT IMPL. -- "error: do other step before"
1.1723 NotLocatable: thus generate_hard
1.1724 *)
1.1725 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
1.1726 - (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
1.1727 - (case lo rss f (Thm thm) of
1.1728 - [] => NotLocatable
1.1729 - | rts' =>
1.1730 - Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.1731 -
1.1732 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
1.1733 +fun locate_gen (thy', _) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
1.1734 + (Rfuns {locate_rule=lo,...}, _) (RrlsState (_,f'',rss,rts), _) =
1.1735 + (case lo rss f (Thm thm) of
1.1736 + [] => NotLocatable
1.1737 + | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
1.1738 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
1.1739 - (scr as Prog (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.1740 - let val thy = assoc_thy thy';
1.1741 - in
1.1742 - case if l = [] orelse ((*init.in solve..Apply_Method...*)
1.1743 - (last_elem o fst) p = 0 andalso snd p = Res)
1.1744 - then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.1745 - else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.1746 - Assoc (iss as (is as (_,_,_,_,_,strong_ass), ss as ((m',f',pt',p',c')::_))) =>
1.1747 - (if strong_ass
1.1748 - then
1.1749 - (Steps (ScrState is, ss))
1.1750 - else
1.1751 - if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
1.1752 - then
1.1753 - let
1.1754 - val (po,p_) = p
1.1755 - val po' = case p_ of Frm => po | Res => lev_on po
1.1756 - val (p'',c'',f'',pt'') =
1.1757 - generate1 thy m (ScrState is, ctxt) (po',p_) pt;
1.1758 - in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.1759 - else Steps (ScrState is, ss))
1.1760 -
1.1761 - | NasApp _ => NotLocatable
1.1762 - | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err) end
1.1763 -
1.1764 + (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
1.1765 + let val thy = assoc_thy thy';
1.1766 + in case if l = [] orelse (
1.1767 + (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
1.1768 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
1.1769 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
1.1770 + Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
1.1771 + (if strong_ass
1.1772 + then (Steps (ScrState is, ss))
1.1773 + else
1.1774 + if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
1.1775 + then
1.1776 + let
1.1777 + val (po,p_) = p
1.1778 + val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
1.1779 + val (p'',c'',f'',pt'') = generate1 thy m (ScrState is, ctxt) (po',p_) pt
1.1780 + in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
1.1781 + else Steps (ScrState is, ss))
1.1782 +
1.1783 + | NasApp _ => NotLocatable
1.1784 + | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err)
1.1785 + end
1.1786 | locate_gen _ m _ (sc,_) (is, _) =
1.1787 - error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
1.1788 - "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
1.1789 + error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
1.1790 + "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
1.1791
1.1792 (** find the next stactic in a script **)
1.1793
1.1794 -datatype appy = (*ExprVal in the sense of denotational semantics*)
1.1795 - Appy of (*applicable stac found, search stalled*)
1.1796 - tac_ * (*tac_ associated (fun assod) with stac*)
1.1797 - scrstate (*after determination of stac WN.18.8.03*)
1.1798 - | Napp of (*stac found was not applicable;
1.1799 - this mode may become Skip in Repeat, Try and Or*)
1.1800 - env (*stack*) (*popped while nxt_up*)
1.1801 - | Skip of (*for restart after Appy, for leaving iterations,
1.1802 - for passing the value of scriptexpressions,
1.1803 - and for finishing the script successfully*)
1.1804 - term * env (*stack*);
1.1805 -
1.1806 (*appy, nxt_up, nstep_up scanning for next_tac.
1.1807 search is clearly separated into (1)-(2):
1.1808 (1) appy is recursive descent;
1.1809 @@ -1234,210 +836,170 @@
1.1810 * call of (2) means _always_ that in this branch below
1.1811 there was an applicable stac (Repeat, Or e1, ...)
1.1812 *)
1.1813 +datatype appy = (* ExprVal in the sense of denotational semantics *)
1.1814 + Appy of (* applicable stac found, search stalled *)
1.1815 + tac_ * (* tac_ associated (fun assod) with stac *)
1.1816 + scrstate (* after determination of stac WN.18.8.03 *)
1.1817 + | Napp of (* stac found was not applicable;
1.1818 + this mode may become Skip in Repeat, Try and Or *)
1.1819 + env (*stack*)(* popped while nxt_up *)
1.1820 + | Skip of (* for restart after Appy, for leaving iterations,
1.1821 + for passing the value of scriptexpressions,
1.1822 + and for finishing the script successfully *)
1.1823 + term * env (*stack*);
1.1824
1.1825 +datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
1.1826 +(*Appy is only (final) returnvalue, not argument during search *)
1.1827 + Napp_ (* ev. detects 'script is not appropriate for this example' *)
1.1828 +| Skip_; (* detects 'script successfully finished'
1.1829 + also used as init-value for resuming; this works,
1.1830 + because 'nxt_up Or e1' treats as Appy *)
1.1831
1.1832 -datatype appy_ = (*as argument in nxt_up, nstep_up, from appy*)
1.1833 - (* Appy is only (final) returnvalue, not argument during search *)
1.1834 - Napp_ (*ev. detects 'script is not appropriate for this example'*)
1.1835 - | Skip_; (*detects 'script successfully finished'
1.1836 - also used as init-value for resuming; this works,
1.1837 - because 'nxt_up Or e1' treats as Appy*)
1.1838 -
1.1839 -fun appy thy ptp E l (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.1840 - (case appy thy ptp E (l@[L,R]) e a v of
1.1841 - Skip (res, E) =>
1.1842 - let val E' = upd_env E (Free (i,T), res);
1.1843 - in appy thy ptp E' (l@[R,D]) b a v end
1.1844 - | ay => ay)
1.1845 -
1.1846 - | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
1.1847 - (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
1.1848 - then appy thy ptp E (l@[L,R]) e (SOME a) v
1.1849 - else Skip (v, E))
1.1850 -
1.1851 - | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*2*),_) $ c $ e) a v =
1.1852 - (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1853 - then appy thy ptp E (l@[R]) e a v
1.1854 - else Skip (v, E))
1.1855 -
1.1856 - | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v =
1.1857 - (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1858 - then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
1.1859 - else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
1.1860 -
1.1861 +fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.1862 + (case appy thy ptp E (l @ [L, R]) e a v of
1.1863 + Skip (res, E) =>
1.1864 + let val E' = upd_env E (Free (i,T), res);
1.1865 + in appy thy ptp E' (l @ [R, D]) b a v end
1.1866 + | ay => ay)
1.1867 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
1.1868 + (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
1.1869 + then appy thy ptp E (l @ [L, R]) e (SOME a) v
1.1870 + else Skip (v, E))
1.1871 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
1.1872 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1873 + then appy thy ptp E (l @ [R]) e a v
1.1874 + else Skip (v, E))
1.1875 + | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =
1.1876 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1877 + then appy thy ptp E (l @ [L, R]) e1 a v
1.1878 + else appy thy ptp E (l @ [R]) e2 a v)
1.1879 | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
1.1880 - (appy thy ptp E (l@[L,R]) e (SOME a) v)
1.1881 -
1.1882 - | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v =
1.1883 - (appy thy ptp E (l@[R]) e a v)
1.1884 -
1.1885 - | appy thy ptp E l (t as Const ("Script.Try",_) $ e $ a) _ v =
1.1886 - (case appy thy ptp E (l@[L,R]) e (SOME a) v of
1.1887 - Napp E => (Skip (v, E))
1.1888 - | ay => ay)
1.1889 -
1.1890 - | appy thy ptp E l(t as Const ("Script.Try",_) $ e) a v =
1.1891 - (case appy thy ptp E (l@[R]) e a v of
1.1892 - Napp E => (Skip (v, E))
1.1893 - | ay => ay)
1.1894 -
1.1895 + appy thy ptp E (l @ [L, R]) e (SOME a) v
1.1896 + | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [R]) e a v
1.1897 + | appy thy ptp E l (Const ("Script.Try",_) $ e $ a) _ v =
1.1898 + (case appy thy ptp E (l @ [L, R]) e (SOME a) v of
1.1899 + Napp E => (Skip (v, E))
1.1900 + | ay => ay)
1.1901 + | appy thy ptp E l(Const ("Script.Try",_) $ e) a v =
1.1902 + (case appy thy ptp E (l @ [R]) e a v of
1.1903 + Napp E => (Skip (v, E))
1.1904 + | ay => ay)
1.1905 | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
1.1906 - (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.1907 - Appy lme => Appy lme
1.1908 - | _ => appy thy ptp E (*env*) (l@[L,R]) e2 (SOME a) v)
1.1909 -
1.1910 + (case appy thy ptp E (l @ [L, L, R]) e1 (SOME a) v of
1.1911 + Appy lme => Appy lme
1.1912 + | _ => appy thy ptp E (*env*) (l @ [L, R]) e2 (SOME a) v)
1.1913 | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
1.1914 - (case appy thy ptp E (l@[L,R]) e1 a v of
1.1915 - Appy lme => Appy lme
1.1916 - | _ => appy thy ptp E (l@[R]) e2 a v)
1.1917 -
1.1918 + (case appy thy ptp E (l @ [L, R]) e1 a v of
1.1919 + Appy lme => Appy lme
1.1920 + | _ => appy thy ptp E (l @ [R]) e2 a v)
1.1921 | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
1.1922 - (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
1.1923 - Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v
1.1924 - | ay => ay)
1.1925 -
1.1926 + (case appy thy ptp E (l @ [L, L, R]) e1 (SOME a) v of
1.1927 + Skip (v,E) => appy thy ptp E (l @ [L, R]) e2 (SOME a) v
1.1928 + | ay => ay)
1.1929 | appy thy ptp E l (Const ("Script.Seq",_) $ e1 $ e2) a v =
1.1930 - (case appy thy ptp E (l@[L,R]) e1 a v of
1.1931 - Skip (v,E) => appy thy ptp E (l@[R]) e2 a v
1.1932 - | ay => ay)
1.1933 -
1.1934 + (case appy thy ptp E (l @ [L,R]) e1 a v of
1.1935 + Skip (v,E) => appy thy ptp E (l @ [R]) e2 a v
1.1936 + | ay => ay)
1.1937 (* a leaf has been found *)
1.1938 - | appy (thy as (th,sr)) (pt, p) E l t a v =
1.1939 - (case handle_leaf "next " th sr E a v t of
1.1940 - (a', Expr s) => Skip (s, E)
1.1941 - | (a', STac stac) =>
1.1942 - let val (m,m') = stac2tac_ pt (assoc_thy th) stac
1.1943 - in
1.1944 - case m of
1.1945 - Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
1.1946 - | _ =>
1.1947 - (case applicable_in p pt m of
1.1948 - Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.1949 - | _ => ((*tracing("### appy: Napp");*)Napp E))
1.1950 - end);
1.1951 -
1.1952 -fun nxt_up thy ptp (scr as (Prog sc)) E l ay
1.1953 - (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
1.1954 - (if ay = Napp_
1.1955 - then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.1956 - else (*Skip_*)
1.1957 - let
1.1958 - val up = drop_last l;
1.1959 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
1.1960 - val i = mk_Free (i, T);
1.1961 - val E = upd_env E (i, v);
1.1962 - in
1.1963 - case appy thy ptp E (up@[R,D]) body a v of
1.1964 - Appy lre => Appy lre
1.1965 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.1966 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end)
1.1967 -
1.1968 - | nxt_up thy ptp scr E l ay
1.1969 - (t as Abs (_,_,_)) a v =
1.1970 - ((*tracing("### nxt_up Abs: " ^ term2str t);*)
1.1971 - nstep_up thy ptp scr E l ay a v)
1.1972 -
1.1973 - | nxt_up thy ptp scr E l ay
1.1974 - (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
1.1975 - ((*tracing("### nxt_up Let$e$Abs: is=");
1.1976 - tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
1.1977 - (*tracing("### nxt_up Let e Abs: " ^ term2str t);*)
1.1978 - nstep_up thy ptp scr E l ay a v)
1.1979 -
1.1980 - (*no appy_: never causes Napp -> Helpless*)
1.1981 - | nxt_up (thy as (th,sr)) ptp scr E l _
1.1982 - (Const ("Script.While"(*1*),_) $ c $ e $ _) a v =
1.1983 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1984 - then case appy thy ptp E (l@[L,R]) e a v of
1.1985 - Appy lr => Appy lr
1.1986 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.1987 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
1.1988 - else nstep_up thy ptp scr E l Skip_ a v
1.1989 -
1.1990 - (*no appy_: never causes Napp - Helpless*)
1.1991 - | nxt_up (thy as (th,sr)) ptp scr E l _
1.1992 - (Const ("Script.While"(*2*),_) $ c $ e) a v =
1.1993 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
1.1994 - then case appy thy ptp E (l@[R]) e a v of
1.1995 - Appy lr => Appy lr
1.1996 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.1997 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
1.1998 - else nstep_up thy ptp scr E l Skip_ a v
1.1999 -
1.2000 - | nxt_up thy ptp scr E l ay (Const ("If",_) $ _ $ _ $ _) a v =
1.2001 - nstep_up thy ptp scr E l ay a v
1.2002 -
1.2003 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
1.2004 - (Const ("Script.Repeat"(*1*),T) $ e $ _) a v =
1.2005 - (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[L,R]):loc_) e a v of
1.2006 - Appy lr => Appy lr
1.2007 - | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
1.2008 - nstep_up thy ptp scr E l Skip_ a v)
1.2009 - | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
1.2010 - (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
1.2011 - nstep_up thy ptp scr E l Skip_ a v))
1.2012 -
1.2013 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
1.2014 - (Const ("Script.Repeat"(*2*),T) $ e) a v =
1.2015 - (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[R]):loc_) e a v of
1.2016 - Appy lr => Appy lr
1.2017 - | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
1.2018 - nstep_up thy ptp scr E l Skip_ a v)
1.2019 - | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
1.2020 - (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
1.2021 - nstep_up thy ptp scr E l Skip_ a v))
1.2022 -
1.2023 - | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.2024 - (t as Const ("Script.Try",_) $ e $ _) a v =
1.2025 - ((*tracing("### nxt_up Try " ^ term2str t);*)
1.2026 - nstep_up thy ptp scr E l Skip_ a v )
1.2027 -
1.2028 - | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
1.2029 - (t as Const ("Script.Try"(*2*),_) $ e) a v =
1.2030 - ((*tracing("### nxt_up Try " ^ term2str t);*)
1.2031 - nstep_up thy ptp scr E l Skip_ a v)
1.2032 -
1.2033 -
1.2034 - | nxt_up thy ptp scr E l ay
1.2035 - (Const ("Script.Or",_) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
1.2036 -
1.2037 - | nxt_up thy ptp scr E l ay
1.2038 - (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
1.2039 -
1.2040 - | nxt_up thy ptp scr E l ay
1.2041 - (Const ("Script.Or",_) $ _ ) a v =
1.2042 - nstep_up thy ptp scr E (drop_last l) ay a v
1.2043 -
1.2044 - | nxt_up thy ptp scr E l ay (*all has been done in (*2*) below*)
1.2045 - (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
1.2046 - nstep_up thy ptp scr E l ay a v
1.2047 -
1.2048 - | nxt_up thy ptp scr E l ay (*comes from e2*)
1.2049 - (Const ("Script.Seq"(*2*),_) $ _ $ e2) a v =
1.2050 - nstep_up thy ptp scr E l ay a v
1.2051 -
1.2052 - | nxt_up thy ptp (scr as Prog sc) E l ay (*comes from e1*)
1.2053 - (Const ("Script.Seq",_) $ _) a v =
1.2054 + | appy ((th,sr)) (pt, p) E l t a v =
1.2055 + case handle_leaf "next " th sr E a v t of
1.2056 + (_, Expr s) => Skip (s, E)
1.2057 + | (a', STac stac) =>
1.2058 + let val (m,m') = stac2tac_ pt (assoc_thy th) stac
1.2059 + in case m of
1.2060 + Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
1.2061 + | _ =>
1.2062 + (case applicable_in p pt m of
1.2063 + Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
1.2064 + | _ => Napp E)
1.2065 + end
1.2066 +(*GOON*)
1.2067 +fun nxt_up thy ptp (scr as (Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
1.2068 if ay = Napp_
1.2069 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.2070 else (*Skip_*)
1.2071 - let val up = drop_last l;
1.2072 - val Const ("Script.Seq"(*2*),_) $ _ $ e2 = go up sc;
1.2073 - in case appy thy ptp E (up@[R]) e2 a v of
1.2074 + let
1.2075 + val up = drop_last l
1.2076 + val (i, T, body) =
1.2077 + (case go up sc of
1.2078 + Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
1.2079 + | t => error ("nxt_up..HOL.Let $ _ with " ^ term2str t))
1.2080 + val i = mk_Free (i, T)
1.2081 + val E = upd_env E (i, v)
1.2082 + in
1.2083 + case appy thy ptp E (up @ [R,D]) body a v of
1.2084 + Appy lre => Appy lre
1.2085 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.2086 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v
1.2087 + end
1.2088 + | nxt_up thy ptp scr E l ay (Abs _) a v = nstep_up thy ptp scr E l ay a v
1.2089 + | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =
1.2090 + nstep_up thy ptp scr E l ay a v
1.2091 + (*no appy_: never causes Napp -> Helpless*)
1.2092 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v =
1.2093 + if eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
1.2094 + then case appy thy ptp E (l @ [L,R]) e a v of
1.2095 + Appy lr => Appy lr
1.2096 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.2097 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
1.2098 + else nstep_up thy ptp scr E l Skip_ a v
1.2099 + (*no appy_: never causes Napp - Helpless*)
1.2100 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v =
1.2101 + if eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
1.2102 + then case appy thy ptp E (l @ [R]) e a v of
1.2103 Appy lr => Appy lr
1.2104 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.2105 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
1.2106 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.2107 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
1.2108 + else nstep_up thy ptp scr E l Skip_ a v
1.2109 + | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
1.2110 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
1.2111 + (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =
1.2112 + (case appy thy ptp (*upd_env*) E (*a,v)*) ((l @ [L, R]):loc_) e a v of
1.2113 + Appy lr => Appy lr
1.2114 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.2115 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
1.2116 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
1.2117 + (Const ("Script.Repeat"(*2*), _) $ e) a v =
1.2118 + (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [R]) e a v of
1.2119 + Appy lr => Appy lr
1.2120 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
1.2121 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
1.2122 + | nxt_up thy ptp scr E l _ (Const ("Script.Try",_) $ _ $ _) a v = (*makes Napp to Skip*)
1.2123 + nstep_up thy ptp scr E l Skip_ a v
1.2124
1.2125 - | nxt_up (thy,_) ptp scr E l ay t a v = error ("nxt_up not impl for " ^ term2str t)
1.2126 -
1.2127 + | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*), _) $ _) a v = (*makes Napp to Skip*)
1.2128 + nstep_up thy ptp scr E l Skip_ a v
1.2129 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =
1.2130 + nstep_up thy ptp scr E l ay a v
1.2131 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
1.2132 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
1.2133 + nstep_up thy ptp scr E (drop_last l) ay a v
1.2134 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
1.2135 + (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
1.2136 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
1.2137 + nstep_up thy ptp scr E l ay a v
1.2138 + | nxt_up thy ptp (scr as Prog sc) E l ay (Const ("Script.Seq",_) $ _) a v = (*comes from e1*)
1.2139 + if ay = Napp_
1.2140 + then nstep_up thy ptp scr E (drop_last l) Napp_ a v
1.2141 + else (*Skip_*)
1.2142 + let val up = drop_last l;
1.2143 + val e2 =
1.2144 + (case go up sc of
1.2145 + Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2
1.2146 + | t => error ("nxt_up..Script.Seq $ _ with " ^ term2str t))
1.2147 + in case appy thy ptp E (up @ [R]) e2 a v of
1.2148 + Appy lr => Appy lr
1.2149 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
1.2150 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
1.2151 + | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ term2str t)
1.2152 and nstep_up thy ptp (Prog sc) E l ay a v =
1.2153 - (if 1 < length l
1.2154 - then
1.2155 - let val up = drop_last l;
1.2156 - in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
1.2157 - else (*interpreted to end*)
1.2158 - if ay = Skip_ then Skip (v, E) else Napp E
1.2159 -);
1.2160 + if 1 < length l
1.2161 + then
1.2162 + let val up = drop_last l;
1.2163 + in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
1.2164 + else (*interpreted to end*)
1.2165 + if ay = Skip_ then Skip (v, E) else Napp E
1.2166 + | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ loc_2str l)
1.2167
1.2168 (* decide for the next applicable stac in the script;
1.2169 returns (stactic, value) - the value in case the script is finished
1.2170 @@ -1449,19 +1011,18 @@
1.2171 (.. not true for other details ..PrfObj ??????????????????
1.2172 20.8.02: do NOT return safe (is only changed in locate !!!)
1.2173 *)
1.2174 -fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
1.2175 +fun next_tac (thy,_) _ (Rfuns {next_rule, ...}) (RrlsState(f, f', rss, _), ctxt) =
1.2176 if f = f'
1.2177 then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
1.2178 (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
1.2179 else
1.2180 (case next_rule rss f of
1.2181 - NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.2182 - | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
1.2183 - (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
1.2184 - (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.2185 -
1.2186 - | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
1.2187 - (ScrState (E,l,a,v,s,b), ctxt) =
1.2188 + NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
1.2189 + | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
1.2190 + (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
1.2191 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
1.2192 + | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body))
1.2193 + (ScrState (E,l,a,v,s,_), ctxt) =
1.2194 (case if l = [] then appy thy ptp E [R] body NONE v
1.2195 else nstep_up thy ptp sc E l Skip_ a v of
1.2196 Skip (v, _) => (*finished*)
1.2197 @@ -1472,106 +1033,103 @@
1.2198 in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
1.2199 (e_istate, ctxt), (v,s))
1.2200 end
1.2201 - | (_, p', rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
1.2202 + | _ => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
1.2203 | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
1.2204 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
1.2205 -
1.2206 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
1.2207
1.2208 -
1.2209 (*.create the initial interpreter state from the items of the guard.*)
1.2210 +local
1.2211 val errmsg = "ERROR: found no actual arguments for prog. of "
1.2212 +fun msg_miss (sc, metID, formals, actuals) =
1.2213 + "ERROR in creating the environment for '" ^ id_of_scr sc ^
1.2214 + "' from \nthe items of the guard of " ^ metID2str metID ^ ",\n" ^
1.2215 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
1.2216 + (string_of_int o length) formals ^ " formals: " ^ terms2str formals ^ "\n" ^
1.2217 + (string_of_int o length) actuals ^ " actuals: " ^ terms2str actuals
1.2218 +fun msg_type (sc, metID, a, f, formals, actuals) =
1.2219 + "ERROR in creating the environment for '" ^
1.2220 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.2221 + metID2str metID ^ ",\n" ^
1.2222 + "different types of formal arg, from the script, " ^
1.2223 + "and actual arg, from the guards env:'\n" ^
1.2224 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
1.2225 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
1.2226 + "in\n" ^
1.2227 + "formals: " ^ terms2str formals ^ "\n" ^
1.2228 + "actuals: " ^ terms2str actuals
1.2229 +in
1.2230 fun init_scrstate thy itms metID =
1.2231 let
1.2232 val actuals = itms2args thy metID itms
1.2233 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
1.2234 - val scr as Prog sc = (#scr o get_met) metID
1.2235 + val (scr, sc) = (case (#scr o get_met) metID of
1.2236 + scr as Prog sc => (scr, sc) | _ => raise ERROR ("init_scrstate with " ^ metID2str metID))
1.2237 val formals = formal_args sc
1.2238 (*expects same sequence of (actual) args in itms and (formal) args in met*)
1.2239 fun relate_args env [] [] = env
1.2240 - | relate_args env _ [] =
1.2241 - error ("ERROR in creating the environment for '" ^
1.2242 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.2243 - metID2str metID ^ ",\n" ^
1.2244 - "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
1.2245 - (string_of_int o length) formals ^
1.2246 - " formals: " ^ terms2str formals ^ "\n" ^
1.2247 - (string_of_int o length) actuals ^
1.2248 - " actuals: " ^ terms2str actuals)
1.2249 - | relate_args env [] actual_finds = env (*may drop Find!*)
1.2250 + | relate_args _ _ [] = error (msg_miss (sc, metID, formals, actuals))
1.2251 + | relate_args env [] _ = env (*may drop Find!*)
1.2252 | relate_args env (a::aa) (f::ff) =
1.2253 - if type_of a = type_of f
1.2254 - then relate_args (env @ [(a, f)]) aa ff
1.2255 - else
1.2256 - error ("ERROR in creating the environment for '" ^
1.2257 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
1.2258 - metID2str metID ^ ",\n" ^
1.2259 - "different types of formal arg, from the script, " ^
1.2260 - "and actual arg, from the guards env:'\n" ^
1.2261 - "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
1.2262 - "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
1.2263 - "in\n" ^
1.2264 - "formals: " ^ terms2str formals ^ "\n" ^
1.2265 - "actuals: " ^ terms2str actuals)
1.2266 - val env = relate_args [] formals actuals;
1.2267 - val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
1.2268 - val {pre, prls, ...} = get_met metID;
1.2269 - val pres = check_preconds thy prls pre itms |> map snd;
1.2270 - val ctxt = ctxt |> insert_assumptions pres;
1.2271 - in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
1.2272 + if type_of a = type_of f
1.2273 + then relate_args (env @ [(a, f)]) aa ff
1.2274 + else error (msg_type (sc, metID, a, f, formals, actuals))
1.2275 + val env = relate_args [] formals actuals;
1.2276 + val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
1.2277 + val {pre, prls, ...} = get_met metID;
1.2278 + val pres = check_preconds thy prls pre itms |> map snd;
1.2279 + val ctxt = ctxt |> insert_assumptions pres;
1.2280 + in (ScrState (env, [], NONE, e_term, Safe, true), ctxt, scr) : istate * Proof.context * scr end;
1.2281 +end (*local*)
1.2282
1.2283 (* decide, where to get script/istate from:
1.2284 - (*1*) from PblObj.env: at begin of script if no init_form
1.2285 - (*2*) from PblObj/PrfObj: if stac is in the middle of the script
1.2286 - (*3*) from rls/PrfObj: in case of detail a ruleset *)
1.2287 -fun from_pblobj_or_detail' thy' (p,p_) pt =
1.2288 - let val ctxt = get_ctxt pt (p,p_)
1.2289 - in
1.2290 - if member op = [Pbl,Met] p_
1.2291 - then case get_obj g_env pt p of
1.2292 - NONE => error "from_pblobj_or_detail': no istate"
1.2293 - | SOME is =>
1.2294 - let
1.2295 - val metID = get_obj g_metID pt p
1.2296 - val {srls,...} = get_met metID
1.2297 - in (srls, is, (#scr o get_met) metID) end
1.2298 - else
1.2299 - let val (pbl,p',rls') = par_pbl_det pt p
1.2300 - in if pbl
1.2301 - then (*2*)
1.2302 - let
1.2303 - val thy = assoc_thy thy'
1.2304 - val PblObj{meth=itms,...} = get_obj I pt p'
1.2305 - val metID = get_obj g_metID pt p'
1.2306 - val {srls,...} = get_met metID
1.2307 - in (*if last_elem p = 0 nothing written to pt yet*)
1.2308 - (srls, get_loc pt (p,p_), (#scr o get_met) metID)
1.2309 - end
1.2310 - else (*3*)
1.2311 - (e_rls, (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*)
1.2312 - get_loc pt (p,p_),
1.2313 - case rls' of
1.2314 - Rls {scr=scr,...} => scr
1.2315 - | Seq {scr=scr,...} => scr
1.2316 - | Rrls {scr=rfuns,...} => rfuns)
1.2317 - end
1.2318 - end;
1.2319 + (* 1 *) from PblObj.env: at begin of script if no init_form
1.2320 + (* 2 *) from PblObj/PrfObj: if stac is in the middle of the script
1.2321 + (* 3 *) from rls/PrfObj: in case of detail a ruleset *)
1.2322 +fun from_pblobj_or_detail' _ (p, p_) pt =
1.2323 + if member op = [Pbl, Met] p_
1.2324 + then case get_obj g_env pt p of
1.2325 + NONE => error "from_pblobj_or_detail': no istate"
1.2326 + | SOME is =>
1.2327 + let
1.2328 + val metID = get_obj g_metID pt p
1.2329 + val {srls, ...} = get_met metID
1.2330 + in (srls, is, (#scr o get_met) metID) end
1.2331 + else
1.2332 + let val (pbl, p', rls') = par_pbl_det pt p
1.2333 + in if pbl
1.2334 + then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
1.2335 + let
1.2336 + val metID = get_obj g_metID pt p'
1.2337 + val {srls,...} = get_met metID
1.2338 + in (srls, get_loc pt (p,p_), (#scr o get_met) metID) end
1.2339 + else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *)
1.2340 + (e_rls, get_loc pt (p,p_),
1.2341 + case rls' of
1.2342 + Rls {scr = scr,...} => scr
1.2343 + | Seq {scr = scr,...} => scr
1.2344 + | Rrls {scr=rfuns,...} => rfuns
1.2345 + | Erls => error "from_pblobj_or_detail' with Erls")
1.2346 + end
1.2347
1.2348 -(*.get script and istate from PblObj, see (*1*) above.*)
1.2349 +(*.get script and istate from PblObj, see ( * 1 *)
1.2350 fun from_pblobj' thy' (p,p_) pt =
1.2351 let
1.2352 val p' = par_pblobj pt p
1.2353 val thy = assoc_thy thy'
1.2354 - val PblObj {meth=itms, ...} = get_obj I pt p'
1.2355 + val itms =
1.2356 + (case get_obj I pt p' of
1.2357 + PblObj {meth = itms, ...} => itms
1.2358 + | PrfObj _ => error "from_pblobj' NOT with PrfObj")
1.2359 val metID = get_obj g_metID pt p'
1.2360 - val {srls,scr,...} = get_met metID
1.2361 + val {srls, scr, ...} = get_met metID
1.2362 in
1.2363 if last_elem p = 0 (*nothing written to pt yet*)
1.2364 then
1.2365 let val (is, ctxt, scr) = init_scrstate thy itms metID
1.2366 in (srls, (is, ctxt), scr) end
1.2367 - else (srls, get_loc pt (p,p_), scr)
1.2368 - end;
1.2369 + else (srls, get_loc pt (p,p_), scr)
1.2370 + end;
1.2371
1.2372 (*.get the stactics and problems of a script as tacs
1.2373 instantiated with the current environment;
1.2374 @@ -1584,26 +1142,29 @@
1.2375 (*. fetch _all_ tactics from script .*)
1.2376 fun sel_rules _ (([],Res):pos') =
1.2377 raise PTREE "no tactics applicable at the end of a calculation"
1.2378 -| sel_rules pt (p,p_) =
1.2379 - if is_spec_pos p_
1.2380 - then [get_obj g_tac pt p]
1.2381 - else
1.2382 - let val pp = par_pblobj pt p;
1.2383 - val thy' = (get_obj g_domID pt pp):theory';
1.2384 - val thy = assoc_thy thy';
1.2385 - val metID = get_obj g_metID pt pp;
1.2386 - val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
1.2387 - else metID
1.2388 - val {scr = Prog sc,srls,...} = get_met metID'
1.2389 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
1.2390 - in map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.2391 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
1.2392 + | sel_rules pt (p,p_) =
1.2393 + if is_spec_pos p_
1.2394 + then [get_obj g_tac pt p]
1.2395 + else
1.2396 + let
1.2397 + val pp = par_pblobj pt p;
1.2398 + val thy' = (get_obj g_domID pt pp):theory';
1.2399 + val thy = assoc_thy thy';
1.2400 + val metID = get_obj g_metID pt pp;
1.2401 + val metID' = if metID =e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
1.2402 + val (sc, srls) = (case get_met metID' of
1.2403 + {scr = Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
1.2404 + val (env, a, v) = (case get_istate pt (p, p_) of
1.2405 + ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
1.2406 + in map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.2407 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
1.2408 + end;
1.2409
1.2410 (*. fetch tactics from script and filter _applicable_ tactics;
1.2411 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
1.2412 -fun sel_appl_atomic_tacs _ (([],Res):pos') =
1.2413 +fun sel_appl_atomic_tacs _ (([], Res) : pos') =
1.2414 raise PTREE "no tactics applicable at the end of a calculation"
1.2415 - | sel_appl_atomic_tacs pt (p,p_) =
1.2416 + | sel_appl_atomic_tacs pt (p, p_) =
1.2417 if is_spec_pos p_
1.2418 then [get_obj g_tac pt p]
1.2419 else
1.2420 @@ -1616,24 +1177,20 @@
1.2421 if metID = e_metID
1.2422 then (thd3 o snd3) (get_obj g_origin pt pp)
1.2423 else metID
1.2424 - val {scr = Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.2425 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
1.2426 + val (sc, srls, erls, ro) = (case get_met metID' of
1.2427 + {scr = Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
1.2428 + | _ => error "sel_appl_atomic_tacs 1")
1.2429 + val (env, a, v) = (case get_istate pt (p, p_) of
1.2430 + ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
1.2431 val alltacs = (*we expect at least 1 stac in a script*)
1.2432 map ((stac2tac pt thy) o rep_stacexpr o #2 o
1.2433 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
1.2434 val f =
1.2435 - case p_ of
1.2436 - Frm => get_obj g_form pt p
1.2437 - | Res => (fst o (get_obj g_result pt)) p
1.2438 + (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
1.2439 + | _ => error "")
1.2440 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
1.2441 in ((gen_distinct eq_tac) o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
1.2442 -
1.2443 -
1.2444 -(*
1.2445 +(**)
1.2446 end
1.2447 -open Interpreter;
1.2448 -*)
1.2449 -
1.2450 -(* use"ME/script.sml";
1.2451 - use"script.sml";
1.2452 - *)
1.2453 +(**)
1.2454 +(*open Lucin;*)