1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jan 20 14:38:46 2020 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Jan 21 09:09:11 2020 +0100
1.3 @@ -394,14 +394,12 @@
1.4 | (Program.Tac prog_tac, form_arg) =>
1.5 check_tac cc ist (form_arg, prog_tac)
1.6
1.7 - (*makes Reject_Tac to Term_Val*)
1.8 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, finish, ...}) =
1.9 - if 1 < length path
1.10 - then
1.11 - scan_up pcc (ist |> path_up) (go_up path sc)
1.12 - else (*interpreted to end*)
1.13 - if finish = Skip_ then Term_Val act_arg else Reject_Tac
1.14 -(* scan is strictly to R, because at L there was a expr_val *)
1.15 + if 1 < length path (*?!?of path = [R] + switch then else*)
1.16 + then scan_up pcc (ist |> path_up) (go_up path sc)
1.17 + else
1.18 + if finish = Skip_ then Term_Val act_arg else raise ERROR "LI.find_next_step without result"
1.19 +(* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
1.20 and scan_up pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up pcc (ist |> set_skip)
1.21 | scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) =
1.22 go_scan_up pcc (ist |> set_skip)
1.23 @@ -409,40 +407,33 @@
1.24 | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
1.25 (case scan_dn cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
1.26 Accept_Tac ict => Accept_Tac ict
1.27 - | Reject_Tac => go_scan_up pcc (ist |> set_skip)
1.28 + | Reject_Tac => go_scan_up pcc (ist (*|> set_skip*))
1.29 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_skip))
1.30 (*no appy_: there was already a stac below*)
1.31 | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.32 (case scan_dn cc (ist |> path_down [R]) e of
1.33 - Accept_Tac lr => Accept_Tac lr
1.34 - | Reject_Tac => go_scan_up pcc (ist |> set_skip)
1.35 + Accept_Tac ict => Accept_Tac ict
1.36 + | Reject_Tac => go_scan_up pcc (ist (*|> set_skip*))
1.37 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_skip))
1.38
1.39 | scan_up pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
1.40 | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up pcc ist
1.41 - | scan_up (pcc as (sc, cc)) (ist as {finish, ...})
1.42 - (Const ("Tactical.Chain"(*3*), _) $ _) =
1.43 - if finish = Napp_
1.44 - then go_scan_up pcc (ist |> path_up)
1.45 - else (*Skip_*)
1.46 + | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
1.47 let
1.48 val e2 = check_Seq_up ist sc
1.49 in
1.50 case scan_dn cc (ist |> path_up_down [R]) e2 of
1.51 - Accept_Tac lr => Accept_Tac lr
1.52 + Accept_Tac ict => Accept_Tac ict
1.53 | Reject_Tac => go_scan_up pcc (ist |> path_up) (*!?! |> set_skip)*)
1.54 | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_skip)
1.55 end
1.56
1.57 - | scan_up (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
1.58 - if finish = Napp_
1.59 - then go_scan_up pcc (ist |> path_up)
1.60 - else (*Skip_*)
1.61 + | scan_up (pcc as (sc, cc)) ist (Const ("HOL.Let"(*1*), _) $ _) =
1.62 let
1.63 val (i, body) = check_Let_up ist sc
1.64 in
1.65 case scan_dn cc (ist |> path_up_down [R, D] |> upd_env i) body of
1.66 - Accept_Tac lre => Accept_Tac lre
1.67 + Accept_Tac ict => Accept_Tac ict
1.68 | Reject_Tac => go_scan_up pcc (ist |> path_up)
1.69 | Term_Val v => go_scan_up pcc (ist |> path_up |> set_act v |> set_skip)
1.70 end
1.71 @@ -456,8 +447,8 @@
1.72 eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.73 then
1.74 case scan_dn cc (ist |> path_down [L, R]) e of
1.75 - Accept_Tac lr => Accept_Tac lr
1.76 - | Reject_Tac => go_scan_up pcc (ist |> set_skip)
1.77 + Accept_Tac ict => Accept_Tac ict
1.78 + | Reject_Tac => go_scan_up pcc (ist (*|> set_skip*))
1.79 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_skip)
1.80 else
1.81 go_scan_up pcc (ist |> set_skip)
1.82 @@ -467,8 +458,8 @@
1.83 eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.84 then
1.85 case scan_dn cc (ist |> path_down [R]) e of
1.86 - Accept_Tac lr => Accept_Tac lr
1.87 - | Reject_Tac => go_scan_up pcc (ist |> set_skip)
1.88 + Accept_Tac ict => Accept_Tac ict
1.89 + | Reject_Tac => go_scan_up pcc (ist (*|> set_skip*))
1.90 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_skip)
1.91 else
1.92 go_scan_up pcc (ist |> set_skip)
2.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Mon Jan 20 14:38:46 2020 +0100
2.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Tue Jan 21 09:09:11 2020 +0100
2.3 @@ -9,7 +9,7 @@
2.4
2.5 datatype asap = ORundef | AssOnly | AssGen;
2.6 val asap2str: asap -> string
2.7 - datatype appy_ = AppUndef_ | Napp_ | Skip_
2.8 + datatype appy_ = AppUndef_(* | Napp_*) | Skip_
2.9 val appy_2str: appy_ -> string
2.10 type pstate
2.11 val e_pstate: pstate
2.12 @@ -47,12 +47,16 @@
2.13 datatype appy_ = (* as argument in scan_up, go_scan_up, from scan_dn *)
2.14 (*Accept_Tac is only (final) return-value, not argument during search *)
2.15 AppUndef_
2.16 +(*
2.17 | Napp_ (* ev. detects 'script is not appropriate for this example' *)
2.18 +*)
2.19 | Skip_; (* detects 'script successfully finished'
2.20 also used as init-value for resuming; this works,
2.21 because 'nxt_up Or e1' treats as Accept_Tac *)
2.22 fun appy_2str AppUndef_ = "AppUndef_"
2.23 +(*
2.24 | appy_2str Napp_ = "Napp_"
2.25 +*)
2.26 | appy_2str Skip_ = "Skip_"
2.27
2.28 type pstate =
3.1 --- a/src/Tools/isac/TODO.thy Mon Jan 20 14:38:46 2020 +0100
3.2 +++ b/src/Tools/isac/TODO.thy Tue Jan 21 09:09:11 2020 +0100
3.3 @@ -27,7 +27,17 @@
3.4 \item xxx
3.5 \item xxx
3.6 \item xxx
3.7 + \item xxx
3.8 + \item xxx
3.9 \item xxx
3.10 + \item rename trans_scan_down2 -> trans_scan_down
3.11 + \item xxx
3.12 + \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
3.13 + \item xxx
3.14 + \item switch args
3.15 + check_tac cc ist (form_arg, prog_tac) to
3.16 + check_tac cc ist (prog_tac, form_arg)
3.17 + + in check_tac1
3.18 \item xxx
3.19 \item shift check_leaf Lucin --> LucinNEW ? LItool ?
3.20 \item xxx
4.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Jan 20 14:38:46 2020 +0100
4.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Jan 21 09:09:11 2020 +0100
4.3 @@ -203,7 +203,7 @@
4.4 scan_up yyy (ist |> path_up) (go_up path prog);
4.5 "~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
4.6 = (yyy, (ist |> path_up), (go_up path prog));
4.7 - (*if*) finish = Napp_ (*else*);
4.8 + (*if* ) finish = Napp_ ( *else*);
4.9 val (i, body) = check_Let_up ist prog;
4.10
4.11 (*case*) scan_dn xxx (ist |> path_up_down [R, D] |> upd_env i) body (*of*);
5.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Jan 20 14:38:46 2020 +0100
5.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Jan 21 09:09:11 2020 +0100
5.3 @@ -76,7 +76,7 @@
5.4 scan_up yyy (ist |> path_up) (go_up path prog);
5.5 "~~~~~ fun scan_up , args:"; val ((yyy as (prog, xxx)), (ist as {finish, ...}), (Const ("HOL.Let"(*1*), _) $ _))
5.6 = (yyy, (ist |> path_up), (go_up path prog));
5.7 - (*if*) finish = Napp_ (*else*);
5.8 + (*if* ) finish = Napp_ ( *else*);
5.9 val (i, body) = check_Let_up ist prog;
5.10
5.11 (*case*)