1.1 --- a/src/Tools/isac/BaseDefinitions/KEStore.thy Wed Apr 15 11:37:43 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/KEStore.thy Wed Apr 15 13:47:56 2020 +0200
1.3 @@ -45,8 +45,8 @@
1.4 *)
1.5 signature KESTORE_ELEMS =
1.6 sig
1.7 - val get_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list
1.8 - val add_rlss: (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
1.9 + val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
1.10 + val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
1.11 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.12 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.13 val get_cas: theory -> Celem.cas_elem list
1.14 @@ -67,7 +67,7 @@
1.15 fun union_overwrite eq l1 l2 = fold (insert eq) l2 (*..swapped..*) l1;
1.16
1.17 structure Data = Theory_Data (
1.18 - type T = (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list;
1.19 + type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
1.20 val empty = [];
1.21 val extend = I;
1.22 val merge = Rule_Set.to_kestore;
1.23 @@ -156,7 +156,7 @@
1.24 val get_ref_thy = KEStore_Elems.get_ref_thy;
1.25
1.26 fun assoc_rls (rls' : Rule_Set.id) =
1.27 - case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.Thy_Info_get_theory "Isac_Knowledge")) rls' of
1.28 + case AList.lookup (op =) (KEStore_Elems.get_rlss (ThyC.get_theory "Isac_Knowledge")) rls' of
1.29 SOME (_, rls) => rls
1.30 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
1.31 "TODO exception hierarchy needs to be established.")
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 11:37:43 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 13:47:56 2020 +0200
2.3 @@ -25,7 +25,7 @@
2.4 datatype thydata
2.5 = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: guh, mathauthors: authors}
2.6 | Hord of {coursedesign: authors, guh: guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
2.7 - | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: ThyC.thyID * Rule_Set.T}
2.8 + | Hrls of {coursedesign: authors, guh: guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
2.9 | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: guh, mathauthors: authors, thm: thm}
2.10 | Html of {coursedesign: authors, guh: guh, html: string, mathauthors: authors}
2.11 type theID
2.12 @@ -52,7 +52,7 @@
2.13 val trace_calc: bool Unsynchronized.ref
2.14 val trace_rewrite: bool Unsynchronized.ref
2.15 val depth: int Unsynchronized.ref
2.16 - val assoc_thy: ThyC.theory' -> theory
2.17 + val assoc_thy: ThyC.id -> theory
2.18 val metID2str: string list -> string
2.19 val e_pblID: pblID
2.20 val e_metID: metID
2.21 @@ -70,20 +70,20 @@
2.22 eqtype filename
2.23 val lim_deriv: int Unsynchronized.ref
2.24 val isabthys: unit -> theory list
2.25 - val partID': ThyC.theory' -> string
2.26 - val thm2guh: string * ThyC.thyID -> ThmC_Def.id -> guh
2.27 - val rls2guh: string * ThyC.thyID -> Rule_Set.id -> guh
2.28 + val partID': ThyC.id -> string
2.29 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> guh
2.30 + val rls2guh: string * ThyC.id -> Rule_Set.id -> guh
2.31 val theID2guh: theID -> guh
2.32 type pbt_ = string * (term * term)
2.33 eqtype xml
2.34 - val cal2guh: string * ThyC.thyID -> string -> guh
2.35 + val cal2guh: string * ThyC.id -> string -> guh
2.36 val ketype2str': ketype -> string
2.37 val str2ketype': string -> ketype
2.38 eqtype filepath
2.39 - val theID2thyID: theID -> ThyC.thyID
2.40 + val theID2thyID: theID -> ThyC.id
2.41 val thy2guh: theID -> guh
2.42 val thypart2guh: theID -> guh
2.43 - val ord2guh: string * ThyC.theory' -> string -> string
2.44 + val ord2guh: string * ThyC.id -> string -> string
2.45 val update_hrls: thydata -> Error_Fill_Def.errpatID list -> thydata
2.46 eqtype iterID
2.47 eqtype calcID
2.48 @@ -157,12 +157,12 @@
2.49
2.50 (*the key into the hierarchy ob methods*)
2.51 type metID = string list;
2.52 -type spec = ThyC.domID * pblID * metID;
2.53 +type spec = ThyC.id * pblID * metID;
2.54 fun spec2str (dom, pbl, met) =
2.55 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
2.56 val e_metID = ["e_metID"];
2.57 val metID2str = strs2str;
2.58 -val empty_spec = (ThyC.e_domID, e_pblID, e_metID);
2.59 +val empty_spec = (ThyC.id_empty, e_pblID, e_metID);
2.60 val e_spec = empty_spec;
2.61
2.62 (* association list with cas-commands, for generating a complete calc-head *)
2.63 @@ -213,7 +213,7 @@
2.64 Html of {guh: guh, coursedesign: authors, mathauthors: authors, html: string}
2.65 | Hthm of {guh: guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
2.66 thm: thm} (* here no sym_thm, thus no thmID required *)
2.67 -| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.thyID * Rule_Set.T)}
2.68 +| Hrls of {guh: guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
2.69 | Hcal of {guh: guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
2.70 | Hord of {guh: guh, coursedesign: authors, mathauthors: authors,
2.71 ord: (UnparseC.subst -> (term * term) -> bool)};
2.72 @@ -325,9 +325,9 @@
2.73 type filename = string;
2.74
2.75 fun assoc_thy thy =
2.76 - if thy = "e_domID"
2.77 - then (ThyC.Thy_Info_get_theory "Base_Tools") (*lower bound of Knowledge*)
2.78 - else (ThyC.Thy_Info_get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.79 + if thy = "thy_empty_id"
2.80 + then (ThyC.get_theory "Base_Tools") (*lower bound of Knowledge*)
2.81 + else (ThyC.get_theory thy) handle _ => error ("ME_Isa: thy \"" ^ thy ^ "\" not in system");
2.82
2.83 (* overwrite an element in an association list and pair it with a thyID
2.84 in order to create the thy_hierarchy;
2.85 @@ -588,7 +588,7 @@
2.86 section "Get and group the theories defined in Isac" *)
2.87 fun isabthys () = (*["Complex_Main", "Taylor", .., "Pure"]*)
2.88 let
2.89 - val allthys = Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata")
2.90 + val allthys = Theory.ancestors_of (ThyC.get_theory "Build_Thydata")
2.91 in
2.92 drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
2.93 end
2.94 @@ -597,15 +597,15 @@
2.95 fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
2.96 let
2.97 val allthys = filter_out (member Context.eq_thy
2.98 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.Thy_Info_get_theory "Interpret",
2.99 - ThyC.Thy_Info_get_theory "MathEngine", ThyC.Thy_Info_get_theory "BridgeLibisabelle"])
2.100 - (Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata"))
2.101 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
2.102 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
2.103 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
2.104 in
2.105 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
2.106 allthys)
2.107 end
2.108 val isacthys' = isacthys ()
2.109 - val proglang_parent = ThyC.Thy_Info_get_theory "ProgLang"
2.110 + val proglang_parent = ThyC.get_theory "ProgLang"
2.111 in
2.112 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
2.113 end
2.114 @@ -615,15 +615,15 @@
2.115 fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
2.116 let
2.117 val allthys = filter_out (member Context.eq_thy
2.118 - [(*Thy_Info_get_theory "ProgLang",*) ThyC.Thy_Info_get_theory "Interpret",
2.119 - ThyC.Thy_Info_get_theory "MathEngine", ThyC.Thy_Info_get_theory "BridgeLibisabelle"])
2.120 - (Theory.ancestors_of (ThyC.Thy_Info_get_theory "Build_Thydata"))
2.121 + [(*Thy_Info_get_theory "ProgLang",*) ThyC.get_theory "Interpret",
2.122 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
2.123 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"))
2.124 in
2.125 take ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys),
2.126 allthys)
2.127 end
2.128 val isacthys' = isacthys ()
2.129 - val proglang_parent = ThyC.Thy_Info_get_theory "ProgLang"
2.130 + val proglang_parent = ThyC.get_theory "ProgLang"
2.131 in
2.132 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys')
2.133 end
2.134 @@ -633,7 +633,7 @@
2.135 else if member Context.eq_thy (progthys ()) thy then "IsacScripts"
2.136 else if member Context.eq_thy (isabthys ()) thy then "Isabelle"
2.137 else error ("closure of thys in Isac is broken by " ^ ThyC.string_of_thy thy)
2.138 -fun partID' thy' = partID (ThyC.Thy_Info_get_theory thy')
2.139 +fun partID' thy' = partID (ThyC.get_theory thy')
2.140
2.141 end (*struct*)
2.142
3.1 --- a/src/Tools/isac/BaseDefinitions/contextC.sml Wed Apr 15 11:37:43 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/contextC.sml Wed Apr 15 13:47:56 2020 +0200
3.3 @@ -37,7 +37,7 @@
3.4 (* in Subproblem take respective actual arguments from program *)
3.5 fun initialise thy' ts =
3.6 let
3.7 - val ctxt = ThyC.Thy_Info_get_theory thy' |> Proof_Context.init_global
3.8 + val ctxt = ThyC.get_theory thy' |> Proof_Context.init_global
3.9 val frees = map TermC.vars ts |> flat |> distinct
3.10 val _ = TermC.raise_type_conflicts frees
3.11 in
4.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Apr 15 11:37:43 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Wed Apr 15 13:47:56 2020 +0200
4.3 @@ -115,7 +115,7 @@
4.4 (* datastructure for KEStore_Elems, intermediate for thehier *)
4.5 type for_kestore =
4.6 (id * (* id unique within Isac *)
4.7 - (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
4.8 + (ThyC.id * (* just for assignment in thehier, not appropriate for parsing etc *)
4.9 T)) (* ((#id o rep) T) = id by coding discipline *)
4.10 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
4.11
5.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Apr 15 11:37:43 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Apr 15 13:47:56 2020 +0200
5.3 @@ -99,7 +99,7 @@
5.4 val atomw: term -> unit
5.5 val atomt: term -> unit
5.6 val atomwy: term -> unit
5.7 - val atomty_thy: ThyC.thyID -> term -> unit
5.8 + val atomty_thy: ThyC.id -> term -> unit
5.9 val free2var: term -> term
5.10 val contains_one_of: thm * (string * typ) list -> bool
5.11 val contains_Const_typeless: term list -> term -> bool
5.12 @@ -508,11 +508,11 @@
5.13 WN130613 probably compare to
5.14 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
5.15 fun parse_patt thy str = (thy, str)
5.16 - |>> ThyC.thy2ctxt
5.17 + |>> ThyC.to_ctxt
5.18 |-> Proof_Context.read_term_pattern
5.19 |> numbers_to_string (*TODO drop*)
5.20 |> typ_a2real; (*TODO drop*)
5.21 -fun str2term str = parse_patt (ThyC.Thy_Info_get_theory "Isac_Knowledge") str
5.22 +fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
5.23
5.24 (* TODO decide with Test_Isac *)
5.25 fun is_atom t = length (vars t) = 1
6.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 15 11:37:43 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Apr 15 13:47:56 2020 +0200
6.3 @@ -6,23 +6,43 @@
6.4 *)
6.5 signature THEORY_ISAC =
6.6 sig
6.7 - eqtype thyID
6.8 +(*eqtype thyID*)
6.9 + eqtype id
6.10 +(** )
6.11 eqtype domID
6.12 eqtype theory'
6.13 +( **)
6.14 + val cut_id: string -> id
6.15 +(*val thyID_of_derivation_name: string -> id*)
6.16
6.17 - val Thy_Info_get_theory: string -> theory
6.18 - val thy2ctxt': string -> Proof.context
6.19 - val thy2ctxt: theory -> Proof.context
6.20 +(*val Thy_Info_get_theory: id -> theory*)
6.21 + val get_theory: id -> theory
6.22 +(*val thy2ctxt': id -> Proof.context*)
6.23 + val id_to_ctxt: id -> Proof.context
6.24 +(*val thy2ctxt: theory -> Proof.context*)
6.25 + val to_ctxt: theory -> Proof.context
6.26 +
6.27 +(*val e_domID: id*)
6.28 + val id_empty: id
6.29 val Isac: 'a -> theory
6.30 - val e_domID: domID
6.31 - val string_of_thy: theory -> theory'
6.32 - val theory2domID: theory -> theory'
6.33 - val theory2thyID: theory -> thyID
6.34 - val theory2theory': theory -> theory'
6.35 - val theory2str: theory -> theory'
6.36 - val thyID2theory': thyID -> thyID
6.37 - val theory'2thyID: theory' -> theory'
6.38 - val thyID_of_derivation_name: string -> string
6.39 +(*=="==*)
6.40 +
6.41 + val string_of_thy: theory -> id
6.42 +(*val string_of_thy: theory -> id*)
6.43 + val theory2domID: theory -> id
6.44 +(*val theory2domID: theory -> id*)
6.45 + val theory2thyID: theory -> id;
6.46 +(*val theory2thyID: theory -> id;*)
6.47 + val theory2theory': theory -> id
6.48 +(*val theory2theory': theory -> id*)
6.49 + val theory2str: theory -> id
6.50 +(*val theory2str: theory -> id*)
6.51 +
6.52 + val thyID2theory': id -> id
6.53 +(*val thyID2theory': id -> id*)
6.54 + val theory'2thyID: id -> id
6.55 +(*val theory'2thyID: id -> id*)
6.56 +
6.57 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.58 (*NONE*)
6.59 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.60 @@ -35,26 +55,29 @@
6.61 struct
6.62 (**)
6.63
6.64 -(* Since Isabelle2017 sessions in theory identifiers are enforced.
6.65 - However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
6.66 -fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
6.67 +(*
6.68 +type thyID = string;
6.69 +type domID = string;
6.70 +type theory' = string;
6.71 +*)
6.72 +type id = string;
6.73 +fun cut_id dn = hd (space_explode "." dn);
6.74
6.75 -fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
6.76 -fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
6.77 -fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
6.78 -type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
6.79 -type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
6.80 -type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
6.81 -val e_domID = "e_domID" : domID;
6.82 -fun string_of_thy thy = Context.theory_name thy: theory';
6.83 +fun get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID);
6.84 +fun id_to_ctxt thy' = Proof_Context.init_global (get_theory thy');
6.85 +fun to_ctxt thy = Proof_Context.init_global thy;
6.86 +
6.87 +val id_empty = "thy_empty_id";
6.88 +fun Isac _ = Proof_Context.theory_of (id_to_ctxt "Isac_Knowledge");
6.89 +
6.90 +fun string_of_thy thy = Context.theory_name thy;
6.91 val theory2domID = string_of_thy;
6.92 -val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
6.93 +val theory2thyID = (get_thy o string_of_thy);
6.94 val theory2theory' = string_of_thy;
6.95 -val theory2str = string_of_thy; (*WN050903 ..most consistent naming*)
6.96 +val theory2str = string_of_thy;
6.97
6.98 -fun thyID2theory' (thyID:thyID) = thyID;
6.99 -fun theory'2thyID (theory':theory') = theory';
6.100 +fun thyID2theory' thyID = thyID;
6.101 +fun theory'2thyID theory' = theory';
6.102
6.103 -fun thyID_of_derivation_name dn = hd (space_explode "." dn);
6.104
6.105 (**)end(**)
7.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml Wed Apr 15 11:37:43 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml Wed Apr 15 13:47:56 2020 +0200
7.3 @@ -21,11 +21,11 @@
7.4 val terms_in_thy: theory -> term list -> term_as_string
7.5
7.6 val typ: typ -> term_as_string
7.7 - val typ_by_thyID: ThyC.thyID -> typ -> term_as_string
7.8 + val typ_by_thyID: ThyC.id -> typ -> term_as_string
7.9
7.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.11 val terms: term list -> term_as_string
7.12 - val term_by_thyID: ThyC.thyID -> term -> term_as_string
7.13 + val term_by_thyID: ThyC.id -> term -> term_as_string
7.14 val terms_to_strings: term list -> term_as_string list
7.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.16 (*NONE*)
7.17 @@ -49,13 +49,13 @@
7.18 fun term_by_thyID thyID t =
7.19 let
7.20 val ctxt' = Config.put show_markup false (Proof_Context.init_global
7.21 - (ThyC.Thy_Info_get_theory thyID));
7.22 + (ThyC.get_theory thyID));
7.23 in
7.24 Print_Mode.setmp [] (Syntax.string_of_term ctxt') t
7.25 end;
7.26
7.27 -fun term t = term_in_ctxt (ThyC.thy2ctxt' "Isac_Knowledge") t;
7.28 -fun term_in_thy thy t = term_in_ctxt (ThyC.thy2ctxt thy) t;
7.29 +fun term t = term_in_ctxt (ThyC.id_to_ctxt "Isac_Knowledge") t;
7.30 +fun term_in_thy thy t = term_in_ctxt (ThyC.to_ctxt thy) t;
7.31 fun terms_in_thy thy ts = ts |> map (term_in_thy thy) |> strs2str';
7.32 fun terms_to_strings ts = map term ts; (* terms_to_strings [t1,t2] = ["1 + 2", "abc"]; *)
7.33 val terms = strs2str o terms_to_strings; (* terms [t1,t2] = "[\"1 + 2\",\"abc\"]"; *)
7.34 @@ -63,10 +63,10 @@
7.35 fun term_opt (SOME t) = "(SOME " ^ term t ^ ")"
7.36 | term_opt NONE = "NONE";
7.37
7.38 -fun type_to_string'' (thyID : ThyC.thyID) t =
7.39 +fun type_to_string'' (thyID : ThyC.id) t =
7.40 let
7.41 val ctxt' = Config.put show_markup false (Proof_Context.init_global
7.42 - (ThyC.Thy_Info_get_theory thyID))
7.43 + (ThyC.get_theory thyID))
7.44 in
7.45 Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t
7.46 end;
8.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 11:37:43 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 13:47:56 2020 +0200
8.3 @@ -6,8 +6,8 @@
8.4 signature DATATYPES = (*TODO: redo with xml_of/to *)
8.5 sig
8.6 val authors2xml : int -> string -> string list -> Celem.xml
8.7 - val calc2xml : int -> ThyC.thyID * Rule_Def.calc -> Celem.xml
8.8 - val calcrefs2xml : int -> ThyC.thyID * Rule_Def.calc list -> Celem.xml
8.9 + val calc2xml : int -> ThyC.id * Rule_Def.calc -> Celem.xml
8.10 + val calcrefs2xml : int -> ThyC.id * Rule_Def.calc list -> Celem.xml
8.11 val contthy2xml : int -> Rtools.contthy -> Celem.xml
8.12 val extref2xml : int -> string -> string -> Celem.xml
8.13 val filterpbl :
8.14 @@ -37,7 +37,7 @@
8.15 val posterms2xml : int -> (Pos.pos' * term) list -> Celem.xml
8.16 val precond2xml : int -> bool * Term.term -> Celem.xml
8.17 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
8.18 - val rls2xml : int -> ThyC.thyID * Rule_Set.T -> Celem.xml
8.19 + val rls2xml : int -> ThyC.id * Rule_Set.T -> Celem.xml
8.20 val rule2xml : int -> Celem.guh -> Rule.rule -> Celem.xml
8.21 val rules2xml : int -> Celem.guh -> Rule.rule list -> Celem.xml
8.22 val scr2xml : int -> Program.T -> Celem.xml
8.23 @@ -47,7 +47,7 @@
8.24 val subst2xml : int -> UnparseC.subst -> Celem.xml
8.25 val tac2xml : int -> Tactic.input -> Celem.xml
8.26 val tacs2xml : int -> Tactic.input list -> Celem.xml
8.27 - val theref2xml : int -> ThyC.thyID -> string -> xstring -> string
8.28 + val theref2xml : int -> ThyC.id -> string -> xstring -> string
8.29 val thm''2xml : int -> thm -> Celem.xml
8.30 val thmstr2xml : int -> string -> Celem.xml
8.31 end
8.32 @@ -641,7 +641,7 @@
8.33 | xml_to_tac x = raise ERROR ("xml_to_tac: not impl. for " ^ xmlstr 0 x);
8.34
8.35 val e_pblterm = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))
8.36 - ("Problem (" ^ ThyC.e_domID ^ "," ^ strs2str' Celem.e_pblID ^ ")");
8.37 + ("Problem (" ^ ThyC.id_empty ^ "," ^ strs2str' Celem.e_pblID ^ ")");
8.38
8.39 (*WN051224 minimal adaption to exporting Formulae _only_ by getFormulaeFromTo*)
8.40 fun xml_of_posterm (p, t, _) =
9.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 15 11:37:43 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 15 13:47:56 2020 +0200
9.3 @@ -55,7 +55,7 @@
9.4 val setMethod : Celem.calcID -> Celem.metID -> XML.tree
9.5 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
9.6 val setProblem : Celem.calcID -> Celem.pblID -> XML.tree
9.7 - val setTheory : Celem.calcID -> ThyC.thyID -> XML.tree
9.8 + val setTheory : Celem.calcID -> ThyC.id -> XML.tree
9.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.10 (* NONE *)
9.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 11:37:43 2020 +0200
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 13:47:56 2020 +0200
10.3 @@ -6,11 +6,11 @@
10.4
10.5 signature THEORY_HIERARCHY =
10.6 sig
10.7 - val collect_cals: string * ThyC.thyID -> (Celem.theID * Celem.thydata) list
10.8 + val collect_cals: string * ThyC.id -> (Celem.theID * Celem.thydata) list
10.9 val collect_isab: string -> string * thm -> Celem.theID * Celem.thydata
10.10 - val collect_ords: 'a * ThyC.thyID -> (Celem.theID * Celem.thydata) list
10.11 + val collect_ords: 'a * ThyC.id -> (Celem.theID * Celem.thydata) list
10.12 val collect_part: string -> theory -> theory list -> (Celem.theID * Celem.thydata) list
10.13 - val collect_rlss: string -> (Rule_Set.id * (ThyC.thyID * Rule_Set.T)) list -> theory list ->
10.14 + val collect_rlss: string -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory list ->
10.15 (Celem.theID * Celem.thydata) list
10.16 val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list
10.17
10.18 @@ -18,14 +18,14 @@
10.19 val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->
10.20 Celem.thydata * Celem.theID
10.21
10.22 - val makeHcal: string * ThyC.thyID -> string * Rule_Def.calc -> Celem.theID * Celem.thydata
10.23 - val makeHord: string * ThyC.thyID -> string * ((term * term) list -> term * term -> bool) ->
10.24 + val makeHcal: string * ThyC.id -> string * Rule_Def.calc -> Celem.theID * Celem.thydata
10.25 + val makeHord: string * ThyC.id -> string * ((term * term) list -> term * term -> bool) ->
10.26 Celem.theID * Celem.thydata
10.27 - val makeHrls: string -> Rule_Set.id * (ThyC.thyID * Rule_Def.rule_set) ->
10.28 + val makeHrls: string -> Rule_Set.id * (ThyC.id * Rule_Def.rule_set) ->
10.29 Celem.theID * Celem.thydata
10.30 - val makeHthm: string * ThyC.thyID -> thm -> Celem.theID * Celem.thydata
10.31 + val makeHthm: string * ThyC.id -> thm -> Celem.theID * Celem.thydata
10.32 val make_cal: theory -> Rule_Def.calc -> Celem.authors -> Celem.thydata * Celem.theID
10.33 - val make_isa: theory -> ThyC.theory' * ThyC.theory' -> Celem.authors ->
10.34 + val make_isa: theory -> ThyC.id * ThyC.id -> Celem.authors ->
10.35 Celem.thydata * Celem.theID
10.36 val make_ord: theory -> ((term * term) list -> term * term -> bool) -> Celem.authors ->
10.37 Celem.thydata * Celem.theID
10.38 @@ -37,7 +37,7 @@
10.39
10.40 val thes2file: Celem.filepath -> unit
10.41 val thms_of: theory -> thm list
10.42 - val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Def.rule_set)) list ->
10.43 + val thms_of_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Def.rule_set)) list ->
10.44 (string * thm) list
10.45 val thy_hierarchy2file: Celem.filepath -> unit
10.46 val thydata2file: Celem.filepath -> Pos.pos -> Celem.theID -> Celem.thydata -> unit
10.47 @@ -70,29 +70,29 @@
10.48
10.49 (* wrap theory-data into the uniform type thydata *)
10.50
10.51 -fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) =
10.52 +fun makeHthm (part : string, thyID : ThyC.id) (thm : thm) =
10.53 let val theID = [part, thyID, "Theorems"] @ [ThmC.id_of_thm thm] : Celem.theID
10.54 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
10.55 mathauthors = ["isac-team"], fillpats = [], thm = thm})
10.56 end;
10.57 -fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.thyID * Rule_Set.T) =
10.58 +fun makeHrls (part : string) (rls' : Rule_Set.id, thy_rls as (thyID, rls): ThyC.id * Rule_Set.T) =
10.59 let val theID = [part, thyID,"Rulesets"] @ [rls'] : Celem.theID
10.60 in (theID, Celem.Hrls {guh = Celem.theID2guh theID, coursedesign = [],
10.61 mathauthors = ["isac-team"], thy_rls = thy_rls})
10.62 end;
10.63 -fun makeHcal (part : string, thyID : ThyC.thyID) (calID, cal) =
10.64 +fun makeHcal (part : string, thyID : ThyC.id) (calID, cal) =
10.65 let val theID = [part, thyID,"Operations"] @ [calID] : Celem.theID
10.66 in (theID, Celem.Hcal {guh = Celem.theID2guh theID, coursedesign=[],
10.67 mathauthors = ["isac-team"], calc = cal})
10.68 end;
10.69 -fun makeHord (part : string, thyID : ThyC.thyID) (ordID, ord) =
10.70 +fun makeHord (part : string, thyID : ThyC.id) (ordID, ord) =
10.71 let val theID = [part, thyID,"TODO-Orders"] @ [ordID] : Celem.theID
10.72 in (theID, Celem.Hord {guh = Celem.theID2guh theID, coursedesign=[],
10.73 mathauthors = ["isac-team"], ord = ord})
10.74 end;
10.75
10.76 (* get all theorems from the list of rule-sets (defined in Knowledge) *)
10.77 -fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list)
10.78 +fun thms_of_rlss thy rlss = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
10.79 |> map (Rtools.thms_of_rls o #2 o #2)
10.80 |> flat
10.81 |> map (ThmC.revert_sym_rule thy)
10.82 @@ -104,7 +104,7 @@
10.83
10.84 fun collect_thms part thy =
10.85 map (makeHthm (part, Context.theory_name thy)) (rev (thms_of thy))
10.86 -fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.thyID * Rule_Set.T)) list)
10.87 +fun collect_rlss part rlss thys = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
10.88 |> filter (fn (_, (thyID, _)) => member (op=) (map Context.theory_name thys) thyID)
10.89 |> map (makeHrls part)
10.90 fun collect_cals (part, thy') =
10.91 @@ -123,7 +123,7 @@
10.92 (* collect theorems defined in Isabelle *)
10.93 fun collect_isab isa (thmDeriv, thm) =
10.94 let val theID =
10.95 - [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
10.96 + [isa, ThyC.cut_id thmDeriv, "Theorems", ThmC.cut_id thmDeriv]
10.97 in
10.98 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID,
10.99 mathauthors = ["Isabelle team, TU Munich"],
11.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 11:37:43 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 13:47:56 2020 +0200
11.3 @@ -178,7 +178,7 @@
11.4 (* check if an input formula is exactly equal the rewrite from a rule
11.5 which is stored at the pos where the input is stored of "ok". *)
11.6 fun is_exactly_equal (pt, pos as (p, _)) istr =
11.7 - case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.thy2ctxt) istr of
11.8 + case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> ThyC.to_ctxt) istr of
11.9 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
11.10 | SOME ifo =>
11.11 let
12.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 15 11:37:43 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 15 13:47:56 2020 +0200
12.3 @@ -18,7 +18,7 @@
12.4 Istate.T * Proof.context * Program.T
12.5
12.6 val get_simplifier : Calc.T -> Rule_Set.T
12.7 - val resume_prog : ThyC.theory' (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
12.8 + val resume_prog : ThyC.id (*..for lookup in KEStore*) -> Pos.pos' -> Ctree.ctree ->
12.9 (Istate.T * Proof.context) * Program.T
12.10
12.11 val tac_from_prog : Ctree.ctree -> theory (*..for lookup in KEStore*) -> term -> Tactic.input
13.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 15 11:37:43 2020 +0200
13.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 15 13:47:56 2020 +0200
13.3 @@ -10,19 +10,19 @@
13.4 type deriv
13.5 val contains_rule : Rule.rule -> Rule_Set.T -> bool
13.6 val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
13.7 - val thy_containing_rls : ThyC.theory' -> Rule_Set.id -> string * ThyC.theory'
13.8 - val thy_containing_cal : ThyC.theory' -> Exec_Def.prog_calcID -> string * string
13.9 + val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
13.10 + val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
13.11 datatype contthy
13.12 - = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.thyID}
13.13 - | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.thyID}
13.14 - | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.thyID}
13.15 - | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Celem.guh, thyID: ThyC.thyID}
13.16 + = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: ThyC.id}
13.17 + | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Celem.guh, thminst: term, thyID: ThyC.id}
13.18 + | ContRls of {applto: term, asms: term list, result: term, rls: Celem.guh, thyID: ThyC.id}
13.19 + | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Celem.guh, thyID: ThyC.id}
13.20 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
13.21 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
13.22 - thm: Celem.guh, thyID: ThyC.thyID}
13.23 + thm: Celem.guh, thyID: ThyC.id}
13.24 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
13.25 bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
13.26 - rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
13.27 + rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.id}
13.28 | EContThy
13.29 val guh2filename : Celem.guh -> Celem.filename
13.30 val thms_of_rls : Rule_Set.T -> Rule.rule list
13.31 @@ -193,15 +193,15 @@
13.32 let
13.33 val isabthys' = map Context.theory_name (Celem.isabthys ());
13.34 in
13.35 - if member op= isabthys' (ThyC.thyID_of_derivation_name thmDeriv)
13.36 - then ("Isabelle", ThyC.thyID_of_derivation_name thmDeriv)
13.37 - else ("IsacKnowledge", ThyC.thyID_of_derivation_name thmDeriv)
13.38 + if member op= isabthys' (ThyC.cut_id thmDeriv)
13.39 + then ("Isabelle", ThyC.cut_id thmDeriv)
13.40 + else ("IsacKnowledge", ThyC.cut_id thmDeriv)
13.41 end
13.42
13.43 (* which theory in ancestors of thy' contains a ruleset *)
13.44 fun thy_containing_rls thy' rls' =
13.45 let
13.46 - val thy = ThyC.Thy_Info_get_theory thy'
13.47 + val thy = ThyC.get_theory thy'
13.48 in
13.49 case AList.lookup op= (KEStore_Elems.get_rlss thy) rls' of
13.50 SOME (thy'', _) => (Celem.partID' thy'', thy'')
13.51 @@ -211,7 +211,7 @@
13.52 (* this function cannot work as long as the datastructure does not contain thy' *)
13.53 fun thy_containing_cal thy' sop =
13.54 let
13.55 - val thy = ThyC.Thy_Info_get_theory thy'
13.56 + val thy = ThyC.get_theory thy'
13.57 in
13.58 case AList.lookup op= (KEStore_Elems.get_calcs thy) sop of
13.59 SOME (_(*"Groups.plus_class.plus"*), _) => ("IsacKnowledge", "Base_Tools")
13.60 @@ -222,7 +222,7 @@
13.61 datatype contthy = (*also an item from KEStore on Browser ...........#*)
13.62 EContThy (* not from KEStore ..............................*)
13.63 | ContThm of (* a theorem in contex ===========================*)
13.64 - {thyID : ThyC.thyID, (* for *2guh in sub-elems here .*)
13.65 + {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
13.66 thm : Celem.guh, (* theorem in the context .*)
13.67 applto : term, (* applied to formula ... .*)
13.68 applat : term, (* ... with lhs inserted .*)
13.69 @@ -238,7 +238,7 @@
13.70 asmrls : Rule_Set.id (* ruleset for evaluating asms .*)
13.71 }
13.72 | ContThmInst of (* a theorem with bdvs in contex ============ *)
13.73 - {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
13.74 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
13.75 thm : Celem.guh, (*theorem in the context .*)
13.76 bdvs : UnparseC.subst, (*bound variables to modify... .*)
13.77 thminst : term, (*... theorem instantiated .*)
13.78 @@ -256,14 +256,14 @@
13.79 asmrls : Rule_Set.id (*ruleset for evaluating asms .*)
13.80 }
13.81 | ContRls of (* a rule set in contex ========================= *)
13.82 - {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
13.83 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
13.84 rls : Celem.guh, (*rule set in the context .*)
13.85 applto : term, (*rewrite this formula .*)
13.86 result : term, (*resulting from the rewrite .*)
13.87 asms : term list (*... with asms stored .*)
13.88 }
13.89 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
13.90 - {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
13.91 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
13.92 rls : Celem.guh, (*rule set in the context .*)
13.93 bdvs : UnparseC.subst, (*for bound variables in thms .*)
13.94 applto : term, (*rewrite this formula .*)
13.95 @@ -271,12 +271,12 @@
13.96 asms : term list (*... with asms stored .*)
13.97 }
13.98 | ContNOrew of (* no rewrite for thm or rls ================== *)
13.99 - {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
13.100 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
13.101 thm_rls : Celem.guh, (*thm or rls in the context .*)
13.102 applto : term (*rewrite this formula .*)
13.103 }
13.104 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
13.105 - {thyID : ThyC.thyID, (*for *2guh in sub-elems here .*)
13.106 + {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
13.107 thm_rls : Celem.guh, (*thm or rls in the context .*)
13.108 bdvs : UnparseC.subst, (*for bound variables in thms .*)
13.109 thminst : term, (*... theorem instantiated .*)
14.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Apr 15 11:37:43 2020 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Apr 15 13:47:56 2020 +0200
14.3 @@ -54,7 +54,7 @@
14.4
14.5 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
14.6 |> filter (fn (deriv, _) =>
14.7 - member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
14.8 + member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
14.9 : ThmC.T list
14.10 \<close>
14.11
15.1 --- a/src/Tools/isac/Knowledge/Equation.thy Wed Apr 15 11:37:43 2020 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Apr 15 13:47:56 2020 +0200
15.3 @@ -34,7 +34,7 @@
15.4
15.5 ML \<open>
15.6 val thy = @{theory};
15.7 -val ctxt = ThyC.thy2ctxt thy;
15.8 +val ctxt = ThyC.to_ctxt thy;
15.9
15.10 val univariate_equation_prls =
15.11 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty
16.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Wed Apr 15 11:37:43 2020 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Wed Apr 15 13:47:56 2020 +0200
16.3 @@ -210,7 +210,7 @@
16.4 val _ = if pairopt <> NONE then ()
16.5 else error("rewrite_set_, rewrite_ \""^
16.6 (ThmC.string_of_thm thm')^"\" \""^
16.7 - (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
16.8 + (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE")
16.9 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
16.10 val ruls = (#rules o Rule_Set.rep) ruless;
16.11 val (ct',asm') = rew_once ruls [] ct Noap ruls;
16.12 @@ -246,7 +246,7 @@
16.13 val _ = if pairopt <> NONE then ()
16.14 else error("rewrite_set_, rewrite_ \""^
16.15 (ThmC.string_of_thm thm')^"\" \""^
16.16 - (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
16.17 + (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE")
16.18 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
16.19 val ruls = (#rules o Rule_Set.rep) ruless;
16.20 val (ct',asm') = rew_once ruls [] ct Noap ruls;
17.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 15 11:37:43 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 15 13:47:56 2020 +0200
17.3 @@ -7,7 +7,7 @@
17.4
17.5 val get_last_formula: CTbasic.state -> term
17.6 val update_branch : CTbasic.ctree -> Pos.pos -> CTbasic.branch -> CTbasic.ctree
17.7 - val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.domID -> CTbasic.ctree
17.8 + val update_domID : CTbasic.ctree -> Pos.pos -> ThyC.id -> CTbasic.ctree
17.9 val update_met : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =vvv= ? *)
17.10 val update_metppc : CTbasic.ctree -> Pos.pos -> Model.itm list -> CTbasic.ctree (* =^^^= ? *)
17.11 val update_metID : CTbasic.ctree -> Pos.pos -> Celem.metID -> CTbasic.ctree
18.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 15 11:37:43 2020 +0200
18.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 15 13:47:56 2020 +0200
18.3 @@ -63,7 +63,7 @@
18.4 val g_metID : ppobj -> Celem.metID
18.5 val g_result : ppobj -> Selem.result
18.6 val g_tac : ppobj -> Tactic.input
18.7 - val g_domID : ppobj -> ThyC.domID (* for appl.sml TODO: replace by thyID *)
18.8 + val g_domID : ppobj -> ThyC.id (* for appl.sml TODO: replace by thyID *)
18.9
18.10 val g_origin : ppobj -> Model.ori list * Celem.spec * term (* for script.sml *)
18.11 val get_loc : ctree -> Pos.pos' -> Istate_Def.T * Proof.context (* for script.sml *)
18.12 @@ -484,7 +484,7 @@
18.13
18.14 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
18.15 let
18.16 - val domID = if dI = ThyC.e_domID then dI' else dI
18.17 + val domID = if dI = ThyC.id_empty then dI' else dI
18.18 val pblID = if pI = Celem.e_pblID then pI' else pI
18.19 val metID = if mI = Celem.e_metID then mI' else mI
18.20 in (domID, pblID, metID) end;
18.21 @@ -545,7 +545,7 @@
18.22 (apfst bool2str)))) bts;
18.23 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
18.24 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^
18.25 - ", " ^ Model.itms2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itms ^
18.26 + ", " ^ Model.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms ^
18.27 ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )";
18.28
18.29 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
19.1 --- a/src/Tools/isac/MathEngBasic/model.sml Wed Apr 15 11:37:43 2020 +0200
19.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Wed Apr 15 13:47:56 2020 +0200
19.3 @@ -108,7 +108,7 @@
19.4 (b)
19.5 ==========================================================================*)
19.6
19.7 -val script_parse = the o (@{theory ProgLang} |> ThyC.thy2ctxt |> TermC.parseNEW);
19.8 +val script_parse = the o (@{theory ProgLang} |> ThyC.to_ctxt |> TermC.parseNEW);
19.9 val e_listReal = script_parse "[]::(real list)";
19.10 val e_listBool = script_parse "[]::(bool list)";
19.11
19.12 @@ -400,7 +400,7 @@
19.13 | itm_2str_ ctxt (Mis (d, pid)) =
19.14 "Mis "^ UnparseC.term_in_ctxt ctxt d ^ " " ^ UnparseC.term_in_ctxt ctxt pid
19.15 | itm_2str_ _ (Par s) = "Trm "^s;
19.16 -fun itm_2str t = itm_2str_ (ThyC.thy2ctxt' "Isac_Knowledge") t;
19.17 +fun itm_2str t = itm_2str_ (ThyC.id_to_ctxt "Isac_Knowledge") t;
19.18 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
19.19 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
19.20 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
20.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 15 11:37:43 2020 +0200
20.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 15 13:47:56 2020 +0200
20.3 @@ -21,14 +21,14 @@
20.4 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
20.5
20.6 | CAScmd' of term
20.7 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
20.8 + | Calculate' of ThyC.id * string * term * (term * ThmC.T)
20.9 | Check_Postcond' of Celem.pblID * term
20.10 | Check_elementwise' of term * TermC.as_string * Selem.result
20.11 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
20.12
20.13 | Derive' of Rule_Set.T
20.14 - | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
20.15 - | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.16 + | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
20.17 + | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.18 | End_Detail' of Selem.result
20.19
20.20 | Empty_Tac_
20.21 @@ -38,16 +38,16 @@
20.22 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
20.23 | Or_to_List' of term * term
20.24 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
20.25 - | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
20.26 + | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.id * Celem.metID * Model.itm list
20.27
20.28 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
20.29 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
20.30 - | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
20.31 - | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.32 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
20.33 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
20.34 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
20.35 + | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.36
20.37 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
20.38 | Specify_Problem' of Celem.pblID * (bool * (Model.itm list * (bool * term) list))
20.39 - | Specify_Theory' of ThyC.domID
20.40 + | Specify_Theory' of ThyC.id
20.41 | Subproblem' of
20.42 Celem.spec * Model.ori list *
20.43 term * (* CAScmd, e.g. "solve (-1 + x = 0, x)" *)
20.44 @@ -98,8 +98,8 @@
20.45
20.46 | Specify_Method of Celem.metID
20.47 | Specify_Problem of Celem.pblID
20.48 - | Specify_Theory of ThyC.domID
20.49 - | Subproblem of ThyC.domID * Celem.pblID
20.50 + | Specify_Theory of ThyC.id
20.51 + | Subproblem of ThyC.id * Celem.pblID
20.52
20.53 | Substitute of Selem.sube
20.54 | Tac of string
20.55 @@ -190,8 +190,8 @@
20.56
20.57 | Specify_Method of Celem.metID
20.58 | Specify_Problem of Celem.pblID
20.59 - | Specify_Theory of ThyC.domID
20.60 - | Subproblem of ThyC.domID * Celem.pblID (* WN0509 drop *)
20.61 + | Specify_Theory of ThyC.id
20.62 + | Subproblem of ThyC.id * Celem.pblID (* WN0509 drop *)
20.63
20.64 | Substitute of Selem.sube
20.65 | Tac of string (* WN0509 drop *)
20.66 @@ -351,7 +351,7 @@
20.67 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
20.68 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
20.69 | CAScmd' of term
20.70 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.T)
20.71 + | Calculate' of ThyC.id * string * term * (term * ThmC.T)
20.72 | Check_Postcond' of Celem.pblID *
20.73 term (* returnvalue of program in solve *)
20.74 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
20.75 @@ -361,8 +361,8 @@
20.76 | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
20.77
20.78 | Derive' of Rule_Set.T
20.79 - | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
20.80 - | Detail_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.81 + | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
20.82 + | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.83 | End_Detail' of Selem.result
20.84
20.85 | Empty_Tac_
20.86 @@ -378,20 +378,20 @@
20.87 | Refine_Tacitly' of
20.88 Celem.pblID * (* input *)
20.89 Celem.pblID * (* the refined from applicable_in *)
20.90 - ThyC.domID * (* from new pbt?! filled in specify *)
20.91 + ThyC.id * (* from new pbt?! filled in specify *)
20.92 Celem.metID * (* from new pbt?! filled in specify *)
20.93 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
20.94 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
20.95 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
20.96 - | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
20.97 - | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.98 + | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
20.99 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
20.100 + | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
20.101 + | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
20.102
20.103 | Specify_Method' of Celem.metID * Model.ori list * Model.itm list
20.104 | Specify_Problem' of Celem.pblID *
20.105 (bool * (* matches *)
20.106 (Model.itm list * (* ppc *)
20.107 (bool * term) list)) (* preconditions marked true/false *)
20.108 - | Specify_Theory' of ThyC.domID
20.109 + | Specify_Theory' of ThyC.id
20.110 | Subproblem' of
20.111 Celem.spec *
20.112 (Model.ori list) * (* filled in associate Subproblem' *)
21.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Wed Apr 15 11:37:43 2020 +0200
21.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Apr 15 13:47:56 2020 +0200
21.3 @@ -48,7 +48,7 @@
21.4 fun id_of_thm thm = (cut_id o Thm.get_name_hint) thm;
21.5 fun of_thm thm = (id_of_thm thm, thm);
21.6
21.7 -fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.thy2ctxt thy) (Thm.prop_of thm);
21.8 +fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.to_ctxt thy) (Thm.prop_of thm);
21.9
21.10
21.11 (** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
22.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 11:37:43 2020 +0200
22.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 13:47:56 2020 +0200
22.3 @@ -16,7 +16,7 @@
22.4 val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
22.5 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
22.6 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
22.7 - val set_theory : ThyC.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
22.8 + val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
22.9 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
22.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22.11 (*NONE*)
23.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 15 11:37:43 2020 +0200
23.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 15 13:47:56 2020 +0200
23.3 @@ -28,7 +28,7 @@
23.4 val contain_bdv: Rule.rule list -> bool
23.5 val contains_bdv: thm -> bool
23.6 val subst_typs: term -> typ -> typ -> term
23.7 - val pblterm: ThyC.domID -> Celem.pblID -> term
23.8 + val pblterm: ThyC.id -> Celem.pblID -> term
23.9 val subpbl: string -> string list -> term
23.10 val stacpbls: term -> term list
23.11 val op_of_calc: term -> string
24.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 15 11:37:43 2020 +0200
24.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 15 13:47:56 2020 +0200
24.3 @@ -148,7 +148,7 @@
24.4 in
24.5 case Specify.refine_ori oris pI of
24.6 SOME pblID =>
24.7 - Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.e_domID, Celem.e_metID, [](*filled in specify*)))
24.8 + Appl (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Celem.e_metID, [](*filled in specify*)))
24.9 | NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Tacitly pI)) ^ " not applicable")
24.10 end
24.11 | applicable_in (p, p_) pt (Tactic.Refine_Problem pI) =
24.12 @@ -160,7 +160,7 @@
24.13 PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
24.14 => (dI, dI', itms)
24.15 | _ => error "applicable_in Refine_Problem: uncovered case get_obj"
24.16 - val thy = if dI' = ThyC.e_domID then dI else dI';
24.17 + val thy = if dI' = ThyC.id_empty then dI else dI';
24.18 in
24.19 case Specify.refine_pbl (Celem.assoc_thy thy) pI itms of
24.20 NONE => Notappl ((Tactic.input_to_string (Tactic.Refine_Problem pI)) ^ " not applicable")
24.21 @@ -208,7 +208,7 @@
24.22 PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
24.23 => (oris, dI, pI, dI', pI', itms)
24.24 | _ => error "applicable_in Specify_Problem: uncovered case get_obj"
24.25 - val thy = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');
24.26 + val thy = Celem.assoc_thy (if dI' = ThyC.id_empty then dI else dI');
24.27 val {ppc, where_, prls, ...} = Specify.get_pbt pID;
24.28 val pbl = if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
24.29 then (false, (Generate.init_pbl ppc, []))
24.30 @@ -471,7 +471,7 @@
24.31 Frm => (get_obj g_form pt p , [])
24.32 | Res => get_obj g_result pt p
24.33 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
24.34 - val vp = (ThyC.thy2ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
24.35 + val vp = (ThyC.to_ctxt thy, pred) |-> TermC.parseNEW |> the |> mk_set thy pt p f;
24.36 in
24.37 Appl (Tactic.Check_elementwise' (f, pred, (f, asm)))
24.38 end
24.39 @@ -511,7 +511,7 @@
24.40 in
24.41 if id' <> "subproblem_equation_dummy"
24.42 then Notappl "no subproblem"
24.43 - else if (ThyC.thy2ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
24.44 + else if (ThyC.to_ctxt thy, f') |-> TermC.parseNEW |> the |> TermC.is_expliceq
24.45 then Appl (Tactic.Tac_ (thy, UnparseC.term f, id, "[" ^ f' ^ "]"))
24.46 else error ("applicable_in: f= " ^ f')
24.47 end
25.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 15 11:37:43 2020 +0200
25.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 15 13:47:56 2020 +0200
25.3 @@ -74,7 +74,7 @@
25.4
25.5 val reset_calchead : Calc.T -> Calc.T
25.6 val get_ocalhd : Calc.T -> Ctree.ocalhd
25.7 - val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.domID * Celem.pblID * Celem.metID -> bool
25.8 + val ocalhd_complete : Model.itm list -> (bool * term) list -> ThyC.id * Celem.pblID * Celem.metID -> bool
25.9 val all_modspec : Calc.T -> Calc.T
25.10
25.11 val complete_metitms : Model.ori list -> Model.itm list -> Model.itm list -> Celem.pat list -> Model.itm list
25.12 @@ -185,7 +185,7 @@
25.13 fun ocalhd_complete its pre (dI, pI, mI) =
25.14 foldl and_ (true, map #3 (its: Model.itm list)) andalso
25.15 foldl and_ (true, map #1 (pre: (bool * term) list)) andalso
25.16 - dI <> ThyC.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID
25.17 + dI <> ThyC.id_empty andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID
25.18
25.19 (* ["BOOL (1+x=2)","REAL x"] --match_ags--> oris
25.20 --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
25.21 @@ -359,18 +359,18 @@
25.22 (pbt, mpc) problem type, guard of method
25.23 *)
25.24 fun nxt_spec Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) =
25.25 - (if dI' = ThyC.e_domID andalso dI = ThyC.e_domID then (Pbl, Tactic.Specify_Theory dI')
25.26 + (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
25.27 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
25.28 else
25.29 case find_first (is_error o #5) pbl of
25.30 SOME (_, _, _, fd, itm_) =>
25.31 - (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_)
25.32 + (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
25.33 | NONE =>
25.34 - (case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl of
25.35 + (case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
25.36 SOME (fd, ct') => (Pbl, mk_additem fd ct')
25.37 | NONE => (*pbl-items complete*)
25.38 if not preok then (Pbl, Tactic.Refine_Problem pI')
25.39 - else if dI = ThyC.e_domID then (Pbl, Tactic.Specify_Theory dI')
25.40 + else if dI = ThyC.id_empty then (Pbl, Tactic.Specify_Theory dI')
25.41 else if pI = Celem.e_pblID then (Pbl, Tactic.Specify_Problem pI')
25.42 else if mI = Celem.e_metID then (Pbl, Tactic.Specify_Method mI')
25.43 else
25.44 @@ -382,12 +382,12 @@
25.45 | NONE => (Met, Tactic.Apply_Method mI))))
25.46 | nxt_spec Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
25.47 (case find_first (is_error o #5) met of
25.48 - SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_)
25.49 + SOME (_,_,_,fd,itm_) => (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
25.50 | NONE =>
25.51 - case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris mpc met of
25.52 + case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
25.53 SOME (fd,ct') => (Met, mk_additem fd ct')
25.54 | NONE =>
25.55 - (if dI = ThyC.e_domID then (Met, Tactic.Specify_Theory dI')
25.56 + (if dI = ThyC.id_empty then (Met, Tactic.Specify_Theory dI')
25.57 else if pI = Celem.e_pblID then (Met, Tactic.Specify_Problem pI')
25.58 else if not preok then (Met, Tactic.Specify_Method mI)
25.59 else (Met, Tactic.Apply_Method mI)))
25.60 @@ -649,7 +649,7 @@
25.61 fun overwrite_ppc thy itm ppc =
25.62 let
25.63 fun repl _ (_, _, _, _, itm_) [] =
25.64 - error ("overwrite_ppc: " ^ (Model.itm_2str_ (ThyC.thy2ctxt thy) itm_) ^ " not found")
25.65 + error ("overwrite_ppc: " ^ (Model.itm_2str_ (ThyC.to_ctxt thy) itm_) ^ " not found")
25.66 | repl ppc' itm (p :: ppc) =
25.67 if (#1 itm) = (#1 p)
25.68 then ppc' @ [itm] @ ppc
25.69 @@ -685,7 +685,7 @@
25.70 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
25.71 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
25.72 | _ => error "specify_additem: uncovered case of get_obj I pt p"
25.73 - val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
25.74 + val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
25.75 val cpI = if pI = Celem.e_pblID then pI' else pI
25.76 val cmI = if mI = Celem.e_metID then mI' else mI
25.77 val {ppc, pre, prls, ...} = Specify.get_met cmI
25.78 @@ -727,7 +727,7 @@
25.79 (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
25.80 => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
25.81 | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
25.82 - val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
25.83 + val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI
25.84 val cpI = if pI = Celem.e_pblID then pI' else pI
25.85 val cmI = if mI = Celem.e_metID then mI' else mI
25.86 val {ppc, where_, prls, ...} = Specify.get_pbt cpI
25.87 @@ -773,7 +773,7 @@
25.88 PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>
25.89 (oris, dI', pI', dI, pI, pbl, ctxt)
25.90 | _ => error "specify (Specify_Theory': uncovered case get_obj"
25.91 - val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
25.92 + val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
25.93 val cpI = if pI = Celem.e_pblID then pI' else pI;
25.94 in
25.95 case appl_add ctxt sel oris pbl ((#ppc o Specify.get_pbt) cpI) ct of
25.96 @@ -794,7 +794,7 @@
25.97 end
25.98 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
25.99 FIXME ..and dont abuse a tactic for that purpose*)
25.100 - ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
25.101 + ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),
25.102 (e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp)
25.103 end
25.104 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
25.105 @@ -803,7 +803,7 @@
25.106 PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
25.107 (oris, dI', mI', dI, mI, met, ctxt)
25.108 | _ => error "nxt_specif_additem Met: uncovered case get_obj"
25.109 - val thy = if dI = ThyC.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI;
25.110 + val thy = if dI = ThyC.id_empty then Celem.assoc_thy dI' else Celem.assoc_thy dI;
25.111 val cmI = if mI = Celem.e_metID then mI' else mI;
25.112 in
25.113 case appl_add ctxt sel oris met ((#ppc o Specify.get_met) cmI) ct of
25.114 @@ -873,7 +873,7 @@
25.115 in (pits, mits) end
25.116
25.117 fun some_spec (odI, opI, omI) (dI, pI, mI) =
25.118 - (if dI = ThyC.e_domID then odI else dI,
25.119 + (if dI = ThyC.id_empty then odI else dI,
25.120 if pI = Celem.e_pblID then opI else pI,
25.121 if mI = Celem.e_metID then omI else mI)
25.122
25.123 @@ -976,7 +976,7 @@
25.124 then error ("is_complete_spec: called by PrfObj at "^pos'2str pos)
25.125 else
25.126 let val (dI,pI,mI) = get_obj g_spec pt p
25.127 - in dI <> ThyC.e_domID andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID end
25.128 + in dI <> ThyC.id_empty andalso pI <> Celem.e_pblID andalso mI <> Celem.e_metID end
25.129
25.130 (* complete empty items in specification from origin (pbl, met ev.refined);
25.131 assumes 'is_complete_mod' *)
26.1 --- a/src/Tools/isac/Specify/generate.sml Wed Apr 15 11:37:43 2020 +0200
26.2 +++ b/src/Tools/isac/Specify/generate.sml Wed Apr 15 13:47:56 2020 +0200
26.3 @@ -338,7 +338,7 @@
26.4 let
26.5 val (pt, c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
26.6 (oris, (domID, pblID, metID), hdl, ctxt_specify)
26.7 - val f = Syntax.string_of_term (ThyC.thy2ctxt (Proof_Context.theory_of ctxt)) f
26.8 + val f = Syntax.string_of_term (ThyC.to_ctxt (Proof_Context.theory_of ctxt)) f
26.9 in
26.10 ((p, Pbl), c, FormKF f, pt)
26.11 end
27.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 15 11:37:43 2020 +0200
27.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 15 13:47:56 2020 +0200
27.3 @@ -140,7 +140,7 @@
27.4 in itm end
27.5 handle _ => (i, v, false, f, Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
27.6 | parsitm dI (itm as (_, _, _, _, Model.Par _)) =
27.7 - error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt dI) itm ^ "): Par should be internal");
27.8 + error ("parsitm (" ^ Model.itm2str_ (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
27.9
27.10 (*separate a list to a pair of elements that do NOT satisfy the predicate,
27.11 and of elements that satisfy the predicate, i.e. (false, true)*)
27.12 @@ -162,7 +162,7 @@
27.13 (* WN.9.11.03 copied from fun appl_add *)
27.14 fun appl_add' dI oris ppc pbt (sel, ct) =
27.15 let
27.16 - val ctxt = Celem.assoc_thy dI |> ThyC.thy2ctxt;
27.17 + val ctxt = Celem.assoc_thy dI |> ThyC.to_ctxt;
27.18 in
27.19 case TermC.parseNEW ctxt ct of
27.20 NONE => (0, [], false, sel, Model.Syn ct)
27.21 @@ -224,7 +224,7 @@
27.22 else oris2itms pbt vat os
27.23
27.24 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
27.25 - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm)
27.26 + | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm)
27.27 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
27.28 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
27.29 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
27.30 @@ -232,7 +232,7 @@
27.31 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
27.32 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
27.33 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
27.34 - error ("parsitm (" ^ Model.itm2str_ (ThyC.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
27.35 + error ("parsitm (" ^ Model.itm2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
27.36
27.37 fun imodel2fstr iitems =
27.38 let
28.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Apr 15 11:37:43 2020 +0200
28.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed Apr 15 13:47:56 2020 +0200
28.3 @@ -135,7 +135,7 @@
28.4 (* all mets of the respective theory PLUS of all ancestor theories*)
28.5 val fun_ids = mets |> map fun_id_of |> filter is_some |> map the
28.6 in
28.7 - filter (fn (str, _) => ThyC.thyID_of_derivation_name str = Context.theory_name thy) fun_ids
28.8 + filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids
28.9 end
28.10
28.11 type field = string * (term * term)
29.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 15 11:37:43 2020 +0200
29.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 15 13:47:56 2020 +0200
29.3 @@ -43,18 +43,18 @@
29.4 in
29.5 case p_ of
29.6 Pbl =>
29.7 - (if dI' = ThyC.e_domID andalso dI = ThyC.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
29.8 + (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
29.9 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
29.10 else
29.11 case find_first (is_error o #5) pbl of
29.12 SOME (_, _, _, fd, itm_) =>
29.13 - ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))
29.14 + ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
29.15 | NONE =>
29.16 - (case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl of
29.17 + (case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
29.18 SOME (fd, ct') => ("dummy", (Pbl, mk_additem fd ct'))
29.19 | NONE => (*pbl-items complete*)
29.20 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
29.21 - else if dI = ThyC.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
29.22 + else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
29.23 else if pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
29.24 else if mI = Celem.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))
29.25 else
29.26 @@ -66,12 +66,12 @@
29.27 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
29.28 | Met =>
29.29 (case find_first (is_error o #5) met of
29.30 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))
29.31 + SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
29.32 | NONE =>
29.33 - case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris mpc met of
29.34 + case nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
29.35 SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
29.36 | NONE =>
29.37 - (if dI = ThyC.e_domID then ("dummy", (Met, Tactic.Specify_Theory dI'))
29.38 + (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
29.39 else if pI = Celem.e_pblID then ("dummy", (Met, Tactic.Specify_Problem pI'))
29.40 else if not preok then ("dummy", (Met, Tactic.Specify_Method mI))
29.41 else ("dummy", (Met, Tactic.Apply_Method mI))))
30.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 15 11:37:43 2020 +0200
30.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 15 13:47:56 2020 +0200
30.3 @@ -76,7 +76,7 @@
30.4 PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
30.5 (dI, dI', probl, ctxt)
30.6 | _ => error "by_tactic_input Refine_Problem: uncovered case get_obj"
30.7 - val thy = if dI' = ThyC.e_domID then dI else dI'
30.8 + val thy = if dI' = ThyC.id_empty then dI else dI'
30.9 in
30.10 case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
30.11 NONE => ([], [], ptp)
30.12 @@ -93,7 +93,7 @@
30.13 PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
30.14 (oris, dI, dI', pI', probl, ctxt)
30.15 | _ => error ""
30.16 - val thy = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');
30.17 + val thy = Celem.assoc_thy (if dI' = ThyC.id_empty then dI else dI');
30.18 val {ppc,where_,prls,...} = Specify.get_pbt pI
30.19 val pbl =
30.20 if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
30.21 @@ -151,7 +151,7 @@
30.22 let (* either """"""""""""""" all empty or complete *)
30.23 val thy = Celem.assoc_thy dI'
30.24 val (oris, ctxt) =
30.25 - if dI' = ThyC.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
30.26 + if dI' = ThyC.id_empty orelse pI' = Celem.e_pblID (*andalso? WN110511*)
30.27 then ([], ContextC.empty)
30.28 else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
30.29 (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
30.30 @@ -170,7 +170,7 @@
30.31 PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
30.32 (oris, dI',pI',mI', dI, ctxt)
30.33 | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
30.34 - val thy' = if dI = ThyC.e_domID then dI' else dI
30.35 + val thy' = if dI = ThyC.id_empty then dI' else dI
30.36 val thy = Celem.assoc_thy thy'
30.37 val {ppc, prls, where_, ...} = Specify.get_pbt pI'
30.38 val pre = Stool.check_preconds thy prls where_ pbl
31.1 --- a/src/Tools/isac/TODO.thy Wed Apr 15 11:37:43 2020 +0200
31.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 15 13:47:56 2020 +0200
31.3 @@ -164,7 +164,7 @@
31.4 \end{itemize}
31.5 \item xxx
31.6 \item unify in signature LANGUAGE_TOOLS =\\
31.7 - val pblterm: ThyC.domID -> Celem.pblID -> term vvv vvv\\
31.8 + val pblterm: ThyC.id -> Celem.pblID -> term vvv vvv\\
31.9 val subpbl: string -> string list -> term unify with ^^^
31.10 \item xxx
31.11 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
32.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Wed Apr 15 11:37:43 2020 +0200
32.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Wed Apr 15 13:47:56 2020 +0200
32.3 @@ -4,6 +4,6 @@
32.4
32.5 ML_file "lucas_interpreter.sml"
32.6 ML \<open>
32.7 -(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.id * (theory' * rls)) list)*)
32.8 +(*val test_ruleset' = Unsynchronized.ref ([] : (Rule_Set.id * (ThyC.id * rls)) list)*)
32.9 \<close>
32.10 end
33.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 15 11:37:43 2020 +0200
33.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 15 13:47:56 2020 +0200
33.3 @@ -7,8 +7,8 @@
33.4 *)
33.5 signature KESTORE_ELEMS =
33.6 sig
33.7 - val get_rlss: theory -> (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list
33.8 - val add_rlss: (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list -> theory -> theory
33.9 + val get_rlss: theory -> (Rule_Set.id * (ThyC.id * Rule_Set.T)) list
33.10 + val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
33.11 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
33.12 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
33.13 (*etc*)
33.14 @@ -20,7 +20,7 @@
33.15
33.16 fun rls_eq ((id1, (thyID1, _)), (id2, (thyID2, _))) = id1 = id2 (*andalso thyID1 = thyID2*)
33.17 structure Data = Theory_Data (
33.18 - type T = (Rule_Set.id * (ThyC.theory' * Rule_Set.T)) list;
33.19 + type T = (Rule_Set.id * (ThyC.id * Rule_Set.T)) list;
33.20 val empty = [];
33.21 val extend = I;
33.22 val merge = merge rls_eq;
34.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 11:37:43 2020 +0200
34.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Wed Apr 15 13:47:56 2020 +0200
34.3 @@ -44,7 +44,7 @@
34.4 else error "calcelems.sml Thm.derivation_name changed 1";
34.5
34.6 val thmID = ThmC.cut_id dn;
34.7 -val thyID = ThyC.thyID_of_derivation_name dn;
34.8 +val thyID = ThyC.cut_id dn;
34.9 if thmID = "radd_0" andalso thyID = "Test" then ()
34.10 else error "calcelems.sml Thm.derivation_name changed 2";
34.11
34.12 @@ -52,7 +52,7 @@
34.13 val thm = @{thm add_divide_distrib}
34.14 val dn = Thm.derivation_name thm;
34.15 val thmID = ThmC.cut_id dn;
34.16 -val thyID = ThyC.thyID_of_derivation_name dn;
34.17 +val thyID = ThyC.cut_id dn;
34.18 if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()
34.19 else error "calcelems.sml Thm.derivation_name changed 3";
34.20
34.21 @@ -97,8 +97,8 @@
34.22 if ThmC.cut_id long_id = "mult_1_left" then ()
34.23 else error "fun ThmC.cut_id broken";
34.24
34.25 -if ThyC.thyID_of_derivation_name long_id = "Groups" then ()
34.26 -else error "fun ThyC.thyID_of_derivation_name broken";
34.27 +if ThyC.cut_id long_id = "Groups" then ()
34.28 +else error "fun ThyC.cut_id broken";
34.29
34.30 "-------- fun Rule_Set.merge -----------------------------------------------------";
34.31 "-------- fun Rule_Set.merge -----------------------------------------------------";
35.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Wed Apr 15 11:37:43 2020 +0200
35.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Wed Apr 15 13:47:56 2020 +0200
35.3 @@ -445,7 +445,7 @@
35.4 "----------- *** prep_pbt: syntax error in '#Where' of [v";
35.5 "===== deconstruct datatype typ ===";
35.6 val str = "?a";
35.7 - val t = (thy, str) |>> thy2ctxt
35.8 + val t = (thy, str) |>> ThyC.to_ctxt
35.9 |-> Proof_Context.read_term_pattern
35.10 |> ThmC_Def.num_to_Free;
35.11 val Var (("a", 0), ty) = t;
35.12 @@ -456,7 +456,7 @@
35.13
35.14 "----- real type in pattern ---";
35.15 val str = "?a :: real";
35.16 - val t = (thy, str) |>> thy2ctxt
35.17 + val t = (thy, str) |>> ThyC.to_ctxt
35.18 |-> Proof_Context.read_term_pattern
35.19 |> ThmC_Def.num_to_Free;
35.20 val Var (("a", 0), ty) = t;
35.21 @@ -473,7 +473,7 @@
35.22 val ctxt = Proof_Context.init_global thy;
35.23 val ctxt = Config.put show_types true ctxt;
35.24 "----- read_term_pattern ---";
35.25 -val t = (thy, str) |>> thy2ctxt
35.26 +val t = (thy, str) |>> ThyC.to_ctxt
35.27 |-> Proof_Context.read_term_pattern
35.28 |> ThmC_Def.num_to_Free;
35.29 val t_real = typ_a2real t;
35.30 @@ -488,7 +488,7 @@
35.31 "----------- check writeln, tracing for string markup ---";
35.32 val t = @{term "x + 1"};
35.33 val str_markup = (Syntax.string_of_term
35.34 - (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t;
35.35 + (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;
35.36 val str = UnparseC.term_by_thyID "Isac_Knowledge" t;
35.37
35.38 writeln "----------------writeln str_markup---";
35.39 @@ -526,7 +526,7 @@
35.40 "----------- check writeln, tracing for string markup ---";
35.41 val t = @{term "x + 1"};
35.42 val str_markup = (Syntax.string_of_term
35.43 - (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t;
35.44 + (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge"))) t;
35.45 val str = UnparseC.term_by_thyID "Isac_Knowledge" t;
35.46
35.47 writeln "----------------writeln str_markup---";
36.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 11:37:43 2020 +0200
36.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 15 13:47:56 2020 +0200
36.3 @@ -35,13 +35,13 @@
36.4 (*val thydata = get_the ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"];
36.5 (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
36.6 "~~~~~ fun get_the, args:"; val (theID:theID) = (["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]);
36.7 -(*get_py (Thy_Info_get_theory "Pure") theID theID (get_thes ());
36.8 +(*get_py (ThyC.get_theory "Pure") theID theID (get_thes ());
36.9 (* ERROR: get_pbt not found: ["IsacKnowledge","Test","Rulesets","ac_plus_times"] *)*)
36.10 (*default_print_depth 3; 999*)
36.11 (get_thes ());
36.12
36.13 -(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));*)
36.14 -"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((Thy_Info_get_theory "Pure"), theID, theID, (get_thes ()));
36.15 +(*"~~~~~ fun get_py, args:"; val (thy, d, _, []) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));*)
36.16 +"~~~~~ fun get_py, args:"; val (thy, d, _, [_]) = ((ThyC.get_theory "Pure"), theID, theID, (get_thes ()));
36.17 error ("get_pbt not found: "^(strs2str d));
36.18 (*AK110725 To be continued...s*)
36.19 *)
36.20 @@ -247,7 +247,7 @@
36.21
36.22 "----------- these are : string -> tac: ";
36.23 Calculate: string -> Tactic.input;; (* should be the operator*)
36.24 -Specify_Theory: domID -> Tactic.input;;
36.25 +Specify_Theory: ThyC.id -> Tactic.input;;
36.26 val tac = Specify_Theory("Differentiate");
36.27 xml_of_tac tac;(*
36.28 <SIMPLETACTIC name="Specify_Theory">
37.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml Wed Apr 15 11:37:43 2020 +0200
37.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml Wed Apr 15 13:47:56 2020 +0200
37.3 @@ -48,21 +48,21 @@
37.4 (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
37.5 Failed to parse term*)*)
37.6 "~~~~~ fun str2term, args:"; val (str) = (str);
37.7 -Thy_Info_get_theory "Isac_Knowledge";
37.8 +ThyC.get_theory "Isac_Knowledge";
37.9
37.10 parse_patt;
37.11 -parse_patt (Thy_Info_get_theory "Isac_Knowledge");
37.12 -(*parse_patt (Thy_Info_get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
37.13 +parse_patt (ThyC.get_theory "Isac_Knowledge");
37.14 +(*parse_patt (ThyC.get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
37.15 Failed to parse term*)*)
37.16
37.17 -"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac_Knowledge"), str);
37.18 +"~~~~~ fun parse_patt, args:"; val (thy, str) = ((ThyC.get_theory "Isac_Knowledge"), str);
37.19 (thy, str)
37.20 -|>> thy2ctxt
37.21 +|>> ThyC.to_ctxt
37.22 (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
37.23 Failed to parse term*)*)
37.24
37.25 Proof_Context.read_term_pattern;
37.26 -(@{theory "Isac_Knowledge"}, str) |>> thy2ctxt;
37.27 +(@{theory "Isac_Knowledge"}, str) |>> ThyC.to_ctxt;
37.28 "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
37.29 (*AK110725 To be continued...*)
37.30 *)
38.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 15 11:37:43 2020 +0200
38.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Wed Apr 15 13:47:56 2020 +0200
38.3 @@ -144,7 +144,7 @@
38.4 "----- fun pbl2term ----------------------------------------------";
38.5 "----- fun pbl2term ----------------------------------------------";
38.6 (*see WN120405a.TODO.txt*)
38.7 -if UnparseC.term (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
38.8 +if UnparseC.term (pbl2term (ThyC.get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
38.9 "Problem (Isac_Knowledge', [normalise, univariate, equations])"
38.10 then () else error "fun pbl2term changed";
38.11
39.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 11:37:43 2020 +0200
39.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Wed Apr 15 13:47:56 2020 +0200
39.3 @@ -188,8 +188,8 @@
39.4 "----------- fun thms_of_rlss ------------------------------------";
39.5 "----------- fun thms_of_rlss ------------------------------------";
39.6 val rlss =
39.7 - [("empty" : Rule_Set.id, ("KEStore": theory', Rule_Set.empty)),
39.8 - ("discard_minus" : Rule_Set.id, ("Poly": theory', discard_minus))]
39.9 + [("empty" : Rule_Set.id, ("KEStore": ThyC.id, Rule_Set.empty)),
39.10 + ("discard_minus" : Rule_Set.id, ("Poly": ThyC.id, discard_minus))]
39.11 ;
39.12 val [_, (thmID, term)] = thms_of_rlss thy rlss;
39.13 (*
39.14 @@ -198,7 +198,7 @@
39.15 *)
39.16 ;
39.17 "~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
39.18 -val rlss' = (rlss : (Rule_Set.id * (theory' * Rule_Set.T)) list)
39.19 +val rlss' = (rlss : (Rule_Set.id * (ThyC.id * Rule_Set.T)) list)
39.20 |> map (thms_of_rls o #2 o #2)
39.21 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),
39.22 Thm ("sym_real_mult_minus1", "- ?z1 = -1 * ?z1")]]*)
39.23 @@ -287,7 +287,7 @@
39.24
39.25 val rlsthmsNOTisac = isacrlsthms (*length = 2*)
39.26 |> filter (fn (deriv, _) =>
39.27 - member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
39.28 + member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
39.29 ;
39.30 val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
39.31 ;
40.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 15 11:37:43 2020 +0200
40.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 15 13:47:56 2020 +0200
40.3 @@ -91,7 +91,7 @@
40.4 Iterator 1;
40.5 moveActiveRoot 1;
40.6 refFormula 1 (get_pos 1 1);
40.7 -(*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
40.8 +(*WN.040222: stoert das sehr, dass ThyC.id_empty etc. statt leer kommt ???*)
40.9 DEconstrCalcTree 1;
40.10
40.11 "--------- solve_linear as rootpbl FE -------------------";
40.12 @@ -585,7 +585,7 @@
40.13 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
40.14 refFormula 1 (get_pos 1 1);
40.15 val ((pt,_),_) = get_calc 1;
40.16 - if get_obj g_spec pt [] = ("e_domID",
40.17 + if get_obj g_spec pt [] = ("thy_empty_id",
40.18 ["LINEAR", "univariate","equation","test"],
40.19 ["Test","solve_linear"]) then ()
40.20 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
40.21 @@ -925,7 +925,7 @@
40.22 loc = (SOME scrst_ctxt, NONE),
40.23 ctxt,
40.24 meth,
40.25 - spec = ("e_domID", ["e_pblID"], ["e_metID"]),
40.26 + spec = ("thy_empty_id", ["e_pblID"], ["e_metID"]),
40.27 probl,
40.28 branch = TransitiveB,
40.29 origin,
40.30 @@ -1530,7 +1530,7 @@
40.31 "--------- UC errpat add-fraction, fillpat by input --------------";
40.32 "--------- UC errpat add-fraction, fillpat by input --------------";
40.33 (*cp from BridgeLog Java <=> SML*)
40.34 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
40.35 +CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
40.36 Iterator 1;
40.37 moveActiveRoot 1;
40.38 moveActiveFormula 1 ([],Pbl);
41.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 11:37:43 2020 +0200
41.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 15 13:47:56 2020 +0200
41.3 @@ -414,7 +414,7 @@
41.4 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
41.5 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
41.6 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
41.7 - if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
41.8 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
41.9
41.10 (*there is one input to the model (could be more)*)
41.11 val (b,pt,ocalhd) =
41.12 @@ -422,7 +422,7 @@
41.13 Find ["maximum", "valuesFor"],
41.14 Relate ["relations"]], Pbl, e_spec);
41.15 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
41.16 - if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
41.17 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
41.18 else error "informtest.sml: diff.behav. max 2";
41.19
41.20 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
41.21 @@ -471,7 +471,7 @@
41.22 "--------- CAS-command on ([],Pbl) -------------------------------";
41.23 "--------- CAS-command on ([],Pbl) -------------------------------";
41.24 val (p,_,f,nxt,_,pt) =
41.25 - CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
41.26 + CalcTreeTEST [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
41.27 val ifo = "solve(x+1=2,x)";
41.28 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
41.29 show_pt pt;
41.30 @@ -485,7 +485,7 @@
41.31 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
41.32 "--------- CAS-command on ([],Pbl) FE-interface ------------------";
41.33 reset_states ();
41.34 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
41.35 +CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
41.36 Iterator 1;
41.37 moveActiveRoot 1;
41.38 replaceFormula 1 "solve(x+1=2,x)";
41.39 @@ -636,7 +636,7 @@
41.40 atomty t;
41.41 "-----------------------------------------------------------------";
41.42 (*1>*)reset_states ();
41.43 -(*2>*)CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
41.44 +(*2>*)CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
41.45 (*3>*)Iterator 1;moveActiveRoot 1;
41.46 "----- here the Headline has been finished";
41.47 (*4>*)moveActiveFormula 1 ([],Pbl);
41.48 @@ -738,7 +738,7 @@
41.49 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
41.50 "--------- implicit_take, start with <NEW> (CAS input) ---------------";
41.51 reset_states ();
41.52 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
41.53 +CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
41.54 (*[[from sml: > @@@@@begin@@@@@
41.55 [[from sml: 1
41.56 [[from sml: <CALCTREE>
41.57 @@ -800,7 +800,7 @@
41.58 [[from sml: </POSITION>
41.59 [[from sml: <HEAD>
41.60 [[from sml: <MATHML>
41.61 -[[from sml: <ISA> Problem (e_domID, [e_pblID]) </ISA>
41.62 +[[from sml: <ISA> Problem (ThyC.id_empty, [e_pblID]) </ISA>
41.63 [[from sml: </MATHML>
41.64 [[from sml: </HEAD>
41.65 [[from sml: <MODEL>
41.66 @@ -811,7 +811,7 @@
41.67 [[from sml: </MODEL>
41.68 [[from sml: <BELONGSTO> Pbl </BELONGSTO>
41.69 [[from sml: <SPECIFICATION>
41.70 -[[from sml: <THEORYID> e_domID </THEORYID>
41.71 +[[from sml: <THEORYID> ThyC.id_empty </THEORYID>
41.72 [[from sml: <PROBLEMID>
41.73 [[from sml: <STRINGLIST>
41.74 [[from sml: <STRING> e_pblID </STRING>
41.75 @@ -1210,7 +1210,7 @@
41.76 val pos = get_pos cI 1;
41.77
41.78 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
41.79 - val SOME ifo = parseNEW (assoc_thy "Isac_Knowledge" |> thy2ctxt) istr
41.80 + val SOME ifo = parseNEW (assoc_thy "Isac_Knowledge" |> ThyC.to_ctxt) istr
41.81 val p' = lev_on p;
41.82 val tac = get_obj g_tac pt p';
41.83 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
42.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 11:37:43 2020 +0200
42.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 15 13:47:56 2020 +0200
42.3 @@ -199,7 +199,7 @@
42.4 "~~~~~ fun specific_from_prog , args:"; val (pt, (p, p_)) = (pt, p);
42.5 Pos.on_specification p_ = false;
42.6 val pp = par_pblobj pt p
42.7 - val thy' = (get_obj g_domID pt pp):theory'
42.8 + val thy' = (get_obj g_domID pt pp):ThyC.id
42.9 val thy = assoc_thy thy'
42.10 val metID = get_obj g_metID pt pp
42.11 val metID' =
43.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Apr 15 11:37:43 2020 +0200
43.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Apr 15 13:47:56 2020 +0200
43.3 @@ -41,7 +41,7 @@
43.4 else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
43.5 ;
43.6 "~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
43.7 - val thy = Thy_Info_get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
43.8 + val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
43.9 val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
43.10 val SOME (thy'', _) = xxx;
43.11 val SOME ("Poly", _) = xxx;
43.12 @@ -50,20 +50,20 @@
43.13 if partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
43.14 ;
43.15 "~~~~~ fun partID', args:"; val (thy') = (thy');
43.16 -Thy_Info_get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
43.17 +ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
43.18 ;
43.19 -"~~~~~ fun partID, args:"; val (thy) = (Thy_Info_get_theory thy');
43.20 +"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
43.21 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
43.22 knowthys ()
43.23 ;
43.24 "~~~~~ fun knowthys , args:"; val () = ();
43.25 val allthys = filter_out (member Context.eq_thy
43.26 - [(*Thy_Info_get_theory "ProgLang",*) Thy_Info_get_theory "Interpret",
43.27 - Thy_Info_get_theory "MathEngine", Thy_Info_get_theory "BridgeLibisabelle"])
43.28 - (Theory.ancestors_of (Thy_Info_get_theory "Build_Thydata"));
43.29 + [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
43.30 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
43.31 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
43.32 length allthys = 152; (*in Isabelle2015/Isac*)
43.33 (*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
43.34 -Thy_Info_get_theory "Complex_Main";*)
43.35 +ThyC.get_theory "Complex_Main";*)
43.36 Thy_Info.get_theory "Complex_Main";;
43.37
43.38 "----------- apply thy_containing_rls -------------------";
44.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Apr 15 11:37:43 2020 +0200
44.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Wed Apr 15 13:47:56 2020 +0200
44.3 @@ -27,7 +27,7 @@
44.4 "-----------------------------------------------------------------";
44.5
44.6 val thy = @{theory "Biegelinie"};
44.7 -val ctxt = ThyC.thy2ctxt' "Biegelinie";
44.8 +val ctxt = ThyC.id_to_ctxt "Biegelinie";
44.9 fun str2term str = (Thm.term_of o the o (parse thy)) str;
44.10 fun term2s t = UnparseC.term_by_thyID "Biegelinie" t;
44.11 fun rewrit thm str = fst (the (rewrite_ thy tless_true Rule_Set.empty true thm str));
45.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 15 11:37:43 2020 +0200
45.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 15 13:47:56 2020 +0200
45.3 @@ -237,7 +237,7 @@
45.4 (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
45.5 val {ppc, pre, prls,...} = Specify.get_met mID
45.6 val thy = Celem.assoc_thy dI
45.7 - val dI'' = if dI = ThyC.e_domID then dI' else dI
45.8 + val dI'' = if dI = ThyC.id_empty then dI' else dI
45.9 val pI'' = if pI = Celem.e_pblID then pI' else pI
45.10 ;
45.11 (*+*)writeln (oris2str oris); (*[
46.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Wed Apr 15 11:37:43 2020 +0200
46.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Wed Apr 15 13:47:56 2020 +0200
46.3 @@ -57,7 +57,7 @@
46.4 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
46.5 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
46.6 |> filter (fn (deriv, _) =>
46.7 - member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
46.8 + member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
46.9 : (ThmC.id * thm) list
46.10 ;
46.11 (*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
47.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 15 11:37:43 2020 +0200
47.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Apr 15 13:47:56 2020 +0200
47.3 @@ -460,7 +460,7 @@
47.4 =========================================================================/
47.5
47.6 -----fun refin' ff:
47.7 -> (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) itms;
47.8 +> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
47.9 [
47.10 (1 ,[1] ,true ,#Given ,Cor equalities
47.11 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
47.12 @@ -475,7 +475,7 @@
47.13 (true, length_ [c, c_2] = 2)]
47.14
47.15 ----- fun match_oris':
47.16 -> (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) itms;
47.17 +> (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) itms;
47.18 > (writeln o pres2str) pre';
47.19 ..as in refin'
47.20
47.21 @@ -542,7 +542,7 @@
47.22
47.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
47.24 val PblObj {probl,...} = get_obj I pt [5];
47.25 - (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl;
47.26 + (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
47.27 (*[
47.28 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
47.29 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
47.30 @@ -610,7 +610,7 @@
47.31
47.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
47.33 val PblObj {probl,...} = get_obj I pt [5];
47.34 - (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl;
47.35 + (writeln o (itms2str_ (ThyC.to_ctxt @{theory Isac_Knowledge}))) probl;
47.36 (*[
47.37 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
47.38 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
48.1 --- a/test/Tools/isac/Knowledge/equation.sml Wed Apr 15 11:37:43 2020 +0200
48.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Apr 15 13:47:56 2020 +0200
48.3 @@ -18,7 +18,7 @@
48.4 "----------- CAS input -------------------------------------------";
48.5 "----------- CAS input -------------------------------------------";
48.6 reset_states ();
48.7 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
48.8 +CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
48.9 Iterator 1;
48.10 moveActiveRoot 1;
48.11 replaceFormula 1 "solve (x+1=2, x)";
49.1 --- a/test/Tools/isac/Knowledge/inssort.sml Wed Apr 15 11:37:43 2020 +0200
49.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Apr 15 13:47:56 2020 +0200
49.3 @@ -119,7 +119,7 @@
49.4 "----------- insertion sort: CAS-command -------------------------------------";
49.5 "----------- insertion sort: CAS-command -------------------------------------";
49.6 "----------- insertion sort: CAS-command -------------------------------------";
49.7 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
49.8 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
49.9 val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt, p) "Sort {||1, 3, 2||}";
49.10 show_pt pt;
49.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method",..*)
50.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Apr 15 11:37:43 2020 +0200
50.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Apr 15 13:47:56 2020 +0200
50.3 @@ -24,7 +24,7 @@
50.4 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
50.5 they are used several times below; TODO remove duplicates*)
50.6 val thy = @{theory "Integrate"};
50.7 -val ctxt = thy2ctxt thy;
50.8 +val ctxt = ThyC.to_ctxt thy;
50.9
50.10 fun str2t str = parseNEW ctxt str |> the;
50.11 fun term2s t = UnparseC.term_in_ctxt ctxt t;
51.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Apr 15 11:37:43 2020 +0200
51.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Apr 15 13:47:56 2020 +0200
51.3 @@ -143,7 +143,7 @@
51.4 val (f,asm) = case p_ of Frm => (get_obj g_form pt p , [])
51.5 | Res => get_obj g_result pt p;
51.6 UnparseC.term f = "[x = 1 / 5]"; (*the current formula*)
51.7 - val vp = (thy2ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
51.8 + val vp = (ThyC.to_ctxt thy, pred) |-> parseNEW |> the |> mk_set thy pt p f;
51.9 val (bdv, asms) = vp;
51.10
51.11 UnparseC.term bdv = "x";
52.1 --- a/test/Tools/isac/Knowledge/simplify.sml Wed Apr 15 11:37:43 2020 +0200
52.2 +++ b/test/Tools/isac/Knowledge/simplify.sml Wed Apr 15 13:47:56 2020 +0200
52.3 @@ -23,7 +23,7 @@
52.4 "----------- CAS-command Simplify -----------------------";
52.5 "----------- CAS-command Simplify -----------------------";
52.6 reset_states ();
52.7 -CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
52.8 +CalcTree [([], ("thy_empty_id", ["e_pblID"], ["e_metID"]))];
52.9 Iterator 1;
52.10 moveActiveRoot 1;
52.11 replaceFormula 1 "Simplify (2*a + 3*a)";
53.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 15 11:37:43 2020 +0200
53.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Wed Apr 15 13:47:56 2020 +0200
53.3 @@ -69,7 +69,7 @@
53.4 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
53.5 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
53.6 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
53.7 -val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
53.8 +val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
53.9 val cpI = if pI = e_pblID then pI' else pI;
53.10 val ctxt = get_ctxt pt (p, Pbl);
53.11 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
54.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 11:37:43 2020 +0200
54.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Wed Apr 15 13:47:56 2020 +0200
54.3 @@ -69,7 +69,7 @@
54.4 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
54.5 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
54.6 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
54.7 -val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
54.8 +val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
54.9 val cpI = if pI = e_pblID then pI' else pI;
54.10 val ctxt = get_ctxt pt (p, Pbl);
54.11 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);
55.1 --- a/test/Tools/isac/MathEngBasic/tactic.sml Wed Apr 15 11:37:43 2020 +0200
55.2 +++ b/test/Tools/isac/MathEngBasic/tactic.sml Wed Apr 15 13:47:56 2020 +0200
55.3 @@ -18,7 +18,7 @@
55.4 val thm'' = ("real_mult_div_cancel2", @{thm real_mult_div_cancel2});
55.5 val (f, res) = (@{term "a * x / (b * x) :: real"}, (@{term "a / b :: real"}, [@{term "k \<noteq> (0 :: real)"}]: term list))
55.6 ;
55.7 -Rewrite': theory' * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * result -> Tactic.T;
55.8 +Rewrite': ThyC.id * Rule_Def.rew_ord' * Rule_Set.T * bool * ThmC.T * term * result -> Tactic.T;
55.9 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res)
55.10 ;
55.11 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED";
56.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 11:37:43 2020 +0200
56.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 15 13:47:56 2020 +0200
56.3 @@ -163,9 +163,9 @@
56.4 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
56.5
56.6 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
56.7 -dI = e_domID; (*true*)
56.8 +dI = ThyC.id_empty; (*true*)
56.9 odI = "Build_Inverse_Z_Transform"; (*true*)
56.10 -dI = "e_domID"; (*true*)
56.11 +dI = "thy_empty_id"; (*true*)
56.12 "~~~~~ after fun some_spec:";
56.13 val (dI, pI, mI) = some_spec ospec spec;
56.14 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
57.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 15 11:37:43 2020 +0200
57.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Wed Apr 15 13:47:56 2020 +0200
57.3 @@ -46,14 +46,14 @@
57.4 (p_, pb, oris, (dI',pI',mI'), (probl, meth),
57.5 (ppc, (#ppc o get_met) cmI), (dI, pI, mI));
57.6
57.7 -dI' = e_domID andalso dI = e_domID; (* = false*)
57.8 +dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
57.9 pI' = e_pblID andalso pI = e_pblID; (* = false*)
57.10 find_first (is_error o #5) (pbl:itm list); (* = NONE*)
57.11
57.12 -(* nxt_add (assoc_thy (if dI = e_domID then dI' else dI)) oris pbt pbl;
57.13 +(* nxt_add (assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
57.14 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
57.15 "~~~~~ fun nxt_add, args:"; val (thy, oris, pbt, itms) =
57.16 - ((assoc_thy (if dI = e_domID then dI' else dI)), oris, pbt, pbl);
57.17 + ((assoc_thy (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
57.18 local infix mem;
57.19 fun x mem [] = false
57.20 | x mem (y :: ys) = x = y orelse x mem ys;
58.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 15 11:37:43 2020 +0200
58.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Wed Apr 15 13:47:56 2020 +0200
58.3 @@ -30,7 +30,7 @@
58.4 > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
58.5 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
58.6 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
58.7 -> Syntax.string_of_term (thy2ctxt thy) t';
58.8 +> Syntax.string_of_term (ThyC.to_ctxt thy) t';
58.9 *)
58.10 (******************************************************************)
58.11 (* ------------------------------------- *)
58.12 @@ -276,15 +276,15 @@
58.13 val pt = update_met pt [] [];
58.14 (*
58.15 > get_obj g_spec pt [];
58.16 -val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec
58.17 +val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec
58.18 > val pt = update_domID pt [] "RatArith";
58.19 > get_obj g_spec pt [];
58.20 -val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec
58.21 +val it = ("RatArith",["e_pblID"],("thy_empty_id","e_metID")) : spec
58.22 > val pt = update_pblID pt [] ["RatArith",
58.23 "equations","univariate","square-root"];
58.24 > get_obj g_spec pt [];
58.25 ("RatArith",["RatArith","equations","univariate","square-root"],
58.26 - ("e_domID","e_metID")) : spec
58.27 + ("thy_empty_id","e_metID")) : spec
58.28 > val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
58.29 > get_obj g_spec pt [];
58.30 ("RatArith",["RatArith","equations","univariate","square-root"],
58.31 @@ -413,7 +413,7 @@
58.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
58.33 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
58.34 > get_obj g_spec pt (fst p);
58.35 -val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
58.36 +val it = ("thy_empty_id",["e_pblID"],("thy_empty_id","e_metID")) : spec*)
58.37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
58.38 (*val nxt = ("Specify_Problem", Specify_Problem *)
58.39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
59.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Apr 15 11:37:43 2020 +0200
59.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Apr 15 13:47:56 2020 +0200
59.3 @@ -92,19 +92,19 @@
59.4 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
59.5 loc_2str l1;
59.6 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
59.7 -Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t1;
59.8 +Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t1;
59.9 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
59.10
59.11 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
59.12 loc_2str l2;
59.13 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
59.14 -Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t2;
59.15 +Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t2;
59.16 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
59.17
59.18 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
59.19 loc_2str l3;
59.20 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
59.21 -Syntax.string_of_term (ThyC.thy2ctxt' "DiffApp") t3;
59.22 +Syntax.string_of_term (ThyC.id_to_ctxt "DiffApp") t3;
59.23 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
59.24
59.25
60.1 --- a/test/Tools/isac/Specify/appl.sml Wed Apr 15 11:37:43 2020 +0200
60.2 +++ b/test/Tools/isac/Specify/appl.sml Wed Apr 15 13:47:56 2020 +0200
60.3 @@ -73,7 +73,7 @@
60.4 "~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
60.5 val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
60.6 probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
60.7 -val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
60.8 +val thy = if dI = ThyC.id_empty then assoc_thy dI' else assoc_thy dI;
60.9 val cpI = if pI = e_pblID then pI' else pI;
60.10 val ctxt = get_ctxt pt (p, Pbl);
60.11 oris; (*= [(1, [1], "#Given", Const ("Input_Descript.equality", "HOL.bool...*)
61.1 --- a/test/Tools/isac/Specify/calchead.sml Wed Apr 15 11:37:43 2020 +0200
61.2 +++ b/test/Tools/isac/Specify/calchead.sml Wed Apr 15 13:47:56 2020 +0200
61.3 @@ -234,7 +234,7 @@
61.4 EmptyPtree;
61.5 val nxt = tac2tac_ pt p nxt;
61.6 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
61.7 -(*val nxt = Specify_Theory "e_domID" : tac*)
61.8 +(*val nxt = Specify_Theory "thy_empty_id" : tac*)
61.9
61.10 val nxt = Specify_Theory "DiffApp";
61.11 val nxt = tac2tac_ pt p nxt;
61.12 @@ -275,7 +275,7 @@
61.13 val nxt = Add_Relation "relations [(A=a+b)]";
61.14 val nxt = tac2tac_ pt p nxt;
61.15 val(p,_, PpcKF ppc, nxt,_,pt) = specify nxt p [] pt;
61.16 -(*val nxt = Specify_Method ("e_domID","e_metID") : tac*)
61.17 +(*val nxt = Specify_Method ("thy_empty_id","e_metID") : tac*)
61.18
61.19 val nxt = Specify_Method ["DiffApp","max_by_calculus"];
61.20 val nxt = tac2tac_ pt p nxt;
61.21 @@ -689,7 +689,7 @@
61.22 loc =
61.23 (Some (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
61.24 None),
61.25 - cell = None, meth = [], spec = ("e_domID", ["e_pblID"], ["e_metID"]),
61.26 + cell = None, meth = [], spec = ("thy_empty_id", ["e_pblID"], ["e_metID"]),
61.27 probl = [], branch = TransitiveB,
61.28 origin =
61.29 ([(1, [1], "#Given",
61.30 @@ -751,7 +751,7 @@
61.31 (Pstate ([], [], None, Const ("empty", "'a"), Sundef, false)),
61.32 None),
61.33 cell = None, meth = [], spec =
61.34 - ("e_domID", ["e_pblID"], ["e_metID"]), probl =
61.35 + ("thy_empty_id", ["e_pblID"], ["e_metID"]), probl =
61.36 [(0, [], false, "#Given",
61.37 Inc ((Const ("Input_Descript.functionTerm",
61.38 "Real.real => Tools.una"),[]),
62.1 --- a/test/Tools/isac/Specify/step-specify.sml Wed Apr 15 11:37:43 2020 +0200
62.2 +++ b/test/Tools/isac/Specify/step-specify.sml Wed Apr 15 13:47:56 2020 +0200
62.3 @@ -27,7 +27,7 @@
62.4 pt;(*isa==REP*)
62.5 val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
62.6 = get_obj g_origin pt (fst p);
62.7 -get_obj g_spec pt (fst p) = ("e_domID", ["e_pblID"], ["e_metID"]); (*isa==REP*)
62.8 +get_obj g_spec pt (fst p) = ("thy_empty_id", ["e_pblID"], ["e_metID"]); (*isa==REP*)
62.9
62.10 (*this steps into according to "----- step 2 ---" below*)
62.11 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
62.12 @@ -68,12 +68,12 @@
62.13 "~~~~~ fun nxt_spec , args:"; val (Pbl, preok, oris, (dI', pI', mI'), (pbl, met), (pbt, mpc), (dI, pI, mI))
62.14 (* vv----^^*)
62.15 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Specify.get_met) cmI), (dI, pI, mI));
62.16 - (*if*) dI' = ThyC.e_domID andalso dI = ThyC.e_domID (*else*);
62.17 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
62.18 (*if*) pI' = Celem.e_pblID andalso pI = Celem.e_pblID (*else*);
62.19 val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
62.20 - val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl (*of*);
62.21 + val NONE = (*case*) nxt_add (Celem.assoc_thy (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
62.22 (*if*) not preok (*else*);
62.23 - (*if*) dI = ThyC.e_domID (*then*);
62.24 + (*if*) dI = ThyC.id_empty (*then*);
62.25
62.26 (Pbl, Tactic.Specify_Theory dI') (*return from nxt_spec*);
62.27 "~~~~~ from fun nxt_spec\<longrightarrow>fun nxt_specify_, return:"; val (_, tac)