(* Title:  BaseDefinitions/celem-91.sml

    Author: Walther Neuper

    (c) due to copyright terms

           *)

 signature CALCELEMENT_91 =

 (*/------- to Celem91 -------\*)

 (*\------- to Celem91 -------/*)

 sig

 (*/------- to Celem91 -------\*)

   val check_guhs_unique: bool Unsynchronized.ref

   val check_pblguh_unique: Celem2.guh -> Celem5.pbt Celem1.ptyp list -> unit

   val check_metguh_unique: Celem2.guh -> Celem6.met Celem1.ptyp list -> unit

   val coll_pblguhs: Celem5.pbt Celem1.ptyp list -> Celem2.guh list

   val coll_metguhs: Celem6.met Celem1.ptyp list -> Celem2.guh list

 (*\------- to Celem91 -------/*)

 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

   (*NONE*)

 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

   (*NONE*)

 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

 end

 (**)

 structure Celem91(**): CALCELEMENT_91(**) =

 struct

 (**)

 (*/------- to Celem91 -------\*)

 (* switch for checking guhs unique before storing a pbl or met;

    set true at startup (done at begin of ROOT.ML)

    set false for editing IsacKnowledge (done at end of ROOT.ML) *)

 val check_guhs_unique = Unsynchronized.ref true;

 fun coll_pblguhs pbls =

   let

     fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Celem2.guh) n] @ (nodes coll ns)

       | node _ _ = raise ERROR "coll_pblguhs - node"

 	  and nodes coll [] = coll

       | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);

   in nodes [] pbls end;

 fun check_pblguh_unique guh pbls =

   if member op = (coll_pblguhs pbls) guh

   then error ("check_guh_unique failed with \""^ guh ^"\";\n"^

 	      "use \"sort_pblguhs()\" for a list of guhs;\n"^

 	      "consider setting \"check_guhs_unique := false\"")

   else ();

 fun coll_metguhs mets =

   let

     fun node coll (Celem1.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Celem2.guh) n] @ (nodes coll ns)

       | node _ _ = raise ERROR "coll_pblguhs - node"

   	and nodes coll [] = coll

   	  | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);

     in nodes [] mets end;

 fun check_metguh_unique (guh: Celem2.guh) (mets: (Celem6.met Celem1.ptyp) list) =

     if member op = (coll_metguhs mets) guh

     then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^

 		(*"use \"sort_metguhs()\" for a list of guhs;\n" ^        ...evaluates to [] ?!?*)

 		  "consider setting \"check_guhs_unique := false\"")

     else ();

 (*\------- to Celem91 -------/*)

 (**)end(**)