(* Title:  Specify-phase: specifying and modeling a problem or a subproblem. The

           most important types are declared in mstools.sml.

           TODO: allocate elements of Selem and of Stool appropriately

   Author: Walther Neuper 991122, Mathias Lehnfeld

   (c) due to copyright terms

*)

signature SPECIFY_ELEMENT =

sig

  type fmz

  type fmz_

  type result

  val res2str : term * term list -> string

  datatype safe = Sundef | Safe | Unsafe | Helpless;

  val safe2str : safe -> string

  type scrstate

  datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate

  val istate2str : istate -> string

  val e_istate : istate

  type subs

  type sube

  type subte

  val sube2str : cterm' list -> string

  val sube2subst : theory -> cterm' list -> (term * term) list

  val sube2subte : cterm' list -> term list

  val subs2subst : theory -> cterm' list -> (term * term) list

  val subst2sube : (term * term) list -> cterm' list                       (* for datatypes.sml *)

  val subst2subs : (term * term) list -> cterm' list

  val subst2subs' : (term * term) list -> (string * string) list

  val subte2sube : term list -> cterm' list

  val e_ctxt : Proof.context

(*----- needed for tac, tac_ immediately (probably pre-requisites missing)

  type istate

  type subte

  type subs

  type sube

*)

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

  val e_fmz : fmz_ * spec                                                  (* for datatypes.sml *)

  val e_sube : cterm' list

  val e_subs : string list

  val scrstate2str : subst * loc_ * term option * term * safe * bool -> string

  val istates2str : istate option * istate option -> string

  val subte2subst : term list -> (term * term) list

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

  (*  NONE *)

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  (* NONE *)

end

structure Selem(**): SPECIFY_ELEMENT(**) =

struct

type fmz_ = cterm' list;

(* a formalization of an example containing data 

   sufficient for mechanically finding the solution for the example

   FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)

type fmz = fmz_ * spec;

val e_fmz = ([], e_spec);

type result = term * term list

fun res2str (t, ts) = pair2str (term2str t, terms2str ts); (* for tests only *)

datatype safe = Sundef | Safe | Unsafe | Helpless;

fun safe2str Sundef   = "Sundef"

  | safe2str Safe     = "Safe"

  | safe2str Unsafe   = "Unsafe" 

  | safe2str Helpless = "Helpless";

type scrstate =  (* state for script interpreter                       *)

	 env(*stack*)  (* used to instantiate tac for checking assod

		                12.03.noticed: e_ not updated during execution ?!? *)

	 * loc_        (* location of tac in script                          *)

	 * term option (* argument of curried functions                      *)

	 * term        (* value obtained by tac executed

		                updated also after a derivation by 'new_val'       *)

	 * safe        (* estimation of how result will be obtained          *)

	 * bool;       (* true = strongly .., false = weakly associated: 

					          only used during ass_dn/up                         *)

fun topt2str NONE = "NONE"

  | topt2str (SOME t) = "SOME" ^ term2str t;

fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)

  "(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^ 

  term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";

(* for handling type istate see fun from_pblobj_or_detail', +? *)

datatype istate =              (*interpreter state*)

	  Uistate                    (*undefined in modspec, in '_deriv'ation*)

  | ScrState of scrstate       (*for script interpreter*)

  | RrlsState of rrlsstate;    (*for reverse rewriting*)

val e_istate = (ScrState ([], [], NONE, e_term, Sundef, false));

fun rta2str (r, (t, a)) = "\n(" ^ rule2str r ^ ",(" ^ term2str t ^", " ^ terms2str a ^ "))";

fun istate2str Uistate = "Uistate"

  | istate2str (ScrState (e, l, to, t, s, b)) =

    "ScrState ("^ subst2str e ^ ",\n " ^ 

    loc_2str l ^ ", " ^ termopt2str to ^ ",\n " ^

    term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"

  | istate2str (RrlsState (t, t1, rss, rtas)) = 

    "RrlsState (" ^ term2str t ^ ", " ^ term2str t1 ^ ", " ^

    (strs2str o (map (strs2str o (map rule2str)))) rss ^ ", " ^

    (strs2str o (map rta2str)) rtas ^ ")";

fun istates2str (NONE, NONE) = "(#NONE, #NONE)"  (* for tests only *)

  | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"

  | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"

  | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";

type subs = cterm' list; (*16.11.00 for FE-KE*)

val e_subs = ["(bdv, x)"]; (* for tests only *)

(* argument type of tac Rewrite_Inst *)

type sube = cterm' list;

val e_sube = []: cterm' list; (* for tests only *)

fun sube2str s = strs2str s;

(* _sub_stitution as _t_erms of _e_qualities *)

type subte = term list;

val subte2sube = map term2str;

val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));

fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)

val subst2subs' = map ((apfst term2str) o (apsnd term2str));

fun subs2subst thy s = map (isapair2pair o (parse_patt thy)) s;

fun sube2subst thy s = map (dest_equals' o (parse_patt thy)) s;

val sube2subte = map str2term;

val subte2subst = map HOLogic.dest_eq;

val e_ctxt = Proof_Context.init_global @{theory "Pure"};

end