592 | NONE => Notappl (sube2str sube^" not applicable") |
592 | NONE => Notappl (sube2str sube^" not applicable") |
593 end |
593 end |
594 ------------------*) |
594 ------------------*) |
595 |
595 |
596 | applicable_in p pt (Apply_Assumption cts') = |
596 | applicable_in p pt (Apply_Assumption cts') = |
597 (error ("applicable_in: not impl. for "^ |
597 (error ("applicable_in: not impl. for " ^ (tac2str (Apply_Assumption cts')))) |
598 (tac2str (Apply_Assumption cts')))) |
|
599 |
598 |
600 (*'logical' applicability wrt. script in locate: Inconsistent?*) |
599 (*'logical' applicability wrt. script in locate: Inconsistent?*) |
601 | applicable_in (p,p_) pt (m as Take ct') = |
600 | applicable_in (p,p_) pt (m as Take ct') = |
602 if member op = [Pbl,Met] p_ |
601 if member op = [Pbl,Met] p_ |
603 then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
602 then Notappl (tac2str m ^ " not for pos " ^ pos'2str (p,p_)) |
604 else |
603 else |
605 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
604 let val thy' = get_obj g_domID pt (par_pblobj pt p); |
606 in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of |
605 in (case parseNEW (assoc_thy thy' |> thy2ctxt) ct' of |
607 SOME ct => Appl (Take' ct) |
606 SOME ct => Appl (Take' ct) |
608 | NONE => Notappl ("syntax error in "^ct')) |
607 | NONE => Notappl ("syntax error in " ^ ct')) |
609 end |
608 end |
610 |
609 |
611 | applicable_in p pt (Take_Inst ct') = |
610 | applicable_in p pt (Take_Inst ct') = |
612 error ("applicable_in: not impl. for "^ |
611 error ("applicable_in: not impl. for " ^ tac2str (Take_Inst ct')) |
613 (tac2str (Take_Inst ct'))) |
|
614 |
|
615 | applicable_in p pt (Group (con, ints)) = |
612 | applicable_in p pt (Group (con, ints)) = |
616 error ("applicable_in: not impl. for "^ |
613 error ("applicable_in: not impl. for " ^ tac2str (Group (con, ints))) |
617 (tac2str (Group (con, ints)))) |
|
618 |
614 |
619 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = |
615 | applicable_in (p,p_) pt (m as Subproblem (domID, pblID)) = |
620 if member op = [Pbl,Met] p_ |
616 if member op = [Pbl,Met] p_ |
621 then (*maybe Apply_Method has already been done*) |
617 then (*maybe Apply_Method has already been done FIXME.WN150511: declare_constraints*) |
622 case get_obj g_env pt p of |
618 case get_obj g_env pt p of |
623 SOME is => Appl (Subproblem' ((domID, pblID, e_metID), [], |
619 SOME is => |
624 e_term, [], e_ctxt, subpbl domID pblID)) |
620 Appl (Subproblem' ((domID, pblID, e_metID), [], |
625 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
621 e_term, [], e_ctxt(*FIXME.WN150511*), subpbl domID pblID)) |
|
622 | NONE => Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_))) |
626 else (*somewhere later in the script*) |
623 else (*somewhere later in the script*) |
627 Appl (Subproblem' ((domID, pblID, e_metID), [], |
624 Appl (Subproblem' ((domID, pblID, e_metID), [], |
628 e_term, [], e_ctxt, subpbl domID pblID)) |
625 e_term, [], e_ctxt, subpbl domID pblID)) |
629 |
626 |
630 | applicable_in p pt (End_Subproblem) = |
627 | applicable_in p pt (End_Subproblem) = |
631 error ("applicable_in: not impl. for "^ |
628 error ("applicable_in: not impl. for " ^ tac2str End_Subproblem) |
632 (tac2str (End_Subproblem))) |
|
633 |
|
634 | applicable_in p pt (CAScmd ct') = |
629 | applicable_in p pt (CAScmd ct') = |
635 error ("applicable_in: not impl. for "^ |
630 error ("applicable_in: not impl. for " ^ tac2str (CAScmd ct')) |
636 (tac2str (CAScmd ct'))) |
|
637 |
|
638 | applicable_in p pt (Split_And) = |
631 | applicable_in p pt (Split_And) = |
639 error ("applicable_in: not impl. for "^ |
632 error ("applicable_in: not impl. for " ^ tac2str Split_And) |
640 (tac2str (Split_And))) |
|
641 | applicable_in p pt (Conclude_And) = |
633 | applicable_in p pt (Conclude_And) = |
642 error ("applicable_in: not impl. for "^ |
634 error ("applicable_in: not impl. for " ^ tac2str Conclude_And) |
643 (tac2str (Conclude_And))) |
|
644 | applicable_in p pt (Split_Or) = |
635 | applicable_in p pt (Split_Or) = |
645 error ("applicable_in: not impl. for "^ |
636 error ("applicable_in: not impl. for " ^ tac2str Split_Or) |
646 (tac2str (Split_Or))) |
|
647 | applicable_in p pt (Conclude_Or) = |
637 | applicable_in p pt (Conclude_Or) = |
648 error ("applicable_in: not impl. for "^ |
638 error ("applicable_in: not impl. for " ^ tac2str Conclude_Or) |
649 (tac2str (Conclude_Or))) |
|
650 |
639 |
651 | applicable_in (p,p_) pt (Begin_Trans) = |
640 | applicable_in (p,p_) pt (Begin_Trans) = |
652 let |
641 let |
653 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
642 val (f,p) = case p_ of (*p 12.4.00 unnecessary*) |
654 (*_____ implizit Take in gen*) |
643 (*_____ implizit Take in gen*) |