(* 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 = References_Def.id

  val id_empty: id

  val id_to_string: id -> string

  type T

  val empty: T

  type store

  val empty_store: T Store.node

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

  val s_to_string: T list -> string

end

(**)

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

struct

(**)

type id = References_Def.id;

val id_empty = References_Def.empty_probl_id;

val id_to_string = References_Def.id_to_string;

type T = 

  {guh : Check_Unique.id,    (* unique within Isac_Knowledge, for html-presentation      *)

  mathauthors : string list, (* copyright                                                *)

  start_refine : References_Def.id,  (* to start refinement with                         *)

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

                        (*^^^ 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_Cmd                                                  *)

  solve_mets : References_Def.id list,   (* methods solving the T                               *)

  where_rls : Rule_Set.T,         (* for evaluation of preconditions in "#Where" on "#Given"  *)

  where_ : term list,        (* ? DEL, as soon as they are input interactively ?         *)

  model : Model_Pattern.T      (* contains "#Given", "#Find", "#Relate"

                                for constraints on identifiers see "O_Model.copy_name"   *)

}   

val empty = {guh = "pbl_empty", mathauthors = [], start_refine = id_empty, thy = @{theory "Pure"},

  cas = NONE, where_rls = Rule_Set.Empty, where_ = [], model = [], solve_mets = []} : T

fun pbt2str ({cas = cas', guh = guh', start_refine = init', mathauthors = ma', solve_mets = met', model = model',

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

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

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

      ^ (strslist2strs met') ^ ", model = " ^ Model_Pattern.to_string model' ^ ", where_rls = "

      ^ (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(*struct*)