(* Title:  BaseDefinitions/refernces-def.sml

    Author: Walther Neuper

    (c) due to copyright terms

 References into Know_Store.

 *)

 signature REFERENCES_DEFINITION =

 sig

   type id (* will be specialised to Problem.id, MethodC.id *)

   val id_to_string: id -> string

   val empty_probl_id: id

   val empty_meth_id: id

   val explode_id: string -> id

   val implode_id: id -> string

   type T

   val empty: T

   val to_string: string * string list * string list -> string

   val select : T -> T -> T

 end

 (**)

 structure References_Def(**): REFERENCES_DEFINITION(**) =

 struct

 (**)

 type id = string list;

 val id_to_string = strs2str;

 val empty_probl_id = ["empty_probl_id"];

 val empty_meth_id = ["empty_meth_id"];

 val explode_id = space_explode "/";

 val implode_id = space_implode "/";

 type T =    (* 3-dimensional universe of math knowledge:       *)

   ThyC.id * (* reference to a theory comprising definitions    *)

   id *      (* will become Problem.id; a reference into a tree *)

   id;       (* will become MethodC.id; a reference into a tree  *)

 fun to_string (dom, pbl, met) = 

   "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";

 val empty = (ThyC.id_empty, empty_probl_id, empty_meth_id);

 (* select a Specification; if still unspecified take it from PblObj.origin *)

 fun select (odI, opI, omI) (dI, pI, mI) =

   (if dI = ThyC.id_empty then odI else dI,

    if pI = empty_probl_id then opI else pI,

    if mI = empty_meth_id then omI else mI);

 (**)end(**)