1.1 --- a/src/Tools/isac/Specify/specify-step.sml Sat May 02 16:34:42 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/specify-step.sml Sat May 02 16:55:14 2020 +0200
1.3 @@ -24,121 +24,78 @@
1.4 check tactics (input by the user, mostly) for applicability
1.5 and determine as much of the result of the tactic as possible initially.
1.6 *)
1.7 -fun check (Tactic.Add_Find ct') (pt, (p, p_)) =
1.8 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.9 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.10 - else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
1.11 - (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
1.12 - | check (Tactic.Add_Given ct') (pt, (p, p_)) =
1.13 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.14 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.15 - else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
1.16 - (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
1.17 - | check (Tactic.Add_Relation ct') (pt, (p, p_)) =
1.18 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.19 - then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.20 - else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
1.21 - | check (Tactic.Apply_Method mI) (pt, (p, p_)) =
1.22 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.23 - then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.24 - else
1.25 +fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))
1.26 + (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
1.27 + | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
1.28 + | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
1.29 + | check (Tactic.Apply_Method mI) (pt, (p, _)) =
1.30 let
1.31 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
1.32 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
1.33 - | _ => error "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
1.34 + | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj"
1.35 val {where_, ...} = Specify.get_pbt pI
1.36 val pres = map (Model.mk_env probl |> subst_atomic) where_
1.37 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
1.38 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
1.39 else ctxt
1.40 - (*TODO.WN110416 here do evalprecond according to fun check_preconds'
1.41 - and then decide on Applicable.No/Applicable.Yes accordingly once more.
1.42 - Implement after all tests are running, since this changes
1.43 - overall system behavior*)
1.44 - in
1.45 - Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
1.46 - end
1.47 - (*required for corner cases, e.g. test setup in inssort.sml*)
1.48 - | check (Tactic.Del_Find ct') (pt, (p, p_)) =
1.49 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.50 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.51 - else Applicable.Yes (Tactic.Del_Find' ct')
1.52 - | check (Tactic.Del_Given ct') (pt, (p, p_)) =
1.53 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.54 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.55 - else Applicable.Yes (Tactic.Del_Given' ct')
1.56 - | check (Tactic.Del_Relation ct') (pt, (p, p_)) =
1.57 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.58 - then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.59 - else Applicable.Yes (Tactic.Del_Relation' ct')
1.60 - | check Tactic.Model_Problem (pt, (p, p_)) =
1.61 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
1.62 - Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.63 - else
1.64 - let
1.65 - val pI' = case Ctree.get_obj I pt p of
1.66 - Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
1.67 - | _ => error "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
1.68 - val {ppc, ...} = Specify.get_pbt pI'
1.69 - val pbl = Generate.init_pbl ppc
1.70 - in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
1.71 - | check (Tactic.Refine_Problem pI) (pt, (p, p_)) =
1.72 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.73 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
1.74 - else
1.75 + in
1.76 + Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt))
1.77 + end
1.78 + (*required for corner cases, e.g. test setup in inssort.sml*)
1.79 + | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
1.80 + | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
1.81 + | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
1.82 + | check Tactic.Model_Problem (pt, (p, _)) =
1.83 + let
1.84 + val pI' = case Ctree.get_obj I pt p of
1.85 + Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
1.86 + | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
1.87 + val {ppc, ...} = Specify.get_pbt pI'
1.88 + val pbl = Generate.init_pbl ppc
1.89 + in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
1.90 + | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
1.91 let
1.92 val (dI, dI', itms) = case Ctree.get_obj I pt p of
1.93 Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
1.94 => (dI, dI', itms)
1.95 - | _ => error "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
1.96 + | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
1.97 val thy = if dI' = ThyC.id_empty then dI else dI';
1.98 in
1.99 case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
1.100 - NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
1.101 + NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
1.102 | SOME (rf as (pI', _)) =>
1.103 if pI' = pI
1.104 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
1.105 + then Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
1.106 else Applicable.Yes (Tactic.Refine_Problem' rf)
1.107 end
1.108 - | check (Tactic.Refine_Tacitly pI) (pt, (p, p_)) =
1.109 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.110 - then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.111 - else
1.112 - let
1.113 - val oris = case Ctree.get_obj I pt p of
1.114 - Ctree.PblObj {origin = (oris, _, _), ...} => oris
1.115 - | _ => error "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
1.116 - in
1.117 - case Specify.refine_ori oris pI of
1.118 - SOME pblID =>
1.119 - Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
1.120 - | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
1.121 - end
1.122 - | check (Tactic.Specify_Method mID) (pt, (p, p_)) =
1.123 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.124 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.125 - else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
1.126 + | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
1.127 + let
1.128 + val oris = case Ctree.get_obj I pt p of
1.129 + Ctree.PblObj {origin = (oris, _, _), ...} => oris
1.130 + | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
1.131 + in
1.132 + case Specify.refine_ori oris pI of
1.133 + SOME pblID =>
1.134 + Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [(*filled later*)]))
1.135 + | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")
1.136 + end
1.137 + | check (Tactic.Specify_Method mID) _ =
1.138 + Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled later*)], [(*filled later*)]))
1.139 | check (Tactic.Specify_Problem pID) (pt, (p, p_)) =
1.140 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.141 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.142 - else
1.143 let
1.144 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
1.145 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
1.146 => (oris, dI, pI, dI', pI', itms)
1.147 - | _ => error "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
1.148 + | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
1.149 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
1.150 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
1.151 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
1.152 then (false, (Generate.init_pbl ppc, []))
1.153 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
1.154 in
1.155 - Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
1.156 - end
1.157 - | check (Tactic.Specify_Theory dI) (pt, (p, p_)) =
1.158 - if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
1.159 - then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
1.160 - else Applicable.Yes (Tactic.Specify_Theory' dI)
1.161 + Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
1.162 + end
1.163 + | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
1.164 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
1.165 | check tac (_, pos) =
1.166 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
2.1 --- a/src/Tools/isac/TODO.thy Sat May 02 16:34:42 2020 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Sat May 02 16:55:14 2020 +0200
2.3 @@ -54,6 +54,8 @@
2.4 text \<open>
2.5 \begin{itemize}
2.6 \item xxx
2.7 + \item Solve_Check: postponed parsing input to _ option
2.8 + \item xxx
2.9 \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?
2.10 \item xxx
2.11 \item ? unify struct.Step and struct.Solve in MathEngine ?