1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Nov 21 15:31:32 2019 +0100
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Nov 25 16:39:52 2019 +0100
1.3 @@ -36,7 +36,7 @@
1.4
1.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.6 datatype expr_val1 =
1.7 - Ackn_Tac1 of Istate.pstate * Proof.context * Tactic.T
1.8 + Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
1.9 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
1.10 | Term_Val1 of term;
1.11 val assoc2str : expr_val1 -> string
1.12 @@ -51,8 +51,9 @@
1.13 val scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> term -> expr_val1;
1.14 val go_scan_up1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.pstate -> expr_val1;
1.15 val scan_to_tactic1: term * (Ctree.state * Proof.context * Tactic.T) -> Istate.T -> expr_val1
1.16 + val interpret_tac1: Ctree.state * Proof.context * Tactic.T -> Istate.pstate -> term option * term -> expr_val1
1.17
1.18 - datatype expr_val2 = Ackn_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
1.19 + datatype expr_val2 = Accept_Tac2 of Tactic.T * Istate.pstate | Reject_Tac2 | Term_Val2 of term
1.20 val scan_dn2: Ctree.state * Rule.theory'(*Proof.context*) -> Istate.pstate -> term -> expr_val2
1.21 val scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> term -> expr_val2
1.22 val go_scan_up2: term * (Ctree.state * Rule.theory') -> Istate.pstate -> expr_val2
1.23 @@ -100,17 +101,33 @@
1.24 datatype expr_val1 = (* "ExprVal" in the sense of denotational semantics *)
1.25 Reject_Tac1 of (* tactic is found but NOT acknowledged, scan is continued *)
1.26 Istate.pstate * Proof.context * Tactic.T (*TODO: revise Pstate {or,...},no args as Reject_Tac2*)
1.27 -| Ackn_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
1.28 +| Accept_Tac1 of (* tactic is found and acknowledged, scan is stalled *)
1.29 Istate.pstate * (* the current state, returned for resuming execution *)
1.30 Proof.context * (* updated according to evaluation of Prog_Tac *)
1.31 Tactic.T (* Prog_Tac is associated to Tactic.input *)
1.32 | Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
1.33 term (* value of Prog_Expr, for updating environment *)
1.34 -fun assoc2str (Ackn_Tac1 _) = "Ackn_Tac1"
1.35 +fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
1.36 | assoc2str (Term_Val1 _) = "Term_Val1"
1.37 | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
1.38
1.39
1.40 +(** interpret a Prog_Tac: is it associated to Tactic ? **)
1.41 +
1.42 +fun interpret_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (form_arg, prog_tac) =
1.43 + case Lucin.associate pt ctxt (tac, prog_tac) of
1.44 + (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
1.45 + Lucin.Ass (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_true (form_arg, v'), ctxt, m)
1.46 + | Lucin.Ass_Weak (m, v', ctxt) => Accept_Tac1 (ist |> set_subst_false (form_arg, v'), ctxt, m)
1.47 +
1.48 + | Lucin.NotAss =>
1.49 + (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
1.50 + AssOnly => Term_Val1 act_arg
1.51 + | _(*ORundef*) =>
1.52 + case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
1.53 + Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Lucin.tac_2res m'), ctxt, tac)
1.54 + | Chead.Notappl _ => Term_Val1 act_arg)
1.55 +
1.56 (** scan to a Prog_Tac **)
1.57
1.58 fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =
1.59 @@ -154,7 +171,7 @@
1.60 then scan_dn1 cct (ist |> path_down [R]) e
1.61 else Term_Val1 act_arg
1.62
1.63 - | scan_dn1 cct (ist as {or = Aundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.64 + | scan_dn1 cct (ist as {or = ORundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.65 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
1.66 Term_Val1 v =>
1.67 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
1.68 @@ -176,54 +193,38 @@
1.69 then scan_dn1 cct (ist |> path_down [L, R]) e1
1.70 else scan_dn1 cct (ist |> path_down [R]) e2
1.71
1.72 - | scan_dn1 ((pt, p), ctxt, tac) (ist as {eval, act_arg, or, ...}) t =
1.73 + | scan_dn1 cct (ist as {eval, ...}) t =
1.74 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
1.75 else
1.76 - case Lucin.handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
1.77 - (a', Program.Expr _) =>
1.78 -(*--------------------------- eval_Prog_Expr -----*)
1.79 - Term_Val1 (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") eval
1.80 - (subst_atomic (Env.update_opt'' (get_act_env ist, a')) t))
1.81 - | (a', Program.Tac stac) =>
1.82 -(*/------------ interprete_Prog_Tac -----*)
1.83 - case Lucin.associate pt ctxt (tac, stac) of
1.84 - (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
1.85 - Lucin.Ass (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_true (a', v'), ctxt, m)
1.86 - | Lucin.Ass_Weak (m, v', ctxt) => Ackn_Tac1 (ist |> set_subst_false (a', v'), ctxt, m)
1.87 -
1.88 - | Lucin.NotAss =>
1.89 - (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
1.90 - AssOnly => Term_Val1 act_arg
1.91 - | _(*Aundef*) =>
1.92 - case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
1.93 - Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (a', Lucin.tac_2res m'), ctxt, tac)
1.94 - | Chead.Notappl _ => Term_Val1 act_arg)
1.95 -(*------------- interprete_tactic ---//*)
1.96 - ;
1.97 + case Lucin.interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t of
1.98 + (form_arg, Program.Expr _) =>
1.99 + Term_Val1 (Rewrite.eval_prog_expr (Celem.assoc_thy "Isac_Knowledge") eval
1.100 + (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
1.101 + | (form_arg, Program.Tac prog_tac) =>
1.102 + interpret_tac1 cct ist (form_arg, prog_tac)
1.103
1.104 fun scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
1.105 | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
1.106
1.107 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
1.108 - (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
1.109 + (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
1.110 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.111 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.112 | goback => goback)
1.113 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
1.114 - (case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
1.115 + (case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
1.116 Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
1.117 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.118 | goback => goback)
1.119
1.120 (*all has been done in (*2*) below*)
1.121 | scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
1.122 - | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
1.123 - (*comes from e1, goes to e2*)
1.124 + | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
1.125 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =
1.126 let
1.127 - val e2 = check_Seq_up ist prog
1.128 + val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
1.129 in
1.130 - case scan_dn1 cct (ist |> path_up_down [R] |> set_or Aundef) e2 of
1.131 + case scan_dn1 cct (ist |> path_up_down [R] |> set_or ORundef) e2 of
1.132 Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.133 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.134 | goback => goback
1.135 @@ -232,8 +233,8 @@
1.136 | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("HOL.Let"(*1*), _) $ _) =
1.137 let
1.138 val (i, body) = check_Let_up ist prog
1.139 - in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body of
1.140 - Ackn_Tac1 iss => Ackn_Tac1 iss
1.141 + in case scan_dn1 cct (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body of
1.142 + Accept_Tac1 iss => Accept_Tac1 iss
1.143 | Reject_Tac1 (ist', ctxt', tac') => go_scan_up1 (prog, (cstate, ctxt', tac')) ist'
1.144 | Term_Val1 v => go_scan_up1 pcct (ist |> path_up |> set_act v)
1.145 end
1.146 @@ -244,7 +245,7 @@
1.147 (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
1.148 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update' a (get_act_env ist)) c)
1.149 then
1.150 - case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or Aundef) e of
1.151 + case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
1.152 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
1.153
1.154 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.155 @@ -254,7 +255,7 @@
1.156 (t as Const ("Tactical.While"(*2*), _) $ c $ e) =
1.157 if Rewrite.eval_true_ "Isac_Knowledge" eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.158 then
1.159 - case scan_dn1 cct (ist |> path_down [R] |> set_or Aundef) e of
1.160 + case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
1.161 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v)
1.162 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
1.163 | goback => goback
1.164 @@ -276,14 +277,14 @@
1.165
1.166 fun scan_to_tactic1 (prog, (cctt as ((_, p), _, _))) (Istate.Pstate (ist as {path, ...})) =
1.167 if path = [] orelse Pos.at_first_tactic(*RM prog path RM WITH determine_next_tactic IN solve*)p
1.168 - then scan_dn1 cctt (ist |> set_path [R] |> set_or Aundef) (Program.body_of prog)
1.169 + then scan_dn1 cctt (ist |> set_path [R] |> set_or ORundef) (Program.body_of prog)
1.170 else go_scan_up1 (prog, cctt) ist
1.171 | scan_to_tactic1 _ _ = raise ERROR "scan_to_tactic1: uncovered pattern in fun.def"
1.172
1.173 (*locate an input tactic within a program*)
1.174 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
1.175 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
1.176 - Ackn_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
1.177 + Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
1.178 if assoc
1.179 then Safe_Step (Istate.Pstate ist, ctxt, tac')
1.180 else Unsafe_Step (Istate.Pstate ist, ctxt, tac')
1.181 @@ -301,7 +302,7 @@
1.182
1.183 datatype expr_val2 = (* "ExprVal" in the sense of denotational semantics *)
1.184 Reject_Tac2 (* tactic is found but NOT acknowledged, scan is continued *)
1.185 -| Ackn_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
1.186 +| Accept_Tac2 of (* tactic is found and acknowledged, scan is stalled *)
1.187 Tactic.T * (* Prog_Tac is applicable_in cstate *)
1.188 Istate.pstate (* the current state, returned for resuming execution *)
1.189 | Term_Val2 of (* Prog_Expr is found and evaluated, scan is continued *)
1.190 @@ -353,11 +354,11 @@
1.191
1.192 |scan_dn2 cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
1.193 (case scan_dn2 cc (ist |> path_down_form ([L, L, R], a)) e1 of
1.194 - Ackn_Tac2 lme => Ackn_Tac2 lme
1.195 + Accept_Tac2 lme => Accept_Tac2 lme
1.196 | _ => scan_dn2 cc (ist |> path_down_form ([L, R], a)) e2)
1.197 | scan_dn2 cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
1.198 (case scan_dn2 cc (ist |> path_down [L, R]) e1 of
1.199 - Ackn_Tac2 lme => Ackn_Tac2 lme
1.200 + Accept_Tac2 lme => Accept_Tac2 lme
1.201 | _ => scan_dn2 cc (ist |> path_down [R]) e2)
1.202
1.203 | scan_dn2 (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
1.204 @@ -368,17 +369,17 @@
1.205 | scan_dn2 ((pt, p), ctxt) (ist as {eval, ...}) t =
1.206 if Tactical.contained_in t then raise TERM ("scan_dn2 expects Prog_Tac or Prog_Expr", [t])
1.207 else
1.208 - case Lucin.handle_leaf "next " ctxt eval (get_subst ist) t of
1.209 + case Lucin.interpret_leaf "next " ctxt eval (get_subst ist) t of
1.210 (_, Program.Expr s) => Term_Val2 s
1.211 | (a', Program.Tac stac) =>
1.212 let
1.213 val (m, m') = Lucin.stac2tac_ pt (Celem.assoc_thy ctxt) stac
1.214 in
1.215 case m of (*TODO?: make applicable_in..Subproblem analogous to other tacs ?refine problem?*)
1.216 - Tactic.Subproblem _ => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.217 + Tactic.Subproblem _ => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.218 | _ =>
1.219 (case Applicable.applicable_in p pt m of
1.220 - Chead.Appl m' => Ackn_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.221 + Chead.Appl m' => Accept_Tac2 (m', ist |> set_subst_reset (a', Lucin.tac_2res m'))
1.222 | _ => Reject_Tac2)
1.223 end
1.224
1.225 @@ -388,13 +389,13 @@
1.226
1.227 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
1.228 (case scan_dn2 cc (ist |> path_down [L, R]) e of (* no appy_: there was already a stac below *)
1.229 - Ackn_Tac2 lr => Ackn_Tac2 lr
1.230 + Accept_Tac2 lr => Accept_Tac2 lr
1.231 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.232 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.233 (*no appy_: there was already a stac below*)
1.234 | scan_up2 (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
1.235 (case scan_dn2 cc (ist |> path_down [R]) e of
1.236 - Ackn_Tac2 lr => Ackn_Tac2 lr
1.237 + Accept_Tac2 lr => Accept_Tac2 lr
1.238 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.239 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_))
1.240
1.241 @@ -408,7 +409,7 @@
1.242 val e2 = check_Seq_up ist sc
1.243 in
1.244 case scan_dn2 cc (ist |> path_up_down [R]) e2 of
1.245 - Ackn_Tac2 lr => Ackn_Tac2 lr
1.246 + Accept_Tac2 lr => Accept_Tac2 lr
1.247 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
1.248 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.249 end
1.250 @@ -421,7 +422,7 @@
1.251 val (i, body) = check_Let_up ist sc
1.252 in
1.253 case scan_dn2 cc (ist |> path_up_down [R, D] |> upd_env i) body of
1.254 - Ackn_Tac2 lre => Ackn_Tac2 lre
1.255 + Accept_Tac2 lre => Accept_Tac2 lre
1.256 | Reject_Tac2 => go_scan_up2 pcc (ist |> path_up)
1.257 | Term_Val2 v => go_scan_up2 pcc (ist |> path_up |> set_act v |> set_appy Skip_)
1.258 end
1.259 @@ -434,7 +435,7 @@
1.260 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.261 then
1.262 case scan_dn2 cc (ist |> path_down [L, R]) e of
1.263 - Ackn_Tac2 lr => Ackn_Tac2 lr
1.264 + Accept_Tac2 lr => Accept_Tac2 lr
1.265 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.266 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.267 else
1.268 @@ -444,7 +445,7 @@
1.269 if Rewrite.eval_true_ ctxt eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
1.270 then
1.271 case scan_dn2 cc (ist |> path_down [R]) e of
1.272 - Ackn_Tac2 lr => Ackn_Tac2 lr
1.273 + Accept_Tac2 lr => Accept_Tac2 lr
1.274 | Reject_Tac2 => go_scan_up2 pcc (ist |> set_appy Skip_)
1.275 | Term_Val2 v => go_scan_up2 pcc (ist |> set_act v |> set_appy Skip_)
1.276 else
1.277 @@ -486,7 +487,7 @@
1.278 (Tactic.End_Detail' (Rule.e_term,[])(*8.6.03*), (Istate.e_istate, ContextC.e_ctxt), (v, Telem.Safe)))
1.279 | Reject_Tac2 =>
1.280 (Tactic.Empty_Tac_, (Istate.e_istate, ContextC.e_ctxt), (Rule.e_term, Telem.Helpless_))(* helpless *)
1.281 - | Ackn_Tac2 (m', (ist as {act_arg, ...})) =>
1.282 + | Accept_Tac2 (m', (ist as {act_arg, ...})) =>
1.283 (m', (Pstate ist, ContextC.e_ctxt), (act_arg, Telem.Safe))) (* found next tac *)
1.284 | determine_next_tactic _ _ _ (is, _) =
1.285 error ("determine_next_tactic: not impl for " ^ (Istate.istate2str is));