(* Title:  BaseDefinitions/problem-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

Here is a minimum of code required for Know_Store.thy.

For main code see structure Problem.

*)

signature PROBLEM_DEFINITION =

sig

  type id = Spec.id

  val id_empty: id

  val id_to_string: id -> string

(*type pbt*)

  type T

(*val e_Ptyp: T Store.node*)

  val empty_store: T Store.node

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

  val check_unique: Check_Unique.id -> 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

(**)

type id = Spec.id;

val id_empty = Spec.empty_probl_id;

val id_to_string = Spec.id_to_string;

type T = 

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

  mathauthors : string list, (* copyright                                                *)

  init : Spec.id,       (* 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.id 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 = id_empty, 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;

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

type store = (T Store.node) list

val check_unique =

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

(**)end(**)