1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Dec 16 14:03:16 2019 +0100
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Dec 16 15:38:13 2019 +0100
1.3 @@ -342,8 +342,8 @@
1.4 | ("failure", _) => sysERROR2xml cI "failure"
1.5 | ("not-applicable", _) => (*the rule comes from anywhere..*)
1.6 (case Applicable.applicable_in ip pt tac of
1.7 - Chead.Notappl e => message2xml cI ("'" ^ Tactic.tac2str tac ^ "' not-applicable")
1.8 - | Chead.Appl m =>
1.9 + Applicable.Notappl e => message2xml cI ("'" ^ Tactic.tac2str tac ^ "' not-applicable")
1.10 + | Applicable.Appl m =>
1.11 let
1.12 val ctxt = get_ctxt pt pold
1.13 val (p, c, _, pt) =
2.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Dec 16 14:03:16 2019 +0100
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Dec 16 15:38:13 2019 +0100
2.3 @@ -455,8 +455,8 @@
2.4 val tac = Ctree.get_obj Ctree.g_tac pt p';
2.5 in
2.6 case Applicable.applicable_in pos pt tac of
2.7 - Chead.Notappl msg => (msg, Tactic.Tac "")
2.8 - | Chead.Appl rew =>
2.9 + Applicable.Notappl msg => (msg, Tactic.Tac "")
2.10 + | Applicable.Appl rew =>
2.11 let
2.12 val res = case rew of
2.13 Tactic.Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) => res
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 16 14:03:16 2019 +0100
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Dec 16 15:38:13 2019 +0100
3.3 @@ -120,8 +120,8 @@
3.4 AssOnly => Term_Val1 act_arg
3.5 | _(*ORundef*) =>
3.6 case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
3.7 - Chead.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
3.8 - | Chead.Notappl _ => Term_Val1 act_arg)
3.9 + Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
3.10 + | Applicable.Notappl _ => Term_Val1 act_arg)
3.11
3.12 (** scan to a Prog_Tac **)
3.13
3.14 @@ -378,7 +378,7 @@
3.15 Accept_Tac2 (m', ist |> set_subst_reset (a', Tactic.result m'), ctxt)
3.16 | _ =>
3.17 (case Applicable.applicable_in p pt m of
3.18 - Chead.Appl m' => Accept_Tac2 (m',
3.19 + Applicable.Appl m' => Accept_Tac2 (m',
3.20 ist |> set_subst_reset (a', Tactic.result m'), Tactic.insert_assumptions m' ctxt)
3.21 | _ => Reject_Tac2)
3.22 end
4.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Dec 16 14:03:16 2019 +0100
4.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Dec 16 15:38:13 2019 +0100
4.3 @@ -348,14 +348,14 @@
4.4 let val thm_deriv = deriv_of_thm'' thm''
4.5 in
4.6 (case Applicable.applicable_in pos pt tac of
4.7 - Chead.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
4.8 + Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
4.9 ContThm
4.10 {thyID = Rule.theory'2thyID thy',
4.11 thm = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
4.12 applto = f, applat = Rule.e_term, reword = ord',
4.13 asms = [](*asms ~~ asms'*), lhs = (Rule.e_term, Rule.e_term)(*(lhs, lhs')*), rhs = (Rule.e_term, Rule.e_term)(*(rhs, rhs')*),
4.14 result = res, resasms = asm, asmrls = Rule.id_rls erls}
4.15 - | Chead.Notappl _ =>
4.16 + | Applicable.Notappl _ =>
4.17 let
4.18 val pp = Ctree.par_pblobj pt p
4.19 val thy' = Ctree.get_obj Ctree.g_domID pt pp
4.20 @@ -376,7 +376,7 @@
4.21 let val thm = Global_Theory.get_thm (Rule.Isac ()) thmID
4.22 in
4.23 (case Applicable.applicable_in pos pt tac of
4.24 - Chead.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
4.25 + Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
4.26 let
4.27 val thm_deriv = Thm.get_name_hint thm
4.28 val thminst = TermC.inst_bdv subst ((Calc.norm o #prop o Thm.rep_thm) thm)
4.29 @@ -389,7 +389,7 @@
4.30 asms = [](*asms ~~ asms'*), lhs = (Rule.e_term, Rule.e_term)(*(lhs, lhs')*), rhs = (Rule.e_term, Rule.e_term)(*(rhs, rhs')*),
4.31 result = res, resasms = asm, asmrls = Rule.id_rls erls}
4.32 end
4.33 - | Chead.Notappl _ =>
4.34 + | Applicable.Notappl _ =>
4.35 let
4.36 val thm = Global_Theory.get_thm (Rule.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
4.37 val thm_deriv = Thm.get_name_hint thm
4.38 @@ -411,20 +411,20 @@
4.39 end
4.40 | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =
4.41 (case Applicable.applicable_in p pt tac of
4.42 - Chead.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
4.43 + Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
4.44 ContRls
4.45 {thyID = Rule.theory'2thyID thy',
4.46 rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
4.47 applto = f, result = res, asms = asm}
4.48 - | _ => error ("context_thy Rewrite_Set: not for Chead.Notappl"))
4.49 + | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
4.50 | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
4.51 (case Applicable.applicable_in p pt tac of
4.52 - Chead.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
4.53 + Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
4.54 ContRlsInst
4.55 {thyID = Rule.theory'2thyID thy',
4.56 rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
4.57 bdvs = subst, applto = f, result = res, asms = asm}
4.58 - | _ => error ("context_thy Rewrite_Set_Inst: not for Chead.Notappl"))
4.59 + | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
4.60 | context_thy (_, p) tac =
4.61 error ("context_thy: not for tac " ^ Tactic.tac2str tac ^ " at " ^ Pos.pos'2str p)
4.62
5.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon Dec 16 14:03:16 2019 +0100
5.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Dec 16 15:38:13 2019 +0100
5.3 @@ -114,6 +114,7 @@
5.4 val result : T -> term
5.5 val creates_assms: T -> term list
5.6 val insert_assumptions: T -> Proof.context -> Proof.context
5.7 +
5.8 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.9 (* NONE *)
5.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.11 @@ -503,4 +504,7 @@
5.12
5.13 fun insert_assumptions tac ctxt = ContextC.insert_assumptions (creates_assms tac) ctxt
5.14
5.15 +(*---------------------------------------- NEW ---------------------------------------------*)
5.16 +
5.17 +
5.18 (**)end(**)
6.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 16 14:03:16 2019 +0100
6.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon Dec 16 15:38:13 2019 +0100
6.3 @@ -88,8 +88,8 @@
6.4 val (mI, m) = Solve.mk_tac'_ tac;
6.5 in
6.6 case Applicable.applicable_in p pt m of
6.7 - Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
6.8 - | Chead.Appl m =>
6.9 + Applicable.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
6.10 + | Applicable.Appl m =>
6.11 let
6.12 val x = if member op = Solve.specsteps mI
6.13 then loc_specify_ m ptp else loc_solve_ (mI, m) ptp
7.1 --- a/src/Tools/isac/MathEngine/solve.sml Mon Dec 16 14:03:16 2019 +0100
7.2 +++ b/src/Tools/isac/MathEngine/solve.sml Mon Dec 16 15:38:13 2019 +0100
7.3 @@ -379,8 +379,8 @@
7.4
7.5 fun get_form (mI, m) (p,p_) pt =
7.6 case Applicable.applicable_in (p, p_) pt m of
7.7 - Chead.Notappl e => Generate.Error' e
7.8 - | Chead.Appl m =>
7.9 + Applicable.Notappl e => Generate.Error' e
7.10 + | Applicable.Appl m =>
7.11 if member op = specsteps mI
7.12 then
7.13 let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt
8.1 --- a/src/Tools/isac/Specify/appl.sml Mon Dec 16 14:03:16 2019 +0100
8.2 +++ b/src/Tools/isac/Specify/appl.sml Mon Dec 16 15:38:13 2019 +0100
8.3 @@ -7,7 +7,8 @@
8.4 signature APPLICABLE =
8.5 sig
8.6 exception PTREE of string
8.7 - val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> Chead.appl
8.8 + datatype appl = Appl of Tactic.T | Notappl of string
8.9 + val applicable_in : Ctree.pos' -> Ctree.ctree -> Tactic.input -> appl
8.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.11 val tac2tac_ : Ctree.ctree -> Ctree.pos' -> Tactic.input -> Tactic.T
8.12 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.13 @@ -116,14 +117,18 @@
8.14 else scan (s' @ [s]) ss;
8.15 in ((scan []) o Symbol.explode) str end;
8.16
8.17 +datatype appl =
8.18 + Appl of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
8.19 +| Notappl of string (* tactic is NOT applicable *)
8.20 +
8.21 (* applicability of a tacic wrt. a calc-state (ctree, pos').
8.22 additionally used by determine_next_tactic.
8.23 tests for applicability are so expensive, that results (rewrites!)
8.24 are kept in the return-value of 'type tac_' *)
8.25 -fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Chead.Appl (Tactic.Init_Proof' (ct', spec))
8.26 +fun applicable_in _ _ (Tactic.Init_Proof (ct', spec)) = Appl (Tactic.Init_Proof' (ct', spec))
8.27 | applicable_in (p, p_) pt Tactic.Model_Problem =
8.28 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.29 - then Chead.Notappl ((Tactic.tac2str Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
8.30 + then Notappl ((Tactic.tac2str Tactic.Model_Problem) ^ " not for pos " ^ (pos'2str (p, p_)))
8.31 else
8.32 let
8.33 val pI' = case get_obj I pt p of
8.34 @@ -131,10 +136,10 @@
8.35 | _ => error "applicable_in Init_Proof: uncovered case get_obj"
8.36 val {ppc, ...} = Specify.get_pbt pI'
8.37 val pbl = Generate.init_pbl ppc
8.38 - in Chead.Appl (Tactic.Model_Problem' (pI', pbl, [])) end
8.39 + in Appl (Tactic.Model_Problem' (pI', pbl, [])) end
8.40 | applicable_in (p, p_) pt (Tactic.Refine_Tacitly pI) =
8.41 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.42 - then Chead.Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
8.43 + then Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p, p_)))
8.44 else
8.45 let
8.46 val oris = case get_obj I pt p of
8.47 @@ -143,12 +148,12 @@
8.48 in
8.49 case Specify.refine_ori oris pI of
8.50 SOME pblID =>
8.51 - Chead.Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))
8.52 - | NONE => Chead.Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not applicable")
8.53 + Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))
8.54 + | NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Tacitly pI)) ^ " not applicable")
8.55 end
8.56 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
8.57 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.58 - then Chead.Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
8.59 + then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not for pos "^(pos'2str (p, p_)))
8.60 else
8.61 let
8.62 val (dI, dI', itms) = case get_obj I pt p of
8.63 @@ -158,45 +163,45 @@
8.64 val thy = if dI' = Rule.e_domID then dI else dI';
8.65 in
8.66 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
8.67 - NONE => Chead.Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
8.68 + NONE => Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
8.69 | SOME (rf as (pI', _)) =>
8.70 if pI' = pI
8.71 - then Chead.Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
8.72 - else Chead.Appl (Tactic.Refine_Problem' rf)
8.73 + then Notappl ((Tactic.tac2str (Tactic.Refine_Problem pI)) ^ " not applicable")
8.74 + else Appl (Tactic.Refine_Problem' rf)
8.75 end
8.76 (*the specify-tacs have cterm' instead term: parse+error here!!!: see appl_add*)
8.77 | applicable_in (p, p_) pt (Tactic.Add_Given ct') =
8.78 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.79 - then Chead.Notappl ((Tactic.tac2str (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.80 - else Chead.Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
8.81 + then Notappl ((Tactic.tac2str (Tactic.Add_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.82 + else Appl (Tactic.Add_Given' (ct', [(*filled in specify_additem*)]))
8.83 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
8.84 | applicable_in (p, p_) pt (Tactic.Del_Given ct') =
8.85 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.86 - then Chead.Notappl ((Tactic.tac2str (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.87 - else Chead.Appl (Tactic.Del_Given' ct')
8.88 + then Notappl ((Tactic.tac2str (Tactic.Del_Given ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.89 + else Appl (Tactic.Del_Given' ct')
8.90 | applicable_in (p, p_) pt (Tactic.Add_Find ct') =
8.91 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.92 - then Chead.Notappl ((Tactic.tac2str (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.93 - else Chead.Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
8.94 + then Notappl ((Tactic.tac2str (Tactic.Add_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.95 + else Appl (Tactic.Add_Find' (ct', [(*filled in specify_additem*)]))
8.96 | applicable_in (p, p_) pt (Tactic.Del_Find ct') =
8.97 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.98 - then Chead.Notappl ((Tactic.tac2str (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.99 - else Chead.Appl (Tactic.Del_Find' ct')
8.100 + then Notappl ((Tactic.tac2str (Tactic.Del_Find ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.101 + else Appl (Tactic.Del_Find' ct')
8.102 | applicable_in (p, p_) pt (Tactic.Add_Relation ct') =
8.103 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.104 - then Chead.Notappl ((Tactic.tac2str (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.105 - else Chead.Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
8.106 + then Notappl ((Tactic.tac2str (Tactic.Add_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.107 + else Appl (Tactic.Add_Relation' (ct', [(*filled in specify_additem*)]))
8.108 | applicable_in (p, p_) pt (Tactic.Del_Relation ct') =
8.109 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.110 - then Chead.Notappl ((Tactic.tac2str (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.111 - else Chead.Appl (Tactic.Del_Relation' ct')
8.112 + then Notappl ((Tactic.tac2str (Tactic.Del_Relation ct')) ^ " not for pos " ^ pos'2str (p, p_))
8.113 + else Appl (Tactic.Del_Relation' ct')
8.114 | applicable_in (p, p_) pt (Tactic.Specify_Theory dI) =
8.115 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.116 - then Chead.Notappl ((Tactic.tac2str (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
8.117 - else Chead.Appl (Tactic.Specify_Theory' dI)
8.118 + then Notappl ((Tactic.tac2str (Tactic.Specify_Theory dI)) ^ " not for pos " ^ pos'2str (p, p_))
8.119 + else Appl (Tactic.Specify_Theory' dI)
8.120 | applicable_in (p, p_) pt (Tactic.Specify_Problem pID) =
8.121 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.122 - then Chead.Notappl ((Tactic.tac2str (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
8.123 + then Notappl ((Tactic.tac2str (Tactic.Specify_Problem pID)) ^ " not for pos " ^ pos'2str (p, p_))
8.124 else
8.125 let
8.126 val (oris, dI, pI, dI', pI', itms) = case get_obj I pt p of
8.127 @@ -209,15 +214,15 @@
8.128 then (false, (Generate.init_pbl ppc, []))
8.129 else Specify.match_itms_oris thy itms (ppc, where_, prls) oris;
8.130 in
8.131 - Chead.Appl (Tactic.Specify_Problem' (pID, pbl))
8.132 + Appl (Tactic.Specify_Problem' (pID, pbl))
8.133 end
8.134 | applicable_in (p, p_) pt (Tactic.Specify_Method mID) =
8.135 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.136 - then Chead.Notappl ((Tactic.tac2str (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
8.137 - else Chead.Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
8.138 + then Notappl ((Tactic.tac2str (Tactic.Specify_Method mID)) ^ " not for pos " ^ pos'2str (p, p_))
8.139 + else Appl (Tactic.Specify_Method' (mID, [(*filled in specify*)], [(*filled in specify*)]))
8.140 | applicable_in (p, p_) pt (Tactic.Apply_Method mI) =
8.141 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
8.142 - then Chead.Notappl ((Tactic.tac2str (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
8.143 + then Notappl ((Tactic.tac2str (Tactic.Apply_Method mI)) ^ " not for pos " ^ pos'2str (p, p_))
8.144 else
8.145 let
8.146 val (dI, pI, probl, ctxt) = case get_obj I pt p of
8.147 @@ -229,21 +234,21 @@
8.148 then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres
8.149 else ctxt
8.150 (*TODO.WN110416 here do evalprecond according to fun check_preconds'
8.151 - and then decide on Chead.Notappl/Appl accordingly once more.
8.152 + and then decide on Notappl/Appl accordingly once more.
8.153 Implement after all tests are running, since this changes
8.154 overall system behavior*)
8.155 in
8.156 - Chead.Appl (Tactic.Apply_Method' (mI, NONE, Istate.e_istate (*filled in solve*), ctxt))
8.157 + Appl (Tactic.Apply_Method' (mI, NONE, Istate.e_istate (*filled in solve*), ctxt))
8.158 end
8.159 | applicable_in (p, p_) _ (Tactic.Check_Postcond pI) =
8.160 if member op = [Pbl, Met] p_
8.161 - then Chead.Notappl ((Tactic.tac2str (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
8.162 - else Chead.Appl (Tactic.Check_Postcond' (pI, (Rule.e_term, [(*fun solve assigns returnvalue of scr*)])))
8.163 - | applicable_in _ _ (Tactic.Take str) = Chead.Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
8.164 - | applicable_in _ _ (Tactic.Free_Solve) = Chead.Appl (Tactic.Free_Solve') (* always applicable *)
8.165 + then Notappl ((Tactic.tac2str (Tactic.Check_Postcond pI)) ^ " not for pos " ^ pos'2str (p, p_))
8.166 + else Appl (Tactic.Check_Postcond' (pI, (Rule.e_term, [(*fun solve assigns returnvalue of scr*)])))
8.167 + | applicable_in _ _ (Tactic.Take str) = Appl (Tactic.Take' (TermC.str2term str)) (* always applicable ?*)
8.168 + | applicable_in _ _ (Tactic.Free_Solve) = Appl (Tactic.Free_Solve') (* always applicable *)
8.169 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Inst (subs, thm'')) =
8.170 if member op = [Pbl, Met] p_
8.171 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos " ^ pos'2str (p, p_))
8.172 + then Notappl ((Tactic.tac2str m)^" not for pos " ^ pos'2str (p, p_))
8.173 else
8.174 let
8.175 val pp = par_pblobj pt p;
8.176 @@ -260,14 +265,14 @@
8.177 in
8.178 case Rewrite.rewrite_inst_ thy (Rule.assoc_rew_ord ro') erls false subst (snd thm'') f of
8.179 SOME (f',asm) =>
8.180 - Chead.Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
8.181 - | NONE => Chead.Notappl ((fst thm'')^" not applicable")
8.182 + Appl (Tactic.Rewrite_Inst' (thy', ro', erls, false, subst, thm'', f, (f', asm)))
8.183 + | NONE => Notappl ((fst thm'')^" not applicable")
8.184 end
8.185 - handle _ => Chead.Notappl ("syntax error in "^(subs2str subs))
8.186 + handle _ => Notappl ("syntax error in "^(subs2str subs))
8.187 end
8.188 | applicable_in (p, p_) pt (m as Tactic.Rewrite thm'') =
8.189 if member op = [Pbl, Met] p_
8.190 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
8.191 + then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
8.192 else
8.193 let
8.194 val (msg, thy', ro, rls', _)= from_pblobj_or_detail_thm thm'' p pt;
8.195 @@ -280,13 +285,13 @@
8.196 if msg = "OK"
8.197 then
8.198 case Rewrite.rewrite_ thy (Rule.assoc_rew_ord ro) rls' false (snd thm'') f of
8.199 - SOME (f',asm) => Chead.Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
8.200 - | NONE => Chead.Notappl ("'" ^ fst thm'' ^"' not applicable")
8.201 - else Chead.Notappl msg
8.202 + SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro, rls', false, thm'', f, (f', asm)))
8.203 + | NONE => Notappl ("'" ^ fst thm'' ^"' not applicable")
8.204 + else Notappl msg
8.205 end
8.206 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Asm thm'') =
8.207 if member op = [Pbl, Met] p_
8.208 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.209 + then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.210 else
8.211 let
8.212 val pp = par_pblobj pt p;
8.213 @@ -299,11 +304,11 @@
8.214 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
8.215 in
8.216 case Rewrite.rewrite_ thy (Rule.assoc_rew_ord ro') erls false (snd thm'') f of
8.217 - SOME (f',asm) => Chead.Appl (Tactic.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
8.218 - | NONE => Chead.Notappl ("'" ^ fst thm'' ^ "' not applicable") end
8.219 + SOME (f',asm) => Appl (Tactic.Rewrite' (thy', ro', erls, false, thm'', f, (f', asm)))
8.220 + | NONE => Notappl ("'" ^ fst thm'' ^ "' not applicable") end
8.221 | applicable_in (p, p_) pt (m as Tactic.Detail_Set_Inst (subs, rls)) =
8.222 if member op = [Pbl, Met] p_
8.223 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
8.224 + then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p, p_)))
8.225 else
8.226 let
8.227 val pp = par_pblobj pt p;
8.228 @@ -316,13 +321,13 @@
8.229 in
8.230 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
8.231 SOME (f', asm)
8.232 - => Chead.Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
8.233 - | NONE => Chead.Notappl (rls ^ " not applicable")
8.234 - handle _ => Chead.Notappl ("syntax error in " ^ subs2str subs)
8.235 + => Appl (Tactic.Detail_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
8.236 + | NONE => Notappl (rls ^ " not applicable")
8.237 + handle _ => Notappl ("syntax error in " ^ subs2str subs)
8.238 end
8.239 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set_Inst (subs, rls)) =
8.240 if member op = [Pbl, Met] p_
8.241 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.242 + then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.243 else
8.244 let
8.245 val pp = par_pblobj pt p;
8.246 @@ -336,13 +341,13 @@
8.247 in
8.248 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
8.249 SOME (f',asm)
8.250 - => Chead.Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
8.251 - | NONE => Chead.Notappl (rls ^ " not applicable")
8.252 - handle _ => Chead.Notappl ("syntax error in " ^(subs2str subs))
8.253 + => Appl (Tactic.Rewrite_Set_Inst' (thy', false, subst, assoc_rls rls, f, (f', asm)))
8.254 + | NONE => Notappl (rls ^ " not applicable")
8.255 + handle _ => Notappl ("syntax error in " ^(subs2str subs))
8.256 end
8.257 | applicable_in (p, p_) pt (m as Tactic.Rewrite_Set rls) =
8.258 if member op = [Pbl, Met] p_
8.259 - then Chead.Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.260 + then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.261 else
8.262 let
8.263 val pp = par_pblobj pt p;
8.264 @@ -354,12 +359,12 @@
8.265 in
8.266 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
8.267 SOME (f', asm)
8.268 - => Chead.Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
8.269 - | NONE => Chead.Notappl (rls ^ " not applicable")
8.270 + => Appl (Tactic.Rewrite_Set' (thy', false, assoc_rls rls, f, (f', asm)))
8.271 + | NONE => Notappl (rls ^ " not applicable")
8.272 end
8.273 | applicable_in (p, p_) pt (m as Tactic.Detail_Set rls) =
8.274 if member op = [Pbl, Met] p_
8.275 - then Chead.Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.276 + then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.277 else
8.278 let
8.279 val pp = par_pblobj pt p
8.280 @@ -370,13 +375,13 @@
8.281 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
8.282 in
8.283 case Rewrite.rewrite_set_ (Celem.assoc_thy thy') false (assoc_rls rls) f of
8.284 - SOME (f',asm) => Chead.Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
8.285 - | NONE => Chead.Notappl (rls^" not applicable")
8.286 + SOME (f',asm) => Appl (Tactic.Detail_Set' (thy', false, assoc_rls rls, f, (f', asm)))
8.287 + | NONE => Notappl (rls^" not applicable")
8.288 end
8.289 | applicable_in _ _ Tactic.End_Ruleset = error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Ruleset)
8.290 | applicable_in (p, p_) pt (m as Tactic.Calculate op_) =
8.291 if member op = [Pbl, Met] p_
8.292 - then Chead.Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.293 + then Notappl ((Tactic.tac2str m)^" not for pos "^(pos'2str (p,p_)))
8.294 else
8.295 let
8.296 val (msg,thy',isa_fn) = from_pblobj_or_detail_calc op_ p pt;
8.297 @@ -389,16 +394,16 @@
8.298 then
8.299 case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
8.300 SOME (f', (id, thm))
8.301 - => Chead.Appl (Tactic.Calculate' (thy', op_, f, (f', (id, Rule.string_of_thmI thm))))
8.302 - | NONE => Chead.Notappl ("'calculate "^op_^"' not applicable")
8.303 - else Chead.Notappl msg
8.304 + => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, Rule.string_of_thmI thm))))
8.305 + | NONE => Notappl ("'calculate "^op_^"' not applicable")
8.306 + else Notappl msg
8.307 end
8.308 (*Substitute combines two different kind of "substitution":
8.309 (1) subst_atomic: for ?a..?z
8.310 (2) Pattern.match: for solving equational systems (which raises exn for ?a..?z)*)
8.311 | applicable_in (p, p_) pt (m as Tactic.Substitute sube) =
8.312 if member op = [Pbl, Met] p_
8.313 - then Chead.Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.314 + then Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p, p_))
8.315 else
8.316 let
8.317 val pp = par_pblobj pt p
8.318 @@ -416,13 +421,13 @@
8.319 then (*1*)
8.320 let val f' = subst_atomic subst f
8.321 in if f = f'
8.322 - then Chead.Notappl (Selem.sube2str sube^" not applicable")
8.323 - else Chead.Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
8.324 + then Notappl (Selem.sube2str sube^" not applicable")
8.325 + else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
8.326 end
8.327 else (*2*)
8.328 case Rewrite.rewrite_terms_ thy ro erls subte f of
8.329 - SOME (f', _) => Chead.Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
8.330 - | NONE => Chead.Notappl (Selem.sube2str sube ^ " not applicable")
8.331 + SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
8.332 + | NONE => Notappl (Selem.sube2str sube ^ " not applicable")
8.333 end
8.334 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
8.335 error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Apply_Assumption cts'))
8.336 @@ -434,11 +439,11 @@
8.337 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*)
8.338 case get_obj g_env pt p of
8.339 SOME _ =>
8.340 - Chead.Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
8.341 + Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
8.342 Rule.e_term, [], ContextC.e_ctxt(*init. in Subproblem'*), Auto_Prog.subpbl domID pblID))
8.343 - | NONE => Chead.Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p,p_))
8.344 + | NONE => Notappl (Tactic.tac2str m ^ " not for pos " ^ pos'2str (p,p_))
8.345 else (*somewhere later in the script*)
8.346 - Chead.Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
8.347 + Appl (Tactic.Subproblem' ((domID, pblID, Celem.e_metID), [],
8.348 Rule.e_term, [], ContextC.e_ctxt, Auto_Prog.subpbl domID pblID))
8.349 | applicable_in _ _ (Tactic.End_Subproblem) =
8.350 error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.End_Subproblem)
8.351 @@ -458,13 +463,13 @@
8.352 Frm => (get_obj g_form pt p, (lev_on o lev_dn) p)
8.353 | Res => ((fst o (get_obj g_result pt)) p, (lev_on o lev_dn o lev_on) p)
8.354 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
8.355 - in (Chead.Appl (Tactic.Begin_Trans' f))
8.356 + in (Appl (Tactic.Begin_Trans' f))
8.357 handle _ => error ("applicable_in: Begin_Trans finds syntaxerror in '" ^ Rule.term2str f ^ "'")
8.358 end
8.359 | applicable_in (p, p_) pt (Tactic.End_Trans) = (*TODO: check parent branches*)
8.360 if p_ = Res
8.361 - then Chead.Appl (Tactic.End_Trans' (get_obj g_result pt p))
8.362 - else Chead.Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
8.363 + then Appl (Tactic.End_Trans' (get_obj g_result pt p))
8.364 + else Notappl "'End_Trans' is not applicable at the beginning of a transitive sequence"
8.365 | applicable_in _ _ (Tactic.Begin_Sequ) =
8.366 error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.Begin_Sequ))
8.367 | applicable_in _ _ (Tactic.End_Sequ) =
8.368 @@ -475,7 +480,7 @@
8.369 error ("applicable_in: not impl. for " ^ Tactic.tac2str (Tactic.End_Intersect))
8.370 | applicable_in (p, p_) pt (m as Tactic.Check_elementwise pred) =
8.371 if member op = [Pbl, Met] p_
8.372 - then Chead.Notappl ((Tactic.tac2str m) ^ " not for pos " ^ pos'2str (p, p_))
8.373 + then Notappl ((Tactic.tac2str m) ^ " not for pos " ^ pos'2str (p, p_))
8.374 else
8.375 let
8.376 val pp = par_pblobj pt p;
8.377 @@ -490,16 +495,16 @@
8.378 val vp = (Rule.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
8.379 in case f of
8.380 Const ("List.list.Cons", _) $ _ $ _ =>
8.381 - Chead.Appl (Tactic.Check_elementwise' (f, pred, check_elementwise thy crls f vp))
8.382 + Appl (Tactic.Check_elementwise' (f, pred, check_elementwise thy crls f vp))
8.383 | Const ("ListC.UniversalList", _) =>
8.384 - Chead.Appl (Tactic.Check_elementwise' (f, pred, (f,asm)))
8.385 + Appl (Tactic.Check_elementwise' (f, pred, (f,asm)))
8.386 | Const ("List.list.Nil", _) =>
8.387 - Chead.Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
8.388 - | _ => Chead.Notappl ("Check_elementwise not appl.: " ^ Rule.term2str f ^ " should be constants")
8.389 + Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
8.390 + | _ => Notappl ("Check_elementwise not appl.: " ^ Rule.term2str f ^ " should be constants")
8.391 end
8.392 | applicable_in (p, p_) pt Tactic.Or_to_List =
8.393 if member op = [Pbl, Met] p_
8.394 - then Chead.Notappl ((Tactic.tac2str Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
8.395 + then Notappl ((Tactic.tac2str Tactic.Or_to_List)^" not for pos "^(pos'2str (p,p_)))
8.396 else
8.397 let
8.398 val f = case p_ of
8.399 @@ -507,12 +512,12 @@
8.400 | Res => (fst o (get_obj g_result pt)) p
8.401 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
8.402 in (let val ls = Prog_Expr.or2list f
8.403 - in Chead.Appl (Tactic.Or_to_List' (f, ls)) end)
8.404 - handle _ => Chead.Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)
8.405 + in Appl (Tactic.Or_to_List' (f, ls)) end)
8.406 + handle _ => Notappl ("'Or_to_List' not applicable to " ^ Rule.term2str f)
8.407 end
8.408 | applicable_in _ _ Tactic.Collect_Trues =
8.409 error ("applicable_in: not impl. for " ^ Tactic.tac2str Tactic.Collect_Trues)
8.410 - | applicable_in _ _ Tactic.Empty_Tac = Chead.Notappl "Empty_Tac is not applicable"
8.411 + | applicable_in _ _ Tactic.Empty_Tac = Notappl "Empty_Tac is not applicable"
8.412 | applicable_in (p, p_) pt (Tactic.Tac id) =
8.413 let
8.414 val pp = par_pblobj pt p;
8.415 @@ -526,25 +531,25 @@
8.416 in case id of
8.417 "subproblem_equation_dummy" =>
8.418 if TermC.is_expliceq f
8.419 - then Chead.Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "subproblem_equation_dummy (" ^ Rule.term2str f ^ ")"))
8.420 - else Chead.Notappl "applicable only to equations made explicit"
8.421 + then Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "subproblem_equation_dummy (" ^ Rule.term2str f ^ ")"))
8.422 + else Notappl "applicable only to equations made explicit"
8.423 | "solve_equation_dummy" =>
8.424 let val (id', f') = split_dummy (Rule.term2str f);
8.425 in
8.426 if id' <> "subproblem_equation_dummy"
8.427 - then Chead.Notappl "no subproblem"
8.428 + then Notappl "no subproblem"
8.429 else if (Rule.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
8.430 - then Chead.Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "[" ^ f' ^ "]"))
8.431 + then Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "[" ^ f' ^ "]"))
8.432 else error ("applicable_in: f= " ^ f')
8.433 end
8.434 - | _ => Chead.Appl (Tactic.Tac_ (thy, Rule.term2str f, id, Rule.term2str f))
8.435 + | _ => Appl (Tactic.Tac_ (thy, Rule.term2str f, id, Rule.term2str f))
8.436 end
8.437 - | applicable_in _ _ Tactic.End_Proof' = Chead.Appl Tactic.End_Proof''
8.438 + | applicable_in _ _ Tactic.End_Proof' = Appl Tactic.End_Proof''
8.439 | applicable_in _ _ m = error ("applicable_in called for " ^ Tactic.tac2str m);
8.440
8.441 fun tac2tac_ pt p m =
8.442 case applicable_in p pt m of
8.443 - Chead.Appl m' => m'
8.444 - | Chead.Notappl _ => error ("tac2mstp': fails with" ^ Tactic.tac2str m);
8.445 + Appl m' => m'
8.446 + | Notappl _ => error ("tac2mstp': fails with" ^ Tactic.tac2str m);
8.447
8.448 end;
9.1 --- a/src/Tools/isac/Specify/calchead.sml Mon Dec 16 14:03:16 2019 +0100
9.2 +++ b/src/Tools/isac/Specify/calchead.sml Mon Dec 16 15:38:13 2019 +0100
9.3 @@ -68,7 +68,7 @@
9.4 sig
9.5 type calcstate
9.6 type calcstate'
9.7 - datatype appl = Appl of Tactic.T | Notappl of string
9.8 +
9.9 val nxt_specify_init_calc : Selem.fmz -> calcstate
9.10 val specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
9.11 Ctree.pos' * (Ctree.pos' * Istate.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
9.12 @@ -230,10 +230,6 @@
9.13 fun seek_ppc _ [] = NONE
9.14 | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
9.15
9.16 -datatype appl =
9.17 - Appl of Tactic.T (* tactic is applicable at a certain position in the Ctree *)
9.18 -| Notappl of string (* tactic is NOT applicable *)
9.19 -
9.20 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} =
9.21 gis @ whs @ fis @ wis @ res
9.22