1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Apr 20 16:47:01 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Apr 21 10:13:30 2020 +0200
1.3 @@ -6,6 +6,7 @@
1.4 *)
1.5 theory BaseDefinitions imports Know_Store
1.6 begin
1.7 + ML_file tracing.sml
1.8 ML_file calcelems.sml
1.9 ML_file termC.sml
1.10 ML_file contextC.sml
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Mon Apr 20 16:47:01 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:13:30 2020 +0200
2.3 @@ -38,7 +38,6 @@
2.4 ML_file "cas-def.sml"
2.5 ML_file "thy-html.sml"
2.6
2.7 -ML_file tracing.sml
2.8 ML \<open>
2.9 \<close> ML \<open>
2.10 \<close> ML \<open>
2.11 @@ -66,8 +65,8 @@
2.12 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
2.13 val get_cas: theory -> CAS_Def.cas_elem list
2.14 val add_cas: CAS_Def.cas_elem list -> theory -> theory
2.15 - val get_ptyps: theory -> Probl_Def.ptyps
2.16 - val add_pbts: (Probl_Def.pbt * Spec.pblID) list -> theory -> theory
2.17 + val get_ptyps: theory -> Probl_Def.store
2.18 + val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
2.19 val get_mets: theory -> Meth_Def.mets
2.20 val add_mets: (Meth_Def.met * Spec.metID) list -> theory -> theory
2.21 val get_thes: theory -> (Thy_Html.thydata Store.ptyp) list
2.22 @@ -109,8 +108,8 @@
2.23 fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
2.24
2.25 structure Data = Theory_Data (
2.26 - type T = Probl_Def.ptyps;
2.27 - val empty = [Probl_Def.e_Ptyp];
2.28 + type T = Probl_Def.store;
2.29 + val empty = [Probl_Def.empty_store];
2.30 val extend = I;
2.31 val merge = Store.merge_ptyps;
2.32 );
2.33 @@ -118,7 +117,7 @@
2.34 fun add_pbts pbts thy = let
2.35 fun add_pbt (pbt as {guh,...}, pblID) =
2.36 (* the pblID has the leaf-element as first; better readability achieved *)
2.37 - (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_pblguh_unique guh (Data.get thy) else ();
2.38 + (if (!Check_Unique.check_guhs_unique) then Probl_Def.check_unique guh (Data.get thy) else ();
2.39 rev pblID |> Store.insrt pblID pbt);
2.40 in Data.map (fold add_pbt pbts) thy end;
2.41
2.42 @@ -242,9 +241,9 @@
2.43 1 + count_kestore_ptyps ps + count_kestore_ptyps ps';
2.44 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
2.45 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
2.46 -val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.pbts2str;
2.47 +val check_kestore_ptyp = check_kestore_ptyp' Probl_Def.s_to_string;
2.48 fun ptyp_ord ((Store.Ptyp (s1, _, _)), (Store.Ptyp (s2, _, _))) = string_ord (s1, s2);
2.49 -fun pbt_ord ({guh = guh'1, ...} : Probl_Def.pbt, {guh = guh'2, ...} : Probl_Def.pbt) = string_ord (guh'1, guh'2);
2.50 +fun pbt_ord ({guh = guh'1, ...} : Probl_Def.T, {guh = guh'2, ...} : Probl_Def.T) = string_ord (guh'1, guh'2);
2.51 fun sort_kestore_ptyp' _ [] = []
2.52 | sort_kestore_ptyp' ordfun ((Store.Ptyp (key, pbts, ps)) :: ps') =
2.53 ((Store.Ptyp (key, sort ordfun pbts, sort_kestore_ptyp' ordfun ps |> sort ptyp_ord))
3.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Mon Apr 20 16:47:01 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:13:30 2020 +0200
3.3 @@ -16,10 +16,10 @@
3.4 (*\------- to Celem7 -------/*)
3.5
3.6 (*/------- to Celem5 -------\*)
3.7 - type pbt = Probl_Def.pbt
3.8 + type pbt = Probl_Def.T
3.9 val e_pbt: pbt;
3.10 val e_Ptyp: pbt Store.ptyp
3.11 - type ptyps = Probl_Def.ptyps
3.12 + type ptyps = Probl_Def.store
3.13 val pbts2str: pbt list -> string
3.14 (*\------- to Celem5 -------/*)
3.15
3.16 @@ -280,11 +280,11 @@
3.17 (term * (* description *)
3.18 term)); (* id | struct-var *)
3.19 (*/------- to Celem5 -------\*)
3.20 -type pbt = Probl_Def.pbt;
3.21 -val e_pbt = Probl_Def.e_pbt;
3.22 -val e_Ptyp = Probl_Def.e_Ptyp;
3.23 -val pbts2str = Probl_Def.pbts2str;
3.24 -type ptyps = Probl_Def.ptyps;
3.25 +type pbt = Probl_Def.T;
3.26 +val e_pbt = Probl_Def.empty;
3.27 +val e_Ptyp = Probl_Def.empty_store;
3.28 +val pbts2str = Probl_Def.s_to_string;
3.29 +type ptyps = Probl_Def.store;
3.30 (*\------- to Celem5 -------/*)
3.31
3.32 (*/------- to Celem6 -------\*)
3.33 @@ -296,8 +296,8 @@
3.34
3.35 (*/------- to Celem91 -------\*)
3.36 val check_guhs_unique = Check_Unique.check_guhs_unique;
3.37 -val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh);
3.38 -val check_pblguh_unique = Probl_Def.check_pblguh_unique;
3.39 +val coll_pblguhs = Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh);
3.40 +val check_pblguh_unique = Probl_Def.check_unique;
3.41 val coll_metguhs = Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh);
3.42 val check_metguh_unique = Meth_Def.check_metguh_unique;
3.43 (*\------- to Celem91 -------/*)
4.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Apr 20 16:47:01 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Tue Apr 21 10:13:30 2020 +0200
4.3 @@ -6,14 +6,20 @@
4.4 *)
4.5 signature PROBLEM_DEFINITION =
4.6 sig
4.7 - type pbt
4.8 - type ptyps
4.9 - val pbts2str: pbt list -> string
4.10 - val e_Ptyp: pbt Store.ptyp
4.11 -(*vvv check_unique*)
4.12 - val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
4.13 +(*type pbt*)
4.14 + type T
4.15 +(*val e_Ptyp: T Store.ptyp*)
4.16 + val empty_store: T Store.ptyp
4.17 +(*val check_pblguh_unique: Check_Unique.guh -> T Store.ptyp list -> unit*)
4.18 + val check_unique: Check_Unique.guh -> T Store.ptyp list -> unit
4.19 +
4.20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.21 - val e_pbt: pbt
4.22 +(*type ptyps*)
4.23 + type store
4.24 +(*val e_pbt: T*)
4.25 + val empty: T
4.26 +(*val pbts2str: T list -> string*)
4.27 + val s_to_string: T list -> string
4.28 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.29 (*NONE*)
4.30 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.31 @@ -25,17 +31,17 @@
4.32 (**)
4.33
4.34 (*/------- to Celem5 -------\*)
4.35 -type pbt =
4.36 +type T =
4.37 {guh : Check_Unique.guh, (* unique within this isac-knowledge *)
4.38 mathauthors : string list, (* copyright *)
4.39 init : Spec.pblID, (* to start refinement with *)
4.40 - thy : theory, (* which allows to compile that pbt
4.41 + thy : theory, (* which allows to compile that T
4.42 TODO: search generalized for subthy (ref.p.69*)
4.43 (*^^^ WN050912 NOT used during application of the problem,
4.44 because applied terms may be from 'subthy' as well as from super;
4.45 thus we take 'maxthy'; see match_ags ! *)
4.46 cas : term option, (* 'CAS-command' *)
4.47 - met : Spec.metID list, (* methods solving the pbt *)
4.48 + met : Spec.metID list, (* methods solving the T *)
4.49 (*TODO: abstract to ?pre_model?...*)
4.50 prls : Rule_Set.T, (* for preds in where_ *)
4.51 where_ : term list, (* where - predicates *)
4.52 @@ -43,23 +49,23 @@
4.53 it contains "#Given","#Where","#Find","#Relate"-patterns
4.54 for constraints on identifiers see "fun cpy_nam" *)
4.55 }
4.56 -val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
4.57 - cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
4.58 +val empty = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
4.59 + cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : T
4.60 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
4.61 - prls = prls', thy = thy', where_ = w'} : pbt)
4.62 + prls = prls', thy = thy', where_ = w'} : T)
4.63 = "{cas = " ^ (UnparseC.term_opt cas') ^ ", guh = \"" ^ guh' ^ "\", init = "
4.64 ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
4.65 ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "
4.66 ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
4.67 ^ (UnparseC.terms w') ^ "}" |> linefeed;
4.68 -fun pbts2str pbts = map pbt2str pbts |> list2str;
4.69 +fun s_to_string pbts = map pbt2str pbts |> list2str;
4.70 (*\------- to Celem5 -------/*)
4.71 (*/------- to Celem5 -------\*)
4.72 -val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], [])
4.73 -type ptyps = (pbt Store.ptyp) list
4.74 +val empty_store = Store.Ptyp ("e_pblID", [empty], [])
4.75 +type store = (T Store.ptyp) list
4.76 (*\------- to Celem5 -------/*)
4.77
4.78 -val check_pblguh_unique =
4.79 - Check_Unique.message (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
4.80 +val check_unique =
4.81 + Check_Unique.message (Check_Unique.collect (#guh : T -> Check_Unique.guh));
4.82
4.83 (**)end(**)
5.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Mon Apr 20 16:47:01 2020 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Tue Apr 21 10:13:30 2020 +0200
5.3 @@ -50,7 +50,7 @@
5.4 (*.create a hierarchy with references to the guh's.*)
5.5 fun hierarchy_pbl h =
5.6 let val j = indentation
5.7 - fun nd i p (Store.Ptyp (id,[n as {guh,...} : Celem.pbt],ns)) =
5.8 + fun nd i p (Store.Ptyp (id,[n as {guh,...} : Problem.T],ns)) =
5.9 let val p' = Pos.lev_on p
5.10 in (indt i) ^ "<NODE>\n" ^
5.11 (indt (i+j)) ^ "<ID> " ^ id ^ " </ID>\n" ^
5.12 @@ -116,7 +116,7 @@
5.13
5.14 (* new version with <KESTOREREF>s -- not used *)
5.15 fun pbl2xml (id:(*pblRD*)Celem.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
5.16 - thy,where_}:Celem.pbt) =
5.17 + thy,where_}:Problem.T) =
5.18 let val thy' = Context.theory_name thy
5.19 val prls' = (#id o Rule_Set.rep) prls
5.20 in "<NODECONTENT>\n" ^
5.21 @@ -150,7 +150,7 @@
5.22 end;
5.23 (* old version with 'dead' strings for rls, calc, ....* *)
5.24 fun pbl2xml (id:(*pblRD*)Celem.pblID) ({guh,mathauthors,init,cas,met,ppc,prls,
5.25 - thy,where_}:Celem.pbt) =
5.26 + thy,where_}:Problem.T) =
5.27 "<NODECONTENT>\n" ^
5.28 indt i ^ "<GUH> " ^ guh ^ " </GUH>\n" ^
5.29 (((id2xml i)(* o rev*)) id) ^
6.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Mon Apr 20 16:47:01 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Tue Apr 21 10:13:30 2020 +0200
6.3 @@ -1,14 +1,19 @@
6.4 -(* Title: collect all defitions for the Lucas-Interpreter
6.5 +(* Title: "MathEngBasic/MathEngBasic.thy"
6.6 Author: Walther Neuper 110226
6.7 (c) due to copyright terms
6.8 - *)
6.9
6.10 +Defitions required for both, for Specify and for the Lucas-Interpreter.
6.11 +*)
6.12 theory MathEngBasic
6.13 imports "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
6.14 begin
6.15 (* removed all warnings here, only "handle _" remains *)
6.16 ML_file thmC.sml
6.17 - ML_file rewrite.sml
6.18 + ML_file problem.sml
6.19 + ML_file method.sml
6.20 + ML_file "cas-command.sml"
6.21 +
6.22 +ML_file rewrite.sml
6.23 ML_file "calc-tree-elem.sml"
6.24 ML_file model.sml
6.25 ML_file mstools.sml
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Tools/isac/MathEngBasic/cas-command.sml Tue Apr 21 10:13:30 2020 +0200
7.3 @@ -0,0 +1,20 @@
7.4 +(* Title: Interpret/lucas-interpreter.sml
7.5 + Author: Walther Neuper 2019
7.6 + (c) due to copyright terms
7.7 +*)
7.8 +
7.9 +signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
7.10 +sig
7.11 +
7.12 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.13 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
7.15 +end
7.16 +
7.17 +(**)
7.18 +structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =
7.19 +struct
7.20 +(**)
7.21 +
7.22 +
7.23 +(**)end(**)
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Tue Apr 21 10:13:30 2020 +0200
8.3 @@ -0,0 +1,20 @@
8.4 +(* Title: Interpret/lucas-interpreter.sml
8.5 + Author: Walther Neuper 2019
8.6 + (c) due to copyright terms
8.7 +*)
8.8 +
8.9 +signature METHOD =
8.10 +sig
8.11 +
8.12 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.13 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.14 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.15 +end
8.16 +
8.17 +(**)
8.18 +structure Method(**): METHOD(**) =
8.19 +struct
8.20 +(**)
8.21 +
8.22 +
8.23 +(**)end(**)
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Tue Apr 21 10:13:30 2020 +0200
9.3 @@ -0,0 +1,25 @@
9.4 +(* Title: MathEngBasic/problem.sml
9.5 + Author: Walther Neuper 2019
9.6 + (c) due to copyright terms
9.7 +*)
9.8 +
9.9 +signature PROBLEM =
9.10 +sig
9.11 + type T = Probl_Def.T
9.12 +
9.13 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.14 + (*NONE*)
9.15 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9.16 + (*NONE*)
9.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
9.18 +end
9.19 +
9.20 +(**)
9.21 +structure Problem(**): PROBLEM(**) =
9.22 +struct
9.23 +(**)
9.24 +
9.25 +type T = Probl_Def.T;
9.26 +
9.27 +
9.28 +(**)end(**)
10.1 --- a/src/Tools/isac/Specify/ptyps.sml Mon Apr 20 16:47:01 2020 +0200
10.2 +++ b/src/Tools/isac/Specify/ptyps.sml Tue Apr 21 10:13:30 2020 +0200
10.3 @@ -25,7 +25,7 @@
10.4 val mappc : ('a -> 'b) -> 'a Model.ppc -> 'b Model.ppc
10.5 val itms2itemppc : theory -> Model.itm list -> (bool * term) list -> Model.item Model.ppc (* for generate.sml *)
10.6
10.7 - val get_pbt : Celem.pblID -> Celem.pbt
10.8 + val get_pbt : Celem.pblID -> Problem.T
10.9 val get_met : Celem.metID -> Celem.met (* for generate.sml *)
10.10 val get_met' : theory -> Celem.metID -> Celem.met (* for pbl-met-hierarchy.sml *)
10.11 val get_the : Celem.theID -> Celem.thydata (* for inform.sml *)
10.12 @@ -43,7 +43,7 @@
10.13 (* for Knowledge/, if below at left margin *)
10.14 val prep_pbt : theory -> Celem.guh -> string list -> Celem.pblID ->
10.15 string list * (string * string list) list * Rule_Set.T * string option * Celem.metID list ->
10.16 - Celem.pbt * Celem.pblID
10.17 + Problem.T * Celem.pblID
10.18 val prep_met : theory -> string -> string list -> Celem.pblID ->
10.19 string list * (string * string list) list *
10.20 {calc: 'a, crls: Rule_Set.T, errpats: Error_Fill_Def.errpat list, nrls: Rule_Set.T, prls: Rule_Set.T,
10.21 @@ -53,7 +53,7 @@
10.22 val show_ptyps : unit -> unit
10.23 val show_mets : unit -> unit
10.24 datatype match' = Matches' of Model.item Model.ppc | NoMatch' of Model.item Model.ppc
10.25 - val match_pbl : Selem.fmz_ -> Celem.pbt -> match'
10.26 + val match_pbl : Selem.fmz_ -> Problem.T -> match'
10.27 val refine : Selem.fmz_ -> Celem.pblID -> Stool.match list
10.28 val e_errpat : Error_Fill_Def.errpat
10.29 val show_pblguhs : unit -> unit
11.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 20 16:47:01 2020 +0200
11.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 10:13:30 2020 +0200
11.3 @@ -53,10 +53,10 @@
11.4 (message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
11.5 (message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
11.6
11.7 -(Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
11.8 +(Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
11.9 (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
11.10
11.11 -val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh));
11.12 +val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh));
11.13 check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
11.14 ;
11.15 val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
12.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Apr 20 16:47:01 2020 +0200
12.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Apr 21 10:13:30 2020 +0200
12.3 @@ -188,84 +188,6 @@
12.4 ML_file "BaseDefinitions/error-fill-def.sml"
12.5 ML_file "BaseDefinitions/rule-set.sml"
12.6 ML_file "BaseDefinitions/check-unique.sml"
12.7 -ML \<open>
12.8 -\<close> ML \<open>
12.9 -\<close> ML \<open>
12.10 -\<close> ML \<open>
12.11 -(* Title: "BaseDefinitions/check-unique.sml"
12.12 - Author: Walther Neuper
12.13 - (c) due to copyright terms
12.14 -*)
12.15 -
12.16 -"-----------------------------------------------------------------------------------------------";
12.17 -"table of contents -----------------------------------------------------------------------------";
12.18 -"-----------------------------------------------------------------------------------------------";
12.19 -"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
12.20 -"-----------------------------------------------------------------------------------------------";
12.21 -"-----------------------------------------------------------------------------------------------";
12.22 -"-----------------------------------------------------------------------------------------------";
12.23 -
12.24 -
12.25 -"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
12.26 -"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
12.27 -"----------- re-build check_pblguh_unique with high order funs ---------------------------------";
12.28 -(*------- auxiliary format for fn*)
12.29 -fun pbl_select_guh pbt =
12.30 - let
12.31 - val {guh, ...} = (**)(pbt: pbt)(** )(pbt: met)( **)
12.32 - in guh end;
12.33 -pbl_select_guh: pbt -> guh;(**)
12.34 -
12.35 -fun met_select_guh pbt =
12.36 - let
12.37 - val {guh, ...} = (pbt: met)
12.38 - in guh end;
12.39 -met_select_guh: met -> guh;(**)
12.40 -
12.41 -(*------- hint: build higher order functions be replacing the selector by a variable argument *)
12.42 -(* collect*)
12.43 -fun collect select_guh pbls =
12.44 - let
12.45 - fun node coll (Store.Ptyp (_, [n], ns)) = [select_guh n] @ (nodes coll ns)
12.46 - | node _ _ = raise ERROR "collect_guhs: too general Store.Ptyp"
12.47 - and nodes coll [] = coll
12.48 - | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
12.49 - in nodes [] pbls end;
12.50 -
12.51 -\<close> ML \<open>
12.52 -collect
12.53 -\<close> ML \<open>
12.54 -collect: ('a -> 'b) -> 'a Store.ptyp list -> 'b list;
12.55 -collect pbl_select_guh: pbt Store.ptyp list -> guh list;
12.56 -collect met_select_guh: met Store.ptyp list -> guh list;
12.57 -
12.58 -fun message select store guh =
12.59 - if member op = (select store) guh
12.60 - then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
12.61 - "use \"sort_guhs()\" for a list of guhs;\n" ^
12.62 - "consider setting \"Check_Unique.on := false\"")
12.63 - else ();
12.64 -
12.65 - message: ('a -> guh list ) -> 'a -> guh -> unit;
12.66 -(message (collect pbl_select_guh)): pbt Store.ptyp list -> guh -> unit;
12.67 -(message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
12.68 -
12.69 -(Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
12.70 -(Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
12.71 -
12.72 -val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.pbt -> Check_Unique.guh));
12.73 -check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
12.74 -;
12.75 -val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
12.76 -check_metguh_unique: met Store.ptyp list -> guh -> unit
12.77 -;\<close> ML \<open>
12.78 -\<close> ML \<open>
12.79 -\<close> ML \<open>
12.80 -\<close> ML \<open>
12.81 -\<close> ML \<open>
12.82 -\<close> ML \<open>
12.83 -\<close> ML \<open>
12.84 -\<close>
12.85 ML_file "BaseDefinitions/calcelems.sml"
12.86 ML_file "BaseDefinitions/termC.sml"
12.87 ML_file "BaseDefinitions/contextC.sml"