1.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 16:43:53 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Mon Apr 20 15:54:19 2020 +0200
1.3 @@ -10,25 +10,25 @@
1.4 (*/------- to Celem8 -------\*)
1.5 type authors
1.6 datatype thydata
1.7 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Spec.guh, mathauthors: authors}
1.8 - | Hord of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
1.9 - | Hrls of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
1.10 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Spec.guh, mathauthors: authors, thm: thm}
1.11 - | Html of {coursedesign: authors, guh: Spec.guh, html: string, mathauthors: authors}
1.12 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors}
1.13 + | Hord of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
1.14 + | Hrls of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
1.15 + | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.guh, mathauthors: authors, thm: thm}
1.16 + | Html of {coursedesign: authors, guh: Check_Unique.guh, html: string, mathauthors: authors}
1.17 type theID
1.18 val theID2str: string list -> string
1.19 val the2str: thydata -> string
1.20 val thes2str: thydata list -> string
1.21 val theID2thyID: theID -> ThyC.id
1.22
1.23 - val part2guh: theID -> Spec.guh
1.24 - val thy2guh: theID -> Spec.guh
1.25 - val thypart2guh: theID -> Spec.guh
1.26 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Spec.guh
1.27 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Spec.guh
1.28 - val cal2guh: string * ThyC.id -> string -> Spec.guh
1.29 - val ord2guh: string * ThyC.id -> string -> Spec.guh
1.30 - val theID2guh: theID -> Spec.guh
1.31 + val part2guh: theID -> Check_Unique.guh
1.32 + val thy2guh: theID -> Check_Unique.guh
1.33 + val thypart2guh: theID -> Check_Unique.guh
1.34 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
1.35 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
1.36 + val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
1.37 + val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
1.38 + val theID2guh: theID -> Check_Unique.guh
1.39
1.40 val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
1.41 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
1.42 @@ -56,12 +56,12 @@
1.43 (* datatype for collecting thydata for hierarchy *)
1.44 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
1.45 datatype thydata =
1.46 - Html of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, html: string}
1.47 -| Hthm of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
1.48 + Html of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, html: string}
1.49 +| Hthm of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
1.50 thm: thm} (* here no sym_thm, thus no thmID required *)
1.51 -| Hrls of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
1.52 -| Hcal of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
1.53 -| Hord of {guh: Spec.guh, coursedesign: authors, mathauthors: authors,
1.54 +| Hrls of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
1.55 +| Hcal of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
1.56 +| Hord of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors,
1.57 ord: (UnparseC.subst -> (term * term) -> bool)};
1.58 fun the2str (Html {guh, ...}) = guh
1.59 | the2str (Hthm {guh, ...}) = guh
1.60 @@ -86,7 +86,7 @@
1.61 type thehier = (thydata Store.ptyp) list;
1.62 (* required to determine sequence of main nodes of thehier in Know_Store.thy *)
1.63 fun part2guh [str] = (case str of
1.64 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Spec.guh
1.65 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.guh
1.66 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
1.67 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
1.68 | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
1.69 @@ -100,7 +100,7 @@
1.70 | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
1.71
1.72 fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
1.73 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Spec.guh
1.74 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.guh
1.75 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
1.76 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
1.77 | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
1.78 @@ -110,28 +110,28 @@
1.79 (* convert the data got via contextToThy to a globally unique handle.
1.80 there is another way to get the guh: get out of the 'theID' in the hierarchy *)
1.81 fun thm2guh (isa, thyID) thmID = case isa of
1.82 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Spec.guh
1.83 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.guh
1.84 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
1.85 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
1.86 | _ => raise ERROR
1.87 ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
1.88
1.89 fun rls2guh (isa, thyID) rls' = case isa of
1.90 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Spec.guh
1.91 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.guh
1.92 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
1.93 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
1.94 | _ => raise ERROR
1.95 ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
1.96
1.97 fun cal2guh (isa, thyID) calID = case isa of
1.98 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Spec.guh
1.99 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.guh
1.100 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
1.101 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
1.102 | _ => raise ERROR
1.103 ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
1.104
1.105 fun ord2guh (isa, thyID) rew_ord' = case isa of
1.106 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Spec.guh
1.107 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.guh
1.108 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
1.109 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
1.110 | _ => raise ERROR