1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 28 15:44:59 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 28 16:51:36 2020 +0200
1.3 @@ -19,12 +19,6 @@
1.4 type pbt_ = string * (term * term)
1.5 val update_hrls: Thy_Html.thydata -> Error_Pattern_Def.id list -> Thy_Html.thydata
1.6
1.7 -(*/------- to ? from Celem -------\*)
1.8 - val knowthys: unit -> theory list
1.9 - val isabthys: unit -> theory list
1.10 - val partID': ThyC.id -> string
1.11 -(*\------- to ? from Celem -------/*)
1.12 -
1.13 end
1.14
1.15 (**)
1.16 @@ -65,57 +59,5 @@
1.17 end
1.18 | update_hrls _ _ = raise ERROR "update_hrls: wrong arguments";
1.19
1.20 -
1.21 -(*/------- to ? from Celem -------\*)
1.22 -(* group the theories defined in Isac, compare Build_Thydata:
1.23 - section "Get and group the theories defined in Isac" *)
1.24 -fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
1.25 - let
1.26 - val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata")
1.27 - in
1.28 - drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
1.29 - end
1.30 -fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*)
1.31 - let
1.32 - fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
1.33 - let
1.34 - val allthys = filter_out (member Context.eq_thy
1.35 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
1.36 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
1.37 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
1.38 - in
1.39 - take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.40 - allthys)
1.41 - end
1.42 - val isacthys' = isacthys ()
1.43 - val proglang_parent = ThyC.get_theory "ProgLang"
1.44 - in
1.45 - take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
1.46 - end
1.47 -fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)
1.48 - let
1.49 - fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
1.50 - let
1.51 - val allthys = filter_out (member Context.eq_thy
1.52 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
1.53 - ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
1.54 - (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
1.55 - in
1.56 - take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
1.57 - allthys)
1.58 - end
1.59 - val isacthys' = isacthys ()
1.60 - val proglang_parent = ThyC.get_theory "ProgLang"
1.61 - in
1.62 - drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
1.63 - end
1.64 -fun partID thy =
1.65 - if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
1.66 - else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
1.67 - else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
1.68 - else error ("closure of thys in Isac is broken by " ^ Context.theory_name thy)
1.69 -fun partID' thy' = partID (ThyC.get_theory thy')
1.70 -(*\------- to ? from Celem -------/*)
1.71 -
1.72 end (*struct*)
1.73
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Tue Apr 28 15:44:59 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Tue Apr 28 16:51:36 2020 +0200
2.3 @@ -106,6 +106,9 @@
2.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.5 val typ_a2real: term -> term
2.6 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.7 +
2.8 +(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
2.9 + val sym_trm : term -> term
2.10 end
2.11
2.12 (**)
2.13 @@ -595,5 +598,14 @@
2.14 |> member (fn (t1, t2) => fst (dest_Const t1) = fst (dest_Const t2)) ts
2.15 ) handle TERM("dest_Const", _) => raise TERM ("contains_Const_typeless", [t])
2.16
2.17 +(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
2.18 +fun sym_trm trm =
2.19 + let
2.20 + val (lhs, rhs) = (dest_equals o strip_trueprop o Logic.strip_imp_concl) trm
2.21 + val trm' = case strip_imp_prems' trm of
2.22 + NONE => mk_equality (rhs, lhs)
2.23 + | SOME cs => ins_concl cs (mk_equality (rhs, lhs))
2.24 + in trm' end
2.25 +
2.26
2.27 end
2.28 \ No newline at end of file
3.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 28 15:44:59 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Tue Apr 28 16:51:36 2020 +0200
3.3 @@ -98,7 +98,7 @@
3.4 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
3.5 indt (j+i) ^ "<STRING> " ^ ThmC.cut_id thmDeriv ^ " </STRING>\n" ^
3.6 indt (j+i) ^ "<GUH> " ^
3.7 - Thy_Html.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
3.8 + Thy_Html.thm2guh (Thy_Read.thy_containing_thm thmDeriv) (ThmC.cut_id thmDeriv) ^ " </GUH>\n" ^
3.9 indt j ^ "</RULE>\n"
3.10 | rule2xml _ _ (Rule.Eval (_(*termop*), _)) = ""
3.11 (*FIXXXXXXXME.WN060714 in rls make Eval : calc -> rule [add scriptop!]
3.12 @@ -116,7 +116,7 @@
3.13 indt j ^ "<RULE>\n" ^
3.14 indt (j+i) ^ "<TAG> Ruleset </TAG>\n" ^
3.15 indt (j+i) ^ "<STRING> " ^ rls' ^ " </STRING>\n" ^
3.16 - indt (j+i) ^ "<GUH> " ^ Thy_Html.rls2guh (Rtools.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
3.17 + indt (j+i) ^ "<GUH> " ^ Thy_Html.rls2guh (Thy_Read.thy_containing_rls thyID rls') rls' ^ " </GUH>\n" ^
3.18 indt j ^ "</RULE>\n"
3.19 end;
3.20 fun rules2xml _ _ [] = ""
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 15:44:59 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 28 16:51:36 2020 +0200
4.3 @@ -142,7 +142,7 @@
4.4 foldl op ^ ("", map (keref2xml (i+i) Specify.Met_) met) ^
4.5 (indt i) ^ "</METHODS>\n") ^
4.6 indt i ^ "<EVALPRECOND>\n" ^
4.7 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
4.8 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
4.9 indt i ^ "</EVALPRECOND>\n" ^
4.10 authors2xml i "MATHAUTHORS" mathauthors ^
4.11 authors2xml i "COURSEDESIGNS" ["isac team 2006"] ^
4.12 @@ -207,19 +207,19 @@
4.13 pattern2xml i ppc pre ^
4.14 indt i ^ "<EXPLANATIONS> </EXPLANATIONS>\n" ^
4.15 indt i ^ "<EVALPRECOND>\n" ^
4.16 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' prls')) "Rulesets" prls'^
4.17 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' prls')) "Rulesets" prls'^
4.18 indt i ^ "</EVALPRECOND>\n" ^
4.19 indt i ^ "<EVALCOND>\n" ^
4.20 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' erls')) "Rulesets" erls'^
4.21 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' erls')) "Rulesets" erls'^
4.22 indt i ^ "</EVALCOND>\n" ^
4.23 indt i ^ "<EVALLISTEXPR>\n"^
4.24 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' srls')) "Rulesets" srls'^
4.25 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' srls')) "Rulesets" srls'^
4.26 indt i ^ "</EVALLISTEXPR>\n" ^
4.27 indt i ^ "<CHECKELEMENTWISE>\n" ^
4.28 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' crls')) "Rulesets" crls'^
4.29 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' crls')) "Rulesets" crls'^
4.30 indt i ^ "</CHECKELEMENTWISE>\n" ^
4.31 indt i ^ "<NORMALFORM>\n" ^
4.32 - theref2xml (i+i) (snd (Rtools.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
4.33 + theref2xml (i+i) (snd (Thy_Read.thy_containing_rls thy' nrls')) "Rulesets" nrls'^
4.34 indt i ^ "</NORMALFORM>\n" ^
4.35 indt i ^ "<REWORDER> " ^ rew_ord' ^ " </REWORDER>\n" ^
4.36 calcs2xmlOLD i calc ^
5.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Apr 28 15:44:59 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Apr 28 16:51:36 2020 +0200
5.3 @@ -11,6 +11,7 @@
5.4 (* removed all warnings here, only "handle _" remains *)
5.5 ML_file istate.sml
5.6 ML_file "sub-problem.sml"
5.7 + ML_file "thy-read.sml"
5.8 ML_file rewtools.sml
5.9 ML_file "error-pattern.sml"
5.10 ML_file derive.sml
6.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue Apr 28 15:44:59 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Tue Apr 28 16:51:36 2020 +0200
6.3 @@ -23,13 +23,13 @@
6.4
6.5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.6 val find_fill_patterns: Calc.T -> id -> record list
6.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
6.9 val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
6.10 val fill_from_store: Subst.input option * (term * term) list -> term -> id -> thm ->
6.11 record list
6.12 val fill_form: Subst.input option * (term * term) list -> thm * term -> id -> fill_in ->
6.13 record option
6.14 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.15 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.16 end
6.17
6.18 (**)
6.19 @@ -101,7 +101,7 @@
6.20 fun fill_from_store subst form id thm =
6.21 let
6.22 val thmDeriv = Thm.get_name_hint thm
6.23 - val (part, thyID) = Rtools.thy_containing_thm thmDeriv
6.24 + val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
6.25 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
6.26 val fillpats = case Specify.get_the theID of
6.27 Thy_Html.Hthm {fillpats, ...} => fillpats
6.28 @@ -160,7 +160,7 @@
6.29 Tactic.Rewrite_Set rlsID => rlsID
6.30 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
6.31 | _ => "empty"
6.32 - val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
6.33 + val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
6.34 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
6.35 Thy_Html.Hrls {thy_rls = (_, rls), ...} => rls
6.36 | _ => raise ERROR "from_store: uncovered case of get_the"
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 15:44:59 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 16:51:36 2020 +0200
7.3 @@ -8,12 +8,6 @@
7.4 signature REWRITE_TOOLS =
7.5 sig
7.6
7.7 -(*/------- to error-fill-pattern from Rtools -------\*)
7.8 - val thy_containing_thm : string -> string * string
7.9 - val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
7.10 - val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
7.11 -(*\------- to error-fill-pattern from Rtools -------/*)
7.12 -
7.13 datatype contthy
7.14 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
7.15 | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
7.16 @@ -41,53 +35,12 @@
7.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.18 (* NONE *)
7.19 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.20 -
7.21 -(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
7.22 - val sym_trm : term -> term
7.23 end
7.24 (**)
7.25 structure Rtools(**): REWRITE_TOOLS(**) =
7.26 struct
7.27 (**)
7.28
7.29 -(* WN100910 weaker than fun sym_thm for Theory.axioms_of in isa02 *)
7.30 -fun sym_trm trm =
7.31 - let
7.32 - val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) trm
7.33 - val trm' = case TermC.strip_imp_prems' trm of
7.34 - NONE => TermC.mk_equality (rhs, lhs)
7.35 - | SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))
7.36 - in trm' end
7.37 -
7.38 -fun thy_containing_thm thmDeriv =
7.39 - let
7.40 - val isabthys' = map Context.theory_name (Celem.isabthys ());
7.41 - in
7.42 - if member op= isabthys' (ThyC.cut_id thmDeriv)
7.43 - then ("Isabelle", ThyC.cut_id thmDeriv)
7.44 - else ("IsacKnowledge", ThyC.cut_id thmDeriv)
7.45 - end
7.46 -
7.47 -(* which theory in ancestors of thy' contains a ruleset *)
7.48 -fun thy_containing_rls thy' rls' =
7.49 - let
7.50 - val thy = ThyC.get_theory thy'
7.51 - in
7.52 - case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
7.53 - SOME (thy'', _) => (Celem.partID' thy'', thy'')
7.54 - | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
7.55 - end
7.56 -
7.57 -(* this function cannot work as long as the datastructure does not contain thy' *)
7.58 -fun thy_containing_cal thy' sop =
7.59 - let
7.60 - val thy = ThyC.get_theory thy'
7.61 - in
7.62 - case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
7.63 - SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")
7.64 - | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
7.65 - end
7.66 -
7.67 (* packing return-values to matchTheory, contextToThy for xml-generation *)
7.68 datatype contthy = (*also an item from Know_Store on Browser ...........#*)
7.69 EContThy (* not from Know_Store ..............................*)
7.70 @@ -166,7 +119,7 @@
7.71 Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
7.72 ContThm
7.73 {thyID = thy',
7.74 - thm = Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.75 + thm = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.76 applto = f, applat = TermC.empty, reword = ord',
7.77 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
7.78 result = res, resasms = asm, asmrls = Rule_Set.id erls}
7.79 @@ -182,7 +135,7 @@
7.80 ContNOrew
7.81 {thyID = thy',
7.82 thm_rls =
7.83 - Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.84 + Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.85 applto = f}
7.86 end
7.87 | _ => error "context_thy..Rewrite: uncovered case 2")
7.88 @@ -199,7 +152,7 @@
7.89 ContThmInst
7.90 {thyID = thy',
7.91 thm =
7.92 - Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.93 + Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.94 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
7.95 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
7.96 result = res, resasms = asm, asmrls = Rule_Set.id erls}
7.97 @@ -219,7 +172,7 @@
7.98 in
7.99 ContNOrewInst
7.100 {thyID = thy',
7.101 - thm_rls = Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.102 + thm_rls = Thy_Html.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
7.103 bdvs = subst, thminst = thminst, applto = f}
7.104 end
7.105 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
7.106 @@ -229,7 +182,7 @@
7.107 Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
7.108 ContRls
7.109 {thyID = thy',
7.110 - rls = Thy_Html.rls2guh (thy_containing_rls thy' rls') rls',
7.111 + rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
7.112 applto = f, result = res, asms = asm}
7.113 | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
7.114 | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) =
7.115 @@ -237,7 +190,7 @@
7.116 Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
7.117 ContRlsInst
7.118 {thyID = thy',
7.119 - rls = Thy_Html.rls2guh (thy_containing_rls thy' rls') rls',
7.120 + rls = Thy_Html.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',
7.121 bdvs = subst, applto = f, result = res, asms = asm}
7.122 | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
7.123 | context_thy (_, p) tac =
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/Interpret/thy-read.sml Tue Apr 28 16:51:36 2020 +0200
8.3 @@ -0,0 +1,105 @@
8.4 +(* Interpret/thy-read.sml
8.5 + authors: Walther Neuper 2002, 2006
8.6 + (c) due to copyright terms
8.7 +
8.8 +tools for rewriting, reverse rewriting, context to thy concerning rewriting
8.9 +*)
8.10 +
8.11 +signature THEORY_STORE_READ =
8.12 +sig
8.13 + val thy_containing_thm : string -> string * string
8.14 + val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
8.15 + val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
8.16 +
8.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.18 + (* NONE *)
8.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.20 + val isabthys: unit -> theory list
8.21 + val knowthys: unit -> theory list
8.22 + val partID': ThyC.id -> string
8.23 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.24 +end
8.25 +(**)
8.26 +structure Thy_Read(**): THEORY_STORE_READ(**) =
8.27 +struct
8.28 +(**)
8.29 +
8.30 +(* group the theories defined in Isac, compare Build_Thydata:
8.31 + section "Get and group the theories defined in Isac" *)
8.32 +fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
8.33 + let
8.34 + val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata")
8.35 + in
8.36 + drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
8.37 + end
8.38 +fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*)
8.39 + let
8.40 + fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
8.41 + let
8.42 + val allthys = filter_out (member Context.eq_thy
8.43 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
8.44 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
8.45 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
8.46 + in
8.47 + take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
8.48 + allthys)
8.49 + end
8.50 + val isacthys' = isacthys ()
8.51 + val proglang_parent = ThyC.get_theory "ProgLang"
8.52 + in
8.53 + take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
8.54 + end
8.55 +fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)
8.56 + let
8.57 + fun isacthys () = (* ["Isac_Knowledge", .., "Know_Store"] without Build_Isac thys: "Interpret" etc *)
8.58 + let
8.59 + val allthys = filter_out (member Context.eq_thy
8.60 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
8.61 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
8.62 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
8.63 + in
8.64 + take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
8.65 + allthys)
8.66 + end
8.67 + val isacthys' = isacthys ()
8.68 + val proglang_parent = ThyC.get_theory "ProgLang"
8.69 + in
8.70 + drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
8.71 + end
8.72 +fun partID thy =
8.73 + if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
8.74 + else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
8.75 + else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
8.76 + else error ("closure of thys in Isac is broken by " ^ Context.theory_name thy)
8.77 +fun partID' thy' = partID (ThyC.get_theory thy')
8.78 +
8.79 +fun thy_containing_thm thmDeriv =
8.80 + let
8.81 + val isabthys' = map Context.theory_name (isabthys ());
8.82 + in
8.83 + if member op= isabthys' (ThyC.cut_id thmDeriv)
8.84 + then ("Isabelle", ThyC.cut_id thmDeriv)
8.85 + else ("IsacKnowledge", ThyC.cut_id thmDeriv)
8.86 + end
8.87 +
8.88 +(* which theory in ancestors of thy' contains a ruleset *)
8.89 +fun thy_containing_rls thy' rls' =
8.90 + let
8.91 + val thy = ThyC.get_theory thy'
8.92 + in
8.93 + case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
8.94 + SOME (thy'', _) => (partID' thy'', thy'')
8.95 + | _ => error ("thy_containing_rls : rls '" ^ rls' ^ "' not in ancestors of thy '" ^ thy' ^ "'")
8.96 + end
8.97 +
8.98 +(* this function cannot work as long as the datastructure does not contain thy' *)
8.99 +fun thy_containing_cal thy' sop =
8.100 + let
8.101 + val thy = ThyC.get_theory thy'
8.102 + in
8.103 + case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
8.104 + SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")
8.105 + | _ => error ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
8.106 + end
8.107 +
8.108 +(**)end(**)
9.1 --- a/test/Tools/isac/Interpret/rewtools.sml Tue Apr 28 15:44:59 2020 +0200
9.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Apr 28 16:51:36 2020 +0200
9.3 @@ -46,14 +46,14 @@
9.4 val SOME ("Poly", _) = xxx;
9.5 if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
9.6 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
9.7 -if partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
9.8 +if Thy_Read.partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
9.9 ;
9.10 "~~~~~ fun partID', args:"; val (thy') = (thy');
9.11 ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
9.12 ;
9.13 "~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
9.14 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
9.15 -knowthys ()
9.16 +Thy_Read.knowthys ()
9.17 ;
9.18 "~~~~~ fun knowthys , args:"; val () = ();
9.19 val allthys = filter_out (Library.member Context.eq_thy