1.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 15:44:59 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 16:51:36 2020 +0200
1.3 @@ -8,12 +8,6 @@
1.4 signature REWRITE_TOOLS =
1.5 sig
1.6
1.7 -(*/------- to error-fill-pattern from Rtools -------\*)
1.8 - val thy_containing_thm : string -> string * string
1.9 - val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
1.10 - val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
1.11 -(*\------- to error-fill-pattern from Rtools -------/*)
1.12 -
1.13 datatype contthy
1.14 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
1.15 | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
1.16 @@ -41,53 +35,12 @@
1.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.18 (* NONE *)
1.19 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.20 -
1.21 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
1.22 - val sym_trm : term -> term
1.23 end
1.24 (**)
1.25 structure Rtools(**): REWRITE_TOOLS(**) =
1.26 struct
1.27 (**)
1.28
1.29 -(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
1.30 -fun sym_trm trm =
1.31 - let
1.32 - val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) trm
1.33 - val trm' = case TermC.strip_imp_prems' trm of
1.34 - NONE => TermC.mk_equality (rhs, lhs)
1.35 - | SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))
1.36 - in trm' end
1.37 -
1.38 -fun thy_containing_thm thmDeriv =
1.39 - let
1.40 - val isabthys' = map Context.theory_name (Celem.isabthys ());
1.41 - in
1.42 - if member op= isabthys' (ThyC.cut_id thmDeriv)
1.43 - then ("Isabelle", ThyC.cut_id thmDeriv)
1.44 - else ("IsacKnowledge", ThyC.cut_id thmDeriv)
1.45 - end
1.46 -
1.47 -(* which theory in ancestors of thy' contains a ruleset *)
1.48 -fun thy_containing_rls thy' rls' =
1.49 - let
1.50 - val thy = ThyC.get_theory thy'
1.51 - in
1.52 - case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
1.53 - SOME (thy'', _) => (Celem.partID' thy'', thy'')
1.54 - | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
1.55 - end
1.56 -
1.57 -(* this function cannot work as long as the datastructure does not contain thy' *)
1.58 -fun thy_containing_cal thy' sop =
1.59 - let
1.60 - val thy = ThyC.get_theory thy'
1.61 - in
1.62 - case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
1.63 - SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")
1.64 - | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
1.65 - end
1.66 -
1.67 (* packing return-values to matchTheory, contextToThy for xml-generation *)
1.68 datatype contthy = (*also an item from Know_Store on Browser ...........#*)
1.69 EContThy (* not from Know_Store ..............................*)
1.70 @@ -166,7 +119,7 @@
1.71 Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
1.72 ContThm
1.73 {thyID = thy',
1.74 - thm = Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.75 + thm = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.76 applto = f, applat = TermC.empty, reword = ord',
1.77 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
1.78 result = res, resasms = asm, asmrls = Rule_Set.id erls}
1.79 @@ -182,7 +135,7 @@
1.80 ContNOrew
1.81 {thyID = thy',
1.82 thm_rls =
1.83 - Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.84 + Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.85 applto = f}
1.86 end
1.87 | _ => error "context_thy..Rewrite: uncovered case 2")
1.88 @@ -199,7 +152,7 @@
1.89 ContThmInst
1.90 {thyID = thy',
1.91 thm =
1.92 - Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.93 + Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.94 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
1.95 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
1.96 result = res, resasms = asm, asmrls = Rule_Set.id erls}
1.97 @@ -219,7 +172,7 @@
1.98 in
1.99 ContNOrewInst
1.100 {thyID = thy',
1.101 - thm_rls = Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.102 + thm_rls = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
1.103 bdvs = subst, thminst = thminst, applto = f}
1.104 end
1.105 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
1.106 @@ -229,7 +182,7 @@
1.107 Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
1.108 ContRls
1.109 {thyID = thy',
1.110 - rls = Thy_Html.rls2guh (thy_containing_rls thy' rls') rls',
1.111 + rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
1.112 applto = f, result = res, asms = asm}
1.113 | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
1.114 | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
1.115 @@ -237,7 +190,7 @@
1.116 Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
1.117 ContRlsInst
1.118 {thyID = thy',
1.119 - rls = Thy_Html.rls2guh (thy_containing_rls thy' rls') rls',
1.120 + rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
1.121 bdvs = subst, applto = f, result = res, asms = asm}
1.122 | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
1.123 | context_thy (_, p) tac =