1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 15:54:19 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 16:47:01 2020 +0200
1.3 @@ -33,10 +33,10 @@
1.4 ML_file "check-unique.sml"
1.5 ML_file "specification.sml"
1.6 ML_file "celem-4.sml" (*pat*)
1.7 -ML_file "celem-5.sml" (*ptyps*)
1.8 -ML_file "celem-6.sml" (*mets*)
1.9 -ML_file "celem-7.sml" (*cas_elem*)
1.10 -ML_file "celem-8.sml" (*thydata*)
1.11 +ML_file "problem-def.sml"
1.12 +ML_file "method-def.sml"
1.13 +ML_file "cas-def.sml"
1.14 +ML_file "thy-html.sml"
1.15
1.16 ML_file tracing.sml
1.17 ML \<open>
1.18 @@ -64,15 +64,15 @@
1.19 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
1.20 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.21 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.22 - val get_cas: theory -> Celem7.cas_elem list
1.23 - val add_cas: Celem7.cas_elem list -> theory -> theory
1.24 - val get_ptyps: theory -> Celem5.ptyps
1.25 - val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
1.26 - val get_mets: theory -> Celem6.mets
1.27 - val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
1.28 - val get_thes: theory -> (Celem8.thydata Store.ptyp) list
1.29 - val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.30 - val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.31 + val get_cas: theory -> CAS_Def.cas_elem list
1.32 + val add_cas: CAS_Def.cas_elem list -> theory -> theory
1.33 + val get_ptyps: theory -> Probl_Def.ptyps
1.34 + val add_pbts: (Probl_Def.pbt * Spec.pblID) list -> theory -> theory
1.35 + val get_mets: theory -> Meth_Def.mets
1.36 + val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
1.37 + val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
1.38 + val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.39 + val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.40 val get_ref_thy: unit -> theory
1.41 val set_ref_thy: theory -> unit
1.42 end;
1.43 @@ -103,14 +103,14 @@
1.44 type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
1.45 val empty = [];
1.46 val extend = I;
1.47 - val merge = merge Celem7.cas_eq;
1.48 + val merge = merge CAS_Def.cas_eq;
1.49 );
1.50 fun get_cas thy = Data.get thy
1.51 - fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
1.52 + fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
1.53
1.54 structure Data = Theory_Data (
1.55 - type T = Celem5.ptyps;
1.56 - val empty = [Celem5.e_Ptyp];
1.57 + type T = Probl_Def.ptyps;
1.58 + val empty = [Probl_Def.e_Ptyp];
1.59 val extend = I;
1.60 val merge = Store.merge_ptyps;
1.61 );
1.62 @@ -118,39 +118,39 @@
1.63 fun add_pbts pbts thy = let
1.64 fun add_pbt (pbt as {guh,...}, pblID) =
1.65 (* the pblID has the leaf-element as first; better readability achieved *)
1.66 - (if (!Check_Unique.check_guhs_unique) then Celem5.check_pblguh_unique guh (Data.get thy) else ();
1.67 + (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_pblguh_unique guh (Data.get thy) else ();
1.68 rev pblID |> Store.insrt pblID pbt);
1.69 in Data.map (fold add_pbt pbts) thy end;
1.70
1.71 structure Data = Theory_Data (
1.72 - type T = Celem6.mets;
1.73 - val empty = [Celem6.e_Mets];
1.74 + type T = Meth_Def.mets;
1.75 + val empty = [Meth_Def.e_Mets];
1.76 val extend = I;
1.77 val merge = Store.merge_ptyps;
1.78 );
1.79 val get_mets = Data.get;
1.80 fun add_mets mets thy = let
1.81 fun add_met (met as {guh,...}, metID) =
1.82 - (if (!Check_Unique.check_guhs_unique) then Celem6.check_metguh_unique guh (Data.get thy) else ();
1.83 + (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_metguh_unique guh (Data.get thy) else ();
1.84 Store.insrt metID met metID);
1.85 in Data.map (fold add_met mets) thy end;
1.86
1.87 structure Data = Theory_Data (
1.88 - type T = (Celem8.thydata Store.ptyp) list;
1.89 + type T = (Thy_Html.thydata Store.ptyp) list;
1.90 val empty = [];
1.91 val extend = I;
1.92 val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
1.93 );
1.94 fun get_thes thy = Data.get thy
1.95 fun add_thes thes thy = let
1.96 - fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
1.97 + fun add_the (thydata, theID) = Thy_Html.add_thydata ([], theID) thydata
1.98 in Data.map (fold add_the thes) thy end;
1.99 fun insert_fillpats fis thy =
1.100 let
1.101 fun update_elem (theID, fillpats) =
1.102 let
1.103 val hthm = Store.get_py (Data.get thy) theID theID
1.104 - val hthm' = Celem8.update_hthm hthm fillpats
1.105 + val hthm' = Thy_Html.update_hthm hthm fillpats
1.106 handle ERROR _ =>
1.107 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.108 in Store.update_ptyps theID theID hthm' end
1.109 @@ -209,11 +209,11 @@
1.110 section \<open>determine sequence of main parts in thehier\<close>
1.111 setup \<open>
1.112 KEStore_Elems.add_thes
1.113 - [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
1.114 + [(Thy_Html.Html {guh = Thy_Html.part2guh ["IsacKnowledge"], html = "",
1.115 mathauthors = ["Isac team"], coursedesign = []}, ["IsacKnowledge"]),
1.116 - (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
1.117 + (Thy_Html.Html {guh = Thy_Html.part2guh ["Isabelle"], html = "",
1.118 mathauthors = ["Isabelle team, TU Munich"], coursedesign = []}, ["Isabelle"]),
1.119 - (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
1.120 + (Thy_Html.Html {guh = Thy_Html.part2guh ["IsacScripts"], html = "",
1.121 mathauthors = ["Isac team"], coursedesign = []}, ["IsacScripts"])]
1.122 \<close>
1.123
1.124 @@ -233,7 +233,7 @@
1.125 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.126
1.127 (* we avoid term_to_string''' defined later *)
1.128 -fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
1.129 +fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
1.130 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.131 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.132
1.133 @@ -242,25 +242,25 @@
1.134 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.135 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.136 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.137 -val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
1.138 +val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.pbts2str;
1.139 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.140 -fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
1.141 +fun pbt_ord ({guh = guh'1, ...} : Probl_Def.pbt, {guh = guh'2, ...} : Probl_Def.pbt) = string_ord (guh'1, guh'2);
1.142 fun sort_kestore_ptyp' _ [] = []
1.143 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
1.144 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.145 :: sort_kestore_ptyp' ordfun ps');
1.146 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.147
1.148 -fun metguh2str ({guh,...} : Celem6.met) = guh : string;
1.149 -fun check_kestore_met (mp: Celem6.met Store.ptyp) =
1.150 +fun metguh2str ({guh,...} : Meth_Def.met) = guh : string;
1.151 +fun check_kestore_met (mp: Meth_Def.met Store.ptyp) =
1.152 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.153 -fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
1.154 +fun met_ord ({guh = guh'1, ...} : Meth_Def.met, {guh = guh'2, ...} : Meth_Def.met) = string_ord (guh'1, guh'2);
1.155 val sort_kestore_met = sort_kestore_ptyp' met_ord;
1.156
1.157 -fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
1.158 +fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Thy_Html.thes2str))) thes
1.159 fun write_thes thydata_list =
1.160 thydata_list
1.161 - |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
1.162 + |> map (fn (id, the) => (Thy_Html.theID2str id, Thy_Html.the2str the))
1.163 |> map pair2str
1.164 |> map writeln
1.165 \<close>
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Mon Apr 20 15:54:19 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Mon Apr 20 16:47:01 2020 +0200
2.3 @@ -16,10 +16,10 @@
2.4 (*\------- to Celem7 -------/*)
2.5
2.6 (*/------- to Celem5 -------\*)
2.7 - type pbt = Celem5.pbt
2.8 + type pbt = Probl_Def.pbt
2.9 val e_pbt: pbt;
2.10 val e_Ptyp: pbt Store.ptyp
2.11 - type ptyps = Celem5.ptyps
2.12 + type ptyps = Probl_Def.ptyps
2.13 val pbts2str: pbt list -> string
2.14 (*\------- to Celem5 -------/*)
2.15
2.16 @@ -49,9 +49,9 @@
2.17 (*\------- to Celem2 -------/*)
2.18
2.19 (*/------- to Celem8 -------\*)
2.20 - type authors = Celem8.authors
2.21 - datatype thydata = datatype Celem8.thydata
2.22 - type theID = Celem8.theID
2.23 + type authors = Thy_Html.authors
2.24 + datatype thydata = datatype Thy_Html.thydata
2.25 + type theID = Thy_Html.theID
2.26 val theID2str: string list -> string
2.27 val the2str: thydata -> string
2.28 val thes2str: thydata list -> string
2.29 @@ -71,8 +71,8 @@
2.30 (*\------- to Celem8 -------/*)
2.31
2.32 (*/------- to Celem6 -------\*)
2.33 - type met = Celem6.met
2.34 - type mets = Celem6.mets
2.35 + type met = Meth_Def.met
2.36 + type mets = Meth_Def.mets
2.37 val e_Mets: met Store.ptyp
2.38 (*\------- to Celem6 -------/*)
2.39
2.40 @@ -182,8 +182,8 @@
2.41 (*\------- to Spec -------/*)
2.42
2.43 (*/------- to Celem7 -------\*)
2.44 -type cas_elem = Celem7.cas_elem;
2.45 -val cas_eq = Celem7.cas_eq;
2.46 +type cas_elem = CAS_Def.cas_elem;
2.47 +val cas_eq = CAS_Def.cas_eq;
2.48 (*\------- to Celem7 -------/*)
2.49
2.50 (*either theID or pblID or metID*)
2.51 @@ -215,25 +215,25 @@
2.52 (*\------- to Store -------/*)
2.53
2.54 (*/------- to Celem8 -------\*)
2.55 -type authors = Celem8.authors;
2.56 -datatype thydata = datatype Celem8.thydata;
2.57 -type theID = Celem8.theID;
2.58 -val theID2str = Celem8.theID2str;
2.59 -val the2str = Celem8.the2str;
2.60 -val thes2str = Celem8.thes2str;
2.61 -val theID2thyID = Celem8.theID2thyID;
2.62 +type authors = Thy_Html.authors;
2.63 +datatype thydata = datatype Thy_Html.thydata;
2.64 +type theID = Thy_Html.theID;
2.65 +val theID2str = Thy_Html.theID2str;
2.66 +val the2str = Thy_Html.the2str;
2.67 +val thes2str = Thy_Html.thes2str;
2.68 +val theID2thyID = Thy_Html.theID2thyID;
2.69
2.70 -val part2guh = Celem8.part2guh;
2.71 -val thy2guh = Celem8.thy2guh;
2.72 -val thypart2guh = Celem8.thypart2guh;
2.73 -val thm2guh = Celem8.thm2guh;
2.74 -val rls2guh = Celem8.rls2guh;
2.75 -val cal2guh = Celem8.cal2guh;
2.76 -val ord2guh = Celem8.ord2guh;
2.77 -val theID2guh = Celem8.theID2guh;
2.78 +val part2guh = Thy_Html.part2guh;
2.79 +val thy2guh = Thy_Html.thy2guh;
2.80 +val thypart2guh = Thy_Html.thypart2guh;
2.81 +val thm2guh = Thy_Html.thm2guh;
2.82 +val rls2guh = Thy_Html.rls2guh;
2.83 +val cal2guh = Thy_Html.cal2guh;
2.84 +val ord2guh = Thy_Html.ord2guh;
2.85 +val theID2guh = Thy_Html.theID2guh;
2.86
2.87 -val add_thydata = Celem8.add_thydata;
2.88 -val update_hthm = Celem8.update_hthm;
2.89 +val add_thydata = Thy_Html.add_thydata;
2.90 +val update_hthm = Thy_Html.update_hthm;
2.91 (*\------- to Celem8 -------/*)
2.92
2.93 type filepath = string;
2.94 @@ -280,26 +280,26 @@
2.95 (term * (* description *)
2.96 term)); (* id | struct-var *)
2.97 (*/------- to Celem5 -------\*)
2.98 -type pbt = Celem5.pbt;
2.99 -val e_pbt = Celem5.e_pbt;
2.100 -val e_Ptyp = Celem5.e_Ptyp;
2.101 -val pbts2str = Celem5.pbts2str;
2.102 -type ptyps = Celem5.ptyps;
2.103 +type pbt = Probl_Def.pbt;
2.104 +val e_pbt = Probl_Def.e_pbt;
2.105 +val e_Ptyp = Probl_Def.e_Ptyp;
2.106 +val pbts2str = Probl_Def.pbts2str;
2.107 +type ptyps = Probl_Def.ptyps;
2.108 (*\------- to Celem5 -------/*)
2.109
2.110 (*/------- to Celem6 -------\*)
2.111 -type met = Celem6.met;
2.112 -val e_met = Celem6.e_met;
2.113 -val e_Mets = Celem6.e_Mets;
2.114 +type met = Meth_Def.met;
2.115 +val e_met = Meth_Def.e_met;
2.116 +val e_Mets = Meth_Def.e_Mets;
2.117 type mets = (met Store.ptyp) list;
2.118 (*\------- to Celem6 -------/*)
2.119
2.120 (*/------- to Celem91 -------\*)
2.121 val check_guhs_unique = Check_Unique.check_guhs_unique;
2.122 -val coll_pblguhs = Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh);
2.123 -val check_pblguh_unique = Celem5.check_pblguh_unique;
2.124 -val coll_metguhs = Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh);
2.125 -val check_metguh_unique = Celem6.check_metguh_unique;
2.126 +val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh);
2.127 +val check_pblguh_unique = Probl_Def.check_pblguh_unique;
2.128 +val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh);
2.129 +val check_metguh_unique = Meth_Def.check_metguh_unique;
2.130 (*\------- to Celem91 -------/*)
2.131
2.132 (*/------- to Celem8 -------\*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml Mon Apr 20 16:47:01 2020 +0200
3.3 @@ -0,0 +1,40 @@
3.4 +(* Title: BaseDefinitions/celem-7.sml
3.5 + Author: Walther Neuper
3.6 + (c) due to copyright terms
3.7 +
3.8 + *)
3.9 +signature COMPUTER_ALGEBRA_SYSTEM__COMMAND_DEF =
3.10 +(*/------- to Celem7 -------\*)
3.11 +(*\------- to Celem7 -------/*)
3.12 +sig
3.13 +(*/------- to Celem7 -------\*)
3.14 + type cas_elem
3.15 + val cas_eq: cas_elem * cas_elem -> bool
3.16 +(*\------- to Celem7 -------/*)
3.17 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.18 + (*NONE*)
3.19 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.20 + (*NONE*)
3.21 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.22 +end
3.23 +
3.24 +(**)
3.25 +structure CAS_Def(**): COMPUTER_ALGEBRA_SYSTEM__COMMAND_DEF(**) =
3.26 +struct
3.27 +(**)
3.28 +
3.29 +(*/------- to Celem7 -------\*)
3.30 +(* association list with cas-commands, for generating a complete calc-head *)
3.31 +type generate_fn =
3.32 + (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
3.33 + (term * (* description of an element *)
3.34 + term list) (* value of the element (always put into a list) *)
3.35 + list) (* of elements in the formalization *)
3.36 +type cas_elem =
3.37 + (term * (* cas-command, eg. 'solve' *)
3.38 + (Spec.spec * (* theory, problem, method *)
3.39 + generate_fn))
3.40 +fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
3.41 +(*\------- to Celem7 -------/*)
3.42 +
3.43 +(**)end(**)
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Mon Apr 20 15:54:19 2020 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,65 +0,0 @@
4.4 -(* Title: BaseDefinitions/problem-def.sml
4.5 - Author: Walther Neuper
4.6 - (c) due to copyright terms
4.7 -
4.8 -Will be enhanced by Problem later.
4.9 -*)
4.10 -signature CALCELEMENT_5 =
4.11 -sig
4.12 - type pbt
4.13 - type ptyps
4.14 - val pbts2str: pbt list -> string
4.15 - val e_Ptyp: pbt Store.ptyp
4.16 -(*vvv check_unique*)
4.17 - val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
4.18 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.19 - val e_pbt: pbt
4.20 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.21 - (*NONE*)
4.22 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.23 -end
4.24 -
4.25 -(**)
4.26 -structure Celem5(**): CALCELEMENT_5(**) =
4.27 -struct
4.28 -(**)
4.29 -
4.30 -(*/------- to Celem5 -------\*)
4.31 -type pbt =
4.32 - {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
4.33 - mathauthors : string list, (* copyright *)
4.34 - init : Spec.pblID, (* to start refinement with *)
4.35 - thy : theory, (* which allows to compile that pbt
4.36 - TODO: search generalized for subthy (ref.p.69*)
4.37 - (*^^^ WN050912 NOT used during application of the problem,
4.38 - because applied terms may be from 'subthy' as well as from super;
4.39 - thus we take 'maxthy'; see match_ags ! *)
4.40 - cas : term option, (* 'CAS-command' *)
4.41 - met : Spec.metID list, (* methods solving the pbt *)
4.42 -(*TODO: abstract to ?pre_model?...*)
4.43 - prls : Rule_Set.T, (* for preds in where_ *)
4.44 - where_ : term list, (* where - predicates *)
4.45 - ppc : Celem4.pat list (* this is the model-pattern;
4.46 - it contains "#Given","#Where","#Find","#Relate"-patterns
4.47 - for constraints on identifiers see "fun cpy_nam" *)
4.48 -}
4.49 -val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
4.50 - cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
4.51 -fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
4.52 - prls = prls', thy = thy', where_ = w'} : pbt)
4.53 - = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
4.54 - ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
4.55 - ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "
4.56 - ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
4.57 - ^ (UnparseC.terms w') ^ "}" |> linefeed;
4.58 -fun pbts2str pbts = map pbt2str pbts |> list2str;
4.59 -(*\------- to Celem5 -------/*)
4.60 -(*/------- to Celem5 -------\*)
4.61 -val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], [])
4.62 -type ptyps = (pbt Store.ptyp) list
4.63 -(*\------- to Celem5 -------/*)
4.64 -
4.65 -val check_pblguh_unique =
4.66 - Check_Unique.messsage (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
4.67 -
4.68 -(**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Mon Apr 20 15:54:19 2020 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,64 +0,0 @@
5.4 -(* Title: BaseDefinitions/method-def.sml
5.5 - Author: Walther Neuper
5.6 - (c) due to copyright terms
5.7 -
5.8 -Will be enhanced by Method later.
5.9 -*)
5.10 -signature CALCELEMENT_6 =
5.11 -sig
5.12 - type met
5.13 - val e_met: met
5.14 - type mets
5.15 - val e_Mets: met Store.ptyp
5.16 -(*vvv check_unique*)
5.17 - val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit
5.18 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.19 - (*NONE*)
5.20 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.21 - (*NONE*)
5.22 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.23 -end
5.24 -
5.25 -(**)
5.26 -structure Celem6(**): CALCELEMENT_6(**) =
5.27 -struct
5.28 -(**)
5.29 -
5.30 -(*/------- to Celem6 -------\*)
5.31 -(* data for methods stored in 'methods'-database*)
5.32 -type met =
5.33 - {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
5.34 - mathauthors: string list, (* copyright *)
5.35 - init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
5.36 - rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
5.37 - TODO.WN0509 store fun itself, see 'type pbt' *)
5.38 - erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
5.39 - instead erls in "fun prep_met" *)
5.40 - srls : Rule_Set.T, (* for evaluating list expressions in scr *)
5.41 - crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
5.42 - nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
5.43 - errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
5.44 - calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
5.45 - (*branch : TransitiveB set in append_problem at generation ob pblobj *)
5.46 - scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
5.47 -(*TODO: abstract to ?pre_model?...*)
5.48 - prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
5.49 - ppc : Celem4.pat list, (* items in given, find, relate;
5.50 - items (in "#Find") which need not occur in the arg-list of a SubProblem
5.51 - are 'copy-named' with an identifier "*'.'".
5.52 - copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
5.53 - see ME/calchead.sml 'fun is_copy_named'. *)
5.54 - pre : term list (* preconditions in where *)
5.55 - };
5.56 -val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
5.57 - erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
5.58 - errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
5.59 -val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
5.60 -
5.61 -type mets = (met Store.ptyp) list;
5.62 -(*\------- to Celem6 -------/*)
5.63 -
5.64 -val check_metguh_unique =
5.65 - Check_Unique.messsage (Check_Unique.collect (#guh: met -> Check_Unique.guh));
5.66 -
5.67 -(**)end(**)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-7.sml Mon Apr 20 15:54:19 2020 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,40 +0,0 @@
6.4 -(* Title: BaseDefinitions/celem-7.sml
6.5 - Author: Walther Neuper
6.6 - (c) due to copyright terms
6.7 -
6.8 - *)
6.9 -signature CALCELEMENT_7 =
6.10 -(*/------- to Celem7 -------\*)
6.11 -(*\------- to Celem7 -------/*)
6.12 -sig
6.13 -(*/------- to Celem7 -------\*)
6.14 - type cas_elem
6.15 - val cas_eq: cas_elem * cas_elem -> bool
6.16 -(*\------- to Celem7 -------/*)
6.17 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.18 - (*NONE*)
6.19 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.20 - (*NONE*)
6.21 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.22 -end
6.23 -
6.24 -(**)
6.25 -structure Celem7(**): CALCELEMENT_7(**) =
6.26 -struct
6.27 -(**)
6.28 -
6.29 -(*/------- to Celem7 -------\*)
6.30 -(* association list with cas-commands, for generating a complete calc-head *)
6.31 -type generate_fn =
6.32 - (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
6.33 - (term * (* description of an element *)
6.34 - term list) (* value of the element (always put into a list) *)
6.35 - list) (* of elements in the formalization *)
6.36 -type cas_elem =
6.37 - (term * (* cas-command, eg. 'solve' *)
6.38 - (Spec.spec * (* theory, problem, method *)
6.39 - generate_fn))
6.40 -fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
6.41 -(*\------- to Celem7 -------/*)
6.42 -
6.43 -(**)end(**)
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Mon Apr 20 15:54:19 2020 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,216 +0,0 @@
7.4 -(* Title: BaseDefinitions/celem-8.sml
7.5 - Author: Walther Neuper
7.6 - (c) due to copyright terms
7.7 -
7.8 - *)
7.9 -signature CALCELEMENT_8 =
7.10 -(*/------- to Celem8 -------\*)
7.11 -(*\------- to Celem8 -------/*)
7.12 -sig
7.13 -(*/------- to Celem8 -------\*)
7.14 - type authors
7.15 - datatype thydata
7.16 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors}
7.17 - | Hord of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
7.18 - | Hrls of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
7.19 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.guh, mathauthors: authors, thm: thm}
7.20 - | Html of {coursedesign: authors, guh: Check_Unique.guh, html: string, mathauthors: authors}
7.21 - type theID
7.22 - val theID2str: string list -> string
7.23 - val the2str: thydata -> string
7.24 - val thes2str: thydata list -> string
7.25 - val theID2thyID: theID -> ThyC.id
7.26 -
7.27 - val part2guh: theID -> Check_Unique.guh
7.28 - val thy2guh: theID -> Check_Unique.guh
7.29 - val thypart2guh: theID -> Check_Unique.guh
7.30 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
7.31 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
7.32 - val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
7.33 - val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
7.34 - val theID2guh: theID -> Check_Unique.guh
7.35 -
7.36 - val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
7.37 - val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
7.38 -(*\------- to Celem8 -------/*)
7.39 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.40 - (*NONE*)
7.41 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.42 - (*NONE*)
7.43 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.44 -end
7.45 -
7.46 -(**)
7.47 -structure Celem8(**): CALCELEMENT_8(**) =
7.48 -struct
7.49 -(**)
7.50 -
7.51 -(*/------- to Celem8 -------\*)
7.52 -(*the key into the hierarchy ob theory elements*)
7.53 -type theID = string list;
7.54 -val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
7.55 -fun theID2thyID theID =
7.56 - if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
7.57 - else error ("theID2thyID called with " ^ theID2str theID);
7.58 -type authors = string list;
7.59 -(* datatype for collecting thydata for hierarchy *)
7.60 -(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
7.61 -datatype thydata =
7.62 - Html of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, html: string}
7.63 -| Hthm of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
7.64 - thm: thm} (* here no sym_thm, thus no thmID required *)
7.65 -| Hrls of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
7.66 -| Hcal of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
7.67 -| Hord of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors,
7.68 - ord: (UnparseC.subst -> (term * term) -> bool)};
7.69 -fun the2str (Html {guh, ...}) = guh
7.70 - | the2str (Hthm {guh, ...}) = guh
7.71 - | the2str (Hrls {guh, ...}) = guh
7.72 - | the2str (Hcal {guh, ...}) = guh
7.73 - | the2str (Hord {guh, ...}) = guh
7.74 -fun thes2str thes = map the2str thes |> list2str;
7.75 -(*\------- to Celem8 -------/*)
7.76 -
7.77 -(*/------- to Celem8 -------\*)
7.78 -(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
7.79 - (a): thehier does not contain sym_thmID theorems
7.80 - (b): lookup for sym_thmID directly from Isabelle using sym_thm
7.81 - (within math-engine NO lookup in thehier -- within java in *.xml only!)
7.82 -TODO (c): export from thehier to xml
7.83 -TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
7.84 -TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
7.85 -TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
7.86 - stands for both, "thmID" and "sym_thmID"
7.87 -TODO (d1) lookup from calctxt
7.88 -TODO (d1) lookup from from rule set in MiniBrowser *)
7.89 -type thehier = (thydata Store.ptyp) list;
7.90 -(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
7.91 -fun part2guh [str] = (case str of
7.92 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.guh
7.93 - | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
7.94 - | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
7.95 - | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
7.96 - | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
7.97 -
7.98 -fun thy2guh [part, thyID] = (case part of
7.99 - "Isabelle" => "thy_isab_" ^ thyID
7.100 - | "IsacScripts" => "thy_scri_" ^ thyID
7.101 - | "IsacKnowledge" => "thy_isac_" ^ thyID
7.102 - | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
7.103 - | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
7.104 -
7.105 -fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
7.106 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.guh
7.107 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
7.108 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
7.109 - | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
7.110 - | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
7.111 -
7.112 -
7.113 -(* convert the data got via contextToThy to a globally unique handle.
7.114 - there is another way to get the guh: get out of the 'theID' in the hierarchy *)
7.115 -fun thm2guh (isa, thyID) thmID = case isa of
7.116 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.guh
7.117 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
7.118 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
7.119 - | _ => raise ERROR
7.120 - ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
7.121 -
7.122 -fun rls2guh (isa, thyID) rls' = case isa of
7.123 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.guh
7.124 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
7.125 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
7.126 - | _ => raise ERROR
7.127 - ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
7.128 -
7.129 -fun cal2guh (isa, thyID) calID = case isa of
7.130 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.guh
7.131 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
7.132 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
7.133 - | _ => raise ERROR
7.134 - ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
7.135 -
7.136 -fun ord2guh (isa, thyID) rew_ord' = case isa of
7.137 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.guh
7.138 - | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
7.139 - | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
7.140 - | _ => raise ERROR
7.141 - ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
7.142 -
7.143 -(* not only for thydata, but also for thy's etc *)
7.144 -(* TODO
7.145 -fun theID2guh theID = case length theID of
7.146 - 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
7.147 - | 1 => part2guh theID
7.148 - | 2 => thy2guh theID
7.149 - | 3 => thypart2guh theID
7.150 - | 4 =>
7.151 - let val [isa, thyID, typ, elemID] = theID
7.152 - in case typ of
7.153 - "Theorems" => thm2guh (isa, thyID) elemID
7.154 - | "Rulesets" => rls2guh (isa, thyID) elemID
7.155 - | "Calculations" => cal2guh (isa, thyID) elemID
7.156 - | "Orders" => ord2guh (isa, thyID) elemID
7.157 - | "Theorems" => thy2guh [isa, thyID]
7.158 - | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
7.159 - end
7.160 - | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
7.161 -*)
7.162 -(* not only for thydata, but also for thy's etc *)
7.163 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
7.164 - | theID2guh [str] = part2guh [str]
7.165 - | theID2guh [s1, s2] = thy2guh [s1, s2]
7.166 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
7.167 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
7.168 - "Theorems" => thm2guh (isa, thyID) elemID
7.169 - | "Rulesets" => rls2guh (isa, thyID) elemID
7.170 - | "Calculations" => cal2guh (isa, thyID) elemID
7.171 - | "Orders" => ord2guh (isa, thyID) elemID
7.172 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
7.173 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
7.174 -(*\------- to Celem8 -------/*)
7.175 -
7.176 -(*/------- to Celem8 -------\*)
7.177 -(* not only for thydata, but also for thy's etc *)
7.178 -fun theID2guh [] = raise ERROR ("theID2guh: called with []")
7.179 - | theID2guh [str] = part2guh [str]
7.180 - | theID2guh [s1, s2] = thy2guh [s1, s2]
7.181 - | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
7.182 - | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
7.183 - "Theorems" => thm2guh (isa, thyID) elemID
7.184 - | "Rulesets" => rls2guh (isa, thyID) elemID
7.185 - | "Calculations" => cal2guh (isa, thyID) elemID
7.186 - | "Orders" => ord2guh (isa, thyID) elemID
7.187 - | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
7.188 - | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
7.189 -(*\------- to Celem8 -------/*)
7.190 -(*/------- to Celem8 -------\*)
7.191 -fun Html_default exist = (Html {guh = theID2guh exist,
7.192 - coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
7.193 -
7.194 -fun fill_parents (_, [i]) thydata = Store.Ptyp (i, [thydata], [])
7.195 - | fill_parents (exist, i :: is) thydata =
7.196 - Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
7.197 - | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
7.198 -
7.199 -fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
7.200 - | add_thydata (exist, [i]) data (pys as (py as Store.Ptyp (key, _, _)) :: pyss) =
7.201 - if i = key
7.202 - then pys (* preserve existing thydata *)
7.203 - else py :: add_thydata (exist, [i]) data pyss
7.204 - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Ptyp (key, d, pys)) :: pyss) =
7.205 - if i = key
7.206 - then
7.207 - if length pys = 0
7.208 - then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
7.209 - else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
7.210 - else py :: add_thydata (exist, iss) data pyss
7.211 - | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
7.212 -
7.213 -fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
7.214 - Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
7.215 - fillpats = fillpats', thm = thm}
7.216 - | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
7.217 -(*\------- to Celem8 -------/*)
7.218 -
7.219 -(**)end(**)
8.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 15:54:19 2020 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 16:47:01 2020 +0200
8.3 @@ -13,7 +13,7 @@
8.4 val check_guhs_unique: bool Unsynchronized.ref
8.5 (*val collect *)
8.6 val collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
8.7 - val messsage: ('a -> guh list) -> guh -> 'a -> unit;
8.8 + val message: ('a -> guh list) -> guh -> 'a -> unit;
8.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.10 (*NONE*)
8.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.12 @@ -45,7 +45,7 @@
8.13 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
8.14 in nodes [] pbls end;
8.15
8.16 -fun messsage select guh store =
8.17 +fun message select guh store =
8.18 if member op = (select store) guh
8.19 then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
8.20 "use \"sort_guhs()\" for a list of guhs;\n" ^
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Mon Apr 20 16:47:01 2020 +0200
9.3 @@ -0,0 +1,64 @@
9.4 +(* Title: BaseDefinitions/method-def.sml
9.5 + Author: Walther Neuper
9.6 + (c) due to copyright terms
9.7 +
9.8 +Will be enhanced by Method later.
9.9 +*)
9.10 +signature METHOD_DEFINITION =
9.11 +sig
9.12 + type met
9.13 + val e_met: met
9.14 + type mets
9.15 + val e_Mets: met Store.ptyp
9.16 +(*vvv check_unique*)
9.17 + val check_metguh_unique: Check_Unique.guh -> met Store.ptyp list -> unit
9.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.19 + (*NONE*)
9.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.21 + (*NONE*)
9.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.23 +end
9.24 +
9.25 +(**)
9.26 +structure Meth_Def(**): METHOD_DEFINITION(**) =
9.27 +struct
9.28 +(**)
9.29 +
9.30 +(*/------- to Celem6 -------\*)
9.31 +(* data for methods stored in 'methods'-database*)
9.32 +type met =
9.33 + {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
9.34 + mathauthors: string list, (* copyright *)
9.35 + init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
9.36 + rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
9.37 + TODO.WN0509 store fun itself, see 'type pbt' *)
9.38 + erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
9.39 + instead erls in "fun prep_met" *)
9.40 + srls : Rule_Set.T, (* for evaluating list expressions in scr *)
9.41 + crls : Rule_Set.T, (* for check_elementwise, ie. formulae in calc. *)
9.42 + nrls : Rule_Set.T, (* canonical simplifier specific for this met *)
9.43 + errpats : Error_Fill_Def.errpat list,(* error patterns expected in this method *)
9.44 + calc : Rule_Def.calc list, (* Theory_Data in fun prep_met *)
9.45 + (*branch : TransitiveB set in append_problem at generation ob pblobj *)
9.46 + scr : Rule.program, (* progam, empty as @{thm refl} or Rfuns *)
9.47 +(*TODO: abstract to ?pre_model?...*)
9.48 + prls : Rule_Set.T, (* for evaluating predicates in modelpattern *)
9.49 + ppc : Celem4.pat list, (* items in given, find, relate;
9.50 + items (in "#Find") which need not occur in the arg-list of a SubProblem
9.51 + are 'copy-named' with an identifier "*'.'".
9.52 + copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
9.53 + see ME/calchead.sml 'fun is_copy_named'. *)
9.54 + pre : term list (* preconditions in where *)
9.55 + };
9.56 +val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
9.57 + erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
9.58 + errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
9.59 +val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
9.60 +
9.61 +type mets = (met Store.ptyp) list;
9.62 +(*\------- to Celem6 -------/*)
9.63 +
9.64 +val check_metguh_unique =
9.65 + Check_Unique.message (Check_Unique.collect (#guh: met -> Check_Unique.guh));
9.66 +
9.67 +(**)end(**)
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Apr 20 16:47:01 2020 +0200
10.3 @@ -0,0 +1,65 @@
10.4 +(* Title: BaseDefinitions/problem-def.sml
10.5 + Author: Walther Neuper
10.6 + (c) due to copyright terms
10.7 +
10.8 +Will be enhanced by Problem later.
10.9 +*)
10.10 +signature PROBLEM_DEFINITION =
10.11 +sig
10.12 + type pbt
10.13 + type ptyps
10.14 + val pbts2str: pbt list -> string
10.15 + val e_Ptyp: pbt Store.ptyp
10.16 +(*vvv check_unique*)
10.17 + val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
10.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.19 + val e_pbt: pbt
10.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.21 + (*NONE*)
10.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.23 +end
10.24 +
10.25 +(**)
10.26 +structure Probl_Def(**): PROBLEM_DEFINITION(**) =
10.27 +struct
10.28 +(**)
10.29 +
10.30 +(*/------- to Celem5 -------\*)
10.31 +type pbt =
10.32 + {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
10.33 + mathauthors : string list, (* copyright *)
10.34 + init : Spec.pblID, (* to start refinement with *)
10.35 + thy : theory, (* which allows to compile that pbt
10.36 + TODO: search generalized for subthy (ref.p.69*)
10.37 + (*^^^ WN050912 NOT used during application of the problem,
10.38 + because applied terms may be from 'subthy' as well as from super;
10.39 + thus we take 'maxthy'; see match_ags ! *)
10.40 + cas : term option, (* 'CAS-command' *)
10.41 + met : Spec.metID list, (* methods solving the pbt *)
10.42 +(*TODO: abstract to ?pre_model?...*)
10.43 + prls : Rule_Set.T, (* for preds in where_ *)
10.44 + where_ : term list, (* where - predicates *)
10.45 + ppc : Celem4.pat list (* this is the model-pattern;
10.46 + it contains "#Given","#Where","#Find","#Relate"-patterns
10.47 + for constraints on identifiers see "fun cpy_nam" *)
10.48 +}
10.49 +val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
10.50 + cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
10.51 +fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
10.52 + prls = prls', thy = thy', where_ = w'} : pbt)
10.53 + = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
10.54 + ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
10.55 + ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "
10.56 + ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
10.57 + ^ (UnparseC.terms w') ^ "}" |> linefeed;
10.58 +fun pbts2str pbts = map pbt2str pbts |> list2str;
10.59 +(*\------- to Celem5 -------/*)
10.60 +(*/------- to Celem5 -------\*)
10.61 +val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], [])
10.62 +type ptyps = (pbt Store.ptyp) list
10.63 +(*\------- to Celem5 -------/*)
10.64 +
10.65 +val check_pblguh_unique =
10.66 + Check_Unique.message (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
10.67 +
10.68 +(**)end(**)
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Mon Apr 20 16:47:01 2020 +0200
11.3 @@ -0,0 +1,212 @@
11.4 +(* Title: BaseDefinitions/celem-8.sml
11.5 + Author: Walther Neuper
11.6 + (c) due to copyright terms
11.7 +
11.8 +Legacy for HTML representation of theory data in Isac's Java front end.
11.9 +*)
11.10 +signature HTML_FOR_THEORY_DATA =
11.11 +sig
11.12 + type authors
11.13 + datatype thydata
11.14 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors}
11.15 + | Hord of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
11.16 + | Hrls of {coursedesign: authors, guh: Check_Unique.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
11.17 + | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Check_Unique.guh, mathauthors: authors, thm: thm}
11.18 + | Html of {coursedesign: authors, guh: Check_Unique.guh, html: string, mathauthors: authors}
11.19 + type theID
11.20 + val theID2str: string list -> string
11.21 + val the2str: thydata -> string
11.22 + val thes2str: thydata list -> string
11.23 + val theID2thyID: theID -> ThyC.id
11.24 +
11.25 + val part2guh: theID -> Check_Unique.guh
11.26 + val thy2guh: theID -> Check_Unique.guh
11.27 + val thypart2guh: theID -> Check_Unique.guh
11.28 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Check_Unique.guh
11.29 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Check_Unique.guh
11.30 + val cal2guh: string * ThyC.id -> string -> Check_Unique.guh
11.31 + val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
11.32 + val theID2guh: theID -> Check_Unique.guh
11.33 +
11.34 + val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
11.35 + val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
11.36 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.37 + (*NONE*)
11.38 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.39 + (*NONE*)
11.40 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.41 +end
11.42 +
11.43 +(**)
11.44 +structure Thy_Html(**): HTML_FOR_THEORY_DATA(**) =
11.45 +struct
11.46 +(**)
11.47 +
11.48 +(*/------- to Celem8 -------\*)
11.49 +(*the key into the hierarchy ob theory elements*)
11.50 +type theID = string list;
11.51 +val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
11.52 +fun theID2thyID theID =
11.53 + if length theID >= 3 then (last_elem o (drop_last_n 2)) theID
11.54 + else error ("theID2thyID called with " ^ theID2str theID);
11.55 +type authors = string list;
11.56 +(* datatype for collecting thydata for hierarchy *)
11.57 +(*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
11.58 +datatype thydata =
11.59 + Html of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, html: string}
11.60 +| Hthm of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
11.61 + thm: thm} (* here no sym_thm, thus no thmID required *)
11.62 +| Hrls of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
11.63 +| Hcal of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
11.64 +| Hord of {guh: Check_Unique.guh, coursedesign: authors, mathauthors: authors,
11.65 + ord: (UnparseC.subst -> (term * term) -> bool)};
11.66 +fun the2str (Html {guh, ...}) = guh
11.67 + | the2str (Hthm {guh, ...}) = guh
11.68 + | the2str (Hrls {guh, ...}) = guh
11.69 + | the2str (Hcal {guh, ...}) = guh
11.70 + | the2str (Hord {guh, ...}) = guh
11.71 +fun thes2str thes = map the2str thes |> list2str;
11.72 +(*\------- to Celem8 -------/*)
11.73 +
11.74 +(*/------- to Celem8 -------\*)
11.75 +(* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
11.76 + (a): thehier does not contain sym_thmID theorems
11.77 + (b): lookup for sym_thmID directly from Isabelle using sym_thm
11.78 + (within math-engine NO lookup in thehier -- within java in *.xml only!)
11.79 +TODO (c): export from thehier to xml
11.80 +TODO (c1) creates one entry for "thmID" (and NONE for "sym_thmID") in the hierarchy
11.81 +TODO (c2) creates 2 files "thy_*-thm-thmID.xml" and "thy_*-thm-sym_thmID.xml"
11.82 +TODO (d): 1 entry in the MiniBrowser's hierarchy (generated from xml)
11.83 + stands for both, "thmID" and "sym_thmID"
11.84 +TODO (d1) lookup from calctxt
11.85 +TODO (d1) lookup from from rule set in MiniBrowser *)
11.86 +type thehier = (thydata Store.ptyp) list;
11.87 +(* required to determine sequence of main nodes of thehier in Know_Store.thy *)
11.88 +fun part2guh [str] = (case str of
11.89 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Check_Unique.guh
11.90 + | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
11.91 + | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
11.92 + | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
11.93 + | part2guh theID = raise ERROR ("part2guh called with theID = \"" ^ theID2str theID ^ "'");
11.94 +
11.95 +fun thy2guh [part, thyID] = (case part of
11.96 + "Isabelle" => "thy_isab_" ^ thyID
11.97 + | "IsacScripts" => "thy_scri_" ^ thyID
11.98 + | "IsacKnowledge" => "thy_isac_" ^ thyID
11.99 + | str => raise ERROR ("thy2guh: called with \"" ^ str ^ "\""))
11.100 + | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
11.101 +
11.102 +fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
11.103 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Check_Unique.guh
11.104 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
11.105 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
11.106 + | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
11.107 + | thypart2guh strs = raise ERROR ("thypart2guh called with \"" ^ strs2str' strs ^ "\"");
11.108 +
11.109 +
11.110 +(* convert the data got via contextToThy to a globally unique handle.
11.111 + there is another way to get the guh: get out of the 'theID' in the hierarchy *)
11.112 +fun thm2guh (isa, thyID) thmID = case isa of
11.113 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Check_Unique.guh
11.114 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
11.115 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
11.116 + | _ => raise ERROR
11.117 + ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
11.118 +
11.119 +fun rls2guh (isa, thyID) rls' = case isa of
11.120 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Check_Unique.guh
11.121 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
11.122 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
11.123 + | _ => raise ERROR
11.124 + ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
11.125 +
11.126 +fun cal2guh (isa, thyID) calID = case isa of
11.127 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Check_Unique.guh
11.128 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
11.129 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
11.130 + | _ => raise ERROR
11.131 + ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
11.132 +
11.133 +fun ord2guh (isa, thyID) rew_ord' = case isa of
11.134 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Check_Unique.guh
11.135 + | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
11.136 + | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
11.137 + | _ => raise ERROR
11.138 + ("ord2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for ord = \"" ^ rew_ord' ^ "\"");
11.139 +
11.140 +(* TODO
11.141 +fun theID2guh theID = case length theID of
11.142 + 0 => error ("theID2guh: called with theID = " ^ strs2str' theID)
11.143 + | 1 => part2guh theID
11.144 + | 2 => thy2guh theID
11.145 + | 3 => thypart2guh theID
11.146 + | 4 =>
11.147 + let val [isa, thyID, typ, elemID] = theID
11.148 + in case typ of
11.149 + "Theorems" => thm2guh (isa, thyID) elemID
11.150 + | "Rulesets" => rls2guh (isa, thyID) elemID
11.151 + | "Calculations" => cal2guh (isa, thyID) elemID
11.152 + | "Orders" => ord2guh (isa, thyID) elemID
11.153 + | "Theorems" => thy2guh [isa, thyID]
11.154 + | str => raise ERROR ("theID2guh: called with theID = " ^ strs2str' theID)
11.155 + end
11.156 + | n => raise ERROR ("theID2guh called with theID = " ^ strs2str' theID);
11.157 +*)
11.158 +(* not only for thydata, but also for thy's etc *)
11.159 +fun theID2guh [] = raise ERROR ("theID2guh: called with []")
11.160 + | theID2guh [str] = part2guh [str]
11.161 + | theID2guh [s1, s2] = thy2guh [s1, s2]
11.162 + | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
11.163 + | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
11.164 + "Theorems" => thm2guh (isa, thyID) elemID
11.165 + | "Rulesets" => rls2guh (isa, thyID) elemID
11.166 + | "Calculations" => cal2guh (isa, thyID) elemID
11.167 + | "Orders" => ord2guh (isa, thyID) elemID
11.168 + | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
11.169 + | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
11.170 +(*\------- to Celem8 -------/*)
11.171 +
11.172 +(*/------- to Celem8 -------\*)
11.173 +(* not only for thydata, but also for thy's etc *)
11.174 +fun theID2guh [] = raise ERROR ("theID2guh: called with []")
11.175 + | theID2guh [str] = part2guh [str]
11.176 + | theID2guh [s1, s2] = thy2guh [s1, s2]
11.177 + | theID2guh [s1, s2, s3] = thypart2guh [s1, s2, s3]
11.178 + | theID2guh (strs as [isa, thyID, typ, elemID]) = (case typ of
11.179 + "Theorems" => thm2guh (isa, thyID) elemID
11.180 + | "Rulesets" => rls2guh (isa, thyID) elemID
11.181 + | "Calculations" => cal2guh (isa, thyID) elemID
11.182 + | "Orders" => ord2guh (isa, thyID) elemID
11.183 + | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
11.184 + | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
11.185 +(*\------- to Celem8 -------/*)
11.186 +(*/------- to Celem8 -------\*)
11.187 +fun Html_default exist = (Html {guh = theID2guh exist,
11.188 + coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
11.189 +
11.190 +fun fill_parents (_, [i]) thydata = Store.Ptyp (i, [thydata], [])
11.191 + | fill_parents (exist, i :: is) thydata =
11.192 + Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
11.193 + | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
11.194 +
11.195 +fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
11.196 + | add_thydata (exist, [i]) data (pys as (py as Store.Ptyp (key, _, _)) :: pyss) =
11.197 + if i = key
11.198 + then pys (* preserve existing thydata *)
11.199 + else py :: add_thydata (exist, [i]) data pyss
11.200 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Ptyp (key, d, pys)) :: pyss) =
11.201 + if i = key
11.202 + then
11.203 + if length pys = 0
11.204 + then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
11.205 + else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
11.206 + else py :: add_thydata (exist, iss) data pyss
11.207 + | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
11.208 +
11.209 +fun update_hthm (Hthm {guh, coursedesign, mathauthors, thm, ...}) fillpats' =
11.210 + Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
11.211 + fillpats = fillpats', thm = thm}
11.212 + | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
11.213 +(*\------- to Celem8 -------/*)
11.214 +
11.215 +(**)end(**)
12.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Apr 20 15:54:19 2020 +0200
12.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Mon Apr 20 16:47:01 2020 +0200
12.3 @@ -437,7 +437,7 @@
12.4 type ocalhd =
12.5 bool * (* ALL itms+preconds true *)
12.6 pos_ * (* model belongs to Problem | Method *)
12.7 - term * (* header: Problem... or Cas FIXME.0312: item for marking syntaxerrors *)
12.8 + term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*)
12.9 Model.itm list * (* model: given, find, relate *)
12.10 ((bool * term) list) *(* model: preconds *)
12.11 Celem.spec; (* specification *)
13.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 15:54:19 2020 +0200
13.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 16:47:01 2020 +0200
13.3 @@ -38,9 +38,9 @@
13.4 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
13.5 in nodes [] pbls end;
13.6
13.7 -collect: ('a -> 'b) -> 'a ptyp list -> 'b list;
13.8 -collect pbl_select_guh: pbt ptyp list -> guh list;
13.9 -collect met_select_guh: met ptyp list -> guh list;
13.10 +collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
13.11 +collect pbl_select_guh: pbt Store.ptyp list -> guh list;
13.12 +collect met_select_guh: met Store.ptyp list -> guh list;
13.13
13.14 fun message select store guh =
13.15 if member op = (select store) guh
13.16 @@ -50,15 +50,15 @@
13.17 else ();
13.18
13.19 message: ('a -> guh list ) -> 'a -> guh -> unit;
13.20 -(message (collect pbl_select_guh)): pbt ptyp list -> guh -> unit;
13.21 -(message (collect met_select_guh)): met ptyp list -> guh -> unit;
13.22 +(message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
13.23 +(message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
13.24
13.25 -(Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh)): pbt ptyp list -> guh list;
13.26 -(Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh)): met ptyp list -> guh list;
13.27 +(Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
13.28 +(Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
13.29
13.30 -val check_pblguh_unique = messsage (Check_Unique.collect (#guh : Celem5.pbt -> Check_Unique.guh));
13.31 -check_pblguh_unique: pbt ptyp list -> guh -> unit
13.32 +val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh));
13.33 +check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
13.34 ;
13.35 -val check_metguh_unique = messsage (Check_Unique.collect (#guh : Celem6.met -> Check_Unique.guh));
13.36 -check_metguh_unique: met ptyp list -> guh -> unit
13.37 +val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
13.38 +check_metguh_unique: met Store.ptyp list -> guh -> unit
13.39 ;
13.40 \ No newline at end of file
14.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Apr 20 15:54:19 2020 +0200
14.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 20 16:47:01 2020 +0200
14.3 @@ -188,6 +188,84 @@
14.4 ML_file "BaseDefinitions/error-fill-def.sml"
14.5 ML_file "BaseDefinitions/rule-set.sml"
14.6 ML_file "BaseDefinitions/check-unique.sml"
14.7 +ML \<open>
14.8 +\<close> ML \<open>
14.9 +\<close> ML \<open>
14.10 +\<close> ML \<open>
14.11 +(* Title: "BaseDefinitions/check-unique.sml"
14.12 + Author: Walther Neuper
14.13 + (c) due to copyright terms
14.14 +*)
14.15 +
14.16 +"-----------------------------------------------------------------------------------------------";
14.17 +"table of contents -----------------------------------------------------------------------------";
14.18 +"-----------------------------------------------------------------------------------------------";
14.19 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
14.20 +"-----------------------------------------------------------------------------------------------";
14.21 +"-----------------------------------------------------------------------------------------------";
14.22 +"-----------------------------------------------------------------------------------------------";
14.23 +
14.24 +
14.25 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
14.26 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
14.27 +"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
14.28 +(*------- auxiliary format for fn*)
14.29 +fun pbl_select_guh pbt =
14.30 + let
14.31 + val {guh, ...} = (**)(pbt: pbt)(** )(pbt: met)( **)
14.32 + in guh end;
14.33 +pbl_select_guh: pbt -> guh;(**)
14.34 +
14.35 +fun met_select_guh pbt =
14.36 + let
14.37 + val {guh, ...} = (pbt: met)
14.38 + in guh end;
14.39 +met_select_guh: met -> guh;(**)
14.40 +
14.41 +(*------- hint: build higher order functions be replacing the selector by a variable argument *)
14.42 +(* collect*)
14.43 +fun collect select_guh pbls =
14.44 + let
14.45 + fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
14.46 + | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
14.47 + and nodes coll [] = coll
14.48 + | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
14.49 + in nodes [] pbls end;
14.50 +
14.51 +\<close> ML \<open>
14.52 +collect
14.53 +\<close> ML \<open>
14.54 +collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
14.55 +collect pbl_select_guh: pbt Store.ptyp list -> guh list;
14.56 +collect met_select_guh: met Store.ptyp list -> guh list;
14.57 +
14.58 +fun message select store guh =
14.59 + if member op = (select store) guh
14.60 + then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
14.61 + "use \"sort_guhs()\" for a list of guhs;\n" ^
14.62 + "consider setting \"Check_Unique.on := false\"")
14.63 + else ();
14.64 +
14.65 + message: ('a -> guh list ) -> 'a -> guh -> unit;
14.66 +(message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
14.67 +(message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
14.68 +
14.69 +(Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
14.70 +(Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
14.71 +
14.72 +val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh));
14.73 +check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
14.74 +;
14.75 +val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
14.76 +check_metguh_unique: met Store.ptyp list -> guh -> unit
14.77 +;\<close> ML \<open>
14.78 +\<close> ML \<open>
14.79 +\<close> ML \<open>
14.80 +\<close> ML \<open>
14.81 +\<close> ML \<open>
14.82 +\<close> ML \<open>
14.83 +\<close> ML \<open>
14.84 +\<close>
14.85 ML_file "BaseDefinitions/calcelems.sml"
14.86 ML_file "BaseDefinitions/termC.sml"
14.87 ML_file "BaseDefinitions/contextC.sml"