1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Nov 16 20:13:43 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat Nov 16 20:38:55 2019 +0100
1.3 @@ -52,7 +52,7 @@
1.4 val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> assoc;
1.5 val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> assoc
1.6
1.7 - datatype appy = Appy of Tactic.T * Istate.pstate | Napp of Env.T | Skip2 of term * Env.T
1.8 + datatype appy = Appy of Tactic.T * Istate.pstate | Napp | Skip2 of term
1.9 val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> appy
1.10 val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> appy
1.11 val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> appy
1.12 @@ -305,22 +305,20 @@
1.13 Appy of (* applicable Prog_Tac found, search stalled *)
1.14 Tactic.T * (* found associated (fun associate) with Prog_Tac *)
1.15 Istate.pstate (* the current, returned for resuming execution *)
1.16 -| Napp of (* Prog_Tac found was not applicable, may become Skip2 *)
1.17 - Env.T (* TODO delete *)
1.18 +| Napp (* Prog_Tac found was not applicable, may become Skip2 *)
1.19 | Skip2 of (* restarts after Appy, leaves iterations, finishes prog.*)
1.20 - term * (* in case of a Prog_Expr the respective value *)
1.21 - Env.T; (* TODO delete *)
1.22 + term; (* in case of a Prog_Expr the respective value *)
1.23
1.24
1.25 (** scan to a Prog_Tac **)
1.26
1.27 -fun scan_dn2 cc (ist as {env, act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
1.28 +fun scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
1.29 (case scan_dn2 cc (ist|> path_down_form ([L, R], a)) e of
1.30 - Napp _ => (Skip2 (act_arg, env))
1.31 + Napp => Skip2 act_arg
1.32 | goback => goback)
1.33 - | scan_dn2 cc (ist as {env, act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
1.34 + | scan_dn2 cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
1.35 (case scan_dn2 cc (ist |> path_down [R]) e of
1.36 - Napp _ => (Skip2 (act_arg, env))
1.37 + Napp => Skip2 act_arg
1.38 | goback => goback)
1.39
1.40 | scan_dn2 cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
1.41 @@ -328,28 +326,28 @@
1.42 | scan_dn2 cc ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.43 scan_dn2 cc (ist |> path_down [R]) e
1.44
1.45 - | scan_dn2 cc (ist as {env, ...}) (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
1.46 + | scan_dn2 cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
1.47 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
1.48 - Skip2 (v, _) => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act_env (v, env)) e2 (*UPD*)
1.49 + Skip2 v => scan_dn2 cc (ist |> path_down_form ([L, R], a) |> set_act v) e2 (*UPD*)
1.50 | goback => goback)
1.51 - | scan_dn2 cc (ist as {env, ...}) (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
1.52 + | scan_dn2 cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
1.53 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
1.54 - Skip2 (v, _) => scan_dn2 cc (ist |> path_down [R] |> set_act_env (v, env)) e2
1.55 + Skip2 v => scan_dn2 cc (ist |> path_down [R] |> set_act v) e2
1.56 | goback => goback)
1.57
1.58 - | scan_dn2 cc (ist as {env, ...}) (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
1.59 + | scan_dn2 cc ist (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b))) =
1.60 (case scan_dn2 cc (ist |> path_down [L, R]) e of
1.61 - Skip2 (res, _) => scan_dn2 cc (ist |> path_down [R, D] |> upd_env' (env , (Free (i, T), res))) b
1.62 + Skip2 res => scan_dn2 cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
1.63 | goback => goback)
1.64
1.65 - | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
1.66 + | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
1.67 if Rewrite.eval_true_ ctxt eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
1.68 then scan_dn2 cc (ist |> path_down_form ([L, R], a)) e
1.69 - else Skip2 (get_act_env ist)
1.70 - | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.71 + else Skip2 act_arg
1.72 + | scan_dn2 (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.73 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.74 then scan_dn2 cc (ist |> path_down [R]) e
1.75 - else Skip2 (get_act_env ist)
1.76 + else Skip2 act_arg
1.77
1.78 |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.79 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
1.80 @@ -368,7 +366,7 @@
1.81 (*======= end of scanning tacticals, a Prog_Tac as leaf =======*)
1.82 | scan_dn2 ((pt, p), ctxt) (ist as {env, eval, ...}) t =
1.83 case Lucin.handle_leaf "next " ctxt eval (get_subst ist) t of
1.84 - (_, Celem.Expr s) => Skip2 (s, env)
1.85 + (_, Celem.Expr s) => Skip2 s
1.86 | (a', Celem.STac stac) =>
1.87 let
1.88 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
1.89 @@ -378,28 +376,28 @@
1.90 | _ =>
1.91 (case Applicable.applicable_in p pt m of
1.92 Chead.Appl m' => (Appy (m', ist |> set_subst_reset (a', Lucin.tac_2res m')))
1.93 - | _ => Napp env)
1.94 + | _ => Napp)
1.95 end
1.96
1.97 (*makes Napp to Skip2*)
1.98 fun scan_up2 pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
1.99 | scan_up2 pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up2 pcc (ist |> set_appy Skip_)
1.100
1.101 - | scan_up2 (pcc as (_, cc)) (ist as {env, ...}) (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
1.102 + | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
1.103 (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
1.104 Appy lr => Appy lr
1.105 - | Napp E => go_scan_up2 pcc (ist |> set_env E |> set_appy Skip_)
1.106 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> set_act_env (v, env) |> set_appy Skip_))
1.107 + | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.108 + | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.109 (*no appy_: there was already a stac below*)
1.110 - | scan_up2 (pcc as (_, cc)) (ist as {env, ...}) (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.111 + | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.112 (case scan_dn2 cc (ist |> path_down [R]) e of
1.113 Appy lr => Appy lr
1.114 - | Napp _ => go_scan_up2 pcc (ist |> set_env env |> set_appy Skip_)
1.115 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> set_act_env (v, env) |> set_appy Skip_))
1.116 + | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.117 + | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.118
1.119 | scan_up2 pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
1.120 | scan_up2 pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up2 pcc ist
1.121 - | scan_up2 (pcc as (sc, cc)) (ist as {env, finish, ...}) (Const ("Tactical.Chain"(*3*), _) $ _) =
1.122 + | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("Tactical.Chain"(*3*), _) $ _) =
1.123 if finish = Napp_
1.124 then go_scan_up2 pcc (ist |> path_up)
1.125 else (*Skip_*)
1.126 @@ -408,11 +406,11 @@
1.127 in
1.128 case scan_dn2 cc (ist |> path_up_down [R]) e2 of
1.129 Appy lr => Appy lr
1.130 - | Napp _ => go_scan_up2 pcc (ist |> path_up |> set_env env)
1.131 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, env) |> set_appy Skip_)
1.132 + | Napp => go_scan_up2 pcc (ist |> path_up)
1.133 + | Skip2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.134 end
1.135
1.136 - | scan_up2 (pcc as (sc, cc)) (ist as {env, finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
1.137 + | scan_up2 (pcc as (sc, cc)) (ist as {finish, ...}) (Const ("HOL.Let"(*1*), _) $ _) =
1.138 if finish = Napp_
1.139 then go_scan_up2 pcc (ist |> path_up)
1.140 else (*Skip_*)
1.141 @@ -421,31 +419,31 @@
1.142 in
1.143 case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
1.144 Appy lre => Appy lre
1.145 - | Napp _ => go_scan_up2 pcc (ist |> path_up |> set_env env)
1.146 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> path_up |> set_act_env (v, env) |> set_appy Skip_)
1.147 + | Napp => go_scan_up2 pcc (ist |> path_up)
1.148 + | Skip2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.149 end
1.150 | scan_up2 pcc ist (Abs _(*2*)) = go_scan_up2 pcc ist
1.151 | scan_up2 pcc ist (Const ("HOL.Let"(*3*),_) $ _ $ (Abs _)) =
1.152 go_scan_up2 pcc ist
1.153
1.154 (*no appy_: never causes Napp -> Helpless*)
1.155 - | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {env, eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
1.156 + | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
1.157 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.158 then
1.159 case scan_dn2 cc (ist |> path_down [L, R]) e of
1.160 Appy lr => Appy lr
1.161 - | Napp _ => go_scan_up2 pcc (ist |> set_env env |> set_appy Skip_)
1.162 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> set_act_env (v, env) |> set_appy Skip_)
1.163 + | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.164 + | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.165 else
1.166 go_scan_up2 pcc (ist |> set_appy Skip_)
1.167 (*no appy_: never causes Napp - Helpless*)
1.168 - | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {env, eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.169 + | scan_up2 (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
1.170 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.171 then
1.172 case scan_dn2 cc (ist |> path_down [R]) e of
1.173 Appy lr => Appy lr
1.174 - | Napp _ => go_scan_up2 pcc (ist |> set_env env |> set_appy Skip_)
1.175 - | Skip2 (v, _) => go_scan_up2 pcc (ist |> set_act_env (v, env) |> set_appy Skip_)
1.176 + | Napp => go_scan_up2 pcc (ist |> set_appy Skip_)
1.177 + | Skip2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.178 else
1.179 go_scan_up2 pcc (ist |> set_appy Skip_)
1.180
1.181 @@ -456,12 +454,12 @@
1.182 | scan_up2 pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up2 pcc ist
1.183
1.184 | scan_up2 _ _ t = error ("scan_up2 not impl for " ^ Rule.term2str t)
1.185 -and go_scan_up2 (pcc as (sc, _)) (ist as {env, path, finish, ...}) =
1.186 +and go_scan_up2 (pcc as (sc, _)) (ist as {env, path, act_arg, finish, ...}) =
1.187 if 1 < length path
1.188 then
1.189 scan_up2 pcc (ist |> path_up) (go_up path sc)
1.190 else (*interpreted to end*)
1.191 - if finish = Skip_ then Skip2 (get_act_env ist) else Napp env
1.192 + if finish = Skip_ then Skip2 act_arg else Napp
1.193
1.194 fun scan_to_tactic2 (prog, cc) (Istate.Pstate (ist as {path, ...})) =
1.195 if path = []
1.196 @@ -472,7 +470,7 @@
1.197 (*decide for the next applicable Prog_Tac*)
1.198 fun determine_next_tactic (thy, _) (ptp as (pt, (p, _))) (Rule.Prog prog) (Istate.Pstate ist, _(*ctxt*)) =
1.199 (case scan_to_tactic2 (prog, (ptp, thy)) (Istate.Pstate ist) of
1.200 - Skip2 (v, _) => (* program finished *)
1.201 + Skip2 v => (* program finished *)
1.202 (case par_pbl_det pt p of
1.203 (true, p', _) =>
1.204 let
1.205 @@ -483,7 +481,7 @@
1.206 end
1.207 | _ =>
1.208 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)))
1.209 - | Napp _ =>
1.210 + | Napp =>
1.211 (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
1.212 | Appy (m', (ist as {act_arg, ...})) =>
1.213 (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *)