1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 08 13:21:19 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 08 14:24:38 2020 +0200
1.3 @@ -6,8 +6,8 @@
1.4 signature DATATYPES = (*TODO: redo with xml_of/to *)
1.5 sig
1.6 val authors2xml : int -> string -> string list -> Celem.xml
1.7 - val calc2xml : int -> Rule.thyID * Rule_Def.calc -> Celem.xml
1.8 - val calcrefs2xml : int -> Rule.thyID * Rule_Def.calc list -> Celem.xml
1.9 + val calc2xml : int -> ThyC.thyID * Rule_Def.calc -> Celem.xml
1.10 + val calcrefs2xml : int -> ThyC.thyID * Rule_Def.calc list -> Celem.xml
1.11 val contthy2xml : int -> Rtools.contthy -> Celem.xml
1.12 val extref2xml : int -> string -> string -> Celem.xml
1.13 val filterpbl :
1.14 @@ -37,7 +37,7 @@
1.15 val posterms2xml : int -> (Pos.pos' * term) list -> Celem.xml
1.16 val precond2xml : int -> bool * Term.term -> Celem.xml
1.17 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
1.18 - val rls2xml : int -> Rule.thyID * Rule_Set.T -> Celem.xml
1.19 + val rls2xml : int -> ThyC.thyID * Rule_Set.T -> Celem.xml
1.20 val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml
1.21 val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml
1.22 val scr2xml : int -> Program.T -> Celem.xml
1.23 @@ -47,7 +47,7 @@
1.24 val subst2xml : int -> Rule.subst -> Celem.xml
1.25 val tac2xml : int -> Tactic.input -> Celem.xml
1.26 val tacs2xml : int -> Tactic.input list -> Celem.xml
1.27 - val theref2xml : int -> Rule.thyID -> string -> xstring -> string
1.28 + val theref2xml : int -> ThyC.thyID -> string -> xstring -> string
1.29 val thm'2xml : int -> Celem.thm' -> Celem.xml
1.30 val thm''2xml : int -> thm -> Celem.xml
1.31 val thmstr2xml : int -> string -> Celem.xml
1.32 @@ -505,7 +505,7 @@
1.33 (XML.Elem (("THEOREM", []), [
1.34 XML.Elem (("ID", []), [XML.Text ID]),
1.35 XML.Elem (("FORMULA", []), [
1.36 - XML.Text term])])) = (ID, Rewrite.assoc_thm'' (Rule.Isac ()) ID)
1.37 + XML.Text term])])) = (ID, Rewrite.assoc_thm'' (ThyC.Isac ()) ID)
1.38 | xml_to_thm'' x = raise ERROR ("xml_of_thm' wrong arg:" ^ xmlstr 0 x)
1.39
1.40 fun xml_of_src Rule.EmptyScr =
1.41 @@ -642,7 +642,7 @@
1.42 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
1.43
1.44 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
1.45 - ("Problem (" ^ Rule.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
1.46 + ("Problem (" ^ ThyC.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
1.47
1.48 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
1.49 fun xml_of_posterm (p, t, _) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 08 13:21:19 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 08 14:24:38 2020 +0200
2.3 @@ -55,7 +55,7 @@
2.4 val setMethod : Celem.calcID -> Celem.metID -> XML.tree
2.5 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
2.6 val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
2.7 - val setTheory : Celem.calcID -> Rule.thyID -> XML.tree
2.8 + val setTheory : Celem.calcID -> ThyC.thyID -> XML.tree
2.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.10 (* NONE *)
2.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 08 13:21:19 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 08 14:24:38 2020 +0200
3.3 @@ -108,7 +108,7 @@
3.4 requires elements (rls, calc, ...) to be reorganized.*)
3.5 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
3.6 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
3.7 - TermC.str2term ("Problem (" ^ (get_thy o Rule.theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
3.8 + TermC.str2term ("Problem (" ^ (get_thy o ThyC.theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
3.9 (* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations","univariate","normalise"]);
3.10 val it = "Problem (Isac, [normalise, univariate, equations])" : string
3.11 *)
3.12 @@ -117,7 +117,7 @@
3.13 (* new version with <KESTOREREF>s -- not used *)
3.14 fun pbl2xml (id:(*pblRD*)Celem.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
3.15 thy,where_}:Celem.pbt) =
3.16 - let val thy' = Rule.theory2theory' thy
3.17 + let val thy' = ThyC.theory2theory' thy
3.18 val prls' = (#id o Rule_Set.rep) prls
3.19 in "<NODECONTENT>\n" ^
3.20 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
3.21 @@ -167,7 +167,7 @@
3.22 (*--------------- end display --------------------------------*)
3.23 ^
3.24 indt i ^ "<THEORY>\n" ^
3.25 - theref2xml (i+i) (Rule.theory2theory' thy) "Theorems" "" ^
3.26 + theref2xml (i+i) (ThyC.theory2theory' thy) "Theorems" "" ^
3.27 indt i ^ "</THEORY>\n" ^
3.28 (case met of [] => (indt i) ^ "<METHODS> </METHODS>\n"
3.29 | _ => (indt i) ^ "<METHODS>\n" ^
4.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 08 13:21:19 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 08 14:24:38 2020 +0200
4.3 @@ -20,22 +20,22 @@
4.4
4.5 (* wrap theory-data into the uniform type thydata *)
4.6
4.7 -fun makeHthm (part : string, thyID : Rule.thyID) (thm : thm) =
4.8 +fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) =
4.9 let val theID = [part, thyID, "Theorems"] @ [Celem.thmID_of_derivation_name' thm] : Celem.theID
4.10 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
4.11 mathauthors = ["isac-team"], fillpats = [], thm = thm})
4.12 end;
4.13 -fun makeHrls (part : string) (rls' : Rule_Set.identifier, thy_rls as (thyID, rls): Rule.thyID * Rule_Set.T) =
4.14 +fun makeHrls (part : string) (rls' : Rule_Set.identifier, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) =
4.15 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
4.16 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
4.17 mathauthors = ["isac-team"], thy_rls = thy_rls})
4.18 end;
4.19 -fun makeHcal (part : string, thyID : Rule.thyID) (calID, cal) =
4.20 +fun makeHcal (part : string, thyID : ThyC.thyID) (calID, cal) =
4.21 let val theID = [part, thyID,"Operations"] @ [calID] : Celem.theID
4.22 in (theID, Celem.Hcal {guh = Celem.theID2guh theID, coursedesign=[],
4.23 mathauthors = ["isac-team"], calc = cal})
4.24 end;
4.25 -fun makeHord (part : string, thyID : Rule.thyID) (ordID, ord) =
4.26 +fun makeHord (part : string, thyID : ThyC.thyID) (ordID, ord) =
4.27 let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Celem.theID
4.28 in (theID, Celem.Hord {guh = Celem.theID2guh theID, coursedesign=[],
4.29 mathauthors = ["isac-team"], ord = ord})
4.30 @@ -52,7 +52,7 @@
4.31 else Rule.Thm (Thm.get_name_hint thm, thm)
4.32
4.33 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
4.34 -fun thms_of_rlss thy rlss = (rlss : (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list)
4.35 +fun thms_of_rlss thy rlss = (rlss : (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list)
4.36 |> map (Rtools.thms_of_rls o #2 o #2)
4.37 |> flat
4.38 |> map (revert_sym thy)
4.39 @@ -64,14 +64,14 @@
4.40
4.41 fun collect_thms part thy =
4.42 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
4.43 -fun collect_rlss part rlss thys = (rlss : (Rule_Set.identifier * (Rule.thyID * Rule_Set.T)) list)
4.44 +fun collect_rlss part rlss thys = (rlss : (Rule_Set.identifier * (ThyC.thyID * Rule_Set.T)) list)
4.45 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
4.46 |> map (makeHrls part)
4.47 fun collect_cals (part, thy') =
4.48 let val cals = [] (*FIXXXXXXXXXXME.WN060713 add thyID: (thyID, cal)*)
4.49 in map (makeHcal (part, thy')) cals end;
4.50 fun collect_ords (part, thy') =
4.51 - let val thy = Celem.assoc_thy (Rule.thyID2theory' thy')
4.52 + let val thy = Celem.assoc_thy (ThyC.thyID2theory' thy')
4.53 in [(*TODO.WN060120 rew_ord, Num_Calc*)]:(Celem.theID * Celem.thydata) list end;
4.54
4.55 (* parts are: Isabelle | IsacKnowledge | IsacScripts, see KEStore.thy *)
4.56 @@ -196,7 +196,7 @@
4.57 (*.for mathauthors only, other html is added to xml exported from here.*)
4.58 fun make_isa thy (part, thypart) (mathauthors : Celem.authors) =
4.59 let
4.60 - val theID = [part, Rule.string_of_thy thy, thypart]
4.61 + val theID = [part, ThyC.string_of_thy thy, thypart]
4.62 val guh = case theID of
4.63 [part] => Celem.part2guh theID
4.64 | [part, thyID, thypart] => Celem.thypart2guh theID
4.65 @@ -206,14 +206,14 @@
4.66
4.67 fun make_thy thy (mathauthors : Celem.authors) =
4.68 let
4.69 - val guh = Celem.thy2guh ["IsacKnowledge", Rule.theory2thyID thy]
4.70 + val guh = Celem.thy2guh ["IsacKnowledge", ThyC.theory2thyID thy]
4.71 val theID = Rtools.guh2theID guh
4.72 val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
4.73 in (the, theID) end
4.74
4.75 fun make_thm thy part (thmID : Celem.thmID, thm) (mathauthors : Celem.authors) =
4.76 let
4.77 - val guh = Celem.thm2guh (part, Rule.theory2thyID thy) thmID
4.78 + val guh = Celem.thm2guh (part, ThyC.theory2thyID thy) thmID
4.79 val theID = Rtools.guh2theID guh
4.80 val the = Celem.Hthm {guh = guh, coursedesign = [(*inserted in xml after export*)],
4.81 mathauthors = mathauthors, fillpats = [], thm = thm}
4.82 @@ -221,23 +221,23 @@
4.83
4.84 fun make_rls thy rls (mathauthors : Celem.authors) =
4.85 let
4.86 - val guh = Celem.rls2guh ("IsacKnowledge", Rule.theory2thyID thy) ((#id o Rule_Set.rep) rls)
4.87 + val guh = Celem.rls2guh ("IsacKnowledge", ThyC.theory2thyID thy) ((#id o Rule_Set.rep) rls)
4.88 val theID = Rtools.guh2theID guh
4.89 val the = Celem.Hrls {guh = guh, coursedesign = [], mathauthors = mathauthors,
4.90 - thy_rls = (Rule.theory2thyID thy, rls)}
4.91 + thy_rls = (ThyC.theory2thyID thy, rls)}
4.92 (*needs no (!check_guhs_unique) because guh is generated automatically*)
4.93 in (the, theID) end
4.94
4.95 fun make_cal thy cal (mathauthors : Celem.authors) =
4.96 let
4.97 - val guh = Celem.cal2guh ("IsacKnowledge", Rule.theory2thyID thy) ("TODO store_cal")
4.98 + val guh = Celem.cal2guh ("IsacKnowledge", ThyC.theory2thyID thy) ("TODO store_cal")
4.99 val theID = Rtools.guh2theID guh
4.100 val the = Celem.Hcal {guh = guh, coursedesign = [], mathauthors = mathauthors, calc = cal}
4.101 in (the, theID) end
4.102
4.103 fun make_ord thy ord (mathauthors : Celem.authors) =
4.104 let
4.105 - val guh = Celem.ord2guh ("IsacKnowledge", Rule.theory2thyID thy) ("TODO store_ord")
4.106 + val guh = Celem.ord2guh ("IsacKnowledge", ThyC.theory2thyID thy) ("TODO store_ord")
4.107 val theID = Rtools.guh2theID guh
4.108 val the = Celem.Hord {guh = guh, coursedesign = [], mathauthors = mathauthors, ord = ord}
4.109 in (the, theID) end
5.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 13:21:19 2020 +0200
5.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 14:24:38 2020 +0200
5.3 @@ -8,6 +8,7 @@
5.4 ML_file libraryC.sml
5.5 ML_file "rule-def.sml"
5.6 ML_file "exec-def.sml"
5.7 +ML_file theoryC.sml
5.8 ML_file rule.sml
5.9 ML_file "rule-set.sml"
5.10 ML_file calcelems.sml
5.11 @@ -32,10 +33,10 @@
5.12 *)
5.13 signature KESTORE_ELEMS =
5.14 sig
5.15 - val get_rlss: theory -> (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list
5.16 - val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
5.17 - val get_calcs: theory -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
5.18 - val add_calcs: (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
5.19 + val get_rlss: theory -> (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list
5.20 + val add_rlss: (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
5.21 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
5.22 + val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
5.23 val get_cas: theory -> Celem.cas_elem list
5.24 val add_cas: Celem.cas_elem list -> theory -> theory
5.25 val get_ptyps: theory -> Celem.ptyps
5.26 @@ -54,7 +55,7 @@
5.27 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
5.28
5.29 structure Data = Theory_Data (
5.30 - type T = (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list;
5.31 + type T = (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list;
5.32 val empty = [];
5.33 val extend = I;
5.34 val merge = Rule_Set.to_kestore;
5.35 @@ -63,7 +64,7 @@
5.36 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
5.37
5.38 structure Data = Theory_Data (
5.39 - type T = (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
5.40 + type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
5.41 val empty = [];
5.42 val extend = I;
5.43 val merge = merge Exec_Def.calc_eq;
5.44 @@ -143,7 +144,7 @@
5.45 val get_ref_thy = KEStore_Elems.get_ref_thy;
5.46
5.47 fun assoc_rls (rls' : Rule_Set.identifier) =
5.48 - case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
5.49 + case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.Thy_Info_get_theory "Isac_Knowledge")) rls' of
5.50 SOME (_, rls) => rls
5.51 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
5.52 "TODO exception hierarchy needs to be established.")
6.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Wed Apr 08 13:21:19 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Wed Apr 08 14:24:38 2020 +0200
6.3 @@ -26,7 +26,7 @@
6.4 datatype thydata
6.5 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: guh, mathauthors: authors}
6.6 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: Rule.subst -> term * term -> bool}
6.7 - | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: Rule.thyID * Rule_Set.T}
6.8 + | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: ThyC.thyID * Rule_Set.T}
6.9 | Hthm of {coursedesign: authors, fillpats: fillpat list, guh: guh, mathauthors: authors, thm: thm}
6.10 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
6.11 type theID
6.12 @@ -55,7 +55,7 @@
6.13 type thm'
6.14 val trace_rewrite: bool Unsynchronized.ref
6.15 val depth: int Unsynchronized.ref
6.16 - val assoc_thy: Rule.theory' -> theory
6.17 + val assoc_thy: ThyC.theory' -> theory
6.18 type thm''
6.19 val metID2str: string list -> string
6.20 val e_pblID: pblID
6.21 @@ -76,23 +76,23 @@
6.22 val id_of_thm: Rule.rule -> string
6.23 val isabthys: unit -> theory list
6.24 val thyID_of_derivation_name: string -> string
6.25 - val partID': Rule.theory' -> string
6.26 - val thm2guh: string * Rule.thyID -> thmID -> guh
6.27 + val partID': ThyC.theory' -> string
6.28 + val thm2guh: string * ThyC.thyID -> thmID -> guh
6.29 val thmID_of_derivation_name: string -> string
6.30 - val rls2guh: string * Rule.thyID -> Rule_Set.identifier -> guh
6.31 + val rls2guh: string * ThyC.thyID -> Rule_Set.identifier -> guh
6.32 val theID2guh: theID -> guh
6.33 eqtype fillpatID
6.34 type pbt_ = string * (term * term)
6.35 eqtype xml
6.36 - val cal2guh: string * Rule.thyID -> string -> guh
6.37 + val cal2guh: string * ThyC.thyID -> string -> guh
6.38 val ketype2str': ketype -> string
6.39 val str2ketype': string -> ketype
6.40 val thmID_of_derivation_name': thm -> string
6.41 eqtype filepath
6.42 - val theID2thyID: theID -> Rule.thyID
6.43 + val theID2thyID: theID -> ThyC.thyID
6.44 val thy2guh: theID -> guh
6.45 val thypart2guh: theID -> guh
6.46 - val ord2guh: string * Rule.theory' -> string -> string
6.47 + val ord2guh: string * ThyC.theory' -> string -> string
6.48 val update_hrls: thydata -> Rule.errpatID list -> thydata
6.49 eqtype iterID
6.50 eqtype calcID
6.51 @@ -141,7 +141,7 @@
6.52 type thm' = thmID * Rule.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
6.53 val thm'2xml : int -> Celem.thm' -> Celem.xml
6.54 val assoc_thm': theory -> Celem.thm' -> thm
6.55 -| Calculate' of Rule.theory' * string * term * (term * Celem.thm')
6.56 +| Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
6.57 *)
6.58 (* tricky combination of (string, term) for theorems in Isac:
6.59 * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
6.60 @@ -229,12 +229,12 @@
6.61
6.62 (*the key into the hierarchy ob methods*)
6.63 type metID = string list;
6.64 -type spec = Rule.domID * pblID * metID;
6.65 +type spec = ThyC.domID * pblID * metID;
6.66 fun spec2str (dom, pbl, met) =
6.67 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
6.68 val e_metID = ["e_metID"];
6.69 val metID2str = strs2str;
6.70 -val empty_spec = (Rule.e_domID, e_pblID, e_metID);
6.71 +val empty_spec = (ThyC.e_domID, e_pblID, e_metID);
6.72 val e_spec = empty_spec;
6.73
6.74 (* association list with cas-commands, for generating a complete calc-head *)
6.75 @@ -285,7 +285,7 @@
6.76 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
6.77 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: fillpat list,
6.78 thm: thm} (* here no sym_thm, thus no thmID required *)
6.79 -| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (Rule.thyID * Rule_Set.T)}
6.80 +| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.thyID * Rule_Set.T)}
6.81 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
6.82 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
6.83 ord: (Rule.subst -> (term * term) -> bool)};
6.84 @@ -334,30 +334,30 @@
6.85 (* convert the data got via contextToThy to a globally unique handle.
6.86 there is another way to get the guh: get out of the 'theID' in the hierarchy *)
6.87 fun thm2guh (isa, thyID) thmID = case isa of
6.88 - "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
6.89 - | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
6.90 - | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
6.91 + "Isabelle" => "thy_isab_" ^ ThyC.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID : guh
6.92 + | "IsacKnowledge" => "thy_isac_" ^ ThyC.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
6.93 + | "IsacScripts" => "thy_scri_" ^ ThyC.theory'2thyID thyID ^ "-thm-" ^ strip_thy thmID
6.94 | _ => raise ERROR
6.95 ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
6.96
6.97 fun rls2guh (isa, thyID) rls' = case isa of
6.98 - "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls' : guh
6.99 - | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls'
6.100 - | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-rls-" ^ rls'
6.101 + "Isabelle" => "thy_isab_" ^ ThyC.theory'2thyID thyID ^ "-rls-" ^ rls' : guh
6.102 + | "IsacKnowledge" => "thy_isac_" ^ ThyC.theory'2thyID thyID ^ "-rls-" ^ rls'
6.103 + | "IsacScripts" => "thy_scri_" ^ ThyC.theory'2thyID thyID ^ "-rls-" ^ rls'
6.104 | _ => raise ERROR
6.105 ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
6.106
6.107 fun cal2guh (isa, thyID) calID = case isa of
6.108 - "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID : guh
6.109 - | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID
6.110 - | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-cal-" ^ calID
6.111 + "Isabelle" => "thy_isab_" ^ ThyC.theory'2thyID thyID ^ "-cal-" ^ calID : guh
6.112 + | "IsacKnowledge" => "thy_isac_" ^ ThyC.theory'2thyID thyID ^ "-cal-" ^ calID
6.113 + | "IsacScripts" => "thy_scri_" ^ ThyC.theory'2thyID thyID ^ "-cal-" ^ calID
6.114 | _ => raise ERROR
6.115 ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
6.116
6.117 fun ord2guh (isa, thyID) rew_ord' = case isa of
6.118 - "Isabelle" => "thy_isab_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
6.119 - | "IsacKnowledge" => "thy_isac_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
6.120 - | "IsacScripts" => "thy_scri_" ^ Rule.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
6.121 + "Isabelle" => "thy_isab_" ^ ThyC.theory'2thyID thyID ^ "-ord-" ^ rew_ord' : guh
6.122 + | "IsacKnowledge" => "thy_isac_" ^ ThyC.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
6.123 + | "IsacScripts" => "thy_scri_" ^ ThyC.theory'2thyID thyID ^ "-ord-" ^ rew_ord'
6.124 | _ => raise ERROR
6.125 ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
6.126
6.127 @@ -398,8 +398,8 @@
6.128
6.129 fun assoc_thy thy =
6.130 if thy = "e_domID"
6.131 - then (Rule.Thy_Info_get_theory "Base_Tools") (*lower bound of Knowledge*)
6.132 - else (Rule.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
6.133 + then (ThyC.Thy_Info_get_theory "Base_Tools") (*lower bound of Knowledge*)
6.134 + else (ThyC.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
6.135
6.136 (* overwrite an element in an association list and pair it with a thyID
6.137 in order to create the thy_hierarchy;
6.138 @@ -412,7 +412,7 @@
6.139 actually a hack to get alltogether run again with minimal effort *)
6.140 fun insthy thy' (rls', rls) = (rls', (thy', rls));
6.141 fun overwritelthy thy (al, bl: (Rule_Set.identifier * Rule_Set.T) list) =
6.142 - let val bl' = map (insthy ((get_thy o Rule.theory2theory') thy)) bl
6.143 + let val bl' = map (insthy ((get_thy o ThyC.theory2theory') thy)) bl
6.144 in overwritel (al, bl') end;
6.145
6.146 fun maxthy thy1 thy2 = if Context.subthy (thy1, thy2) then thy2 else thy1;
6.147 @@ -474,7 +474,7 @@
6.148 = "{cas = " ^ (Rule.termopt2str cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
6.149 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
6.150 ^ (strslist2strs met') ^ ", ppc = " ^ pats2str ppc' ^ ", prls = "
6.151 - ^ (Rule_Set.rls2str prls' |> quote) ^ ", thy = {" ^ (Rule.theory2str thy') ^ "}, where_ = "
6.152 + ^ (Rule_Set.rls2str prls' |> quote) ^ ", thy = {" ^ (ThyC.theory2str thy') ^ "}, where_ = "
6.153 ^ (Rule.terms2str w') ^ "}" |> linefeed;
6.154 fun pbts2str pbts = map pbt2str pbts |> list2str;
6.155
6.156 @@ -660,7 +660,7 @@
6.157 section "Get and group the theories defined in Isac" *)
6.158 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
6.159 let
6.160 - val allthys = Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata")
6.161 + val allthys = Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata")
6.162 in
6.163 drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
6.164 end
6.165 @@ -669,15 +669,15 @@
6.166 fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
6.167 let
6.168 val allthys = filter_out (member Context.eq_thy
6.169 - [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
6.170 - Rule.Thy_Info_get_theory "MathEngine", Rule.Thy_Info_get_theory "BridgeLibisabelle"])
6.171 - (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))
6.172 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.Thy_Info_get_theory "Interpret",
6.173 + ThyC.Thy_Info_get_theory "MathEngine", ThyC.Thy_Info_get_theory "BridgeLibisabelle"])
6.174 + (Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata"))
6.175 in
6.176 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
6.177 allthys)
6.178 end
6.179 val isacthys' = isacthys ()
6.180 - val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"
6.181 + val proglang_parent = ThyC.Thy_Info_get_theory "ProgLang"
6.182 in
6.183 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
6.184 end
6.185 @@ -687,15 +687,15 @@
6.186 fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
6.187 let
6.188 val allthys = filter_out (member Context.eq_thy
6.189 - [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
6.190 - Rule.Thy_Info_get_theory "MathEngine", Rule.Thy_Info_get_theory "BridgeLibisabelle"])
6.191 - (Theory.ancestors_of (Rule.Thy_Info_get_theory "Build_Thydata"))
6.192 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.Thy_Info_get_theory "Interpret",
6.193 + ThyC.Thy_Info_get_theory "MathEngine", ThyC.Thy_Info_get_theory "BridgeLibisabelle"])
6.194 + (Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata"))
6.195 in
6.196 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
6.197 allthys)
6.198 end
6.199 val isacthys' = isacthys ()
6.200 - val proglang_parent = Rule.Thy_Info_get_theory "ProgLang"
6.201 + val proglang_parent = ThyC.Thy_Info_get_theory "ProgLang"
6.202 in
6.203 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
6.204 end
6.205 @@ -704,8 +704,8 @@
6.206 if member Context.eq_thy (knowthys ()) thy then "IsacKnowledge"
6.207 else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
6.208 else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
6.209 - else error ("closure of thys in Isac is broken by " ^ Rule.string_of_thy thy)
6.210 -fun partID' thy' = partID (Rule.Thy_Info_get_theory thy')
6.211 + else error ("closure of thys in Isac is broken by " ^ ThyC.string_of_thy thy)
6.212 +fun partID' thy' = partID (ThyC.Thy_Info_get_theory thy')
6.213
6.214 end (*struct*)
6.215
7.1 --- a/src/Tools/isac/CalcElements/contextC.sml Wed Apr 08 13:21:19 2020 +0200
7.2 +++ b/src/Tools/isac/CalcElements/contextC.sml Wed Apr 08 14:24:38 2020 +0200
7.3 @@ -31,13 +31,13 @@
7.4 val empty = Proof_Context.init_global @{theory "Pure"};
7.5 (* ATTENTION: does _not_ recognise Variable.declare_constraints, etc...*)
7.6 fun is_empty ctxt = Context.eq_thy (Proof_Context.theory_of ctxt, @{theory "Pure"});
7.7 -fun isac_ctxt xxx = Proof_Context.init_global (Rule.Isac xxx)
7.8 +fun isac_ctxt xxx = Proof_Context.init_global (ThyC.Isac xxx)
7.9
7.10 val declare_constraints = Variable.declare_constraints
7.11 (* in Subproblem take respective actual arguments from program *)
7.12 fun initialise thy' ts =
7.13 let
7.14 - val ctxt = Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global
7.15 + val ctxt = ThyC.Thy_Info_get_theory thy' |> Proof_Context.init_global
7.16 val frees = map TermC.vars ts |> flat |> distinct
7.17 val _ = TermC.raise_type_conflicts frees
7.18 in
8.1 --- a/src/Tools/isac/CalcElements/exec-def.sml Wed Apr 08 13:21:19 2020 +0200
8.2 +++ b/src/Tools/isac/CalcElements/exec-def.sml Wed Apr 08 14:24:38 2020 +0200
8.3 @@ -6,10 +6,12 @@
8.4 *)
8.5 signature EXECUTE_DEFINITION =
8.6 sig
8.7 + eqtype calID
8.8 eqtype prog_calcID
8.9 type cal
8.10 type calc_elem
8.11 val calc_eq: calc_elem * calc_elem -> bool
8.12 + type eval_fn
8.13 val e_evalfn: Rule_Def.eval_fn
8.14 end
8.15
8.16 @@ -18,6 +20,7 @@
8.17 struct
8.18 (**)
8.19
8.20 +type calID = Rule_Def.calID
8.21 type prog_calcID = string;
8.22 (* op in isa-term "Const(op,_)" *)
8.23 type cal = Rule_Def.calID * Rule_Def.eval_fn;
8.24 @@ -29,5 +32,7 @@
8.25 if pi1 = pi2
8.26 then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
8.27 else false
8.28 +
8.29 +type eval_fn = Rule_Def.eval_fn
8.30 fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
8.31 end
9.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 13:21:19 2020 +0200
9.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 14:24:38 2020 +0200
9.3 @@ -180,7 +180,7 @@
9.4 (* datastructure for KEStore_Elems, intermediate for thehier *)
9.5 type for_kestore =
9.6 (identifier * (* identifier unique within Isac *)
9.7 - (Rule.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
9.8 + (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
9.9 T)) (* ((#id o rep) T) = identifier by coding discipline *)
9.10 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
9.11
10.1 --- a/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 13:21:19 2020 +0200
10.2 +++ b/src/Tools/isac/CalcElements/rule.sml Wed Apr 08 14:24:38 2020 +0200
10.3 @@ -15,11 +15,6 @@
10.4 datatype rule = datatype Rule_Def.rule
10.5 datatype program = datatype Rule_Def.program
10.6
10.7 -(*/------- to exec-def.sml ------------------------\*)
10.8 - eqtype calID
10.9 - type eval_fn = Rule_Def.eval_fn
10.10 -(*\------- to exec-def.sml ------------------------/*)
10.11 -
10.12 eqtype cterm'
10.13 type subst = (term * term) list
10.14
10.15 @@ -37,44 +32,26 @@
10.16
10.17 val scr2str: program -> string
10.18
10.19 -(*/------- to theoryC.sml -------------------------\*)
10.20 - val thy2ctxt: theory -> Proof.context
10.21 - val thy2ctxt': string -> Proof.context
10.22 - val Thy_Info_get_theory: string -> theory
10.23 - eqtype thyID
10.24 - eqtype domID
10.25 - val e_domID: domID
10.26 - eqtype theory'
10.27 - val theory'2thyID: theory' -> theory'
10.28 - val theory2theory': theory -> theory'
10.29 - val theory2thyID: theory -> thyID
10.30 - val thyID2theory': thyID -> thyID
10.31 - val string_of_thy: theory -> theory'
10.32 - val theory2domID: theory -> theory'
10.33 - val Isac: 'a -> theory
10.34 - val string_of_thmI: thm -> string
10.35 -(*\------- to theoryC.sml -------------------------/*)
10.36 -
10.37 val e_term: term (* shift up to Unparse *)
10.38 val e_type: typ (* shift up to Unparse *)
10.39 val type2str: typ -> string
10.40 val term_to_string': Proof.context -> term -> string (* shift up to Unparse *)
10.41 val term2str: term -> string (* shift up to Unparse *)
10.42 val termopt2str: term option -> string (* shift up to Unparse *)
10.43 - val theory2str: theory -> theory' (* shift up to Unparse *)
10.44 val terms2str: term list -> string (* shift up to Unparse *)
10.45 val terms2strs: term list -> string list
10.46 - val term_to_string'': thyID -> term -> string (* shift up to Unparse *)
10.47 + val term_to_string'': ThyC.thyID -> term -> string (* shift up to Unparse *)
10.48 val term_to_string''': theory -> term -> string (* shift up to Unparse *)
10.49 val t2str: theory -> term -> string
10.50 val ts2str: theory -> term list -> string (* shift up to Unparse *)
10.51 val string_of_typ: typ -> string (* shift up to Unparse *)
10.52 - val string_of_typ_thy: thyID -> typ -> string (* shift up to Unparse *)
10.53 + val string_of_typ_thy: ThyC.thyID -> typ -> string (* shift up to Unparse *)
10.54
10.55 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.56 val terms2str': term list -> string (* shift up to Unparse *)
10.57 val thm2str: thm -> string
10.58 val thms2str : thm list -> string
10.59 + val string_of_thmI: thm -> string
10.60 val string_of_thm': theory -> thm -> string (* shift up to Unparse *)
10.61 val errpats2str : errpat list -> string
10.62 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.63 @@ -126,28 +103,21 @@
10.64 fun assoc_rew_ord ro = ((the o assoc') (! rew_ord',ro))
10.65 handle _ => raise ERROR ("ME_Isa: rew_ord '" ^ ro ^ "' not in system");
10.66
10.67 -(* Since Isabelle2017 sessions in theory identifiers are enforced.
10.68 - However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
10.69 -fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
10.70 -fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
10.71 -fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
10.72 -fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
10.73 -
10.74 fun term_to_string' ctxt t =
10.75 let
10.76 val ctxt' = Config.put show_markup false ctxt
10.77 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
10.78 fun term_to_string'' thyID t =
10.79 let
10.80 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
10.81 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
10.82 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
10.83 fun term_to_string''' thy t =
10.84 let
10.85 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
10.86 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
10.87
10.88 -fun term2str t = term_to_string' (thy2ctxt' "Isac_Knowledge") t;
10.89 -fun t2str thy t = term_to_string' (thy2ctxt thy) t;
10.90 +fun term2str t = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") t;
10.91 +fun t2str thy t = term_to_string' (ThyC.thy2ctxt thy) t;
10.92 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
10.93 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
10.94 val terms2str = strs2str o terms2strs; (* terms2str [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
10.95 @@ -176,38 +146,18 @@
10.96 "(\"" ^ id ^ "\",\n" ^ terms2str tms ^ ",\n" ^ thms2str thms
10.97 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
10.98
10.99 -(*ad thm':
10.100 - there are two kinds of theorems ...
10.101 - (1) known by isabelle
10.102 - (2) not known, eg. calc_thm, instantiated rls
10.103 - the latter have a thmid "#..."
10.104 - and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
10.105 - and have a special assoc_thm / assoc_rls in this interface *)
10.106 -type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
10.107 -type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
10.108 -type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
10.109 -val e_domID = "e_domID" : domID;
10.110
10.111 -fun string_of_thy thy = Context.theory_name thy: theory';
10.112 -val theory2domID = string_of_thy;
10.113 -val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
10.114 -val theory2theory' = string_of_thy;
10.115 -val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
10.116 -
10.117 -fun thyID2theory' (thyID:thyID) = thyID;
10.118 -fun theory'2thyID (theory':theory') = theory';
10.119 -
10.120 -fun type_to_string'' (thyID : thyID) t =
10.121 +fun type_to_string'' (thyID : ThyC.thyID) t =
10.122 let
10.123 - val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
10.124 + val ctxt' = Config.put show_markup false (Proof_Context.init_global (ThyC.Thy_Info_get_theory thyID))
10.125 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
10.126 fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
10.127 val string_of_typ = type2str; (*legacy*)
10.128 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
10.129
10.130 (*check for [.] as caused by "fun assoc_thm'"*)
10.131 -fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
10.132 -fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
10.133 +fun string_of_thm thm = term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
10.134 +fun string_of_thm' thy thm = term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)
10.135 fun string_of_thmI thm =
10.136 let
10.137 val str = (de_quote o string_of_thm) thm
11.1 --- a/src/Tools/isac/CalcElements/termC.sml Wed Apr 08 13:21:19 2020 +0200
11.2 +++ b/src/Tools/isac/CalcElements/termC.sml Wed Apr 08 14:24:38 2020 +0200
11.3 @@ -95,7 +95,7 @@
11.4 val atomw: term -> unit
11.5 val atomt: term -> unit
11.6 val atomwy: term -> unit
11.7 - val atomty_thy: Rule.thyID -> term -> unit
11.8 + val atomty_thy: ThyC.thyID -> term -> unit
11.9 val free2var: term -> term
11.10 val contains_one_of: thm * (string * typ) list -> bool
11.11 val contains_Const_typeless: term list -> term -> bool
11.12 @@ -541,11 +541,11 @@
11.13 WN130613 probably compare to
11.14 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
11.15 fun parse_patt thy str =
11.16 - (thy, str) |>> Rule.thy2ctxt
11.17 + (thy, str) |>> ThyC.thy2ctxt
11.18 |-> Proof_Context.read_term_pattern
11.19 |> numbers_to_string (*TODO drop*)
11.20 |> typ_a2real; (*TODO drop*)
11.21 -fun str2term str = parse_patt (Rule.Thy_Info_get_theory "Isac_Knowledge") str
11.22 +fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
11.23
11.24 (* TODO decide with Test_Isac *)
11.25 fun is_atom t = length (vars t) = 1
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/CalcElements/theoryC.sml Wed Apr 08 14:24:38 2020 +0200
12.3 @@ -0,0 +1,57 @@
12.4 +(* Title: CalcElements/exec-def.sml
12.5 + Author: Walther Neuper
12.6 + (c) due to copyright terms
12.7 +
12.8 +TODO: use "Exec_Def" for renaming identifiers
12.9 +*)
12.10 +signature THEORY_ISAC =
12.11 +sig
12.12 + val Thy_Info_get_theory: string -> theory
12.13 + val thy2ctxt': string -> Proof.context
12.14 + val thy2ctxt: theory -> Proof.context
12.15 + val Isac: 'a -> theory
12.16 + eqtype thyID
12.17 + eqtype domID
12.18 + eqtype theory'
12.19 + val e_domID: domID
12.20 + val string_of_thy: theory -> theory'
12.21 + val theory2domID: theory -> theory'
12.22 + val theory2thyID: theory -> thyID
12.23 + val theory2theory': theory -> theory'
12.24 + val theory2str: theory -> theory'
12.25 + val thyID2theory': thyID -> thyID
12.26 + val theory'2thyID: theory' -> theory'
12.27 +end
12.28 +
12.29 +(**)
12.30 +structure ThyC(**): THEORY_ISAC(**) =
12.31 +struct
12.32 +(**)
12.33 +
12.34 +(* Since Isabelle2017 sessions in theory identifiers are enforced.
12.35 + However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
12.36 +fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
12.37 +fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
12.38 +fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
12.39 +fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
12.40 +(*ad thm':
12.41 + there are two kinds of theorems ...
12.42 + (1) known by isabelle
12.43 + (2) not known, eg. calc_thm, instantiated rls
12.44 + the latter have a thmid "#..."
12.45 + and thus outside isa we ALWAYS transport both (thmID, string_of_thmI)
12.46 + and have a special assoc_thm / assoc_rls in this interface *)
12.47 +type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
12.48 +type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
12.49 +type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
12.50 +val e_domID = "e_domID" : domID;
12.51 +fun string_of_thy thy = Context.theory_name thy: theory';
12.52 +val theory2domID = string_of_thy;
12.53 +val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
12.54 +val theory2theory' = string_of_thy;
12.55 +val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
12.56 +
12.57 +fun thyID2theory' (thyID:thyID) = thyID;
12.58 +fun theory'2thyID (theory':theory') = theory';
12.59 +
12.60 +end
13.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 08 13:21:19 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 08 14:24:38 2020 +0200
13.3 @@ -76,8 +76,8 @@
13.4 fun derivat ([]:(term * Rule.rule * (term * term list)) list) = Rule.e_term
13.5 | derivat dt = (#1 o #3 o last_elem) dt
13.6 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
13.7 - val fod = Rtools.make_deriv (Rule.Isac()) erls rules (snd rew_ord) NONE fo
13.8 - val ifod = Rtools.make_deriv (Rule.Isac()) erls rules (snd rew_ord) NONE ifo
13.9 + val fod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE fo
13.10 + val ifod = Rtools.make_deriv (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
13.11 in
13.12 case (fod, ifod) of
13.13 ([], []) => if fo = ifo then (true, []) else (false, [])
13.14 @@ -97,14 +97,14 @@
13.15 fun check_err_patt (res, inf) subst (errpatID, pat) rls =
13.16 let
13.17 val (res', _, _, rewritten) =
13.18 - Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
13.19 + Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
13.20 in
13.21 if rewritten then
13.22 let
13.23 - val norm_res = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls res' of
13.24 + val norm_res = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls res' of
13.25 NONE => res'
13.26 | SOME (norm_res, _) => norm_res
13.27 - val norm_inf = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls inf of
13.28 + val norm_inf = case Rewrite.rewrite_set_inst_ (ThyC.Isac()) false subst rls inf of
13.29 NONE => inf
13.30 | SOME (norm_inf, _) => norm_inf
13.31 in if norm_res = norm_inf then SOME errpatID else NONE
13.32 @@ -134,7 +134,7 @@
13.33 fun get_fillform (subs_opt, subst) (thm, form) errpatID (fillpatID, pat, erpaID) =
13.34 let
13.35 val (form', _, _, rewritten) =
13.36 - Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
13.37 + Rewrite.rew_sub (ThyC.Isac()) 1 subst Rule.e_rew_ord Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
13.38 in (*the fillpat of the thm must be dedicated to errpatID*)
13.39 if errpatID = erpaID andalso rewritten then
13.40 SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
13.41 @@ -170,7 +170,7 @@
13.42 (* check if an input formula is exactly equal the rewrite from a rule
13.43 which is stored at the pos where the input is stored of "ok". *)
13.44 fun is_exactly_equal (pt, pos as (p, _)) istr =
13.45 - case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of
13.46 + case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.thy2ctxt) istr of
13.47 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
13.48 | SOME ifo =>
13.49 let
14.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 08 13:21:19 2020 +0200
14.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 08 14:24:38 2020 +0200
14.3 @@ -18,7 +18,7 @@
14.4 Istate.T * Proof.context * Program.T
14.5
14.6 val get_simplifier : Calc.T -> Rule_Set.T
14.7 - val resume_prog : Rule.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
14.8 + val resume_prog : ThyC.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
14.9 (Istate.T * Proof.context) * Program.T
14.10
14.11 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
14.12 @@ -207,7 +207,7 @@
14.13 else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
14.14 end
14.15 else
14.16 - (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
14.17 + (case Rewrite.rewrite_terms_ (ThyC.Isac ()) ro erls subte t of
14.18 SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
14.19 | NONE => error "associate: Substitute' not applicable to val of Expr")
14.20 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
15.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 13:21:19 2020 +0200
15.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 14:24:38 2020 +0200
15.3 @@ -10,19 +10,19 @@
15.4 type deriv
15.5 val contains_rule : Rule.rule -> Rule_Set.T -> bool
15.6 val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
15.7 - val thy_containing_rls : Rule.theory' -> Rule_Set.identifier -> string * Rule.theory'
15.8 - val thy_containing_cal : Rule.theory' -> Exec_Def.prog_calcID -> string * string
15.9 + val thy_containing_rls : ThyC.theory' -> Rule_Set.identifier -> string * ThyC.theory'
15.10 + val thy_containing_cal : ThyC.theory' -> Exec_Def.prog_calcID -> string * string
15.11 datatype contthy
15.12 - = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: Rule.thyID}
15.13 - | ContNOrewInst of {applto: term, bdvs: Rule.subst, thm_rls: Celem.guh, thminst: term, thyID: Rule.thyID}
15.14 - | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: Rule.thyID}
15.15 - | ContRlsInst of {applto: term, asms: term list, bdvs: Rule.subst, result: term, rls: Celem.guh, thyID: Rule.thyID}
15.16 + = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.thyID}
15.17 + | ContNOrewInst of {applto: term, bdvs: Rule.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}
15.18 + | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}
15.19 + | ContRlsInst of {applto: term, asms: term list, bdvs: Rule.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
15.20 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
15.21 lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord', rhs: term * term,
15.22 - thm: Celem.guh, thyID: Rule.thyID}
15.23 + thm: Celem.guh, thyID: ThyC.thyID}
15.24 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.identifier, asms: (term * term) list,
15.25 bdvs: Rule.subst, lhs: term * term, resasms: term list, result: term, reword: Rule_Def.rew_ord',
15.26 - rhs: term * term, thm: Celem.guh, thminst: term, thyID: Rule.thyID}
15.27 + rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
15.28 | EContThy
15.29 val guh2filename : Celem.guh -> Celem.filename
15.30 val is_sym : Celem.thmID -> bool
15.31 @@ -251,7 +251,7 @@
15.32 (* which theory in ancestors of thy' contains a ruleset *)
15.33 fun thy_containing_rls thy' rls' =
15.34 let
15.35 - val thy = Rule.Thy_Info_get_theory thy'
15.36 + val thy = ThyC.Thy_Info_get_theory thy'
15.37 in
15.38 case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
15.39 SOME (thy'', _) => (Celem.partID' thy'', thy'')
15.40 @@ -261,7 +261,7 @@
15.41 (* this function cannot work as long as the datastructure does not contain thy' *)
15.42 fun thy_containing_cal thy' sop =
15.43 let
15.44 - val thy = Rule.Thy_Info_get_theory thy'
15.45 + val thy = ThyC.Thy_Info_get_theory thy'
15.46 in
15.47 case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
15.48 SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")
15.49 @@ -272,7 +272,7 @@
15.50 datatype contthy = (*also an item from KEStore on Browser ...........#*)
15.51 EContThy (* not from KEStore ..............................*)
15.52 | ContThm of (* a theorem in contex ===========================*)
15.53 - {thyID : Rule.thyID, (* for *2guh in sub-elems here .*)
15.54 + {thyID : ThyC.thyID, (* for *2guh in sub-elems here .*)
15.55 thm : Celem.guh, (* theorem in the context .*)
15.56 applto : term, (* applied to formula ... .*)
15.57 applat : term, (* ... with lhs inserted .*)
15.58 @@ -288,7 +288,7 @@
15.59 asmrls : Rule_Set.identifier (* ruleset for evaluating asms .*)
15.60 }
15.61 | ContThmInst of (* a theorem with bdvs in contex ============ *)
15.62 - {thyID : Rule.thyID, (*for *2guh in sub-elems here .*)
15.63 + {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
15.64 thm : Celem.guh, (*theorem in the context .*)
15.65 bdvs : Rule.subst, (*bound variables to modify... .*)
15.66 thminst : term, (*... theorem instantiated .*)
15.67 @@ -306,14 +306,14 @@
15.68 asmrls : Rule_Set.identifier (*ruleset for evaluating asms .*)
15.69 }
15.70 | ContRls of (* a rule set in contex ========================= *)
15.71 - {thyID : Rule.thyID, (*for *2guh in sub-elems here .*)
15.72 + {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
15.73 rls : Celem.guh, (*rule set in the context .*)
15.74 applto : term, (*rewrite this formula .*)
15.75 result : term, (*resulting from the rewrite .*)
15.76 asms : term list (*... with asms stored .*)
15.77 }
15.78 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
15.79 - {thyID : Rule.thyID, (*for *2guh in sub-elems here .*)
15.80 + {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
15.81 rls : Celem.guh, (*rule set in the context .*)
15.82 bdvs : Rule.subst, (*for bound variables in thms .*)
15.83 applto : term, (*rewrite this formula .*)
15.84 @@ -321,12 +321,12 @@
15.85 asms : term list (*... with asms stored .*)
15.86 }
15.87 | ContNOrew of (* no rewrite for thm or rls ================== *)
15.88 - {thyID : Rule.thyID, (*for *2guh in sub-elems here .*)
15.89 + {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
15.90 thm_rls : Celem.guh, (*thm or rls in the context .*)
15.91 applto : term (*rewrite this formula .*)
15.92 }
15.93 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
15.94 - {thyID : Rule.thyID, (*for *2guh in sub-elems here .*)
15.95 + {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
15.96 thm_rls : Celem.guh, (*thm or rls in the context .*)
15.97 bdvs : Rule.subst, (*for bound variables in thms .*)
15.98 thminst : term, (*... theorem instantiated .*)
15.99 @@ -339,7 +339,7 @@
15.100
15.101 (* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
15.102 fun deriv_of_thm'' (thmID, _) =
15.103 - thmID |> Global_Theory.get_thm (Rule.Isac ()) |> Thm.get_name_hint
15.104 + thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint
15.105
15.106 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
15.107 fun context_thy (pt, pos as (p,p_)) (tac as Tactic.Rewrite thm'') =
15.108 @@ -348,7 +348,7 @@
15.109 (case Applicable.applicable_in pos pt tac of
15.110 Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
15.111 ContThm
15.112 - {thyID = Rule.theory'2thyID thy',
15.113 + {thyID = ThyC.theory'2thyID thy',
15.114 thm = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
15.115 applto = f, applat = Rule.e_term, reword = ord',
15.116 asms = [](*asms ~~ asms'*), lhs = (Rule.e_term, Rule.e_term)(*(lhs, lhs')*), rhs = (Rule.e_term, Rule.e_term)(*(rhs, rhs')*),
15.117 @@ -363,7 +363,7 @@
15.118 | _ => error "context_thy: uncovered position"
15.119 in
15.120 ContNOrew
15.121 - {thyID = Rule.theory'2thyID thy',
15.122 + {thyID = ThyC.theory'2thyID thy',
15.123 thm_rls =
15.124 Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
15.125 applto = f}
15.126 @@ -371,7 +371,7 @@
15.127 | _ => error "context_thy..Rewrite: uncovered case 2")
15.128 end
15.129 | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =
15.130 - let val thm = Global_Theory.get_thm (Rule.Isac ()) thmID
15.131 + let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID
15.132 in
15.133 (case Applicable.applicable_in pos pt tac of
15.134 Applicable.Appl (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>
15.135 @@ -380,7 +380,7 @@
15.136 val thminst = TermC.inst_bdv subst ((Num_Calc.norm o #prop o Thm.rep_thm) thm)
15.137 in
15.138 ContThmInst
15.139 - {thyID = Rule.theory'2thyID thy',
15.140 + {thyID = ThyC.theory'2thyID thy',
15.141 thm =
15.142 Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
15.143 bdvs = subst, thminst = thminst, applto = f, applat = Rule.e_term, reword = ord',
15.144 @@ -389,7 +389,7 @@
15.145 end
15.146 | Applicable.Notappl _ =>
15.147 let
15.148 - val thm = Global_Theory.get_thm (Rule.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
15.149 + val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
15.150 val thm_deriv = Thm.get_name_hint thm
15.151 val pp = Ctree.par_pblobj pt p
15.152 val thy' = Ctree.get_obj Ctree.g_domID pt pp
15.153 @@ -401,7 +401,7 @@
15.154 | _ => error "context_thy: uncovered case 3"
15.155 in
15.156 ContNOrewInst
15.157 - {thyID = Rule.theory'2thyID thy',
15.158 + {thyID = ThyC.theory'2thyID thy',
15.159 thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (Celem.thmID_of_derivation_name thm_deriv),
15.160 bdvs = subst, thminst = thminst, applto = f}
15.161 end
15.162 @@ -411,7 +411,7 @@
15.163 (case Applicable.applicable_in p pt tac of
15.164 Applicable.Appl (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>
15.165 ContRls
15.166 - {thyID = Rule.theory'2thyID thy',
15.167 + {thyID = ThyC.theory'2thyID thy',
15.168 rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
15.169 applto = f, result = res, asms = asm}
15.170 | _ => error ("context_thy Rewrite_Set: not for Applicable.Notappl"))
15.171 @@ -419,7 +419,7 @@
15.172 (case Applicable.applicable_in p pt tac of
15.173 Applicable.Appl (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>
15.174 ContRlsInst
15.175 - {thyID = Rule.theory'2thyID thy',
15.176 + {thyID = ThyC.theory'2thyID thy',
15.177 rls = Celem.rls2guh (thy_containing_rls thy' rls') rls',
15.178 bdvs = subst, applto = f, result = res, asms = asm}
15.179 | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.Notappl"))
15.180 @@ -579,7 +579,7 @@
15.181 in
15.182 case sect of
15.183 "Theorems" =>
15.184 - let val thm = Global_Theory.get_thm (Celem.assoc_thy (Rule.thyID2theory' thyID)) xstr
15.185 + let val thm = Global_Theory.get_thm (Celem.assoc_thy (ThyC.thyID2theory' thyID)) xstr
15.186 in
15.187 if Auto_Prog.contains_bdv thm
15.188 then
16.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Wed Apr 08 13:21:19 2020 +0200
16.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Wed Apr 08 14:24:38 2020 +0200
16.3 @@ -36,8 +36,8 @@
16.4 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
16.5 val (fmz_, vals) = Chead.oris2fmz_vals pors;
16.6 val {cas, ppc, thy, ...} = Specify.get_pbt pI
16.7 - val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
16.8 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt))
16.9 + val dI = ThyC.theory2theory' thy (*take dI from _refined_ pbl*)
16.10 + val dI = ThyC.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, Ctree.rootthy pt))
16.11 val ctxt = ContextC.initialise dI vals
16.12 val hdl =
16.13 case cas of
17.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Apr 08 13:21:19 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Apr 08 14:24:38 2020 +0200
17.3 @@ -43,7 +43,7 @@
17.4 \<close>
17.5 declare[[ML_print_depth = 999]]
17.6 ML \<open>
17.7 -map Rule.theory2thyID progthys'
17.8 +map ThyC.theory2thyID progthys'
17.9 \<close> ML \<open>
17.10 \<close>
17.11
17.12 @@ -80,9 +80,9 @@
17.13 : (Celem.theID * Celem.thydata) list
17.14 \<close>
17.15 ML \<open>
17.16 -map Rule.theory2thyID knowthys'
17.17 +map ThyC.theory2thyID knowthys'
17.18 \<close> ML \<open>
17.19 -Rule.theory2thyID knowledge_parent
17.20 +ThyC.theory2thyID knowledge_parent
17.21 \<close> text \<open>
17.22 collect_part "IsacKnowledge" knowledge_parent knowthys'
17.23 \<close> ML \<open>
18.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Apr 08 13:21:19 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Apr 08 14:24:38 2020 +0200
18.3 @@ -34,7 +34,7 @@
18.4
18.5 ML \<open>
18.6 val thy = @{theory};
18.7 -val ctxt = Rule.thy2ctxt thy;
18.8 +val ctxt = ThyC.thy2ctxt thy;
18.9
18.10 val univariate_equation_prls =
18.11 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty
19.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Wed Apr 08 13:21:19 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Wed Apr 08 14:24:38 2020 +0200
19.3 @@ -210,7 +210,7 @@
19.4 val _ = if pairopt <> NONE then ()
19.5 else error("rewrite_set_, rewrite_ \""^
19.6 (string_of_thmI thm')^"\" \""^
19.7 - (Syntax.string_of_term (Rule.thy2ctxt thy) ct)^"\" = NONE")
19.8 + (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
19.9 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
19.10 val ruls = (#rules o Rule_Set.rep) ruless;
19.11 val (ct',asm') = rew_once ruls [] ct Noap ruls;
19.12 @@ -246,7 +246,7 @@
19.13 val _ = if pairopt <> NONE then ()
19.14 else error("rewrite_set_, rewrite_ \""^
19.15 (string_of_thmI thm')^"\" \""^
19.16 - (Syntax.string_of_term (Rule.thy2ctxt thy) ct)^"\" = NONE")
19.17 + (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
19.18 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
19.19 val ruls = (#rules o Rule_Set.rep) ruless;
19.20 val (ct',asm') = rew_once ruls [] ct Noap ruls;
20.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 08 13:21:19 2020 +0200
20.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 08 14:24:38 2020 +0200
20.3 @@ -7,7 +7,7 @@
20.4
20.5 val get_last_formula: CTbasic.state -> term
20.6 val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
20.7 - val update_domID : CTbasic.ctree -> Pos.pos -> Rule.domID -> CTbasic.ctree
20.8 + val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.domID -> CTbasic.ctree
20.9 val update_met : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
20.10 val update_metppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
20.11 val update_metID : CTbasic.ctree -> Pos.pos -> Celem.metID -> CTbasic.ctree
21.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 08 13:21:19 2020 +0200
21.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 08 14:24:38 2020 +0200
21.3 @@ -63,7 +63,7 @@
21.4 val g_metID : ppobj -> Celem.metID
21.5 val g_result : ppobj -> Selem.result
21.6 val g_tac : ppobj -> Tactic.input
21.7 - val g_domID : ppobj -> Rule.domID (* for appl.sml TODO: replace by thyID *)
21.8 + val g_domID : ppobj -> ThyC.domID (* for appl.sml TODO: replace by thyID *)
21.9
21.10 val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *)
21.11 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context (* for script.sml *)
21.12 @@ -484,7 +484,7 @@
21.13
21.14 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
21.15 let
21.16 - val domID = if dI = Rule.e_domID then dI' else dI
21.17 + val domID = if dI = ThyC.e_domID then dI' else dI
21.18 val pblID = if pI = Celem.e_pblID then pI' else pI
21.19 val metID = if mI = Celem.e_metID then mI' else mI
21.20 in (domID, pblID, metID) end;
21.21 @@ -545,7 +545,7 @@
21.22 (apfst bool2str)))) bts;
21.23 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
21.24 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ Rule.term2str hdf ^
21.25 - ", " ^ Model.itms2str_ (Rule.thy2ctxt' "Isac_Knowledge") itms ^
21.26 + ", " ^ Model.itms2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itms ^
21.27 ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )";
21.28
21.29 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
22.1 --- a/src/Tools/isac/MathEngBasic/model.sml Wed Apr 08 13:21:19 2020 +0200
22.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Wed Apr 08 14:24:38 2020 +0200
22.3 @@ -108,7 +108,7 @@
22.4 (b)
22.5 ==========================================================================*)
22.6
22.7 -val script_parse = the o (@{theory ProgLang} |> Rule.thy2ctxt |> TermC.parseNEW);
22.8 +val script_parse = the o (@{theory ProgLang} |> ThyC.thy2ctxt |> TermC.parseNEW);
22.9 val e_listReal = script_parse "[]::(real list)";
22.10 val e_listBool = script_parse "[]::(bool list)";
22.11
22.12 @@ -400,7 +400,7 @@
22.13 | itm_2str_ ctxt (Mis (d, pid)) =
22.14 "Mis "^ Rule.term_to_string' ctxt d ^ " " ^ Rule.term_to_string' ctxt pid
22.15 | itm_2str_ _ (Par s) = "Trm "^s;
22.16 -fun itm_2str t = itm_2str_ (Rule.thy2ctxt' "Isac_Knowledge") t;
22.17 +fun itm_2str t = itm_2str_ (ThyC.thy2ctxt' "Isac_Knowledge") t;
22.18 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
22.19 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
22.20 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
23.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 13:21:19 2020 +0200
23.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 08 14:24:38 2020 +0200
23.3 @@ -21,14 +21,14 @@
23.4 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
23.5
23.6 | CAScmd' of term
23.7 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
23.8 + | Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
23.9 | Check_Postcond' of Celem.pblID * term
23.10 | Check_elementwise' of term * Rule.cterm' * Selem.result
23.11 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
23.12
23.13 | Derive' of Rule_Set.T
23.14 - | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
23.15 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.16 + | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
23.17 + | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.18 | End_Detail' of Selem.result
23.19
23.20 | Empty_Tac_
23.21 @@ -38,16 +38,16 @@
23.22 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
23.23 | Or_to_List' of term * term
23.24 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
23.25 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * Rule.domID * Celem.metID * Model.itm list
23.26 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
23.27
23.28 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
23.29 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
23.30 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
23.31 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.32 + | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
23.33 + | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
23.34 + | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
23.35 + | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.36
23.37 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
23.38 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
23.39 - | Specify_Theory' of Rule.domID
23.40 + | Specify_Theory' of ThyC.domID
23.41 | Subproblem' of
23.42 Celem.spec * Model.ori list *
23.43 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
23.44 @@ -98,8 +98,8 @@
23.45
23.46 | Specify_Method of Celem.metID
23.47 | Specify_Problem of Celem.pblID
23.48 - | Specify_Theory of Rule.domID
23.49 - | Subproblem of Rule.domID * Celem.pblID
23.50 + | Specify_Theory of ThyC.domID
23.51 + | Subproblem of ThyC.domID * Celem.pblID
23.52
23.53 | Substitute of Selem.sube
23.54 | Tac of string
23.55 @@ -190,8 +190,8 @@
23.56
23.57 | Specify_Method of Celem.metID
23.58 | Specify_Problem of Celem.pblID
23.59 - | Specify_Theory of Rule.domID
23.60 - | Subproblem of Rule.domID * Celem.pblID (* WN0509 drop *)
23.61 + | Specify_Theory of ThyC.domID
23.62 + | Subproblem of ThyC.domID * Celem.pblID (* WN0509 drop *)
23.63
23.64 | Substitute of Selem.sube
23.65 | Tac of string (* WN0509 drop *)
23.66 @@ -351,7 +351,7 @@
23.67 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
23.68 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
23.69 | CAScmd' of term
23.70 - | Calculate' of Rule.theory' * string * term * (term * Celem.thm')
23.71 + | Calculate' of ThyC.theory' * string * term * (term * Celem.thm')
23.72 | Check_Postcond' of Celem.pblID *
23.73 term (* returnvalue of program in solve *)
23.74 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
23.75 @@ -361,8 +361,8 @@
23.76 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
23.77
23.78 | Derive' of Rule_Set.T
23.79 - | Detail_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
23.80 - | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.81 + | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
23.82 + | Detail_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.83 | End_Detail' of Selem.result
23.84
23.85 | Empty_Tac_
23.86 @@ -378,20 +378,20 @@
23.87 | Refine_Tacitly' of
23.88 Celem.pblID * (* input *)
23.89 Celem.pblID * (* the refined from applicable_in *)
23.90 - Rule.domID * (* from new pbt?! filled in specify *)
23.91 + ThyC.domID * (* from new pbt?! filled in specify *)
23.92 Celem.metID * (* from new pbt?! filled in specify *)
23.93 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
23.94 - | Rewrite' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
23.95 - | Rewrite_Inst' of Rule.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
23.96 - | Rewrite_Set' of Rule.theory' * bool * Rule_Set.T * term * Selem.result
23.97 - | Rewrite_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.98 + | Rewrite' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Celem.thm'' * term * Selem.result
23.99 + | Rewrite_Inst' of ThyC.theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * Rule.subst * Celem.thm'' * term * Selem.result
23.100 + | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
23.101 + | Rewrite_Set_Inst' of ThyC.theory' * bool * Rule.subst * Rule_Set.T * term * Selem.result
23.102
23.103 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
23.104 | Specify_Problem' of Celem.pblID *
23.105 (bool * (* matches *)
23.106 (Model.itm list * (* ppc *)
23.107 (bool * term) list)) (* preconditions marked true/false *)
23.108 - | Specify_Theory' of Rule.domID
23.109 + | Specify_Theory' of ThyC.domID
23.110 | Subproblem' of
23.111 Celem.spec *
23.112 (Model.ori list) * (* filled in associate Subproblem' *)
24.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 08 13:21:19 2020 +0200
24.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 08 14:24:38 2020 +0200
24.3 @@ -16,7 +16,7 @@
24.4 val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.5 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.6 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.7 - val set_theory : Rule.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.8 + val set_theory : ThyC.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
24.9 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24.11 (*NONE*)
25.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 08 13:21:19 2020 +0200
25.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 08 14:24:38 2020 +0200
25.3 @@ -28,11 +28,11 @@
25.4 val contain_bdv: Rule.rule list -> bool
25.5 val contains_bdv: thm -> bool
25.6 val subst_typs: term -> typ -> typ -> term
25.7 - val pblterm: Rule.domID -> Celem.pblID -> term
25.8 + val pblterm: ThyC.domID -> Celem.pblID -> term
25.9 val subpbl: string -> string list -> term
25.10 val stacpbls: term -> term list
25.11 val op_of_calc: term -> string
25.12 - val get_calcs: theory -> term -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
25.13 + val get_calcs: theory -> term -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
25.14 val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
25.15 val gen: theory -> term -> Rule_Set.T -> term
25.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26.1 --- a/src/Tools/isac/ProgLang/calculate.sml Wed Apr 08 13:21:19 2020 +0200
26.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Apr 08 14:24:38 2020 +0200
26.3 @@ -11,7 +11,7 @@
26.4 val squfact: int -> int
26.5 val gcd: int -> int -> int
26.6 val sqrt: int -> int
26.7 - val adhoc_thm: theory -> string * Rule.eval_fn -> term -> (string * thm) option
26.8 + val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
26.9 val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
26.10 val norm: term -> term
26.11 val popt2str: ('a * term) option -> string
26.12 @@ -23,7 +23,7 @@
26.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
26.14 (* NONE *)
26.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
26.16 - val get_pair: theory -> string -> Rule.eval_fn -> term -> (string * term) option
26.17 + val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
26.18 val mk_rule: term list * term * term -> term
26.19 val divisors: int -> int list
26.20 val doubles: int list -> int list
26.21 @@ -104,7 +104,7 @@
26.22 fun trace_calc4 str t1 t2 =
26.23 if ! Celem.trace_calc then writeln ("### " ^ str ^ Rule.term2str t1 ^ " $ " ^ Rule.term2str t2) else ()
26.24
26.25 -fun get_pair thy op_ (ef: Rule.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
26.26 +fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
26.27 if op_ = op0 then
26.28 let val popt = ef op_ t thy
26.29 in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
27.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Wed Apr 08 13:21:19 2020 +0200
27.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Wed Apr 08 14:24:38 2020 +0200
27.3 @@ -6,7 +6,7 @@
27.4 sig
27.5 val assoc_thm': theory -> Celem.thm' -> thm
27.6 val assoc_thm'': theory -> Celem.thmID -> thm
27.7 - val calculate_: theory -> string * Rule.eval_fn -> term -> (term * (string * thm)) option
27.8 + val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
27.9 val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
27.10 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
27.11 val eval_true_: theory -> Rule_Set.T -> term -> bool
27.12 @@ -319,7 +319,7 @@
27.13 then mk_thm thy ct'
27.14 else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
27.15 ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
27.16 - error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ Rule.theory2domID thy ^ "\" (and parents)")
27.17 + error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
27.18
27.19 fun eval_prog_expr thy srls t =
27.20 let val rew = rewrite_set_ thy false srls t;
28.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 08 13:21:19 2020 +0200
28.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 08 14:24:38 2020 +0200
28.3 @@ -148,7 +148,7 @@
28.4 in
28.5 case Specify.refine_ori oris pI of
28.6 SOME pblID =>
28.7 - Appl (Tactic.Refine_Tacitly' (pI, pblID, Rule.e_domID, Celem.e_metID, [](*filled in specify*)))
28.8 + Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.e_domID, Celem.e_metID, [](*filled in specify*)))
28.9 | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
28.10 end
28.11 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
28.12 @@ -160,7 +160,7 @@
28.13 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
28.14 => (dI, dI', itms)
28.15 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
28.16 - val thy = if dI' = Rule.e_domID then dI else dI';
28.17 + val thy = if dI' = ThyC.e_domID then dI else dI';
28.18 in
28.19 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
28.20 NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
28.21 @@ -208,7 +208,7 @@
28.22 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
28.23 => (oris, dI, pI, dI', pI', itms)
28.24 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
28.25 - val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');
28.26 + val thy = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');
28.27 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
28.28 val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
28.29 then (false, (Generate.init_pbl ppc, []))
28.30 @@ -471,7 +471,7 @@
28.31 Frm => (get_obj g_form pt p , [])
28.32 | Res => get_obj g_result pt p
28.33 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
28.34 - val vp = (Rule.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
28.35 + val vp = (ThyC.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
28.36 in
28.37 Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
28.38 end
28.39 @@ -511,7 +511,7 @@
28.40 in
28.41 if id' <> "subproblem_equation_dummy"
28.42 then Notappl "no subproblem"
28.43 - else if (Rule.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
28.44 + else if (ThyC.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
28.45 then Appl (Tactic.Tac_ (thy, Rule.term2str f, id, "[" ^ f' ^ "]"))
28.46 else error ("applicable_in: f= " ^ f')
28.47 end
29.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 08 13:21:19 2020 +0200
29.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 08 14:24:38 2020 +0200
29.3 @@ -74,7 +74,7 @@
29.4
29.5 val reset_calchead : Calc.T -> Calc.T
29.6 val get_ocalhd : Calc.T -> Ctree.ocalhd
29.7 - val ocalhd_complete : Model.itm list -> (bool * term) list -> Rule.domID * Celem.pblID * Celem.metID -> bool
29.8 + val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.domID * Celem.pblID * Celem.metID -> bool
29.9 val all_modspec : Calc.T -> Calc.T
29.10
29.11 val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem.pat list -> Model.itm list
29.12 @@ -185,7 +185,7 @@
29.13 fun ocalhd_complete its pre (dI, pI, mI) =
29.14 foldl and_ (true, map #3 (its: Model.itm list)) andalso
29.15 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
29.16 - dI <> Rule.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID
29.17 + dI <> ThyC.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID
29.18
29.19 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
29.20 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
29.21 @@ -359,18 +359,18 @@
29.22 (pbt, mpc) problem type, guard of method
29.23 *)
29.24 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
29.25 - (if dI' = Rule.e_domID andalso dI = Rule.e_domID then (Pbl, Tactic.Specify_Theory dI')
29.26 + (if dI' = ThyC.e_domID andalso dI = ThyC.e_domID then (Pbl, Tactic.Specify_Theory dI')
29.27 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
29.28 else
29.29 case find_first (is_error o #5) pbl of
29.30 SOME (_, _, _, fd, itm_) =>
29.31 - (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)
29.32 + (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_)
29.33 | NONE =>
29.34 - (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of
29.35 + (case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl of
29.36 SOME (fd, ct') => (Pbl, mk_additem fd ct')
29.37 | NONE => (*pbl-items complete*)
29.38 if not preok then (Pbl, Tactic.Refine_Problem pI')
29.39 - else if dI = Rule.e_domID then (Pbl, Tactic.Specify_Theory dI')
29.40 + else if dI = ThyC.e_domID then (Pbl, Tactic.Specify_Theory dI')
29.41 else if pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
29.42 else if mI = Celem.e_metID then (Pbl, Tactic.Specify_Method mI')
29.43 else
29.44 @@ -382,12 +382,12 @@
29.45 | NONE => (Met, Tactic.Apply_Method mI))))
29.46 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
29.47 (case find_first (is_error o #5) met of
29.48 - SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_)
29.49 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_)
29.50 | NONE =>
29.51 - case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris mpc met of
29.52 + case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris mpc met of
29.53 SOME (fd,ct') => (Met, mk_additem fd ct')
29.54 | NONE =>
29.55 - (if dI = Rule.e_domID then (Met, Tactic.Specify_Theory dI')
29.56 + (if dI = ThyC.e_domID then (Met, Tactic.Specify_Theory dI')
29.57 else if pI = Celem.e_pblID then (Met, Tactic.Specify_Problem pI')
29.58 else if not preok then (Met, Tactic.Specify_Method mI)
29.59 else (Met, Tactic.Apply_Method mI)))
29.60 @@ -572,7 +572,7 @@
29.61 ^ "*** description: " ^ TermC.term_detail2str dsc
29.62 ^ "*** value: " ^ TermC.term_detail2str var
29.63 ^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
29.64 - ^ "*** checked by theory: " ^ Rule.theory2str thy ^ "\n"
29.65 + ^ "*** checked by theory: " ^ ThyC.theory2str thy ^ "\n"
29.66 ^ "*** " ^ dots 66);
29.67 writeln (@{make_string} e);
29.68 Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
29.69 @@ -649,7 +649,7 @@
29.70 fun overwrite_ppc thy itm ppc =
29.71 let
29.72 fun repl _ (_, _, _, _, itm_) [] =
29.73 - error ("overwrite_ppc: " ^ (Model.itm_2str_ (Rule.thy2ctxt thy) itm_) ^ " not found")
29.74 + error ("overwrite_ppc: " ^ (Model.itm_2str_ (ThyC.thy2ctxt thy) itm_) ^ " not found")
29.75 | repl ppc' itm (p :: ppc) =
29.76 if (#1 itm) = (#1 p)
29.77 then ppc' @ [itm] @ ppc
29.78 @@ -685,7 +685,7 @@
29.79 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
29.80 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
29.81 | _ => error "specify_additem: uncovered case of get_obj I pt p"
29.82 - val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
29.83 + val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
29.84 val cpI = if pI = Celem.e_pblID then pI' else pI
29.85 val cmI = if mI = Celem.e_metID then mI' else mI
29.86 val {ppc, pre, prls, ...} = Specify.get_met cmI
29.87 @@ -727,7 +727,7 @@
29.88 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
29.89 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
29.90 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
29.91 - val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
29.92 + val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
29.93 val cpI = if pI = Celem.e_pblID then pI' else pI
29.94 val cmI = if mI = Celem.e_metID then mI' else mI
29.95 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
29.96 @@ -773,7 +773,7 @@
29.97 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
29.98 (oris, dI', pI', dI, pI, pbl, ctxt)
29.99 | _ => error "specify (Specify_Theory': uncovered case get_obj"
29.100 - val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
29.101 + val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
29.102 val cpI = if pI = Celem.e_pblID then pI' else pI;
29.103 in
29.104 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
29.105 @@ -794,7 +794,7 @@
29.106 end
29.107 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
29.108 FIXME ..and dont abuse a tactic for that purpose*)
29.109 - ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
29.110 + ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
29.111 (e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
29.112 end
29.113 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
29.114 @@ -803,7 +803,7 @@
29.115 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
29.116 (oris, dI', mI', dI, mI, met, ctxt)
29.117 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
29.118 - val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
29.119 + val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
29.120 val cmI = if mI = Celem.e_metID then mI' else mI;
29.121 in
29.122 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
29.123 @@ -873,7 +873,7 @@
29.124 in (pits, mits) end
29.125
29.126 fun some_spec (odI, opI, omI) (dI, pI, mI) =
29.127 - (if dI = Rule.e_domID then odI else dI,
29.128 + (if dI = ThyC.e_domID then odI else dI,
29.129 if pI = Celem.e_pblID then opI else pI,
29.130 if mI = Celem.e_metID then omI else mI)
29.131
29.132 @@ -976,7 +976,7 @@
29.133 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
29.134 else
29.135 let val (dI,pI,mI) = get_obj g_spec pt p
29.136 - in dI <> Rule.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID end
29.137 + in dI <> ThyC.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID end
29.138
29.139 (* complete empty items in specification from origin (pbl, met ev.refined);
29.140 assumes 'is_complete_mod' *)
30.1 --- a/src/Tools/isac/Specify/generate.sml Wed Apr 08 13:21:19 2020 +0200
30.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Apr 08 14:24:38 2020 +0200
30.3 @@ -338,7 +338,7 @@
30.4 let
30.5 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
30.6 (oris, (domID, pblID, metID), hdl, ctxt_specify)
30.7 - val f = Syntax.string_of_term (Rule.thy2ctxt (Proof_Context.theory_of ctxt)) f
30.8 + val f = Syntax.string_of_term (ThyC.thy2ctxt (Proof_Context.theory_of ctxt)) f
30.9 in
30.10 ((p, Pbl), c, FormKF f, pt)
30.11 end
31.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 08 13:21:19 2020 +0200
31.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 08 14:24:38 2020 +0200
31.3 @@ -140,7 +140,7 @@
31.4 in itm end
31.5 handle _ => (i, v, false, f, Model.Syn (Rule.term2str Rule.e_term (*t ..(t) has not been declared*))))
31.6 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
31.7 - error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt dI) itm ^ "): Par should be internal");
31.8 + error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt dI) itm ^ "): Par should be internal");
31.9
31.10 (*separate a list to a pair of elements that do NOT satisfy the predicate,
31.11 and of elements that satisfy the predicate, i.e. (false, true)*)
31.12 @@ -162,7 +162,7 @@
31.13 (* WN.9.11.03 copied from fun appl_add *)
31.14 fun appl_add' dI oris ppc pbt (sel, ct) =
31.15 let
31.16 - val ctxt = Celem.assoc_thy dI |> Rule.thy2ctxt;
31.17 + val ctxt = Celem.assoc_thy dI |> ThyC.thy2ctxt;
31.18 in
31.19 case TermC.parseNEW ctxt ct of
31.20 NONE => (0, [], false, sel, Model.Syn ct)
31.21 @@ -224,7 +224,7 @@
31.22 else oris2itms pbt vat os
31.23
31.24 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
31.25 - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm)
31.26 + | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm)
31.27 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
31.28 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
31.29 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
31.30 @@ -232,7 +232,7 @@
31.31 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
31.32 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t))
31.33 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
31.34 - error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
31.35 + error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
31.36
31.37 fun imodel2fstr iitems =
31.38 let
32.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 08 13:21:19 2020 +0200
32.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 08 14:24:38 2020 +0200
32.3 @@ -43,18 +43,18 @@
32.4 in
32.5 case p_ of
32.6 Pbl =>
32.7 - (if dI' = Rule.e_domID andalso dI = Rule.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
32.8 + (if dI' = ThyC.e_domID andalso dI = ThyC.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
32.9 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
32.10 else
32.11 case find_first (is_error o #5) pbl of
32.12 SOME (_, _, _, fd, itm_) =>
32.13 - ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_))
32.14 + ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))
32.15 | NONE =>
32.16 - (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of
32.17 + (case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl of
32.18 SOME (fd, ct') => ("dummy", (Pbl, mk_additem fd ct'))
32.19 | NONE => (*pbl-items complete*)
32.20 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
32.21 - else if dI = Rule.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
32.22 + else if dI = ThyC.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
32.23 else if pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
32.24 else if mI = Celem.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))
32.25 else
32.26 @@ -66,12 +66,12 @@
32.27 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
32.28 | Met =>
32.29 (case find_first (is_error o #5) met of
32.30 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_))
32.31 + SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))
32.32 | NONE =>
32.33 - case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris mpc met of
32.34 + case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris mpc met of
32.35 SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
32.36 | NONE =>
32.37 - (if dI = Rule.e_domID then ("dummy", (Met, Tactic.Specify_Theory dI'))
32.38 + (if dI = ThyC.e_domID then ("dummy", (Met, Tactic.Specify_Theory dI'))
32.39 else if pI = Celem.e_pblID then ("dummy", (Met, Tactic.Specify_Problem pI'))
32.40 else if not preok then ("dummy", (Met, Tactic.Specify_Method mI))
32.41 else ("dummy", (Met, Tactic.Apply_Method mI))))
32.42 @@ -85,7 +85,7 @@
32.43 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
32.44 let
32.45 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
32.46 - val dI = if dI = "" then Rule.theory2theory' thy else dI
32.47 + val dI = if dI = "" then ThyC.theory2theory' thy else dI
32.48 val mI = if mI = [] then hd met else mI
32.49 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
32.50 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
32.51 @@ -125,7 +125,7 @@
32.52 end
32.53 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
32.54 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
32.55 - val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
32.56 + val dI = ThyC.theory2theory' (Stool.common_subthy (thy, thy'))
32.57 val hdl = case cas of
32.58 NONE => Auto_Prog.pblterm dI pI
32.59 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
33.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 08 13:21:19 2020 +0200
33.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 08 14:24:38 2020 +0200
33.3 @@ -76,7 +76,7 @@
33.4 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
33.5 (dI, dI', probl, ctxt)
33.6 | _ => error "by_tactic_input Refine_Problem: uncovered case get_obj"
33.7 - val thy = if dI' = Rule.e_domID then dI else dI'
33.8 + val thy = if dI' = ThyC.e_domID then dI else dI'
33.9 in
33.10 case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
33.11 NONE => ([], [], ptp)
33.12 @@ -93,7 +93,7 @@
33.13 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
33.14 (oris, dI, dI', pI', probl, ctxt)
33.15 | _ => error ""
33.16 - val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');
33.17 + val thy = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');
33.18 val {ppc,where_,prls,...} = Specify.get_pbt pI
33.19 val pbl =
33.20 if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
33.21 @@ -151,7 +151,7 @@
33.22 let (* either """"""""""""""" all empty or complete *)
33.23 val thy = Celem.assoc_thy dI'
33.24 val (oris, ctxt) =
33.25 - if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
33.26 + if dI' = ThyC.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
33.27 then ([], ContextC.empty)
33.28 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
33.29 (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
33.30 @@ -170,7 +170,7 @@
33.31 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
33.32 (oris, dI',pI',mI', dI, ctxt)
33.33 | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
33.34 - val thy' = if dI = Rule.e_domID then dI' else dI
33.35 + val thy' = if dI = ThyC.e_domID then dI' else dI
33.36 val thy = Celem.assoc_thy thy'
33.37 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
33.38 val pre = Stool.check_preconds thy prls where_ pbl
33.39 @@ -189,7 +189,7 @@
33.40 PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
33.41 | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
33.42 val {met, thy,...} = Specify.get_pbt pIre
33.43 - val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
33.44 + val (domID, metID) = (ThyC.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
33.45 val ((p,_), _, _, pt) =
33.46 Generate.generate1 (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
33.47 (Istate_Def.Uistate, ContextC.empty) (pt, pos)
33.48 @@ -283,7 +283,7 @@
33.49 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
33.50 let
33.51 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
33.52 - val dI = if dI = "" then Rule.theory2theory' thy else dI
33.53 + val dI = if dI = "" then ThyC.theory2theory' thy else dI
33.54 val mI = if mI = [] then hd met else mI
33.55 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
33.56 val (pt,_) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
33.57 @@ -323,7 +323,7 @@
33.58 end
33.59 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
33.60 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
33.61 - val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
33.62 + val dI = ThyC.theory2theory' (Stool.common_subthy (thy, thy'))
33.63 val hdl = case cas of
33.64 NONE => Auto_Prog.pblterm dI pI
33.65 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
34.1 --- a/src/Tools/isac/TODO.thy Wed Apr 08 13:21:19 2020 +0200
34.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 08 14:24:38 2020 +0200
34.3 @@ -161,7 +161,7 @@
34.4 \end{itemize}
34.5 \item xxx
34.6 \item unify in signature LANGUAGE_TOOLS =\\
34.7 - val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
34.8 + val pblterm: ThyC.domID -> Celem.pblID -> term vvv vvv\\
34.9 val subpbl: string -> string list -> term unify with ^^^
34.10 \item xxx
34.11 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
35.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 08 13:21:19 2020 +0200
35.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 08 14:24:38 2020 +0200
35.3 @@ -7,10 +7,10 @@
35.4 *)
35.5 signature KESTORE_ELEMS =
35.6 sig
35.7 - val get_rlss: theory -> (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list
35.8 - val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
35.9 - val get_calcs: theory -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
35.10 - val add_calcs: (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
35.11 + val get_rlss: theory -> (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list
35.12 + val add_rlss: (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
35.13 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
35.14 + val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
35.15 (*etc*)
35.16 end;
35.17
35.18 @@ -20,7 +20,7 @@
35.19
35.20 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
35.21 structure Data = Theory_Data (
35.22 - type T = (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list;
35.23 + type T = (Rule_Set.identifier * (ThyC.theory' * Rule_Set.T)) list;
35.24 val empty = [];
35.25 val extend = I;
35.26 val merge = merge rls_eq;
35.27 @@ -30,7 +30,7 @@
35.28
35.29 val calc_eq = rls_eq
35.30 structure Data = Theory_Data (
35.31 - type T = (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
35.32 + type T = (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list;
35.33 val empty = [];
35.34 val extend = I;
35.35 val merge = merge calc_eq;
36.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Apr 08 13:21:19 2020 +0200
36.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Apr 08 14:24:38 2020 +0200
36.3 @@ -27,7 +27,7 @@
36.4 "-----------------------------------------------------------------";
36.5
36.6 val thy = @{theory "Biegelinie"};
36.7 -val ctxt = thy2ctxt' "Biegelinie";
36.8 +val ctxt = ThyC.thy2ctxt' "Biegelinie";
36.9 fun str2term str = (Thm.term_of o the o (parse thy)) str;
36.10 fun term2s t = term_to_string'' "Biegelinie" t;
36.11 fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
37.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 08 13:21:19 2020 +0200
37.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 08 14:24:38 2020 +0200
37.3 @@ -237,7 +237,7 @@
37.4 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
37.5 val {ppc, pre, prls,...} = Specify.get_met mID
37.6 val thy = Celem.assoc_thy dI
37.7 - val dI'' = if dI = Rule.e_domID then dI' else dI
37.8 + val dI'' = if dI = ThyC.e_domID then dI' else dI
37.9 val pI'' = if pI = Celem.e_pblID then pI' else pI
37.10 ;
37.11 (*+*)writeln (oris2str oris); (*[
38.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 08 13:21:19 2020 +0200
38.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Wed Apr 08 14:24:38 2020 +0200
38.3 @@ -228,8 +228,8 @@
38.4 => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)
38.5 val (fmz_, vals) = Chead.oris2fmz_vals pors;
38.6 val {cas,ppc,thy,...} = Specify.get_pbt pI
38.7 - val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
38.8 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
38.9 + val dI = ThyC.theory2theory' thy (*.take dI from _refined_ pbl.*)
38.10 + val dI = ThyC.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
38.11 val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);
38.12 (*\\--2 end step into relevant call ----------------------------------------------------------//*)
38.13
39.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Apr 08 13:21:19 2020 +0200
39.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Apr 08 14:24:38 2020 +0200
39.3 @@ -92,19 +92,19 @@
39.4 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
39.5 loc_2str l1;
39.6 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
39.7 -Syntax.string_of_term (thy2ctxt' "DiffApp") t1;
39.8 +Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t1;
39.9 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
39.10
39.11 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
39.12 loc_2str l2;
39.13 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
39.14 -Syntax.string_of_term (thy2ctxt' "DiffApp") t2;
39.15 +Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t2;
39.16 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
39.17
39.18 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
39.19 loc_2str l3;
39.20 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
39.21 -Syntax.string_of_term (thy2ctxt' "DiffApp") t3;
39.22 +Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t3;
39.23 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
39.24
39.25
40.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Apr 08 13:21:19 2020 +0200
40.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Wed Apr 08 14:24:38 2020 +0200
40.3 @@ -45,10 +45,10 @@
40.4 (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
40.5 val t = str2term "((1+2)*4/3)^^^2";
40.6 val thy = @{theory};
40.7 -val times = ("Groups.times_class.times", eval_binop "#mult_") : string * eval_fn;
40.8 -val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * eval_fn;
40.9 -val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * eval_fn;
40.10 -val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * eval_fn;
40.11 +val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn;
40.12 +val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn;
40.13 +val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn;
40.14 +val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Exec_Def.eval_fn;
40.15
40.16 "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
40.17 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
41.1 --- a/test/Tools/isac/Specify/step-specify.sml Wed Apr 08 13:21:19 2020 +0200
41.2 +++ b/test/Tools/isac/Specify/step-specify.sml Wed Apr 08 14:24:38 2020 +0200
41.3 @@ -68,12 +68,12 @@
41.4 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI))
41.5 (* vv----^^*)
41.6 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI));
41.7 - (*if*) dI' = Rule.e_domID andalso dI = Rule.e_domID (*else*);
41.8 + (*if*) dI' = ThyC.e_domID andalso dI = ThyC.e_domID (*else*);
41.9 (*if*) pI' = Celem.e_pblID andalso pI = Celem.e_pblID (*else*);
41.10 val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
41.11 - val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl (*of*);
41.12 + val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl (*of*);
41.13 (*if*) not preok (*else*);
41.14 - (*if*) dI = Rule.e_domID (*then*);
41.15 + (*if*) dI = ThyC.e_domID (*then*);
41.16
41.17 (Pbl, Tactic.Specify_Theory dI') (*return from nxt_spec*);
41.18 "~~~~~ from fun nxt_spec\<longrightarrow>fun nxt_specify_, return:"; val (_, tac)
42.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 08 13:21:19 2020 +0200
42.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 08 14:24:38 2020 +0200
42.3 @@ -128,6 +128,8 @@
42.4 open Celem; e_pbt;
42.5 open Rule; string_of_thm;
42.6 open Rule_Set
42.7 + open Exec_Def
42.8 + open ThyC
42.9 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
42.10 \<close>
42.11