1.1 --- a/src/Tools/isac/Interpret/solve-step.sml Mon May 04 11:13:16 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Mon May 04 12:38:16 2020 +0200
1.3 @@ -9,16 +9,22 @@
1.4 sig
1.5 val check: Tactic.input -> Calc.T -> Applicable.T
1.6 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
1.7 +
1.8 val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
1.9 val s_add_general: State_Steps.T ->
1.10 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
1.11 val add_hard:
1.12 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
1.13
1.14 + val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
1.15 + string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
1.16 + val get_eval: string -> Pos.pos ->Ctree.ctree ->
1.17 + string * ThyC.id * (string * Rule_Def.eval_fn)
1.18 +
1.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.20 (*NONE*)
1.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.22 - (*NONE*)
1.23 + val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
1.24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.25 end
1.26
1.27 @@ -27,6 +33,62 @@
1.28 struct
1.29 (**)
1.30
1.31 +(** get data from Calc.T **)
1.32 +
1.33 +(* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *)
1.34 +fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.35 + (rew_ord', erls, ca)
1.36 + | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.37 + (rew_ord', erls, ca)
1.38 + | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
1.39 + (rew_ord', erls, ca)
1.40 + | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
1.41 +
1.42 +fun get_ruleset _ p pt =
1.43 + let
1.44 + val (pbl, p', rls') = Ctree.parent_node pt p
1.45 + in
1.46 + if pbl
1.47 + then
1.48 + let
1.49 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
1.50 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
1.51 + in ("OK", thy', rew_ord', erls, false) end
1.52 + else
1.53 + let
1.54 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
1.55 + val (rew_ord', erls, _) = rew_info rls'
1.56 + in ("OK", thy', rew_ord', erls, false) end
1.57 + end;
1.58 +
1.59 +fun get_eval scrop p pt =
1.60 + let
1.61 + val (pbl, p', rls') = Ctree.parent_node pt p
1.62 + in
1.63 + if pbl
1.64 + then
1.65 + let
1.66 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
1.67 + val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
1.68 + val opt = assoc (scr_isa_fns, scrop)
1.69 + in
1.70 + case opt of
1.71 + SOME isa_fn => ("OK", thy', isa_fn)
1.72 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
1.73 + end
1.74 + else
1.75 + let
1.76 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
1.77 + val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
1.78 + in
1.79 + case assoc (scr_isa_fns, scrop) of
1.80 + SOME isa_fn => ("OK",thy',isa_fn)
1.81 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
1.82 + end
1.83 + end;
1.84 +
1.85 +(** Solve_Step.check **)
1.86 +
1.87 (*
1.88 check tactics (input by the user, mostly) for applicability
1.89 and determine as much of the result of the tactic as possible initially.
1.90 @@ -46,7 +108,7 @@
1.91 end
1.92 | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
1.93 let
1.94 - val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
1.95 + val (msg, thy', isa_fn) = get_eval op_ p pt;
1.96 val f = Calc.current_formula cs;
1.97 in
1.98 if msg = "OK"
1.99 @@ -76,7 +138,7 @@
1.100 end
1.101 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
1.102 let
1.103 - val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;
1.104 + val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
1.105 val thy = ThyC.get_theory thy';
1.106 val f = Calc.current_formula cs;
1.107 in
1.108 @@ -182,6 +244,9 @@
1.109 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
1.110 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
1.111
1.112 +
1.113 +(** Solve_Step.add **)
1.114 +
1.115 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
1.116 (case topt of
1.117 SOME t =>