1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Nov 16 20:38:55 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 19 14:19:44 2019 +0100
1.3 @@ -35,11 +35,11 @@
1.4 -> Tactic.T * (Istate.T * Proof.context) * (term * Telem.safe)
1.5
1.6 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.7 - datatype assoc =
1.8 - Assoc of Istate.pstate * Proof.context * Tactic.T
1.9 - | NasApp of Istate.pstate * Proof.context * Tactic.T
1.10 - | Skip1 of term;
1.11 - val assoc2str : assoc -> string
1.12 + datatype expr_val1 =
1.13 + Ackn_Tac1 of Istate.pstate * Proof.context * Tactic.T
1.14 + | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
1.15 + | Term_Val1 of term;
1.16 + val assoc2str : expr_val1 -> string
1.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.18 val go : Celem.path -> term -> term
1.19 val go_up: Celem.path -> term -> term
1.20 @@ -47,16 +47,16 @@
1.21 val check_Seq_up: Istate.pstate -> term -> term
1.22 val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
1.23
1.24 - val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc
1.25 - val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> assoc;
1.26 - val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;
1.27 - val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> assoc
1.28 + val scan_dn1: (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1
1.29 + val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
1.30 + val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
1.31 + val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
1.32
1.33 - datatype appy = Appy of Tactic.T * Istate.pstate | Napp | Skip2 of term
1.34 - val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy
1.35 - val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy
1.36 - val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> appy
1.37 - val scan_to_tactic2: term * (Ctree.state * Rule.theory') -> Istate.T -> appy
1.38 + datatype expr_val2 = Ackn_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
1.39 + val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> expr_val2
1.40 + val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> expr_val2
1.41 + val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> expr_val2
1.42 + val scan_to_tactic2: term * (Ctree.state * Rule.theory') -> Istate.T -> expr_val2
1.43 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.44 end
1.45
1.46 @@ -97,18 +97,18 @@
1.47 | Unsafe_Step of Istate.T * Proof.context * Tactic.T
1.48 | Not_Locatable of string
1.49
1.50 -datatype assoc = (* "ExprVal" in the sense of denotational semantics *)
1.51 - Assoc of (* the Prog_Tac is associated, strongly or weakly *)
1.52 - Istate.pstate * (* the current, returned for resuming execution *)
1.53 - Proof.context * (* updated according to execution of Prog_Tac *)
1.54 - Tactic.T (* the Prog_Tac found as accociated to the input *)
1.55 -| NasApp of (* Prog_Tac is NOT associated, but applicable *)
1.56 - Istate.pstate * Proof.context * Tactic.T
1.57 -| Skip1 of (* Prog_Tac not associated, not applicable *)
1.58 - term (* in case of a Prog_Expr the respective value *)
1.59 -fun assoc2str (Assoc _) = "Assoc"
1.60 - | assoc2str (Skip1 _) = "Skip1"
1.61 - | assoc2str (NasApp _) = "NasApp";
1.62 +datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
1.63 + Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
1.64 + Istate.pstate * Proof.context * Tactic.T
1.65 +| Ackn_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
1.66 + Istate.pstate * (* the current state, returned for resuming execution *)
1.67 + Proof.context * (* updated according to evaluation of Prog_Tac *)
1.68 + Tactic.T (* Prog_Tac is associated to Tactic.input *)
1.69 +| Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
1.70 + term (* value of Prog_Expr, for updating environment *)
1.71 +fun assoc2str (Ackn_Tac1 _) = "Ackn_Tac1"
1.72 + | assoc2str (Term_Val1 _) = "Term_Val1"
1.73 + | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
1.74
1.75
1.76 (** scan to a Prog_Tac **)
1.77 @@ -125,23 +125,22 @@
1.78
1.79 | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
1.80 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
1.81 - Skip1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
1.82 - | NasApp (ist', ctxt', tac')
1.83 - => scan_dn1 (cstate, ctxt', tac') (ist
1.84 - |> path_down_form ([L, R], a) |> trans_env_act ist') e2
1.85 + Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
1.86 + | Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist
1.87 + |> path_down_form ([L, R], a) |> trans_env_act ist') e2
1.88 | goback => goback)
1.89 | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $e1 $ e2) =
1.90 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
1.91 - Skip1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
1.92 - | NasApp (ist', ctxt', tac')
1.93 - => scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
1.94 + Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
1.95 + | Reject_Tac1 (ist', ctxt', tac') =>
1.96 + scan_dn1 (cstate, ctxt', tac') (ist |> path_down [R] |> trans_env_act ist') e2
1.97 | goback => goback)
1.98
1.99 | scan_dn1 cct ist (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))) =
1.100 (case scan_dn1 cct (ist |> path_down [L, R]) e of
1.101 - NasApp (ist', _, _) =>
1.102 + Reject_Tac1 (ist', _, _) =>
1.103 scan_dn1 cct (ist' |> path_down [R, D] |> upd_env (TermC.mk_Free (id, T)) |> trans_ass ist) b
1.104 - | Skip1 v =>
1.105 + | Term_Val1 v =>
1.106 scan_dn1 cct (ist |> path_down [R, D] |> upd_env'' (TermC.mk_Free (id, T), v)) b
1.107 | goback => goback)
1.108
1.109 @@ -149,27 +148,27 @@
1.110 if Rewrite.eval_true_ "Isac_Knowledge" eval
1.111 (subst_atomic (ist |> get_act_env |> Env.update' a) c)
1.112 then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
1.113 - else Skip1 act_arg
1.114 + else Term_Val1 act_arg
1.115 | scan_dn1 cct (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*),_) $ c $ e) =
1.116 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.117 then scan_dn1 cct (ist |> path_down [R]) e
1.118 - else Skip1 act_arg
1.119 + else Term_Val1 act_arg
1.120
1.121 | scan_dn1 cct (ist as {or = Aundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.122 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
1.123 - Skip1 v =>
1.124 + Term_Val1 v =>
1.125 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
1.126 - Skip1 v =>
1.127 + Term_Val1 v =>
1.128 (case scan_dn1 cct (ist |> path_down [L, L, R] |> upd_env'' (a, v) |> set_or AssGen) e1 of
1.129 - Skip1 v =>
1.130 + Term_Val1 v =>
1.131 scan_dn1 cct (ist |> path_down [L, R] |> upd_env'' (a, v) |> set_or AssGen) e2
1.132 | goback => goback)
1.133 | goback => goback)
1.134 - | NasApp _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return NasApp")
1.135 + | Reject_Tac1 _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return Reject_Tac1")
1.136 | goback => goback)
1.137 | scan_dn1 cct ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
1.138 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
1.139 - Skip1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
1.140 + Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
1.141 | goback => goback)
1.142
1.143 | scan_dn1 cct (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
1.144 @@ -181,21 +180,21 @@
1.145 | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t =
1.146 (case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
1.147 (a', Celem.Expr _) =>
1.148 - Skip1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
1.149 + Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
1.150 (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t))
1.151 | (a', Celem.STac stac) =>
1.152 (case Lucin.associate pt ctxt (tac, stac) of
1.153 (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
1.154 - Lucin.Ass (m, v', ctxt) => Assoc (ist |> set_subst_true (a', v'), ctxt, m)
1.155 - | Lucin.Ass_Weak (m, v', ctxt) => Assoc (ist |> set_subst_false (a', v'), ctxt, m)
1.156 + Lucin.Ass (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m)
1.157 + | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m)
1.158
1.159 | Lucin.NotAss =>
1.160 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
1.161 - AssOnly => Skip1 act_arg
1.162 + AssOnly => Term_Val1 act_arg
1.163 | _(*Aundef*) =>
1.164 case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
1.165 - Chead.Appl m' => NasApp (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
1.166 - | Chead.Notappl _ => Skip1 act_arg)
1.167 + Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
1.168 + | Chead.Notappl _ => Term_Val1 act_arg)
1.169 ));
1.170
1.171 fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
1.172 @@ -203,13 +202,13 @@
1.173
1.174 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
1.175 (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
1.176 - Skip1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.177 - | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.178 + Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.179 + | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.180 | goback => goback)
1.181 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
1.182 (case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
1.183 - Skip1 v' => go_scan_up1 pcct (ist |> set_act v')
1.184 - | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.185 + Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
1.186 + | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.187 | goback => goback)
1.188
1.189 (*all has been done in (*2*) below*)
1.190 @@ -221,8 +220,8 @@
1.191 val e2 = check_Seq_up ist prog
1.192 in
1.193 case scan_dn1 cct (ist |> path_up_down [R] |> set_or Aundef) e2 of
1.194 - Skip1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.195 - | NasApp (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.196 + Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.197 + | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.198 | goback => goback
1.199 end
1.200
1.201 @@ -230,9 +229,9 @@
1.202 let
1.203 val (i, body) = check_Let_up ist prog
1.204 in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body of
1.205 - Assoc iss => Assoc iss
1.206 - | NasApp (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.207 - | Skip1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.208 + Ackn_Tac1 iss => Ackn_Tac1 iss
1.209 + | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.210 + | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.211 end
1.212 | scan_up1 pcct ist (Abs(*2*) _) = go_scan_up1 pcct ist
1.213 | scan_up1 pcct ist (Const ("HOL.Let"(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
1.214 @@ -242,9 +241,9 @@
1.215 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)
1.216 then
1.217 case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
1.218 - Skip1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.219 + Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.220
1.221 - | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.222 + | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.223 | goback => goback
1.224 else go_scan_up1 pcct (ist |> set_form a)
1.225 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) (ist as {eval, ...})
1.226 @@ -252,8 +251,8 @@
1.227 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.228 then
1.229 case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
1.230 - Skip1 v => go_scan_up1 pcct (ist |> set_act v)
1.231 - | NasApp (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.232 + Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
1.233 + | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.234 | goback => goback
1.235 else go_scan_up1 pcct ist
1.236
1.237 @@ -269,7 +268,7 @@
1.238 and go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
1.239 if 1 < length path
1.240 then scan_up1 pcct (ist |> path_up) (go (path_up' path) prog)
1.241 - else Skip1 act_arg
1.242 + else Term_Val1 act_arg
1.243
1.244 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
1.245 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
1.246 @@ -280,11 +279,11 @@
1.247 (*locate an input tactic within a program*)
1.248 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
1.249 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
1.250 - Assoc ((ist as {assoc, ...}), ctxt, tac') =>
1.251 + Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
1.252 if assoc
1.253 then Safe_Step (Istate.Pstate ist, ctxt, tac')
1.254 else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
1.255 - | NasApp _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")
1.256 + | Reject_Tac1 _ => Not_Locatable (Tactic.tac_2str tac ^ " not locatable")
1.257 | err => raise ERROR ("not-found-in-script: NotLocatable from " ^ @{make_string} err))
1.258 | locate_input_tactic _ _ _ _ _ = raise ERROR "locate_input_tactic: uncovered case in definition"
1.259
1.260 @@ -294,6 +293,16 @@
1.261 datatype next_tactic_result = NStep of Ctree.state * Istate.T * Proof.context * tactic
1.262 | Helpless | End_Program
1.263
1.264 +(** scan to a Prog_Tac **)
1.265 +
1.266 +datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics *)
1.267 + Reject_Tac2 (* tactic is found but NOT acknowledged, scan is continued *)
1.268 +| Ackn_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
1.269 + Tactic.T * (* Prog_Tac is applicable_in cstate *)
1.270 + Istate.pstate (* the current state, returned for resuming execution *)
1.271 +| Term_Val2 of (* Prog_Expr is found and evaluated, scan is continued *)
1.272 + term; (* value of Prog_Expr, for updating environment *)
1.273 +
1.274 (*
1.275 scan_dn2, go_scan_up2, scan_up2 scan for determine_next_tactic.
1.276 (1) scan_dn2 is recursive descent;
1.277 @@ -301,24 +310,13 @@
1.278 (3) scan_up2 resumes according to the interpreter-state.
1.279 Call of (2) means that there was an applicable Prog_Tac below
1.280 *)
1.281 -datatype appy = (* "ExprVal" in the sense of denotational semantics *)
1.282 - Appy of (* applicable Prog_Tac found, search stalled *)
1.283 - Tactic.T * (* found associated (fun associate) with Prog_Tac *)
1.284 - Istate.pstate (* the current, returned for resuming execution *)
1.285 -| Napp (* Prog_Tac found was not applicable, may become Skip2 *)
1.286 -| Skip2 of (* restarts after Appy, leaves iterations, finishes prog.*)
1.287 - term; (* in case of a Prog_Expr the respective value *)
1.288 -
1.289 -
1.290 -(** scan to a Prog_Tac **)
1.291 -
1.292 fun scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
1.293 (case scan_dn2 cc (ist|> path_down_form ([L, R], a)) e of
1.294 - Napp => Skip2 act_arg
1.295 + Reject_Tac2 => Term_Val2 act_arg
1.296 | goback => goback)
1.297 | scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
1.298 (case scan_dn2 cc (ist |> path_down [R]) e of
1.299 - Napp => Skip2 act_arg
1.300 + Reject_Tac2 => Term_Val2 act_arg
1.301 | goback => goback)
1.302
1.303 | scan_dn2 cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
1.304 @@ -328,34 +326,34 @@
1.305
1.306 | scan_dn2 cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
1.307 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
1.308 - Skip2 v => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act v) e2 (*UPD*)
1.309 + Term_Val2 v => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act v) e2 (*UPD*)
1.310 | goback => goback)
1.311 | scan_dn2 cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
1.312 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
1.313 - Skip2 v => scan_dn2 cc (ist |> path_down [R] |> set_act v) e2
1.314 + Term_Val2 v => scan_dn2 cc (ist |> path_down [R] |> set_act v) e2
1.315 | goback => goback)
1.316
1.317 | scan_dn2 cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
1.318 (case scan_dn2 cc (ist |> path_down [L, R]) e of
1.319 - Skip2 res => scan_dn2 cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
1.320 + Term_Val2 res => scan_dn2 cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
1.321 | goback => goback)
1.322
1.323 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
1.324 if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
1.325 then scan_dn2 cc (ist |> path_down_form ([L, R], a)) e
1.326 - else Skip2 act_arg
1.327 + else Term_Val2 act_arg
1.328 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.329 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.330 then scan_dn2 cc (ist |> path_down [R]) e
1.331 - else Skip2 act_arg
1.332 + else Term_Val2 act_arg
1.333
1.334 |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.335 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
1.336 - Appy lme => Appy lme
1.337 + Ackn_Tac2 lme => Ackn_Tac2 lme
1.338 | _ => scan_dn2 cc (ist |> path_down_form ([L, R], a)) e2)
1.339 | scan_dn2 cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
1.340 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
1.341 - Appy lme => Appy lme
1.342 + Ackn_Tac2 lme => Ackn_Tac2 lme
1.343 | _ => scan_dn2 cc (ist |> path_down [R]) e2)
1.344
1.345 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
1.346 @@ -366,34 +364,34 @@
1.347 (*======= end of scanning tacticals, a Prog_Tac as leaf =======*)
1.348 | scan_dn2 ((pt, p), ctxt) (ist as {env, eval, ...}) t =
1.349 case Lucin.handle_leaf "next " ctxt eval (get_subst ist) t of
1.350 - (_, Celem.Expr s) => Skip2 s
1.351 + (_, Celem.Expr s) => Term_Val2 s
1.352 | (a', Celem.STac stac) =>
1.353 let
1.354 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
1.355 in
1.356 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
1.357 - Tactic.Subproblem _ => Appy (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.358 + Tactic.Subproblem _ => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.359 | _ =>
1.360 (case Applicable.applicable_in p pt m of
1.361 - Chead.Appl m' => (Appy (m', ist |> set_subst_reset (a', Lucin.tac_2res m')))
1.362 - | _ => Napp)
1.363 + Chead.Appl m' => (Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m')))
1.364 + | _ => Reject_Tac2)
1.365 end
1.366
1.367 - (*makes Napp to Skip2*)
1.368 + (*makes Reject_Tac2 to Term_Val2*)
1.369 fun scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
1.370 | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
1.371
1.372 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
1.373 (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
1.374 - Appy lr => Appy lr
1.375 - | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.376 - | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.377 + Ackn_Tac2 lr => Ackn_Tac2 lr
1.378 + | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.379 + | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.380 (*no appy_: there was already a stac below*)
1.381 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.382 (case scan_dn2 cc (ist |> path_down [R]) e of
1.383 - Appy lr => Appy lr
1.384 - | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.385 - | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.386 + Ackn_Tac2 lr => Ackn_Tac2 lr
1.387 + | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.388 + | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.389
1.390 | scan_up2 pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
1.391 | scan_up2 pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist
1.392 @@ -405,9 +403,9 @@
1.393 val e2 = check_Seq_up ist sc
1.394 in
1.395 case scan_dn2 cc (ist |> path_up_down [R]) e2 of
1.396 - Appy lr => Appy lr
1.397 - | Napp => go_scan_up2 pcc (ist |> path_up)
1.398 - | Skip2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.399 + Ackn_Tac2 lr => Ackn_Tac2 lr
1.400 + | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
1.401 + | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.402 end
1.403
1.404 | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
1.405 @@ -418,32 +416,32 @@
1.406 val (i, body) = check_Let_up ist sc
1.407 in
1.408 case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
1.409 - Appy lre => Appy lre
1.410 - | Napp => go_scan_up2 pcc (ist |> path_up)
1.411 - | Skip2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.412 + Ackn_Tac2 lre => Ackn_Tac2 lre
1.413 + | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
1.414 + | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.415 end
1.416 | scan_up2 pcc ist (Abs _(*2*)) = go_scan_up2 pcc ist
1.417 | scan_up2 pcc ist (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) =
1.418 go_scan_up2 pcc ist
1.419
1.420 - (*no appy_: never causes Napp -> Helpless*)
1.421 + (*no appy_: never causes Reject_Tac2 -> Helpless*)
1.422 | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
1.423 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.424 then
1.425 case scan_dn2 cc (ist |> path_down [L, R]) e of
1.426 - Appy lr => Appy lr
1.427 - | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.428 - | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.429 + Ackn_Tac2 lr => Ackn_Tac2 lr
1.430 + | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.431 + | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.432 else
1.433 go_scan_up2 pcc (ist |> set_appy Skip_)
1.434 - (*no appy_: never causes Napp - Helpless*)
1.435 + (*no appy_: never causes Reject_Tac2 - Helpless*)
1.436 | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.437 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.438 then
1.439 case scan_dn2 cc (ist |> path_down [R]) e of
1.440 - Appy lr => Appy lr
1.441 - | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.442 - | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.443 + Ackn_Tac2 lr => Ackn_Tac2 lr
1.444 + | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.445 + | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.446 else
1.447 go_scan_up2 pcc (ist |> set_appy Skip_)
1.448
1.449 @@ -459,7 +457,7 @@
1.450 then
1.451 scan_up2 pcc (ist |> path_up) (go_up path sc)
1.452 else (*interpreted to end*)
1.453 - if finish = Skip_ then Skip2 act_arg else Napp
1.454 + if finish = Skip_ then Term_Val2 act_arg else Reject_Tac2
1.455
1.456 fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
1.457 if path = []
1.458 @@ -470,7 +468,7 @@
1.459 (*decide for the next applicable Prog_Tac*)
1.460 fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, _(*ctxt*)) =
1.461 (case scan_to_tactic2 (prog, (ptp, thy)) (Istate.Pstate ist) of
1.462 - Skip2 v => (* program finished *)
1.463 + Term_Val2 v => (* program finished *)
1.464 (case par_pbl_det pt p of
1.465 (true, p', _) =>
1.466 let
1.467 @@ -481,9 +479,9 @@
1.468 end
1.469 | _ =>
1.470 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)))
1.471 - | Napp =>
1.472 + | Reject_Tac2 =>
1.473 (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
1.474 - | Appy (m', (ist as {act_arg, ...})) =>
1.475 + | Ackn_Tac2 (m', (ist as {act_arg, ...})) =>
1.476 (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *)
1.477 | determine_next_tactic _ _ _ (is, _) =
1.478 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));
2.1 --- a/src/Tools/isac/Interpret/script.sml Sat Nov 16 20:38:55 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/script.sml Tue Nov 19 14:19:44 2019 +0100
2.3 @@ -59,7 +59,7 @@
2.4 (**)
2.5 (* data for creating a new node in ctree; designed for use as:
2.6 fun ass* pstate steps = / ... case ass* pstate steps of /
2.7 - Assoc (pstate, steps) => ... ass* pstate steps *)
2.8 + Ackn_Tac1 (pstate, steps) => ... ass* pstate steps *)
2.9 type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
2.10 WN190713 COMPARE: taci list, see papernote #139 *)
2.11 Tactic.T (*transformed from associated tac *)
3.1 --- a/src/Tools/isac/MathEngBasic/istate.sml Sat Nov 16 20:38:55 2019 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/istate.sml Tue Nov 19 14:19:44 2019 +0100
3.3 @@ -72,13 +72,13 @@
3.4 | asap2str AssOnly = "AssOnly"
3.5 | asap2str AssGen = "AssGen"
3.6
3.7 -datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *)
3.8 -(*Appy is only (final) returnvalue, not argument during search *)
3.9 +datatype appy_ = (* as argument in scan_up2, go_scan_up2, from scan_dn2 *)
3.10 +(*Ackn_Tac2 is only (final) returnvalue, not argument during search *)
3.11 AppUndef_
3.12 | Napp_ (* ev. detects 'script is not appropriate for this example' *)
3.13 | Skip_; (* detects 'script successfully finished'
3.14 also used as init-value for resuming; this works,
3.15 - because 'nxt_up Or e1' treats as Appy *)
3.16 + because 'nxt_up Or e1' treats as Ackn_Tac2 *)
3.17 fun appy_2str AppUndef_ = "AppUndef_"
3.18 | appy_2str Napp_ = "Napp_"
3.19 | appy_2str Skip_ = "Skip_"
4.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sat Nov 16 20:38:55 2019 +0100
4.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Nov 19 14:19:44 2019 +0100
4.3 @@ -71,7 +71,7 @@
4.4 = ((prog, (cstate, ctxt, tac)), istate);
4.5 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*then*);
4.6
4.7 - val Assoc (_, _, Take' _) =
4.8 + val Ackn_Tac1 (_, _, Take' _) =
4.9 scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog);
4.10 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
4.11 = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
4.12 @@ -128,7 +128,7 @@
4.13 = (sc, (pt, po), (fst is), (snd is), m);
4.14 val srls = get_simplifier cstate;
4.15
4.16 - (** )val Assoc ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
4.17 + (** )val Ackn_Tac1 ((is as (_,_,_,_,_,strong_ass), ctxt, ss as((tac', _, ctree, pos', _) :: _))) =( **)
4.18 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
4.19 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
4.20 = ((prog, (cstate, ctxt, tac)), istate);
4.21 @@ -156,12 +156,12 @@
4.22 val Lucin.Ass (m, v', ctxt) =
4.23 (*case*) associate pt ctxt (m, stac) (*of*);
4.24
4.25 - Assoc (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
4.26 + Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
4.27 "~~~~~ from scan_dn1 to scan_to_tactic1 return val:"; val (xxxxx_xx)
4.28 - = (Assoc (ist |> set_subst_true (a', v'), ctxt, m));
4.29 + = (Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
4.30
4.31 -"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Assoc ((ist as {assoc, ...}), ctxt, tac')
4.32 - = (Assoc (ist |> set_subst_true (a', v'), ctxt, m));
4.33 +"~~~~~ from scan_to_tactic1 to fun locate_input_tactic return val:"; val Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac')
4.34 + = (Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m));
4.35 (*if*) LibraryC.assoc (*then*);
4.36
4.37 Safe_Step (Istate.Pstate ist, ctxt, tac') (*return value*);
4.38 @@ -334,7 +334,7 @@
4.39 val Notappl "norm_equation not applicable" =
4.40 (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
4.41
4.42 - (Skip1 act_arg) (* return value *);
4.43 + (Term_Val1 act_arg) (* return value *);
4.44
4.45 val Rewrite' ("PolyMinus", "tless_true", _, _, ("tausche_minus",_ (*"?b ist_monom \<Longrightarrow> ?a kleiner ?b \<Longrightarrow> ?b - ?a = - ?a + ?b"*)),
4.46 t, (res, asm)) = m;
5.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Sat Nov 16 20:38:55 2019 +0100
5.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Nov 19 14:19:44 2019 +0100
5.3 @@ -199,29 +199,29 @@
5.4 (*TODO simplify assumptions (sqrt!) and check ERROR in has_degree_in*);
5.5 member op = specsteps mI (*false*);
5.6 (*loc_solve_ (mI,m) ptp;
5.7 - WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
5.8 + WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
5.9 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
5.10 (*solve m (pt, pos);
5.11 - WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
5.12 + WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
5.13 "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
5.14 e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
5.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
5.16 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
5.17 val d = e_rls;
5.18 (*locate_input_tactic (thy',srls) m (pt,(p,p_)) (sc,d) is;
5.19 - WAS: not-found-in-script: NotLocatable from Skip1 (Const ("List...*)
5.20 + WAS: not-found-in-script: NotLocatable from Term_Val1 (Const ("List...*)
5.21 "~~~~~ fun locate_input_tactic, args:"; val () = ();
5.22 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
5.23 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
5.24 -(*WAS val NasApp _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
5.25 - ... Assoc ... is correct*)
5.26 +(*WAS val Reject_Tac1 _ =(go_scan_up1 (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
5.27 + ... Ackn_Tac1 ... is correct*)
5.28 "~~~~~ and go_scan_up1, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
5.29 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
5.30 1 < length l (*true*);
5.31 val up = drop_last l;
5.32 term2str (go up sc);
5.33 (go up sc);
5.34 -(*WAS val Skip1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
5.35 +(*WAS val Term_Val1 _ = scan_up1 ys ((E,up,a,v,S,b),ss) (go up sc)
5.36 ... ???? ... is correct*)
5.37 "~~~~~ fun scan_up1, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
5.38 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss:step list), (go up sc));
5.39 @@ -232,8 +232,8 @@
5.40 (*Type error ...: Can't unify _a to pos * pos_ (Incompatible types)*)
5.41 val [(tac_, mout, ctree, pos', xxx)] = ss;
5.42 val ss = [(tac_, mout, ctree, pos', []:(pos * pos_) list)];
5.43 -(*WAS val NasApp iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
5.44 - ... Assoc ... is correct*)
5.45 +(*WAS val Reject_Tac1 iss = scan_dn1 (((y,s),d),Aundef) ((E, l@[R,D], a,v,S,b),ss) body
5.46 + ... Ackn_Tac1 ... is correct*)
5.47 "~~~~~ fun scan_dn1, args:"; val ((((thy',sr),d),ap), (is as (E,l,a,v,S,b), (m,_,pt,(p,p_),c)::ss), t) =
5.48 ((((y,s),d),Aundef), ((E, l@[R,D], a,v,S,b),ss), body);
5.49 val (a', STac stac) = handle_leaf "locate" thy' sr (E, (a, v)) t
6.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Sat Nov 16 20:38:55 2019 +0100
6.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Nov 19 14:19:44 2019 +0100
6.3 @@ -493,7 +493,7 @@
6.4 "~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, pos as (p, _)):ctree * pos'),
6.5 (sc as Prog (h $ body)), (Pstate (ist as (E,l,rls,a,v,s,b)), ctxt)) = ((thy',srls), (pt,pos), sc, is);
6.6 l = [] = false;
6.7 -go_scan_up2 thy ptp sc ist Skip_ (*--> Appy (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
6.8 +go_scan_up2 thy ptp sc ist Skip_ (*--> Ackn_Tac2 (Rewrite' (.., (.., "Test.rnorm_equation_add"), ...)
6.9 BUT WE FIND IN THE CODE ABOVE IN determine_next_tactic:*)
6.10 ;
6.11 (*----------------------------------------------------------------------------------------------*)
7.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Sat Nov 16 20:38:55 2019 +0100
7.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Nov 19 14:19:44 2019 +0100
7.3 @@ -62,19 +62,19 @@
7.4 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b))))
7.5 = (cctt, (ist |> set_path [R] |> set_or Aundef), (Program.body_of prog));
7.6
7.7 -val Assoc (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
7.8 +val Ackn_Tac1 (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
7.9 scan_dn1 xxx (ist |> path_down [L, R]) e (*of*);
7.10 "~~~~~ fun scan_dn1, args:"; val ((xxx as (cstate, _, _)), ist, (Const ("Tactical.Chain"(*1*),_) $e1 $ e2 $ a)) =
7.11 (xxx, (ist |> path_down [L, R]), e);
7.12
7.13 -val Assoc _ = (*case*)
7.14 +val Ackn_Tac1 _ = (*case*)
7.15 scan_dn1 xxx (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
7.16 "~~~~~ fun scan_dn1, args:"; val (xxx, ist, (Const ("Tactical.Try"(*1*),_) $ e)) =
7.17 (xxx, (ist |> path_down_form ([L, L, R], a)), e1);
7.18
7.19 (*+*)term2str e1 = "Try (Rewrite_Set ''norm_equation'')" (*in isabisac*);
7.20
7.21 -val Assoc _ = (*case*)
7.22 +val Ackn_Tac1 _ = (*case*)
7.23 scan_dn1 xxx (ist |> path_down_form ([L, R], a)) e (*of*);
7.24 (*======= end of scanning tacticals, a leaf =======*)
7.25 "~~~~~ fun scan_dn1, args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
7.26 @@ -109,13 +109,13 @@
7.27 "~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), (Rule.Prog prog), (Istate.Pstate ist, _))
7.28 = ((thy', srls), (pt, pos), sc, is);
7.29
7.30 -val Appy (Rewrite_Set' _, _) = (*case*)
7.31 +val Ackn_Tac2 (Rewrite_Set' _, _) = (*case*)
7.32 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
7.33 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
7.34 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
7.35 (*if*) 0 = length path (*else*);
7.36
7.37 -val Appy (Rewrite_Set' _, _) =
7.38 +val Ackn_Tac2 (Rewrite_Set' _, _) =
7.39 go_scan_up2 (prog, cct) (trans_scan_up2 ist |> set_appy Skip_);
7.40 "~~~~~ and go_scan_up2 , args:"; val ((yyy as (prog, _)), (ist as {env, path, finish, ...})) =
7.41 ((prog, cct), (trans_scan_up2 ist |> set_appy Skip_));
7.42 @@ -163,7 +163,7 @@
7.43 "~~~~~ fun determine_next_tactic , args:"; val ((ctxt, _), (ptp as (pt, p)), sc, (Istate.Pstate ist, _))
7.44 = ((thy', srls), (pt, pos), prog, is);
7.45
7.46 -val Appy (_, _) = (*case*)
7.47 +val Ackn_Tac2 (_, _) = (*case*)
7.48 scan_to_tactic2 (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
7.49 "~~~~~ fun scan_to_tactic2 , args:"; val ((prog, cct), (Istate.Pstate (ist as {path, ...})))
7.50 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
7.51 @@ -211,7 +211,7 @@
7.52 "~~~~~ fun scan_dn2 , args:"; val (xxx, ist, (Const ("HOL.Let"(*1*),_) $ e $ (Abs (i,T,b))))
7.53 = (xxx, (ist |> path_up_down [R, D] |> upd_env i), body);
7.54
7.55 - val Appy (Subproblem' _, _) = (*case*)
7.56 + val Ackn_Tac2 (Subproblem' _, _) = (*case*)
7.57 scan_dn2 xxx (ist |> path_down [L, R]) e (*of*);
7.58 (*========== a leaf has been found ==========*)
7.59 "~~~~~ fun scan_dn2 , args:"; val (((pt, p), ctxt), (ist as {env, eval, ...}), t)
8.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Sat Nov 16 20:38:55 2019 +0100
8.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Nov 19 14:19:44 2019 +0100
8.3 @@ -41,7 +41,7 @@
8.4 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac)
8.5 = (sc, (pt, po), (fst is), (snd is), m);
8.6
8.7 - val Assoc (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
8.8 + val Ackn_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*)
8.9 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
8.10 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))),
8.11 (Istate.Pstate (ist as {path, ...})))