(* Title:  BaseDefinitions/specification.sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

signature SPECIFICATION =

sig

  type metID

  type pblID

  type spec

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

  val metID2str: string list -> string

  val e_pblID: pblID

  val e_metID: metID

  val empty: spec

(* ---- 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 Spec(**): SPECIFICATION(**) =

struct

(**)

(*the key into the hierarchy ob problems*)

type pblID = string list; (* domID :: ...*)

val e_pblID = ["e_pblID"];

(*the key into the hierarchy ob methods*)

type metID = string list;

type spec = ThyC.id * pblID * metID;

fun to_string (dom, pbl, met) = 

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

val e_metID = ["e_metID"];

val metID2str = strs2str;

val empty = (ThyC.id_empty, e_pblID, e_metID);

(**)end(**)