prep. separation of check Applicable between specify-phase and solve-phase
1.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Apr 29 09:03:01 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Wed Apr 29 12:30:51 2020 +0200
1.3 @@ -16,7 +16,6 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 -ThmC.string_of_thm_in_thy @{theory} @{thm refl}
1.8 \<close> ML \<open>
1.9 \<close>
1.10 end
1.11 \ No newline at end of file
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 29 09:03:01 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 29 12:30:51 2020 +0200
2.3 @@ -344,9 +344,9 @@
2.4 | ("end-of-calculation", _) => message2xml cI "end-of-calculation"
2.5 | ("failure", _) => sysERROR2xml cI "failure"
2.6 | ("not-applicable", _) => (*the rule comes from anywhere..*)
2.7 - (case Applicable.applicable_in ip pt tac of
2.8 - Applicable.Notappl e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
2.9 - | Applicable.Appl m =>
2.10 + (case ApplicableOLD.applicable_in ip pt tac of
2.11 + Applicable.No e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")
2.12 + | Applicable.Yes m =>
2.13 let
2.14 val ctxt = get_ctxt pt pold
2.15 val (p, c, _, pt) =
3.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-present.sml Wed Apr 29 09:03:01 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-present.sml Wed Apr 29 12:30:51 2020 +0200
3.3 @@ -119,15 +119,15 @@
3.4 let
3.5 val thm_deriv = ThmC.long_id thm''
3.6 in
3.7 - (case Applicable.applicable_in pos pt tac of
3.8 - Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
3.9 + (case ApplicableOLD.applicable_in pos pt tac of
3.10 + Applicable.Yes (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
3.11 ContThm
3.12 {thyID = thy',
3.13 thm = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
3.14 applto = f, applat = TermC.empty, reword = ord',
3.15 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
3.16 result = res, resasms = asm, asmrls = Rule_Set.id erls}
3.17 - | Applicable.Notappl _ =>
3.18 + | Applicable.No _ =>
3.19 let
3.20 val pp = Ctree.par_pblobj pt p
3.21 val thy' = Ctree.get_obj Ctree.g_domID pt pp
3.22 @@ -147,8 +147,8 @@
3.23 | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =
3.24 let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID
3.25 in
3.26 - (case Applicable.applicable_in pos pt tac of
3.27 - Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
3.28 + (case ApplicableOLD.applicable_in pos pt tac of
3.29 + Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
3.30 let
3.31 val thm_deriv = Thm.get_name_hint thm
3.32 val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
3.33 @@ -161,7 +161,7 @@
3.34 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
3.35 result = res, resasms = asm, asmrls = Rule_Set.id erls}
3.36 end
3.37 - | Applicable.Notappl _ =>
3.38 + | Applicable.No _ =>
3.39 let
3.40 val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
3.41 val thm_deriv = Thm.get_name_hint thm
3.42 @@ -182,21 +182,21 @@
3.43 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
3.44 end
3.45 | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =
3.46 - (case Applicable.applicable_in p pt tac of
3.47 - Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
3.48 + (case ApplicableOLD.applicable_in p pt tac of
3.49 + Applicable.Yes (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
3.50 ContRls
3.51 {thyID = thy',
3.52 rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
3.53 applto = f, result = res, asms = asm}
3.54 - | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
3.55 + | _ => error ("context_thy Rewrite_Set: not for Applicable.No"))
3.56 | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
3.57 - (case Applicable.applicable_in p pt tac of
3.58 - Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
3.59 + (case ApplicableOLD.applicable_in p pt tac of
3.60 + Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
3.61 ContRlsInst
3.62 {thyID = thy',
3.63 rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
3.64 bdvs = subst, applto = f, result = res, asms = asm}
3.65 - | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
3.66 + | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.No"))
3.67 | context_thy (_, p) tac =
3.68 error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)
3.69
4.1 --- a/src/Tools/isac/Interpret/Interpret.thy Wed Apr 29 09:03:01 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Wed Apr 29 12:30:51 2020 +0200
4.3 @@ -12,6 +12,7 @@
4.4 ML_file istate.sml
4.5 ML_file "sub-problem.sml"
4.6 ML_file "thy-read.sml"
4.7 + ML_file "solve-step.sml"
4.8 ML_file "error-pattern.sml"
4.9 ML_file derive.sml
4.10 ML_file "li-tool.sml"
5.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 29 09:03:01 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 29 12:30:51 2020 +0200
5.3 @@ -137,9 +137,9 @@
5.4 val p' = Pos.lev_on p;
5.5 val tac = Ctree.get_obj Ctree.g_tac pt p';
5.6 in
5.7 - case Applicable.applicable_in pos pt tac of
5.8 - Applicable.Notappl msg => (msg, Tactic.Tac "")
5.9 - | Applicable.Appl rew =>
5.10 + case ApplicableOLD.applicable_in pos pt tac of
5.11 + Applicable.No msg => (msg, Tactic.Tac "")
5.12 + | Applicable.Yes rew =>
5.13 let
5.14 val res = case rew of
5.15 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
6.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 29 09:03:01 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 29 12:30:51 2020 +0200
6.3 @@ -113,8 +113,8 @@
6.4 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'), ctxt)
6.5 end
6.6 | _ =>
6.7 - (case Applicable.applicable_in p pt m of
6.8 - Applicable.Appl m' =>
6.9 + (case ApplicableOLD.applicable_in p pt m of
6.10 + Applicable.Yes m' =>
6.11 Accept_Tac (m', ist |> set_subst_found (form_arg, Tactic.result m'),
6.12 Tactic.insert_assumptions m' ctxt)
6.13 | _ => Reject_Tac)
6.14 @@ -322,9 +322,9 @@
6.15 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
6.16 AssOnly => Term_Val1 act_arg
6.17 | _(*ORundef*) =>
6.18 - case Applicable.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) of
6.19 - Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
6.20 - | Applicable.Notappl _ => Term_Val1 act_arg)
6.21 + case ApplicableOLD.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") prog_tac) of
6.22 + Applicable.Yes m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
6.23 + | Applicable.No _ => Term_Val1 act_arg)
6.24
6.25 (** scan to a Prog_Tac **)
6.26
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Wed Apr 29 12:30:51 2020 +0200
7.3 @@ -0,0 +1,23 @@
7.4 +(* Title: Specify/solve-step.sml
7.5 + Author: Walther Neuper
7.6 + (c) due to copyright terms
7.7 +
7.8 +Code for the solve-phase in analogy to structure Specify_Step for the specify-phase.
7.9 +*)
7.10 +
7.11 +signature SOLVE_STEP =
7.12 +sig
7.13 + val check_appl: Pos.pos' -> CTbasic.ctree -> Tactic.input -> Applicable.T
7.14 +end
7.15 +
7.16 +(**)
7.17 +structure Solve_Step(** ): SOLVE_STEP( **) =
7.18 +struct
7.19 +(**)
7.20 +
7.21 +(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)
7.22 +(*-----^^^^^- solve ---------------------------------------------------------------------------*)
7.23 +
7.24 +
7.25 +
7.26 +(**)end(**);
8.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Apr 29 09:03:01 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Apr 29 12:30:51 2020 +0200
8.3 @@ -20,6 +20,8 @@
8.4 ML_file "specification-elems.sml"
8.5 ML_file "istate-def.sml"
8.6 ML_file tactic.sml
8.7 + ML_file applicable.sml
8.8 +
8.9 ML_file position.sml
8.10 ML_file "ctree-basic.sml"
8.11 ML_file "ctree-access.sml"
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/MathEngBasic/applicable.sml Wed Apr 29 12:30:51 2020 +0200
9.3 @@ -0,0 +1,26 @@
9.4 +(* Title: MathEngBasic/applicable.sml
9.5 + Author: Walther Neuper
9.6 + (c) due to copyright terms
9.7 +
9.8 +Datatype used for both, the specify-phase by signature Specify_Step
9.9 +and the solve-phase by signature Solve_Step.
9.10 +*)
9.11 +
9.12 +signature APPLICABLE =
9.13 +sig
9.14 + datatype T = Yes of Tactic.T | No of string
9.15 +(*datatype T = Yes of Tactic.T | Notappl of string*)
9.16 +(*datatype T = Appl of Tactic.T | Notappl of string*)
9.17 +(*datatype appl = Appl of Tactic.T | Notappl of string*)
9.18 +end
9.19 +
9.20 +(**)
9.21 +structure Applicable(**): APPLICABLE(**) =
9.22 +struct
9.23 +(**)
9.24 +
9.25 +datatype T =
9.26 + Yes of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
9.27 +| No of string (* tactic is NOT applicable *)
9.28 +
9.29 +(**)end(**);
10.1 --- a/src/Tools/isac/MathEngine/step.sml Wed Apr 29 09:03:01 2020 +0200
10.2 +++ b/src/Tools/isac/MathEngine/step.sml Wed Apr 29 12:30:51 2020 +0200
10.3 @@ -1,25 +1,17 @@
10.4 (* Title: MathEngine/step.sml
10.5 Author: Walther Neuper 2019
10.6 (c) due to copyright terms
10.7 +
10.8 +Unify function of structure Step_Specify and structure Step_Solve
10.9 +as well as of structure Specify_Step and structure Solve_Step.
10.10 *)
10.11
10.12 -(* survey on results of by_tactic, find_next, by_term:
10.13 - * Step_Specify
10.14 - * by_tactic "ok", "ok",
10.15 - * Step_Solve
10.16 - * locate_input_tactic : "ok", "unsafe-ok", "not-applicable", "end-of-calculation"
10.17 - * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found",
10.18 - "error pattern #" ^ errpatID (the latter doesn't fit into the pattern of fixed string)
10.19 - * find_next_formula : "ok", "helpless", "no-fmz-spec"(=helpless), "end-of-calculation"
10.20 - *)
10.21 signature STEP =
10.22 sig
10.23 val do_next: Pos.pos' -> Chead.calcstate -> string * Chead.calcstate'
10.24 val by_tactic: Tactic.input -> Calc.T -> string * Chead.calcstate'
10.25 -(*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate'
10.26 - TODO ------------------------------------"----------> ?????? Calc.T
10.27 - = Step_Specify.by_tactic ? depending on PIDE, see TODO.thy
10.28 -*)
10.29 +(*val by_term = Step_Solve.by_term: Calc.T -> term -> string * Chead.calcstate' *)
10.30 +
10.31 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.32 (*NONE*)
10.33 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.34 @@ -33,6 +25,16 @@
10.35 struct
10.36 (**)
10.37
10.38 +(* survey on results of by_tactic, find_next, by_term:
10.39 + * Step_Specify
10.40 + * by_tactic "ok", "ok",
10.41 + * Step_Solve
10.42 + * locate_input_tactic : "ok", "unsafe-ok", "not-applicable", "end-of-calculation"
10.43 + * locate_input_term : "ok", "syntax error", "same-formula", "no derivation found",
10.44 + "error pattern #" ^ errpatID (the latter doesn't fit into the pattern of fixed string)
10.45 + * find_next_formula : "ok", "helpless", "no-fmz-spec"(=helpless), "end-of-calculation"
10.46 + *)
10.47 +
10.48 (** do a next step **)
10.49
10.50 fun specify_do_next (ptp as (pt, (p, p_))) =
10.51 @@ -86,9 +88,9 @@
10.52 (* LEGACY: report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
10.53 fun by_tactic _ (ptp as (_, ([], Pos.Res))) = ("end-of-calculation", ([], [], ptp))
10.54 | by_tactic m (ptp as (pt, p)) =
10.55 - case Applicable.applicable_in p pt m of
10.56 - Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
10.57 - | Applicable.Appl m =>
10.58 + case ApplicableOLD.applicable_in p pt m of
10.59 + Applicable.No _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
10.60 + | Applicable.Yes m =>
10.61 if Tactic.for_specify' m
10.62 then Step_Specify.by_tactic m ptp
10.63 else Step_Solve.by_tactic m ptp
11.1 --- a/src/Tools/isac/Specify/Specify.thy Wed Apr 29 09:03:01 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/Specify.thy Wed Apr 29 12:30:51 2020 +0200
11.3 @@ -12,6 +12,7 @@
11.4 ML_file calchead.sml
11.5 ML_file "input-calchead.sml"
11.6 ML_file appl.sml
11.7 + ML_file "specify-step.sml"
11.8 ML_file "step-specify.sml"
11.9 ML_file specify.sml
11.10
12.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 29 09:03:01 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 29 12:30:51 2020 +0200
12.3 @@ -4,24 +4,26 @@
12.4 (c) due to copyright terms
12.5 *)
12.6
12.7 -signature APPLICABLE =
12.8 +signature APPLICABLE_OLD =
12.9 sig
12.10 - exception PTREE of string
12.11 - datatype appl = Appl of Tactic.T | Notappl of string
12.12 - val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> appl
12.13 + val applicable_in : Pos.pos' -> Ctree.ctree -> Tactic.input -> Applicable.T
12.14 +
12.15 + val from_pblobj_or_detail_thm: 'a -> Pos.pos -> Ctree.ctree -> string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
12.16 + val from_pblobj_or_detail_calc: string -> Pos.pos -> Ctree.ctree -> string * ThyC.id * (string * Rule_Def.eval_fn)
12.17 + val mk_set: 'a -> Ctree.ctree -> Pos.pos -> term -> term -> term * term list
12.18 + val split_dummy: string -> string * string
12.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.20 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
12.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.22 - val mk_set : 'a -> ctree -> pos -> term -> term -> term * term list
12.23 + val check_elementwise: theory -> Rule_Def.rule_set -> term -> term * term list -> term * term list
12.24 + val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
12.25 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.26 end
12.27
12.28 (**)
12.29 -structure Applicable(**): APPLICABLE(**) =
12.30 +structure ApplicableOLD(**): APPLICABLE_OLD(**) =
12.31 struct
12.32 (**)
12.33 -open Ctree
12.34 -open Pos
12.35
12.36 fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
12.37 (rew_ord', erls, ca)
12.38 @@ -34,30 +36,30 @@
12.39 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
12.40 fun from_pblobj_or_detail_thm _ p pt =
12.41 let
12.42 - val (pbl, p', rls') = parent_node pt p
12.43 - in
12.44 + val (pbl, p', rls') = Ctree.parent_node pt p
12.45 + in
12.46 if pbl
12.47 then
12.48 let
12.49 - val thy' = get_obj g_domID pt p'
12.50 - val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt p')
12.51 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
12.52 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
12.53 in ("OK", thy', rew_ord', erls, false) end
12.54 else
12.55 let
12.56 - val thy' = get_obj g_domID pt (par_pblobj pt p)
12.57 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
12.58 val (rew_ord', erls, _) = rew_info rls'
12.59 in ("OK", thy', rew_ord', erls, false) end
12.60 end;
12.61 (*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
12.62 fun from_pblobj_or_detail_calc scrop p pt =
12.63 let
12.64 - val (pbl, p', rls') = parent_node pt p
12.65 + val (pbl, p', rls') = Ctree.parent_node pt p
12.66 in
12.67 if pbl
12.68 then
12.69 let
12.70 - val thy' = get_obj g_domID pt p'
12.71 - val {calc = scr_isa_fns, ...} = Specify.get_met (get_obj g_metID pt p')
12.72 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
12.73 + val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
12.74 val opt = assoc (scr_isa_fns, scrop)
12.75 in
12.76 case opt of
12.77 @@ -66,7 +68,7 @@
12.78 end
12.79 else
12.80 let
12.81 - val thy' = get_obj g_domID pt (par_pblobj pt p);
12.82 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
12.83 val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
12.84 in
12.85 case assoc (scr_isa_fns, scrop) of
12.86 @@ -80,13 +82,13 @@
12.87 | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =
12.88 (TermC.empty, if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
12.89 then [pred]
12.90 - else Ctree.get_assumptions pt (p, Res))
12.91 + else Ctree.get_assumptions pt (p, Pos.Res))
12.92 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
12.93 let
12.94 val (bdv,_) = HOLogic.dest_eq eq;
12.95 val pred = if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
12.96 then [pred]
12.97 - else Ctree.get_assumptions pt (p, Res)
12.98 + else Ctree.get_assumptions pt (p, Pos.Res)
12.99 in (bdv, pred) end
12.100 | mk_set _ _ _ l _ =
12.101 error ("check_elementwise: no set " ^ UnparseC.term l);
12.102 @@ -117,285 +119,282 @@
12.103 else scan (s' @ [s]) ss;
12.104 in ((scan []) o Symbol.explode) str end;
12.105
12.106 -datatype appl =
12.107 - Appl of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
12.108 -| Notappl of string (* tactic is NOT applicable *)
12.109 -
12.110 (* applicability of a tacic wrt. a calc-state (ctree, pos').
12.111 additionally used by find_next_step.
12.112 tests for applicability are so expensive, that results (rewrites!)
12.113 are kept in the return-value of 'type tac_' *)
12.114 -fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
12.115 +fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Applicable.Yes (Tactic.Init_Proof' (ct', spec))
12.116 | applicable_in (p, p_) pt Tactic.Model_Problem =
12.117 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.118 - then Notappl ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
12.119 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res then
12.120 + Applicable.No ((Tactic.input_to_string Tactic.Model_Problem) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.121 else
12.122 let
12.123 - val pI' = case get_obj I pt p of
12.124 - PblObj {origin = (_, (_, pI', _),_), ...} => pI'
12.125 - | _ => error "applicable_in Init_Proof: uncovered case get_obj"
12.126 + val pI' = case Ctree.get_obj I pt p of
12.127 + Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
12.128 + | _ => error "applicable_in Init_Proof: uncovered case Ctree.get_obj"
12.129 val {ppc, ...} = Specify.get_pbt pI'
12.130 val pbl = Generate.init_pbl ppc
12.131 - in Appl (Tactic.Model_Problem' (pI', pbl, [])) end
12.132 + in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
12.133 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
12.134 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.135 - then Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
12.136 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.137 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.138 else
12.139 let
12.140 - val oris = case get_obj I pt p of
12.141 - PblObj {origin = (oris, _, _), ...} => oris
12.142 - | _ => error "applicable_in Refine_Tacitly: uncovered case get_obj"
12.143 + val oris = case Ctree.get_obj I pt p of
12.144 + Ctree.PblObj {origin = (oris, _, _), ...} => oris
12.145 + | _ => error "applicable_in Refine_Tacitly: uncovered case Ctree.get_obj"
12.146 in
12.147 case Specify.refine_ori oris pI of
12.148 SOME pblID =>
12.149 - Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
12.150 - | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
12.151 + Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [](*filled in specify*)))
12.152 + | NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
12.153 end
12.154 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
12.155 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.156 - then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
12.157 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.158 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not for pos "^(Pos.pos'2str (p, p_)))
12.159 else
12.160 let
12.161 - val (dI, dI', itms) = case get_obj I pt p of
12.162 - PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
12.163 + val (dI, dI', itms) = case Ctree.get_obj I pt p of
12.164 + Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
12.165 => (dI, dI', itms)
12.166 - | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
12.167 + | _ => error "applicable_in Refine_Problem: uncovered case Ctree.get_obj"
12.168 val thy = if dI' = ThyC.id_empty then dI else dI';
12.169 in
12.170 case Specify.refine_pbl (ThyC.get_theory thy) pI itms of
12.171 - NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
12.172 + NONE => Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
12.173 | SOME (rf as (pI', _)) =>
12.174 if pI' = pI
12.175 - then Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
12.176 - else Appl (Tactic.Refine_Problem' rf)
12.177 + then Applicable.No ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
12.178 + else Applicable.Yes (Tactic.Refine_Problem' rf)
12.179 end
12.180 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
12.181 | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
12.182 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.183 - then Notappl ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.184 - else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
12.185 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.186 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.187 + else Applicable.Yes (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
12.188 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
12.189 | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
12.190 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.191 - then Notappl ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.192 - else Appl (Tactic.Del_Given' ct')
12.193 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.194 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Given ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.195 + else Applicable.Yes (Tactic.Del_Given' ct')
12.196 | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
12.197 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.198 - then Notappl ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.199 - else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
12.200 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.201 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.202 + else Applicable.Yes (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
12.203 | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
12.204 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.205 - then Notappl ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.206 - else Appl (Tactic.Del_Find' ct')
12.207 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.208 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Find ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.209 + else Applicable.Yes (Tactic.Del_Find' ct')
12.210 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
12.211 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.212 - then Notappl ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.213 - else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
12.214 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.215 + then Applicable.No ((Tactic.input_to_string (Tactic.Add_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.216 + else Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
12.217 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
12.218 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.219 - then Notappl ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
12.220 - else Appl (Tactic.Del_Relation' ct')
12.221 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.222 + then Applicable.No ((Tactic.input_to_string (Tactic.Del_Relation ct')) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.223 + else Applicable.Yes (Tactic.Del_Relation' ct')
12.224 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
12.225 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.226 - then Notappl ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
12.227 - else Appl (Tactic.Specify_Theory' dI)
12.228 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.229 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Theory dI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.230 + else Applicable.Yes (Tactic.Specify_Theory' dI)
12.231 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
12.232 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.233 - then Notappl ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
12.234 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.235 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Problem pID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.236 else
12.237 let
12.238 - val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
12.239 - PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
12.240 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
12.241 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
12.242 => (oris, dI, pI, dI', pI', itms)
12.243 - | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
12.244 + | _ => error "applicable_in Specify_Problem: uncovered case Ctree.get_obj"
12.245 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
12.246 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
12.247 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
12.248 then (false, (Generate.init_pbl ppc, []))
12.249 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
12.250 in
12.251 - Appl (Tactic.Specify_Problem' (pID, pbl))
12.252 + Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
12.253 end
12.254 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
12.255 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.256 - then Notappl ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
12.257 - else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
12.258 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.259 + then Applicable.No ((Tactic.input_to_string (Tactic.Specify_Method mID)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.260 + else Applicable.Yes (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
12.261 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
12.262 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
12.263 - then Notappl ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
12.264 + if not (Ctree.is_pblobj (Ctree.get_obj I pt p)) orelse p_ = Pos.Res
12.265 + then Applicable.No ((Tactic.input_to_string (Tactic.Apply_Method mI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.266 else
12.267 let
12.268 - val (dI, pI, probl, ctxt) = case get_obj I pt p of
12.269 - PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
12.270 - | _ => error "applicable_in Apply_Method: uncovered case get_obj"
12.271 + val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of
12.272 + Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt)
12.273 + | _ => error "applicable_in Apply_Method: uncovered case Ctree.get_obj"
12.274 val {where_, ...} = Specify.get_pbt pI
12.275 val pres = map (Model.mk_env probl |> subst_atomic) where_
12.276 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*)
12.277 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
12.278 else ctxt
12.279 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
12.280 - and then decide on Notappl/Appl accordingly once more.
12.281 + and then decide on Applicable.No/Applicable.Yes accordingly once more.
12.282 Implement after all tests are running, since this changes
12.283 overall system behavior*)
12.284 in
12.285 - Appl (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
12.286 + Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled in solve*), ctxt))
12.287 end
12.288 +(*-----^^^^^- specify -----vvvvv- solve --------------------------------------------------------*)
12.289 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
12.290 - if member op = [Pbl, Met] p_
12.291 - then Notappl ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
12.292 - else Appl (Tactic.Check_Postcond' (pI, TermC.empty))
12.293 - | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
12.294 - | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve') (* always applicable *)
12.295 + if member op = [Pos.Pbl, Pos.Met] p_
12.296 + then Applicable.No ((Tactic.input_to_string (Tactic.Check_Postcond pI)) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.297 + else Applicable.Yes (Tactic.Check_Postcond' (pI, TermC.empty))
12.298 + | applicable_in _ _ (Tactic.Take str) = Applicable.Yes (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
12.299 + | applicable_in _ _ (Tactic.Free_Solve) = Applicable.Yes (Tactic.Free_Solve') (* always applicable *)
12.300 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
12.301 - if member op = [Pbl, Met] p_
12.302 - then Notappl ((Tactic.input_to_string m)^" not for pos " ^ pos'2str (p, p_))
12.303 + if member op = [Pos.Pbl, Pos.Met] p_
12.304 + then Applicable.No ((Tactic.input_to_string m)^" not for pos " ^ Pos.pos'2str (p, p_))
12.305 else
12.306 let
12.307 - val pp = par_pblobj pt p;
12.308 - val thy' = get_obj g_domID pt pp;
12.309 + val pp = Ctree.par_pblobj pt p;
12.310 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.311 val thy = ThyC.get_theory thy';
12.312 - val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (get_obj g_metID pt pp);
12.313 + val {rew_ord' = ro', erls = erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp);
12.314 val (f, _) = case p_ of (*p 12.4.00 unnecessary*)
12.315 - Frm => (get_obj g_form pt p, p)
12.316 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
12.317 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.318 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
12.319 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
12.320 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.321 in
12.322 let
12.323 val subst = Subst.T_from_input thy subs;
12.324 in
12.325 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
12.326 SOME (f',asm) =>
12.327 - Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
12.328 - | NONE => Notappl ((fst thm'')^" not applicable")
12.329 + Applicable.Yes (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
12.330 + | NONE => Applicable.No ((fst thm'')^" not applicable")
12.331 end
12.332 - handle _ => Notappl ("syntax error in "^(subs2str subs))
12.333 + handle _ => Applicable.No ("syntax error in "^(subs2str subs))
12.334 end
12.335 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
12.336 - if member op = [Pbl, Met] p_
12.337 - then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
12.338 + if member op = [Pos.Pbl, Pos.Met] p_
12.339 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
12.340 else
12.341 let
12.342 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
12.343 val thy = ThyC.get_theory thy';
12.344 val f = case p_ of
12.345 - Frm => get_obj g_form pt p
12.346 - | Res => (fst o (get_obj g_result pt)) p
12.347 - | _ => error ("applicable_in Rewrite: call by " ^ pos'2str (p, p_));
12.348 + Frm => Ctree.get_obj Ctree.g_form pt p
12.349 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.350 + | _ => error ("applicable_in Rewrite: call by " ^ Pos.pos'2str (p, p_));
12.351 in
12.352 if msg = "OK"
12.353 then
12.354 case Rewrite.rewrite_ thy (Rewrite_Ord.assoc_rew_ord ro) rls' false (snd thm'') f of
12.355 - SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
12.356 - | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
12.357 - else Notappl msg
12.358 + SOME (f',asm) => Applicable.Yes (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
12.359 + | NONE => Applicable.No ("'" ^ fst thm'' ^"' not applicable")
12.360 + else Applicable.No msg
12.361 end
12.362 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
12.363 - if member op = [Pbl, Met] p_
12.364 - then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p, p_)))
12.365 + if member op = [Pos.Pbl, Pos.Met] p_
12.366 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p, p_)))
12.367 else
12.368 let
12.369 - val pp = par_pblobj pt p;
12.370 - val thy' = get_obj g_domID pt pp;
12.371 + val pp = Ctree.par_pblobj pt p;
12.372 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.373 val thy = ThyC.get_theory thy';
12.374 - val f = case p_ of Frm => get_obj g_form pt p
12.375 - | Res => (fst o (get_obj g_result pt)) p
12.376 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.377 + val f = case p_ of Frm => Ctree.get_obj Ctree.g_form pt p
12.378 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.379 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.380 val subst = Subst.T_from_input thy subs
12.381 in
12.382 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
12.383 SOME (f', asm)
12.384 - => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
12.385 - | NONE => Notappl (rls ^ " not applicable")
12.386 - handle _ => Notappl ("syntax error in " ^ subs2str subs)
12.387 + => Applicable.Yes (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
12.388 + | NONE => Applicable.No (rls ^ " not applicable")
12.389 + handle _ => Applicable.No ("syntax error in " ^ subs2str subs)
12.390 end
12.391 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
12.392 - if member op = [Pbl, Met] p_
12.393 - then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
12.394 + if member op = [Pos.Pbl, Pos.Met] p_
12.395 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
12.396 else
12.397 let
12.398 - val pp = par_pblobj pt p;
12.399 - val thy' = get_obj g_domID pt pp;
12.400 + val pp = Ctree.par_pblobj pt p;
12.401 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.402 val thy = ThyC.get_theory thy';
12.403 val (f, _) = case p_ of
12.404 - Frm => (get_obj g_form pt p, p)
12.405 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
12.406 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.407 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
12.408 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
12.409 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.410 val subst = Subst.T_from_input thy subs;
12.411 in
12.412 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
12.413 SOME (f',asm)
12.414 - => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
12.415 - | NONE => Notappl (rls ^ " not applicable")
12.416 - handle _ => Notappl ("syntax error in " ^(subs2str subs))
12.417 + => Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
12.418 + | NONE => Applicable.No (rls ^ " not applicable")
12.419 + handle _ => Applicable.No ("syntax error in " ^(subs2str subs))
12.420 end
12.421 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
12.422 - if member op = [Pbl, Met] p_
12.423 - then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
12.424 + if member op = [Pos.Pbl, Pos.Met] p_
12.425 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.426 else
12.427 let
12.428 - val pp = par_pblobj pt p;
12.429 - val thy' = get_obj g_domID pt pp;
12.430 + val pp = Ctree.par_pblobj pt p;
12.431 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.432 val (f, _) = case p_ of
12.433 - Frm => (get_obj g_form pt p, p)
12.434 - | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
12.435 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.436 + Frm => (Ctree.get_obj Ctree.g_form pt p, p)
12.437 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, Pos.lev_on p)
12.438 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.439 in
12.440 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
12.441 SOME (f', asm)
12.442 - => Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
12.443 - | NONE => Notappl (rls ^ " not applicable")
12.444 + => Applicable.Yes (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
12.445 + | NONE => Applicable.No (rls ^ " not applicable")
12.446 end
12.447 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
12.448 - if member op = [Pbl, Met] p_
12.449 - then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
12.450 + if member op = [Pos.Pbl, Pos.Met] p_
12.451 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.452 else
12.453 let
12.454 - val pp = par_pblobj pt p
12.455 - val thy' = get_obj g_domID pt pp
12.456 + val pp = Ctree.par_pblobj pt p
12.457 + val thy' = Ctree.get_obj Ctree.g_domID pt pp
12.458 val f = case p_ of
12.459 - Frm => get_obj g_form pt p
12.460 - | Res => (fst o (get_obj g_result pt)) p
12.461 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.462 + Frm => Ctree.get_obj Ctree.g_form pt p
12.463 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.464 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.465 in
12.466 case Rewrite.rewrite_set_ (ThyC.get_theory thy') false (assoc_rls rls) f of
12.467 - SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
12.468 - | NONE => Notappl (rls^" not applicable")
12.469 + SOME (f',asm) => Applicable.Yes (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
12.470 + | NONE => Applicable.No (rls^" not applicable")
12.471 end
12.472 | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Ruleset)
12.473 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
12.474 - if member op = [Pbl, Met] p_
12.475 - then Notappl ((Tactic.input_to_string m)^" not for pos "^(pos'2str (p,p_)))
12.476 + if member op = [Pos.Pbl, Pos.Met] p_
12.477 + then Applicable.No ((Tactic.input_to_string m)^" not for pos "^(Pos.pos'2str (p,p_)))
12.478 else
12.479 let
12.480 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
12.481 val f = case p_ of
12.482 - Frm => get_obj g_form pt p
12.483 - | Res => (fst o (get_obj g_result pt)) p
12.484 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.485 + Frm => Ctree.get_obj Ctree.g_form pt p
12.486 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.487 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.488 in
12.489 if msg = "OK"
12.490 then
12.491 case Rewrite.calculate_ (ThyC.get_theory thy') isa_fn f of
12.492 SOME (f', (id, thm))
12.493 - => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
12.494 - | NONE => Notappl ("'calculate "^op_^"' not applicable")
12.495 - else Notappl msg
12.496 + => Applicable.Yes (Tactic.Calculate' (thy', op_, f, (f', (id, thm))))
12.497 + | NONE => Applicable.No ("'calculate "^op_^"' not applicable")
12.498 + else Applicable.No msg
12.499 end
12.500 (*Substitute combines two different kind of "substitution":
12.501 (1) subst_atomic: for ?a..?z
12.502 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
12.503 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
12.504 - if member op = [Pbl, Met] p_
12.505 - then Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
12.506 + if member op = [Pos.Pbl, Pos.Met] p_
12.507 + then Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.508 else
12.509 let
12.510 - val pp = par_pblobj pt p
12.511 - val thy = ThyC.get_theory (get_obj g_domID pt pp)
12.512 + val pp = Ctree.par_pblobj pt p
12.513 + val thy = ThyC.get_theory (Ctree.get_obj Ctree.g_domID pt pp)
12.514 val f = case p_ of
12.515 - Frm => get_obj g_form pt p
12.516 - | Res => (fst o (get_obj g_result pt)) p
12.517 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.518 - val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt pp)
12.519 + Frm => Ctree.get_obj Ctree.g_form pt p
12.520 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.521 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.522 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp)
12.523 val subte = Subst.input_to_terms sube
12.524 val subst = Subst.T_from_string_eqs thy sube
12.525 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
12.526 @@ -404,13 +403,13 @@
12.527 then (*1*)
12.528 let val f' = subst_atomic subst f
12.529 in if f = f'
12.530 - then Notappl (Subst.string_eqs_to_string sube ^ " not applicable")
12.531 - else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
12.532 + then Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
12.533 + else Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
12.534 end
12.535 else (*2*)
12.536 case Rewrite.rewrite_terms_ thy ro erls subte f of
12.537 - SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
12.538 - | NONE => Notappl (Subst.string_eqs_to_string sube ^ " not applicable")
12.539 + SOME (f', _) => Applicable.Yes (Tactic.Substitute' (ro, erls, subte, f, f'))
12.540 + | NONE => Applicable.No (Subst.string_eqs_to_string sube ^ " not applicable")
12.541 end
12.542 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
12.543 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
12.544 @@ -420,9 +419,9 @@
12.545 | applicable_in (p, p_) _ (m as Tactic.Subproblem (domID, pblID)) =
12.546 if Pos.on_specification p_
12.547 then
12.548 - Notappl (Tactic.input_to_string m ^ " not for pos " ^ pos'2str (p, p_))
12.549 + Applicable.No (Tactic.input_to_string m ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.550 else (*some fields filled later in LI*)
12.551 - Appl (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
12.552 + Applicable.Yes (Tactic.Subproblem' ((domID, pblID, Method.id_empty), [],
12.553 TermC.empty, [], ContextC.empty, Auto_Prog.subpbl domID pblID))
12.554 | applicable_in _ _ (Tactic.End_Subproblem) =
12.555 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.End_Subproblem)
12.556 @@ -439,16 +438,16 @@
12.557 | applicable_in (p, p_) pt (Tactic.Begin_Trans) =
12.558 let
12.559 val (f, _) = case p_ of (*p 12.4.00 unnecessary, implizit Take in gen*)
12.560 - Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
12.561 - | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
12.562 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.563 - in (Appl (Tactic.Begin_Trans' f))
12.564 + Frm => (Ctree.get_obj Ctree.g_form pt p, (Pos.lev_on o Pos.lev_dn) p)
12.565 + | Pos.Res => ((fst o (Ctree.get_obj Ctree.g_result pt)) p, (Pos.lev_on o Pos.lev_dn o Pos.lev_on) p)
12.566 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.567 + in (Applicable.Yes (Tactic.Begin_Trans' f))
12.568 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ UnparseC.term f ^ "'")
12.569 end
12.570 | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*)
12.571 - if p_ = Res
12.572 - then Appl (Tactic.End_Trans' (get_obj g_result pt p))
12.573 - else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
12.574 + if p_ = Pos.Res
12.575 + then Applicable.Yes (Tactic.End_Trans' (Ctree.get_obj Ctree.g_result pt p))
12.576 + else Applicable.No "'End_Trans' is not applicable at the beginning of a transitive sequence"
12.577 | applicable_in _ _ (Tactic.Begin_Sequ) =
12.578 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Begin_Sequ))
12.579 | applicable_in _ _ (Tactic.End_Sequ) =
12.580 @@ -458,71 +457,72 @@
12.581 | applicable_in _ _ (Tactic.End_Intersect) =
12.582 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.End_Intersect))
12.583 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
12.584 - if member op = [Pbl, Met] p_
12.585 - then Notappl ((Tactic.input_to_string m) ^ " not for pos " ^ pos'2str (p, p_))
12.586 + if member op = [Pos.Pbl, Pos.Met] p_
12.587 + then Applicable.No ((Tactic.input_to_string m) ^ " not for pos " ^ Pos.pos'2str (p, p_))
12.588 else
12.589 let
12.590 - val pp = par_pblobj pt p;
12.591 - val thy' = get_obj g_domID pt pp;
12.592 + val pp = Ctree.par_pblobj pt p;
12.593 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.594 val thy = ThyC.get_theory thy'
12.595 - val metID = (get_obj g_metID pt pp)
12.596 + val metID = (Ctree.get_obj Ctree.g_metID pt pp)
12.597 val {crls, ...} = Specify.get_met metID
12.598 val (f, asm) = case p_ of
12.599 - Frm => (get_obj g_form pt p , [])
12.600 - | Res => get_obj g_result pt p
12.601 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.602 + Frm => (Ctree.get_obj Ctree.g_form pt p , [])
12.603 + | Pos.Res => Ctree.get_obj Ctree.g_result pt p
12.604 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.605 val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
12.606 in
12.607 - Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
12.608 + Applicable.Yes (Tactic.Check_elementwise' (f, pred, (f, asm)))
12.609 end
12.610 | applicable_in (p, p_) pt Tactic.Or_to_List =
12.611 - if member op = [Pbl, Met] p_
12.612 - then Notappl ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
12.613 + if member op = [Pos.Pbl, Pos.Met] p_
12.614 + then Applicable.No ((Tactic.input_to_string Tactic.Or_to_List)^" not for pos "^(Pos.pos'2str (p,p_)))
12.615 else
12.616 let
12.617 val f = case p_ of
12.618 - Frm => get_obj g_form pt p
12.619 - | Res => (fst o (get_obj g_result pt)) p
12.620 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.621 + Frm => Ctree.get_obj Ctree.g_form pt p
12.622 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.623 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.624 in (let val ls = Prog_Expr.or2list f
12.625 - in Appl (Tactic.Or_to_List' (f, ls)) end)
12.626 - handle _ => Notappl ("'Or_to_List' not applicable to " ^ UnparseC.term f)
12.627 + in Applicable.Yes (Tactic.Or_to_List' (f, ls)) end)
12.628 + handle _ => Applicable.No ("'Or_to_List' not applicable to " ^ UnparseC.term f)
12.629 end
12.630 | applicable_in _ _ Tactic.Collect_Trues =
12.631 error ("applicable_in: not impl. for " ^ Tactic.input_to_string Tactic.Collect_Trues)
12.632 - | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"
12.633 + | applicable_in _ _ Tactic.Empty_Tac = Applicable.No "Empty_Tac is not applicable"
12.634 | applicable_in (p, p_) pt (Tactic.Tac id) =
12.635 let
12.636 - val pp = par_pblobj pt p;
12.637 - val thy' = get_obj g_domID pt pp;
12.638 + val pp = Ctree.par_pblobj pt p;
12.639 + val thy' = Ctree.get_obj Ctree.g_domID pt pp;
12.640 val thy = ThyC.get_theory thy';
12.641 val f = case p_ of
12.642 - Frm => get_obj g_form pt p
12.643 - | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
12.644 - | Res => (fst o (get_obj g_result pt)) p
12.645 - | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
12.646 + Frm => Ctree.get_obj Ctree.g_form pt p
12.647 + | Pos.Pbl => error "applicable_in (p,Pos.Pbl) pt (Tac id): not at Pos.Pbl"
12.648 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
12.649 + | _ => error ("applicable_in: call by " ^ Pos.pos'2str (p, p_));
12.650 in case id of
12.651 "subproblem_equation_dummy" =>
12.652 if TermC.is_expliceq f
12.653 - then Appl (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
12.654 - else Notappl "applicable only to equations made explicit"
12.655 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "subproblem_equation_dummy (" ^ UnparseC.term f ^ ")"))
12.656 + else Applicable.No "applicable only to equations made explicit"
12.657 | "solve_equation_dummy" =>
12.658 let val (id', f') = split_dummy (UnparseC.term f);
12.659 in
12.660 if id' <> "subproblem_equation_dummy"
12.661 - then Notappl "no subproblem"
12.662 + then Applicable.No "no subproblem"
12.663 else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
12.664 - then Appl (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
12.665 + then Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
12.666 else error ("applicable_in: f= " ^ f')
12.667 end
12.668 - | _ => Appl (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
12.669 + | _ => Applicable.Yes (Tactic.Tac_ (thy, UnparseC.term f, id, UnparseC.term f))
12.670 end
12.671 - | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''
12.672 + | applicable_in _ _ Tactic.End_Proof' = Applicable.Yes Tactic.End_Proof''
12.673 | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.input_to_string m);
12.674 +(*-----^^^^^- solve ---------------------------------------------------------------------------*)
12.675
12.676 fun tac2tac_ pt p m =
12.677 case applicable_in p pt m of
12.678 - Appl m' => m'
12.679 - | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
12.680 + Applicable.Yes m' => m'
12.681 + | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);
12.682
12.683 -end;
12.684 +(**)end(**);
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed Apr 29 12:30:51 2020 +0200
13.3 @@ -0,0 +1,20 @@
13.4 +(* Title: Specify/specify-step.sml
13.5 + Author: Walther Neuper
13.6 + (c) due to copyright terms
13.7 +
13.8 +Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.
13.9 +*)
13.10 +
13.11 +signature SPECIFY_STEP =
13.12 +sig
13.13 +
13.14 +end
13.15 +
13.16 +(**)
13.17 +structure Specify_Step(**): SPECIFY_STEP(**) =
13.18 +struct
13.19 +(**)
13.20 +
13.21 +
13.22 +
13.23 +(**)end(**);
14.1 --- a/src/Tools/isac/TODO.thy Wed Apr 29 09:03:01 2020 +0200
14.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 29 12:30:51 2020 +0200
14.3 @@ -292,7 +292,7 @@
14.4 \item Step*: Step_Specify | Step_Solve | Step
14.5 \begin{itemize}
14.6 \item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve
14.7 - Specify_Step.check | Specify_Step.add <-- Applicable.applicable_in
14.8 + Specify_Step.check | Specify_Step.add <-- ApplicableOLD.applicable_in
14.9 Solve_Step.check | Solve_Step.add <-- Generate.generate1
14.10 \item xxx
14.11 \end{itemize}
15.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Wed Apr 29 09:03:01 2020 +0200
15.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Wed Apr 29 12:30:51 2020 +0200
15.3 @@ -219,7 +219,7 @@
15.4 val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)
15.5 Step.by_tactic tac (pt, p) (*of*);
15.6 "~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));
15.7 - val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
15.8 + val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt m (*of*);
15.9 (*if*) Tactic.for_specify' m (*else*);
15.10
15.11 val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =
16.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Wed Apr 29 09:03:01 2020 +0200
16.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Wed Apr 29 12:30:51 2020 +0200
16.3 @@ -134,7 +134,7 @@
16.4 is_rewtac tac = true;
16.5 "~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
16.6 ((pt, pos), tac);
16.7 - val Appl (Rewrite' (thy', ord', erls, _, (thmID, thm), f, (res,asm))) = applicable_in pos pt tac
16.8 + val Applicable.Yes (Rewrite' (thy', ord', erls, _, (thmID, thm), f, (res,asm))) = applicable_in pos pt tac
16.9 val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
16.10 val thm_deriv = Thm.get_name_hint thm;
16.11
16.12 @@ -156,7 +156,7 @@
16.13 is_rewtac tac = true;
16.14 "~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
16.15 ((pt, pos), tac);
16.16 -val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
16.17 +val Applicable.Yes (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
16.18 applicable_in pos pt tac
16.19 val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
16.20 val thm_deriv = Thm.get_name_hint thm;
17.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 29 09:03:01 2020 +0200
17.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 29 12:30:51 2020 +0200
17.3 @@ -190,7 +190,7 @@
17.4 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
17.5
17.6 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
17.7 - val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
17.8 + val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt tac (*of*);
17.9 (*if*) Tactic.for_specify' m; (*false*)
17.10
17.11 Step_Solve.by_tactic m (pt, p);
18.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Apr 29 09:03:01 2020 +0200
18.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Apr 29 12:30:51 2020 +0200
18.3 @@ -1215,7 +1215,7 @@
18.4 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
18.5 if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
18.6 else error "inputFillFormula changed 10";
18.7 - val Appl rew = applicable_in pos pt tac;
18.8 + val Applicable.Yes rew = applicable_in pos pt tac;
18.9 val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
18.10
18.11 "~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
19.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 29 09:03:01 2020 +0200
19.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 29 12:30:51 2020 +0200
19.3 @@ -59,7 +59,7 @@
19.4
19.5 (*Step.by_tactic tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
19.6 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
19.7 - val Appl m = applicable_in p pt tac ; (*Appl*)
19.8 + val Applicable.Yes m = applicable_in p pt tac ; (*Applicable.Yes*)
19.9 (*if*) Tactic.for_specify' m; (*false*)
19.10 (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
19.11
19.12 @@ -104,7 +104,7 @@
19.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.14 "~~~~~ fun me, args:"; val tac = nxt;
19.15 "~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
19.16 -val Appl m = applicable_in p pt tac;
19.17 +val Applicable.Yes m = applicable_in p pt tac;
19.18 (*if*) Tactic.for_specify' m; (*false*)
19.19 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
19.20 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
20.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 29 09:03:01 2020 +0200
20.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 29 12:30:51 2020 +0200
20.3 @@ -37,7 +37,7 @@
20.4
20.5 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
20.6 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
20.7 -val Appl m = applicable_in p pt tac;
20.8 +val Applicable.Yes m = applicable_in p pt tac;
20.9 (*if*) Tactic.for_specify' m; (*false*)
20.10 "~~~~~ fun loc_solve_ , args:"; val (m, (pt,pos)) = (m, ptp);
20.11
20.12 @@ -111,7 +111,7 @@
20.13 (** )val (***)xxxx(***) ( *("ok", (_, _, (pt, p))) =( **) (*case*)
20.14 Step.by_tactic tac (pt,p) (*of*);
20.15 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
20.16 - val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
20.17 + val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt tac (*of*);
20.18 (*if*) Tactic.for_specify' m; (*false*)
20.19
20.20 (** )val (***)xxxxx_x(***) ( *(msg, cs') =( **)
20.21 @@ -267,7 +267,7 @@
20.22 (*//----------------- exception PTREE "get_obj f EmptyPtree" raised --------------------------\\*)
20.23 (** )val ("ok", (_, _, ptp as (pt, p))) =( **) Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
20.24 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (hd (specific_from_prog pt p), (pt, p));
20.25 - val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
20.26 + val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt tac (*of*);
20.27 (*if*) Tactic.for_specify' m; (*false*)
20.28
20.29 Step_Solve.by_tactic m (pt, p);
20.30 @@ -321,8 +321,8 @@
20.31 val (Program.Tac stac, a') = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
20.32 val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
20.33 val ORundef = (*case*) or (*of*);
20.34 - val Notappl "norm_equation not applicable" =
20.35 - (*case*) Applicable.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (*of*);
20.36 + val Applicable.No "norm_equation not applicable" =
20.37 + (*case*) ApplicableOLD.applicable_in p pt (LItool.tac_from_prog pt (ThyC.get_theory "Isac_Knowledge") stac) (*of*);
20.38
20.39 (Term_Val1 act_arg) (* return value *);
20.40
21.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 29 09:03:01 2020 +0200
21.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 29 12:30:51 2020 +0200
21.3 @@ -143,7 +143,7 @@
21.4 AbleitungBiegelinie
21.5 *)
21.6 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
21.7 -val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
21.8 +val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt m (*of*);
21.9 (*if*) Library.member op = Solve.specsteps mI = false; (*else*)
21.10
21.11 loc_solve_ (mI,m) ptp;
21.12 @@ -224,7 +224,7 @@
21.13 ("ok", (_, _, ptp)) => ptp
21.14 ;
21.15 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
21.16 -val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
21.17 +val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt m (*of*);
21.18 (*if*) Library.member op = Solve.specsteps mI = true; (*then*)
21.19
21.20 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
22.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Wed Apr 29 09:03:01 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Wed Apr 29 12:30:51 2020 +0200
22.3 @@ -27,7 +27,7 @@
22.4 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
22.5 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
22.6 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---";
22.7 -(* "declare [[ML_print_depth = 999]]" *before* opening structure Applicable
22.8 +(* "declare [[ML_print_depth = 999]]" *before* opening structure ApplicableOLD
22.9 slows down KEStore_Elems.get_rlss in collect_part in Build_Thydata.thy
22.10 such, that it hangs (probably due to some full buffer)
22.11 test below compiled with
23.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 29 09:03:01 2020 +0200
23.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 29 12:30:51 2020 +0200
23.3 @@ -352,7 +352,7 @@
23.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
23.5 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
23.6 "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
23.7 -val Appl m = applicable_in p pt tac;
23.8 +val Applicable.Yes m = applicable_in p pt tac;
23.9 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
23.10 UnparseC.term trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
23.11 str = "Assumptions";
24.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Apr 29 09:03:01 2020 +0200
24.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 29 12:30:51 2020 +0200
24.3 @@ -155,7 +155,7 @@
24.4 WN120317.TODO dropped rateq: ctxt should contain "x ~= 0 here, but it does not, see above.
24.5 *)
24.6
24.7 -val Appl (Check_elementwise' (curr_form, pred, (res, asms))) = applicable_in p''''' pt''''' m''''';
24.8 +val Applicable.Yes (Check_elementwise' (curr_form, pred, (res, asms))) = applicable_in p''''' pt''''' m''''';
24.9 UnparseC.term curr_form = "[x = 1 / 5]";
24.10 pred = "Assumptions";
24.11 res = str2term "[]::bool list";
25.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 29 09:03:01 2020 +0200
25.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Wed Apr 29 12:30:51 2020 +0200
25.3 @@ -525,9 +525,9 @@
25.4 = (thy, 1, bool, []:(term * term) list, rls, term);
25.5
25.6 (*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
25.7 - datatype switch = Appl | Noap;
25.8 + datatype switch = Applicable.Yes | Noap;
25.9 fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
25.10 - | rew_once ruls asm ct Appl [] =
25.11 + | rew_once ruls asm ct Applicable.Yes [] =
25.12 (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
25.13 | Rule_Set.Sequence _ => (ct, asm)
25.14 | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))
25.15 @@ -540,7 +540,7 @@
25.16 NONE => rew_once ruls asm ct apno thms
25.17 | SOME (ct', asm') =>
25.18 (trace1 i (" rewrites to: " ^ UnparseC.term_in_thy thy ct');
25.19 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
25.20 + rew_once ruls (union (op =) asm asm') ct' Applicable.Yes (rul :: thms)))
25.21 (* once again try the same rule, e.g. associativity against "()"*)
25.22 | Rule.Eval (cc as (op_, _)) =>
25.23 let val _= trace1 i (" try calc: " ^ op_ ^ "'")
25.24 @@ -554,7 +554,7 @@
25.25 val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
25.26 ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_thy thy ct ^ " = NONE")
25.27 val _ = trace1 i (" calc. to: " ^ UnparseC.term_in_thy thy ((fst o the) pairopt))
25.28 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
25.29 + in rew_once ruls asm ((fst o the) pairopt) Applicable.Yes (rul :: thms) end
25.30 end
25.31 | Rule.Cal1 (cc as (op_, _)) =>
25.32 let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
25.33 @@ -572,7 +572,7 @@
25.34 end
25.35 | Rule.Rls_ rls' =>
25.36 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
25.37 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
25.38 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Applicable.Yes thms
25.39 | NONE => rew_once ruls asm ct apno thms)
25.40 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.Rule.to_string r ^ "\"");
25.41 val ruls = (#rules o Rule.Rule_Set.rep) rls;
26.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 29 09:03:01 2020 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 29 12:30:51 2020 +0200
26.3 @@ -46,7 +46,7 @@
26.4 "~~~~~ fun me, args:"; val tac = nxt;
26.5 val ("ok", (_, _, (pt''''',p'''''))) = Step.by_tactic tac (pt,p);
26.6 "~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
26.7 -val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)
26.8 +val Applicable.Yes m = applicable_in p pt tac; (*m = Apply_Method'..*)
26.9 (*if*) Tactic.for_specify' m; (*false*)
26.10 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
26.11 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
26.12 @@ -157,7 +157,7 @@
26.13 (*+*)| _ => error "tac_from_prog changed"
26.14
26.15 "~~~~~ continue last scan_dn";
26.16 -val Applicable.Appl m' = Applicable.applicable_in p pt m;
26.17 +val Applicable.Yes m' = ApplicableOLD.applicable_in p pt m;
26.18 "~~~~~ fun result, args:"; val (m) = (m');
26.19 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
26.20 val fT = type_of f;
27.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 29 09:03:01 2020 +0200
27.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 29 12:30:51 2020 +0200
27.3 @@ -36,7 +36,7 @@
27.4 val ("ok", (_, _, ptp''''')) = (*case*)
27.5 Step.by_tactic tac (pt, p) (*of*);
27.6 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
27.7 -val Applicable.Appl m = (*case*) Applicable.applicable_in p pt tac (*of*);
27.8 +val Applicable.Yes m = (*case*) ApplicableOLD.applicable_in p pt tac (*of*);
27.9 (*if*) Tactic.for_specify' m; (*false*)
27.10
27.11 Step_Solve.by_tactic m ptp;
28.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 29 09:03:01 2020 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Apr 29 12:30:51 2020 +0200
28.3 @@ -31,7 +31,7 @@
28.4 Step.by_tactic tac (pt, p) (*of*);
28.5 get_ctxt pt'''' p'''' |> ContextC.is_empty; (*should NOT be true after this step*)
28.6 "~~~~~ fun by_tactic , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
28.7 - val Appl m = applicable_in p pt tac;
28.8 + val Applicable.Yes m = applicable_in p pt tac;
28.9 (*if*) Tactic.for_specify' m; (*false*)
28.10
28.11 (*val (msg, cs') =*)
29.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 29 09:03:01 2020 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Apr 29 12:30:51 2020 +0200
29.3 @@ -40,7 +40,7 @@
29.4 val ("ok", (_, _, (pt'''', p''''))) = (*case*)
29.5 Step.by_tactic tac (pt, p) (*of*);
29.6 "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
29.7 - val Appl m = (*case*) applicable_in p pt tac (*of*);
29.8 + val Applicable.Yes m = (*case*) applicable_in p pt tac (*of*);
29.9 (*if*) Tactic.for_specify' m; (*false*)
29.10
29.11 Step_Solve.by_tactic m ptp;
30.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 29 09:03:01 2020 +0200
30.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 29 12:30:51 2020 +0200
30.3 @@ -553,7 +553,7 @@
30.4 (*me------------
30.5 val (mI,m) = nxt; val pos' as (p,p_) = p;
30.6
30.7 - val Appl m = applicable_in (p,p_) pt m;
30.8 + val Applicable.Yes m = applicable_in (p,p_) pt m;
30.9 (*solve*)
30.10 val pp = par_pblobj pt p;
30.11 val metID = get_obj g_metID pt pp;
31.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Apr 29 09:03:01 2020 +0200
31.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Apr 29 12:30:51 2020 +0200
31.3 @@ -277,7 +277,7 @@
31.4 " --------------- 1. ---------------------------------------------";
31.5 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test",""))(str2term ct,[])Complete;
31.6 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv"
31.7 -val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
31.8 +val Applicable.Yes m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
31.9 *)
31.10
31.11
32.1 --- a/test/Tools/isac/Test_Isac.thy Wed Apr 29 09:03:01 2020 +0200
32.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 29 12:30:51 2020 +0200
32.3 @@ -112,7 +112,7 @@
32.4 open Input_Descript;
32.5 open Specify; show_ptyps;
32.6 open SpecifyNEW;
32.7 - open Applicable; mk_set;
32.8 + open ApplicableOLD; mk_set;
32.9 open Step_Specify;
32.10 open Step_Solve;
32.11 open Step;
33.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 29 09:03:01 2020 +0200
33.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 29 12:30:51 2020 +0200
33.3 @@ -112,7 +112,7 @@
33.4 open Input_Descript;
33.5 open Specify; show_ptyps;
33.6 open SpecifyNEW;
33.7 - open Applicable; mk_set;
33.8 + open ApplicableOLD; mk_set;
33.9 open Step_Specify;
33.10 open Step_Solve;
33.11 open Step;
34.1 --- a/test/Tools/isac/Test_Some.thy Wed Apr 29 09:03:01 2020 +0200
34.2 +++ b/test/Tools/isac/Test_Some.thy Wed Apr 29 12:30:51 2020 +0200
34.3 @@ -32,7 +32,7 @@
34.4 open Input_Descript;
34.5 open Specify; show_ptyps;
34.6 open SpecifyNEW;
34.7 - open Applicable; mk_set;
34.8 + open ApplicableOLD; mk_set;
34.9 open Step_Specify;
34.10 open Step_Solve;
34.11 open Step;
35.1 --- a/test/Tools/isac/Test_Some_meld.thy Wed Apr 29 09:03:01 2020 +0200
35.2 +++ b/test/Tools/isac/Test_Some_meld.thy Wed Apr 29 12:30:51 2020 +0200
35.3 @@ -23,7 +23,7 @@
35.4 open Auto_Prog; rule2stac;
35.5 open Input_Descript;
35.6 open Specify; show_ptyps;
35.7 - open Applicable; mk_set;
35.8 + open ApplicableOLD; mk_set;
35.9 open Solve; (* NONE *)
35.10 open Selem; e_fmz;
35.11 open Stool; (* NONE *)