1.1 --- a/src/Tools/isac/CalcElements/environment.sml Thu Nov 21 15:31:32 2019 +0100
1.2 +++ b/src/Tools/isac/CalcElements/environment.sml Mon Nov 25 16:39:52 2019 +0100
1.3 @@ -40,7 +40,7 @@
1.4 fun update' id (vl, env) = update env (id, vl)
1.5
1.6 (*WN020526: not clear, when a is available in scan_up1 for eval_true*)
1.7 -(*WN060906: in "fun handle_leaf" eg. uses "SOME M__"(from some PREVIOUS
1.8 +(*WN060906: in "fun interpret_leaf" eg. uses "SOME M__"(from some PREVIOUS
1.9 curried Rewrite) for CURRENT value (which may be different from PREVIOUS);
1.10 thus "NONE" must be set at the end of currying (ill designed anyway)*)
1.11 fun update_opt env (SOME id, vl) = update env (id, vl)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 15:31:32 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 25 16:39:52 2019 +0100
2.3 @@ -36,7 +36,7 @@
2.4
2.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.6 datatype expr_val1 =
2.7 - Ackn_Tac1 of Istate.pstate * Proof.context * Tactic.T
2.8 + Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
2.9 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
2.10 | Term_Val1 of term;
2.11 val assoc2str : expr_val1 -> string
2.12 @@ -51,8 +51,9 @@
2.13 val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
2.14 val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
2.15 val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
2.16 + val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
2.17
2.18 - datatype expr_val2 = Ackn_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
2.19 + datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
2.20 val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> expr_val2
2.21 val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> expr_val2
2.22 val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> expr_val2
2.23 @@ -100,17 +101,33 @@
2.24 datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
2.25 Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
2.26 Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac2*)
2.27 -| Ackn_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
2.28 +| Accept_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
2.29 Istate.pstate * (* the current state, returned for resuming execution *)
2.30 Proof.context * (* updated according to evaluation of Prog_Tac *)
2.31 Tactic.T (* Prog_Tac is associated to Tactic.input *)
2.32 | Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
2.33 term (* value of Prog_Expr, for updating environment *)
2.34 -fun assoc2str (Ackn_Tac1 _) = "Ackn_Tac1"
2.35 +fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
2.36 | assoc2str (Term_Val1 _) = "Term_Val1"
2.37 | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
2.38
2.39
2.40 +(** interpret a Prog_Tac: is it associated to Tactic ? **)
2.41 +
2.42 +fun interpret_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (form_arg, prog_tac) =
2.43 + case Lucin.associate pt ctxt (tac, prog_tac) of
2.44 + (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
2.45 + Lucin.Ass (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_true (form_arg, v'), ctxt, m)
2.46 + | Lucin.Ass_Weak (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_false (form_arg, v'), ctxt, m)
2.47 +
2.48 + | Lucin.NotAss =>
2.49 + (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
2.50 + AssOnly => Term_Val1 act_arg
2.51 + | _(*ORundef*) =>
2.52 + case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
2.53 + Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Lucin.tac_2res m'), ctxt, tac)
2.54 + | Chead.Notappl _ => Term_Val1 act_arg)
2.55 +
2.56 (** scan to a Prog_Tac **)
2.57
2.58 fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =
2.59 @@ -154,7 +171,7 @@
2.60 then scan_dn1 cct (ist |> path_down [R]) e
2.61 else Term_Val1 act_arg
2.62
2.63 - | scan_dn1 cct (ist as {or = Aundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
2.64 + | scan_dn1 cct (ist as {or = ORundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
2.65 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
2.66 Term_Val1 v =>
2.67 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
2.68 @@ -176,54 +193,38 @@
2.69 then scan_dn1 cct (ist |> path_down [L, R]) e1
2.70 else scan_dn1 cct (ist |> path_down [R]) e2
2.71
2.72 - | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t =
2.73 + | scan_dn1 cct (ist as {eval, ...}) t =
2.74 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
2.75 else
2.76 - case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
2.77 - (a', Program.Expr _) =>
2.78 -(*--------------------------- eval_Prog_Expr -----*)
2.79 - Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
2.80 - (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t))
2.81 - | (a', Program.Tac stac) =>
2.82 -(*/------------ interprete_Prog_Tac -----*)
2.83 - case Lucin.associate pt ctxt (tac, stac) of
2.84 - (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
2.85 - Lucin.Ass (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m)
2.86 - | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m)
2.87 -
2.88 - | Lucin.NotAss =>
2.89 - (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
2.90 - AssOnly => Term_Val1 act_arg
2.91 - | _(*Aundef*) =>
2.92 - case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
2.93 - Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
2.94 - | Chead.Notappl _ => Term_Val1 act_arg)
2.95 -(*------------- interprete_tactic ---//*)
2.96 - ;
2.97 + case Lucin.interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
2.98 + (form_arg, Program.Expr _) =>
2.99 + Term_Val1 (Rewrite.eval_prog_expr (Celem.assoc_thy "Isac_Knowledge") eval
2.100 + (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
2.101 + | (form_arg, Program.Tac prog_tac) =>
2.102 + interpret_tac1 cct ist (form_arg, prog_tac)
2.103
2.104 fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
2.105 | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
2.106
2.107 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
2.108 - (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
2.109 + (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
2.110 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
2.111 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
2.112 | goback => goback)
2.113 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
2.114 - (case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
2.115 + (case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
2.116 Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
2.117 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
2.118 | goback => goback)
2.119
2.120 (*all has been done in (*2*) below*)
2.121 | scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
2.122 - | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
2.123 - (*comes from e1, goes to e2*)
2.124 + | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
2.125 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =
2.126 let
2.127 - val e2 = check_Seq_up ist prog
2.128 + val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
2.129 in
2.130 - case scan_dn1 cct (ist |> path_up_down [R] |> set_or Aundef) e2 of
2.131 + case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 of
2.132 Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
2.133 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
2.134 | goback => goback
2.135 @@ -232,8 +233,8 @@
2.136 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =
2.137 let
2.138 val (i, body) = check_Let_up ist prog
2.139 - in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body of
2.140 - Ackn_Tac1 iss => Ackn_Tac1 iss
2.141 + in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body of
2.142 + Accept_Tac1 iss => Accept_Tac1 iss
2.143 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
2.144 | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
2.145 end
2.146 @@ -244,7 +245,7 @@
2.147 (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
2.148 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)
2.149 then
2.150 - case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
2.151 + case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
2.152 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
2.153
2.154 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
2.155 @@ -254,7 +255,7 @@
2.156 (t as Const ("Tactical.While"(*2*), _) $ c $ e) =
2.157 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.158 then
2.159 - case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
2.160 + case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
2.161 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
2.162 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
2.163 | goback => goback
2.164 @@ -276,14 +277,14 @@
2.165
2.166 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
2.167 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
2.168 - then scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog)
2.169 + then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
2.170 else go_scan_up1 (prog, cctt) ist
2.171 | scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
2.172
2.173 (*locate an input tactic within a program*)
2.174 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
2.175 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
2.176 - Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
2.177 + Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
2.178 if assoc
2.179 then Safe_Step (Istate.Pstate ist, ctxt, tac')
2.180 else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
2.181 @@ -301,7 +302,7 @@
2.182
2.183 datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics *)
2.184 Reject_Tac2 (* tactic is found but NOT acknowledged, scan is continued *)
2.185 -| Ackn_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
2.186 +| Accept_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
2.187 Tactic.T * (* Prog_Tac is applicable_in cstate *)
2.188 Istate.pstate (* the current state, returned for resuming execution *)
2.189 | Term_Val2 of (* Prog_Expr is found and evaluated, scan is continued *)
2.190 @@ -353,11 +354,11 @@
2.191
2.192 |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
2.193 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
2.194 - Ackn_Tac2 lme => Ackn_Tac2 lme
2.195 + Accept_Tac2 lme => Accept_Tac2 lme
2.196 | _ => scan_dn2 cc (ist |> path_down_form ([L, R], a)) e2)
2.197 | scan_dn2 cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
2.198 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
2.199 - Ackn_Tac2 lme => Ackn_Tac2 lme
2.200 + Accept_Tac2 lme => Accept_Tac2 lme
2.201 | _ => scan_dn2 cc (ist |> path_down [R]) e2)
2.202
2.203 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
2.204 @@ -368,17 +369,17 @@
2.205 | scan_dn2 ((pt, p), ctxt) (ist as {eval, ...}) t =
2.206 if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])
2.207 else
2.208 - case Lucin.handle_leaf "next " ctxt eval (get_subst ist) t of
2.209 + case Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t of
2.210 (_, Program.Expr s) => Term_Val2 s
2.211 | (a', Program.Tac stac) =>
2.212 let
2.213 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
2.214 in
2.215 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
2.216 - Tactic.Subproblem _ => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
2.217 + Tactic.Subproblem _ => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
2.218 | _ =>
2.219 (case Applicable.applicable_in p pt m of
2.220 - Chead.Appl m' => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
2.221 + Chead.Appl m' => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
2.222 | _ => Reject_Tac2)
2.223 end
2.224
2.225 @@ -388,13 +389,13 @@
2.226
2.227 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
2.228 (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
2.229 - Ackn_Tac2 lr => Ackn_Tac2 lr
2.230 + Accept_Tac2 lr => Accept_Tac2 lr
2.231 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
2.232 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
2.233 (*no appy_: there was already a stac below*)
2.234 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
2.235 (case scan_dn2 cc (ist |> path_down [R]) e of
2.236 - Ackn_Tac2 lr => Ackn_Tac2 lr
2.237 + Accept_Tac2 lr => Accept_Tac2 lr
2.238 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
2.239 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
2.240
2.241 @@ -408,7 +409,7 @@
2.242 val e2 = check_Seq_up ist sc
2.243 in
2.244 case scan_dn2 cc (ist |> path_up_down [R]) e2 of
2.245 - Ackn_Tac2 lr => Ackn_Tac2 lr
2.246 + Accept_Tac2 lr => Accept_Tac2 lr
2.247 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
2.248 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
2.249 end
2.250 @@ -421,7 +422,7 @@
2.251 val (i, body) = check_Let_up ist sc
2.252 in
2.253 case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
2.254 - Ackn_Tac2 lre => Ackn_Tac2 lre
2.255 + Accept_Tac2 lre => Accept_Tac2 lre
2.256 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
2.257 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
2.258 end
2.259 @@ -434,7 +435,7 @@
2.260 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.261 then
2.262 case scan_dn2 cc (ist |> path_down [L, R]) e of
2.263 - Ackn_Tac2 lr => Ackn_Tac2 lr
2.264 + Accept_Tac2 lr => Accept_Tac2 lr
2.265 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
2.266 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
2.267 else
2.268 @@ -444,7 +445,7 @@
2.269 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
2.270 then
2.271 case scan_dn2 cc (ist |> path_down [R]) e of
2.272 - Ackn_Tac2 lr => Ackn_Tac2 lr
2.273 + Accept_Tac2 lr => Accept_Tac2 lr
2.274 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
2.275 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
2.276 else
2.277 @@ -486,7 +487,7 @@
2.278 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)))
2.279 | Reject_Tac2 =>
2.280 (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
2.281 - | Ackn_Tac2 (m', (ist as {act_arg, ...})) =>
2.282 + | Accept_Tac2 (m', (ist as {act_arg, ...})) =>
2.283 (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *)
2.284 | determine_next_tactic _ _ _ (is, _) =
2.285 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
3.1 --- a/src/Tools/isac/Interpret/script.sml Thu Nov 21 15:31:32 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Nov 25 16:39:52 2019 +0100
3.3 @@ -31,7 +31,7 @@
3.4 val tac_2res : Tactic.T -> term
3.5 val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
3.6 val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
3.7 - val handle_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
3.8 + val interpret_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
3.9 string -> Rule.theory' -> Rule.rls -> (Env.T * (term option * term)) -> term ->
3.10 term option * Program.leaf
3.11
3.12 @@ -59,7 +59,7 @@
3.13 (**)
3.14 (* data for creating a new node in ctree; designed for use as:
3.15 fun ass* pstate steps = / ... case ass* pstate steps of /
3.16 - Ackn_Tac1 (pstate, steps) => ... ass* pstate steps *)
3.17 + Accept_Tac1 (pstate, steps) => ... ass* pstate steps *)
3.18 type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
3.19 WN190713 COMPARE: taci list, see papernote #139 *)
3.20 Tactic.T (*transformed from associated tac *)
3.21 @@ -605,12 +605,12 @@
3.22 (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
3.23 (2) rewrite the leaf by 'srls'
3.24 *)
3.25 -fun handle_leaf call thy srls (E, (a, v)) t =
3.26 +fun interpret_leaf call thy srls (E, (a, v)) t =
3.27 (*WN050916 'upd_env_opt' is a blind copy from previous version*)
3.28 - case Prog_Tac.subst_stacexpr E a v t of
3.29 + case Prog_Tac.eval_leaf E a v t of
3.30 (a', Program.Tac stac) => (* Prog_Tac *)
3.31 let val stac' =
3.32 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) stac)
3.33 + Rewrite.eval_prog_expr (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) stac)
3.34 in
3.35 (if (! trace_script)
3.36 then tracing ("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
3.37 @@ -619,7 +619,7 @@
3.38 end
3.39 | (a', Program.Expr lexpr) => (* Prog_Expr *)
3.40 let val lexpr' =
3.41 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
3.42 + Rewrite.eval_prog_expr (Celem.assoc_thy thy) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
3.43 in
3.44 (if (! trace_script)
3.45 then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
3.46 @@ -644,7 +644,7 @@
3.47 {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
3.48 val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
3.49 in map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
3.50 - (handle_leaf "selrul" thy' srls subst)) (Auto_Prog.stacpbls sc)
3.51 + (interpret_leaf "selrul" thy' srls subst)) (Auto_Prog.stacpbls sc)
3.52 end;
3.53
3.54 (* fetch tactics from script and filter _applicable_ tactics;
3.55 @@ -671,7 +671,7 @@
3.56 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
3.57 val alltacs = (*we expect at least 1 stac in a script*)
3.58 map ((stac2tac pt thy) o Program.rep_stacexpr o #2 o
3.59 - (handle_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
3.60 + (interpret_leaf "selrul" thy' srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
3.61 val f =
3.62 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
3.63 | _ => error "")
4.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Thu Nov 21 15:31:32 2019 +0100
4.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Mon Nov 25 16:39:52 2019 +0100
4.3 @@ -5,7 +5,7 @@
4.4 signature INTERPRETER_STATE =
4.5 sig
4.6
4.7 - datatype asap = Aundef | AssOnly | AssGen;
4.8 + datatype asap = ORundef | AssOnly | AssGen;
4.9 datatype appy_ = AppUndef_ | Napp_ | Skip_
4.10 type pstate
4.11 val e_scrstate: pstate
4.12 @@ -62,23 +62,23 @@
4.13 open Celem
4.14
4.15 datatype asap = (* arg. of scan_dn1 _only_ for distinction w.r.t. Or *)
4.16 - Aundef (* undefined: set only by (topmost) Or *)
4.17 + ORundef (* undefined: set only by (topmost) Or *)
4.18 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated
4.19 in parallel Or-branch *)
4.20 | AssGen; (* no Ass(Weak) found within Or, thus continue scan
4.21 search for _applicable_ stacs, execute and generate pt *)
4.22 (*this constructions doesnt allow arbitrary nesting of Or !!! *)
4.23 -fun asap2str Aundef = "Aundef"
4.24 +fun asap2str ORundef = "ORundef"
4.25 | asap2str AssOnly = "AssOnly"
4.26 | asap2str AssGen = "AssGen"
4.27
4.28 datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *)
4.29 -(*Ackn_Tac2 is only (final) returnvalue, not argument during search *)
4.30 +(*Accept_Tac2 is only (final) returnvalue, not argument during search *)
4.31 AppUndef_
4.32 | Napp_ (* ev. detects 'script is not appropriate for this example' *)
4.33 | Skip_; (* detects 'script successfully finished'
4.34 also used as init-value for resuming; this works,
4.35 - because 'nxt_up Or e1' treats as Ackn_Tac2 *)
4.36 + because 'nxt_up Or e1' treats as Accept_Tac2 *)
4.37 fun appy_2str AppUndef_ = "AppUndef_"
4.38 | appy_2str Napp_ = "Napp_"
4.39 | appy_2str Skip_ = "Skip_"
4.40 @@ -94,7 +94,7 @@
4.41 assoc: bool} (* is the tactic associated to input *)
4.42 val e_scrstate =
4.43 {env = [], path = [], eval = Rule.e_rls, form_arg = NONE, act_arg = Rule.e_term,
4.44 - or = Aundef, finish = AppUndef_, assoc = false}
4.45 + or = ORundef, finish = AppUndef_, assoc = false}
4.46 fun topt2str NONE = "NONE"
4.47 | topt2str (SOME t) = "SOME" ^ Rule.term2str t;
4.48 fun scrstate2str {env, path, eval, form_arg, act_arg, or, finish, assoc} = (* for tests only *)
4.49 @@ -188,7 +188,7 @@
4.50 or = or, finish = finish, assoc = false}
4.51 fun set_subst_reset (form_arg, act_arg) {env, path, eval, ...} = (*compare NEW OLD usage*)
4.52 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
4.53 - or = Aundef, finish = AppUndef_, assoc = false}
4.54 + or = ORundef, finish = AppUndef_, assoc = false}
4.55
4.56 fun set_env env {path, eval, form_arg, act_arg, or, finish, assoc, ...} =
4.57 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
5.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Nov 21 15:31:32 2019 +0100
5.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Nov 25 16:39:52 2019 +0100
5.3 @@ -82,7 +82,7 @@
5.4 | scan (Const ("Tactical.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
5.5 | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
5.6 | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)
5.7 - | scan t = case Prog_Tac.subst_stacexpr [] NONE Rule.e_term t of
5.8 + | scan t = case Prog_Tac.eval_leaf [] NONE Rule.e_term t of
5.9 (_, Program.Tac _) => [t] | (_, Program.Expr _) => []
5.10 in (distinct o scan) body end
5.11 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'")
6.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Thu Nov 21 15:31:32 2019 +0100
6.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Mon Nov 25 16:39:52 2019 +0100
6.3 @@ -59,7 +59,7 @@
6.4 sig
6.5 val dest_spec : term -> Celem.spec
6.6 val get_stac : 'a -> term -> term option (*rename get_first*)
6.7 - val subst_stacexpr: (term * term) list -> term option -> term -> term -> term option * Program.leaf
6.8 + val eval_leaf: (term * term) list -> term option -> term -> term -> term option * Program.leaf
6.9 val is: term -> bool
6.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.11 (*NONE*)
6.12 @@ -128,60 +128,60 @@
6.13 (2) the non-curried version must return NONE for a
6.14 (3) non-matching patterns become an Program.Expr by fall-through.
6.15 WN060906 quick and dirty fix: due to (2) a is returned, too *)
6.16 -fun subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
6.17 +fun eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite"(*1*), _) $ _ $ _)) =
6.18 (NONE, Program.Tac (subst_atomic E t))
6.19 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
6.20 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite"(*2*), _) $ _)) =
6.21 (a, Program.Tac (
6.22 case a of SOME a' => (subst_atomic E (t $ a'))
6.23 | NONE => ((subst_atomic E t) $ v)))
6.24 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
6.25 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
6.26 (NONE, Program.Tac (subst_atomic E t))
6.27 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
6.28 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
6.29 (a, Program.Tac (
6.30 case a of SOME a' => subst_atomic E (t $ a')
6.31 | NONE => ((subst_atomic E t) $ v)))
6.32 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
6.33 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
6.34 (NONE, Program.Tac (subst_atomic E t))
6.35 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
6.36 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
6.37 (a, Program.Tac (
6.38 case a of SOME a' => subst_atomic E (t $ a')
6.39 | NONE => ((subst_atomic E t) $ v)))
6.40 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
6.41 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
6.42 (NONE, Program.Tac (subst_atomic E t))
6.43 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
6.44 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
6.45 (a, Program.Tac (
6.46 case a of SOME a' => subst_atomic E (t $ a')
6.47 | NONE => ((subst_atomic E t) $ v)))
6.48 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
6.49 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Calculate"(*1*), _) $ _ $ _)) =
6.50 (NONE, Program.Tac (subst_atomic E t))
6.51 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
6.52 + | eval_leaf E a v (t as (Const ("Prog_Tac.Calculate"(*2*), _) $ _)) =
6.53 (a, Program.Tac (
6.54 case a of SOME a' => subst_atomic E (t $ a')
6.55 | NONE => ((subst_atomic E t) $ v)))
6.56 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) =
6.57 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) =
6.58 (NONE, Program.Tac (subst_atomic E t))
6.59 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) =
6.60 + | eval_leaf E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) =
6.61 (a, Program.Tac (
6.62 case a of SOME a' => subst_atomic E (t $ a')
6.63 | NONE => ((subst_atomic E t) $ v)))
6.64 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) =
6.65 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) =
6.66 (NONE, Program.Tac (subst_atomic E t))
6.67 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
6.68 + | eval_leaf E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
6.69 (a, Program.Tac (
6.70 case a of SOME a' => subst_atomic E (t $ a')
6.71 | NONE => ((subst_atomic E t) $ v)))
6.72 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
6.73 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
6.74 (NONE, Program.Tac (subst_atomic E t))
6.75 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
6.76 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
6.77 (NONE, Program.Tac (subst_atomic E t))
6.78 - | subst_stacexpr E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
6.79 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
6.80 (NONE, Program.Tac (subst_atomic E t))
6.81 - | subst_stacexpr E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
6.82 + | eval_leaf E a v (t as (Const ("Prog_Tac.Substitute"(*2*), _) $ _)) =
6.83 (a, Program.Tac (
6.84 case a of SOME a' => subst_atomic E (t $ a')
6.85 | NONE => ((subst_atomic E t) $ v)))
6.86 (*now all tactics are matched out and this leaf must be without a tactic*)
6.87 - | subst_stacexpr E a v t =
6.88 + | eval_leaf E a v t =
6.89 (a, Program.Expr (subst_atomic (case a of SOME a => Env.update E (a,v) | NONE => E) t));
6.90
6.91
7.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Nov 21 15:31:32 2019 +0100
7.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Mon Nov 25 16:39:52 2019 +0100
7.3 @@ -8,7 +8,7 @@
7.4 val assoc_thm'': theory -> Celem.thmID -> thm
7.5 val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
7.6 val eval__true: theory -> int -> term list -> (term * term) list -> Rule.rls -> term list * bool
7.7 - val eval_listexpr_: theory -> Rule.rls -> term -> term
7.8 + val eval_prog_expr: theory -> Rule.rls -> term -> term
7.9 val eval_true: theory -> term list -> Rule.rls -> bool
7.10 val eval_true_: Rule.theory' -> Rule.rls -> term -> bool
7.11 val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
7.12 @@ -321,7 +321,7 @@
7.13 ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
7.14 error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)")
7.15
7.16 -fun eval_listexpr_ thy srls t =
7.17 +fun eval_prog_expr thy srls t =
7.18 let val rew = rewrite_set_ thy false srls t;
7.19 in case rew of SOME (res,_) => res | NONE => t end;
7.20
8.1 --- a/src/Tools/isac/Specify/calchead.sml Thu Nov 21 15:31:32 2019 +0100
8.2 +++ b/src/Tools/isac/Specify/calchead.sml Mon Nov 25 16:39:52 2019 +0100
8.3 @@ -25,7 +25,7 @@
8.4 int.modelling +Cor ++++++Cor \<down> \<down>
8.5 form.args= [ id ..... id , /////// id ....... id ] \<down> \<down>
8.6 env = [(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
8.7 - interprete code env = [(id, v)..(id, v),(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
8.8 + interpret code env = [(id, v)..(id, v),(id, v)..(id, v) , /////// (id, v)....(id, v)] \<down> \<down>
8.9 ..extends env ^^^^^^^^^^^^^^^^ \<down> \<down> \<down> \<down> \<down>
8.10 \<down> \<down> \<down> \<down> \<down> \<down>
8.11 SubProblem on pos = ([2], _) \<down> \<down> \<down> \<down> \<down> \<down>
8.12 @@ -35,14 +35,14 @@
8.13 + met.ppc= [(dsc,id).......................(dsc,id)]\<down> \<down> \<down>
8.14 \<down> \<down> \<down> \<down> \<down>
8.15 oris = [(dsc, v)...................... (dsc, v) ........... (dsc, v)]\<down>
8.16 - Specify_Problem, int.modelling, Specify_Method, interprete code as above #1# \<down>
8.17 + Specify_Problem, int.modelling, Specify_Method, interpret code as above #1# \<down>
8.18 \<down>
8.19 SubProblem on pos = ([3, 4], _) \<down>
8.20 form.args= [id ...................... id ] \<down>
8.21 \<down> REAL..BOOL.. \<down>
8.22 + met.ppc= [(dsc,id).............(dsc,id)] \<down>
8.23 oris = [(dsc, v).............(dsc, v)...................(dsc, v)]
8.24 - Specify_Problem, int.modelling, Specify_Method, interprete code as above #1#
8.25 + Specify_Problem, int.modelling, Specify_Method, interpret code as above #1#
8.26
8.27 Notes:
8.28 (1) SubProblem implements sub-function calls such, that the arguments (+ pre- + post-condition)
9.1 --- a/src/Tools/isac/TODO.thy Thu Nov 21 15:31:32 2019 +0100
9.2 +++ b/src/Tools/isac/TODO.thy Mon Nov 25 16:39:52 2019 +0100
9.3 @@ -14,6 +14,8 @@
9.4 text \<open>
9.5 \begin{itemize}
9.6 \item xxx
9.7 + \item xxx
9.8 + \item assoc2str --> expr_val12str
9.9 \item consistently replace thy by ctxt in lucin; search for
9.10 "Isac_Knowledge", Context.theory_name (Rule.Isac""), etc
9.11 \item fun mathml.indent: use from LibraryC
9.12 @@ -21,11 +23,11 @@
9.13 \item xxx
9.14 \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here
9.15 \item xxx
9.16 - \item fun handle_leaf: trace_prog .. separate message
9.17 + \item fun interpret_leaf: trace_prog .. separate message
9.18 \item xxx
9.19 \item rm test/..--- check Scripts ---
9.20 \item xxx
9.21 - \item reformat + rename "fun subst_stacexpr"+"fun get_stac"
9.22 + \item reformat + rename "fun eval_leaf"+"fun get_stac"
9.23 (*1*)(*2*)
9.24 ?consistency with subst term?
9.25 \item Tactic.Rewrite*: drop "bool"
9.26 @@ -108,7 +110,7 @@
9.27 \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
9.28 \end{itemize}
9.29 \item xxx
9.30 - \item reconsider "fun subst_stacexpr"
9.31 + \item reconsider "fun eval_leaf"
9.32 CAUTION: (1) currying with @@ requires 2 patterns for each tactic
9.33 (2) the non-curried version must return NONE for a
9.34 (3) non-matching patterns become an Program.Expr by fall-through.
9.35 @@ -133,9 +135,9 @@
9.36 \item xxx
9.37 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
9.38 \item xxx
9.39 - \item change Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t
9.40 - to Lucin.handle_leaf "locate" ctxt ( pstate ) !!srls in pstate!!^^
9.41 - and redesign handle_leaf .. subst_stacexpr .. associate
9.42 + \item change Lucin.interpret_leaf "locate" "Isac_Knowledge" sr E a v t
9.43 + to Lucin.interpret_leaf "locate" ctxt ( pstate ) !!srls in pstate!!^^
9.44 + and redesign interpret_leaf .. eval_leaf .. associate
9.45 to Tactic.from_code :
9.46 + keep ! trace_script
9.47 + scrstate2str --> pstate2str
9.48 @@ -384,7 +386,7 @@
9.49 \item cleaup the many conversions string -- theory
9.50 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
9.51 \item 1. Rewrite.eval_true_, then
9.52 - Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac.
9.53 + Lucin.interpret_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac.
9.54 \item fun associate
9.55 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
9.56 \item xxx
10.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Thu Nov 21 15:31:32 2019 +0100
10.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon Nov 25 16:39:52 2019 +0100
10.3 @@ -161,7 +161,7 @@
10.4 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
10.5 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
10.6 andalso istate2str (get_istate pt p)
10.7 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, AppUndef_, true)"
10.8 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)"
10.9 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
10.10 (*-------------------------------------------------------------------------*)
10.11
10.12 @@ -181,11 +181,11 @@
10.13 (*//******************* locatetac returns tac_ + istate + cstate *****************************\\*)
10.14 locatetac : Tactic.input -> state -> string * (taci list * pos' list * state);
10.15 if istate2str istate
10.16 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
10.17 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, true)"
10.18 then () else error "from locatetac return --- changed 1";
10.19
10.20 if istate2str (get_istate (fst cstate) (snd cstate))
10.21 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
10.22 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, true)"
10.23 then () else error "from locatetac return --- changed 2";
10.24 (*\\******************* locatetac returns tac_ + istate + cstate *****************************//*)
10.25
10.26 @@ -207,7 +207,7 @@
10.27 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
10.28 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
10.29 (*+*)if istate2str istate
10.30 -(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
10.31 +(*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, true)"
10.32 then case m of Rewrite_Set_Inst' _ => ()
10.33 else error "from locate_input_tactic return --- changed";
10.34
10.35 @@ -232,7 +232,7 @@
10.36 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
10.37 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
10.38 (*+*)if pos' = ([1], Res) andalso istate2str istate
10.39 - = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
10.40 + = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, true)"
10.41 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
10.42
10.43 val pIopt = get_pblID (pt,ip);
10.44 @@ -244,7 +244,7 @@
10.45 val ("ok", [], ptp as (pt, p)) = xxxx;
10.46
10.47 if istate2str (get_istate pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
10.48 -(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), Aundef, AppUndef_, true)"
10.49 +(*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOMEe_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, AppUndef_, true)"
10.50 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
10.51
10.52 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
11.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 15:31:32 2019 +0100
11.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 25 16:39:52 2019 +0100
11.3 @@ -53,14 +53,14 @@
11.4 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
11.5 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
11.6 | _ => error "solve Apply_Method: uncovered case init_pstate";
11.7 -(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, Aundef, AppUndef_, true)";
11.8 +(*+*)scrstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, AppUndef_, true)";
11.9 val ini = Lucin.init_form thy sc env;
11.10 val p = lev_dn p;
11.11
11.12 val NONE = (*case*) ini (*of*);
11.13 val (m', (is', ctxt'), _) =
11.14 LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
11.15 -(*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, Aundef, AppUndef_, false)";
11.16 +(*+*)scrstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, AppUndef_, false)";
11.17 val Safe_Step (_, _, Take' _) = (*case*)
11.18 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
11.19 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)
11.20 @@ -71,10 +71,10 @@
11.21 = ((prog, (cstate, ctxt, tac)), istate);
11.22 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
11.23
11.24 - val Ackn_Tac1 (_, _, Take' _) =
11.25 - scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
11.26 + val Accept_Tac1 (_, _, Take' _) =
11.27 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
11.28 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
11.29 - = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
11.30 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
11.31
11.32 (*+*) if term2str e = "Take (Integral f_f D v_v)" then () else error "scan_dn1 Integral changed";
11.33
11.34 @@ -83,7 +83,7 @@
11.35 (*======= end of scanning tacticals, a leaf =======*)
11.36 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
11.37 = (xxx, (ist |> path_down [L, R]), e);
11.38 -val (a', Program.Tac stac) = handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
11.39 +val (a', Program.Tac stac) = interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t;
11.40
11.41
11.42 "----------- re-build: fun locate_input_tactic -------------------------------------------------";
11.43 @@ -128,16 +128,16 @@
11.44 = (sc, (pt, po), (fst is), (snd is), m);
11.45 val srls = get_simplifier cstate;
11.46
11.47 - (** )val Ackn_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
11.48 + (** )val Accept_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
11.49 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
11.50 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
11.51 = ((prog, (cstate, ctxt, tac)), istate);
11.52 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
11.53
11.54 (** )val xxxxx_xx = ( **)
11.55 - scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
11.56 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
11.57 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
11.58 - = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
11.59 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
11.60
11.61 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
11.62 "~~~~~ fun scan_dn1 , args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
11.63 @@ -152,16 +152,16 @@
11.64 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t)
11.65 = (xxx, (ist |> path_down [R]), e);
11.66 val (a', Program.Tac stac) =
11.67 - (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
11.68 + (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
11.69 val Lucin.Ass (m, v', ctxt) =
11.70 (*case*) associate pt ctxt (m, stac) (*of*);
11.71
11.72 - Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
11.73 + Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
11.74 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
11.75 - = (Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
11.76 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
11.77
11.78 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac')
11.79 - = (Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
11.80 +"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac')
11.81 + = (Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
11.82 (*if*) LibraryC.assoc (*then*);
11.83
11.84 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
11.85 @@ -316,9 +316,9 @@
11.86 = (yyy, (ist |> path_up), (go (path_up' path) prog));
11.87 val e2 = check_Seq_up ist prog
11.88 ;
11.89 - (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or Aundef) e (*of*);
11.90 + (*case*) scan_dn1 xxx (ist |> path_up_down [R] |> set_or ORundef) e (*of*);
11.91 "~~~~~ fun scan_dn1 , args:"; val (yyy, ist, (Const ("Tactical.Chain"(*2*), _) $ _ $ _))
11.92 - = (xxx, (ist |> path_up_down [R] |> set_or Aundef), e2);
11.93 + = (xxx, (ist |> path_up_down [R] |> set_or ORundef), e2);
11.94
11.95 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e1 (*of*);
11.96 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("Tactical.Try"(*2*), _) $ e))
11.97 @@ -328,9 +328,9 @@
11.98 (*======= end of scanning tacticals, a leaf =======*)
11.99 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
11.100 = (xxx, (ist |> path_down [R]), e);
11.101 - val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
11.102 + val (a', Program.Tac stac) = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
11.103 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
11.104 - val Aundef = (*case*) or (*of*);
11.105 + val ORundef = (*case*) or (*of*);
11.106 val Notappl "norm_equation not applicable" =
11.107 (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
11.108
11.109 @@ -341,7 +341,7 @@
11.110
11.111 if scrstate2str ist =
11.112 "([\"\n(t_t, 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12)\"], [R,L,R,R,L,R,R], e_rls, SOMEt_t, \n" ^
11.113 - "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, Aundef, AppUndef_, false)"
11.114 + "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g, ORundef, AppUndef_, false)"
11.115 andalso
11.116 term2str t = "- (8 * g) + (- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f) + 10 * g"
11.117 andalso
12.1 --- a/test/Tools/isac/Interpret/script.sml Thu Nov 21 15:31:32 2019 +0100
12.2 +++ b/test/Tools/isac/Interpret/script.sml Mon Nov 25 16:39:52 2019 +0100
12.3 @@ -208,7 +208,7 @@
12.4 val Pstate ist = get_istate pt (p,p_)
12.5 val alltacs = (*we expect at least 1 stac in a script*)
12.6 map ((stac2tac pt thy) o rep_stacexpr o #2 o
12.7 - (handle_leaf "selrul" thy' srls (get_subst ist) )) (stacpbls sc)
12.8 + (interpret_leaf "selrul" thy' srls (get_subst ist) )) (stacpbls sc)
12.9 val f =
12.10 case p_ of
12.11 Frm => get_obj g_form pt p
12.12 @@ -416,7 +416,7 @@
12.13 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);
12.14 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
12.15 if scrstate2str st =
12.16 - "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, Aundef, AppUndef_, true)"
12.17 + "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, AppUndef_, true)"
12.18 then () else error "init_pstate changed for Biegelinie";
12.19
12.20 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
13.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Thu Nov 21 15:31:32 2019 +0100
13.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Mon Nov 25 16:39:52 2019 +0100
13.3 @@ -214,7 +214,7 @@
13.4 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
13.5 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
13.6 (*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
13.7 - ... Ackn_Tac1 ... is correct*)
13.8 + ... Accept_Tac1 ... is correct*)
13.9 "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
13.10 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
13.11 1 < length l (*true*);
13.12 @@ -232,11 +232,11 @@
13.13 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
13.14 val [(tac_, mout, ctree, pos', xxx)] = ss;
13.15 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
13.16 -(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
13.17 - ... Ackn_Tac1 ... is correct*)
13.18 +(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),ORundef) ((E, l@[R,D], a,v,S,b),ss) body
13.19 + ... Accept_Tac1 ... is correct*)
13.20 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
13.21 - ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
13.22 -val (a', Program.Tac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
13.23 + ((((y,s),d),ORundef), ((E, l@[R,D], a,v,S,b),ss), body);
13.24 +val (a', Program.Tac stac) = interpret_leaf "locate" thy' sr (E, (a, v)) t
13.25 val ctxt = get_ctxt pt (p,p_)
13.26 val p' = lev_on p : pos;
13.27 (* WAS val NotAss = associate pt d (m, stac)
14.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Nov 21 15:31:32 2019 +0100
14.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Mon Nov 25 16:39:52 2019 +0100
14.3 @@ -119,14 +119,14 @@
14.4 val E = Env.update E (i, v);
14.5 "~~~~~ fun scan_dn2, args:"; val ((thy as (th,sr)), (pt, p), E, l, t, a, v) =
14.6 (thy, ptp, E, (up@[R,D]), body, a, v);
14.7 -"~~~~~ fun handle_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
14.8 -"~~~~~ fun subst_stacexpr, args:"; val (E, a, v,
14.9 +"~~~~~ fun interpret_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
14.10 +"~~~~~ fun eval_leaf, args:"; val (E, a, v,
14.11 (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
14.12 val Program.Tac tm = Program.Tac (subst_atomic E t);
14.13 term2str tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
14.14 (* ------ ^^^ ----- ? "x" ?*)
14.15 -"~~~~~ to handle_leaf return val:"; val ((a', Program.Tac stac)) = ((NONE, Program.Tac (subst_atomic E t)));
14.16 -val stac' = eval_listexpr_ (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
14.17 +"~~~~~ to interpret_leaf return val:"; val ((a', Program.Tac stac)) = ((NONE, Program.Tac (subst_atomic E t)));
14.18 +val stac' = eval_prog_expr (assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
14.19 term2str stac' = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
14.20 "~~~~~ to scan_dn2 return val:"; val ((a', Program.Tac stac)) = ((a', Program.Tac stac'));
14.21 val (m,m') = stac2tac_ pt (assoc_thy th) stac;
15.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Thu Nov 21 15:31:32 2019 +0100
15.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Nov 25 16:39:52 2019 +0100
15.3 @@ -493,7 +493,7 @@
15.4 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
15.5 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
15.6 l = [] = false;
15.7 -go_scan_up2 thy ptp sc ist Skip_ (*--> Ackn_Tac2 (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
15.8 +go_scan_up2 thy ptp sc ist Skip_ (*--> Accept_Tac2 (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
15.9 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
15.10 ;
15.11 (*----------------------------------------------------------------------------------------------*)
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Nov 21 15:31:32 2019 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Nov 25 16:39:52 2019 +0100
16.3 @@ -146,7 +146,7 @@
16.4 (* a leaf has been found *)
16.5 "~~~~~ fun scan_dn2, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
16.6 (thy, ptp, E, (l @ [Celem.R]), e, a, v);
16.7 -val (a', Program.Tac stac) = handle_leaf "next " th sr (E, (a, v)) t;
16.8 +val (a', Program.Tac stac) = interpret_leaf "next " th sr (E, (a, v)) t;
16.9 val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac;
16.10 "~~~~~ fun stac2tac_, args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
16.11 (pt, (Celem.assoc_thy th), stac);
17.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Nov 21 15:31:32 2019 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Nov 25 16:39:52 2019 +0100
17.3 @@ -58,28 +58,28 @@
17.4 = ((progr, (cstate, ctxt, tac)), istate);
17.5 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
17.6
17.7 - scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
17.8 + scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog);
17.9 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
17.10 - = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
17.11 + = (cctt, (ist |> set_path [R] |> set_or ORundef), (Program.body_of prog));
17.12
17.13 -val Ackn_Tac1 (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
17.14 +val Accept_Tac1 (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
17.15 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
17.16 "~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*),_) $e1 $ e2 $ a)) =
17.17 (xxx, (ist |> path_down [L, R]), e);
17.18
17.19 -val Ackn_Tac1 _ = (*case*)
17.20 +val Accept_Tac1 _ = (*case*)
17.21 scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
17.22 "~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const ("Tactical.Try"(*1*),_) $ e)) =
17.23 (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
17.24
17.25 (*+*)term2str e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
17.26
17.27 -val Ackn_Tac1 _ = (*case*)
17.28 +val Accept_Tac1 _ = (*case*)
17.29 scan_dn1 xxx (ist |> path_down_form ([L, R], a)) e (*of*);
17.30 (*======= end of scanning tacticals, a leaf =======*)
17.31 "~~~~~ fun scan_dn1, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
17.32 (xxx, (ist |> path_down_form ([L, R], a)), e);
17.33 -val (a', Program.Tac stac) = (*case*) handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
17.34 +val (a', Program.Tac stac) = (*case*) interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
17.35
17.36 val Ass (Rewrite_Set' _, _, _) = (*case*)
17.37 associate pt ctxt (m, stac) (*of*);
17.38 @@ -109,13 +109,13 @@
17.39 "~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), (Rule.Prog prog), (Istate.Pstate ist, _))
17.40 = ((thy', srls), (pt, pos), sc, is);
17.41
17.42 -val Ackn_Tac2 (Rewrite_Set' _, _) = (*case*)
17.43 +val Accept_Tac2 (Rewrite_Set' _, _) = (*case*)
17.44 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
17.45 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
17.46 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
17.47 (*if*) 0 = length path (*else*);
17.48
17.49 -val Ackn_Tac2 (Rewrite_Set' _, _) =
17.50 +val Accept_Tac2 (Rewrite_Set' _, _) =
17.51 go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);
17.52 "~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...})) =
17.53 ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
17.54 @@ -163,7 +163,7 @@
17.55 "~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _))
17.56 = ((thy', srls), (pt, pos), prog, is);
17.57
17.58 -val Ackn_Tac2 (_, _) = (*case*)
17.59 +val Accept_Tac2 (_, _) = (*case*)
17.60 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
17.61 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
17.62 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
17.63 @@ -211,12 +211,12 @@
17.64 "~~~~~ fun scan_dn2 , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))
17.65 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
17.66
17.67 - val Ackn_Tac2 (Subproblem' _, _) = (*case*)
17.68 + val Accept_Tac2 (Subproblem' _, _) = (*case*)
17.69 scan_dn2 xxx (ist |> path_down [L, R]) e (*of*);
17.70 (*========== a leaf has been found ==========*)
17.71 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
17.72 = (xxx, (ist |> path_down [L, R]), e);
17.73 - val (a', Program.Tac stac) = (*case*) Lucin.handle_leaf "next " ctxt eval (get_subst ist) t (*of*);
17.74 + val (a', Program.Tac stac) = (*case*) Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t (*of*);
17.75
17.76 (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy ctxt) stac;
17.77 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
18.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Nov 21 15:31:32 2019 +0100
18.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Nov 25 16:39:52 2019 +0100
18.3 @@ -41,7 +41,7 @@
18.4 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac)
18.5 = (sc, (pt, po), (fst is), (snd is), m);
18.6
18.7 - val Ackn_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
18.8 + val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
18.9 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
18.10 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))),
18.11 (Istate.Pstate (ist as {path, ...})))
18.12 @@ -85,9 +85,9 @@
18.13 = ( yyy, (ist |> path_up), (go (path_up' path) prog));
18.14 val (i, body) = check_Let_up ist prog
18.15 ;
18.16 - (*case*) scan_dn1 xxx (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body (*of*);
18.17 + (*case*) scan_dn1 xxx (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*);
18.18 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
18.19 - = (xxx, (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef), body);
18.20 + = (xxx, (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef), body);
18.21
18.22 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
18.23 (*======= end of scanning tacticals, a leaf =======*)
18.24 @@ -95,22 +95,22 @@
18.25 = (xxx, (ist |> path_down [L, R]), e);
18.26
18.27 val (NONE, Program.Tac _) = (*case*)
18.28 - handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
18.29 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
18.30 + interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*);
18.31 +"~~~~~ fun interpret_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
18.32 = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t);
18.33
18.34 - val (a', Program.Tac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
18.35 -"~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
18.36 + val (a', Program.Tac stac) = (*case*) Prog_Tac.eval_leaf E a v t (*of*);
18.37 +"~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)))
18.38 = (E, a, v, t);
18.39
18.40 (NONE, Program.Tac (subst_atomic E t)); (*return value*)
18.41 -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', Program.Tac stac))
18.42 +"~~~~~ from eval_leaf to interpret_leaf return val:"; val ((a', Program.Tac stac))
18.43 = ((NONE : term option, Program.Tac (subst_atomic E t)));
18.44 val stac' =
18.45 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac);
18.46 + Rewrite.eval_prog_expr (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac);
18.47
18.48 (*return value*) (a', Program.Tac stac');
18.49 -"~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', Program.Tac stac)
18.50 +"~~~~~ from interpret_leaf to scan_dn1 return val:"; val (a', Program.Tac stac)
18.51 = ((a' : term option, Program.Tac stac'));
18.52 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
18.53
19.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Nov 21 15:31:32 2019 +0100
19.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Nov 25 16:39:52 2019 +0100
19.3 @@ -85,7 +85,7 @@
19.4 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
19.5 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
19.6 val (a', Program.Tac stac) = (*case*)
19.7 - handle_leaf "next " ctxt eval (get_subst ist) t;
19.8 + interpret_leaf "next " ctxt eval (get_subst ist) t;
19.9
19.10 val (Check_elementwise "Assumptions", Empty_Tac_) =
19.11 stac2tac_ pt (Celem.assoc_thy ctxt) stac;
20.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Thu Nov 21 15:31:32 2019 +0100
20.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Nov 25 16:39:52 2019 +0100
20.3 @@ -151,8 +151,8 @@
20.4 = (xxx, (ist |> path_down [R]), e);
20.5
20.6 val (a', Program.Tac stac) =
20.7 - (*case*) handle_leaf "next " th sr (get_subst ist) t (*of*);
20.8 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
20.9 + (*case*) interpret_leaf "next " th sr (get_subst ist) t (*of*);
20.10 +"~~~~~ fun interpret_leaf , args:"; val (call, thy, srls, (E, (a, v)), t)
20.11 = ("next ", th, sr, (get_subst ist), t);
20.12
20.13 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),
20.14 @@ -164,11 +164,11 @@
20.15
20.16 (*+*)val SOME (Const ("empty", Ta)) = a;
20.17 (*+*)val Type ("'a", []) = Ta;
20.18 -(*+*)if term2str v = "x = 0 + -1 * -1" then () else error "handle_leaf changed";
20.19 +(*+*)if term2str v = "x = 0 + -1 * -1" then () else error "interpret_leaf changed";
20.20 (*+*)val Type ("Real.real", []) = Tv;
20.21
20.22 - (*case*) Prog_Tac.subst_stacexpr E a v t (*of*);
20.23 -"~~~~~ fun subst_stacexpr , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)))
20.24 + (*case*) Prog_Tac.eval_leaf E a v t (*of*);
20.25 +"~~~~~ fun eval_leaf , args:"; val (E, a, v, (t as (*2*)(Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ _)))
20.26 = (E, a, v, t);
20.27
20.28 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)),
20.29 @@ -185,12 +185,12 @@
20.30
20.31 val SOME a' = (*case*) a (*of*);
20.32
20.33 -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val (a', Program.Tac stac) =
20.34 +"~~~~~ from eval_leaf to interpret_leaf return val:"; val (a', Program.Tac stac) =
20.35 ((a, Program.Tac (subst_atomic E (t $ a'))));
20.36 - val stac' = Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac)
20.37 + val stac' = Rewrite.eval_prog_expr (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac)
20.38 (*------------------------------------------- HERE IS A SECOND subst_atomic ?!?*)
20.39 ;
20.40 -"~~~~~ from handle_leaf to scan_dn2 return val:"; val (a', Program.Tac stac) = (a', Program.Tac stac);
20.41 +"~~~~~ from interpret_leaf to scan_dn2 return val:"; val (a', Program.Tac stac) = (a', Program.Tac stac);
20.42 val (m,m') = (stac2tac_ : ctree -> theory -> term -> input * T) pt (Celem.assoc_thy th) stac;
20.43 case m of
20.44 (**)Rewrite_Inst ([_(*"(''bdv'', x)"*)], ("risolate_bdv_add", _)) => ();
21.1 --- a/test/Tools/isac/ProgLang/listC.sml Thu Nov 21 15:31:32 2019 +0100
21.2 +++ b/test/Tools/isac/ProgLang/listC.sml Mon Nov 25 16:39:52 2019 +0100
21.3 @@ -94,7 +94,7 @@
21.4 else error "LENGTH [1, 1, 1] = 3 ..list_rls changed";
21.5
21.6 val t = str2term "LENGTH [1, 1, 1]";
21.7 -val t = eval_listexpr_ thy list_rls t;
21.8 +val t = eval_prog_expr thy list_rls t;
21.9 case t of Free ("3", _) => ()
21.10 -| _ => error "LENGTH [1, 1, 1] = 3 ..eval_listexpr_ changed";
21.11 +| _ => error "LENGTH [1, 1, 1] = 3 ..eval_prog_expr changed";
21.12
22.1 --- a/test/Tools/isac/ProgLang/prog-tools.sml Thu Nov 21 15:31:32 2019 +0100
22.2 +++ b/test/Tools/isac/ProgLang/prog-tools.sml Mon Nov 25 16:39:52 2019 +0100
22.3 @@ -11,7 +11,7 @@
22.4 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
22.5 "-------- distinguish input to Model -----------------------------------------";
22.6 "-------- fun subpbl, fun pblterm --------------------------------------------";
22.7 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
22.8 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
22.9 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
22.10 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
22.11 "-------- fun op #> ----------------------------------------------------------";
22.12 @@ -175,9 +175,9 @@
22.13 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
22.14 (str2term "someTermWithBdv");
22.15
22.16 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
22.17 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
22.18 -"-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
22.19 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
22.20 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
22.21 +"-------- fun stacpbls, fun eval_leaf -----------------------------------";
22.22 val {scr, ...} = get_met ["Test","sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
22.23 case stacpbls sc of
22.24 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
22.25 @@ -205,8 +205,8 @@
22.26 @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
22.27 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
22.28
22.29 -(* --- fun subst_stacexpr *)
22.30 -case subst_stacexpr [] NONE e_term sc of
22.31 +(* --- fun eval_leaf *)
22.32 +case eval_leaf [] NONE e_term sc of
22.33 (NONE, Expr (Const ("HOL.eq", _) $
22.34 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
22.35 (Const ("HOL.Let", _) $
22.36 @@ -217,7 +217,7 @@
22.37 Free ("e_e", _)) $
22.38 Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
22.39 )) => ()
22.40 -| _ => error "subst_stacexpr [] NONE e_term";
22.41 +| _ => error "eval_leaf [] NONE e_term";
22.42
22.43 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
22.44 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
23.1 --- a/test/Tools/isac/ProgLang/prog_tac.sml Thu Nov 21 15:31:32 2019 +0100
23.2 +++ b/test/Tools/isac/ProgLang/prog_tac.sml Mon Nov 25 16:39:52 2019 +0100
23.3 @@ -7,7 +7,7 @@
23.4 "-----------------------------------------------------------------------------------------------";
23.5 "table of contents -----------------------------------------------------------------------------";
23.6 "-----------------------------------------------------------------------------------------------";
23.7 -"-------- fun subst_stacexpr -------------------------------------------------------------------";
23.8 +"-------- fun eval_leaf -------------------------------------------------------------------";
23.9 "-------- xxx ------";
23.10 "-------- xxx ------";
23.11 "-----------------------------------------------------------------------------------------------";
23.12 @@ -15,11 +15,11 @@
23.13 "-----------------------------------------------------------------------------------------------";
23.14
23.15
23.16 -"-------- fun subst_stacexpr -------------------------------------------------------------------";
23.17 -"-------- fun subst_stacexpr -------------------------------------------------------------------";
23.18 -"-------- fun subst_stacexpr -------------------------------------------------------------------";
23.19 +"-------- fun eval_leaf -------------------------------------------------------------------";
23.20 +"-------- fun eval_leaf -------------------------------------------------------------------";
23.21 +"-------- fun eval_leaf -------------------------------------------------------------------";
23.22 val {scr = Prog sc, ...} = get_met ["Test","sqrt-equ-test"];
23.23 -case subst_stacexpr [] NONE e_term sc of
23.24 +case eval_leaf [] NONE e_term sc of
23.25 (NONE, Expr (Const ("HOL.eq", _) $
23.26 (Const ("Test.solve_root_equ", _) $ Free ("e_e", _) $ Free ("v_v", _)) $
23.27 (Const ("HOL.Let", _) $
23.28 @@ -30,4 +30,4 @@
23.29 Free ("e_e", _)) $
23.30 Abs ("e_e", _, Const ("List.list.Cons", _) $ Free ("e_e", _) $ Const ("List.list.Nil", _)) )
23.31 )) => ()
23.32 -| _ => error "subst_stacexpr [] NONE e_term";
23.33 +| _ => error "eval_leaf [] NONE e_term";