1 (* Title: BaseDefinitions/celem-91.sml
3 (c) due to copyright terms
6 signature CALCELEMENT_91 =
7 (*/------- to Celem91 -------\*)
8 (*\------- to Celem91 -------/*)
10 (*/------- to Celem91 -------\*)
11 val check_guhs_unique: bool Unsynchronized.ref
12 val check_pblguh_unique: Spec.guh -> Celem5.pbt Store.ptyp list -> unit
13 val check_metguh_unique: Spec.guh -> Celem6.met Store.ptyp list -> unit
14 val coll_pblguhs: Celem5.pbt Store.ptyp list -> Spec.guh list
15 val coll_metguhs: Celem6.met Store.ptyp list -> Spec.guh list
16 (*\------- to Celem91 -------/*)
17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
19 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
21 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25 structure Celem91(**): CALCELEMENT_91(**) =
29 (*/------- to Celem91 -------\*)
30 (* switch for checking guhs unique before storing a pbl or met;
31 set true at startup (done at begin of ROOT.ML)
32 set false for editing IsacKnowledge (done at end of ROOT.ML) *)
33 val check_guhs_unique = Unsynchronized.ref true;
35 fun coll_pblguhs pbls =
37 fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Spec.guh) n] @ (nodes coll ns)
38 | node _ _ = raise ERROR "coll_pblguhs - node"
39 and nodes coll [] = coll
40 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
42 fun check_pblguh_unique guh pbls =
43 if member op = (coll_pblguhs pbls) guh
44 then error ("check_guh_unique failed with \""^ guh ^"\";\n"^
45 "use \"sort_pblguhs()\" for a list of guhs;\n"^
46 "consider setting \"check_guhs_unique := false\"")
48 fun coll_metguhs mets =
50 fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Spec.guh) n] @ (nodes coll ns)
51 | node _ _ = raise ERROR "coll_pblguhs - node"
52 and nodes coll [] = coll
53 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
55 fun check_metguh_unique (guh: Spec.guh) (mets: (Celem6.met Store.ptyp) list) =
56 if member op = (coll_metguhs mets) guh
57 then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
58 (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
59 "consider setting \"check_guhs_unique := false\"")
61 (*\------- to Celem91 -------/*)