1.1 --- a/src/Tools/isac/Frontend/interface.sml Thu Oct 27 10:48:24 2016 +0200
1.2 +++ b/src/Tools/isac/Frontend/interface.sml Sat Nov 12 17:21:43 2016 +0100
1.3 @@ -256,7 +256,7 @@
1.4 *)
1.5 fun fetchApplicableTactics cI (scope:int) (p:pos') = (*---^^^*)
1.6 (let val ((pt, _), _) = get_calc cI
1.7 - in (applicabletacticsOK cI (sel_rules pt p))
1.8 + in (applicabletacticsOK cI (Lucin.sel_rules pt p))
1.9 handle PTREE str => sysERROR2xml cI str
1.10 end)
1.11 handle _ => sysERROR2xml cI "error in kernel 5";
2.1 --- a/src/Tools/isac/Interpret/inform.sml Thu Oct 27 10:48:24 2016 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Sat Nov 12 17:21:43 2016 +0100
2.3 @@ -524,10 +524,10 @@
2.4
2.5 fun mk_tacis ro erls (t, r as Thm (id, thm), (t', a)) =
2.6 (Rewrite (id, thm),
2.7 - Rewrite' ("Isac", fst ro, erls, false, rule2thm'' r, t, (t', a)),
2.8 + Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
2.9 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
2.10 | mk_tacis _ _ (t, r as Rls_ rls, (t', a)) =
2.11 - (Rewrite_Set (rule2rls' r),
2.12 + (Rewrite_Set (Lucin.rule2rls' r),
2.13 Rewrite_Set' ("Isac", false, rls, t, (t', a)),
2.14 (e_pos'(*to be updated before generate tacis!!!*), (Uistate, e_ctxt)))
2.15 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ rule2str r ^ " at " ^ term2str t);
3.1 --- a/src/Tools/isac/Interpret/script.sml Thu Oct 27 10:48:24 2016 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Nov 12 17:21:43 2016 +0100
3.3 @@ -5,296 +5,166 @@
3.4 10 20 30 40 50 60 70 80
3.5 *)
3.6
3.7 -signature INTERPRETER =
3.8 +signature LUCAS_INTERPRETER =
3.9 sig
3.10 - (*type ets (list of executed tactics) see sequent.sml*)
3.11
3.12 - datatype locate
3.13 - = NotLocatable
3.14 - | Steps of (tac_ * mout * ptree * pos' * cid * safe (* ets*)) list
3.15 -(* | ToDo of ets 28.4.02*)
3.16 -
3.17 - (*diss: next-tactic-function*)
3.18 - val next_tac : theory' -> ptree * pos' -> metID -> scr -> ets -> tac_
3.19 - (*diss: locate-function*)
3.20 - val locate_gen : theory'
3.21 - -> tac_
3.22 - -> ptree * pos' -> scr * rls -> ets -> loc_ -> locate
3.23 -
3.24 - val sel_rules : ptree -> pos' -> tac list
3.25 - val init_form : scr -> ets -> loc_ * term option (*FIXME not up to date*)
3.26 + type step = tac_ * mout * ptree * pos' * pos' list
3.27 + datatype locate = NotLocatable | Steps of istate * step list
3.28 +
3.29 + val next_tac : (*diss: next-tactic-function*)
3.30 + theory' * rls -> ptree * pos' -> scr -> istate * 'a -> tac_ * (istate * 'a) * (term * safe)
3.31 + val locate_gen : (*diss: locate-function*)
3.32 + theory' * rls -> tac_ -> ptree * pos' -> scr * 'a -> istate * Proof.context -> locate
3.33 + val sel_rules : ptree -> pos' -> tac list
3.34 + val init_form : 'a -> scr -> (term * term) list -> term option
3.35 val formal_args : term -> term list
3.36
3.37 - (*shift to library ...*)
3.38 - val inst_abs : theory' -> term -> term
3.39 - val itms2args : metID -> itm list -> term list
3.40 - val user_interrupt : loc_ * (tac_ * env * env * term * term * safe)
3.41 - (*val empty : term*)
3.42 + val tac_2tac : tac_ -> tac
3.43 + val init_scrstate : theory -> itm list -> metID -> istate * Proof.context * scr
3.44 + val from_pblobj' : theory' -> pos * pos_ -> ptree -> rls * (istate * Proof.context) * scr
3.45 + val from_pblobj_or_detail' : theory' -> pos * pos_ -> ptree ->
3.46 + rls * (istate * Proof.context) * scr
3.47 + val rule2thm'' : rule -> thm''
3.48 + val rule2rls' : rule -> string
3.49 +
3.50 + val itms2args : 'a -> metID -> itm list -> term list
3.51 end
3.52
3.53 -
3.54 -
3.55 -
3.56 -(*
3.57 -structure Interpreter : INTERPRETER =
3.58 +(**)
3.59 +structure Lucin: LUCAS_INTERPRETER(**) =
3.60 struct
3.61 -*)
3.62 -
3.63 -(*.traces the leaves (ie. non-tactical nodes) of the script
3.64 - found by next_tac.
3.65 - a leaf is either a tactic or an 'exp' in 'let v = expr'
3.66 - where 'exp' does not contain a tactic.*)
3.67 +(**)
3.68 +(* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)
3.69 val trace_script = Unsynchronized.ref false;
3.70
3.71 -type step = (*data for creating a new node in the ptree;
3.72 - designed for use:
3.73 - fun ass* scrstate steps =
3.74 - ... case ass* scrstate steps of
3.75 - Assoc (scrstate, steps) => ... ass* scrstate steps*)
3.76 - tac_ (*transformed from associated tac*)
3.77 - * mout (*result with indentation etc.*)
3.78 - * ptree (*containing node created by tac_ + resp. scrstate*)
3.79 - * pos' (*position in ptree; ptree * pos' is the proofstate*)
3.80 - * pos' list; (*of ptree-nodes probably cut (by fst tac_)*)
3.81 -val e_step = (Empty_Tac_, EmptyMout, EmptyPtree, e_pos',[]:pos' list):step;
3.82 +(* data for creating a new node in ctree; designed for use as:
3.83 + fun ass* scrstate steps = / ... case ass* scrstate steps of /
3.84 + Assoc (scrstate, steps) => ... ass* scrstate steps *)
3.85 +type step =
3.86 + tac_ (*transformed from associated tac *)
3.87 + * mout (*result with indentation etc. *)
3.88 + * ptree (*containing node created by tac_ + resp. scrstate *)
3.89 + * pos' (*position in ptree; ptree * pos' is the proofstate *)
3.90 + * pos' list; (*of ptree-nodes probably cut (by fst tac_) *)
3.91
3.92 fun rule2thm'' (Thm (id, thm)) = (id, thm) : thm''
3.93 - | rule2thm'' r = error ("rule2thm': not defined for "^(rule2str r));
3.94 + | rule2thm'' r = error ("rule2thm': not defined for " ^ rule2str r);
3.95 fun rule2rls' (Rls_ rls) = id_rls rls
3.96 - | rule2rls' r = error ("rule2rls': not defined for "^(rule2str r));
3.97 + | rule2rls' r = error ("rule2rls': not defined for " ^ rule2str r);
3.98
3.99 (*.makes a (rule,term) list to a Step (m, mout, pt', p', cid) for solve;
3.100 complicated with current t in rrlsstate.*)
3.101 -fun rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) [(r, (f', am))] =
3.102 +fun rts2steps steps ((pt, p), (f, f'', rss, rts), (thy', ro, er, pa)) [(r, (f', am))] =
3.103 let
3.104 val thy = assoc_thy thy'
3.105 val ctxt = get_ctxt pt p |> insert_assumptions am
3.106 val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
3.107 val is = RrlsState (f', f'', rss, rts)
3.108 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
3.109 + val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
3.110 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
3.111 in (is, (m, mout, pt', p', cid) :: steps) end
3.112 - | rts2steps steps ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) ((r, (f', am))::rts') =
3.113 + | rts2steps steps ((pt, p) ,(f, f'', rss, rts), (thy', ro, er, pa)) ((r, (f', am)) :: rts') =
3.114 let
3.115 val thy = assoc_thy thy'
3.116 val ctxt = get_ctxt pt p |> insert_assumptions am
3.117 - val m = Rewrite' (thy',ro,er,pa, rule2thm'' r, f, (f', am))
3.118 - val is = RrlsState (f',f'',rss,rts)
3.119 - val p = case p of (p',Frm) => p | (p',Res) => (lev_on p',Res)
3.120 + val m = Rewrite' (thy', ro, er, pa, rule2thm'' r, f, (f', am))
3.121 + val is = RrlsState (f', f'', rss, rts)
3.122 + val p = case p of (_, Frm) => p | (p', Res) => (lev_on p', Res) | _ => error "rts2steps: p1"
3.123 val (p', cid, mout, pt') = generate1 thy m (is, ctxt) p pt
3.124 in rts2steps ((m, mout, pt', p', cid)::steps)
3.125 - ((pt',p'),(f',f'',rss,rts),(thy',ro,er,pa)) rts' end;
3.126 + ((pt', p'), (f', f'', rss, rts), (thy', ro, er, pa)) rts'
3.127 + end
3.128 + | rts2steps _ _ _ = error "rts2steps: uncovered fun-def"
3.129
3.130 -(*. functions for the environment stack .*)
3.131 -fun accessenv id es = the (assoc((top es):env, id))
3.132 - handle _ => error ("accessenv: "^(free2str id)^" not in env");
3.133 -fun updateenv id vl (es:env stack) =
3.134 - (push (overwrite(top es, (id, vl))) (pop es)):env stack;
3.135 -fun pushenv id vl (es:env stack) =
3.136 - (push (overwrite(top es, (id, vl))) es):env stack;
3.137 -val popenv = pop:env stack -> env stack;
3.138 -
3.139 -
3.140 +(* functions for the environment stack: NOT YET IMPLEMENTED
3.141 +fun accessenv id es = the (assoc ((top es) : env, id))
3.142 + handle _ => error ("accessenv: " ^ free2str id ^ " not in env");
3.143 +fun updateenv id vl (es : env stack) =
3.144 + (push (overwrite(top es, (id, vl))) (pop es)) : env stack;
3.145 +fun pushenv id vl (es : env stack) =
3.146 + (push (overwrite(top es, (id, vl))) es) : env stack;
3.147 +val popenv = pop : env stack -> env stack;
3.148 +*)
3.149
3.150 fun de_esc_underscore str =
3.151 - let fun scan [] = []
3.152 - | scan (s::ss) = if s = "'" then (scan ss)
3.153 - else (s::(scan ss))
3.154 + let
3.155 + fun scan [] = []
3.156 + | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
3.157 in (implode o scan o Symbol.explode) str end;
3.158 -(*
3.159 -> val str = "Rewrite_Set_Inst";
3.160 -> val esc = esc_underscore str;
3.161 -val it = "Rewrite'_Set'_Inst" : string
3.162 -> val des = de_esc_underscore esc;
3.163 - val des = de_esc_underscore esc;*)
3.164
3.165 (*go at a location in a script and fetch the contents*)
3.166 fun go [] t = t
3.167 - | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
3.168 - | go (L::p) (t1 $ t2) = go p t1
3.169 - | go (R::p) (t1 $ t2) = go p t2
3.170 - | go l _ = error ("go: no "^(loc_2str l));
3.171 -(*
3.172 -> val t = (Thm.term_of o the o (parse thy)) "a+b";
3.173 -val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
3.174 -> val plus_a = go [L] t;
3.175 -> val b = go [R] t;
3.176 -> val plus = go [L,L] t;
3.177 -> val a = go [L,R] t;
3.178 -
3.179 -> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
3.180 -val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
3.181 -> val pl_pl_a_b = go [L] t;
3.182 -> val c = go [R] t;
3.183 -> val a = go [L,R,L,R] t;
3.184 -> val b = go [L,R,R] t;
3.185 -*)
3.186 -
3.187 -
3.188 -(* get a subterm t with test t, and record location *)
3.189 -fun get l test (t as Const (s,T)) =
3.190 - if test t then SOME (l,t) else NONE
3.191 - | get l test (t as Free (s,T)) =
3.192 - if test t then SOME (l,t) else NONE
3.193 - | get l test (t as Bound n) =
3.194 - if test t then SOME (l,t) else NONE
3.195 - | get l test (t as Var (s,T)) =
3.196 - if test t then SOME (l,t) else NONE
3.197 - | get l test (t as Abs (s,T,body)) =
3.198 - if test t then SOME (l:loc_,t) else get ((l@[D]):loc_) test body
3.199 - | get l test (t as t1 $ t2) =
3.200 - if test t then SOME (l,t)
3.201 - else case get (l@[L]) test t1 of
3.202 - NONE => get (l@[R]) test t2
3.203 - | SOME (l',t') => SOME (l',t');
3.204 -(*18.6.00
3.205 -> val sss = ((Thm.term_of o the o (parse thy))
3.206 - "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
3.207 - \ (let e_ = Try (Rewrite square_equation_left True eq_) \
3.208 - \ in [e_])");
3.209 - ______ compares head_of !!
3.210 -> get [] (eq_str "HOL.Let") sss; [R]
3.211 -> get [] (eq_str "Script.Try") sss; [R,L,R]
3.212 -> get [] (eq_str "Script.Rewrite") sss; [R,L,R,R]
3.213 -> get [] (eq_str "HOL.True") sss; [R,L,R,R,L,R]
3.214 -> get [] (eq_str "e_") sss; [R,R]
3.215 -*)
3.216 + | go (D::p) (Abs(_, _, t0)) = go (p : loc_) t0
3.217 + | go (L::p) (t1 $ _) = go p t1
3.218 + | go (R::p) (_ $ t2) = go p t2
3.219 + | go l _ = error ("go: no " ^ loc_2str l);
3.220
3.221 (*.get argument of first stactic in a script for init_form.*)
3.222 -fun get_stac thy (h $ body) =
3.223 +fun get_stac thy (_ $ body) =
3.224 let
3.225 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
3.226 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.227 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.228 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
3.229 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.230 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.231 | get_t y (Const ("Script.Try",_) $ e) a = get_t y e a
3.232 | get_t y (Const ("Script.Try",_) $ e $ a) _ = get_t y e a
3.233 | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
3.234 | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
3.235 | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
3.236 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.237 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.238 | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
3.239 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.240 - | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
3.241 - | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
3.242 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
3.243 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.244 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.245 + | get_t y (Const ("Script.While",_) $ _ $ e) a = get_t y e a
3.246 + | get_t y (Const ("Script.While",_) $ _ $ e $ a) _ = get_t y e a
3.247 + | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
3.248 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.249 (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
3.250 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.251 + (case get_t y e1 a of NONE => get_t y e2 a | la => la)
3.252 | get_t y (Abs (_,_,e)) a = get_t y e a*)
3.253 - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
3.254 + | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
3.255 get_t y e1 a (*don't go deeper without evaluation !*)
3.256 - | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
3.257 + | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
3.258 (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
3.259
3.260 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
3.261 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
3.262 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
3.263 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
3.264 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
3.265 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
3.266 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
3.267 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
3.268 - | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
3.269 - | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a
3.270 + | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
3.271 + | get_t _ (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
3.272 + | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
3.273 + | get_t _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
3.274 + | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ = SOME a
3.275 + | get_t _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a = SOME a
3.276 + | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
3.277 + | get_t _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
3.278 + | get_t _ (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
3.279 + | get_t _ (Const ("Script.Calculate",_) $ _ ) a = SOME a
3.280
3.281 - | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
3.282 - | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a
3.283 + | get_t _ (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
3.284 + | get_t _ (Const ("Script.Substitute",_) $ _ ) a = SOME a
3.285
3.286 - | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
3.287 + | get_t _ (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
3.288
3.289 - | get_t y x _ =
3.290 - ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
3.291 - NONE)
3.292 -in get_t thy body e_term end;
3.293 + | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
3.294 + in get_t thy body e_term end
3.295 + | get_stac _ t = error ("get_stac: no fun-def. for " ^ term2str t);
3.296
3.297 fun init_form thy (Prog sc) env =
3.298 - (case get_stac thy sc of
3.299 - NONE => NONE
3.300 - | SOME stac => SOME (subst_atomic env stac))
3.301 + (case get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
3.302 | init_form _ _ _ = error "init_form: no match";
3.303
3.304 -(*the 'iteration-argument' of a stac (args not eval)*)
3.305 -fun itr_arg _ (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ v) = v
3.306 - | itr_arg _ (Const ("Script.Rewrite",_) $ _ $ _ $ v) = v
3.307 - | itr_arg _ (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $ v) = v
3.308 - | itr_arg _ (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ v) = v
3.309 - | itr_arg _ (Const ("Script.Calculate",_) $ _ $ v) = v
3.310 - | itr_arg _ (Const ("Script.Check'_elementwise",_) $ consts $ _) = consts
3.311 - | itr_arg _ (Const ("Script.Or'_to'_List",_) $ _) = e_term
3.312 - | itr_arg _ (Const ("Script.Tac",_) $ _) = e_term
3.313 - | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
3.314 - | itr_arg thy t = error ("itr_arg not impl. for " ^ term_to_string'' thy t);
3.315 -(* val t = (Thm.term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
3.316 -> itr_arg "Script" t;
3.317 -val it = Free ("e_","RealDef.real") : term
3.318 -> val t = (Thm.term_of o the o (parse thy))"xxx";
3.319 -> itr_arg "Script" t;
3.320 -*** itr_arg not impl. for xxx
3.321 -uncaught exception ERROR
3.322 - raised at: library.ML:1114.35-1114.40*)
3.323 +(* get the arguments of the script out of the scripts parsetree *)
3.324 +fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
3.325
3.326 -
3.327 -(*.get the arguments of the script out of the scripts parsetree.*)
3.328 -fun formal_args scr = (fst o split_last o snd o strip_comb) scr;
3.329 -(*
3.330 -> formal_args scr;
3.331 - [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
3.332 - Free ("eqs_","bool List.list")] : term list
3.333 -*)
3.334 -
3.335 -(*.get the identifier of the script out of the scripts parsetree.*)
3.336 +(* get the identifier of the script out of the scripts parsetree *)
3.337 fun id_of_scr sc = (id_of o fst o strip_comb) sc;
3.338
3.339 -(*WN020526: not clear, when a is available in ass_up for eva-_true*)
3.340 +(*WN020526: not clear, when a is available in ass_up for eval_true*)
3.341 (*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
3.342 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
3.343 thus "NONE" must be set at the end of currying (ill designed anyway)*)
3.344 -fun upd_env_opt env (SOME a, v) = upd_env env (a,v)
3.345 - | upd_env_opt env (NONE, v) =
3.346 - (tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")"); env);
3.347 +fun upd_env_opt env (SOME a, v) = upd_env env (a, v)
3.348 + | upd_env_opt env (NONE, _) =
3.349 + ((*tracing ("*** upd_env_opt: (NONE," ^ term2str v ^ ")");*) env);
3.350
3.351 -type dsc = typ; (*<-> nam..unknow in Descript.thy*)
3.352 -fun typ_str (Type (s,_)) = s
3.353 - | typ_str (TFree(s,_)) = s
3.354 - | typ_str (TVar ((s,i),_)) = s ^ (string_of_int i);
3.355 -
3.356 -(*get the _result_-type of a description*)
3.357 -fun dsc_valT (Const (_,(Type (_,[_,T])))) = (strip_thy o typ_str) T;
3.358 -(*> val t = (Thm.term_of o the o (parse thy)) "equality";
3.359 -> val T = type_of t;
3.360 -val T = "bool => Tools.una" : typ
3.361 -> val dsc = dsc_valT t;
3.362 -val dsc = "una" : string
3.363 -
3.364 -> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
3.365 -> val T = type_of t;
3.366 -val T = "bool List.list => Tools.nam" : typ
3.367 -> val dsc = dsc_valT t;
3.368 -val dsc = "nam" : string*)
3.369 -
3.370 -(*.from penv in itm_ make args for script depending on type of description.*)
3.371 -(*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
3.372 - 9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
3.373 -fun mk_arg thy d [] =
3.374 - error ("mk_arg: no data for " ^ term_to_string''' thy d)
3.375 - | mk_arg thy d [t] =
3.376 - (case dsc_valT d of
3.377 - "una" => [t]
3.378 - | "nam" =>
3.379 - [case t of
3.380 - r as (Const ("HOL.eq",_) $ _ $ _) => r
3.381 - | _ => error ("mk_arg: dsc-typ 'nam' applied to non-equality " ^ term_to_string''' thy t)]
3.382 - | s => error ("mk_arg: not impl. for "^s))
3.383 - | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
3.384 -(*
3.385 - val d = d_in itm_;
3.386 - val [t] = ts_in itm_;
3.387 -mk_arg thy
3.388 -*)
3.389 -
3.390 -
3.391 -
3.392 +type dsc = typ; (* <-> nam..unknow in Descript.thy *)
3.393
3.394 (*.create the actual parameters (args) of script: their order
3.395 is given by the order in met.pat .*)
3.396 @@ -303,140 +173,93 @@
3.397 !: FIXXXME penv: push it here in itms2args into script-evaluation*)
3.398 (* val (thy, mI, itms) = (thy, metID, itms);
3.399 *)
3.400 -val errmsg =
3.401 - "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
3.402 -fun itms2args thy mI (itms:itm list) =
3.403 - let val mvat = max_vt itms
3.404 - fun okv mvat (_,vats,b,_,_) = member op = vats mvat andalso b
3.405 - val itms = filter (okv mvat) itms
3.406 - fun test_dsc d (_,_,_,_,itm_) = (d = d_in itm_)
3.407 - fun itm2arg itms (_,(d,_)) =
3.408 - case find_first (test_dsc d) itms of
3.409 - NONE =>
3.410 - error ("itms2args: '"^term2str d^"' not in itms")
3.411 - (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
3.412 - penv postponed; presently penv holds already env for script*)
3.413 - | SOME (_,_,_,_,itm_) => penvval_in itm_
3.414 - fun sel_given_find (s,_) = (s = "#Given") orelse (s = "#Find")
3.415 - val pats = (#ppc o get_met) mI
3.416 - val _ = if pats = [] then raise ERROR errmsg else ()
3.417 - in (flat o (map (itm2arg itms))) pats end;
3.418 -(*
3.419 -> val sc = ... Solve_root_equation ...
3.420 -> val mI = ("Script","sqrt-equ-test");
3.421 -> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
3.422 -> val ts = itms2args thy mI itms;
3.423 -> map (term_to_string''' thy) ts;
3.424 -["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
3.425 -*)
3.426 +val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
3.427 +fun itms2args _ mI (itms : itm list) =
3.428 + let
3.429 + val mvat = max_vt itms
3.430 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
3.431 + val itms = filter (okv mvat) itms
3.432 + fun test_dsc d (_, _, _, _, itm_) = (d = d_in itm_)
3.433 + fun itm2arg itms (_,(d,_)) =
3.434 + case find_first (test_dsc d) itms of
3.435 + NONE => error ("itms2args: '" ^ term2str d ^ "' not in itms")
3.436 + | SOME (_, _, _, _, itm_) => penvval_in itm_
3.437 + (*| SOME (_,_,_,_,itm_) => mk_arg thy (d_in itm_) (ts_in itm_);
3.438 + penv postponed; presently penv holds already env for script*)
3.439 + val pats = (#ppc o get_met) mI
3.440 + val _ = if pats = [] then raise ERROR errmsg else ()
3.441 + in (flat o (map (itm2arg itms))) pats end;
3.442
3.443 -
3.444 -(*detour necessary, because generate1 delivers a string-result*)
3.445 -fun mout2term thy (Form' (FormKF (_,_,_,_,res))) =
3.446 - (Thm.term_of o the o (parse (assoc_thy thy))) res
3.447 - | mout2term thy (Form' (PpcKF _)) = e_term;(*3.8.01: res of subpbl
3.448 - at time of detection in script*)
3.449 -
3.450 -(*.convert a script-tac 'stac' to a tactic 'tac'; if stac is an initac,
3.451 - then convert to a 'tac_' (as required in appy).
3.452 - arg pt:ptree for pushing the thy specified in rootpbl into subpbls.*)
3.453 -fun stac2tac_ _ thy (Const ("Script.Rewrite",_) $ Free (thmID,_) $ _ $ _) =
3.454 - let
3.455 - val tid = (de_esc_underscore o strip_thy) thmID
3.456 - in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_)
3.457 - end
3.458 -
3.459 - | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst",_) $ sub $ Free (thmID,_) $ _ $ _) =
3.460 - let
3.461 - val subML = ((map isapair2pair) o isalist2list) sub
3.462 - val subStr = subst2subs subML
3.463 - val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
3.464 - in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
3.465 -
3.466 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set",_) $ Free (rls,_) $ _ $ f) =
3.467 - (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
3.468 -
3.469 - | stac2tac_ pt thy (Const ("Script.Rewrite'_Set'_Inst",_) $ sub $ Free (rls,_) $ _ $ f) =
3.470 - let
3.471 - val subML = ((map isapair2pair) o isalist2list) sub;
3.472 - val subStr = subst2subs subML;
3.473 - in (Rewrite_Set_Inst (subStr,rls), Empty_Tac_) end
3.474 -
3.475 - | stac2tac_ pt thy (Const ("Script.Calculate",_) $ Free (op_,_) $ f) =
3.476 - (Calculate op_, Empty_Tac_)
3.477 -
3.478 - | stac2tac_ pt thy (Const ("Script.Take",_) $ t) =
3.479 - (Take (term2str t), Empty_Tac_)
3.480 -
3.481 - | stac2tac_ pt thy (Const ("Script.Substitute",_) $ isasub $ arg) =
3.482 - (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
3.483 -
3.484 - | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $
3.485 - (set as Const ("Set.Collect",_) $ Abs (_,_,pred))) =
3.486 - (Check_elementwise (term_to_string''' thy pred), (*set*)Empty_Tac_)
3.487 -
3.488 - | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) =
3.489 - (Or_to_List, Empty_Tac_)
3.490 -
3.491 - (*12.1.01.for subproblem_equation_dummy in root-equation *)
3.492 - | stac2tac_ pt thy (Const ("Script.Tac",_) $ Free (str,_)) =
3.493 - (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
3.494 +(* convert a script-tac 'stac' to a tactic 'tac';
3.495 + if stac is an initac, then convert to a 'tac_' (as required in appy).
3.496 + arg ptree for pushing the thy specified in rootpbl into subpbls *)
3.497 +fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ Free (thmID, _) $ _ $ _) =
3.498 + let
3.499 + val tid = (de_esc_underscore o strip_thy) thmID
3.500 + in (Rewrite (tid, assoc_thm'' thy tid), Empty_Tac_) end
3.501 + | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ Free (thmID, _) $ _ $ _) =
3.502 + let
3.503 + val subML = ((map isapair2pair) o isalist2list) sub
3.504 + val subStr = subst2subs subML
3.505 + val tid = (de_esc_underscore o strip_thy) thmID (*4.10.02 unnoetig*)
3.506 + in (Rewrite_Inst (subStr, (tid, assoc_thm'' thy tid)), Empty_Tac_) end
3.507 + | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ Free (rls, _) $ _ $ _) =
3.508 + (Rewrite_Set ((de_esc_underscore o strip_thy) rls), Empty_Tac_)
3.509 + | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ Free (rls, _) $ _ $ _) =
3.510 + let
3.511 + val subML = ((map isapair2pair) o isalist2list) sub;
3.512 + val subStr = subst2subs subML;
3.513 + in (Rewrite_Set_Inst (subStr, rls), Empty_Tac_) end
3.514 + | stac2tac_ _ _ (Const ("Script.Calculate", _) $ Free (op_, _) $ _) = (Calculate op_, Empty_Tac_)
3.515 + | stac2tac_ _ _ (Const ("Script.Take", _) $ t) = (Take (term2str t), Empty_Tac_)
3.516 + | stac2tac_ _ _ (Const ("Script.Substitute", _) $ isasub $ _) =
3.517 + (Substitute ((subte2sube o isalist2list) isasub), Empty_Tac_)
3.518 + | stac2tac_ _ thy (Const("Script.Check'_elementwise", _) $ _ $
3.519 + (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
3.520 + (Check_elementwise (term_to_string''' thy pred), Empty_Tac_)
3.521 + | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Or_to_List, Empty_Tac_)
3.522 + | stac2tac_ _ _ (Const ("Script.Tac", _) $ Free (str, _)) =
3.523 + (Tac ((de_esc_underscore o strip_thy) str), Empty_Tac_)
3.524
3.525 (*compare "| assod _ (Subproblem'"*)
3.526 - | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
3.527 - (Const ("Product_Type.Pair",_) $Free (dI',_) $
3.528 - (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
3.529 - let
3.530 - val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
3.531 - val thy = maxthy (assoc_thy dI) (rootthy pt);
3.532 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
3.533 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
3.534 - val ags = isalist2list ags';
3.535 - val (pI, pors, mI) =
3.536 - if mI = ["no_met"]
3.537 - then
3.538 - let
3.539 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
3.540 - handle ERROR "actual args do not match formal args"
3.541 - => (match_ags_msg pI stac ags(*raise exn*); [])
3.542 - val pI' = refine_ori' pors pI;
3.543 - in (pI', pors (*refinement over models with diff.prec only*),
3.544 - (hd o #met o get_pbt) pI') end
3.545 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
3.546 - handle ERROR "actual args do not match formal args"
3.547 - => (match_ags_msg pI stac ags(*raise exn*); []), mI);
3.548 - val (fmz_, vals) = oris2fmz_vals pors;
3.549 - val {cas,ppc,thy,...} = get_pbt pI
3.550 - val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
3.551 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
3.552 - val ctxt = Proof_Context.init_global
3.553 - val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
3.554 - |> declare_constraints' vals
3.555 - val hdl =
3.556 - case cas of
3.557 - NONE => pblterm dI pI
3.558 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
3.559 - val f = subpbl (strip_thy dI) pI
3.560 - in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
3.561 - end
3.562 - | stac2tac_ pt thy t = error
3.563 - ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
3.564 + | stac2tac_ pt _ (stac as Const ("Script.SubProblem",_) $
3.565 + (Const ("Product_Type.Pair",_) $Free (dI', _) $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $
3.566 + ags') =
3.567 + let
3.568 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
3.569 + val thy = maxthy (assoc_thy dI) (rootthy pt);
3.570 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
3.571 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
3.572 + val ags = isalist2list ags';
3.573 + val (pI, pors, mI) =
3.574 + if mI = ["no_met"]
3.575 + then
3.576 + let
3.577 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
3.578 + handle ERROR "actual args do not match formal args"
3.579 + => (match_ags_msg pI stac ags(*raise exn*); [])
3.580 + val pI' = refine_ori' pors pI;
3.581 + in (pI', pors (* refinement over models with diff.prec only *),
3.582 + (hd o #met o get_pbt) pI') end
3.583 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
3.584 + handle ERROR "actual args do not match formal args"
3.585 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
3.586 + val (fmz_, vals) = oris2fmz_vals pors;
3.587 + val {cas,ppc,thy,...} = get_pbt pI
3.588 + val dI = theory2theory' thy (*.take dI from _refined_ pbl.*)
3.589 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt));
3.590 + val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
3.591 + val hdl =
3.592 + case cas of
3.593 + NONE => pblterm dI pI
3.594 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
3.595 + val f = subpbl (strip_thy dI) pI
3.596 + in (Subproblem (dI, pI), Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
3.597 + end
3.598 + | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ term_to_string''' thy t);
3.599
3.600 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
3.601
3.602 -(*test a term for being a _list_ (set ?) of constants; could be more rigorous*)
3.603 -fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
3.604 - | list_of_consts (Const ("List.list.Nil",_)) = true
3.605 - | list_of_consts _ = false;
3.606 -(*val ttt = (Thm.term_of o the o (parse thy)) "[x=#1,x=#2,x=#3]";
3.607 -> list_of_consts ttt;
3.608 -val it = true : bool
3.609 -> val ttt = (Thm.term_of o the o (parse thy)) "[]";
3.610 -> list_of_consts ttt;
3.611 -val it = true : bool*)
3.612 -
3.613 -
3.614 -
3.615 datatype ass =
3.616 Ass of
3.617 tac_ * (* SubProblem gets args instantiated in assod *)
3.618 @@ -461,378 +284,227 @@
3.619 AssWeak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
3.620 NotAss : e.g. thmID in stac/=/thmID in m (not =)
3.621 *)
3.622 -fun assod pt d (m as Rewrite_Inst' (thy', rod, rls, put, subs, thm'' as (thmID, _), f, (f', asm))) stac =
3.623 +fun assod _ _ (m as Rewrite_Inst' (_, _, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
3.624 (case stac of
3.625 - (Const ("Script.Rewrite'_Inst",_) $ subs_ $ Free (thmID_,idT) $b$f_) =>
3.626 - if thmID = thmID_
3.627 - then
3.628 - if f = f_
3.629 - then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
3.630 - else ((*tracing"3### assod ..AssWeak";*)AssWeak(m, f'))
3.631 - else ((*tracing"3### assod ..NotAss";*)NotAss)
3.632 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $_$f_) =>
3.633 - if contains_rule (Thm thm'') (assoc_rls rls_)
3.634 - then
3.635 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.636 - else NotAss
3.637 - | _ => NotAss)
3.638 - | assod pt d (m as Rewrite' (thy, rod, rls, put, thm'' as (thmID, _), f, (f', asm))) stac =
3.639 + (Const ("Script.Rewrite'_Inst", _) $ _ $ Free (thmID_, _) $ _ $ f_) =>
3.640 + if thmID = thmID_
3.641 + then
3.642 + if f = f_
3.643 + then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
3.644 + else ((*tracing"3### assod ..AssWeak";*) AssWeak(m, f'))
3.645 + else ((*tracing"3### assod ..NotAss";*) NotAss)
3.646 + | (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ Free (rls_, _) $ _ $ f_) =>
3.647 + if contains_rule (Thm thm'') (assoc_rls rls_)
3.648 + then if f = f_ then Ass (m,f') else AssWeak (m,f')
3.649 + else NotAss
3.650 + | _ => NotAss)
3.651 + | assod _ _ (m as Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', _))) stac =
3.652 (case stac of
3.653 - (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
3.654 - ((*tracing ("3### assod: stac = " ^ ter2str t);
3.655 - tracing ("3### assod: f(m)= " ^ term2str f);*)
3.656 - if thmID = thmID_
3.657 - then
3.658 - if f = f_
3.659 - then ((*tracing"3### assod ..Ass";*)Ass (m,f'))
3.660 - else
3.661 - ((*tracing"### assod ..AssWeak";
3.662 - tracing("### assod: f(m) = " ^ term2str f);
3.663 - tracing("### assod: f(stac)= " ^ term2str f_)*)
3.664 - AssWeak (m,f'))
3.665 - else ((*tracing"3### assod ..NotAss";*)NotAss))
3.666 - | (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =>
3.667 - if contains_rule (Thm thm'') (assoc_rls rls_)
3.668 - then
3.669 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.670 - else NotAss
3.671 - | _ => NotAss)
3.672 -
3.673 - | assod pt d (m as Rewrite_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
3.674 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
3.675 - if id_rls rls = rls_
3.676 - then
3.677 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.678 - else NotAss
3.679 -
3.680 - | assod pt d (m as Detail_Set_Inst' (thy',put,sub,rls,f,(f',asm)))
3.681 - (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free (rls_,_) $ _ $ f_) =
3.682 - if id_rls rls = rls_
3.683 - then
3.684 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.685 - else NotAss
3.686 -
3.687 - | assod pt d (m as Rewrite_Set' (thy,put,rls,f,(f',asm)))
3.688 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
3.689 - if id_rls rls = rls_
3.690 - then
3.691 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.692 - else NotAss
3.693 -
3.694 - | assod pt d (m as Detail_Set' (thy,put,rls,f,(f',asm)))
3.695 - (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
3.696 - if id_rls rls = rls_
3.697 - then
3.698 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.699 - else NotAss
3.700 -
3.701 - | assod pt d (m as Calculate' (thy',op_,f,(f',thm'))) stac =
3.702 - (case stac of
3.703 - (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
3.704 - if op_ = op__
3.705 - then
3.706 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.707 - else NotAss
3.708 - | (Const ("Script.Rewrite'_Set'_Inst",_) $ sub_ $ Free(rls_,_) $_$f_) =>
3.709 - let
3.710 - val thy = assoc_thy "Isac";
3.711 - in
3.712 - if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
3.713 - then
3.714 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.715 - else NotAss
3.716 - end
3.717 - | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
3.718 - let
3.719 - val thy = assoc_thy "Isac";
3.720 - in
3.721 - if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
3.722 - then
3.723 - if f = f_ then Ass (m,f') else AssWeak (m,f')
3.724 - else NotAss
3.725 - end
3.726 - | _ => NotAss)
3.727 -
3.728 - | assod pt _ (m as Check_elementwise' (consts,_,(consts_chkd,_)))
3.729 - (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
3.730 - if consts = consts'
3.731 - then Ass (m, consts_chkd)
3.732 - else NotAss
3.733 -
3.734 - | assod pt _ (m as Or_to_List' (ors, list)) (Const ("Script.Or'_to'_List",_) $ _) =
3.735 - Ass (m, list)
3.736 -
3.737 - | assod pt _ (m as Take' term) (Const ("Script.Take",_) $ _) =
3.738 - Ass (m, term)
3.739 -
3.740 - | assod pt _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute",_) $ _ $ t) =
3.741 - if f = t then Ass (m, f')
3.742 - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
3.743 - if foldl and_ (true, map contains_Var subte)
3.744 - then
3.745 - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
3.746 - in if t = t' then error "assod: Substitute' not applicable to val of Expr"
3.747 - else Ass (Substitute' (ro, erls, subte, t, t'), t')
3.748 - end
3.749 - else (case rewrite_terms_ (Isac()) ro erls subte t of
3.750 + (Const ("Script.Rewrite", _) $ Free (thmID_, _) $ _ $ f_) =>
3.751 + ((*tracing ("3### assod: stac = " ^ ter2str t);
3.752 + tracing ("3### assod: f(m)= " ^ term2str f);*)
3.753 + if thmID = thmID_
3.754 + then
3.755 + if f = f_
3.756 + then ((*tracing"3### assod ..Ass";*) Ass (m,f'))
3.757 + else
3.758 + ((*tracing"### assod ..AssWeak";
3.759 + tracing("### assod: f(m) = " ^ term2str f);
3.760 + tracing("### assod: f(stac)= " ^ term2str f_)*)
3.761 + AssWeak (m,f'))
3.762 + else ((*tracing"3### assod ..NotAss";*) NotAss))
3.763 + | (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =>
3.764 + if contains_rule (Thm thm'') (assoc_rls rls_)
3.765 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.766 + else NotAss
3.767 + | _ => NotAss)
3.768 + | assod _ _ (m as Rewrite_Set_Inst' (_, _, _, rls, f, (f', _)))
3.769 + (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) =
3.770 + if id_rls rls = rls_
3.771 + then if f = f_ then Ass (m, f') else AssWeak (m ,f')
3.772 + else NotAss
3.773 + | assod _ _ (m as Detail_Set_Inst' (_, _, _, rls, f, (f',_)))
3.774 + (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free (rls_, _) $ _ $ f_) =
3.775 + if id_rls rls = rls_
3.776 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.777 + else NotAss
3.778 + | assod _ _ (m as Rewrite_Set' (_, _, rls, f, (f', _)))
3.779 + (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =
3.780 + if id_rls rls = rls_
3.781 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.782 + else NotAss
3.783 + | assod _ _ (m as Detail_Set' (_, _, rls, f, (f', _)))
3.784 + (Const ("Script.Rewrite'_Set", _) $ Free (rls_, _) $ _ $ f_) =
3.785 + if id_rls rls = rls_
3.786 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.787 + else NotAss
3.788 + | assod _ _ (m as Calculate' (_, op_, f, (f', _))) stac =
3.789 + (case stac of
3.790 + (Const ("Script.Calculate",_) $ Free (op__,_) $ f_) =>
3.791 + if op_ = op__
3.792 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.793 + else NotAss
3.794 + | (Const ("Script.Rewrite'_Set'_Inst", _) $ _ $ Free(rls_,_) $_$f_) =>
3.795 + let val thy = assoc_thy "Isac";
3.796 + in
3.797 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
3.798 + then if f = f_ then Ass (m, f') else AssWeak (m, f')
3.799 + else NotAss
3.800 + end
3.801 + | (Const ("Script.Rewrite'_Set",_) $ Free (rls_, _) $ _ $ f_) =>
3.802 + let val thy = assoc_thy "Isac";
3.803 + in
3.804 + if contains_rule (Calc (assoc_calc' thy op_ |> snd)) (assoc_rls rls_)
3.805 + then if f = f_ then Ass (m,f') else AssWeak (m,f')
3.806 + else NotAss
3.807 + end
3.808 + | _ => NotAss)
3.809 + | assod _ _ (m as Check_elementwise' (consts, _, (consts_chkd, _)))
3.810 + (Const ("Script.Check'_elementwise",_) $ consts' $ _) =
3.811 + if consts = consts'
3.812 + then Ass (m, consts_chkd)
3.813 + else NotAss
3.814 + | assod _ _ (m as Or_to_List' (_, list)) (Const ("Script.Or'_to'_List", _) $ _) = Ass (m, list)
3.815 + | assod _ _ (m as Take' term) (Const ("Script.Take", _) $ _) = Ass (m, term)
3.816 + | assod _ _ (m as Substitute' (ro, erls, subte, f, f')) (Const ("Script.Substitute", _) $ _ $ t) =
3.817 + if f = t then Ass (m, f')
3.818 + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
3.819 + if foldl and_ (true, map contains_Var subte)
3.820 + then
3.821 + let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
3.822 + in if t = t' then error "assod: Substitute' not applicable to val of Expr"
3.823 + else Ass (Substitute' (ro, erls, subte, t, t'), t')
3.824 + end
3.825 + else (case rewrite_terms_ (Isac()) ro erls subte t of
3.826 SOME (t', _) => Ass (Substitute' (ro, erls, subte, t, t'), t')
3.827 | NONE => error "assod: Substitute' not applicable to val of Expr")
3.828 -
3.829 - | assod pt _ (m as Tac_ (thy,f,id,f')) (Const ("Script.Tac",_) $ Free (id',_)) =
3.830 - if id = id'
3.831 - then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
3.832 - else NotAss
3.833 + | assod _ _ (m as Tac_ (thy, _, id, f')) (Const ("Script.Tac",_) $ Free (id', _)) =
3.834 + if id = id'
3.835 + then Ass (m, ((Thm.term_of o the o (parse thy)) f'))
3.836 + else NotAss
3.837
3.838 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
3.839 - | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,_,f))
3.840 - (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
3.841 - Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
3.842 - let
3.843 - val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
3.844 - val thy = maxthy (assoc_thy dI) (rootthy pt);
3.845 - val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
3.846 - val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
3.847 - val ags = isalist2list ags';
3.848 - val (pI, pors, mI) =
3.849 - if mI = ["no_met"]
3.850 - then
3.851 - let
3.852 - val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
3.853 - handle ERROR "actual args do not match formal args"
3.854 - => (match_ags_msg pI stac ags(*raise exn*);[]);
3.855 - val pI' = refine_ori' pors pI;
3.856 - in (pI', pors (*refinement over models with diff.prec only*),
3.857 - (hd o #met o get_pbt) pI')
3.858 - end
3.859 - else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
3.860 - handle ERROR "actual args do not match formal args"
3.861 - => (match_ags_msg pI stac ags(*raise exn*);[]), mI);
3.862 - val (fmz_, vals) = oris2fmz_vals pors;
3.863 - val {cas, ppc, thy,...} = get_pbt pI
3.864 - val dI = theory2theory' thy (*take dI from _refined_ pbl*)
3.865 - val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
3.866 - val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global
3.867 - |> declare_constraints' vals
3.868 - val hdl =
3.869 - case cas of
3.870 - NONE => pblterm dI pI
3.871 - | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
3.872 - val f = subpbl (strip_thy dI) pI
3.873 - in
3.874 - if domID = dI andalso pblID = pI
3.875 - then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
3.876 - else NotAss
3.877 - end
3.878 + | assod pt _ (Subproblem' ((domID, pblID, _), _, _, _, _, _))
3.879 + (stac as Const ("Script.SubProblem",_) $ (Const ("Product_Type.Pair",_) $
3.880 + Free (dI',_) $ (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
3.881 + let
3.882 + val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
3.883 + val thy = maxthy (assoc_thy dI) (rootthy pt);
3.884 + val pI = ((map (de_esc_underscore o free2str)) o isalist2list) pI';
3.885 + val mI = ((map (de_esc_underscore o free2str)) o isalist2list) mI';
3.886 + val ags = isalist2list ags';
3.887 + val (pI, pors, mI) =
3.888 + if mI = ["no_met"]
3.889 + then
3.890 + let
3.891 + val pors = (match_ags thy ((#ppc o get_pbt) pI) ags)
3.892 + handle ERROR "actual args do not match formal args"
3.893 + => (match_ags_msg pI stac ags(*raise exn*);[]);
3.894 + val pI' = refine_ori' pors pI;
3.895 + in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o get_pbt) pI')
3.896 + end
3.897 + else (pI, (match_ags thy ((#ppc o get_pbt) pI) ags)
3.898 + handle ERROR "actual args do not match formal args"
3.899 + => (match_ags_msg pI stac ags(*raise exn*); []), mI);
3.900 + val (fmz_, vals) = oris2fmz_vals pors;
3.901 + val {cas, ppc, thy, ...} = get_pbt pI
3.902 + val dI = theory2theory' thy (*take dI from _refined_ pbl*)
3.903 + val dI = theory2theory' (maxthy (assoc_thy dI) (rootthy pt))
3.904 + val ctxt = dI |> Thy_Info.get_theory |> Proof_Context.init_global |> declare_constraints' vals
3.905 + val hdl =
3.906 + case cas of
3.907 + NONE => pblterm dI pI
3.908 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals) t
3.909 + val f = subpbl (strip_thy dI) pI
3.910 + in
3.911 + if domID = dI andalso pblID = pI
3.912 + then Ass (Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f), f)
3.913 + else NotAss
3.914 + end
3.915 + | assod _ _ m _ =
3.916 + (if (!trace_script)
3.917 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
3.918 + ^ "@@@ tac_ = " ^ tac_2str m)
3.919 + else ();
3.920 + NotAss);
3.921
3.922 - | assod pt d m t =
3.923 - (if (!trace_script)
3.924 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"^
3.925 - "@@@ tac_ = "^(tac_2str m))
3.926 - else ();
3.927 - NotAss);
3.928 -
3.929 -fun tac_2tac (Refine_Tacitly' (pI,_,_,_,_)) = Refine_Tacitly pI
3.930 - | tac_2tac (Model_Problem' (pI,_,_)) = Model_Problem
3.931 - | tac_2tac (Add_Given' (t,_)) = Add_Given t
3.932 - | tac_2tac (Add_Find' (t,_)) = Add_Find t
3.933 - | tac_2tac (Add_Relation' (t,_)) = Add_Relation t
3.934 +fun tac_2tac (Refine_Tacitly' (pI, _, _, _, _)) = Refine_Tacitly pI
3.935 + | tac_2tac (Model_Problem' (_, _, _)) = Model_Problem
3.936 + | tac_2tac (Add_Given' (t, _)) = Add_Given t
3.937 + | tac_2tac (Add_Find' (t, _)) = Add_Find t
3.938 + | tac_2tac (Add_Relation' (t, _)) = Add_Relation t
3.939
3.940 - | tac_2tac (Specify_Theory' dI) = Specify_Theory dI
3.941 - | tac_2tac (Specify_Problem' (dI,_)) = Specify_Problem dI
3.942 - | tac_2tac (Specify_Method' (dI,_,_)) = Specify_Method dI
3.943 + | tac_2tac (Specify_Theory' dI) = Specify_Theory dI
3.944 + | tac_2tac (Specify_Problem' (dI, _)) = Specify_Problem dI
3.945 + | tac_2tac (Specify_Method' (dI, _, _)) = Specify_Method dI
3.946
3.947 | tac_2tac (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
3.948 | tac_2tac (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (subst2subs sub, thm)
3.949
3.950 - | tac_2tac (Rewrite_Set' (thy,put,rls,f,(f',asm))) = Rewrite_Set (id_rls rls)
3.951 - | tac_2tac (Detail_Set' (thy,put,rls,f,(f',asm))) = Detail_Set (id_rls rls)
3.952 + | tac_2tac (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (id_rls rls)
3.953 + | tac_2tac (Detail_Set' (_, _, rls, _, _)) = Detail_Set (id_rls rls)
3.954
3.955 - | tac_2tac (Rewrite_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
3.956 - Rewrite_Set_Inst (subst2subs sub,id_rls rls)
3.957 - | tac_2tac (Detail_Set_Inst' (thy,put,sub,rls,f,(f',asm))) =
3.958 - Detail_Set_Inst (subst2subs sub,id_rls rls)
3.959 + | tac_2tac (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
3.960 + Rewrite_Set_Inst (subst2subs sub,id_rls rls)
3.961 + | tac_2tac (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
3.962 + Detail_Set_Inst (subst2subs sub,id_rls rls)
3.963
3.964 - | tac_2tac (Calculate' (thy,op_,t,(t',thm'))) = Calculate (op_)
3.965 -
3.966 - | tac_2tac (Check_elementwise' (consts,pred,consts')) = Check_elementwise pred
3.967 + | tac_2tac (Calculate' (_, op_, _, _)) = Calculate (op_)
3.968 + | tac_2tac (Check_elementwise' (_, pred, _)) = Check_elementwise pred
3.969
3.970 | tac_2tac (Or_to_List' _) = Or_to_List
3.971 | tac_2tac (Take' term) = Take (term2str term)
3.972 - | tac_2tac (Substitute' (_, _, subte, t, res)) = Substitute (subte2sube subte)
3.973 -
3.974 - | tac_2tac (Tac_ (_,f,id,f')) = Tac id
3.975 + | tac_2tac (Substitute' (_, _, subte, _, _)) = Substitute (subte2sube subte)
3.976 + | tac_2tac (Tac_ (_, _, id, _)) = Tac id
3.977
3.978 | tac_2tac (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
3.979 | tac_2tac (Check_Postcond' (pblID, _)) = Check_Postcond pblID
3.980 | tac_2tac Empty_Tac_ = Empty_Tac
3.981 - | tac_2tac m =
3.982 - error ("tac_2tac: not impl. for "^(tac_2str m));
3.983 + | tac_2tac m = error ("tac_2tac: not impl. for "^(tac_2str m));
3.984
3.985 -
3.986 -
3.987 -
3.988 -(** decompose tac_ to a rule and to (lhs,rhs)
3.989 - unly needed --- **)
3.990 -
3.991 -val idT = Type ("Script.ID",[]);
3.992 -(*val tt = (Thm.term_of o the o (parse thy)) "square_equation_left::ID";
3.993 -type_of tt = idT;
3.994 -val it = true : bool
3.995 -*)
3.996 +val idT = Type ("Script.ID", []);
3.997
3.998 fun make_rule thy t =
3.999 let val ct = Thm.global_cterm_of thy (Trueprop $ t)
3.1000 in Thm (term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
3.1001
3.1002 -(* val (Rewrite_Inst'(thy',rod,rls,put,subs,(thmID,thm),f,(f',asm)))=m;
3.1003 - *)
3.1004 -(*decompose tac_ to a rule and to (lhs,rhs) for ets FIXME.12.03: obsolete!
3.1005 - NOTE.12.03: also used for msg 'not locatable' ?!: 'Subproblem' missing !!!
3.1006 -WN0508 only use in tac_2res, which uses only last return-value*)
3.1007 -fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
3.1008 - let val fT = type_of f;
3.1009 - val b = if put then @{term True} else @{term False};
3.1010 - val sT = (type_of o fst o hd) subs;
3.1011 - val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
3.1012 - (map HOLogic.mk_prod subs);
3.1013 - val sT' = type_of subs';
3.1014 - val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,(*fT*)bool,fT] ---> fT)
3.1015 - $ subs' $ Free (thmID, idT) $ b $ f;
3.1016 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1017 -(*Fehlersuche 25.4.01
3.1018 -(a)----- als String zusammensetzen:
3.1019 -ML> term2str f;
3.1020 -val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
3.1021 -ML> term2str f';
3.1022 -val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
3.1023 -ML> subs;
3.1024 -val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
3.1025 -> val tt = (Thm.term_of o the o (parse thy))
3.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))";
3.1027 -> atomty tt;
3.1028 -ML> tracing (term2str tt);
3.1029 -(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
3.1030 - #0 + d_d x (x ^^^ #2 + #3 * x)
3.1031 +fun rep_tac_ (Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _))) =
3.1032 + let val fT = type_of f;
3.1033 + val b = if put then @{term True} else @{term False};
3.1034 + val sT = (type_of o fst o hd) subs;
3.1035 + val subs' = list2isalist (HOLogic.mk_prodT (sT, sT)) (map HOLogic.mk_prod subs);
3.1036 + val sT' = type_of subs';
3.1037 + val lhs = Const ("Script.Rewrite'_Inst", [sT', idT, bool, fT] ---> fT)
3.1038 + $ subs' $ Free (thmID, idT) $ b $ f;
3.1039 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
3.1040 + | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
3.1041 + let
3.1042 + val fT = type_of f;
3.1043 + val b = if put then @{term True} else @{term False};
3.1044 + val lhs = Const ("Script.Rewrite", [idT, HOLogic.boolT, fT] ---> fT)
3.1045 + $ Free (thmID, idT) $ b $ f;
3.1046 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
3.1047 + | rep_tac_ (Rewrite_Set_Inst' (_, _, _, _, _, (f', _))) = (e_rule, (e_term, f'))
3.1048 + | rep_tac_ (Rewrite_Set' (thy', put, rls, f, (f', _))) =
3.1049 + let
3.1050 + val fT = type_of f;
3.1051 + val b = if put then @{term True} else @{term False};
3.1052 + val lhs = Const ("Script.Rewrite'_Set", [idT, bool, fT] ---> fT)
3.1053 + $ Free (id_rls rls, idT) $ b $ f;
3.1054 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1055 + | rep_tac_ (Calculate' (thy', op_, f, (f', _)))=
3.1056 + let
3.1057 + val fT = type_of f;
3.1058 + val lhs = Const ("Script.Calculate",[idT,fT] ---> fT) $ Free (op_,idT) $ f
3.1059 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1060 + | rep_tac_ (Check_elementwise' (_, _, (t', _))) = (Erule, (e_term, t'))
3.1061 + | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
3.1062 + | rep_tac_ (Take' t') = (Erule, (e_term, t'))
3.1063 + | rep_tac_ (Substitute' (_, _, _, t, t')) = (Erule, (t, t'))
3.1064 + | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
3.1065 + | rep_tac_ m = error ("rep_tac_: not impl.for " ^ tac_2str m)
3.1066
3.1067 -(b)----- laut rep_tac_:
3.1068 -> val ttt=HOLogic.mk_eq (lhs,f');
3.1069 -> atomty ttt;
3.1070 -
3.1071 -
3.1072 -(*Fehlersuche 1-2Monate vor 4.01:*)
3.1073 -> val tt = (Thm.term_of o the o (parse thy))
3.1074 - "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
3.1075 -> atomty tt;
3.1076 -
3.1077 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
3.1078 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
3.1079 -> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
3.1080 - (Thm.term_of o the o (parse thy)) "x")];
3.1081 -> val sT = (type_of o fst o hd) subs;
3.1082 -> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
3.1083 - (map HOLogic.mk_prod subs);
3.1084 -> val sT' = type_of subs';
3.1085 -> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
3.1086 - $ subs' $ Free (thmID,idT) $ @{term True} $ f;
3.1087 -> lhs = tt;
3.1088 -val it = true : bool
3.1089 -> rep_tac_ (Rewrite_Inst'
3.1090 - ("Script","tless_true","eval_rls",false,subs,
3.1091 - ("square_equation_left",""),f,(f',[])));
3.1092 -*)
3.1093 - | rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
3.1094 - let
3.1095 - val fT = type_of f;
3.1096 - val b = if put then @{term True} else @{term False};
3.1097 - val lhs = Const ("Script.Rewrite",[idT,HOLogic.boolT,fT] ---> fT)
3.1098 - $ Free (thmID, idT) $ b $ f;
3.1099 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1100 -(*
3.1101 -> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
3.1102 - "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
3.1103 -
3.1104 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
3.1105 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
3.1106 -> val Thm (id,thm) =
3.1107 - rep_tac_ (Rewrite'
3.1108 - ("Script","tless_true","eval_rls",false,
3.1109 - ("square_equation_left",""),f,(f',[])));
3.1110 -> val SOME ct = parse thy
3.1111 - "Rewrite square_equation_left True (x=#1+#2)";
3.1112 -> rewrite_ Script.thy tless_true eval_rls true thm ct;
3.1113 -val it = SOME ("x = #3",[]) : (cterm * cterm list) option
3.1114 -*)
3.1115 - | rep_tac_ (Rewrite_Set_Inst'
3.1116 - (thy',put,subs,rls,f,(f',asm))) =
3.1117 - (e_rule, (e_term, f'))
3.1118 -(*WN050824: type error ...
3.1119 - let val fT = type_of f;
3.1120 - val sT = (type_of o fst o hd) subs;
3.1121 - val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
3.1122 - (map HOLogic.mk_prod subs);
3.1123 - val sT' = type_of subs';
3.1124 - val b = if put then @{term True} else @{term False}
3.1125 - val lhs = Const ("Script.Rewrite'_Set'_Inst",
3.1126 - [sT',idT,fT,fT] ---> fT)
3.1127 - $ subs' $ Free (id_rls rls,idT) $ b $ f;
3.1128 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
3.1129 -(* ... vals from Rewrite_Inst' ...
3.1130 -> rep_tac_ (Rewrite_Set_Inst'
3.1131 - ("Script",false,subs,
3.1132 - "isolate_bdv",f,(f',[])));
3.1133 -*)
3.1134 -(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
3.1135 -*)
3.1136 - | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
3.1137 - let val fT = type_of f;
3.1138 - val b = if put then @{term True} else @{term False};
3.1139 - val lhs = Const ("Script.Rewrite'_Set",[idT,bool,fT] ---> fT)
3.1140 - $ Free (id_rls rls,idT) $ b $ f;
3.1141 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1142 -(* 13.3.01:
3.1143 -val thy = assoc_thy thy';
3.1144 -val t = HOLogic.mk_eq (lhs,f');
3.1145 -make_rule thy t;
3.1146 ---------------------------------------------------
3.1147 -val lll = (Thm.term_of o the o (parse thy))
3.1148 - "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
3.1149 -
3.1150 ---------------------------------------------------
3.1151 -> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
3.1152 -> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
3.1153 -> val Thm (id,thm) =
3.1154 - rep_tac_ (Rewrite_Set'
3.1155 - ("Script",false,"SqRoot_simplify",f,(f',[])));
3.1156 -val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
3.1157 -val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
3.1158 -*)
3.1159 - | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
3.1160 - let val fT = type_of f;
3.1161 - val lhs = Const ("Script.Calculate",[idT,fT] ---> fT)
3.1162 - $ Free (op_,idT) $ f
3.1163 - in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
3.1164 -(*
3.1165 -> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
3.1166 - ... test-root-equ.sml: calculate ...
3.1167 -> val Appl m'=applicable_in p pt (Calculate "PLUS");
3.1168 -> val (lhs,_)=tac_2etac m';
3.1169 -> lhs'=lhs;
3.1170 -val it = true : bool*)
3.1171 - | rep_tac_ (Check_elementwise' (t,str,(t',asm))) = (Erule, (e_term, t'))
3.1172 - | rep_tac_ (Subproblem' (_, _, _, _, _, t')) = (Erule, (e_term, t'))
3.1173 - | rep_tac_ (Take' (t')) = (Erule, (e_term, t'))
3.1174 - | rep_tac_ (Substitute' (_, _, subst,t,t')) = (Erule, (t, t'))
3.1175 - | rep_tac_ (Or_to_List' (t, t')) = (Erule, (t, t'))
3.1176 - | rep_tac_ m = error ("rep_tac_: not impl.for "^
3.1177 - (tac_2str m));
3.1178 -
3.1179 -(*"N.3.6.03------
3.1180 -fun tac_2rule m = (fst o rep_tac_) m;
3.1181 -fun tac_2etac m = (snd o rep_tac_) m;
3.1182 -fun tac_2tac m = (fst o snd o rep_tac_) m;*)
3.1183 -fun tac_2res m = (snd o snd o rep_tac_) m;(*ONLYuse of rep_tac_
3.1184 - FIXXXXME: simplify rep_tac_*)
3.1185 -
3.1186 +fun tac_2res m = (snd o snd o rep_tac_) m;
3.1187
3.1188 (* handle a leaf at the end of recursive descent:
3.1189 a leaf is either a tactic or an 'expr' in "let v = expr"
3.1190 @@ -843,295 +515,244 @@
3.1191 *)
3.1192 fun handle_leaf call thy srls E a v t =
3.1193 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
3.1194 - case subst_stacexpr E a v t of
3.1195 - (a', STac stac) => (*script-tactic*)
3.1196 - let val stac' =
3.1197 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
3.1198 - in
3.1199 - (if (!trace_script)
3.1200 - then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac'^"'")
3.1201 - else ();
3.1202 - (a', STac stac'))
3.1203 - end
3.1204 - | (a', Expr lexpr) => (*leaf-expression*)
3.1205 - let val lexpr' =
3.1206 - eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
3.1207 - in
3.1208 - (if (!trace_script)
3.1209 - then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
3.1210 - else ();
3.1211 - (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
3.1212 - end;
3.1213 + case subst_stacexpr E a v t of
3.1214 + (a', STac stac) => (*script-tactic*)
3.1215 + let val stac' =
3.1216 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
3.1217 + in
3.1218 + (if (! trace_script)
3.1219 + then tracing ("@@@ "^call^" leaf '"^term2str t^"' ---> STac '"^term2str stac ^"'")
3.1220 + else ();
3.1221 + (a', STac stac'))
3.1222 + end
3.1223 + | (a', Expr lexpr) => (*leaf-expression*)
3.1224 + let val lexpr' =
3.1225 + eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) lexpr)
3.1226 + in
3.1227 + (if (! trace_script)
3.1228 + then tracing("@@@ "^call^" leaf '"^term2str t^"' ---> Expr '"^term2str lexpr'^"'")
3.1229 + else ();
3.1230 + (a', Expr lexpr')) (*lexpr' is the value of the Expr*)
3.1231 + end;
3.1232
3.1233 -
3.1234 -(** locate an applicable stactic in a script **)
3.1235 -
3.1236 -datatype assoc = (*ExprVal in the sense of denotational semantics*)
3.1237 - Assoc of (*the stac is associated, strongly or weakly*)
3.1238 - scrstate * (*the current; returned for next_tac etc. outside ass* *)
3.1239 - (step list) (*list of steps done until associated stac found;
3.1240 - initiated with the data for doing the 1st step,
3.1241 - thus the head holds these data further on,
3.1242 - while the tail holds steps finished (incl.scrstate in ptree)*)
3.1243 -| NasApp of (*stac not associated, but applicable, ptree-node generated*)
3.1244 +(** locate an applicable stac in a script **)
3.1245 +datatype assoc = (* ExprVal in the sense of denotational semantics *)
3.1246 + Assoc of (* the stac is associated, strongly or weakly *)
3.1247 + scrstate * (* the current; returned for next_tac etc. outside ass* *)
3.1248 + (step list) (* list of steps done until associated stac found;
3.1249 + initiated with the data for doing the 1st step,
3.1250 + thus the head holds these data further on,
3.1251 + while the tail holds steps finished (incl.scrstate in ptree) *)
3.1252 +| NasApp of (* stac not associated, but applicable, ptree-node generated *)
3.1253 scrstate * (step list)
3.1254 -| NasNap of (*stac not associated, not applicable, nothing generated;
3.1255 - for distinction in Or, for leaving iterations, leaving Seq,
3.1256 - evaluate scriptexpressions*)
3.1257 +| NasNap of (* stac not associated, not applicable, nothing generated;
3.1258 + for distinction in Or, for leaving iterations, leaving Seq,
3.1259 + evaluate scriptexpressions *)
3.1260 term * env;
3.1261 -fun assoc2str (Assoc _) = "Assoc"
3.1262 - | assoc2str (NasNap _) = "NasNap"
3.1263 +fun assoc2str (Assoc _) = "Assoc"
3.1264 + | assoc2str (NasNap _) = "NasNap"
3.1265 | assoc2str (NasApp _) = "NasApp";
3.1266
3.1267 +datatype asap = (* arg. of assy _only_ for distinction w.r.t. Or *)
3.1268 + Aundef (* undefined: set only by (topmost) Or *)
3.1269 +| AssOnly (* do not execute appl stacs - there could be an associated
3.1270 + in parallel Or-branch *)
3.1271 +| AssGen; (* no Ass(Weak) found within Or, thus
3.1272 + search for _applicable_ stacs, execute and generate pt *)
3.1273 +(*this constructions doesnt allow arbitrary nesting of Or !!! *)
3.1274
3.1275 -datatype asap = (*arg. of assy _only_ for distinction w.r.t. Or*)
3.1276 - Aundef (*undefined: set only by (topmost) Or*)
3.1277 -| AssOnly (*do not execute appl stacs - there could be an associated
3.1278 - in parallel Or-branch*)
3.1279 -| AssGen; (*no Ass(Weak) found within Or, thus
3.1280 - search for _applicable_ stacs, execute and generate pt*)
3.1281 -(*this constructions doesnt allow arbitrary nesting of Or !!!*)
3.1282 +(* assy, ass_up, astep_up scan for locate_gen in a script.
3.1283 + search is clearly separated into (1)-(2):
3.1284 + (1) assy is recursive descent;
3.1285 + (2) ass_up resumes interpretation at a location somewhere in the script;
3.1286 + astep_up does only get to the parentnode of the scriptexpr.
3.1287 + consequence:
3.1288 + * call of (2) means _always_ that in this branch below
3.1289 + there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
3.1290 +*)
3.1291 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
3.1292 +fun assy ya ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
3.1293 + (case assy ya ((E , l @ [L, R], a,v,S,b),ss) e of
3.1294 + NasApp ((E',l,a,v,S,_),ss) =>
3.1295 + let
3.1296 + val id' = mk_Free (id, T);
3.1297 + val E' = upd_env E' (id', v);
3.1298 + in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
3.1299 + | NasNap (v,E) =>
3.1300 + let
3.1301 + val id' = mk_Free (id, T);
3.1302 + val E' = upd_env E (id', v);
3.1303 + in assy ya ((E', l @ [R, D], a,v,S,b),ss) body end
3.1304 + | ay => ay)
3.1305 + | assy (ya as (thy,_,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
3.1306 + if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
3.1307 + then assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e
3.1308 + else NasNap (v, E)
3.1309 + | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
3.1310 + if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
3.1311 + then assy ya ((E, l @ [R], a,v,S,b),ss) e
3.1312 + else NasNap (v, E)
3.1313 + | assy (ya as (thy,_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
3.1314 + if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
3.1315 + then assy ya ((E, l @ [L, R], a,v,S,b),ss) e1
3.1316 + else assy ya ((E, l @ [R], a,v,S,b),ss) e2
3.1317 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
3.1318 + (case assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e of ay => ay)
3.1319 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
3.1320 + (case assy ya ((E, l @ [R], a,v,S,b),ss) e of ay => ay)
3.1321 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
3.1322 + (case assy ya ((E, l @ [L, L, R], SOME a,v,S,b),ss) e1 of
3.1323 + NasNap (v, E) => assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e2
3.1324 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [L, R], SOME a,v,S,b),ss) e2
3.1325 + | ay => ay)
3.1326 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
3.1327 + (case assy ya ((E, l @ [L, R], a,v,S,b),ss) e1 of
3.1328 + NasNap (v, E) => assy ya ((E, l @ [R], a,v,S,b),ss) e2
3.1329 + | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l @ [R], a,v,S,b),ss) e2
3.1330 + | ay => ay)
3.1331 + | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
3.1332 + assy ya ((E,(l @ [L, R]),SOME a,v,S,b),ss) e
3.1333 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
3.1334 + assy ya ((E,(l @ [R]),a,v,S,b),ss) e
3.1335 + | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
3.1336 + (case assy (y,x,s,sc,AssOnly) ((E,(l @ [L, L, R]),SOME a,v,S,b),ss) e1 of
3.1337 + NasNap (v, E) =>
3.1338 + (case assy (y,x,s,sc,AssOnly) ((E,(l @ [L, R]),SOME a,v,S,b),ss) e2 of
3.1339 + NasNap (v, E) =>
3.1340 + (case assy (y,x,s,sc,AssGen) ((E,(l @ [L, L, R]),SOME a,v,S,b),ss) e1 of
3.1341 + NasNap (v, E) =>
3.1342 + assy (y,x,s,sc,AssGen) ((E, (l @ [L, R]), SOME a,v,S,b),ss) e2
3.1343 + | ay => ay)
3.1344 + | ay =>ay)
3.1345 + | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
3.1346 + | ay => (ay))
3.1347 + | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
3.1348 + (case assy ya ((E,(l @ [L, R]),a,v,S,b),ss) e1 of
3.1349 + NasNap (v, E) => assy ya ((E,(l @ [R]),a,v,S,b),ss) e2
3.1350 + | ay => (ay))
3.1351 + (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
3.1352 + | assy (thy',ctxt,sr,d,ap) ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss) t =
3.1353 + (case handle_leaf "locate" thy' sr E a v t of
3.1354 + (a', Expr _) =>
3.1355 + (NasNap (eval_listexpr_ (assoc_thy thy') sr
3.1356 + (subst_atomic (upd_env_opt E (a',v)) t), E))
3.1357 + | (a', STac stac) =>
3.1358 + let
3.1359 + val p' =
3.1360 + case p_ of Frm => p
3.1361 + | Res => lev_on p
3.1362 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
3.1363 + in
3.1364 + case assod pt d m stac of
3.1365 + Ass (m,v') =>
3.1366 + let val (p'',c',f',pt') =
3.1367 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
3.1368 + in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
3.1369 + | AssWeak (m,v') =>
3.1370 + let val (p'',c',f',pt') =
3.1371 + generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
3.1372 + in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
3.1373 + | NotAss =>
3.1374 + (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
3.1375 + AssOnly => (NasNap (v, E))
3.1376 + | _ =>
3.1377 + (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
3.1378 + Appl m' =>
3.1379 + let
3.1380 + val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
3.1381 + val (p'',c',f',pt') =
3.1382 + generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
3.1383 + in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
3.1384 + | Notappl _ => (NasNap (v, E))
3.1385 + )
3.1386 + )
3.1387 + end)
3.1388 + | assy _ (_, []) t = error ("assy: uncovered fun-def with " ^ term2str t);
3.1389
3.1390 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
3.1391 +fun ass_up (ys as (y,ctxt,s,Prog sc,d)) ((E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
3.1392 + let
3.1393 + val l = drop_last l; (*comes from e, goes to Abs*)
3.1394 + val (i, T, body) =
3.1395 + (case go l sc of
3.1396 + Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
3.1397 + | t => error ("ass_up..HOL.Let $ _ with " ^ term2str t))
3.1398 + val i = mk_Free (i, T);
3.1399 + val E = upd_env E (i, v);
3.1400 + in case assy (y,ctxt,s,d,Aundef) ((E, l @ [R, D], a,v,S,b),ss) body of
3.1401 + Assoc iss => Assoc iss
3.1402 + | NasApp iss => astep_up ys iss
3.1403 + | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss)
3.1404 + end
3.1405 + | ass_up ys iss (Abs (_,_,_)) = astep_up ys iss (*TODO 5.9.00: env ?*)
3.1406 + | ass_up ys iss (Const ("HOL.Let",_) $ _ $ (Abs _)) = astep_up ys iss (*TODO 5.9.00: env ?*)
3.1407 + | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
3.1408 + astep_up ysa iss (*all has been done in (*2*) below*)
3.1409 + | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
3.1410 + astep_up ysa iss (*2*: comes from e2*)
3.1411
3.1412 -(*assy, ass_up, astep_up scan for locate_gen in a script.
3.1413 - search is clearly separated into (1)-(2):
3.1414 - (1) assy is recursive descent;
3.1415 - (2) ass_up resumes interpretation at a location somewhere in the script;
3.1416 - astep_up does only get to the parentnode of the scriptexpr.
3.1417 - consequence:
3.1418 - * call of (2) means _always_ that in this branch below
3.1419 - there was an appl.stac (Repeat, Or e1, ...) found by the previous step.
3.1420 -*)
3.1421 -fun assy ya (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))) =
3.1422 - (case assy ya ((E , l@[L,R], a,v,S,b),ss) e of
3.1423 - NasApp ((E',l,a,v,S,bb),ss) =>
3.1424 - let
3.1425 - val id' = mk_Free (id, T);
3.1426 - val E' = upd_env E' (id', v);
3.1427 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
3.1428 - | NasNap (v,E) =>
3.1429 - let
3.1430 - val id' = mk_Free (id, T);
3.1431 - val E' = upd_env E (id', v);
3.1432 - in assy ya ((E', l@[R,D], a,v,S,b),ss) body end
3.1433 - | ay => ay)
3.1434 -
3.1435 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Script.While",_) $ c $ e $ a) =
3.1436 - (if eval_true_ thy srls (subst_atomic (upd_env E (a,v)) c)
3.1437 - then assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e
3.1438 - else NasNap (v, E))
3.1439 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Script.While",_) $ c $ e) =
3.1440 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
3.1441 - then assy ya ((E, l@[R], a,v,S,b),ss) e
3.1442 - else NasNap (v, E))
3.1443 -
3.1444 - | assy (ya as (thy,ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
3.1445 - (if eval_true_ thy srls (subst_atomic (upd_env_opt E (a,v)) c)
3.1446 - then assy ya ((E, l@[L,R], a,v,S,b),ss) e1
3.1447 - else assy ya ((E, l@[ R], a,v,S,b),ss) e2)
3.1448 -
3.1449 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Try",_) $ e $ a) =
3.1450 - (case assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e of
3.1451 - ay => ay)
3.1452 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Try",_) $ e) =
3.1453 - (case assy ya ((E, l@[R], a,v,S,b),ss) e of
3.1454 - ay => ay)
3.1455 -
3.1456 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2 $ a) =
3.1457 - (case assy ya ((E, l@[L,L,R], SOME a,v,S,b),ss) e1 of
3.1458 - NasNap (v, E) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
3.1459 - | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[L,R], SOME a,v,S,b),ss) e2
3.1460 - | ay => ay)
3.1461 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Seq",_) $e1 $ e2) =
3.1462 - (case assy ya ((E, l@[L,R], a,v,S,b),ss) e1 of
3.1463 - NasNap (v, E) => assy ya ((E, l@[R], a,v,S,b),ss) e2
3.1464 - | NasApp ((E,_,_,v,_,_),ss) => assy ya ((E, l@[R], a,v,S,b),ss) e2
3.1465 - | ay => ay)
3.1466 -
3.1467 - | assy ya ((E,l,_,v,S,b),ss) (Const ("Script.Repeat",_) $ e $ a) =
3.1468 - assy ya ((E,(l@[L,R]),SOME a,v,S,b),ss) e
3.1469 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Repeat",_) $ e) =
3.1470 - assy ya ((E,(l@[R]),a,v,S,b),ss) e
3.1471 -
3.1472 - | assy (y,x,s,sc,Aundef) ((E,l,_,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2 $ a) =
3.1473 - (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
3.1474 - NasNap (v, E) =>
3.1475 - (case assy (y,x,s,sc,AssOnly) ((E,(l@[L,R]),SOME a,v,S,b),ss) e2 of
3.1476 - NasNap (v, E) =>
3.1477 - (case assy (y,x,s,sc,AssGen) ((E,(l@[L,L,R]),SOME a,v,S,b),ss) e1 of
3.1478 - NasNap (v, E) =>
3.1479 - assy (y,x,s,sc,AssGen) ((E, (l@[L,R]), SOME a,v,S,b),ss) e2
3.1480 - | ay => ay)
3.1481 - | ay =>(ay))
3.1482 - | NasApp _ => error ("assy: FIXXXME ///must not return NasApp///")
3.1483 - | ay => (ay))
3.1484 - | assy ya ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $e1 $ e2) =
3.1485 - (case assy ya ((E,(l@[L,R]),a,v,S,b),ss) e1 of
3.1486 - NasNap (v, E) => assy ya ((E,(l@[R]),a,v,S,b),ss) e2
3.1487 - | ay => (ay))
3.1488 -
3.1489 - (*here is not a tactical like TRY etc, but a tactic creating a step in calculation*)
3.1490 - | assy (thy',ctxt,sr,d,ap) (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss) t =
3.1491 - (case handle_leaf "locate" thy' sr E a v t of
3.1492 - (a', Expr s) =>
3.1493 - (NasNap (eval_listexpr_ (assoc_thy thy') sr
3.1494 - (subst_atomic (upd_env_opt E (a',v)) t), E))
3.1495 - | (a', STac stac) =>
3.1496 - let
3.1497 - val p' =
3.1498 - case p_ of Frm => p
3.1499 - | Res => lev_on p
3.1500 - | _ => error ("assy: call by " ^ pos'2str (p,p_));
3.1501 - in
3.1502 - case assod pt d m stac of
3.1503 - Ass (m,v') =>
3.1504 - let val (p'',c',f',pt') =
3.1505 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
3.1506 - in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
3.1507 - | AssWeak (m,v') =>
3.1508 - let val (p'',c',f',pt') =
3.1509 - generate1 (assoc_thy thy') m (ScrState (E,l,a',v',S,false), ctxt) (p',p_) pt;
3.1510 - in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
3.1511 - | NotAss =>
3.1512 - (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
3.1513 - AssOnly => (NasNap (v, E))
3.1514 - | gen =>
3.1515 - (case applicable_in (p,p_) pt (stac2tac pt (assoc_thy thy') stac) of
3.1516 - Appl m' =>
3.1517 - let
3.1518 - val is = (E,l,a',tac_2res m',S,false(*FIXXXME.WN0?*))
3.1519 - val (p'',c',f',pt') =
3.1520 - generate1 (assoc_thy thy') m' (ScrState is, ctxt) (p',p_) pt;
3.1521 - in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
3.1522 - | Notappl _ => (NasNap (v, E))
3.1523 - )
3.1524 - )
3.1525 - end);
3.1526 -
3.1527 -fun ass_up (ys as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss) (Const ("HOL.Let",_) $ _) =
3.1528 - let
3.1529 - (*val _= tracing("### ass_up1 Let$e: is=")
3.1530 - val _= tracing(istate2str (ScrState is))*)
3.1531 - val l = drop_last l; (*comes from e, goes to Abs*)
3.1532 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
3.1533 - val i = mk_Free (i, T);
3.1534 - val E = upd_env E (i, v);
3.1535 - (*val _=tracing("### ass_up2 Let$e: E="^(subst2str E));*)
3.1536 - in case assy (y,ctxt,s,d,Aundef) ((E, l@[R,D], a,v,S,b),ss) body of
3.1537 - Assoc iss => Assoc iss
3.1538 - | NasApp iss => astep_up ys iss
3.1539 - | NasNap (v, E) => astep_up ys ((E,l,a,v,S,b),ss) end
3.1540 -
3.1541 - | ass_up ys (iss as (is,_)) (Abs (_,_,_)) =
3.1542 - ((*tracing("### ass_up Abs: is=");
3.1543 - tracing(istate2str (ScrState is));*)
3.1544 - astep_up ys iss) (*TODO 5.9.00: env ?*)
3.1545 -
3.1546 - | ass_up ys (iss as (is,_)) (Const ("HOL.Let",_) $ e $ (Abs (i,T,b)))=
3.1547 - ((*tracing("### ass_up Let $ e $ Abs: is=");
3.1548 - tracing(istate2str (ScrState is));*)
3.1549 - astep_up ys iss) (*TODO 5.9.00: env ?*)
3.1550 -
3.1551 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _ $ _) =
3.1552 - astep_up ysa iss (*all has been done in (*2*) below*)
3.1553 -
3.1554 - | ass_up ysa iss (Const ("Script.Seq",_) $ _ $ _) =
3.1555 - astep_up ysa iss (*2*: comes from e2*)
3.1556 -
3.1557 - | ass_up (ysa as (y,ctxt,s,Prog sc,d)) (is as (E,l,a,v,S,b),ss)
3.1558 - (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
3.1559 - let
3.1560 - val up = drop_last l;
3.1561 - val Const ("Script.Seq",_) $ _ $ e2 = go up sc
3.1562 - (*val _= tracing("### ass_up Seq$e: is=")
3.1563 - val _= tracing(istate2str (ScrState is))*)
3.1564 - in
3.1565 - case assy (y,ctxt,s,d,Aundef) ((E, up@[R], a,v,S,b),ss) e2 of
3.1566 - NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
3.1567 - | NasApp iss => astep_up ysa iss
3.1568 - | ay => ay end
3.1569 -
3.1570 - | ass_up ysa iss (Const ("Script.Try",_) $ e $ _) =
3.1571 - astep_up ysa iss
3.1572 -
3.1573 - (* val (ysa, iss, (Const ("Script.Try",_) $ e)) =
3.1574 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
3.1575 - *)
3.1576 - | ass_up ysa iss (Const ("Script.Try",_) $ e) =
3.1577 - ((*tracing("### ass_up Try $ e");*)
3.1578 - astep_up ysa iss)
3.1579 -
3.1580 + | ass_up (ysa as (y,ctxt,s,Prog sc,d)) ((E,l,a,v,S,b),ss)
3.1581 + (Const ("Script.Seq",_) $ _ ) = (*2*: comes from e1, goes to e2*)
3.1582 + let
3.1583 + val up = drop_last l;
3.1584 + val e2 =
3.1585 + (case go up sc of
3.1586 + Const ("Script.Seq",_) $ _ $ e2 => e2
3.1587 + | t => error ("ass_up..Script.Seq $ _ with " ^ term2str t))
3.1588 + in case assy (y,ctxt,s,d,Aundef) ((E, up @ [R], a,v,S,b),ss) e2 of
3.1589 + NasNap (v,E) => astep_up ysa ((E,up,a,v,S,b),ss)
3.1590 + | NasApp iss => astep_up ysa iss
3.1591 + | ay => ay
3.1592 + end
3.1593 + | ass_up ysa iss (Const ("Script.Try",_) $ _ $ _) = astep_up ysa iss
3.1594 + | ass_up ysa iss (Const ("Script.Try",_) $ _) = astep_up ysa iss
3.1595 | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
3.1596 (*(Const ("Script.While",_) $ c $ e $ a) = WN050930 blind fix*)
3.1597 - (t as Const ("Script.While",_) $ c $ e $ a) =
3.1598 - ((*tracing("### ass_up: While c= "^
3.1599 - (term2str (subst_atomic (upd_env E (a,v)) c)));*)
3.1600 - if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
3.1601 - then (case assy (y,ctxt,s,d,Aundef) ((E, l@[L,R], SOME a,v,S,b),ss) e of
3.1602 - NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.1603 - | NasApp ((E',l,a,v,S,b),ss) =>
3.1604 - ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
3.1605 - | ay => ay)
3.1606 + (t as Const ("Script.While",_) $ c $ e $ a) =
3.1607 + if eval_true_ y s (subst_atomic (upd_env E (a,v)) c)
3.1608 + then case assy (y,ctxt,s,d,Aundef) ((E, l @ [L, R], SOME a,v,S,b),ss) e of
3.1609 + NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.1610 + | NasApp ((E',l,a,v,S,b),ss) =>
3.1611 + ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
3.1612 + | ay => ay
3.1613 else astep_up ys ((E,l, SOME a,v,S,b),ss)
3.1614 - )
3.1615 -
3.1616 | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
3.1617 (*(Const ("Script.While",_) $ c $ e) = WN050930 blind fix*)
3.1618 - (t as Const ("Script.While",_) $ c $ e) =
3.1619 + (t as Const ("Script.While",_) $ c $ e) =
3.1620 if eval_true_ y s (subst_atomic (upd_env_opt E (a,v)) c)
3.1621 - then (case assy (y,ctxt,s,d,Aundef) ((E, l@[R], a,v,S,b),ss) e of
3.1622 + then case assy (y,ctxt,s,d,Aundef) ((E, l @ [R], a,v,S,b),ss) e of
3.1623 NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)
3.1624 | NasApp ((E',l,a,v,S,b),ss) =>
3.1625 ass_up ys ((E',l,a,v,S,b),ss) t (*WN050930 't' was not assigned*)
3.1626 + | ay => ay
3.1627 + else astep_up ys ((E,l, a,v,S,b),ss)
3.1628 + | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
3.1629 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
3.1630 + (t as Const ("Script.Repeat",_) $ e $ a) =
3.1631 + (case assy (y,ctxt,s,d, Aundef) ((E, (l @ [L, R]), SOME a,v,S,b),ss) e of
3.1632 + NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.1633 + | NasApp ((E',l,a,v,S,b),ss) =>
3.1634 + ass_up ys ((E',l,a,v,S,b),ss) t
3.1635 + | ay => ay)
3.1636 + | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
3.1637 + (t as Const ("Script.Repeat",_) $ e) =
3.1638 + (case assy (y,ctxt,s,d,Aundef) ((E, (l @ [R]), a,v,S,b),ss) e of
3.1639 + NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
3.1640 + | NasApp ((E',l,a,v',S,_),ss) => ass_up ys ((E',l,a,v',S,b),ss) t
3.1641 | ay => ay)
3.1642 - else astep_up ys ((E,l, a,v,S,b),ss)
3.1643 -
3.1644 - | ass_up y iss (Const ("If",_) $ _ $ _ $ _) = astep_up y iss
3.1645 -
3.1646 - | ass_up (ys as (y,ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
3.1647 - (t as Const ("Script.Repeat",_) $ e $ a) =
3.1648 - (case assy (y,ctxt,s,d, Aundef) ((E, (l@[L,R]), SOME a,v,S,b),ss) e of
3.1649 - NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
3.1650 - | NasApp ((E',l,a,v,S,b),ss) =>
3.1651 - ass_up ys ((E',l,a,v,S,b),ss) t
3.1652 - | ay => ay)
3.1653 -
3.1654 - | ass_up (ys as (y,ctxt,s,_,d)) (is as ((E,l,a,v,S,b),ss))
3.1655 - (t as Const ("Script.Repeat",_) $ e) =
3.1656 - (case assy (y,ctxt,s,d,Aundef) ((E, (l@[R]), a,v,S,b),ss) e of
3.1657 - NasNap (v', E') => astep_up ys ((E',l,a,v',S,b),ss)
3.1658 - | NasApp ((E',l,a,v',S,bb),ss) =>
3.1659 - ass_up ys ((E',l,a,v',S,b),ss) t
3.1660 - | ay => ay)
3.1661 -
3.1662 | ass_up y iss (Const ("Script.Or",_) $ _ $ _ $ _) = astep_up y iss
3.1663 -
3.1664 | ass_up y iss (Const ("Script.Or",_) $ _ $ _) = astep_up y iss
3.1665 -
3.1666 | ass_up y ((E,l,a,v,S,b),ss) (Const ("Script.Or",_) $ _ ) =
3.1667 astep_up y ((E, (drop_last l), a,v,S,b),ss)
3.1668 -
3.1669 - | ass_up y iss t =
3.1670 - error ("ass_up not impl for t= "^(term2str t))
3.1671 -
3.1672 + | ass_up _ _ t =
3.1673 + error ("ass_up not impl for t= " ^ term2str t)
3.1674 and astep_up (ys as (_,_,_,Prog sc,_)) ((E,l,a,v,S,b),ss) =
3.1675 if 1 < length l
3.1676 - then
3.1677 - let val up = drop_last l;
3.1678 - (*val _= tracing("### astep_up: E= "^env2str E);*)
3.1679 - in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
3.1680 + then
3.1681 + let val up = drop_last l;
3.1682 + in ass_up ys ((E,up,a,v,S,b),ss) (go up sc) end
3.1683 else (NasNap (v, E))
3.1684 -;
3.1685 -
3.1686 -
3.1687 -
3.1688 -
3.1689 -
3.1690 -(* use"ME/script.sml";
3.1691 - use"script.sml";
3.1692 - term2str (go up sc);
3.1693 -
3.1694 - *)
3.1695 + | astep_up _ ((_,l,_,_,_,_),_) = error ("astep_up: uncovered fun-def with " ^ loc_2str l)
3.1696
3.1697 (*check if there are tacs for rewriting only*)
3.1698 fun rew_only ([]:step list) = true
3.1699 @@ -1143,16 +764,13 @@
3.1700 | rew_only (((Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
3.1701 | rew_only (((End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
3.1702 | rew_only _ = false;
3.1703 -
3.1704
3.1705 datatype locate =
3.1706 - Steps of istate (*producing hd of step list (which was latest)
3.1707 - for next_tac, for reporting Safe|Unsafe to DG*)
3.1708 - * step (*(scrstate producing this step is in ptree !)*)
3.1709 - list (*locate_gen may produce intermediate steps*)
3.1710 -| NotLocatable; (*no (m Ass m') or (m AssWeak m') found*)
3.1711 -
3.1712 -
3.1713 + Steps of istate (* producing hd of step list (which was latest)
3.1714 + for next_tac, for reporting Safe|Unsafe to DG *)
3.1715 + * step (* (scrstate producing this step is in ptree !) *)
3.1716 + list (* locate_gen may produce intermediate steps *)
3.1717 +| NotLocatable; (* no (m Ass m') or (m AssWeak m') found *)
3.1718
3.1719 (* locate_gen tries to locate an input tac m in the script.
3.1720 pursuing this goal the script is executed until an (m' equiv m) is found,
3.1721 @@ -1174,57 +792,41 @@
3.1722 NOT IMPL. -- "error: do other step before"
3.1723 NotLocatable: thus generate_hard
3.1724 *)
3.1725 -fun locate_gen (thy', g_) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
3.1726 - (Rfuns {locate_rule=lo,...}, d) (RrlsState (_,f'',rss,rts), ctxt) =
3.1727 - (case lo rss f (Thm thm) of
3.1728 - [] => NotLocatable
3.1729 - | rts' =>
3.1730 - Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
3.1731 -
3.1732 +(*WN161112 blanks between list elements left as is until istate is introduced here*)
3.1733 +fun locate_gen (thy', _) (Rewrite' (_, ro, er, pa, thm, f, _)) (pt, p)
3.1734 + (Rfuns {locate_rule=lo,...}, _) (RrlsState (_,f'',rss,rts), _) =
3.1735 + (case lo rss f (Thm thm) of
3.1736 + [] => NotLocatable
3.1737 + | rts' => Steps (rts2steps [] ((pt,p),(f,f'',rss,rts),(thy',ro,er,pa)) rts'))
3.1738 | locate_gen (thy',srls) (m:tac_) ((pt,p):ptree * pos')
3.1739 - (scr as Prog (h $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
3.1740 - let val thy = assoc_thy thy';
3.1741 - in
3.1742 - case if l = [] orelse ((*init.in solve..Apply_Method...*)
3.1743 - (last_elem o fst) p = 0 andalso snd p = Res)
3.1744 - then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
3.1745 - else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
3.1746 - Assoc (iss as (is as (_,_,_,_,_,strong_ass), ss as ((m',f',pt',p',c')::_))) =>
3.1747 - (if strong_ass
3.1748 - then
3.1749 - (Steps (ScrState is, ss))
3.1750 - else
3.1751 - if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
3.1752 - then
3.1753 - let
3.1754 - val (po,p_) = p
3.1755 - val po' = case p_ of Frm => po | Res => lev_on po
3.1756 - val (p'',c'',f'',pt'') =
3.1757 - generate1 thy m (ScrState is, ctxt) (po',p_) pt;
3.1758 - in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
3.1759 - else Steps (ScrState is, ss))
3.1760 -
3.1761 - | NasApp _ => NotLocatable
3.1762 - | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err) end
3.1763 -
3.1764 + (scr as Prog (_ $ body),d) (ScrState (E,l,a,v,S,b), ctxt) =
3.1765 + let val thy = assoc_thy thy';
3.1766 + in case if l = [] orelse (
3.1767 + (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res)
3.1768 + then (assy (thy',ctxt,srls,d,Aundef) ((E,[R],a,v,S,b), [(m,EmptyMout,pt,p,[])]) body)
3.1769 + else (astep_up (thy',ctxt,srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) ) of
3.1770 + Assoc ((is as (_,_,_,_,_,strong_ass), ss as (_ :: _))) =>
3.1771 + (if strong_ass
3.1772 + then (Steps (ScrState is, ss))
3.1773 + else
3.1774 + if rew_only ss (*andalso 'not strong_ass'= associated weakly*)
3.1775 + then
3.1776 + let
3.1777 + val (po,p_) = p
3.1778 + val po' = case p_ of Frm => po | Res => lev_on po | _ => error ("locate_gen " ^ pos_2str p_)
3.1779 + val (p'',c'',f'',pt'') = generate1 thy m (ScrState is, ctxt) (po',p_) pt
3.1780 + in Steps (ScrState is, [(m, f'',pt'',p'',c'')]) end
3.1781 + else Steps (ScrState is, ss))
3.1782 +
3.1783 + | NasApp _ => NotLocatable
3.1784 + | err => error ("not-found-in-script: NotLocatable from " ^ PolyML.makestring err)
3.1785 + end
3.1786 | locate_gen _ m _ (sc,_) (is, _) =
3.1787 - error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
3.1788 - "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
3.1789 + error ("locate_gen: wrong arguments,\n tac= " ^ tac_2str m ^ ",\n " ^
3.1790 + "scr= " ^ scr2str sc ^ ",\n istate= " ^ istate2str is);
3.1791
3.1792 (** find the next stactic in a script **)
3.1793
3.1794 -datatype appy = (*ExprVal in the sense of denotational semantics*)
3.1795 - Appy of (*applicable stac found, search stalled*)
3.1796 - tac_ * (*tac_ associated (fun assod) with stac*)
3.1797 - scrstate (*after determination of stac WN.18.8.03*)
3.1798 - | Napp of (*stac found was not applicable;
3.1799 - this mode may become Skip in Repeat, Try and Or*)
3.1800 - env (*stack*) (*popped while nxt_up*)
3.1801 - | Skip of (*for restart after Appy, for leaving iterations,
3.1802 - for passing the value of scriptexpressions,
3.1803 - and for finishing the script successfully*)
3.1804 - term * env (*stack*);
3.1805 -
3.1806 (*appy, nxt_up, nstep_up scanning for next_tac.
3.1807 search is clearly separated into (1)-(2):
3.1808 (1) appy is recursive descent;
3.1809 @@ -1234,210 +836,170 @@
3.1810 * call of (2) means _always_ that in this branch below
3.1811 there was an applicable stac (Repeat, Or e1, ...)
3.1812 *)
3.1813 +datatype appy = (* ExprVal in the sense of denotational semantics *)
3.1814 + Appy of (* applicable stac found, search stalled *)
3.1815 + tac_ * (* tac_ associated (fun assod) with stac *)
3.1816 + scrstate (* after determination of stac WN.18.8.03 *)
3.1817 + | Napp of (* stac found was not applicable;
3.1818 + this mode may become Skip in Repeat, Try and Or *)
3.1819 + env (*stack*)(* popped while nxt_up *)
3.1820 + | Skip of (* for restart after Appy, for leaving iterations,
3.1821 + for passing the value of scriptexpressions,
3.1822 + and for finishing the script successfully *)
3.1823 + term * env (*stack*);
3.1824
3.1825 +datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
3.1826 +(*Appy is only (final) returnvalue, not argument during search *)
3.1827 + Napp_ (* ev. detects 'script is not appropriate for this example' *)
3.1828 +| Skip_; (* detects 'script successfully finished'
3.1829 + also used as init-value for resuming; this works,
3.1830 + because 'nxt_up Or e1' treats as Appy *)
3.1831
3.1832 -datatype appy_ = (*as argument in nxt_up, nstep_up, from appy*)
3.1833 - (* Appy is only (final) returnvalue, not argument during search *)
3.1834 - Napp_ (*ev. detects 'script is not appropriate for this example'*)
3.1835 - | Skip_; (*detects 'script successfully finished'
3.1836 - also used as init-value for resuming; this works,
3.1837 - because 'nxt_up Or e1' treats as Appy*)
3.1838 -
3.1839 -fun appy thy ptp E l (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
3.1840 - (case appy thy ptp E (l@[L,R]) e a v of
3.1841 - Skip (res, E) =>
3.1842 - let val E' = upd_env E (Free (i,T), res);
3.1843 - in appy thy ptp E' (l@[R,D]) b a v end
3.1844 - | ay => ay)
3.1845 -
3.1846 - | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
3.1847 - (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
3.1848 - then appy thy ptp E (l@[L,R]) e (SOME a) v
3.1849 - else Skip (v, E))
3.1850 -
3.1851 - | appy (thy as (th,sr)) ptp E l (t as Const ("Script.While"(*2*),_) $ c $ e) a v =
3.1852 - (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1853 - then appy thy ptp E (l@[R]) e a v
3.1854 - else Skip (v, E))
3.1855 -
3.1856 - | appy (thy as (th,sr)) ptp E l (t as Const ("If",_) $ c $ e1 $ e2) a v =
3.1857 - (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1858 - then ((*tracing("### appy If: true");*)appy thy ptp E (l@[L,R]) e1 a v)
3.1859 - else ((*tracing("### appy If: false");*)appy thy ptp E (l@[ R]) e2 a v))
3.1860 -
3.1861 +fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
3.1862 + (case appy thy ptp E (l @ [L, R]) e a v of
3.1863 + Skip (res, E) =>
3.1864 + let val E' = upd_env E (Free (i,T), res);
3.1865 + in appy thy ptp E' (l @ [R, D]) b a v end
3.1866 + | ay => ay)
3.1867 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
3.1868 + (if eval_true_ th sr (subst_atomic (upd_env E (a,v)) c)
3.1869 + then appy thy ptp E (l @ [L, R]) e (SOME a) v
3.1870 + else Skip (v, E))
3.1871 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
3.1872 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1873 + then appy thy ptp E (l @ [R]) e a v
3.1874 + else Skip (v, E))
3.1875 + | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =
3.1876 + (if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1877 + then appy thy ptp E (l @ [L, R]) e1 a v
3.1878 + else appy thy ptp E (l @ [R]) e2 a v)
3.1879 | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
3.1880 - (appy thy ptp E (l@[L,R]) e (SOME a) v)
3.1881 -
3.1882 - | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v =
3.1883 - (appy thy ptp E (l@[R]) e a v)
3.1884 -
3.1885 - | appy thy ptp E l (t as Const ("Script.Try",_) $ e $ a) _ v =
3.1886 - (case appy thy ptp E (l@[L,R]) e (SOME a) v of
3.1887 - Napp E => (Skip (v, E))
3.1888 - | ay => ay)
3.1889 -
3.1890 - | appy thy ptp E l(t as Const ("Script.Try",_) $ e) a v =
3.1891 - (case appy thy ptp E (l@[R]) e a v of
3.1892 - Napp E => (Skip (v, E))
3.1893 - | ay => ay)
3.1894 -
3.1895 + appy thy ptp E (l @ [L, R]) e (SOME a) v
3.1896 + | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [R]) e a v
3.1897 + | appy thy ptp E l (Const ("Script.Try",_) $ e $ a) _ v =
3.1898 + (case appy thy ptp E (l @ [L, R]) e (SOME a) v of
3.1899 + Napp E => (Skip (v, E))
3.1900 + | ay => ay)
3.1901 + | appy thy ptp E l(Const ("Script.Try",_) $ e) a v =
3.1902 + (case appy thy ptp E (l @ [R]) e a v of
3.1903 + Napp E => (Skip (v, E))
3.1904 + | ay => ay)
3.1905 | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
3.1906 - (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
3.1907 - Appy lme => Appy lme
3.1908 - | _ => appy thy ptp E (*env*) (l@[L,R]) e2 (SOME a) v)
3.1909 -
3.1910 + (case appy thy ptp E (l @ [L, L, R]) e1 (SOME a) v of
3.1911 + Appy lme => Appy lme
3.1912 + | _ => appy thy ptp E (*env*) (l @ [L, R]) e2 (SOME a) v)
3.1913 | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
3.1914 - (case appy thy ptp E (l@[L,R]) e1 a v of
3.1915 - Appy lme => Appy lme
3.1916 - | _ => appy thy ptp E (l@[R]) e2 a v)
3.1917 -
3.1918 + (case appy thy ptp E (l @ [L, R]) e1 a v of
3.1919 + Appy lme => Appy lme
3.1920 + | _ => appy thy ptp E (l @ [R]) e2 a v)
3.1921 | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2 $ a) _ v =
3.1922 - (case appy thy ptp E (l@[L,L,R]) e1 (SOME a) v of
3.1923 - Skip (v,E) => appy thy ptp E (l@[L,R]) e2 (SOME a) v
3.1924 - | ay => ay)
3.1925 -
3.1926 + (case appy thy ptp E (l @ [L, L, R]) e1 (SOME a) v of
3.1927 + Skip (v,E) => appy thy ptp E (l @ [L, R]) e2 (SOME a) v
3.1928 + | ay => ay)
3.1929 | appy thy ptp E l (Const ("Script.Seq",_) $ e1 $ e2) a v =
3.1930 - (case appy thy ptp E (l@[L,R]) e1 a v of
3.1931 - Skip (v,E) => appy thy ptp E (l@[R]) e2 a v
3.1932 - | ay => ay)
3.1933 -
3.1934 + (case appy thy ptp E (l @ [L,R]) e1 a v of
3.1935 + Skip (v,E) => appy thy ptp E (l @ [R]) e2 a v
3.1936 + | ay => ay)
3.1937 (* a leaf has been found *)
3.1938 - | appy (thy as (th,sr)) (pt, p) E l t a v =
3.1939 - (case handle_leaf "next " th sr E a v t of
3.1940 - (a', Expr s) => Skip (s, E)
3.1941 - | (a', STac stac) =>
3.1942 - let val (m,m') = stac2tac_ pt (assoc_thy th) stac
3.1943 - in
3.1944 - case m of
3.1945 - Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
3.1946 - | _ =>
3.1947 - (case applicable_in p pt m of
3.1948 - Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
3.1949 - | _ => ((*tracing("### appy: Napp");*)Napp E))
3.1950 - end);
3.1951 -
3.1952 -fun nxt_up thy ptp (scr as (Prog sc)) E l ay
3.1953 - (t as Const ("HOL.Let",_) $ _) a v = (*comes from let=...*)
3.1954 - (if ay = Napp_
3.1955 - then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.1956 - else (*Skip_*)
3.1957 - let
3.1958 - val up = drop_last l;
3.1959 - val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
3.1960 - val i = mk_Free (i, T);
3.1961 - val E = upd_env E (i, v);
3.1962 - in
3.1963 - case appy thy ptp E (up@[R,D]) body a v of
3.1964 - Appy lre => Appy lre
3.1965 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.1966 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end)
3.1967 -
3.1968 - | nxt_up thy ptp scr E l ay
3.1969 - (t as Abs (_,_,_)) a v =
3.1970 - ((*tracing("### nxt_up Abs: " ^ term2str t);*)
3.1971 - nstep_up thy ptp scr E l ay a v)
3.1972 -
3.1973 - | nxt_up thy ptp scr E l ay
3.1974 - (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
3.1975 - ((*tracing("### nxt_up Let$e$Abs: is=");
3.1976 - tracing(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
3.1977 - (*tracing("### nxt_up Let e Abs: " ^ term2str t);*)
3.1978 - nstep_up thy ptp scr E l ay a v)
3.1979 -
3.1980 - (*no appy_: never causes Napp -> Helpless*)
3.1981 - | nxt_up (thy as (th,sr)) ptp scr E l _
3.1982 - (Const ("Script.While"(*1*),_) $ c $ e $ _) a v =
3.1983 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1984 - then case appy thy ptp E (l@[L,R]) e a v of
3.1985 - Appy lr => Appy lr
3.1986 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.1987 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.1988 - else nstep_up thy ptp scr E l Skip_ a v
3.1989 -
3.1990 - (*no appy_: never causes Napp - Helpless*)
3.1991 - | nxt_up (thy as (th,sr)) ptp scr E l _
3.1992 - (Const ("Script.While"(*2*),_) $ c $ e) a v =
3.1993 - if eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.1994 - then case appy thy ptp E (l@[R]) e a v of
3.1995 - Appy lr => Appy lr
3.1996 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.1997 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.1998 - else nstep_up thy ptp scr E l Skip_ a v
3.1999 -
3.2000 - | nxt_up thy ptp scr E l ay (Const ("If",_) $ _ $ _ $ _) a v =
3.2001 - nstep_up thy ptp scr E l ay a v
3.2002 -
3.2003 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.2004 - (Const ("Script.Repeat"(*1*),T) $ e $ _) a v =
3.2005 - (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[L,R]):loc_) e a v of
3.2006 - Appy lr => Appy lr
3.2007 - | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
3.2008 - nstep_up thy ptp scr E l Skip_ a v)
3.2009 - | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
3.2010 - (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
3.2011 - nstep_up thy ptp scr E l Skip_ a v))
3.2012 -
3.2013 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.2014 - (Const ("Script.Repeat"(*2*),T) $ e) a v =
3.2015 - (case appy thy ptp (*upd_env*) E (*a,v)*) ((l@[R]):loc_) e a v of
3.2016 - Appy lr => Appy lr
3.2017 - | Napp E => ((*tracing("### nxt_up Repeat a: ");*)
3.2018 - nstep_up thy ptp scr E l Skip_ a v)
3.2019 - | Skip (v,E) => ((*tracing("### nxt_up Repeat: Skip res ="^
3.2020 - (Sign.string_of_term(sign_of (assoc_thy thy)) res'));*)
3.2021 - nstep_up thy ptp scr E l Skip_ a v))
3.2022 -
3.2023 - | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
3.2024 - (t as Const ("Script.Try",_) $ e $ _) a v =
3.2025 - ((*tracing("### nxt_up Try " ^ term2str t);*)
3.2026 - nstep_up thy ptp scr E l Skip_ a v )
3.2027 -
3.2028 - | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
3.2029 - (t as Const ("Script.Try"(*2*),_) $ e) a v =
3.2030 - ((*tracing("### nxt_up Try " ^ term2str t);*)
3.2031 - nstep_up thy ptp scr E l Skip_ a v)
3.2032 -
3.2033 -
3.2034 - | nxt_up thy ptp scr E l ay
3.2035 - (Const ("Script.Or",_) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.2036 -
3.2037 - | nxt_up thy ptp scr E l ay
3.2038 - (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.2039 -
3.2040 - | nxt_up thy ptp scr E l ay
3.2041 - (Const ("Script.Or",_) $ _ ) a v =
3.2042 - nstep_up thy ptp scr E (drop_last l) ay a v
3.2043 -
3.2044 - | nxt_up thy ptp scr E l ay (*all has been done in (*2*) below*)
3.2045 - (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
3.2046 - nstep_up thy ptp scr E l ay a v
3.2047 -
3.2048 - | nxt_up thy ptp scr E l ay (*comes from e2*)
3.2049 - (Const ("Script.Seq"(*2*),_) $ _ $ e2) a v =
3.2050 - nstep_up thy ptp scr E l ay a v
3.2051 -
3.2052 - | nxt_up thy ptp (scr as Prog sc) E l ay (*comes from e1*)
3.2053 - (Const ("Script.Seq",_) $ _) a v =
3.2054 + | appy ((th,sr)) (pt, p) E l t a v =
3.2055 + case handle_leaf "next " th sr E a v t of
3.2056 + (_, Expr s) => Skip (s, E)
3.2057 + | (a', STac stac) =>
3.2058 + let val (m,m') = stac2tac_ pt (assoc_thy th) stac
3.2059 + in case m of
3.2060 + Subproblem _ => Appy (m', (E,l,a',tac_2res m',Sundef,false))
3.2061 + | _ =>
3.2062 + (case applicable_in p pt m of
3.2063 + Appl m' => (Appy (m', (E,l,a',tac_2res m',Sundef,false)))
3.2064 + | _ => Napp E)
3.2065 + end
3.2066 +(*GOON*)
3.2067 +fun nxt_up thy ptp (scr as (Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
3.2068 if ay = Napp_
3.2069 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.2070 else (*Skip_*)
3.2071 - let val up = drop_last l;
3.2072 - val Const ("Script.Seq"(*2*),_) $ _ $ e2 = go up sc;
3.2073 - in case appy thy ptp E (up@[R]) e2 a v of
3.2074 + let
3.2075 + val up = drop_last l
3.2076 + val (i, T, body) =
3.2077 + (case go up sc of
3.2078 + Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
3.2079 + | t => error ("nxt_up..HOL.Let $ _ with " ^ term2str t))
3.2080 + val i = mk_Free (i, T)
3.2081 + val E = upd_env E (i, v)
3.2082 + in
3.2083 + case appy thy ptp E (up @ [R,D]) body a v of
3.2084 + Appy lre => Appy lre
3.2085 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.2086 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v
3.2087 + end
3.2088 + | nxt_up thy ptp scr E l ay (Abs _) a v = nstep_up thy ptp scr E l ay a v
3.2089 + | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =
3.2090 + nstep_up thy ptp scr E l ay a v
3.2091 + (*no appy_: never causes Napp -> Helpless*)
3.2092 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v =
3.2093 + if eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
3.2094 + then case appy thy ptp E (l @ [L,R]) e a v of
3.2095 + Appy lr => Appy lr
3.2096 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.2097 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.2098 + else nstep_up thy ptp scr E l Skip_ a v
3.2099 + (*no appy_: never causes Napp - Helpless*)
3.2100 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v =
3.2101 + if eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
3.2102 + then case appy thy ptp E (l @ [R]) e a v of
3.2103 Appy lr => Appy lr
3.2104 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.2105 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
3.2106 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.2107 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.2108 + else nstep_up thy ptp scr E l Skip_ a v
3.2109 + | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.2110 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.2111 + (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =
3.2112 + (case appy thy ptp (*upd_env*) E (*a,v)*) ((l @ [L, R]):loc_) e a v of
3.2113 + Appy lr => Appy lr
3.2114 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.2115 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.2116 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.2117 + (Const ("Script.Repeat"(*2*), _) $ e) a v =
3.2118 + (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [R]) e a v of
3.2119 + Appy lr => Appy lr
3.2120 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.2121 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.2122 + | nxt_up thy ptp scr E l _ (Const ("Script.Try",_) $ _ $ _) a v = (*makes Napp to Skip*)
3.2123 + nstep_up thy ptp scr E l Skip_ a v
3.2124
3.2125 - | nxt_up (thy,_) ptp scr E l ay t a v = error ("nxt_up not impl for " ^ term2str t)
3.2126 -
3.2127 + | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*), _) $ _) a v = (*makes Napp to Skip*)
3.2128 + nstep_up thy ptp scr E l Skip_ a v
3.2129 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =
3.2130 + nstep_up thy ptp scr E l ay a v
3.2131 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.2132 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
3.2133 + nstep_up thy ptp scr E (drop_last l) ay a v
3.2134 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
3.2135 + (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
3.2136 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
3.2137 + nstep_up thy ptp scr E l ay a v
3.2138 + | nxt_up thy ptp (scr as Prog sc) E l ay (Const ("Script.Seq",_) $ _) a v = (*comes from e1*)
3.2139 + if ay = Napp_
3.2140 + then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.2141 + else (*Skip_*)
3.2142 + let val up = drop_last l;
3.2143 + val e2 =
3.2144 + (case go up sc of
3.2145 + Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2
3.2146 + | t => error ("nxt_up..Script.Seq $ _ with " ^ term2str t))
3.2147 + in case appy thy ptp E (up @ [R]) e2 a v of
3.2148 + Appy lr => Appy lr
3.2149 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.2150 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
3.2151 + | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ term2str t)
3.2152 and nstep_up thy ptp (Prog sc) E l ay a v =
3.2153 - (if 1 < length l
3.2154 - then
3.2155 - let val up = drop_last l;
3.2156 - in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
3.2157 - else (*interpreted to end*)
3.2158 - if ay = Skip_ then Skip (v, E) else Napp E
3.2159 -);
3.2160 + if 1 < length l
3.2161 + then
3.2162 + let val up = drop_last l;
3.2163 + in (nxt_up thy ptp (Prog sc) E up ay (go up sc) a v ) end
3.2164 + else (*interpreted to end*)
3.2165 + if ay = Skip_ then Skip (v, E) else Napp E
3.2166 + | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ loc_2str l)
3.2167
3.2168 (* decide for the next applicable stac in the script;
3.2169 returns (stactic, value) - the value in case the script is finished
3.2170 @@ -1449,19 +1011,18 @@
3.2171 (.. not true for other details ..PrfObj ??????????????????
3.2172 20.8.02: do NOT return safe (is only changed in locate !!!)
3.2173 *)
3.2174 -fun next_tac (thy,_) (pt,p) (Rfuns {next_rule,...}) (RrlsState(f,f',rss,_), ctxt) =
3.2175 +fun next_tac (thy,_) _ (Rfuns {next_rule, ...}) (RrlsState(f, f', rss, _), ctxt) =
3.2176 if f = f'
3.2177 then (End_Detail' (f',[])(*8.6.03*), (Uistate, ctxt),
3.2178 (f', Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
3.2179 else
3.2180 (case next_rule rss f of
3.2181 - NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
3.2182 - | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
3.2183 - (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
3.2184 - (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
3.2185 -
3.2186 - | next_tac thy (ptp as (pt, pos as (p, _)):ptree * pos') (sc as Prog (h $ body))
3.2187 - (ScrState (E,l,a,v,s,b), ctxt) =
3.2188 + NONE => (Empty_Tac_, (Uistate, ctxt), (e_term, Sundef)) (*helpless*)
3.2189 + | SOME (Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
3.2190 + (Rewrite' (thy, "e_rew_ord", e_rls, false, thm'', f, (e_term, [(*!?!8.6.03*)])),
3.2191 + (Uistate, ctxt), (e_term, Sundef))) (*next stac*)
3.2192 + | next_tac thy (ptp as (pt, (p, _)):ptree * pos') (sc as Prog (_ $ body))
3.2193 + (ScrState (E,l,a,v,s,_), ctxt) =
3.2194 (case if l = [] then appy thy ptp E [R] body NONE v
3.2195 else nstep_up thy ptp sc E l Skip_ a v of
3.2196 Skip (v, _) => (*finished*)
3.2197 @@ -1472,106 +1033,103 @@
3.2198 in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
3.2199 (e_istate, ctxt), (v,s))
3.2200 end
3.2201 - | (_, p', rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
3.2202 + | _ => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
3.2203 | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
3.2204 | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, ctxt), (v, Sundef))) (*next stac*)
3.2205 -
3.2206 | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
3.2207
3.2208 -
3.2209 (*.create the initial interpreter state from the items of the guard.*)
3.2210 +local
3.2211 val errmsg = "ERROR: found no actual arguments for prog. of "
3.2212 +fun msg_miss (sc, metID, formals, actuals) =
3.2213 + "ERROR in creating the environment for '" ^ id_of_scr sc ^
3.2214 + "' from \nthe items of the guard of " ^ metID2str metID ^ ",\n" ^
3.2215 + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
3.2216 + (string_of_int o length) formals ^ " formals: " ^ terms2str formals ^ "\n" ^
3.2217 + (string_of_int o length) actuals ^ " actuals: " ^ terms2str actuals
3.2218 +fun msg_type (sc, metID, a, f, formals, actuals) =
3.2219 + "ERROR in creating the environment for '" ^
3.2220 + id_of_scr sc ^ "' from \nthe items of the guard of " ^
3.2221 + metID2str metID ^ ",\n" ^
3.2222 + "different types of formal arg, from the script, " ^
3.2223 + "and actual arg, from the guards env:'\n" ^
3.2224 + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
3.2225 + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
3.2226 + "in\n" ^
3.2227 + "formals: " ^ terms2str formals ^ "\n" ^
3.2228 + "actuals: " ^ terms2str actuals
3.2229 +in
3.2230 fun init_scrstate thy itms metID =
3.2231 let
3.2232 val actuals = itms2args thy metID itms
3.2233 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
3.2234 - val scr as Prog sc = (#scr o get_met) metID
3.2235 + val (scr, sc) = (case (#scr o get_met) metID of
3.2236 + scr as Prog sc => (scr, sc) | _ => raise ERROR ("init_scrstate with " ^ metID2str metID))
3.2237 val formals = formal_args sc
3.2238 (*expects same sequence of (actual) args in itms and (formal) args in met*)
3.2239 fun relate_args env [] [] = env
3.2240 - | relate_args env _ [] =
3.2241 - error ("ERROR in creating the environment for '" ^
3.2242 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
3.2243 - metID2str metID ^ ",\n" ^
3.2244 - "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
3.2245 - (string_of_int o length) formals ^
3.2246 - " formals: " ^ terms2str formals ^ "\n" ^
3.2247 - (string_of_int o length) actuals ^
3.2248 - " actuals: " ^ terms2str actuals)
3.2249 - | relate_args env [] actual_finds = env (*may drop Find!*)
3.2250 + | relate_args _ _ [] = error (msg_miss (sc, metID, formals, actuals))
3.2251 + | relate_args env [] _ = env (*may drop Find!*)
3.2252 | relate_args env (a::aa) (f::ff) =
3.2253 - if type_of a = type_of f
3.2254 - then relate_args (env @ [(a, f)]) aa ff
3.2255 - else
3.2256 - error ("ERROR in creating the environment for '" ^
3.2257 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
3.2258 - metID2str metID ^ ",\n" ^
3.2259 - "different types of formal arg, from the script, " ^
3.2260 - "and actual arg, from the guards env:'\n" ^
3.2261 - "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
3.2262 - "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
3.2263 - "in\n" ^
3.2264 - "formals: " ^ terms2str formals ^ "\n" ^
3.2265 - "actuals: " ^ terms2str actuals)
3.2266 - val env = relate_args [] formals actuals;
3.2267 - val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
3.2268 - val {pre, prls, ...} = get_met metID;
3.2269 - val pres = check_preconds thy prls pre itms |> map snd;
3.2270 - val ctxt = ctxt |> insert_assumptions pres;
3.2271 - in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
3.2272 + if type_of a = type_of f
3.2273 + then relate_args (env @ [(a, f)]) aa ff
3.2274 + else error (msg_type (sc, metID, a, f, formals, actuals))
3.2275 + val env = relate_args [] formals actuals;
3.2276 + val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
3.2277 + val {pre, prls, ...} = get_met metID;
3.2278 + val pres = check_preconds thy prls pre itms |> map snd;
3.2279 + val ctxt = ctxt |> insert_assumptions pres;
3.2280 + in (ScrState (env, [], NONE, e_term, Safe, true), ctxt, scr) : istate * Proof.context * scr end;
3.2281 +end (*local*)
3.2282
3.2283 (* decide, where to get script/istate from:
3.2284 - (*1*) from PblObj.env: at begin of script if no init_form
3.2285 - (*2*) from PblObj/PrfObj: if stac is in the middle of the script
3.2286 - (*3*) from rls/PrfObj: in case of detail a ruleset *)
3.2287 -fun from_pblobj_or_detail' thy' (p,p_) pt =
3.2288 - let val ctxt = get_ctxt pt (p,p_)
3.2289 - in
3.2290 - if member op = [Pbl,Met] p_
3.2291 - then case get_obj g_env pt p of
3.2292 - NONE => error "from_pblobj_or_detail': no istate"
3.2293 - | SOME is =>
3.2294 - let
3.2295 - val metID = get_obj g_metID pt p
3.2296 - val {srls,...} = get_met metID
3.2297 - in (srls, is, (#scr o get_met) metID) end
3.2298 - else
3.2299 - let val (pbl,p',rls') = par_pbl_det pt p
3.2300 - in if pbl
3.2301 - then (*2*)
3.2302 - let
3.2303 - val thy = assoc_thy thy'
3.2304 - val PblObj{meth=itms,...} = get_obj I pt p'
3.2305 - val metID = get_obj g_metID pt p'
3.2306 - val {srls,...} = get_met metID
3.2307 - in (*if last_elem p = 0 nothing written to pt yet*)
3.2308 - (srls, get_loc pt (p,p_), (#scr o get_met) metID)
3.2309 - end
3.2310 - else (*3*)
3.2311 - (e_rls, (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*)
3.2312 - get_loc pt (p,p_),
3.2313 - case rls' of
3.2314 - Rls {scr=scr,...} => scr
3.2315 - | Seq {scr=scr,...} => scr
3.2316 - | Rrls {scr=rfuns,...} => rfuns)
3.2317 - end
3.2318 - end;
3.2319 + (* 1 *) from PblObj.env: at begin of script if no init_form
3.2320 + (* 2 *) from PblObj/PrfObj: if stac is in the middle of the script
3.2321 + (* 3 *) from rls/PrfObj: in case of detail a ruleset *)
3.2322 +fun from_pblobj_or_detail' _ (p, p_) pt =
3.2323 + if member op = [Pbl, Met] p_
3.2324 + then case get_obj g_env pt p of
3.2325 + NONE => error "from_pblobj_or_detail': no istate"
3.2326 + | SOME is =>
3.2327 + let
3.2328 + val metID = get_obj g_metID pt p
3.2329 + val {srls, ...} = get_met metID
3.2330 + in (srls, is, (#scr o get_met) metID) end
3.2331 + else
3.2332 + let val (pbl, p', rls') = par_pbl_det pt p
3.2333 + in if pbl
3.2334 + then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
3.2335 + let
3.2336 + val metID = get_obj g_metID pt p'
3.2337 + val {srls,...} = get_met metID
3.2338 + in (srls, get_loc pt (p,p_), (#scr o get_met) metID) end
3.2339 + else (*FIXME.WN0?: get from pbl or met !!! unused for Rrls in locate_gen, next_tac*) (* 3 *)
3.2340 + (e_rls, get_loc pt (p,p_),
3.2341 + case rls' of
3.2342 + Rls {scr = scr,...} => scr
3.2343 + | Seq {scr = scr,...} => scr
3.2344 + | Rrls {scr=rfuns,...} => rfuns
3.2345 + | Erls => error "from_pblobj_or_detail' with Erls")
3.2346 + end
3.2347
3.2348 -(*.get script and istate from PblObj, see (*1*) above.*)
3.2349 +(*.get script and istate from PblObj, see ( * 1 *)
3.2350 fun from_pblobj' thy' (p,p_) pt =
3.2351 let
3.2352 val p' = par_pblobj pt p
3.2353 val thy = assoc_thy thy'
3.2354 - val PblObj {meth=itms, ...} = get_obj I pt p'
3.2355 + val itms =
3.2356 + (case get_obj I pt p' of
3.2357 + PblObj {meth = itms, ...} => itms
3.2358 + | PrfObj _ => error "from_pblobj' NOT with PrfObj")
3.2359 val metID = get_obj g_metID pt p'
3.2360 - val {srls,scr,...} = get_met metID
3.2361 + val {srls, scr, ...} = get_met metID
3.2362 in
3.2363 if last_elem p = 0 (*nothing written to pt yet*)
3.2364 then
3.2365 let val (is, ctxt, scr) = init_scrstate thy itms metID
3.2366 in (srls, (is, ctxt), scr) end
3.2367 - else (srls, get_loc pt (p,p_), scr)
3.2368 - end;
3.2369 + else (srls, get_loc pt (p,p_), scr)
3.2370 + end;
3.2371
3.2372 (*.get the stactics and problems of a script as tacs
3.2373 instantiated with the current environment;
3.2374 @@ -1584,26 +1142,29 @@
3.2375 (*. fetch _all_ tactics from script .*)
3.2376 fun sel_rules _ (([],Res):pos') =
3.2377 raise PTREE "no tactics applicable at the end of a calculation"
3.2378 -| sel_rules pt (p,p_) =
3.2379 - if is_spec_pos p_
3.2380 - then [get_obj g_tac pt p]
3.2381 - else
3.2382 - let val pp = par_pblobj pt p;
3.2383 - val thy' = (get_obj g_domID pt pp):theory';
3.2384 - val thy = assoc_thy thy';
3.2385 - val metID = get_obj g_metID pt pp;
3.2386 - val metID' =if metID =e_metID then(thd3 o snd3)(get_obj g_origin pt pp)
3.2387 - else metID
3.2388 - val {scr = Prog sc,srls,...} = get_met metID'
3.2389 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_);
3.2390 - in map ((stac2tac pt thy) o rep_stacexpr o #2 o
3.2391 - (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc) end;
3.2392 + | sel_rules pt (p,p_) =
3.2393 + if is_spec_pos p_
3.2394 + then [get_obj g_tac pt p]
3.2395 + else
3.2396 + let
3.2397 + val pp = par_pblobj pt p;
3.2398 + val thy' = (get_obj g_domID pt pp):theory';
3.2399 + val thy = assoc_thy thy';
3.2400 + val metID = get_obj g_metID pt pp;
3.2401 + val metID' = if metID =e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
3.2402 + val (sc, srls) = (case get_met metID' of
3.2403 + {scr = Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
3.2404 + val (env, a, v) = (case get_istate pt (p, p_) of
3.2405 + ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_rules 2")
3.2406 + in map ((stac2tac pt thy) o rep_stacexpr o #2 o
3.2407 + (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
3.2408 + end;
3.2409
3.2410 (*. fetch tactics from script and filter _applicable_ tactics;
3.2411 in case of Rewrite_Set* go down to _atomic_ rewrite-tactics .*)
3.2412 -fun sel_appl_atomic_tacs _ (([],Res):pos') =
3.2413 +fun sel_appl_atomic_tacs _ (([], Res) : pos') =
3.2414 raise PTREE "no tactics applicable at the end of a calculation"
3.2415 - | sel_appl_atomic_tacs pt (p,p_) =
3.2416 + | sel_appl_atomic_tacs pt (p, p_) =
3.2417 if is_spec_pos p_
3.2418 then [get_obj g_tac pt p]
3.2419 else
3.2420 @@ -1616,24 +1177,20 @@
3.2421 if metID = e_metID
3.2422 then (thd3 o snd3) (get_obj g_origin pt pp)
3.2423 else metID
3.2424 - val {scr = Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
3.2425 - val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
3.2426 + val (sc, srls, erls, ro) = (case get_met metID' of
3.2427 + {scr = Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
3.2428 + | _ => error "sel_appl_atomic_tacs 1")
3.2429 + val (env, a, v) = (case get_istate pt (p, p_) of
3.2430 + ScrState (env, _, a, v, _, _) => (env, a, v) | _ => error "sel_appl_atomic_tacs 2")
3.2431 val alltacs = (*we expect at least 1 stac in a script*)
3.2432 map ((stac2tac pt thy) o rep_stacexpr o #2 o
3.2433 (handle_leaf "selrul" thy' srls env a v)) (stacpbls sc)
3.2434 val f =
3.2435 - case p_ of
3.2436 - Frm => get_obj g_form pt p
3.2437 - | Res => (fst o (get_obj g_result pt)) p
3.2438 + (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
3.2439 + | _ => error "")
3.2440 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
3.2441 in ((gen_distinct eq_tac) o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs end;
3.2442 -
3.2443 -
3.2444 -(*
3.2445 +(**)
3.2446 end
3.2447 -open Interpreter;
3.2448 -*)
3.2449 -
3.2450 -(* use"ME/script.sml";
3.2451 - use"script.sml";
3.2452 - *)
3.2453 +(**)
3.2454 +(*open Lucin;*)
4.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Oct 27 10:48:24 2016 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve.sml Sat Nov 12 17:21:43 2016 +0100
4.3 @@ -134,8 +134,8 @@
4.4 "-----------------------------------------------------------------------";
4.5
4.6
4.7 -fun step2taci ((tac_, _, pt, p, _):step) = (*FIXXME.040312: redesign step*)
4.8 - (tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
4.9 +fun step2taci ((tac_, _, pt, p, _) : Lucin.step) = (*FIXXME.040312: redesign step*)
4.10 + (Lucin.tac_2tac tac_, tac_, (p, get_loc pt p)):taci;
4.11
4.12
4.13 (*FIXME.WN050821 compare solve ... nxt_solv*)
4.14 @@ -147,8 +147,8 @@
4.15 val PblObj {meth=itms, ...} = get_obj I pt p;
4.16 val thy' = get_obj g_domID pt p;
4.17 val thy = assoc_thy thy';
4.18 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
4.19 - val ini = init_form thy sc env;
4.20 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = Lucin.init_scrstate thy itms mI;
4.21 + val ini = Lucin.init_form thy sc env;
4.22 val p = lev_dn p;
4.23 in
4.24 case ini of
4.25 @@ -161,16 +161,17 @@
4.26 end
4.27 | NONE => (*execute the first tac in the Script, compare solve m*)
4.28 let
4.29 - val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
4.30 + val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
4.31 val d = e_rls (*FIXME: get simplifier from domID*);
4.32 in
4.33 - case locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
4.34 - Steps (is'', ss as (m'',f',pt',p',c')::_) =>
4.35 + case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
4.36 + Lucin.Steps (is'', ss as (m'',f',pt',p',c')::_) =>
4.37 ("ok", (map step2taci ss, c', (pt',p')))
4.38 | NotLocatable =>
4.39 - let val (p,ps,f,pt) =
4.40 - generate_hard (assoc_thy "Isac") m (p,Frm) pt;
4.41 - in ("not-found-in-script", ([(tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p))) end
4.42 + let val (p,ps,f,pt) = generate_hard (assoc_thy "Isac") m (p,Frm) pt;
4.43 + in
4.44 + ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt,p)))
4.45 + end
4.46 end
4.47 end
4.48
4.49 @@ -195,7 +196,7 @@
4.50 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
4.51 val thy' = get_obj g_domID pt pp;
4.52 val thy = assoc_thy thy';
4.53 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
4.54 + val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
4.55 in
4.56 if pp = []
4.57 then
4.58 @@ -233,8 +234,8 @@
4.59 val r = (fst o (get_obj g_result pt)) p'
4.60 (*Rewrite_Set* done at Detail_Set*: this result is already in ptree*)
4.61 val thy' = get_obj g_domID pt pp
4.62 - val (srls, is, sc) = from_pblobj' thy' pr pt
4.63 - val (tac_,is',_) = next_tac (thy',srls) (pt,pr) sc is
4.64 + val (srls, is, sc) = Lucin.from_pblobj' thy' pr pt
4.65 + val (tac_,is',_) = Lucin.next_tac (thy',srls) (pt,pr) sc is
4.66 in ("ok", ([(End_Detail, End_Detail' t ,
4.67 ((p,p_), get_loc pt (p,p_)))], [], (pt,pr)))
4.68 end
4.69 @@ -253,11 +254,11 @@
4.70 else
4.71 let
4.72 val thy' = get_obj g_domID pt (par_pblobj pt p);
4.73 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
4.74 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
4.75 val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
4.76 in
4.77 - case locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
4.78 - Steps (is', ss as (m',f',pt',p',c')::_) =>
4.79 + case Lucin.locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is of
4.80 + Lucin.Steps (is', ss as (m',f',pt',p',c')::_) =>
4.81 let
4.82 (*27.8.02:next_tac may change to other branches in pt FIXXXXME*)
4.83 in ("ok", (map step2taci ss, c', (pt',p'))) end
4.84 @@ -265,7 +266,7 @@
4.85 let val (p,ps,f,pt) =
4.86 generate_hard (assoc_thy "Isac") m (p,p_) pt;
4.87 in ("not-found-in-script",
4.88 - ([(tac_2tac m, m, (po,is))], ps, (pt,p)))
4.89 + ([(Lucin.tac_2tac m, m, (po,is))], ps, (pt,p)))
4.90 end
4.91 end;
4.92
4.93 @@ -278,8 +279,8 @@
4.94 val itms = if itms <> [] then itms else complete_metitms oris probl [] ppc
4.95 val thy' = get_obj g_domID pt p;
4.96 val thy = assoc_thy thy';
4.97 - val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = init_scrstate thy itms mI;
4.98 - val ini = init_form thy scr env;
4.99 + val (is as ScrState (env,_,_,_,_,_), ctxt, scr) = Lucin.init_scrstate thy itms mI;
4.100 + val ini = Lucin.init_form thy scr env;
4.101 in
4.102 case ini of
4.103 SOME t =>
4.104 @@ -314,7 +315,7 @@
4.105 val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
4.106 val thy' = get_obj g_domID pt pp;
4.107 val thy = assoc_thy thy';
4.108 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
4.109 + val (_,_,(scval,scsaf)) = Lucin.next_tac (thy',srls) (pt,(p,p_)) sc loc;
4.110 in
4.111 if pp = []
4.112 then
4.113 @@ -349,7 +350,7 @@
4.114 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
4.115 | _ => pos
4.116 val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
4.117 - in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
4.118 + in ([(Lucin.tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
4.119
4.120 (* find the next tac from the script, nxt_solv will update the ptree *)
4.121 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
4.122 @@ -358,8 +359,8 @@
4.123 else
4.124 let
4.125 val thy' = get_obj g_domID pt (par_pblobj pt p);
4.126 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
4.127 - val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
4.128 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
4.129 + val (tac_,is,(t,_)) = Lucin.next_tac (thy',srls) (pt,pos) sc is;
4.130 (*TODO here ^^^ return finished/helpless/ok !*)
4.131 in case tac_ of
4.132 End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]),
5.1 --- a/src/Tools/isac/calcelems.sml Thu Oct 27 10:48:24 2016 +0200
5.2 +++ b/src/Tools/isac/calcelems.sml Sat Nov 12 17:21:43 2016 +0100
5.3 @@ -135,7 +135,8 @@
5.4 | Rls_ of rls (*.ie. rule sets may be nested.*)
5.5 and scr =
5.6 EmptyScr
5.7 - | Prog of term (* for met *)
5.8 + | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr'
5.9 + where 'exp' does not contain a tactic. *)
5.10 | Rfuns of (* for Rrls, usage see rational.sml ----- reverse rewrite ----- *)
5.11 {init_state : (* initialise for reverse rewriting by the Interpreter *)
5.12 term -> (* for this the rrlsstate is initialised: *)
6.1 --- a/test/Tools/isac/Interpret/script.sml Thu Oct 27 10:48:24 2016 +0200
6.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Nov 12 17:21:43 2016 +0100
6.3 @@ -14,6 +14,12 @@
6.4 "----------- 'trace_script' from outside 'fun me '----------------";
6.5 "----------- fun sel_rules ---------------------------------------";
6.6 "----------- fun sel_appl_atomic_tacs ----------------------------";
6.7 +"----------- fun de_esc_underscore -------------------------------";
6.8 +"----------- fun go ----------------------------------------------";
6.9 +"----------- fun formal_args -------------------------------------";
6.10 +"----------- fun dsc_valT ----------------------------------------";
6.11 +"----------- fun itms2args ---------------------------------------";
6.12 +"----------- fun rep_tac_ ----------------------------------------";
6.13 "-----------------------------------------------------------------";
6.14 "-----------------------------------------------------------------";
6.15 "-----------------------------------------------------------------";
6.16 @@ -570,7 +576,7 @@
6.17 val f =
6.18 case p_ of
6.19 Frm => get_obj g_form pt p
6.20 - | Res => (fst o (get_obj g_result pt)) p
6.21 + | Res => (fst o (get_obj g_result pt)) p;
6.22 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
6.23 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
6.24 ...
6.25 @@ -578,3 +584,169 @@
6.26 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
6.27 *)
6.28
6.29 +"----------- fun de_esc_underscore -------------------------------";
6.30 +"----------- fun de_esc_underscore -------------------------------";
6.31 +"----------- fun de_esc_underscore -------------------------------";
6.32 +(*
6.33 +> val str = "Rewrite_Set_Inst";
6.34 +> val esc = esc_underscore str;
6.35 +val it = "Rewrite'_Set'_Inst" : string
6.36 +> val des = de_esc_underscore esc;
6.37 + val des = de_esc_underscore esc;*)
6.38 +
6.39 +"----------- fun go ----------------------------------------------";
6.40 +"----------- fun go ----------------------------------------------";
6.41 +"----------- fun go ----------------------------------------------";
6.42 +(*
6.43 +> val t = (Thm.term_of o the o (parse thy)) "a+b";
6.44 +val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
6.45 +> val plus_a = go [L] t;
6.46 +> val b = go [R] t;
6.47 +> val plus = go [L,L] t;
6.48 +> val a = go [L,R] t;
6.49 +
6.50 +> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
6.51 +val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
6.52 +> val pl_pl_a_b = go [L] t;
6.53 +> val c = go [R] t;
6.54 +> val a = go [L,R,L,R] t;
6.55 +> val b = go [L,R,R] t;
6.56 +*)
6.57 +
6.58 +"----------- fun formal_args -------------------------------------";
6.59 +"----------- fun formal_args -------------------------------------";
6.60 +"----------- fun formal_args -------------------------------------";
6.61 +(*
6.62 +> formal_args scr;
6.63 + [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
6.64 + Free ("eqs_","bool List.list")] : term list
6.65 +*)
6.66 +"----------- fun dsc_valT ----------------------------------------";
6.67 +"----------- fun dsc_valT ----------------------------------------";
6.68 +"----------- fun dsc_valT ----------------------------------------";
6.69 +(*> val t = (Thm.term_of o the o (parse thy)) "equality";
6.70 +> val T = type_of t;
6.71 +val T = "bool => Tools.una" : typ
6.72 +> val dsc = dsc_valT t;
6.73 +val dsc = "una" : string
6.74 +
6.75 +> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
6.76 +> val T = type_of t;
6.77 +val T = "bool List.list => Tools.nam" : typ
6.78 +> val dsc = dsc_valT t;
6.79 +val dsc = "nam" : string*)
6.80 +"----------- fun itms2args ---------------------------------------";
6.81 +"----------- fun itms2args ---------------------------------------";
6.82 +"----------- fun itms2args ---------------------------------------";
6.83 +(*
6.84 +> val sc = ... Solve_root_equation ...
6.85 +> val mI = ("Script","sqrt-equ-test");
6.86 +> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
6.87 +> val ts = itms2args thy mI itms;
6.88 +> map (term_to_string''' thy) ts;
6.89 +["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
6.90 +*)
6.91 +"----------- fun rep_tac_ ----------------------------------------";
6.92 +"----------- fun rep_tac_ ----------------------------------------";
6.93 +"----------- fun rep_tac_ ----------------------------------------";
6.94 +(***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
6.95 +Fehlersuche 25.4.01
6.96 +(a)----- als String zusammensetzen:
6.97 +ML> term2str f;
6.98 +val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
6.99 +ML> term2str f';
6.100 +val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
6.101 +ML> subs;
6.102 +val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
6.103 +> val tt = (Thm.term_of o the o (parse thy))
6.104 + "(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))";
6.105 +> atomty tt;
6.106 +ML> tracing (term2str tt);
6.107 +(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
6.108 + #0 + d_d x (x ^^^ #2 + #3 * x)
6.109 +
6.110 +(b)----- laut rep_tac_:
6.111 +> val ttt=HOLogic.mk_eq (lhs,f');
6.112 +> atomty ttt;
6.113 +
6.114 +
6.115 +(*Fehlersuche 1-2Monate vor 4.01:*)
6.116 +> val tt = (Thm.term_of o the o (parse thy))
6.117 + "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
6.118 +> atomty tt;
6.119 +
6.120 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.121 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.122 +> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
6.123 + (Thm.term_of o the o (parse thy)) "x")];
6.124 +> val sT = (type_of o fst o hd) subs;
6.125 +> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
6.126 + (map HOLogic.mk_prod subs);
6.127 +> val sT' = type_of subs';
6.128 +> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
6.129 + $ subs' $ Free (thmID,idT) $ @{term True} $ f;
6.130 +> lhs = tt;
6.131 +val it = true : bool
6.132 +> rep_tac_ (Rewrite_Inst'
6.133 + ("Script","tless_true","eval_rls",false,subs,
6.134 + ("square_equation_left",""),f,(f',[])));
6.135 +*)
6.136 +(****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
6.137 +> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
6.138 + "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
6.139 +
6.140 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.141 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.142 +> val Thm (id,thm) =
6.143 + rep_tac_ (Rewrite'
6.144 + ("Script","tless_true","eval_rls",false,
6.145 + ("square_equation_left",""),f,(f',[])));
6.146 +> val SOME ct = parse thy
6.147 + "Rewrite square_equation_left True (x=#1+#2)";
6.148 +> rewrite_ Script.thy tless_true eval_rls true thm ct;
6.149 +val it = SOME ("x = #3",[]) : (cterm * cterm list) option
6.150 +*)
6.151 +(**************************************** | rep_tac_ (Rewrite_Set_Inst'
6.152 +WN050824: type error ...
6.153 + let val fT = type_of f;
6.154 + val sT = (type_of o fst o hd) subs;
6.155 + val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
6.156 + (map HOLogic.mk_prod subs);
6.157 + val sT' = type_of subs';
6.158 + val b = if put then @{term True} else @{term False}
6.159 + val lhs = Const ("Script.Rewrite'_Set'_Inst",
6.160 + [sT',idT,fT,fT] ---> fT)
6.161 + $ subs' $ Free (id_rls rls,idT) $ b $ f;
6.162 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
6.163 +(* ... vals from Rewrite_Inst' ...
6.164 +> rep_tac_ (Rewrite_Set_Inst'
6.165 + ("Script",false,subs,
6.166 + "isolate_bdv",f,(f',[])));
6.167 +*)
6.168 +(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
6.169 +*)
6.170 +(************************************** | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
6.171 +13.3.01:
6.172 +val thy = assoc_thy thy';
6.173 +val t = HOLogic.mk_eq (lhs,f');
6.174 +make_rule thy t;
6.175 +--------------------------------------------------
6.176 +val lll = (Thm.term_of o the o (parse thy))
6.177 + "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
6.178 +
6.179 +--------------------------------------------------
6.180 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
6.181 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
6.182 +> val Thm (id,thm) =
6.183 + rep_tac_ (Rewrite_Set'
6.184 + ("Script",false,"SqRoot_simplify",f,(f',[])));
6.185 +val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
6.186 +val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
6.187 +*)
6.188 +(***************************************** | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
6.189 +> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
6.190 + ... test-root-equ.sml: calculate ...
6.191 +> val Appl m'=applicable_in p pt (Calculate "PLUS");
6.192 +> val (lhs,_)=tac_2etac m';
6.193 +> lhs'=lhs;
6.194 +val it = true : bool*)