1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 11:28:20 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 12:26:08 2020 +0200
1.3 @@ -69,7 +69,7 @@
1.4 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
1.5 val get_mets: theory -> Meth_Def.store
1.6 val add_mets: (Meth_Def.T * Spec.metID) list -> theory -> theory
1.7 - val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
1.8 + val get_thes: theory -> (Thy_Html.thydata Store.node) list
1.9 val add_thes: (Thy_Html.thydata * Thy_Html.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.10 val insert_fillpats: (Thy_Html.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.11 val get_ref_thy: unit -> theory
1.12 @@ -111,34 +111,34 @@
1.13 type T = Probl_Def.store;
1.14 val empty = [Probl_Def.empty_store];
1.15 val extend = I;
1.16 - val merge = Store.merge_ptyps;
1.17 + val merge = Store.merge;
1.18 );
1.19 fun get_ptyps thy = Data.get thy;
1.20 fun add_pbts pbts thy = let
1.21 fun add_pbt (pbt as {guh,...}, pblID) =
1.22 (* the pblID has the leaf-element as first; better readability achieved *)
1.23 (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
1.24 - rev pblID |> Store.insrt pblID pbt);
1.25 + rev pblID |> Store.insert pblID pbt);
1.26 in Data.map (fold add_pbt pbts) thy end;
1.27
1.28 structure Data = Theory_Data (
1.29 type T = Meth_Def.store;
1.30 val empty = [Meth_Def.empty_store];
1.31 val extend = I;
1.32 - val merge = Store.merge_ptyps;
1.33 + val merge = Store.merge;
1.34 );
1.35 val get_mets = Data.get;
1.36 fun add_mets mets thy = let
1.37 fun add_met (met as {guh,...}, metID) =
1.38 (if (!Check_Unique.check_guhs_unique) then Meth_Def.check_unique guh (Data.get thy) else ();
1.39 - Store.insrt metID met metID);
1.40 + Store.insert metID met metID);
1.41 in Data.map (fold add_met mets) thy end;
1.42
1.43 structure Data = Theory_Data (
1.44 - type T = (Thy_Html.thydata Store.ptyp) list;
1.45 + type T = (Thy_Html.thydata Store.node) list;
1.46 val empty = [];
1.47 val extend = I;
1.48 - val merge = Store.merge_ptyps; (* relevant for store_thm, store_rls *)
1.49 + val merge = Store.merge; (* relevant for store_thm, store_rls *)
1.50 );
1.51 fun get_thes thy = Data.get thy
1.52 fun add_thes thes thy = let
1.53 @@ -148,11 +148,11 @@
1.54 let
1.55 fun update_elem (theID, fillpats) =
1.56 let
1.57 - val hthm = Store.get_py (Data.get thy) theID theID
1.58 + val hthm = Store.get (Data.get thy) theID theID
1.59 val hthm' = Thy_Html.update_hthm hthm fillpats
1.60 handle ERROR _ =>
1.61 error ("insert_fillpats: " ^ strs2str theID ^ "must address a theorem")
1.62 - in Store.update_ptyps theID theID hthm' end
1.63 + in Store.update theID theID hthm' end
1.64 in Data.map (fold update_elem fis) thy end
1.65
1.66 val cur_thy = Synchronized.var "finally_knowledge_complete" @{theory};
1.67 @@ -237,21 +237,21 @@
1.68 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.69
1.70 fun count_kestore_ptyps [] = 0
1.71 - | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
1.72 + | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
1.73 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
1.74 -fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.75 +fun check_kestore_ptyp' strfun (Store.Node (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
1.76 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
1.77 val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
1.78 -fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
1.79 +fun ptyp_ord ((Store.Node (s1, _, _)), (Store.Node (s2, _, _))) = string_ord (s1, s2);
1.80 fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
1.81 fun sort_kestore_ptyp' _ [] = []
1.82 - | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
1.83 - ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.84 + | sort_kestore_ptyp' ordfun ((Store.Node (key, pbts, ps)) :: ps') =
1.85 + ((Store.Node (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
1.86 :: sort_kestore_ptyp' ordfun ps');
1.87 val sort_kestore_ptyp = sort_kestore_ptyp' pbt_ord;
1.88
1.89 fun metguh2str ({guh,...} : Meth_Def.T) = guh : string;
1.90 -fun check_kestore_met (mp: Meth_Def.T Store.ptyp) =
1.91 +fun check_kestore_met (mp: Meth_Def.T Store.node) =
1.92 check_kestore_ptyp' (fn xs => map metguh2str xs |> strs2str) mp;
1.93 fun met_ord ({guh = guh'1, ...} : Meth_Def.T, {guh = guh'2, ...} : Meth_Def.T) = string_ord (guh'1, guh'2);
1.94 val sort_kestore_met = sort_kestore_ptyp' met_ord;
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 11:28:20 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 12:26:08 2020 +0200
2.3 @@ -18,7 +18,7 @@
2.4 (*/------- to Celem5 -------\*)
2.5 type pbt = Probl_Def.T
2.6 val e_pbt: pbt;
2.7 - val e_Ptyp: pbt Store.ptyp
2.8 + val e_Ptyp: pbt Store.node
2.9 type ptyps = Probl_Def.store
2.10 val pbts2str: pbt list -> string
2.11 (*\------- to Celem5 -------/*)
2.12 @@ -37,11 +37,11 @@
2.13
2.14 (*/------- to Store -------\*)
2.15 (*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*)
2.16 - val merge_ptyps: 'a Store.ptyp list * 'a Store.ptyp list -> 'a Store.ptyp list
2.17 - val insrt: pblID -> 'a -> string list -> 'a Store.ptyp list -> 'a Store.ptyp list
2.18 - val get_py: 'a Store.ptyp list -> pblID -> string list -> 'a
2.19 - val update_ptyps: string list -> string list -> 'a -> 'a Store.ptyp list -> 'a Store.ptyp list
2.20 - val app_py: 'a Store.ptyp list -> ('a Store.ptyp -> 'b) -> pblID -> string list -> 'b
2.21 + val merge_ptyps: 'a Store.T * 'a Store.T -> 'a Store.T
2.22 + val insrt: pblID -> 'a -> string list -> 'a Store.T -> 'a Store.T
2.23 + val get_py: 'a Store.T -> pblID -> string list -> 'a
2.24 + val update_ptyps: string list -> string list -> 'a -> 'a Store.T -> 'a Store.T
2.25 + val app_py: 'a Store.T -> ('a Store.node -> 'b) -> pblID -> string list -> 'b
2.26 (*\------- to Store -------/*)
2.27
2.28 (*/------- to Celem2 -------\*)
2.29 @@ -66,22 +66,22 @@
2.30 val ord2guh: string * ThyC.id -> string -> string
2.31 val theID2guh: theID -> guh
2.32
2.33 - val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
2.34 + val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
2.35 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
2.36 (*\------- to Celem8 -------/*)
2.37
2.38 (*/------- to Celem6 -------\*)
2.39 type met = Meth_Def.T
2.40 type mets = Meth_Def.store
2.41 - val e_Mets: met Store.ptyp
2.42 + val e_Mets: met Store.node
2.43 (*\------- to Celem6 -------/*)
2.44
2.45 (*/------- to Celem91 -------\*)
2.46 val check_guhs_unique: bool Unsynchronized.ref
2.47 - val coll_pblguhs: pbt Store.ptyp list -> guh list
2.48 - val check_pblguh_unique: guh -> pbt Store.ptyp list -> unit
2.49 - val coll_metguhs: met Store.ptyp list -> guh list
2.50 - val check_metguh_unique: guh -> met Store.ptyp list -> unit
2.51 + val coll_pblguhs: pbt Store.T -> guh list
2.52 + val check_pblguh_unique: guh -> pbt Store.T -> unit
2.53 + val coll_metguhs: met Store.T -> guh list
2.54 + val check_metguh_unique: guh -> met Store.T -> unit
2.55 (*\------- to Celem91 -------/*)
2.56
2.57 val linefeed: string -> string
2.58 @@ -111,8 +111,8 @@
2.59
2.60 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.61 val pats2str' : pat list -> string
2.62 - val insert_fillpats: thydata Store.ptyp list -> (pblID * Error_Fill_Def.fillpat list) list -> thydata Store.ptyp list ->
2.63 - thydata Store.ptyp list
2.64 + val insert_fillpats: thydata Store.T -> (pblID * Error_Fill_Def.fillpat list) list -> thydata Store.T ->
2.65 + thydata Store.T
2.66 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.67 val knowthys: unit -> theory list
2.68 (*/------- to Celem6 -------\*)
2.69 @@ -207,11 +207,11 @@
2.70 | str2ketype' str = raise ERROR ("str2ketype': WRONG arg = " ^ str)
2.71
2.72 (*/------- to Store -------\*)
2.73 -val merge_ptyps = Store.merge_ptyps;
2.74 -val insrt = Store.insrt;
2.75 -val app_py = Store.app_py;
2.76 -val get_py = Store.get_py;
2.77 -val update_ptyps = Store.update_ptyps;
2.78 +val merge_ptyps = Store.merge;
2.79 +val insrt = Store.insert;
2.80 +val app_py = Store.apply;
2.81 +val get_py = Store.get;
2.82 +val update_ptyps = Store.update;
2.83 (*\------- to Store -------/*)
2.84
2.85 (*/------- to Celem8 -------\*)
2.86 @@ -291,7 +291,7 @@
2.87 type met = Meth_Def.T;
2.88 val e_met = Meth_Def.empty;
2.89 val e_Mets = Meth_Def.empty_store;
2.90 -type mets = (met Store.ptyp) list;
2.91 +type mets = (met Store.node) list;
2.92 (*\------- to Celem6 -------/*)
2.93
2.94 (*/------- to Celem91 -------\*)
2.95 @@ -306,22 +306,22 @@
2.96 fun Html_default exist = (Html {guh = theID2guh exist,
2.97 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
2.98
2.99 -fun fill_parents (_, [i]) thydata = Store.Ptyp (i, [thydata], [])
2.100 +fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
2.101 | fill_parents (exist, i :: is) thydata =
2.102 - Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
2.103 + Store.Node (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
2.104 | fill_parents _ _ = raise ERROR "Html_default: avoid ML warning: Matches are not exhaustive"
2.105
2.106 fun add_thydata (exist, is) thydata [] = [fill_parents (exist, is) thydata]
2.107 - | add_thydata (exist, [i]) data (pys as (py as Store.Ptyp (key, _, _)) :: pyss) =
2.108 + | add_thydata (exist, [i]) data (pys as (py as Store.Node (key, _, _)) :: pyss) =
2.109 if i = key
2.110 then pys (* preserve existing thydata *)
2.111 else py :: add_thydata (exist, [i]) data pyss
2.112 - | add_thydata (exist, iss as (i :: is)) data ((py as Store.Ptyp (key, d, pys)) :: pyss) =
2.113 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
2.114 if i = key
2.115 then
2.116 if length pys = 0
2.117 - then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
2.118 - else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
2.119 + then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
2.120 + else Store.Node (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
2.121 else py :: add_thydata (exist, iss) data pyss
2.122 | add_thydata _ _ _ = raise ERROR "add_thydata: avoid ML warning: Matches are not exhaustive"
2.123
3.1 --- a/src/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 11:28:20 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 12:26:08 2020 +0200
3.3 @@ -12,7 +12,7 @@
3.4 (*val on *)
3.5 val check_guhs_unique: bool Unsynchronized.ref
3.6 (*val collect *)
3.7 - val collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
3.8 + val collect: ('a -> 'b) -> 'a Store.T -> 'b list;
3.9 val message: ('a -> guh list) -> guh -> 'a -> unit;
3.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.11 (*NONE*)
3.12 @@ -39,8 +39,8 @@
3.13
3.14 fun collect select_guh pbls =
3.15 let
3.16 - fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
3.17 - | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
3.18 + fun node coll (Store.Node (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
3.19 + | node _ _ = raise ERROR "collect_guhs: too general Store.Node"
3.20 and nodes coll [] = coll
3.21 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
3.22 in nodes [] pbls end;
4.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 11:28:20 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 21 12:26:08 2020 +0200
4.3 @@ -12,10 +12,10 @@
4.4 (*val e_met: T*)
4.5 type store
4.6 (*type mets*)
4.7 - val empty_store: T Store.ptyp
4.8 -(*val e_Mets: T Store.ptyp*)
4.9 - val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit
4.10 -(*val check_metguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*)
4.11 + val empty_store: T Store.node
4.12 +(*val e_Mets: T Store.node*)
4.13 + val check_unique: Check_Unique.guh -> T Store.T -> unit
4.14 +(*val check_metguh_unique: Check_Unique.guh -> T Store.T -> unit*)
4.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.16 (*NONE*)
4.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.18 @@ -56,9 +56,9 @@
4.19 val empty = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
4.20 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
4.21 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
4.22 -val empty_store = Store.Ptyp ("e_metID", [empty],[]);
4.23 +val empty_store = Store.Node ("e_metID", [empty],[]);
4.24
4.25 -type store = (T Store.ptyp) list;
4.26 +type store = (T Store.node) list;
4.27 (*\------- to Celem6 -------/*)
4.28
4.29 val check_unique =
5.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Tue Apr 21 11:28:20 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Tue Apr 21 12:26:08 2020 +0200
5.3 @@ -8,10 +8,10 @@
5.4 sig
5.5 (*type pbt*)
5.6 type T
5.7 -(*val e_Ptyp: T Store.ptyp*)
5.8 - val empty_store: T Store.ptyp
5.9 -(*val check_pblguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*)
5.10 - val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit
5.11 +(*val e_Ptyp: T Store.node*)
5.12 + val empty_store: T Store.node
5.13 +(*val check_pblguh_unique: Check_Unique.guh -> T Store.T -> unit*)
5.14 + val check_unique: Check_Unique.guh -> T Store.T -> unit
5.15
5.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.17 (*type ptyps*)
5.18 @@ -61,8 +61,8 @@
5.19 fun s_to_string pbts = map pbt2str pbts |> list2str;
5.20 (*\------- to Celem5 -------/*)
5.21 (*/------- to Celem5 -------\*)
5.22 -val empty_store = Store.Ptyp ("e_pblID", [empty], [])
5.23 -type store = (T Store.ptyp) list
5.24 +val empty_store = Store.Node ("e_pblID", [empty], [])
5.25 +type store = (T Store.node) list
5.26 (*\------- to Celem5 -------/*)
5.27
5.28 val check_unique =
6.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Tue Apr 21 11:28:20 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Tue Apr 21 12:26:08 2020 +0200
6.3 @@ -7,17 +7,21 @@
6.4 signature STORE_TREE =
6.5 sig
6.6 type key
6.7 - datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
6.8 -(*vvv merge *)
6.9 - val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
6.10 -(*vvv insert *)
6.11 - val insrt: key -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
6.12 -(*vvv get *)
6.13 - val get_py: 'a ptyp list -> key -> (*rev*)key -> 'a
6.14 -(*vvv update *)
6.15 - val update_ptyps: key -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
6.16 -(*vvv apply *)
6.17 - val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> key -> (*rev*)key -> 'b
6.18 +(*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list *)
6.19 + datatype 'a node = Node of string * 'a list * 'a node list
6.20 + type 'a T = 'a node list
6.21 +
6.22 +(*val merge_ptyps: 'a T * 'a T -> 'a T *)
6.23 + val merge: 'a T * 'a T -> 'a T
6.24 +(*val insrt: key -> 'a -> string list -> 'a T -> 'a T *)
6.25 + val insert: key -> 'a -> string list -> 'a T -> 'a T
6.26 +(*val get_py: 'a T -> key -> (*rev*)key -> 'a *)
6.27 + val get: 'a T -> key -> (*rev*)key -> 'a
6.28 +(*val update_ptyps: key -> string list -> 'a -> 'a T -> 'a T *)
6.29 + val update: key -> string list -> 'a -> 'a T -> 'a T
6.30 +(*val app_py: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b *)
6.31 + val apply: 'a T -> ('a node -> 'b) -> key -> (*rev*)key -> 'b
6.32 +
6.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.34 (*NONE*)
6.35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.36 @@ -36,69 +40,70 @@
6.37 for access from the Interpreter and from dialogue authoring
6.38 using a string list as key.
6.39 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
6.40 -datatype 'a ptyp =
6.41 - Ptyp of string * (* element of the key *)
6.42 +datatype 'a node =
6.43 + Node of string * (* element of the key *)
6.44 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
6.45 presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
6.46 - ('a ptyp) list; (* the children nodes *)
6.47 + ('a node) list; (* the children nodes *)
6.48 +type 'a T = ('a node) list
6.49
6.50 (* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
6.51 function for trees / ptyps *)
6.52 -fun merge_ptyps ([], pt) = pt
6.53 - | merge_ptyps (pt, []) = pt
6.54 - | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
6.55 +fun merge ([], pt) = pt
6.56 + | merge (pt, []) = pt
6.57 + | merge ((x' as Node (k, _, ps)) :: xs, (xs' as Node (k', y, ps') :: ys)) =
6.58 if k = k'
6.59 - then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
6.60 - else x' :: merge_ptyps (xs, xs');
6.61 + then Node (k, y, merge (ps, ps')) :: merge (xs, ys)
6.62 + else x' :: merge (xs, xs');
6.63
6.64 -fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
6.65 - | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
6.66 +fun insert _ pbt [k] [] = [Node (k, [pbt], [])]
6.67 + | insert d pbt [k] ((Node (k', [p], ps)) :: pys) =
6.68 ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
6.69 if k = k'
6.70 - then ((Ptyp (k', [pbt], ps)) :: pys)
6.71 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
6.72 + then ((Node (k', [pbt], ps)) :: pys)
6.73 + else ((Node (k', [p], ps)) :: (insert d pbt [k] pys))
6.74 )
6.75 - | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
6.76 + | insert d pbt (k::ks) ((Node (k', [p], ps)) :: pys) =
6.77 ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
6.78 if k = k'
6.79 - then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
6.80 + then ((Node (k', [p], insert d pbt ks ps)) :: pys)
6.81 else
6.82 if length pys = 0
6.83 then error ("insert: not found " ^ (strs2str (d(* : pblID*))))
6.84 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
6.85 + else ((Node (k', [p], ps)) :: (insert d pbt (k :: ks) pys))
6.86 )
6.87 - | insrt _ _ _ _ = raise ERROR "";
6.88 + | insert _ _ _ _ = raise ERROR "";
6.89
6.90 -fun app_py p f (d(*:pblID*)) (k(*:pblRD*)) =
6.91 +fun apply p f (d(*:pblID*)) (k(*:pblRD*)) =
6.92 let
6.93 - fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
6.94 + fun py_err _ = raise ERROR ("apply: not found: " ^ strs2str d);
6.95 fun app_py' _ [] = py_err ()
6.96 | app_py' [] _ = py_err ()
6.97 - | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
6.98 + | app_py' [k0] ((p' as Node (k', _, _ )) :: ps) =
6.99 if k0 = k' then f p' else app_py' [k0] ps
6.100 - | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
6.101 + | app_py' (k' as (k0 :: ks)) (Node (k'', _, ps) :: ps') =
6.102 if k0 = k'' then app_py' ks ps else app_py' k' ps';
6.103 in app_py' k p end;
6.104 -fun get_py p =
6.105 +fun get p =
6.106 let
6.107 - fun extract_py (Ptyp (_, [py], _)) = py
6.108 - | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
6.109 - in app_py p extract_py end;
6.110 + fun extract_py (Node (_, [py], _)) = py
6.111 + | extract_py _ = raise ERROR ("extract_py: Node has wrong format.");
6.112 + in apply p extract_py end;
6.113
6.114 -fun update_ptyps ID _ _ [] =
6.115 - error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
6.116 - | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
6.117 +fun update ID _ _ [] =
6.118 + error ("update: " ^ strs2str' ID ^ " does not exist")
6.119 + | update ID [i] data ((py as Node (key, _, pys)) :: pyss) =
6.120 if i = key
6.121 then
6.122 if length pys = 0
6.123 - then ((Ptyp (key, [data], [])) :: pyss)
6.124 - else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
6.125 - else py :: update_ptyps ID [i] data pyss
6.126 - | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
6.127 + then ((Node (key, [data], [])) :: pyss)
6.128 + else error ("update: " ^ strs2str' ID ^ " has descendants")
6.129 + else py :: update ID [i] data pyss
6.130 + | update ID (i :: is) data ((py as Node (key, d, pys)) :: pyss) =
6.131 if i = key
6.132 - then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
6.133 - else (py :: (update_ptyps ID (i :: is) data pyss))
6.134 - | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
6.135 + then ((Node (key, d, update ID is data pys)) :: pyss)
6.136 + else (py :: (update ID (i :: is) data pyss))
6.137 + | update _ _ _ _ = raise ERROR "update called with undef pattern.";
6.138 (*\------- to Store -------/*)
6.139
6.140 (**)end(**)
7.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Tue Apr 21 11:28:20 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Tue Apr 21 12:26:08 2020 +0200
7.3 @@ -28,7 +28,7 @@
7.4 val ord2guh: string * ThyC.id -> string -> Check_Unique.guh
7.5 val theID2guh: theID -> Check_Unique.guh
7.6
7.7 - val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
7.8 + val add_thydata: string list * string list -> thydata -> thydata Store.T -> thydata Store.T
7.9 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
7.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.11 (*NONE*)
7.12 @@ -80,7 +80,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 Store.ptyp) list;
7.17 +type thehier = (thydata Store.node) 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" : Check_Unique.guh
7.21 @@ -184,22 +184,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 = Store.Ptyp (i, [thydata], [])
7.26 +fun fill_parents (_, [i]) thydata = Store.Node (i, [thydata], [])
7.27 | fill_parents (exist, i :: is) thydata =
7.28 - Store.Ptyp (i, [Html_default (exist @ [i])], [fill_parents (exist @ [i], is) thydata])
7.29 + Store.Node (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 Store.Ptyp (key, _, _)) :: pyss) =
7.34 + | add_thydata (exist, [i]) data (pys as (py as Store.Node (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 Store.Ptyp (key, d, pys)) :: pyss) =
7.39 + | add_thydata (exist, iss as (i :: is)) data ((py as Store.Node (key, d, pys)) :: pyss) =
7.40 if i = key
7.41 then
7.42 if length pys = 0
7.43 - then Store.Ptyp (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
7.44 - else Store.Ptyp (key, d, add_thydata (exist @ [i], is) data pys) :: pyss
7.45 + then Store.Node (key, d, [fill_parents (exist @ [i], is) data]) :: pyss
7.46 + else Store.Node (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/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 11:28:20 2020 +0200
8.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 12:26:08 2020 +0200
8.3 @@ -33,7 +33,7 @@
8.4 (*old version with pos2filename*)
8.5 fun hierarchy pm(*"pbl" | "met"*) h =
8.6 let val j = indentation
8.7 - fun nd i p (Store.Ptyp (id,_,ns)) =
8.8 + fun nd i p (Store.Node (id,_,ns)) =
8.9 let val p' = Pos.lev_on p
8.10 in (indt i) ^ "<NODE>\n" ^
8.11 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
8.12 @@ -50,7 +50,7 @@
8.13 (*.create a hierarchy with references to the guh's.*)
8.14 fun hierarchy_pbl h =
8.15 let val j = indentation
8.16 - fun nd i p (Store.Ptyp (id,[n as {guh,...} : Problem.T],ns)) =
8.17 + fun nd i p (Store.Node (id,[n as {guh,...} : Problem.T],ns)) =
8.18 let val p' = Pos.lev_on p
8.19 in (indt i) ^ "<NODE>\n" ^
8.20 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
8.21 @@ -66,7 +66,7 @@
8.22 in nds j [0] h : Celem.xml end;
8.23 fun hierarchy_met h =
8.24 let val j = indentation
8.25 - fun nd i p (Store.Ptyp (id,[n as {guh,...} : Method.T],ns)) =
8.26 + fun nd i p (Store.Node (id,[n as {guh,...} : Method.T],ns)) =
8.27 let val p' = Pos.lev_on p
8.28 in (indt i) ^ "<NODE>\n" ^
8.29 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
8.30 @@ -264,7 +264,7 @@
8.31 ((str2file (path ^ Rtools.guh2filename guh)) o (met2xml id)) met);
8.32
8.33 (*.scan the mtree Ptyp and print the nodes using wfn.*)
8.34 -fun node (pa: Celem.filepath) ids po wfn (Store.Ptyp (id,[n],ns)) =
8.35 +fun node (pa: Celem.filepath) ids po wfn (Store.Node (id,[n],ns)) =
8.36 let val po' = Pos.lev_on po
8.37 in
8.38 wfn pa po' (ids@[id]) n;
9.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 21 11:28:20 2020 +0200
9.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 21 12:26:08 2020 +0200
9.3 @@ -14,7 +14,7 @@
9.4 (Celem.theID * Celem.thydata) list
9.5 val collect_thms: string -> theory -> (Celem.theID * Celem.thydata) list
9.6
9.7 - val hierarchy_guh: 'a Store.ptyp list -> string
9.8 + val hierarchy_guh: 'a Store.T -> string
9.9 val insert_errpatIDs: 'a -> Celem.theID -> Error_Fill_Def.errpatID list ->
9.10 Celem.thydata * Celem.theID
9.11
9.12 @@ -46,9 +46,9 @@
9.13 (*NONE*)
9.14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.15 val thenode: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
9.16 - string list -> 'a -> 'b) -> 'a Store.ptyp -> unit
9.17 + string list -> 'a -> 'b) -> 'a Store.node -> unit
9.18 val thenodes: Celem.filepath -> string list -> Pos.pos -> (Celem.filepath -> Pos.pos ->
9.19 - string list -> 'a -> 'b) -> 'a Store.ptyp list -> unit
9.20 + string list -> 'a -> 'b) -> 'a Store.T -> unit
9.21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.22 end
9.23
9.24 @@ -145,7 +145,7 @@
9.25 let
9.26 val i = indentation
9.27 val j = indentation
9.28 - fun node i p theID (Store.Ptyp (id, _, ns)) =
9.29 + fun node i p theID (Store.Node (id, _, ns)) =
9.30 let
9.31 val p' = Pos.lev_on p
9.32 val theID' = theID @ [id]
9.33 @@ -222,7 +222,7 @@
9.34 str2file (path ^ Rtools.theID2filename theID) (thydata2xml (theID, thydata)));
9.35
9.36 (* analoguous to 'fun node' *)
9.37 -fun thenode (pa : Celem.filepath) ids po wfn (Store.Ptyp (id, [n], ns)) =
9.38 +fun thenode (pa : Celem.filepath) ids po wfn (Store.Node (id, [n], ns)) =
9.39 let val po' = Pos.lev_on po
9.40 in wfn pa po' (ids @ [id]) n; thenodes pa (ids @ [id]) (Pos.lev_dn po') wfn ns end
9.41 and thenodes _ _ _ _ [] = ()
10.1 --- a/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 11:28:20 2020 +0200
10.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 12:26:08 2020 +0200
10.3 @@ -32,7 +32,7 @@
10.4
10.5 type pblRD = string list (* for pbl-met-hierarchy.sml *)
10.6 val format_pblIDl : string list list -> string (* for thy-hierarchy.sml *)
10.7 - val scan : string list -> 'a Store.ptyp list -> string list list (* for thy-hierarchy.sml *)
10.8 + val scan : string list -> 'a Store.T -> string list list (* for thy-hierarchy.sml *)
10.9 val itm_out : theory -> Model.itm_ -> string
10.10 val dsc_unknown : term
10.11
10.12 @@ -123,10 +123,10 @@
10.13 fun get_data ptyp =
10.14 let
10.15 fun scan [] = []
10.16 - | scan ((Store.Ptyp ((_, data, []))) :: []) = data
10.17 - | scan ((Store.Ptyp ((_, data, pl))) :: []) = data @ scan pl
10.18 - | scan ((Store.Ptyp ((_, data, []))) :: ps) = data @ scan ps
10.19 - | scan ((Store.Ptyp ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
10.20 + | scan ((Store.Node ((_, data, []))) :: []) = data
10.21 + | scan ((Store.Node ((_, data, pl))) :: []) = data @ scan pl
10.22 + | scan ((Store.Node ((_, data, []))) :: ps) = data @ scan ps
10.23 + | scan ((Store.Node ((_, data, pl))) :: ps) = data @ scan pl @ scan ps
10.24 in scan ptyp end
10.25
10.26 fun get_fun_ids thy =
10.27 @@ -300,7 +300,7 @@
10.28 case (implode o (take_fromto 1 4) o Symbol.explode) guh of
10.29 "pbl_" =>
10.30 let
10.31 - fun node ids gu (Store.Ptyp (id, [{guh, ...}], ns)) =
10.32 + fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =
10.33 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
10.34 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
10.35 and nodes _ _ [] = NONE
10.36 @@ -313,7 +313,7 @@
10.37 end
10.38 | "met_" =>
10.39 let
10.40 - fun node ids gu (Store.Ptyp (id, [{guh, ...}], ns)) =
10.41 + fun node ids gu (Store.Node (id, [{guh, ...}], ns)) =
10.42 if gu = guh then SOME (ids @ [id]) else nodes (ids @ [id]) gu ns
10.43 | node _ _ _ = error "guh2kestoreID node: uncovered fun def."
10.44 and nodes _ _ [] = NONE
10.45 @@ -421,10 +421,10 @@
10.46 fun format_pblIDl strll = enclose "[\n" "\n]\n" (space_implode ",\n" (map format_pblID strll));
10.47
10.48 fun scan _ [] = [] (* no base case, for empty doms only *)
10.49 - | scan id ((Store.Ptyp ((i, _, []))) :: []) = [id @ [i]]
10.50 - | scan id ((Store.Ptyp ((i, _, pl))) :: []) = scan (id @ [i]) pl
10.51 - | scan id ((Store.Ptyp ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
10.52 - | scan id ((Store.Ptyp ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
10.53 + | scan id ((Store.Node ((i, _, []))) :: []) = [id @ [i]]
10.54 + | scan id ((Store.Node ((i, _, pl))) :: []) = scan (id @ [i]) pl
10.55 + | scan id ((Store.Node ((i, _, []))) :: ps) = [id @ [i]] @ (scan id ps)
10.56 + | scan id ((Store.Node ((i, _, pl))) :: ps) = (scan (id @ [i]) pl) @ (scan id ps);
10.57
10.58 fun show_ptyps () = (writeln o format_pblIDl o (scan [])) (get_ptyps ()); (* for tests *)
10.59 fun show_mets () = (writeln o format_pblIDl o (scan [])) (get_mets ()); (* for tests *)
10.60 @@ -595,11 +595,11 @@
10.61 end;
10.62
10.63 (* refine a problem; construct pblRD while scanning *)
10.64 -fun refin (pblRD: pblRD) ori (Store.Ptyp (pI, [py], [])) =
10.65 +fun refin (pblRD: pblRD) ori (Store.Node (pI, [py], [])) =
10.66 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
10.67 then SOME ((pblRD @ [pI]): pblRD)
10.68 else NONE
10.69 - | refin pblRD ori (Store.Ptyp (pI, [py], pys)) =
10.70 + | refin pblRD ori (Store.Node (pI, [py], pys)) =
10.71 if match_oris (#thy py) (#prls py) ori (#ppc py, #where_ py)
10.72 then (case refins (pblRD @ [pI]) ori pys of
10.73 SOME pblRD' => SOME pblRD'
10.74 @@ -607,13 +607,13 @@
10.75 else NONE
10.76 | refin _ _ _ = error "refin: uncovered fun def."
10.77 and refins _ _ [] = NONE
10.78 - | refins pblRD ori ((p as Store.Ptyp _) :: pts) =
10.79 + | refins pblRD ori ((p as Store.Node _) :: pts) =
10.80 (case refin pblRD ori p of
10.81 SOME pblRD' => SOME pblRD'
10.82 | NONE => refins pblRD ori pts);
10.83
10.84 (* refine a problem; version providing output for math-experts *)
10.85 -fun refin' (pblRD: pblRD) fmz pbls (Store.Ptyp (pI, [py], [])) =
10.86 +fun refin' (pblRD: pblRD) fmz pbls (Store.Node (pI, [py], [])) =
10.87 let
10.88 val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
10.89 val {thy, ppc, where_, prls, ...} = py
10.90 @@ -625,7 +625,7 @@
10.91 then pbls @ [Stool.Matches (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
10.92 else pbls @ [Stool.NoMatch (rev (pblRD @ [pI]), itms2itemppc thy itms pre')]
10.93 end
10.94 - | refin' pblRD fmz pbls (Store.Ptyp (pI, [py], pys)) =
10.95 + | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
10.96 let
10.97 val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
10.98 val {thy, ppc, where_, prls, ...} = py
10.99 @@ -641,7 +641,7 @@
10.100 end
10.101 | refin' _ _ _ _ = error "refin': uncovered fun def."
10.102 and refins' _ _ pbls [] = pbls
10.103 - | refins' pblRD fmz pbls ((p as Store.Ptyp _) :: pts) =
10.104 + | refins' pblRD fmz pbls ((p as Store.Node _) :: pts) =
10.105 let
10.106 val pbls' = refin' pblRD fmz pbls p
10.107 in
10.108 @@ -651,7 +651,7 @@
10.109 end;
10.110
10.111 (* refine a problem; version for tactic Refine_Problem *)
10.112 -fun refin'' _ (pblRD: pblRD) itms pbls (Store.Ptyp (pI, [py], [])) =
10.113 +fun refin'' _ (pblRD: pblRD) itms pbls (Store.Node (pI, [py], [])) =
10.114 let
10.115 val {thy, ppc, where_, prls, ...} = py
10.116 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
10.117 @@ -660,7 +660,7 @@
10.118 then pbls @ [Stool.Match_ (rev (pblRD @ [pI]), (itms', pre'))]
10.119 else pbls @ [Stool.NoMatch_]
10.120 end
10.121 - | refin'' _ pblRD itms pbls (Store.Ptyp (pI, [py], pys)) =
10.122 + | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
10.123 let
10.124 val {thy, ppc, where_, prls, ...} = py
10.125 val (b, (itms', pre')) = match_itms thy itms (ppc, where_, prls);
10.126 @@ -671,7 +671,7 @@
10.127 end
10.128 | refin'' _ _ _ _ _ = error "refin': uncovered fun def."
10.129 and refins'' _ _ _ pbls [] = pbls
10.130 - | refins'' thy pblRD itms pbls ((p as Store.Ptyp _) :: pts) =
10.131 + | refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
10.132 let
10.133 val pbls' = refin'' thy pblRD itms pbls p
10.134 in case last_elem pbls' of
11.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 11:28:20 2020 +0200
11.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 12:26:08 2020 +0200
11.3 @@ -120,24 +120,24 @@
11.4 "-------- fun update_ptyps --------------------------------------------------";
11.5 "-------- fun update_ptyps --------------------------------------------------";
11.6 val pty = [
11.7 - Store.Ptyp ("aaa", [1], [
11.8 - Store.Ptyp ("aaa-1", [11], [])]),
11.9 - Store.Ptyp ("bbb", [2], [
11.10 - Store.Ptyp ("bbb-1", [21], []),
11.11 - Store.Ptyp ("bbb-2", [22], [
11.12 - Store.Ptyp ("bbb-21", [221], []),
11.13 - Store.Ptyp ("bbb-22", [222], [])])]),
11.14 - Store.Ptyp ("ccc", [3], [])] : int Store.ptyp list
11.15 + Store.Node ("aaa", [1], [
11.16 + Store.Node ("aaa-1", [11], [])]),
11.17 + Store.Node ("bbb", [2], [
11.18 + Store.Node ("bbb-1", [21], []),
11.19 + Store.Node ("bbb-2", [22], [
11.20 + Store.Node ("bbb-21", [221], []),
11.21 + Store.Node ("bbb-22", [222], [])])]),
11.22 + Store.Node ("ccc", [3], [])] : int Store.T
11.23
11.24 val ID = ["ddd"];
11.25 (*update_ptyps ID ID 99999 pty; ERROR update_ptyps: [aaa] does not exist*)
11.26
11.27 val ID = ["ccc"];
11.28 if update_ptyps ID ID 99999 pty =
11.29 - [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
11.30 - Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []),
11.31 - Store.Ptyp ("bbb-2", [22], [Store.Ptyp ("bbb-21", [221], []), Store.Ptyp ("bbb-22", [222], [])])]),
11.32 - Store.Ptyp ("ccc", [99999], [])]
11.33 + [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
11.34 + Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []),
11.35 + Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [222], [])])]),
11.36 + Store.Node ("ccc", [99999], [])]
11.37 then () else error "update_ptyps has changed 1";
11.38
11.39 val ID = ["aaa"];
11.40 @@ -145,18 +145,18 @@
11.41
11.42 val ID = ["bbb", "bbb-2", "bbb-21"];
11.43 if update_ptyps ID ID 99999 pty =
11.44 - [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
11.45 - Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []), Store.Ptyp ("bbb-2", [22],
11.46 - [Store.Ptyp ("bbb-21", [99999], []), Store.Ptyp ("bbb-22", [222], [])])]),
11.47 - Store.Ptyp ("ccc", [3], [])]
11.48 + [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
11.49 + Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []), Store.Node ("bbb-2", [22],
11.50 + [Store.Node ("bbb-21", [99999], []), Store.Node ("bbb-22", [222], [])])]),
11.51 + Store.Node ("ccc", [3], [])]
11.52 then () else error "update_ptyps has changed 2";
11.53
11.54 val ID = ["bbb", "bbb-2", "bbb-22"];
11.55 if update_ptyps ID ID 99999 pty =
11.56 - [Store.Ptyp ("aaa", [1], [Store.Ptyp ("aaa-1", [11], [])]),
11.57 - Store.Ptyp ("bbb", [2], [Store.Ptyp ("bbb-1", [21], []),
11.58 - Store.Ptyp ("bbb-2", [22], [Store.Ptyp ("bbb-21", [221], []), Store.Ptyp ("bbb-22", [99999], [])])]),
11.59 - Store.Ptyp ("ccc", [3], [])]
11.60 + [Store.Node ("aaa", [1], [Store.Node ("aaa-1", [11], [])]),
11.61 + Store.Node ("bbb", [2], [Store.Node ("bbb-1", [21], []),
11.62 + Store.Node ("bbb-2", [22], [Store.Node ("bbb-21", [221], []), Store.Node ("bbb-22", [99999], [])])]),
11.63 + Store.Node ("ccc", [3], [])]
11.64 then () else error "update_ptyps has changed 3";
11.65
11.66 "----------- fun subst2str' --------------------------------------------------------------------";
12.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 11:28:20 2020 +0200
12.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 12:26:08 2020 +0200
12.3 @@ -32,15 +32,15 @@
12.4 (* collect*)
12.5 fun collect select_guh pbls =
12.6 let
12.7 - fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
12.8 - | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
12.9 + fun node coll (Store.Node (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
12.10 + | node _ _ = raise ERROR "collect_guhs: too general Store.Node"
12.11 and nodes coll [] = coll
12.12 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
12.13 in nodes [] pbls end;
12.14
12.15 -collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
12.16 -collect pbl_select_guh: pbt Store.ptyp list -> guh list;
12.17 -collect met_select_guh: met Store.ptyp list -> guh list;
12.18 +collect: ('a -> 'b) -> 'a Store.T -> 'b list;
12.19 +collect pbl_select_guh: pbt Store.T -> guh list;
12.20 +collect met_select_guh: met Store.T -> guh list;
12.21
12.22 fun message select store guh =
12.23 if member op = (select store) guh
12.24 @@ -50,15 +50,15 @@
12.25 else ();
12.26
12.27 message: ('a -> guh list ) -> 'a -> guh -> unit;
12.28 -(message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
12.29 -(message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
12.30 +(message (collect pbl_select_guh)): pbt Store.T -> guh -> unit;
12.31 +(message (collect met_select_guh)): met Store.T -> guh -> unit;
12.32
12.33 -(Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
12.34 -(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)): met Store.ptyp list -> guh list;
12.35 +(Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)): pbt Store.T -> guh list;
12.36 +(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)): met Store.T -> guh list;
12.37
12.38 val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh));
12.39 -check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
12.40 +check_pblguh_unique: pbt Store.T -> guh -> unit
12.41 ;
12.42 val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh));
12.43 -check_metguh_unique: met Store.ptyp list -> guh -> unit
12.44 +check_metguh_unique: met Store.T -> guh -> unit
12.45 ;
12.46 \ No newline at end of file
13.1 --- a/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 11:28:20 2020 +0200
13.2 +++ b/test/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 12:26:08 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, Store.Ptyp (id,[n],ns)) = (pa, ids, po, wfn, n);
13.8 +"~~~~~ fun node, args:"; val (pa:filepath, ids, po, wfn, Store.Node (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 Tue Apr 21 11:28:20 2020 +0200
14.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 21 12:26:08 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, Store.Ptyp ("xxx", [], []): thydata Store.ptyp);
14.8 + ("path": filepath, ["ids"]: theID, []: pos, thydata2file, Store.Node ("xxx", [], []): thydata Store.node);
14.9
14.10 -fun TESTthenode (pa:filepath) ids po wfn (Store.Ptyp (id, [n], ns)) TESTids =
14.11 +fun TESTthenode (pa:filepath) ids po wfn (Store.Node (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, (Store.Ptyp (id, [n], ns)));
14.17 + (TESTdump := (pa, ids, po', wfn, (Store.Node (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, (Store.Ptyp (id, [n], ns))) = ! TESTdump;
14.26 +val (pa, ids, po', wfn, (Store.Node (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, (Store.Ptyp (id, [n], ns))) =
14.35 +"~~~~~ fun thenode, args:"; val ((pa : filepath), ids, po, wfn, (Store.Node (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 Tue Apr 21 11:28:20 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Tue Apr 21 12:26:08 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, ((Store.Ptyp (pI, [py], [])): pbt Store.ptyp)) =
15.8 +"~~~~~ fun refin', args:"; val ((pblRD: pblRD), fmz, pbls, ((Store.Node (pI, [py], [])): pbt Store.node)) =
15.9 ((rev o tl) pblID, fmz, [(*match list*)],
15.10 - ((Store.Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Store.ptyp));
15.11 + ((Store.Node ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt Store.node));
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 ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp) =
15.20 -(* val ((pblRD:pblRD), fmz, pbls, ((Store.Ptyp (pI,[py],[])):pbt Store.ptyp)) =
15.21 +(*-----fun refin' (pblRD:pblRD) fmz pbls ((Store.Node (pI,[py],[])):pbt Store.store) =
15.22 +(* val ((pblRD:pblRD), fmz, pbls, ((Store.Node (pI,[py],[])):pbt Store.store)) =
15.23 (rev ["LINEAR","system"], fmz, [(*match list*)],
15.24 - ((Store.Ptyp ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.ptyp));
15.25 + ((Store.Node ("2x2",[get_pbt ["2x2","LINEAR","system"]],[])):pbt Store.store));
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 Tue Apr 21 11:28:20 2020 +0200
16.2 +++ b/test/Tools/isac/Specify/ptyps.sml Tue Apr 21 12:26:08 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 -Store.Ptyp ("test", _, level_1) => level_1 | _ => error "refin broken: root-branch in ptyps changed?"
16.8 +Store.Node ("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 -Store.Ptyp ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
16.11 +Store.Node ("refine", _, level_2) => level_2 | _ => error "refin broken: lev1-branch in ptyps changed?"
16.12 val pbla_branch = case level_2 of
16.13 -[Store.Ptyp ("pbla", _, _)] => level_2 | _ => error "refin broken: lev2-branch in ptyps changed?";
16.14 +[Store.Node ("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 [Store.Ptyp ("pbla",_,[_, ppp as Store.Ptyp ("pbla2",_,_), _])] = pbla_branch;
16.23 +val [Store.Node ("pbla",_,[_, ppp as Store.Node ("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 (Store.Ptyp (_,[n],ns)) =
16.32 +fun XXXnode coll (Store.Node (_,[n],ns)) =
16.33 [(#guh : pbt -> guh) n]
16.34 and XXXnodes coll [] = coll
16.35 - | XXXnodes coll (n::ns : pbt Store.ptyp list) = (XXXnode coll n) @
16.36 + | XXXnodes coll (n::ns : pbt Store.T) = (XXXnode coll n) @
16.37 (XXXnodes coll ns);
16.38 (*^^^ this works, but not this ...
16.39 -fun node coll (Store.Ptyp (_,[n],ns)) =
16.40 +fun node coll (Store.Node (_,[n],ns)) =
16.41 [(#guh : 'a -> guh) n]
16.42 and nodes coll [] = coll
16.43 - | nodes coll (n::ns : 'a Store.ptyp list) = (node coll n) @ (nodes coll ns);
16.44 + | nodes coll (n::ns : 'a Store.T) = (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 (Store.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
16.53 - Store.Ptyp (id2,[n2 as {guh=guh2,...} : pbt], ns2):: _) = (get_ptyps ());
16.54 +val (Store.Node (id1,[n1 as {guh=guh1,...} : pbt], ns1)::
16.55 + Store.Node (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 (Store.Ptyp (id1,[n1 as {guh=guh1,...} : pbt], ns1)
16.62 +val (Store.Node (id1,[n1 as {guh=guh1,...} : pbt], ns1)
16.63 ::
16.64 - Store.Ptyp (id2,[n2 as {guh=guh2,...} : pbt],
16.65 - (Store.Ptyp (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
16.66 + Store.Node (id2,[n2 as {guh=guh2,...} : pbt],
16.67 + (Store.Node (id21,[n21 as {guh=guh21,...} : pbt], ns21)) :: _ )
16.68 ::
16.69 - Store.Ptyp (id3,[n3 as {guh=guh3,...} : pbt], ns3)
16.70 + Store.Node (id3,[n3 as {guh=guh3,...} : pbt], ns3)
16.71 ::
16.72 _ ) = (get_ptyps ());
16.73 (*