1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 14:36:27 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 16:01:53 2020 +0200
1.3 @@ -117,7 +117,7 @@
1.4 fun add_pbts pbts thy = let
1.5 fun add_pbt (pbt as {guh,...}, pblID) =
1.6 (* the pblID has the leaf-element as first; better readability achieved *)
1.7 - (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
1.8 + (if (!Check_Unique.on) then Probl_Def.check_unique guh (Data.get thy) else ();
1.9 rev pblID |> Store.insert pblID pbt);
1.10 in Data.map (fold add_pbt pbts) thy end;
1.11
1.12 @@ -130,7 +130,7 @@
1.13 val get_mets = Data.get;
1.14 fun add_mets mets thy = let
1.15 fun add_met (met as {guh,...}, metID) =
1.16 - (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
1.17 + (if (!Check_Unique.on) then Meth_Def.check_unique guh (Data.get thy) else ();
1.18 Store.insert metID met metID);
1.19 in Data.map (fold add_met mets) thy end;
1.20
2.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml Wed Apr 22 14:36:27 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml Wed Apr 22 16:01:53 2020 +0200
2.3 @@ -4,16 +4,19 @@
2.4
2.5 Check entries to Know_Store unique.
2.6 This is legacy code; check runs on #guh.
2.7 +
2.8 +"guh" stands for "globally unique handle" -- over all of the internet,
2.9 +the last remaining code from Klaus Schmaranz's Dinopolis Project.
2.10 *)
2.11 signature CHECK_UNIQUE =
2.12 sig
2.13 -(*type switch *)
2.14 - type guh
2.15 -(*val on *)
2.16 - val check_guhs_unique: bool Unsynchronized.ref
2.17 +(*type guh *)
2.18 + type id
2.19 +(*val check_guhs_unique *)
2.20 + val on: bool Unsynchronized.ref
2.21 (*val collect *)
2.22 val collect: ('a -> 'b) -> 'a Store.T -> 'b list;
2.23 - val message: ('a -> guh list) -> guh -> 'a -> unit;
2.24 + val message: ('a -> id list) -> id -> 'a -> unit;
2.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.26 (*NONE*)
2.27 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.28 @@ -26,16 +29,12 @@
2.29 struct
2.30 (**)
2.31
2.32 -(*
2.33 - the last remaining code from Klaus Schmaranz's Dinopolis Project:
2.34 - guh stands for "globally unique handle" -- over all of the internet.
2.35 -*)
2.36 -type guh = string;
2.37 +type id = string;
2.38
2.39 (* switch for checking guhs unique before storing a pbl or met;
2.40 set true at startup (done at begin of ROOT.ML)
2.41 set false for editing Isac_Knowledge (done at end of ROOT.ML) *)
2.42 -val check_guhs_unique = Unsynchronized.ref true;
2.43 +val on = Unsynchronized.ref true;
2.44
2.45 fun collect select_guh pbls =
2.46 let
2.47 @@ -45,9 +44,9 @@
2.48 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
2.49 in nodes [] pbls end;
2.50
2.51 -fun message select guh store =
2.52 - if member op = (select store) guh
2.53 - then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
2.54 +fun message select id store =
2.55 + if member op = (select store) id
2.56 + then error ("Check_Unique failed with \"" ^ id ^ "\";\n" ^
2.57 "use \"sort_guhs()\" for a list of guhs;\n" ^
2.58 "consider setting \"Check_Unique.on := false\"")
2.59 else ();
3.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Wed Apr 22 14:36:27 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Wed Apr 22 16:01:53 2020 +0200
3.3 @@ -18,8 +18,8 @@
3.4 (*type mets*)
3.5 val empty_store: T Store.node
3.6 (*val e_Mets: T Store.node*)
3.7 - val check_unique: Check_Unique.guh -> T Store.T -> unit
3.8 -(*val check_metguh_unique: Check_Unique.guh -> T Store.T -> unit*)
3.9 + val check_unique: Check_Unique.id -> T Store.T -> unit
3.10 +(*val check_metguh_unique: Check_Unique.id -> T Store.T -> unit*)
3.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.12 (*NONE*)
3.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.14 @@ -38,7 +38,7 @@
3.15
3.16 (* data for methods stored in 'methods'-database*)
3.17 type T =
3.18 - {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
3.19 + {guh : Check_Unique.id, (* unique within this isac-knowledge *)
3.20 mathauthors: string list, (* copyright *)
3.21 init : Spec.id, (* WN060721 pblID introduced mistakenly--TODO.REMOVE! *)
3.22 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
3.23 @@ -70,6 +70,6 @@
3.24 (*\------- to Celem6 -------/*)
3.25
3.26 val check_unique =
3.27 - Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.guh));
3.28 + Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));
3.29
3.30 (**)end(**)
4.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Wed Apr 22 14:36:27 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Wed Apr 22 16:01:53 2020 +0200
4.3 @@ -13,8 +13,8 @@
4.4 type T
4.5 (*val e_Ptyp: T Store.node*)
4.6 val empty_store: T Store.node
4.7 -(*val check_pblguh_unique: Check_Unique.guh -> T Store.T -> unit*)
4.8 - val check_unique: Check_Unique.guh -> T Store.T -> unit
4.9 +(*val check_pblguh_unique: Check_Unique.id -> T Store.T -> unit*)
4.10 + val check_unique: Check_Unique.id -> T Store.T -> unit
4.11
4.12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.13 (*type ptyps*)
4.14 @@ -38,7 +38,7 @@
4.15 val id_to_string = Spec.id_to_string;
4.16
4.17 type T =
4.18 - {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
4.19 + {guh : Check_Unique.id, (* unique within this isac-knowledge *)
4.20 mathauthors : string list, (* copyright *)
4.21 init : Spec.id, (* to start refinement with *)
4.22 thy : theory, (* which allows to compile that T
4.23 @@ -72,6 +72,6 @@
4.24 (*\------- to Celem5 -------/*)
4.25
4.26 val check_unique =
4.27 - Check_Unique.message (Check_Unique.collect (#guh : T -> Check_Unique.guh));
4.28 + Check_Unique.message (Check_Unique.collect (#guh : T -> Check_Unique.id));
4.29
4.30 (**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Wed Apr 22 14:36:27 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Wed Apr 22 16:01:53 2020 +0200
5.3 @@ -8,25 +8,25 @@
5.4 sig
5.5 type authors
5.6 datatype thydata
5.7 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors}
5.8 - | Hord of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
5.9 - | Hrls of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
5.10 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.guh, mathauthors: authors, thm: thm}
5.11 - | Html of {coursedesign: authors, guh: Check_Unique.guh, html: string, mathauthors: authors}
5.12 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.id, mathauthors: authors}
5.13 + | Hord of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
5.14 + | Hrls of {coursedesign: authors, guh: Check_Unique.id, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
5.15 + | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.id, mathauthors: authors, thm: thm}
5.16 + | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}
5.17 type theID
5.18 val theID2str: string list -> string
5.19 val the2str: thydata -> string
5.20 val thes2str: thydata list -> string
5.21 val theID2thyID: theID -> ThyC.id
5.22
5.23 - val part2guh: theID -> Check_Unique.guh
5.24 - val thy2guh: theID -> Check_Unique.guh
5.25 - val thypart2guh: theID -> Check_Unique.guh
5.26 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
5.27 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
5.28 - val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
5.29 - val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
5.30 - val theID2guh: theID -> Check_Unique.guh
5.31 + val part2guh: theID -> Check_Unique.id
5.32 + val thy2guh: theID -> Check_Unique.id
5.33 + val thypart2guh: theID -> Check_Unique.id
5.34 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.id
5.35 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.id
5.36 + val cal2guh: string * ThyC.id -> string -> Check_Unique.id
5.37 + val ord2guh: string * ThyC.id -> string -> Check_Unique.id
5.38 + val theID2guh: theID -> Check_Unique.id
5.39
5.40 val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
5.41 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
5.42 @@ -53,12 +53,12 @@
5.43 (* datatype for collecting thydata for hierarchy *)
5.44 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
5.45 datatype thydata =
5.46 - Html of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, html: string}
5.47 -| Hthm of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
5.48 + Html of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, html: string}
5.49 +| Hthm of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
5.50 thm: thm} (* here no sym_thm, thus no thmID required *)
5.51 -| Hrls of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
5.52 -| Hcal of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
5.53 -| Hord of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors,
5.54 +| Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
5.55 +| Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
5.56 +| Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
5.57 ord: (UnparseC.subst -> (term * term) -> bool)};
5.58 fun the2str (Html {guh, ...}) = guh
5.59 | the2str (Hthm {guh, ...}) = guh
5.60 @@ -83,7 +83,7 @@
5.61 type thehier = (thydata Store.node) list;
5.62 (* required to determine sequence of main nodes of thehier in Know_Store.thy *)
5.63 fun part2guh [str] = (case str of
5.64 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.guh
5.65 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.id
5.66 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
5.67 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
5.68 | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
5.69 @@ -97,7 +97,7 @@
5.70 | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
5.71
5.72 fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
5.73 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.guh
5.74 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.id
5.75 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
5.76 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
5.77 | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
5.78 @@ -107,28 +107,28 @@
5.79 (* convert the data got via contextToThy to a globally unique handle.
5.80 there is another way to get the guh: get out of the 'theID' in the hierarchy *)
5.81 fun thm2guh (isa, thyID) thmID = case isa of
5.82 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.guh
5.83 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.id
5.84 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
5.85 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
5.86 | _ => raise ERROR
5.87 ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
5.88
5.89 fun rls2guh (isa, thyID) rls' = case isa of
5.90 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.guh
5.91 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.id
5.92 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
5.93 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
5.94 | _ => raise ERROR
5.95 ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
5.96
5.97 fun cal2guh (isa, thyID) calID = case isa of
5.98 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.guh
5.99 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.id
5.100 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
5.101 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
5.102 | _ => raise ERROR
5.103 ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
5.104
5.105 fun ord2guh (isa, thyID) rew_ord' = case isa of
5.106 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.guh
5.107 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.id
5.108 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
5.109 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
5.110 | _ => raise ERROR
6.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 14:36:27 2020 +0200
6.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 16:01:53 2020 +0200
6.3 @@ -38,8 +38,8 @@
6.4 val precond2xml : int -> bool * Term.term -> Celem.xml
6.5 val preconds2xml : int -> (bool * Term.term) list -> Celem.xml
6.6 val rls2xml : int -> ThyC.id * Rule_Set.T -> Celem.xml
6.7 - val rule2xml : int -> Check_Unique.guh -> Rule.rule -> Celem.xml
6.8 - val rules2xml : int -> Check_Unique.guh -> Rule.rule list -> Celem.xml
6.9 + val rule2xml : int -> Check_Unique.id -> Rule.rule -> Celem.xml
6.10 + val rules2xml : int -> Check_Unique.id -> Rule.rule list -> Celem.xml
6.11 val scr2xml : int -> Program.T -> Celem.xml
6.12 val spec2xml : int -> Spec.T -> Celem.xml
6.13 val sub2xml : int -> Term.term * Term.term -> Celem.xml
7.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 22 14:36:27 2020 +0200
7.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Wed Apr 22 16:01:53 2020 +0200
7.3 @@ -15,7 +15,7 @@
7.4 val autoCalculate : Celem.calcID -> Solve.auto -> XML.tree (*unit future*)
7.5 val applyTactic : Celem.calcID -> Pos.pos' -> Tactic.input -> XML.tree
7.6 val CalcTree : Selem.fmz list -> XML.tree
7.7 - val checkContext : Celem.calcID -> Pos.pos' -> Check_Unique.guh -> XML.tree
7.8 + val checkContext : Celem.calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
7.9 val DEconstrCalcTree : Celem.calcID -> XML.tree
7.10 val fetchApplicableTactics : Celem.calcID -> int -> Pos.pos' -> XML.tree
7.11 val fetchProposedTactic : Celem.calcID -> XML.tree
7.12 @@ -47,11 +47,11 @@
7.13 val moveRoot : Celem.calcID -> XML.tree
7.14 val moveUp : Celem.calcID -> Pos.pos' -> XML.tree
7.15 val refFormula : Celem.calcID -> Pos.pos' -> XML.tree
7.16 - val refineProblem : Celem.calcID -> Pos.pos' -> Check_Unique.guh -> XML.tree
7.17 + val refineProblem : Celem.calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
7.18 val replaceFormula : Celem.calcID -> TermC.as_string -> XML.tree
7.19 val requestFillformula : Celem.calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
7.20 val resetCalcHead : Celem.calcID -> XML.tree
7.21 - val setContext : Celem.calcID -> Pos.pos' -> Check_Unique.guh -> XML.tree
7.22 + val setContext : Celem.calcID -> Pos.pos' -> Check_Unique.id -> XML.tree
7.23 val setMethod : Celem.calcID -> Method.id -> XML.tree
7.24 val setNextTactic : Celem.calcID -> Tactic.input -> XML.tree
7.25 val setProblem : Celem.calcID -> Problem.id -> XML.tree
8.1 --- a/src/Tools/isac/Build_Isac.thy Wed Apr 22 14:36:27 2020 +0200
8.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 22 16:01:53 2020 +0200
8.3 @@ -134,7 +134,7 @@
8.4 ML \<open>@{thm last_thmI}\<close>
8.5 ML \<open>@{thm Querkraft_Belastung}\<close>
8.6
8.7 -ML \<open>Check_Unique.check_guhs_unique := false;\<close>
8.8 +ML \<open>Check_Unique.on := false;\<close>
8.9 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
8.10 ML \<open>@{theory "Isac_Knowledge"}\<close>
8.11 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
9.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 22 14:36:27 2020 +0200
9.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 22 16:01:53 2020 +0200
9.3 @@ -13,23 +13,23 @@
9.4 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
9.5 val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
9.6 datatype contthy
9.7 - = ContNOrew of {applto: term, thm_rls: Check_Unique.guh, thyID: ThyC.id}
9.8 - | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Check_Unique.guh, thminst: term, thyID: ThyC.id}
9.9 - | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.guh, thyID: ThyC.id}
9.10 - | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Check_Unique.guh, thyID: ThyC.id}
9.11 + = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
9.12 + | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
9.13 + | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
9.14 + | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
9.15 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
9.16 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
9.17 - thm: Check_Unique.guh, thyID: ThyC.id}
9.18 + thm: Check_Unique.id, thyID: ThyC.id}
9.19 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
9.20 bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
9.21 - rhs: term * term, thm: Check_Unique.guh, thminst: term, thyID: ThyC.id}
9.22 + rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
9.23 | EContThy
9.24 - val guh2filename : Check_Unique.guh -> Celem.filename
9.25 + val guh2filename : Check_Unique.id -> Celem.filename
9.26 val thms_of_rls : Rule_Set.T -> Rule.rule list
9.27 val theID2filename : Thy_Html.theID -> Celem.filename
9.28 - val no_thycontext : Check_Unique.guh -> bool
9.29 - val subs_from : Istate.T -> 'a -> Check_Unique.guh -> Selem.subs
9.30 - val guh2rewtac : Check_Unique.guh -> Selem.subs -> Tactic.input
9.31 + val no_thycontext : Check_Unique.id -> bool
9.32 + val subs_from : Istate.T -> 'a -> Check_Unique.id -> Selem.subs
9.33 + val guh2rewtac : Check_Unique.id -> Selem.subs -> Tactic.input
9.34 val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
9.35 val context_thy : Calc.T -> Tactic.input -> contthy
9.36 val distinct_Thm : Rule.rule list -> Rule.rule list
9.37 @@ -40,7 +40,7 @@
9.38 term option -> term -> (Rule.rule * (term * term list)) list
9.39 val get_bdv_subst : term -> (term * term) list -> Selem.subs option * UnparseC.subst
9.40 val thy_containing_thm : string -> string * string
9.41 - val guh2theID : Check_Unique.guh -> Thy_Html.theID
9.42 + val guh2theID : Check_Unique.id -> Thy_Html.theID
9.43 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.44 (* NONE *)
9.45 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.46 @@ -225,7 +225,7 @@
9.47 EContThy (* not from Know_Store ..............................*)
9.48 | ContThm of (* a theorem in contex ===========================*)
9.49 {thyID : ThyC.id, (* for *2guh in sub-elems here .*)
9.50 - thm : Check_Unique.guh, (* theorem in the context .*)
9.51 + thm : Check_Unique.id, (* theorem in the context .*)
9.52 applto : term, (* applied to formula ... .*)
9.53 applat : term, (* ... with lhs inserted .*)
9.54 reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*)
9.55 @@ -241,7 +241,7 @@
9.56 }
9.57 | ContThmInst of (* a theorem with bdvs in contex ============ *)
9.58 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
9.59 - thm : Check_Unique.guh, (*theorem in the context .*)
9.60 + thm : Check_Unique.id, (*theorem in the context .*)
9.61 bdvs : UnparseC.subst, (*bound variables to modify... .*)
9.62 thminst : term, (*... theorem instantiated .*)
9.63 applto : term, (*applied to formula ... .*)
9.64 @@ -259,14 +259,14 @@
9.65 }
9.66 | ContRls of (* a rule set in contex ========================= *)
9.67 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
9.68 - rls : Check_Unique.guh, (*rule set in the context .*)
9.69 + rls : Check_Unique.id, (*rule set in the context .*)
9.70 applto : term, (*rewrite this formula .*)
9.71 result : term, (*resulting from the rewrite .*)
9.72 asms : term list (*... with asms stored .*)
9.73 }
9.74 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
9.75 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
9.76 - rls : Check_Unique.guh, (*rule set in the context .*)
9.77 + rls : Check_Unique.id, (*rule set in the context .*)
9.78 bdvs : UnparseC.subst, (*for bound variables in thms .*)
9.79 applto : term, (*rewrite this formula .*)
9.80 result : term, (*resulting from the rewrite .*)
9.81 @@ -274,12 +274,12 @@
9.82 }
9.83 | ContNOrew of (* no rewrite for thm or rls ================== *)
9.84 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
9.85 - thm_rls : Check_Unique.guh, (*thm or rls in the context .*)
9.86 + thm_rls : Check_Unique.id, (*thm or rls in the context .*)
9.87 applto : term (*rewrite this formula .*)
9.88 }
9.89 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
9.90 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
9.91 - thm_rls : Check_Unique.guh, (*thm or rls in the context .*)
9.92 + thm_rls : Check_Unique.id, (*thm or rls in the context .*)
9.93 bdvs : UnparseC.subst, (*for bound variables in thms .*)
9.94 thminst : term, (*... theorem instantiated .*)
9.95 applto : term (*rewrite this formula .*)
10.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 22 14:36:27 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Apr 22 16:01:53 2020 +0200
10.3 @@ -145,7 +145,7 @@
10.4 decomposedFunction :: "real => una"
10.5
10.6 ML \<open>
10.7 -Check_Unique.check_guhs_unique := false; (*WN120307 REMOVE after editing*)
10.8 +Check_Unique.on := false; (*WN120307 REMOVE after editing*)
10.9 \<close>
10.10 setup \<open>KEStore_Elems.add_pbts
10.11 [(Specify.prep_pbt @{theory} "pbl_simp_rat_partfrac" [] Problem.id_empty
11.1 --- a/src/Tools/isac/Specify/ptyps.sml Wed Apr 22 14:36:27 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/ptyps.sml Wed Apr 22 16:01:53 2020 +0200
11.3 @@ -36,12 +36,12 @@
11.4 val itm_out : theory -> Model.itm_ -> string
11.5 val dsc_unknown : term
11.6
11.7 - val pblID2guh : Problem.id -> Check_Unique.guh (* for datatypes.sml *)
11.8 - val metID2guh : Method.id -> Check_Unique.guh (* for datatypes.sml *)
11.9 - val kestoreID2guh : Celem.ketype -> Celem.kestoreID -> Check_Unique.guh (* for datatypes.sml *)
11.10 - val guh2kestoreID : Check_Unique.guh -> string list (* for interface.sml *)
11.11 + val pblID2guh : Problem.id -> Check_Unique.id (* for datatypes.sml *)
11.12 + val metID2guh : Method.id -> Check_Unique.id (* for datatypes.sml *)
11.13 + val kestoreID2guh : Celem.ketype -> Celem.kestoreID -> Check_Unique.id (* for datatypes.sml *)
11.14 + val guh2kestoreID : Check_Unique.id -> string list (* for interface.sml *)
11.15 (* for Knowledge/, if below at left margin *)
11.16 - val prep_pbt : theory -> Check_Unique.guh -> string list -> Problem.id ->
11.17 + val prep_pbt : theory -> Check_Unique.id -> string list -> Problem.id ->
11.18 string list * (string * string list) list * Rule_Set.T * string option * Method.id list ->
11.19 Problem.T * Problem.id
11.20 val prep_met : theory -> string -> string list -> Problem.id ->
11.21 @@ -719,18 +719,18 @@
11.22
11.23 fun show_pblguhs () = (* for tests *)
11.24 (tracing o strs2str o (map linefeed))
11.25 - (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh) (get_ptyps ()))
11.26 + (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id) (get_ptyps ()))
11.27 fun sort_pblguhs () = (* for tests *)
11.28 (tracing o strs2str o (map linefeed))
11.29 - (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)))
11.30 + (((sort string_ord) o (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)))
11.31 (get_ptyps ()))
11.32
11.33 fun show_metguhs () = (* for tests *)
11.34 (tracing o strs2str o (map linefeed))
11.35 - (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh) (get_mets ()))
11.36 + (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id) (get_mets ()))
11.37 fun sort_metguhs () = (* for tests *)
11.38 (tracing o strs2str o (map linefeed))
11.39 - (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)))
11.40 + (((sort string_ord) o (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)))
11.41 (get_mets ()))
11.42
11.43 end
12.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Wed Apr 22 14:36:27 2020 +0200
12.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Wed Apr 22 16:01:53 2020 +0200
12.3 @@ -20,13 +20,13 @@
12.4 let
12.5 val {guh, ...} = (**)(pbt: Problem.T)(** )(pbt: met)( **)
12.6 in guh end;
12.7 -pbl_select_guh: Problem.T -> Check_Unique.guh;(**)
12.8 +pbl_select_guh: Problem.T -> Check_Unique.id;(**)
12.9
12.10 fun met_select_guh pbt =
12.11 let
12.12 val {guh, ...} = (pbt: Method.T)
12.13 in guh end;
12.14 -met_select_guh: Method.T -> Check_Unique.guh;(**)
12.15 +met_select_guh: Method.T -> Check_Unique.id;(**)
12.16
12.17 (*------- hint: build higher order functions be replacing the selector by a variable argument *)
12.18 (* collect*)
12.19 @@ -39,8 +39,8 @@
12.20 in nodes [] pbls end;
12.21
12.22 collect: ('a -> 'b) -> 'a Store.T -> 'b list;
12.23 -collect pbl_select_guh: Problem.T Store.T -> Check_Unique.guh list;
12.24 -collect met_select_guh: Method.T Store.T -> Check_Unique.guh list;
12.25 +collect pbl_select_guh: Problem.T Store.T -> Check_Unique.id list;
12.26 +collect met_select_guh: Method.T Store.T -> Check_Unique.id list;
12.27
12.28 fun message select store guh =
12.29 if member op = (select store) guh
12.30 @@ -49,16 +49,16 @@
12.31 "consider setting \"Check_Unique.on := false\"")
12.32 else ();
12.33
12.34 - message: ('a -> Check_Unique.guh list ) -> 'a -> Check_Unique.guh -> unit;
12.35 -(message (collect pbl_select_guh)): Problem.T Store.T -> Check_Unique.guh -> unit;
12.36 -(message (collect met_select_guh)): Method.T Store.T -> Check_Unique.guh -> unit;
12.37 + message: ('a -> Check_Unique.id list ) -> 'a -> Check_Unique.id -> unit;
12.38 +(message (collect pbl_select_guh)): Problem.T Store.T -> Check_Unique.id -> unit;
12.39 +(message (collect met_select_guh)): Method.T Store.T -> Check_Unique.id -> unit;
12.40
12.41 -(Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)): Problem.T Store.T -> Check_Unique.guh list;
12.42 -(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)): Method.T Store.T -> Check_Unique.guh list;
12.43 +(Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id)): Problem.T Store.T -> Check_Unique.id list;
12.44 +(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id)): Method.T Store.T -> Check_Unique.id list;
12.45
12.46 -val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh));
12.47 -check_pblguh_unique: Problem.T Store.T -> Check_Unique.guh -> unit
12.48 +val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id));
12.49 +check_pblguh_unique: Problem.T Store.T -> Check_Unique.id -> unit
12.50 ;
12.51 -val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh));
12.52 -check_metguh_unique: Meth_Def.T Store.T -> Check_Unique.guh -> unit
12.53 +val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.id));
12.54 +check_metguh_unique: Meth_Def.T Store.T -> Check_Unique.id -> unit
12.55 ;
12.56 \ No newline at end of file
13.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 14:36:27 2020 +0200
13.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Apr 22 16:01:53 2020 +0200
13.3 @@ -85,7 +85,7 @@
13.4 Iterator 1;
13.5 moveActiveRoot 1; autoCalculate 1 CompleteCalc;
13.6 refineProblem 1 ([1],Res) "pbl_equ_univ";
13.7 -"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : Check_Unique.guh)) =
13.8 +"~~~~~ fun refineProblem, args:"; val (cI, ((p,p_) : pos'), (guh : Check_Unique.id)) =
13.9 (1, ([1],Res), "pbl_equ_univ");
13.10 val pblID = guh2kestoreID guh
13.11 val ((pt,_),_) = get_calc cI
14.1 --- a/test/Tools/isac/Specify/ptyps.sml Wed Apr 22 14:36:27 2020 +0200
14.2 +++ b/test/Tools/isac/Specify/ptyps.sml Wed Apr 22 16:01:53 2020 +0200
14.3 @@ -421,27 +421,27 @@
14.4 "----------- fun coll_guhs ---------------------------------------";
14.5 "----------- fun coll_guhs ---------------------------------------";
14.6 val n = Probl_Def.empty;
14.7 -(#guh : Problem.T -> Check_Unique.guh) Probl_Def.empty;
14.8 +(#guh : Problem.T -> Check_Unique.id) Probl_Def.empty;
14.9
14.10 fun XXXnode coll (Store.Node (_,[n],ns)) =
14.11 - [(#guh : Problem.T -> Check_Unique.guh) n]
14.12 + [(#guh : Problem.T -> Check_Unique.id) n]
14.13 and XXXnodes coll [] = coll
14.14 | XXXnodes coll (n::ns : Problem.T Store.T) = (XXXnode coll n) @
14.15 (XXXnodes coll ns);
14.16 (*^^^ this works, but not this ...
14.17 fun node coll (Store.Node (_,[n],ns)) =
14.18 - [(#guh : 'a -> Check_Unique.guh) n]
14.19 + [(#guh : 'a -> Check_Unique.id) n]
14.20 and nodes coll [] = coll
14.21 | nodes coll (n::ns : 'a Store.T) = (node coll n) @ (nodes coll ns);
14.22
14.23 Error:
14.24 Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)
14.25 - Found near #guh : 'a -> Check_Unique.guh
14.26 + Found near #guh : 'a -> Check_Unique.id
14.27
14.28 i.e. there is no common fun for pbls and mets ?!?*)
14.29
14.30 -((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh))) (get_ptyps ());
14.31 -sort string_ord (((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh))) (get_ptyps ()));
14.32 +((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ());
14.33 +sort string_ord (((Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.id))) (get_ptyps ()));
14.34 show_pblguhs ();
14.35 sort_pblguhs ();
14.36