(* Title:  BaseDefinitions/problem-def.sml

    Author: Walther Neuper

    (c) due to copyright terms

 Will be enhanced by Problem later.

 *)

 signature PROBLEM_DEFINITION =

 sig

 (*type pbt*)

   type T

 (*val e_Ptyp: T Store.node*)

   val empty_store: T Store.node

 (*val check_pblguh_unique: Check_Unique.guh -> T Store.T -> unit*)

   val check_unique: Check_Unique.guh -> T Store.T -> unit

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

 (*type ptyps*)

   type store

 (*val e_pbt: T*)

   val empty: T

 (*val pbts2str: T list -> string*)

   val s_to_string: T list -> string

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

   (*NONE*)

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

 end

 (**)

 structure Probl_Def(**): PROBLEM_DEFINITION(**) =

 struct

 (**)

 (*/------- to Celem5 -------\*)

 type T = 

   {guh : Check_Unique.guh,         (* unique within this isac-knowledge                               *)

   mathauthors : string list, (* copyright                                                *)

   init : Spec.pblID,       (* to start refinement with                                        *)

   thy  : theory,      (* which allows to compile that T

                         TODO: search generalized for subthy (ref.p.69*)

                         (*^^^ WN050912 NOT used during application of the problem,

                         because applied terms may be from 'subthy' as well as from super;

                         thus we take 'maxthy'; see match_ags !                           *)

   cas : term option,  (* 'CAS-command'                                                   *)

   met : Spec.metID list,   (* methods solving the T                                         *)

 (*TODO: abstract to ?pre_model?...*)

   prls : Rule_Set.T,    (* for preds in where_                                             *)

   where_ : term list, (* where - predicates                                              *)

   ppc : Celem4.pat list      (* this is the model-pattern; 

                          it contains "#Given","#Where","#Find","#Relate"-patterns

                          for constraints on identifiers see "fun cpy_nam"                *)

 }   

 val empty = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",

   cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : T

 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',

       prls = prls', thy = thy', where_ = w'} : T)

     = "{cas = " ^ (UnparseC.term_opt cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "

       ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "

       ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "

       ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "

       ^ (UnparseC.terms w') ^ "}" |> linefeed;

 fun s_to_string pbts = map pbt2str pbts |> list2str;

 (*\------- to Celem5 -------/*)

 (*/------- to Celem5 -------\*)

 val empty_store = Store.Node ("e_pblID", [empty], [])

 type store = (T Store.node) list

 (*\------- to Celem5 -------/*)

 val check_unique =

   Check_Unique.message (Check_Unique.collect (#guh : T -> Check_Unique.guh));

 (**)end(**)