1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 15:51:31 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 16:17:27 2020 +0200
1.3 @@ -1,6 +1,11 @@
1.4 (* Title: src/Tools/isac/Know_Store.thy
1.5 Author: Mathias Lehnfeld
1.6
1.7 +Calc work on Problem employing Method; both are collected in a respective Store;
1.8 +The collections' structure is independent from the dependency graph of Isabelle's theories
1.9 +in Knowledge.
1.10 +Store is also used by Thy_Html, required for Isac's Java front end, irrelevant for PIDE.
1.11 +
1.12 The files (in "xxxxx-def.sml") contain definitions required for Know_Store;
1.13 they also include minimal code required for other "xxxxx-def.sml" files.
1.14 These files have companion files "xxxxx.sml" with all further code,
1.15 @@ -67,7 +72,7 @@
1.16 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
1.17 val get_mets: theory -> Celem6.mets
1.18 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
1.19 - val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
1.20 + val get_thes: theory -> (Celem8.thydata Store.ptyp) list
1.21 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.22 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.23 val get_ref_thy: unit -> theory
1.24 @@ -109,34 +114,34 @@
1.25 type T = Celem5.ptyps;
1.26 val empty = [Celem5.e_Ptyp];
1.27 val extend = I;
1.28 - val merge = Celem1.merge_ptyps;
1.29 + val merge = Store.merge_ptyps;
1.30 );
1.31 fun get_ptyps thy = Data.get thy;
1.32 fun add_pbts pbts thy = let
1.33 fun add_pbt (pbt as {guh,...}, pblID) =
1.34 (* the pblID has the leaf-element as first; better readability achieved *)
1.35 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
1.36 - rev pblID |> Celem1.insrt pblID pbt);
1.37 + rev pblID |> Store.insrt pblID pbt);
1.38 in Data.map (fold add_pbt pbts) thy end;
1.39
1.40 structure Data = Theory_Data (
1.41 type T = Celem6.mets;
1.42 val empty = [Celem6.e_Mets];
1.43 val extend = I;
1.44 - val merge = Celem1.merge_ptyps;
1.45 + val merge = Store.merge_ptyps;
1.46 );
1.47 val get_mets = Data.get;
1.48 fun add_mets mets thy = let
1.49 fun add_met (met as {guh,...}, metID) =
1.50 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
1.51 - Celem1.insrt metID met metID);
1.52 + Store.insrt metID met metID);
1.53 in Data.map (fold add_met mets) thy end;
1.54
1.55 structure Data = Theory_Data (
1.56 - type T = (Celem8.thydata Celem1.ptyp) list;
1.57 + type T = (Celem8.thydata Store.ptyp) list;
1.58 val empty = [];
1.59 val extend = I;
1.60 - val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
1.61 + val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
1.62 );
1.63 fun get_thes thy = Data.get thy
1.64 fun add_thes thes thy = let
1.65 @@ -146,11 +151,11 @@
1.66 let
1.67 fun update_elem (theID, fillpats) =
1.68 let
1.69 - val hthm = Celem1.get_py (Data.get thy) theID theID
1.70 + val hthm = Store.get_py (Data.get thy) theID theID
1.71 val hthm' = Celem8.update_hthm hthm fillpats
1.72 handle ERROR _ =>
1.73 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.74 - in Celem1.update_ptyps theID theID hthm' end
1.75 + in Store.update_ptyps theID theID hthm' end
1.76 in Data.map (fold update_elem fis) thy end
1.77
1.78 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.79 @@ -235,21 +240,21 @@
1.80 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
1.81
1.82 fun count_kestore_ptyps [] = 0
1.83 - | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
1.84 + | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
1.85 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.86 -fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.87 +fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.88 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.89 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
1.90 -fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.91 +fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.92 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
1.93 fun sort_kestore_ptyp' _ [] = []
1.94 - | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
1.95 - ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.96 + | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
1.97 + ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.98 :: sort_kestore_ptyp' ordfun ps');
1.99 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.100
1.101 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
1.102 -fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
1.103 +fun check_kestore_met (mp: Celem6.met Store.ptyp) =
1.104 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.105 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
1.106 val sort_kestore_met = sort_kestore_ptyp' met_ord;
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 15:51:31 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 16:17:27 2020 +0200
2.3 @@ -18,7 +18,7 @@
2.4 (*/------- to Celem5 -------\*)
2.5 type pbt = Celem5.pbt
2.6 val e_pbt: pbt;
2.7 - val e_Ptyp: pbt Celem1.ptyp
2.8 + val e_Ptyp: pbt Store.ptyp
2.9 type ptyps = Celem5.ptyps
2.10 val pbts2str: pbt list -> string
2.11 (*\------- to Celem5 -------/*)
2.12 @@ -35,14 +35,14 @@
2.13 val e_spec: spec
2.14 (*\------- to Celem3 -------/*)
2.15
2.16 -(*/------- to Celem1 -------\*)
2.17 +(*/------- to Store -------\*)
2.18 (*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*)
2.19 - val merge_ptyps: 'a Celem1.ptyp list * 'a Celem1.ptyp list -> 'a Celem1.ptyp list
2.20 - val insrt: pblID -> 'a -> string list -> 'a Celem1.ptyp list -> 'a Celem1.ptyp list
2.21 - val get_py: 'a Celem1.ptyp list -> pblID -> string list -> 'a
2.22 - val update_ptyps: string list -> string list -> 'a -> 'a Celem1.ptyp list -> 'a Celem1.ptyp list
2.23 - val app_py: 'a Celem1.ptyp list -> ('a Celem1.ptyp -> 'b) -> pblID -> string list -> 'b
2.24 -(*\------- to Celem1 -------/*)
2.25 + val merge_ptyps: 'a Store.ptyp list * 'a Store.ptyp list -> 'a Store.ptyp list
2.26 + val insrt: pblID -> 'a -> string list -> 'a Store.ptyp list -> 'a Store.ptyp list
2.27 + val get_py: 'a Store.ptyp list -> pblID -> string list -> 'a
2.28 + val update_ptyps: string list -> string list -> 'a -> 'a Store.ptyp list -> 'a Store.ptyp list
2.29 + val app_py: 'a Store.ptyp list -> ('a Store.ptyp -> 'b) -> pblID -> string list -> 'b
2.30 +(*\------- to Store -------/*)
2.31
2.32 (*/------- to Celem2 -------\*)
2.33 type guh
2.34 @@ -66,22 +66,22 @@
2.35 val ord2guh: string * ThyC.id -> string -> string
2.36 val theID2guh: theID -> guh
2.37
2.38 - val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list
2.39 + val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
2.40 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
2.41 (*\------- to Celem8 -------/*)
2.42
2.43 (*/------- to Celem6 -------\*)
2.44 type met = Celem6.met
2.45 type mets = Celem6.mets
2.46 - val e_Mets: met Celem1.ptyp
2.47 + val e_Mets: met Store.ptyp
2.48 (*\------- to Celem6 -------/*)
2.49
2.50 (*/------- to Celem91 -------\*)
2.51 val check_guhs_unique: bool Unsynchronized.ref
2.52 - val coll_pblguhs: pbt Celem1.ptyp list -> guh list
2.53 - val check_pblguh_unique: guh -> pbt Celem1.ptyp list -> unit
2.54 - val coll_metguhs: met Celem1.ptyp list -> guh list
2.55 - val check_metguh_unique: guh -> met Celem1.ptyp list -> unit
2.56 + val coll_pblguhs: pbt Store.ptyp list -> guh list
2.57 + val check_pblguh_unique: guh -> pbt Store.ptyp list -> unit
2.58 + val coll_metguhs: met Store.ptyp list -> guh list
2.59 + val check_metguh_unique: guh -> met Store.ptyp list -> unit
2.60 (*\------- to Celem91 -------/*)
2.61
2.62 val linefeed: string -> string
2.63 @@ -111,8 +111,8 @@
2.64
2.65 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.66 val pats2str' : pat list -> string
2.67 - val insert_fillpats: thydata Celem1.ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata Celem1.ptyp list ->
2.68 - thydata Celem1.ptyp list
2.69 + val insert_fillpats: thydata Store.ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata Store.ptyp list ->
2.70 + thydata Store.ptyp list
2.71 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.72 val knowthys: unit -> theory list
2.73 (*/------- to Celem6 -------\*)
2.74 @@ -206,13 +206,13 @@
2.75 | str2ketype' "met" = Met_
2.76 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
2.77
2.78 -(*/------- to Celem1 -------\*)
2.79 -val merge_ptyps = Celem1.merge_ptyps;
2.80 -val insrt = Celem1.insrt;
2.81 -val app_py = Celem1.app_py;
2.82 -val get_py = Celem1.get_py;
2.83 -val update_ptyps = Celem1.update_ptyps;
2.84 -(*\------- to Celem1 -------/*)
2.85 +(*/------- to Store -------\*)
2.86 +val merge_ptyps = Store.merge_ptyps;
2.87 +val insrt = Store.insrt;
2.88 +val app_py = Store.app_py;
2.89 +val get_py = Store.get_py;
2.90 +val update_ptyps = Store.update_ptyps;
2.91 +(*\------- to Store -------/*)
2.92
2.93 (*/------- to Celem8 -------\*)
2.94 type authors = Celem8.authors;
2.95 @@ -291,7 +291,7 @@
2.96 type met = Celem6.met;
2.97 val e_met = Celem6.e_met;
2.98 val e_Mets = Celem6.e_Mets;
2.99 -type mets = (met Celem1.ptyp) list;
2.100 +type mets = (met Store.ptyp) list;
2.101 (*\------- to Celem6 -------/*)
2.102
2.103 (*/------- to Celem91 -------\*)
2.104 @@ -306,22 +306,22 @@
2.105 fun Html_default exist = (Html {guh = theID2guh exist,
2.106 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
2.107
2.108 -fun fill_parents (_, [i]) thydata = Celem1.Ptyp (i, [thydata], [])
2.109 +fun fill_parents (_, [i]) thydata = Store.Ptyp (i, [thydata], [])
2.110 | fill_parents (exist, i :: is) thydata =
2.111 - Celem1.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
2.112 + Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
2.113 | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
2.114
2.115 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
2.116 - | add_thydata (exist, [i]) data (pys as (py as Celem1.Ptyp (key, _, _)) :: pyss) =
2.117 + | add_thydata (exist, [i]) data (pys as (py as Store.Ptyp (key, _, _)) :: pyss) =
2.118 if i = key
2.119 then pys (* preserve existing thydata *)
2.120 else py :: add_thydata (exist, [i]) data pyss
2.121 - | add_thydata (exist, iss as (i :: is)) data ((py as Celem1.Ptyp (key, d, pys)) :: pyss) =
2.122 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Ptyp (key, d, pys)) :: pyss) =
2.123 if i = key
2.124 then
2.125 if length pys = 0
2.126 - then Celem1.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
2.127 - else Celem1.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
2.128 + then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
2.129 + else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
2.130 else py :: add_thydata (exist, iss) data pyss
2.131 | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
2.132
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 15:51:31 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 16:17:27 2020 +0200
3.3 @@ -25,7 +25,7 @@
3.4 val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
3.5 val get_mets: theory -> Celem6.mets
3.6 val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
3.7 - val get_thes: theory -> (Celem8.thydata Celem1.ptyp) list
3.8 + val get_thes: theory -> (Celem8.thydata Store.ptyp) list
3.9 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
3.10 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
3.11 type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
3.12 @@ -33,35 +33,35 @@
3.13 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
3.14 type T = Celem5.ptyps;
3.15 val empty = [Celem5.e_Ptyp];
3.16 - val merge = Celem1.merge_ptyps;
3.17 + val merge = Store.merge_ptyps;
3.18 (if (!Celem91.check_guhs_unique) then Celem91.check_pblguh_unique guh (Data.get thy) else ();
3.19 - rev pblID |> Celem1.insrt pblID pbt);
3.20 + rev pblID |> Store.insrt pblID pbt);
3.21 type T = Celem6.mets;
3.22 val empty = [Celem6.e_Mets];
3.23 - val merge = Celem1.merge_ptyps;
3.24 + val merge = Store.merge_ptyps;
3.25 (if (!Celem91.check_guhs_unique) then Celem91.check_metguh_unique guh (Data.get thy) else ();
3.26 - Celem1.insrt metID met metID);
3.27 - type T = (Celem8.thydata Celem1.ptyp) list;
3.28 - val merge = Celem1.merge_ptyps; (* relevant for store_thm, store_rls *)
3.29 + Store.insrt metID met metID);
3.30 + type T = (Celem8.thydata Store.ptyp) list;
3.31 + val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
3.32 fun add_the (thydata, theID) = Celem8.add_thydata ([], theID) thydata
3.33 - val hthm = Celem1.get_py (Data.get thy) theID theID
3.34 + val hthm = Store.get_py (Data.get thy) theID theID
3.35 val hthm' = Celem8.update_hthm hthm fillpats
3.36 - in Celem1.update_ptyps theID theID hthm' end
3.37 + in Store.update_ptyps theID theID hthm' end
3.38 [(Celem8.Html {guh = Celem8.part2guh ["IsacKnowledge"], html = "",
3.39 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
3.40 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
3.41 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
3.42 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
3.43 - | count_kestore_ptyps ((Celem1.Ptyp (_, _, ps)) :: ps') =
3.44 -fun check_kestore_ptyp' strfun (Celem1.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
3.45 + | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
3.46 +fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
3.47 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
3.48 val check_kestore_ptyp = check_kestore_ptyp' Celem5.pbts2str;
3.49 -fun ptyp_ord ((Celem1.Ptyp (s1, _, _)), (Celem1.Ptyp (s2, _, _))) = string_ord (s1, s2);
3.50 +fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
3.51 fun pbt_ord ({guh = guh'1, ...} : Celem5.pbt, {guh = guh'2, ...} : Celem5.pbt) = string_ord (guh'1, guh'2);
3.52 - | sort_kestore_ptyp' ordfun ((Celem1.Ptyp (key, pbts, ps)) :: ps') =
3.53 - ((Celem1.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
3.54 + | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
3.55 + ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
3.56 fun metguh2str ({guh,...} : Celem6.met) = guh : string;
3.57 -fun check_kestore_met (mp: Celem6.met Celem1.ptyp) =
3.58 +fun check_kestore_met (mp: Celem6.met Store.ptyp) =
3.59 fun met_ord ({guh = guh'1, ...} : Celem6.met, {guh = guh'2, ...} : Celem6.met) = string_ord (guh'1, guh'2);
3.60 fun check_kestore_thes thes = ((map writeln) o (map (check_kestore_ptyp' Celem8.thes2str))) thes
3.61 |> map (fn (id, the) => (Celem8.theID2str id, Celem8.the2str the))
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-1.sml Sun Apr 19 15:51:31 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/celem-1.sml Sun Apr 19 16:17:27 2020 +0200
4.3 @@ -3,18 +3,18 @@
4.4 (c) due to copyright terms
4.5
4.6 *)
4.7 -signature CALCELEMENT_1 =
4.8 -(*/------- to Celem1 -------\*)
4.9 -(*\------- to Celem1 -------/*)
4.10 +signature STORE_TREE =
4.11 +(*/------- to Store -------\*)
4.12 +(*\------- to Store -------/*)
4.13 sig
4.14 -(*/------- to Celem1 -------\*)
4.15 +(*/------- to Store -------\*)
4.16 datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
4.17 val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
4.18 val insrt: (*pblID*)string list -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
4.19 val get_py: 'a ptyp list -> (*pblID*)string list -> string list -> 'a
4.20 val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
4.21 val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> (*pblID*)string list -> string list -> 'b
4.22 -(*\------- to Celem1 -------/*)
4.23 +(*\------- to Store -------/*)
4.24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.25 (*NONE*)
4.26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.27 @@ -23,11 +23,11 @@
4.28 end
4.29
4.30 (**)
4.31 -structure Celem1(**): CALCELEMENT_1(**) =
4.32 +structure Store(**): STORE_TREE(**) =
4.33 struct
4.34 (**)
4.35
4.36 -(*/------- to Celem1 -------\*)
4.37 +(*/------- to Store -------\*)
4.38 (* A tree for storing data defined in different theories
4.39 for access from the Interpreter and from dialogue authoring
4.40 using a string list as key.
4.41 @@ -95,6 +95,6 @@
4.42 then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
4.43 else (py :: (update_ptyps ID (i :: is) data pyss))
4.44 | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
4.45 -(*\------- to Celem1 -------/*)
4.46 +(*\------- to Store -------/*)
4.47
4.48 (**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 15:51:31 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 16:17:27 2020 +0200
5.3 @@ -11,7 +11,7 @@
5.4 type pbt
5.5 type ptyps
5.6 val pbts2str: pbt list -> string
5.7 - val e_Ptyp: pbt Celem1.ptyp
5.8 + val e_Ptyp: pbt Store.ptyp
5.9 (*\------- to Celem5 -------/*)
5.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.11 val e_pbt: pbt
5.12 @@ -56,8 +56,8 @@
5.13 fun pbts2str pbts = map pbt2str pbts |> list2str;
5.14 (*\------- to Celem5 -------/*)
5.15 (*/------- to Celem5 -------\*)
5.16 -val e_Ptyp = Celem1.Ptyp ("e_pblID", [e_pbt], [])
5.17 -type ptyps = (pbt Celem1.ptyp) list
5.18 +val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], [])
5.19 +type ptyps = (pbt Store.ptyp) list
5.20 (*\------- to Celem5 -------/*)
5.21
5.22 (**)end(**)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 15:51:31 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 16:17:27 2020 +0200
6.3 @@ -11,7 +11,7 @@
6.4 type met
6.5 val e_met: met
6.6 type mets
6.7 - val e_Mets: met Celem1.ptyp
6.8 + val e_Mets: met Store.ptyp
6.9 (*\------- to Celem6 -------/*)
6.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.11 (*NONE*)
6.12 @@ -54,9 +54,9 @@
6.13 val e_met = {guh = "met_empty", mathauthors = [], init = Celem3.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
6.14 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
6.15 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
6.16 -val e_Mets = Celem1.Ptyp ("e_metID", [e_met],[]);
6.17 +val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
6.18
6.19 -type mets = (met Celem1.ptyp) list;
6.20 +type mets = (met Store.ptyp) list;
6.21 (*\------- to Celem6 -------/*)
6.22
6.23 (**)end(**)
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 15:51:31 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 16:17:27 2020 +0200
7.3 @@ -30,7 +30,7 @@
7.4 val ord2guh: string * ThyC.id -> string -> Celem2.guh
7.5 val theID2guh: theID -> Celem2.guh
7.6
7.7 - val add_thydata: string list * string list -> thydata -> thydata Celem1.ptyp list -> thydata Celem1.ptyp list
7.8 + val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
7.9 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
7.10 (*\------- to Celem8 -------/*)
7.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.12 @@ -83,7 +83,7 @@
7.13 stands for both, "thmID" and "sym_thmID"
7.14 TODO (d1) lookup from calctxt
7.15 TODO (d1) lookup from from rule set in MiniBrowser *)
7.16 -type thehier = (thydata Celem1.ptyp) list;
7.17 +type thehier = (thydata Store.ptyp) list;
7.18 (* required to determine sequence of main nodes of thehier in Know_Store.thy *)
7.19 fun part2guh [str] = (case str of
7.20 "Isabelle" => "thy_isab_" ^ str ^ "-part" : Celem2.guh
7.21 @@ -188,22 +188,22 @@
7.22 fun Html_default exist = (Html {guh = theID2guh exist,
7.23 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
7.24
7.25 -fun fill_parents (_, [i]) thydata = Celem1.Ptyp (i, [thydata], [])
7.26 +fun fill_parents (_, [i]) thydata = Store.Ptyp (i, [thydata], [])
7.27 | fill_parents (exist, i :: is) thydata =
7.28 - Celem1.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
7.29 + Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
7.30 | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
7.31
7.32 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
7.33 - | add_thydata (exist, [i]) data (pys as (py as Celem1.Ptyp (key, _, _)) :: pyss) =
7.34 + | add_thydata (exist, [i]) data (pys as (py as Store.Ptyp (key, _, _)) :: pyss) =
7.35 if i = key
7.36 then pys (* preserve existing thydata *)
7.37 else py :: add_thydata (exist, [i]) data pyss
7.38 - | add_thydata (exist, iss as (i :: is)) data ((py as Celem1.Ptyp (key, d, pys)) :: pyss) =
7.39 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Ptyp (key, d, pys)) :: pyss) =
7.40 if i = key
7.41 then
7.42 if length pys = 0
7.43 - then Celem1.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
7.44 - else Celem1.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
7.45 + then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
7.46 + else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
7.47 else py :: add_thydata (exist, iss) data pyss
7.48 | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
7.49
8.1 --- a/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 15:51:31 2020 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 16:17:27 2020 +0200
8.3 @@ -9,10 +9,10 @@
8.4 sig
8.5 (*/------- to Celem91 -------\*)
8.6 val check_guhs_unique: bool Unsynchronized.ref
8.7 - val check_pblguh_unique: Celem2.guh -> Celem5.pbt Celem1.ptyp list -> unit
8.8 - val check_metguh_unique: Celem2.guh -> Celem6.met Celem1.ptyp list -> unit
8.9 - val coll_pblguhs: Celem5.pbt Celem1.ptyp list -> Celem2.guh list
8.10 - val coll_metguhs: Celem6.met Celem1.ptyp list -> Celem2.guh list
8.11 + val check_pblguh_unique: Celem2.guh -> Celem5.pbt Store.ptyp list -> unit
8.12 + val check_metguh_unique: Celem2.guh -> Celem6.met Store.ptyp list -> unit
8.13 + val coll_pblguhs: Celem5.pbt Store.ptyp list -> Celem2.guh list
8.14 + val coll_metguhs: Celem6.met Store.ptyp list -> Celem2.guh list
8.15 (*\------- to Celem91 -------/*)
8.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.17 (*NONE*)
8.18 @@ -34,7 +34,7 @@
8.19
8.20 fun coll_pblguhs pbls =
8.21 let
8.22 - fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Celem2.guh) n] @ (nodes coll ns)
8.23 + fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Celem2.guh) n] @ (nodes coll ns)
8.24 | node _ _ = raise ERROR "coll_pblguhs - node"
8.25 and nodes coll [] = coll
8.26 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
8.27 @@ -47,12 +47,12 @@
8.28 else ();
8.29 fun coll_metguhs mets =
8.30 let
8.31 - fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Celem2.guh) n] @ (nodes coll ns)
8.32 + fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Celem2.guh) n] @ (nodes coll ns)
8.33 | node _ _ = raise ERROR "coll_pblguhs - node"
8.34 and nodes coll [] = coll
8.35 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
8.36 in nodes [] mets end;
8.37 -fun check_metguh_unique (guh: Celem2.guh) (mets: (Celem6.met Celem1.ptyp) list) =
8.38 +fun check_metguh_unique (guh: Celem2.guh) (mets: (Celem6.met Store.ptyp) list) =
8.39 if member op = (coll_metguhs mets) guh
8.40 then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
8.41 (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
9.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 15:51:31 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 16:17:27 2020 +0200
9.3 @@ -33,7 +33,7 @@
9.4 (*old version with pos2filename*)
9.5 fun hierarchy pm(*"pbl" | "met"*) h =
9.6 let val j = indentation
9.7 - fun nd i p (Celem1.Ptyp (id,_,ns)) =
9.8 + fun nd i p (Store.Ptyp (id,_,ns)) =
9.9 let val p' = Pos.lev_on p
9.10 in (indt i) ^ "<NODE>\n" ^
9.11 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.12 @@ -50,7 +50,7 @@
9.13 (*.create a hierarchy with references to the guh's.*)
9.14 fun hierarchy_pbl h =
9.15 let val j = indentation
9.16 - fun nd i p (Celem1.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
9.17 + fun nd i p (Store.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
9.18 let val p' = Pos.lev_on p
9.19 in (indt i) ^ "<NODE>\n" ^
9.20 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.21 @@ -66,7 +66,7 @@
9.22 in nds j [0] h : Celem.xml end;
9.23 fun hierarchy_met h =
9.24 let val j = indentation
9.25 - fun nd i p (Celem1.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
9.26 + fun nd i p (Store.Ptyp (id,[n as {guh,...} : Celem.met],ns)) =
9.27 let val p' = Pos.lev_on p
9.28 in (indt i) ^ "<NODE>\n" ^
9.29 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
9.30 @@ -264,7 +264,7 @@
9.31 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
9.32
9.33 (*.scan the mtree Ptyp and print the nodes using wfn.*)
9.34 -fun node (pa: Celem.filepath) ids po wfn (Celem1.Ptyp (id,[n],ns)) =
9.35 +fun node (pa: Celem.filepath) ids po wfn (Store.Ptyp (id,[n],ns)) =
9.36 let val po' = Pos.lev_on po
9.37 in
9.38 wfn pa po' (ids@[id]) n;
10.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 15:51:31 2020 +0200
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 16:17:27 2020 +0200
10.3 @@ -14,7 +14,7 @@
10.4 (Celem.theID * Celem.thydata) list
10.5 val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list
10.6
10.7 - val hierarchy_guh: 'a Celem1.ptyp list -> string
10.8 + val hierarchy_guh: 'a Store.ptyp list -> string
10.9 val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->
10.10 Celem.thydata * Celem.theID
10.11
10.12 @@ -46,9 +46,9 @@
10.13 (*NONE*)
10.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.15 val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
10.16 - string list -> 'a -> 'b) -> 'a Celem1.ptyp -> unit
10.17 + string list -> 'a -> 'b) -> 'a Store.ptyp -> unit
10.18 val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
10.19 - string list -> 'a -> 'b) -> 'a Celem1.ptyp list -> unit
10.20 + string list -> 'a -> 'b) -> 'a Store.ptyp list -> unit
10.21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.22 end
10.23
10.24 @@ -145,7 +145,7 @@
10.25 let
10.26 val i = indentation
10.27 val j = indentation
10.28 - fun node i p theID (Celem1.Ptyp (id, _, ns)) =
10.29 + fun node i p theID (Store.Ptyp (id, _, ns)) =
10.30 let
10.31 val p' = Pos.lev_on p
10.32 val theID' = theID @ [id]
10.33 @@ -222,7 +222,7 @@
10.34 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
10.35
10.36 (* analoguous to 'fun node' *)
10.37 -fun thenode (pa : Celem.filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) =
10.38 +fun thenode (pa : Celem.filepath) ids po wfn (Store.Ptyp (id, [n], ns)) =
10.39 let val po' = Pos.lev_on po
10.40 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
10.41 and thenodes _ _ _ _ [] = ()
11.1 --- a/src/Tools/isac/Specify/ptyps.sml Sun Apr 19 15:51:31 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/ptyps.sml Sun Apr 19 16:17:27 2020 +0200
11.3 @@ -32,7 +32,7 @@
11.4
11.5 type pblRD = string list (* for pbl-met-hierarchy.sml *)
11.6 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
11.7 - val scan : string list -> 'a Celem1.ptyp list -> string list list (* for thy-hierarchy.sml *)
11.8 + val scan : string list -> 'a Store.ptyp list -> string list list (* for thy-hierarchy.sml *)
11.9 val itm_out : theory -> Model.itm_ -> string
11.10 val dsc_unknown : term
11.11
11.12 @@ -123,10 +123,10 @@
11.13 fun get_data ptyp =
11.14 let
11.15 fun scan [] = []
11.16 - | scan ((Celem1.Ptyp ((_, data, []))) :: []) = data
11.17 - | scan ((Celem1.Ptyp ((_, data, pl))) :: []) = data @ scan pl
11.18 - | scan ((Celem1.Ptyp ((_, data, []))) :: ps) = data @ scan ps
11.19 - | scan ((Celem1.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
11.20 + | scan ((Store.Ptyp ((_, data, []))) :: []) = data
11.21 + | scan ((Store.Ptyp ((_, data, pl))) :: []) = data @ scan pl
11.22 + | scan ((Store.Ptyp ((_, data, []))) :: ps) = data @ scan ps
11.23 + | scan ((Store.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
11.24 in scan ptyp end
11.25
11.26 fun get_fun_ids thy =
11.27 @@ -300,7 +300,7 @@
11.28 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
11.29 "pbl_" =>
11.30 let
11.31 - fun node ids gu (Celem1.Ptyp (id, [{guh, ...}], ns)) =
11.32 + fun node ids gu (Store.Ptyp (id, [{guh, ...}], ns)) =
11.33 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
11.34 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
11.35 and nodes _ _ [] = NONE
11.36 @@ -313,7 +313,7 @@
11.37 end
11.38 | "met_" =>
11.39 let
11.40 - fun node ids gu (Celem1.Ptyp (id, [{guh, ...}], ns)) =
11.41 + fun node ids gu (Store.Ptyp (id, [{guh, ...}], ns)) =
11.42 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
11.43 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
11.44 and nodes _ _ [] = NONE
11.45 @@ -421,10 +421,10 @@
11.46 fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
11.47
11.48 fun scan _ [] = [] (* no base case, for empty doms only *)
11.49 - | scan id ((Celem1.Ptyp ((i, _, []))) :: []) = [id @ [i]]
11.50 - | scan id ((Celem1.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
11.51 - | scan id ((Celem1.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
11.52 - | scan id ((Celem1.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
11.53 + | scan id ((Store.Ptyp ((i, _, []))) :: []) = [id @ [i]]
11.54 + | scan id ((Store.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
11.55 + | scan id ((Store.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
11.56 + | scan id ((Store.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
11.57
11.58 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
11.59 fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
11.60 @@ -595,11 +595,11 @@
11.61 end;
11.62
11.63 (* refine a problem; construct pblRD while scanning *)
11.64 -fun refin (pblRD: pblRD) ori (Celem1.Ptyp (pI, [py], [])) =
11.65 +fun refin (pblRD: pblRD) ori (Store.Ptyp (pI, [py], [])) =
11.66 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.67 then SOME ((pblRD @ [pI]): pblRD)
11.68 else NONE
11.69 - | refin pblRD ori (Celem1.Ptyp (pI, [py], pys)) =
11.70 + | refin pblRD ori (Store.Ptyp (pI, [py], pys)) =
11.71 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
11.72 then (case refins (pblRD @ [pI]) ori pys of
11.73 SOME pblRD' => SOME pblRD'
11.74 @@ -607,13 +607,13 @@
11.75 else NONE
11.76 | refin _ _ _ = error "refin: uncovered fun def."
11.77 and refins _ _ [] = NONE
11.78 - | refins pblRD ori ((p as Celem1.Ptyp _) :: pts) =
11.79 + | refins pblRD ori ((p as Store.Ptyp _) :: pts) =
11.80 (case refin pblRD ori p of
11.81 SOME pblRD' => SOME pblRD'
11.82 | NONE => refins pblRD ori pts);
11.83
11.84 (* refine a problem; version providing output for math-experts *)
11.85 -fun refin' (pblRD: pblRD) fmz pbls (Celem1.Ptyp (pI, [py], [])) =
11.86 +fun refin' (pblRD: pblRD) fmz pbls (Store.Ptyp (pI, [py], [])) =
11.87 let
11.88 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
11.89 val {thy, ppc, where_, prls, ...} = py
11.90 @@ -625,7 +625,7 @@
11.91 then pbls @ [Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
11.92 else pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
11.93 end
11.94 - | refin' pblRD fmz pbls (Celem1.Ptyp (pI, [py], pys)) =
11.95 + | refin' pblRD fmz pbls (Store.Ptyp (pI, [py], pys)) =
11.96 let
11.97 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
11.98 val {thy, ppc, where_, prls, ...} = py
11.99 @@ -641,7 +641,7 @@
11.100 end
11.101 | refin' _ _ _ _ = error "refin': uncovered fun def."
11.102 and refins' _ _ pbls [] = pbls
11.103 - | refins' pblRD fmz pbls ((p as Celem1.Ptyp _) :: pts) =
11.104 + | refins' pblRD fmz pbls ((p as Store.Ptyp _) :: pts) =
11.105 let
11.106 val pbls' = refin' pblRD fmz pbls p
11.107 in
11.108 @@ -651,7 +651,7 @@
11.109 end;
11.110
11.111 (* refine a problem; version for tactic Refine_Problem *)
11.112 -fun refin'' _ (pblRD: pblRD) itms pbls (Celem1.Ptyp (pI, [py], [])) =
11.113 +fun refin'' _ (pblRD: pblRD) itms pbls (Store.Ptyp (pI, [py], [])) =
11.114 let
11.115 val {thy, ppc, where_, prls, ...} = py
11.116 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
11.117 @@ -660,7 +660,7 @@
11.118 then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]
11.119 else pbls @ [Stool.NoMatch_]
11.120 end
11.121 - | refin'' _ pblRD itms pbls (Celem1.Ptyp (pI, [py], pys)) =
11.122 + | refin'' _ pblRD itms pbls (Store.Ptyp (pI, [py], pys)) =
11.123 let
11.124 val {thy, ppc, where_, prls, ...} = py
11.125 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
11.126 @@ -671,7 +671,7 @@
11.127 end
11.128 | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
11.129 and refins'' _ _ _ pbls [] = pbls
11.130 - | refins'' thy pblRD itms pbls ((p as Celem1.Ptyp _) :: pts) =
11.131 + | refins'' thy pblRD itms pbls ((p as Store.Ptyp _) :: pts) =
11.132 let
11.133 val pbls' = refin'' thy pblRD itms pbls p
11.134 in case last_elem pbls' of
12.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 15:51:31 2020 +0200
12.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 16:17:27 2020 +0200
12.3 @@ -120,24 +120,24 @@
12.4 "-------- fun update_ptyps --------------------------------------------------";
12.5 "-------- fun update_ptyps --------------------------------------------------";
12.6 val pty = [
12.7 - Celem1.Ptyp ("aaa", [1], [
12.8 - Celem1.Ptyp ("aaa-1", [11], [])]),
12.9 - Celem1.Ptyp ("bbb", [2], [
12.10 - Celem1.Ptyp ("bbb-1", [21], []),
12.11 - Celem1.Ptyp ("bbb-2", [22], [
12.12 - Celem1.Ptyp ("bbb-21", [221], []),
12.13 - Celem1.Ptyp ("bbb-22", [222], [])])]),
12.14 - Celem1.Ptyp ("ccc", [3], [])] : int Celem1.ptyp list
12.15 + Store.Ptyp ("aaa", [1], [
12.16 + Store.Ptyp ("aaa-1", [11], [])]),
12.17 + Store.Ptyp ("bbb", [2], [
12.18 + Store.Ptyp ("bbb-1", [21], []),
12.19 + Store.Ptyp ("bbb-2", [22], [
12.20 + Store.Ptyp ("bbb-21", [221], []),
12.21 + Store.Ptyp ("bbb-22", [222], [])])]),
12.22 + Store.Ptyp ("ccc", [3], [])] : int Store.ptyp list
12.23
12.24 val ID = ["ddd"];
12.25 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
12.26
12.27 val ID = ["ccc"];
12.28 if update_ptyps ID ID 99999 pty =
12.29 - [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
12.30 - Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []),
12.31 - Celem1.Ptyp ("bbb-2", [22], [Celem1.Ptyp ("bbb-21", [221], []), Celem1.Ptyp ("bbb-22", [222], [])])]),
12.32 - Celem1.Ptyp ("ccc", [99999], [])]
12.33 + [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
12.34 + Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []),
12.35 + Store.Ptyp ("bbb-2", [22], [Store.Ptyp ("bbb-21", [221], []), Store.Ptyp ("bbb-22", [222], [])])]),
12.36 + Store.Ptyp ("ccc", [99999], [])]
12.37 then () else error "update_ptyps has changed 1";
12.38
12.39 val ID = ["aaa"];
12.40 @@ -145,18 +145,18 @@
12.41
12.42 val ID = ["bbb", "bbb-2", "bbb-21"];
12.43 if update_ptyps ID ID 99999 pty =
12.44 - [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
12.45 - Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []), Celem1.Ptyp ("bbb-2", [22],
12.46 - [Celem1.Ptyp ("bbb-21", [99999], []), Celem1.Ptyp ("bbb-22", [222], [])])]),
12.47 - Celem1.Ptyp ("ccc", [3], [])]
12.48 + [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
12.49 + Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []), Store.Ptyp ("bbb-2", [22],
12.50 + [Store.Ptyp ("bbb-21", [99999], []), Store.Ptyp ("bbb-22", [222], [])])]),
12.51 + Store.Ptyp ("ccc", [3], [])]
12.52 then () else error "update_ptyps has changed 2";
12.53
12.54 val ID = ["bbb", "bbb-2", "bbb-22"];
12.55 if update_ptyps ID ID 99999 pty =
12.56 - [Celem1.Ptyp ("aaa", [1], [Celem1.Ptyp ("aaa-1", [11], [])]),
12.57 - Celem1.Ptyp ("bbb", [2], [Celem1.Ptyp ("bbb-1", [21], []),
12.58 - Celem1.Ptyp ("bbb-2", [22], [Celem1.Ptyp ("bbb-21", [221], []), Celem1.Ptyp ("bbb-22", [99999], [])])]),
12.59 - Celem1.Ptyp ("ccc", [3], [])]
12.60 + [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
12.61 + Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []),
12.62 + Store.Ptyp ("bbb-2", [22], [Store.Ptyp ("bbb-21", [221], []), Store.Ptyp ("bbb-22", [99999], [])])]),
12.63 + Store.Ptyp ("ccc", [3], [])]
12.64 then () else error "update_ptyps has changed 3";
12.65
12.66 "----------- fun subst2str' --------------------------------------------------------------------";
13.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 15:51:31 2020 +0200
13.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Sun Apr 19 16:17:27 2020 +0200
13.3 @@ -124,7 +124,7 @@
13.4 get_ptyps (); (*not = []*)
13.5 "~~~~~ fun nodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
13.6 (p, []: string list, [0], pbl2file, (get_ptyps ()));
13.7 -"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Celem1.Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
13.8 +"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Store.Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
13.9 val po' = lev_on po;
13.10 wfn (*= pbl2file*)
13.11 "~~~~~ fun pbl2file, args:"; val ((path:filepath), (pos:pos), (id:metID), (pbl as {guh,...})) =
14.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 15:51:31 2020 +0200
14.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sun Apr 19 16:17:27 2020 +0200
14.3 @@ -90,14 +90,14 @@
14.4 "----------- search for data error in thes2file ------------------";
14.5 "----------- search for data error in thes2file ------------------";
14.6 val TESTdump = Unsynchronized.ref
14.7 - ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Celem1.Ptyp ("xxx", [], []): thydata Celem1.ptyp);
14.8 + ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Store.Ptyp ("xxx", [], []): thydata Store.ptyp);
14.9
14.10 -fun TESTthenode (pa:filepath) ids po wfn (Celem1.Ptyp (id, [n], ns)) TESTids =
14.11 +fun TESTthenode (pa:filepath) ids po wfn (Store.Ptyp (id, [n], ns)) TESTids =
14.12 let val po' = lev_on po
14.13 in
14.14 if (ids@[id]) = TESTids
14.15 then
14.16 - (TESTdump := (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns)));
14.17 + (TESTdump := (pa, ids, po', wfn, (Store.Ptyp (id, [n], ns)));
14.18 error "stopped before error, created TESTdump") (* this exn creates right signature*)
14.19 else
14.20 wfn pa po' (ids @ [id]) n; TESTthenodes pa (ids @ [id]) ((lev_dn po'): pos) wfn ns TESTids
14.21 @@ -120,7 +120,7 @@
14.22 handle _(* "stopped before error, created TESTdump" *) => ());
14.23 ;
14.24 (* /----- uncomment in case of "data error in thes2file" ----------------------------(*1*)-----\*)
14.25 -val (pa, ids, po', wfn, (Celem1.Ptyp (id, [n], ns))) = ! TESTdump;
14.26 +val (pa, ids, po', wfn, (Store.Ptyp (id, [n], ns))) = ! TESTdump;
14.27 ;
14.28 "~~~~~ fun thydata2file, args:"; val ((xmldata:filepath), (pos:pos), (theID:theID), thydata) =
14.29 (pa, po', (ids@[id]), n);
14.30 @@ -361,7 +361,7 @@
14.31 "~~~~~ fun MINIthes2file, args:"; val (path) = ("/tmp/");
14.32 "~~~~~ and thenodes, args:"; val (pa, ids, po, wfn, (n::ns)) =
14.33 (path, [], [0], thydata2file, MINIthehier);
14.34 -"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Celem1.Ptyp (id, [n], ns))) =
14.35 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Ptyp (id, [n], ns))) =
14.36 (pa, ids, po, wfn, n);
14.37 val po' = lev_on po;
14.38 (*wfn pa po' (ids @ [id]) n -------------> writes xml to file; we want xml before written: *)
15.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Sun Apr 19 15:51:31 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Sun Apr 19 16:17:27 2020 +0200
15.3 @@ -283,9 +283,9 @@
15.4
15.5 (*WN120313 in "solution L" above "refine fmz ["LINEAR","system"]" caused an error...*)
15.6 "~~~~~ fun refine, args:"; val ((fmz:fmz_), (pblID:pblID)) = (fmz, ["LINEAR","system"]);
15.7 -"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Celem1.Ptyp (pI, [py], [])): pbt Celem1.ptyp)) =
15.8 +"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Ptyp (pI, [py], [])): pbt Store.ptyp)) =
15.9 ((rev o tl) pblID, fmz, [(*match list*)],
15.10 - ((Celem1.Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Celem1.ptyp));
15.11 + ((Store.Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Store.ptyp));
15.12 val {thy, ppc, where_, prls, ...} = py ;
15.13 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
15.14 val ctxt = Proof_Context.init_global thy;
15.15 @@ -427,10 +427,10 @@
15.16 (*default_print_depth 11;*) matches; (*default_print_depth 3;*)
15.17 (*brought: 'False "length_ es_ = 2"'*)
15.18
15.19 -(*-----fun refin' (pblRD:pblRD) fmz pbls ((Celem1.Ptyp (pI,[py],[])):pbt Celem1.ptyp) =
15.20 -(* val ((pblRD:pblRD), fmz, pbls, ((Celem1.Ptyp (pI,[py],[])):pbt Celem1.ptyp)) =
15.21 +(*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp) =
15.22 +(* val ((pblRD:pblRD), fmz, pbls, ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp)) =
15.23 (rev ["LINEAR","system"], fmz, [(*match list*)],
15.24 - ((Celem1.Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Celem1.ptyp));
15.25 + ((Store.Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.ptyp));
15.26 *)
15.27 > show_types:=true; UnparseC.term (hd where_); show_types:=false;
15.28 val it = "length_ (es_::real list) = (2::real)" : string
16.1 --- a/test/Tools/isac/Specify/ptyps.sml Sun Apr 19 15:51:31 2020 +0200
16.2 +++ b/test/Tools/isac/Specify/ptyps.sml Sun Apr 19 16:17:27 2020 +0200
16.3 @@ -61,11 +61,11 @@
16.4 "----------- refin test-pbtyps -----------------------------------";
16.5 (* fragile test setup: expects ptyps as fixed *)
16.6 val level_1 = case nth 9 (get_ptyps ()) of
16.7 -Celem1.Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
16.8 +Store.Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
16.9 val level_2 = case nth 4 level_1 of
16.10 -Celem1.Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
16.11 +Store.Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
16.12 val pbla_branch = case level_2 of
16.13 -[Celem1.Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
16.14 +[Store.Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
16.15
16.16 (*case 1: no refinement *)
16.17 case refin [] ori1 (hd pbla_branch) of
16.18 @@ -84,7 +84,7 @@
16.19 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 4 broken";
16.20
16.21 (*case 5: start refinement somewhere in ptyps*)
16.22 -val [Celem1.Ptyp ("pbla",_,[_, ppp as Celem1.Ptyp ("pbla2",_,_), _])] = pbla_branch;
16.23 +val [Store.Ptyp ("pbla",_,[_, ppp as Store.Ptyp ("pbla2",_,_), _])] = pbla_branch;
16.24 case refin ["pbla"] ori4 ppp of
16.25 SOME ["pbla", "pbla2", "pbla2y"] => () | _ => error "refin case 5 broken";
16.26 ==================================================================*)
16.27 @@ -423,16 +423,16 @@
16.28 val n = e_pbt;
16.29 (#guh : pbt -> guh) e_pbt;
16.30
16.31 -fun XXXnode coll (Celem1.Ptyp (_,[n],ns)) =
16.32 +fun XXXnode coll (Store.Ptyp (_,[n],ns)) =
16.33 [(#guh : pbt -> guh) n]
16.34 and XXXnodes coll [] = coll
16.35 - | XXXnodes coll (n::ns : pbt Celem1.ptyp list) = (XXXnode coll n) @
16.36 + | XXXnodes coll (n::ns : pbt Store.ptyp list) = (XXXnode coll n) @
16.37 (XXXnodes coll ns);
16.38 (*^^^ this works, but not this ...
16.39 -fun node coll (Celem1.Ptyp (_,[n],ns)) =
16.40 +fun node coll (Store.Ptyp (_,[n],ns)) =
16.41 [(#guh : 'a -> guh) n]
16.42 and nodes coll [] = coll
16.43 - | nodes coll (n::ns : 'a Celem1.ptyp list) = (node coll n) @ (nodes coll ns);
16.44 + | nodes coll (n::ns : 'a Store.ptyp list) = (node coll n) @ (nodes coll ns);
16.45
16.46 Error:
16.47 Can't unify {guh: 'a, ...} with 'b (Cannot unify with explicit type variable)
16.48 @@ -450,19 +450,19 @@
16.49 "----------- fun guh2kestoreID -----------------------------------";
16.50 "----- we assumed the problem-hierarchy containing 3 elements on toplevel";
16.51 (* ERROR: Exception Bind raised *)
16.52 -val (Celem1.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
16.53 - Celem1.Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
16.54 +val (Store.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
16.55 + Store.Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
16.56
16.57 (*
16.58 nodes [] guh1 (get_ptyps ());
16.59 nodes [] guh2 (get_ptyps ());
16.60 *)
16.61 -val (Celem1.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
16.62 +val (Store.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
16.63 ::
16.64 - Celem1.Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
16.65 - (Celem1.Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
16.66 + Store.Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
16.67 + (Store.Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
16.68 ::
16.69 - Celem1.Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
16.70 + Store.Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
16.71 ::
16.72 _ ) = (get_ptyps ());
16.73 (*