(* 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

  type subs   (* substitution as seen by learner. rename stubst_user    ["(''bdv'', x)"]*)

  type sube   (* = subs. delete !                     =  stubst_user                    *)

  type subte  (* _sub_stitution as _t_erms of _e_qualities: revise !    [bdv = x]       *)

  type subst' (* substitution in isac-programs; rename subst_prog       [(bdv, x)]      *)

(*type subst     for rewriting, in Rule (+?Isabelle); rename subst_rew  [(bools, x)]    *)

  (* TODO use these types in functions below and elsewhere; rename below according to types  *)

  val subst'_to_sube : subst' -> TermC.as_string list      (* e.g. rename to subst_user_of_prog  *)

  val subst_to_subst' : UnparseC.subst -> subst'

  val subst'_to_subst : subst' -> (term * term) list

  val sube2str : TermC.as_string list -> string

  val sube2subst : theory -> TermC.as_string list -> (term * term) list

  val sube2subte : TermC.as_string list -> term list

  val subs2subst : theory -> TermC.as_string list -> (term * term) list

  val subst2sube : (term * term) list -> TermC.as_string list                 (* for datatypes.sml *)

  val subst2subs : (term * term) list -> TermC.as_string list

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

  val subte2sube : term list -> TermC.as_string list

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

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

  val e_sube : TermC.as_string list

  val e_subs : string list

  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

fun subst2str s =

    (strs2str o

      (map (

        linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;

type fmz_ = TermC.as_string list;

(* a formalization of an example contains 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.spec;

val e_fmz = ([], Spec.empty_spec);

type result = term * term list

fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)

type subs = TermC.as_string list; (* substitution as seen by learner in tactics, in programs, etc.

  questionable design. rename to stubst_user *)

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

(* argument type of tac Rewrite_Inst *)

type sube = TermC.as_string list; (* = subs. delete *)

val e_sube = []: TermC.as_string list; (* for tests only *)

fun sube2str s = strs2str s;

type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)

type subst' = term; (* substitution in isac-programs. rename to subst_prog

  is "(char list * term) list", where term is Free ("xxx", _)

  e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)

fun subst'_to_sube sub = (sub 

  |> HOLogic.dest_list 

  |> map HOLogic.dest_prod 

  |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))

  |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)

  handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])

fun subst_to_subst' subst = subst

  |> map (apfst TermC.free2str)

  |> map (apfst HOLogic.mk_string)

  |> map HOLogic.mk_prod

  |> HOLogic.mk_list (HOLogic.mk_prodT (HOLogic.stringT, HOLogic.realT (*FIXME: 'a*)))

fun subst'_to_subst t = (t 

  |> HOLogic.dest_list 

  |> map HOLogic.dest_prod 

  |> map (apfst HOLogic.dest_string))

  |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))

  handle TERM _ => raise TERM ("subst'_to_subst: wrong argument ", [t])

val subte2sube = map UnparseC.term;

fun subst2subs subst_rew = (subst_rew

  |> map (apsnd UnparseC.term)

  |> map (apfst UnparseC.term)

  |> map (apfst (enclose "''" "''")))

  |> map pair2str

  handle TERM _ => raise TERM ("subst2subs: wrong argument " ^ subst2str subst_rew, [])

fun subst2sube subst = map UnparseC.term (map HOLogic.mk_eq subst)

val subst2subs' = map ((apfst UnparseC.term) o (apsnd UnparseC.term));

fun subs2subst thy subs = (subs

  |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))

  |> map TermC.isapair2pair

  |> map (apfst HOLogic.dest_string)

  |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))

  handle TERM _ => raise TERM ("subs2subst: wrong argument " ^ strs2str' subs, [])

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

val sube2subte = map TermC.str2term;

val subte2subst = map HOLogic.dest_eq;

end