1.1 --- a/src/Tools/isac/Interpret/Interpret.thy Sun Jun 23 14:44:00 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Mon Jun 24 14:02:39 2019 +0200
1.3 @@ -21,8 +21,9 @@
1.4 ML_file "~~/src/Tools/isac/Interpret/appl.sml"
1.5 ML_file "~~/src/Tools/isac/Interpret/rewtools.sml"
1.6 ML_file "~~/src/Tools/isac/Interpret/script.sml"
1.7 + ML_file "~~/src/Tools/isac/Interpret/inform.sml"
1.8 + ML_file "~~/src/Tools/isac/Interpret/lucas-interpreter.sml"
1.9 ML_file "~~/src/Tools/isac/Interpret/solve.sml"
1.10 - ML_file "~~/src/Tools/isac/Interpret/inform.sml"
1.11 ML_file "~~/src/Tools/isac/Interpret/mathengine.sml"
1.12 (* declare [[ML_print_depth = 999]] *)
1.13 ML \<open>
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jun 24 14:02:39 2019 +0200
2.3 @@ -0,0 +1,268 @@
2.4 +(* Title: Interpret/lucase-interpreter.sml
2.5 + Author: Walther Neuper 2019
2.6 + (c) due to copyright terms
2.7 +*)
2.8 +
2.9 +signature LUCAS_INTERPRETER =
2.10 +sig
2.11 + val next_tac : (*diss: next-tactic-function*)
2.12 + Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
2.13 +
2.14 +end
2.15 +
2.16 +structure LucinNEW(** ): LUCAS_INTERPRETER( **) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)
2.17 +struct
2.18 +open Ctree
2.19 +
2.20 +(*go at a location in a script and fetch the contents*)
2.21 +fun go [] t = t
2.22 + | go (Celem.D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0
2.23 + | go (Celem.L :: p) (t1 $ _) = go p t1
2.24 + | go (Celem.R :: p) (_ $ t2) = go p t2
2.25 + | go l _ = error ("go: no " ^ Celem.loc_2str l);
2.26 +
2.27 +(** find the next stactic in a program **)
2.28 +
2.29 +(* handle a leaf at the end of recursive descent:
2.30 + a leaf is either a tactic or an 'expr' in "let v = expr"
2.31 + where "expr" does not contain a tactic.
2.32 + Handling a leaf comprises
2.33 + (1) 'subst_stacexpr' substitute LTool.env and complete curried tactic
2.34 + (2) rewrite the leaf by 'srls'
2.35 +*)
2.36 +fun handle_leaf call thy srls E a v t =
2.37 + (*WN050916 'upd_env_opt' is a blind copy from previous version*)
2.38 + case LTool.subst_stacexpr E a v t of
2.39 + (a', LTool.STac stac) => (*script-tactic*)
2.40 + let val stac' =
2.41 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Lucin.upd_env_opt E (a,v)) stac)
2.42 + in
2.43 + (if (! trace_script)
2.44 + then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> STac '" ^ Rule.term2str stac ^"'")
2.45 + else ();
2.46 + (a', LTool.STac stac'))
2.47 + end
2.48 + | (a', LTool.Expr lexpr) => (*leaf-expression*)
2.49 + let val lexpr' =
2.50 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Lucin.upd_env_opt E (a,v)) lexpr)
2.51 + in
2.52 + (if (! trace_script)
2.53 + then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t^"' ---> Expr '" ^ Rule.term2str lexpr'^"'")
2.54 + else ();
2.55 + (a', LTool.Expr lexpr')) (*lexpr' is the value of the Expr*)
2.56 + end;
2.57 +
2.58 +(*appy, nxt_up, nstep_up scanning for next_tac.
2.59 + search is clearly separated into (1)-(2):
2.60 + (1) appy is recursive descent;
2.61 + (2) nxt_up resumes interpretation at a location somewhere in the script;
2.62 + nstep_up does only get to the parentnode of the scriptexpr.
2.63 + consequence:
2.64 + * call of (2) means _always_ that in this branch below
2.65 + there was an applicable stac (Repeat, Or e1, ...)
2.66 +*)
2.67 +datatype appy = (* ExprVal in the sense of denotational semantics *)
2.68 + Appy of (* applicable stac found, search stalled *)
2.69 + Tac.tac_ * (* tac_ associated (fun assod) with stac *)
2.70 + Selem.scrstate (* after determination of stac WN.18.8.03 *)
2.71 + | Napp of (* stac found was not applicable;
2.72 + this mode may become Skip in Repeat, Try and Or *)
2.73 + LTool.env (* popped while nxt_up *)
2.74 + | Skip of (* for restart after Appy, for leaving iterations,
2.75 + for passing the value of scriptexpressions,
2.76 + and for finishing the script successfully *)
2.77 + term * LTool.env (*a stack*);
2.78 +
2.79 +datatype appy_ = (* as argument in nxt_up, nstep_up, from appy *)
2.80 +(*Appy is only (final) returnvalue, not argument during search *)
2.81 + Napp_ (* ev. detects 'script is not appropriate for this example' *)
2.82 +| Skip_; (* detects 'script successfully finished'
2.83 + also used as init-value for resuming; this works,
2.84 + because 'nxt_up Or e1' treats as Appy *)
2.85 +
2.86 +fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
2.87 + (case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of
2.88 + Skip (res, E) =>
2.89 + let val E' = LTool.upd_env E (Free (i,T), res);
2.90 + in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end
2.91 + | ay => ay)
2.92 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
2.93 + (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)
2.94 + then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
2.95 + else Skip (v, E))
2.96 + | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
2.97 + (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
2.98 + then appy thy ptp E (l @ [Celem.R]) e a v
2.99 + else Skip (v, E))
2.100 + | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =
2.101 + (if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
2.102 + then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v
2.103 + else appy thy ptp E (l @ [Celem.R]) e2 a v)
2.104 + | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
2.105 + appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
2.106 + | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v
2.107 + | appy thy ptp E l (Const ("Script.Try"(*2*),_) $ e $ a) _ v =
2.108 + (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of
2.109 + Napp E => (Skip (v, E))
2.110 + | ay => ay)
2.111 + | appy thy ptp E l(Const ("Script.Try"(*1*),_) $ e) a v =
2.112 + (case appy thy ptp E (l @ [Celem.R]) e a v of
2.113 + Napp E => (Skip (v, E))
2.114 + | ay => ay)
2.115 + | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
2.116 + (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
2.117 + Appy lme => Appy lme
2.118 + | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)
2.119 + | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
2.120 + (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
2.121 + Appy lme => Appy lme
2.122 + | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)
2.123 + | appy thy ptp E l (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =
2.124 + (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
2.125 + Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v
2.126 + | ay => ay)
2.127 + | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2) a v =
2.128 + (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
2.129 + Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v
2.130 + | ay => ay)
2.131 + (* a leaf has been found *)
2.132 + | appy ((th,sr)) (pt, p) E l t a v =
2.133 + case handle_leaf "next " th sr E a v t of
2.134 + (_, LTool.Expr s) => Skip (s, E)
2.135 + | (a', LTool.STac stac) =>
2.136 + let val (m,m') = Lucin.stac2tac_ pt (Celem.assoc_thy th) stac
2.137 + in case m of
2.138 + Tac.Subproblem _ => Appy (m', (E,l,a',Lucin.tac_2res m',Selem.Sundef,false))
2.139 + | _ =>
2.140 + (case Applicable.applicable_in p pt m of
2.141 + Chead.Appl m' => (Appy (m', (E,l,a',Lucin.tac_2res m',Selem.Sundef,false)))
2.142 + | _ => Napp E)
2.143 + end
2.144 +
2.145 +fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
2.146 + if ay = Napp_
2.147 + then nstep_up thy ptp scr E (drop_last l) Napp_ a v
2.148 + else (*Skip_*)
2.149 + let
2.150 + val up = drop_last l
2.151 + val (i, T, body) =
2.152 + (case go up sc of
2.153 + Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
2.154 + | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))
2.155 + val i = TermC.mk_Free (i, T)
2.156 + val E = LTool.upd_env E (i, v)
2.157 + in
2.158 + case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v of
2.159 + Appy lre => Appy lre
2.160 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
2.161 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v
2.162 + end
2.163 + | nxt_up thy ptp scr E l ay (Abs _) a v = nstep_up thy ptp scr E l ay a v
2.164 + | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =
2.165 + nstep_up thy ptp scr E l ay a v
2.166 + (*no appy_: never causes Napp -> Helpless*)
2.167 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v =
2.168 + if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c)
2.169 + then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of
2.170 + Appy lr => Appy lr
2.171 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
2.172 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
2.173 + else nstep_up thy ptp scr E l Skip_ a v
2.174 + (*no appy_: never causes Napp - Helpless*)
2.175 + | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v =
2.176 + if Rewrite.eval_true_ th sr (subst_atomic (Lucin.upd_env_opt E (a, v)) c)
2.177 + then case appy thy ptp E (l @ [Celem.R]) e a v of
2.178 + Appy lr => Appy lr
2.179 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
2.180 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
2.181 + else nstep_up thy ptp scr E l Skip_ a v
2.182 + | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
2.183 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
2.184 + (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =
2.185 + (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v of
2.186 + Appy lr => Appy lr
2.187 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
2.188 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
2.189 + | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
2.190 + (Const ("Script.Repeat"(*2*), _) $ e) a v =
2.191 + (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v of
2.192 + Appy lr => Appy lr
2.193 + | Napp E => nstep_up thy ptp scr E l Skip_ a v
2.194 + | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
2.195 + | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)
2.196 + nstep_up thy ptp scr E l Skip_ a v
2.197 +
2.198 + | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)
2.199 + nstep_up thy ptp scr E l Skip_ a v
2.200 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =
2.201 + nstep_up thy ptp scr E l ay a v
2.202 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
2.203 + | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
2.204 + nstep_up thy ptp scr E (drop_last l) ay a v
2.205 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
2.206 + (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
2.207 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
2.208 + nstep_up thy ptp scr E l ay a v
2.209 + | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)
2.210 + if ay = Napp_
2.211 + then nstep_up thy ptp scr E (drop_last l) Napp_ a v
2.212 + else (*Skip_*)
2.213 + let val up = drop_last l;
2.214 + val e2 =
2.215 + (case go up sc of
2.216 + Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2
2.217 + | t => error ("nxt_up..Script.Seq $ _ with " ^ Rule.term2str t))
2.218 + in case appy thy ptp E (up @ [Celem.R]) e2 a v of
2.219 + Appy lr => Appy lr
2.220 + | Napp E => nstep_up thy ptp scr E up Napp_ a v
2.221 + | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
2.222 + | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ Rule.term2str t)
2.223 +and nstep_up thy ptp (Rule.Prog sc) E l ay a v =
2.224 + if 1 < length l
2.225 + then
2.226 + let val up = drop_last l;
2.227 + in (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v ) end
2.228 + else (*interpreted to end*)
2.229 + if ay = Skip_ then Skip (v, E) else Napp E
2.230 + | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)
2.231 +
2.232 +(* decide for the next applicable stac in the script;
2.233 + returns (stactic, value) - the value in case the script is finished
2.234 + 12.8.02: ~~~~~ and no assumptions ??? FIXME ???
2.235 + 20.8.02: must return p in case of finished, because the next script
2.236 + consulted need not be the calling script:
2.237 + in case of detail ie. _inserted_ PrfObjs, the next stac
2.238 + has to searched in a script with PblObj.status<>Complete !
2.239 + (.. not true for other details ..PrfObj ??????????????????
2.240 + 20.8.02: do NOT return safe (is only changed in locate !!!)
2.241 +*)
2.242 +fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =
2.243 + if f = f'
2.244 + then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt),
2.245 + (f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
2.246 + else
2.247 + (case next_rule rss f of
2.248 + NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*)
2.249 + | SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
2.250 + (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),
2.251 + (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*next stac*)
2.252 + | _ => error "next_tac: uncovered case next_rule")
2.253 + | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog)
2.254 + (Selem.ScrState (E,l,a,v,s,_), ctxt) =
2.255 + (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
2.256 + else nstep_up thy ptp sc E l Skip_ a v of
2.257 + Skip (v, _) => (*finished*)
2.258 + (case par_pbl_det pt p of
2.259 + (true, p', _) =>
2.260 + let
2.261 + val (_,pblID,_) = get_obj g_spec pt p';
2.262 + in (Tac.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
2.263 + (Selem.e_istate, ctxt), (v,s))
2.264 + end
2.265 + | _ => (Tac.End_Detail' (Rule.e_term,[])(*8.6.03*), (Selem.e_istate, ctxt), (v,s)))
2.266 + | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*)
2.267 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.268 + (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef))) (*next stac*)
2.269 + | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));
2.270 +
2.271 +end
3.1 --- a/src/Tools/isac/Interpret/script.sml Sun Jun 23 14:44:00 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Jun 24 14:02:39 2019 +0200
3.3 @@ -9,8 +9,6 @@
3.4 type step = Tac.tac_ * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
3.5 datatype locate = NotLocatable | Steps of Selem.istate * step list
3.6
3.7 - val next_tac : (*diss: next-tactic-function*)
3.8 - Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> Selem.istate * 'a -> Tac.tac_ * (Selem.istate * 'a) * (term * Selem.safe)
3.9 val locate_gen : (*diss: locate-function*)
3.10 Rule.theory' * Rule.rls -> Tac.tac_ -> Ctree.state -> Rule.scr * 'a -> Selem.istate * Proof.context -> locate
3.11
3.12 @@ -25,6 +23,13 @@
3.13 val rule2thm'' : Rule.rule -> Celem.thm''
3.14 val rule2rls' : Rule.rule -> string
3.15 val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tac.tac list
3.16 +(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
3.17 + val upd_env_opt : LTool.env -> term option * term -> LTool.env
3.18 + val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_
3.19 + val tac_2res : Tac.tac_ -> term
3.20 +
3.21 +
3.22 +
3.23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.24 (* NONE *)
3.25 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.26 @@ -46,16 +51,13 @@
3.27 val go : Celem.loc_ -> term -> term
3.28 val handle_leaf : string -> Rule.theory' -> Rule.rls -> LTool.env -> term option -> term -> term ->
3.29 term option * LTool.stacexpr
3.30 - val is_spec_pos : Ctree.pos_ -> bool
3.31 + val is_spec_pos : Ctree.pos_ -> bool
3.32 val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
3.33 val nstep_up : Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env ->
3.34 Celem.lrd list -> appy_ -> term option -> term -> appy
3.35 val nxt_up: Rule.theory' * Rule.rls -> Ctree.state -> Rule.scr -> LTool.env ->
3.36 Celem.lrd list -> appy_ -> term -> term option -> term -> appy
3.37 val stac2tac : Ctree.ctree -> theory -> term -> Tac.tac
3.38 - val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_
3.39 - val tac_2res : Tac.tac_ -> term
3.40 - val upd_env_opt : LTool.env -> term option * term -> LTool.env
3.41 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.42
3.43 end
3.44 @@ -125,7 +127,7 @@
3.45 | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
3.46 in (implode o scan o Symbol.explode) str end;
3.47
3.48 -(*go at a location in a script and fetch the contents*)
3.49 +(*go at a location in a script and fetch the contents*) (*TODO-LucinNEW del in script.sml*)
3.50 fun go [] t = t
3.51 | go (Celem.D :: p) (Abs(_, _, t0)) = go (p : Celem.loc_) t0
3.52 | go (Celem.L :: p) (t1 $ _) = go p t1
3.53 @@ -533,14 +535,14 @@
3.54
3.55 fun tac_2res m = (snd o snd o rep_tac_) m;
3.56
3.57 -(* handle a leaf at the end of recursive descent:
3.58 +(* handle a leaf at the end of recursive descent: (*TODO-LucinNEW del in script.sml*)
3.59 a leaf is either a tactic or an 'expr' in "let v = expr"
3.60 where "expr" does not contain a tactic.
3.61 Handling a leaf comprises
3.62 (1) 'subst_stacexpr' substitute LTool.env and complete curried tactic
3.63 (2) rewrite the leaf by 'srls'
3.64 *)
3.65 -fun handle_leaf call thy srls E a v t =
3.66 +fun handle_leaf call thy srls E a v t = (*TODO-LucinNEW del in script.sml*)
3.67 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
3.68 case LTool.subst_stacexpr E a v t of
3.69 (a', LTool.STac stac) => (*script-tactic*)
3.70 @@ -854,7 +856,7 @@
3.71
3.72 (** find the next stactic in a script **)
3.73
3.74 -(*appy, nxt_up, nstep_up scanning for next_tac.
3.75 +(*appy, nxt_up, nstep_up scanning for next_tac. (*TODO-LucinNEW del in script.sml*)
3.76 search is clearly separated into (1)-(2):
3.77 (1) appy is recursive descent;
3.78 (2) nxt_up resumes interpretation at a location somewhere in the script;
3.79 @@ -882,191 +884,6 @@
3.80 also used as init-value for resuming; this works,
3.81 because 'nxt_up Or e1' treats as Appy *)
3.82
3.83 -fun appy thy ptp E l (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) a v =
3.84 - (case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of
3.85 - Skip (res, E) =>
3.86 - let val E' = LTool.upd_env E (Free (i,T), res);
3.87 - in appy thy ptp E' (l @ [Celem.R, Celem.D]) b a v end
3.88 - | ay => ay)
3.89 - | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*1*),_) $ c $ e $ a) _ v =
3.90 - (if Rewrite.eval_true_ th sr (subst_atomic (LTool.upd_env E (a,v)) c)
3.91 - then appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
3.92 - else Skip (v, E))
3.93 - | appy (thy as (th,sr)) ptp E l (Const ("Script.While"(*2*),_) $ c $ e) a v =
3.94 - (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.95 - then appy thy ptp E (l @ [Celem.R]) e a v
3.96 - else Skip (v, E))
3.97 - | appy (thy as (th,sr)) ptp E l (Const ("If",_) $ c $ e1 $ e2) a v =
3.98 - (if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a,v)) c)
3.99 - then appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v
3.100 - else appy thy ptp E (l @ [Celem.R]) e2 a v)
3.101 - | appy thy ptp E l (Const ("Script.Repeat"(*1*),_) $ e $ a) _ v =
3.102 - appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v
3.103 - | appy thy ptp E l (Const ("Script.Repeat"(*2*),_) $ e) a v = appy thy ptp E (l @ [Celem.R]) e a v
3.104 - | appy thy ptp E l (Const ("Script.Try"(*2*),_) $ e $ a) _ v =
3.105 - (case appy thy ptp E (l @ [Celem.L, Celem.R]) e (SOME a) v of
3.106 - Napp E => (Skip (v, E))
3.107 - | ay => ay)
3.108 - | appy thy ptp E l(Const ("Script.Try"(*1*),_) $ e) a v =
3.109 - (case appy thy ptp E (l @ [Celem.R]) e a v of
3.110 - Napp E => (Skip (v, E))
3.111 - | ay => ay)
3.112 - | appy thy ptp E l (Const ("Script.Or"(*1*),_) $e1 $ e2 $ a) _ v =
3.113 - (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
3.114 - Appy lme => Appy lme
3.115 - | _ => appy thy ptp E (*LTool.env*) (l @ [Celem.L, Celem.R]) e2 (SOME a) v)
3.116 - | appy thy ptp E l (Const ("Script.Or"(*2*),_) $e1 $ e2) a v =
3.117 - (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
3.118 - Appy lme => Appy lme
3.119 - | _ => appy thy ptp E (l @ [Celem.R]) e2 a v)
3.120 - | appy thy ptp E l (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a) _ v =
3.121 - (case appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v of
3.122 - Skip (v,E) => appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v
3.123 - | ay => ay)
3.124 - | appy thy ptp E l (Const ("Script.Seq"(*1*),_) $ e1 $ e2) a v =
3.125 - (case appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v of
3.126 - Skip (v,E) => appy thy ptp E (l @ [Celem.R]) e2 a v
3.127 - | ay => ay)
3.128 - (* a leaf has been found *)
3.129 - | appy ((th,sr)) (pt, p) E l t a v =
3.130 - case handle_leaf "next " th sr E a v t of
3.131 - (_, LTool.Expr s) => Skip (s, E)
3.132 - | (a', LTool.STac stac) =>
3.133 - let val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac
3.134 - in case m of
3.135 - Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))
3.136 - | _ =>
3.137 - (case Applicable.applicable_in p pt m of
3.138 - Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))
3.139 - | _ => Napp E)
3.140 - end
3.141 -
3.142 -fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
3.143 - if ay = Napp_
3.144 - then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.145 - else (*Skip_*)
3.146 - let
3.147 - val up = drop_last l
3.148 - val (i, T, body) =
3.149 - (case go up sc of
3.150 - Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
3.151 - | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))
3.152 - val i = TermC.mk_Free (i, T)
3.153 - val E = LTool.upd_env E (i, v)
3.154 - in
3.155 - case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v of
3.156 - Appy lre => Appy lre
3.157 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.158 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v
3.159 - end
3.160 - | nxt_up thy ptp scr E l ay (Abs _) a v = nstep_up thy ptp scr E l ay a v
3.161 - | nxt_up thy ptp scr E l ay (Const ("HOL.Let",_) $ _ $ (Abs _)) a v =
3.162 - nstep_up thy ptp scr E l ay a v
3.163 - (*no appy_: never causes Napp -> Helpless*)
3.164 - | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*1*), _) $ c $ e $ _) a v =
3.165 - if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
3.166 - then case appy thy ptp E (l @ [Celem.L, Celem.R]) e a v of
3.167 - Appy lr => Appy lr
3.168 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.169 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.170 - else nstep_up thy ptp scr E l Skip_ a v
3.171 - (*no appy_: never causes Napp - Helpless*)
3.172 - | nxt_up (thy as (th, sr)) ptp scr E l _ (Const ("Script.While"(*2*), _) $ c $ e) a v =
3.173 - if Rewrite.eval_true_ th sr (subst_atomic (upd_env_opt E (a, v)) c)
3.174 - then case appy thy ptp E (l @ [Celem.R]) e a v of
3.175 - Appy lr => Appy lr
3.176 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.177 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v
3.178 - else nstep_up thy ptp scr E l Skip_ a v
3.179 - | nxt_up thy ptp scr E l ay (Const ("If", _) $ _ $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.180 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.181 - (Const ("Script.Repeat"(*1*), _) $ e $ _) a v =
3.182 - (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.L, Celem.R]) e a v of
3.183 - Appy lr => Appy lr
3.184 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.185 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.186 - | nxt_up thy ptp scr E l _ (*no appy_: there was already a stac below*)
3.187 - (Const ("Script.Repeat"(*2*), _) $ e) a v =
3.188 - (case appy thy ptp (*upd_env*) E (*a,v)*) (l @ [Celem.R]) e a v of
3.189 - Appy lr => Appy lr
3.190 - | Napp E => nstep_up thy ptp scr E l Skip_ a v
3.191 - | Skip (v,E) => nstep_up thy ptp scr E l Skip_ a v)
3.192 - | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*2*),_) $ _ $ _) a v = (*makes Napp to Skip*)
3.193 - nstep_up thy ptp scr E l Skip_ a v
3.194 -
3.195 - | nxt_up thy ptp scr E l _ (Const ("Script.Try"(*1*), _) $ _) a v = (*makes Napp to Skip*)
3.196 - nstep_up thy ptp scr E l Skip_ a v
3.197 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _ $ _) a v =
3.198 - nstep_up thy ptp scr E l ay a v
3.199 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
3.200 - | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
3.201 - nstep_up thy ptp scr E (drop_last l) ay a v
3.202 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
3.203 - (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
3.204 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
3.205 - nstep_up thy ptp scr E l ay a v
3.206 - | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)
3.207 - if ay = Napp_
3.208 - then nstep_up thy ptp scr E (drop_last l) Napp_ a v
3.209 - else (*Skip_*)
3.210 - let val up = drop_last l;
3.211 - val e2 =
3.212 - (case go up sc of
3.213 - Const ("Script.Seq"(*2*), _) $ _ $ e2 => e2
3.214 - | t => error ("nxt_up..Script.Seq $ _ with " ^ Rule.term2str t))
3.215 - in case appy thy ptp E (up @ [Celem.R]) e2 a v of
3.216 - Appy lr => Appy lr
3.217 - | Napp E => nstep_up thy ptp scr E up Napp_ a v
3.218 - | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v end
3.219 - | nxt_up _ _ _ _ _ _ t _ _ = error ("nxt_up not impl for " ^ Rule.term2str t)
3.220 -and nstep_up thy ptp (Rule.Prog sc) E l ay a v =
3.221 - if 1 < length l
3.222 - then
3.223 - let val up = drop_last l;
3.224 - in (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v ) end
3.225 - else (*interpreted to end*)
3.226 - if ay = Skip_ then Skip (v, E) else Napp E
3.227 - | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)
3.228 -
3.229 -(* decide for the next applicable stac in the script;
3.230 - returns (stactic, value) - the value in case the script is finished
3.231 - 12.8.02: ~~~~~ and no assumptions ??? FIXME ???
3.232 - 20.8.02: must return p in case of finished, because the next script
3.233 - consulted need not be the calling script:
3.234 - in case of detail ie. _inserted_ PrfObjs, the next stac
3.235 - has to searched in a script with PblObj.status<>Complete !
3.236 - (.. not true for other details ..PrfObj ??????????????????
3.237 - 20.8.02: do NOT return safe (is only changed in locate !!!)
3.238 -*)
3.239 -fun next_tac (thy,_) _ (Rule.Rfuns {next_rule, ...}) (Selem.RrlsState(f, f', rss, _), ctxt) =
3.240 - if f = f'
3.241 - then (Tac.End_Detail' (f',[])(*8.6.03*), (Selem.Uistate, ctxt),
3.242 - (f', Selem.Sundef(*FIXME is no value of next_tac! vor 8.6.03*))) (*finished*)
3.243 - else
3.244 - (case next_rule rss f of
3.245 - NONE => (Tac.Empty_Tac_, (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*)
3.246 - | SOME (Rule.Thm thm'')(*8.6.03: muss auch f' liefern ?!!*) =>
3.247 - (Tac.Rewrite' (thy, "e_rew_ord", Rule.e_rls, false, thm'', f, (Rule.e_term, [(*!?!8.6.03*)])),
3.248 - (Selem.Uistate, ctxt), (Rule.e_term, Selem.Sundef)) (*next stac*)
3.249 - | _ => error "next_tac: uncovered case next_rule")
3.250 - | next_tac thy (ptp as (pt, (p, _))) (sc as Rule.Prog prog)
3.251 - (Selem.ScrState (E,l,a,v,s,_), ctxt) =
3.252 - (case if l = [] then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
3.253 - else nstep_up thy ptp sc E l Skip_ a v of
3.254 - Skip (v, _) => (*finished*)
3.255 - (case par_pbl_det pt p of
3.256 - (true, p', _) =>
3.257 - let
3.258 - val (_,pblID,_) = get_obj g_spec pt p';
3.259 - in (Tac.Check_Postcond' (pblID, (v, [(*assigned in next step*)])),
3.260 - (Selem.e_istate, ctxt), (v,s))
3.261 - end
3.262 - | _ => (Tac.End_Detail' (Rule.e_term,[])(*8.6.03*), (Selem.e_istate, ctxt), (v,s)))
3.263 - | Napp _ => (Tac.Empty_Tac_, (Selem.e_istate, ctxt), (Rule.e_term, Selem.Sundef)) (*helpless*)
3.264 - | Appy (m', scrst as (_,_,_,v,_,_)) =>
3.265 - (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef))) (*next stac*)
3.266 - | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));
3.267 -
3.268 (* create the initial interpreter state
3.269 from the items of the guard and the formal arguments of the partial_function.
3.270 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
4.1 --- a/src/Tools/isac/Interpret/solve.sml Sun Jun 23 14:44:00 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Jun 24 14:02:39 2019 +0200
4.3 @@ -138,7 +138,7 @@
4.4 end
4.5 | NONE => (*execute the first tac in the Script, compare solve m*)
4.6 let
4.7 - val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
4.8 + val (m', (is', ctxt'), _) = LucinNEW.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
4.9 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
4.10 in
4.11 case Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') of
4.12 @@ -174,7 +174,7 @@
4.13 | _ => error "solve Check_Postcond: uncovered case get_loc"
4.14 val thy' = get_obj g_domID pt pp;
4.15 val thy = Celem.assoc_thy thy';
4.16 - val (_, _, (scval, scsaf)) = Lucin.next_tac (thy', srls) (pt, (p, p_)) sc loc;
4.17 + val (_, _, (scval, scsaf)) = LucinNEW.next_tac (thy', srls) (pt, (p, p_)) sc loc;
4.18 in
4.19 if pp = []
4.20 then
4.21 @@ -295,7 +295,7 @@
4.22 | _ => error "nxt_solv Check_Postcond': uncovered case get_loc"
4.23 val thy' = get_obj g_domID pt pp;
4.24 val thy = Celem.assoc_thy thy';
4.25 - val (_, _, (scval, scsaf)) = Lucin.next_tac (thy', srls) (pt, (p, p_)) sc loc;
4.26 + val (_, _, (scval, scsaf)) = LucinNEW.next_tac (thy', srls) (pt, (p, p_)) sc loc;
4.27 in
4.28 if pp = []
4.29 then
4.30 @@ -337,7 +337,7 @@
4.31 let
4.32 val thy' = get_obj g_domID pt (par_pblobj pt p);
4.33 val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
4.34 - val (tac_, is, (t, _)) = Lucin.next_tac (thy', srls) (pt, pos) sc is;
4.35 + val (tac_, is, (t, _)) = LucinNEW.next_tac (thy', srls) (pt, pos) sc is;
4.36 (* TODO here ^^^ return finished/helpless/ok !*)
4.37 in case tac_ of
4.38 Tac.End_Detail' _ => ([(Tac.End_Detail, Tac.End_Detail' (t, [(*FIXME.04*)]), (pos, is))], [], (pt, pos))