1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml	Mon Apr 20 16:47:01 2020 +0200
     1.3 @@ -0,0 +1,65 @@
     1.4 +(* Title:  BaseDefinitions/problem-def.sml
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +Will be enhanced by Problem later.
     1.9 +*)
    1.10 +signature PROBLEM_DEFINITION =
    1.11 +sig
    1.12 +  type pbt
    1.13 +  type ptyps
    1.14 +  val pbts2str: pbt list -> string
    1.15 +  val e_Ptyp: pbt Store.ptyp
    1.16 +(*vvv check_unique*)
    1.17 +  val check_pblguh_unique: Check_Unique.guh -> pbt Store.ptyp list -> unit
    1.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.19 +  val e_pbt: pbt
    1.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.21 +  (*NONE*)
    1.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.23 +end
    1.24 +
    1.25 +(**)
    1.26 +structure Probl_Def(**): PROBLEM_DEFINITION(**) =
    1.27 +struct
    1.28 +(**)
    1.29 +
    1.30 +(*/------- to Celem5 -------\*)
    1.31 +type pbt = 
    1.32 +  {guh : Check_Unique.guh,         (* unique within this isac-knowledge                               *)
    1.33 +  mathauthors : string list, (* copyright                                                *)
    1.34 +  init : Spec.pblID,       (* to start refinement with                                        *)
    1.35 +  thy  : theory,      (* which allows to compile that pbt
    1.36 +                        TODO: search generalized for subthy (ref.p.69*)
    1.37 +                        (*^^^ WN050912 NOT used during application of the problem,
    1.38 +                        because applied terms may be from 'subthy' as well as from super;
    1.39 +                        thus we take 'maxthy'; see match_ags !                           *)
    1.40 +  cas : term option,  (* 'CAS-command'                                                   *)
    1.41 +  met : Spec.metID list,   (* methods solving the pbt                                         *)
    1.42 +(*TODO: abstract to ?pre_model?...*)
    1.43 +  prls : Rule_Set.T,    (* for preds in where_                                             *)
    1.44 +  where_ : term list, (* where - predicates                                              *)
    1.45 +  ppc : Celem4.pat list      (* this is the model-pattern; 
    1.46 +                         it contains "#Given","#Where","#Find","#Relate"-patterns
    1.47 +                         for constraints on identifiers see "fun cpy_nam"                *)
    1.48 +}   
    1.49 +val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
    1.50 +  cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
    1.51 +fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
    1.52 +      prls = prls', thy = thy', where_ = w'} : pbt)
    1.53 +    = "{cas = " ^ (UnparseC.term_opt cas') ^  ", guh = \"" ^ guh'  ^ "\", init = "
    1.54 +      ^ (strs2str init') ^ ", mathauthors = " ^ (strs2str ma' |> quote) ^ ", met = "
    1.55 +      ^ (strslist2strs met') ^ ", ppc = " ^ Celem4.pats2str ppc' ^ ", prls = "
    1.56 +      ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
    1.57 +      ^ (UnparseC.terms w') ^ "}" |> linefeed;
    1.58 +fun pbts2str pbts = map pbt2str pbts |> list2str;
    1.59 +(*\------- to Celem5 -------/*)
    1.60 +(*/------- to Celem5 -------\*)
    1.61 +val e_Ptyp = Store.Ptyp ("e_pblID", [e_pbt], [])
    1.62 +type ptyps = (pbt Store.ptyp) list
    1.63 +(*\------- to Celem5 -------/*)
    1.64 +
    1.65 +val check_pblguh_unique =
    1.66 +  Check_Unique.message (Check_Unique.collect (#guh : pbt -> Check_Unique.guh));
    1.67 +
    1.68 +(**)end(**)