(* Title:  BaseDefinitions/model-pattern.sml

    Author: Walther Neuper

    (c) due to copyright terms

 A \<open>Model_Pattern\<close> defines a -> \<open>Problem\<close>-type: its \<open>variables\<close> are to be instantiated

 by the values for particular \<open>Problem\<close>s in a \<open>Formalise.model\<close>.

 The \<open>variables\<close> are used twice, in a model and as formal arguments in a \<open>Program\<close>.

 The \<open>descriptor\<close>s are unique identifiers within one \<open>Model_Pattern\<close>.

 *)

 signature MODEL_PATTERN =

 sig

   type T

   type single

   val to_string: Proof.context -> single list -> string

   type model_input_pos

   type empty_input

   val empty_input: empty_input list

   type pre_model

   type pre_model_TEST

   type pre_model_single

   type m_field = string

   type descriptor = term

   val parse_pos: Proof.context -> (m_field * (string * Position.T) list) list ->

     pre_model * (term * Position.T) list

   val parse_pos_TEST: Proof.context -> (m_field * (string * Position.T) list) list ->

     pre_model_TEST * (term * Position.T) list

   val variables: T -> term list

   val get_field: descriptor -> T -> m_field option

   datatype for = Problem | Method | Undef

   val adapt_to_type: Proof.context -> single -> single

 (*from isac_test for Minisubpbl*)

   val split_descriptor: Proof.context -> m_field * term * Position.T ->

     (m_field * (descriptor * term) * Position.T)

   val split_descriptor': string -> (*TermC.as_*)string * empty_input

   datatype pre_model_single_TEST =

       Empty of (m_field * (descriptor * empty_input) * Position.T)

     | Proper of (m_field * (descriptor * term) * Position.T)

   val parse_pattern: Proof.context -> 'a * (string * Position.T) -> 'a * term * Position.T

   val empty_for: typ -> string

   val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) ->

     m_field * term * Position.T

   val parse_term_TEST: Proof.context -> m_field * (string * Position.T) -> pre_model_single_TEST

 \<^isac_test>\<open>

   (**)

 \<close>

 end

 (**)

 structure Model_Pattern(**): MODEL_PATTERN(**) =

 struct

 (**)

 (* the pattern for an item of a problems model or a methods guard *)

 type m_field = string;

 type descriptor = term;

 type single =

   (m_field *      (* field Given, Find, Relate *)

 	  (descriptor * (* for snd term              *)

 	     term))     (* id | arbitrary term       *);

 (* does NOT contain pre-conditions, because these have no \<open>descriptor\<close> *)

 type T = single list;

 type model_input_pos =                       (* for internal use                       *)

   (m_field *                                 (* "#Given", "#Find", "#Where", "#Relate" *)

     ((*TermC.as_*)string * Position.T) list) (* list of items belonging to m_field     *)

   list;                                      (* list of "#Given" .. "#Relate"          *)

 type empty_input = string

 val empty_bool_list_input = "[__=__, __=__]"

 val empty_reallist_input = "[__, __]"

 val empty_bool_input = "(__=__)"

 val empty_item_input = "__"

 val empty_input = [empty_bool_list_input, empty_reallist_input, empty_bool_input, empty_item_input]

 fun empty_for (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) = empty_bool_list_input

   | empty_for (Type ("fun", [Type ("List.list", [Type ("Real.real", [])]), _])) = empty_reallist_input

   | empty_for (Type ("HOL.bool", [])) = empty_bool_input

   | empty_for _ = empty_item_input

 type pre_model_single = (m_field * (descriptor * term) * Position.T)

 datatype pre_model_single_TEST =

     Empty of (m_field * (descriptor * empty_input) * Position.T)

   | Proper of (m_field * (descriptor * term) * Position.T)

 type pre_model = pre_model_single list

 type pre_model_TEST = pre_model_single_TEST list

 (*val split_descriptor: Proof.context -> m_field * term * Position.T ->

     m_field * (descriptor * term)(* * Position.T*)*)

 fun split_descriptor ctxt (m_field: string, dsc_tm, pos) = 

   let

     val (m_field, (hd, arg)) = case strip_comb dsc_tm of

       (hd, [arg]) => (m_field, (hd, arg))

     | _ => error ("Wrong descriptor " ^ quote (UnparseC.term ctxt dsc_tm) ^ Position.here pos)

   in (m_field, (hd, arg), pos) end

 fun is_undefined tm =

   if Term.exists_subterm (fn Const ("HOL.undefined", _) => true | _ => false) tm then true else false

 fun is_empty_input arg = member (op =) empty_input arg

 fun split_descriptor' str =

   let

     val chars = Symbol.explode str

     val end_descr = find_index (fn str => (if str = " " then true else false)) chars

       (*^^^ TODO find parser for identifier*)

   in

     (implode (take (end_descr, chars)), implode (drop (end_descr + 1, chars)))

     (* 1 blank inbetween descriptor and argument, I_Model.feedback_to_string_TEST *)

   end    

 (*val parse_term: Proof.context -> m_field * ((*TermC.as_*)string * Position.T) -> m_field * term*)

 fun parse_term ctxt (m_field, (str, pos)) =

   (m_field, ParseC.term_position ctxt (str, pos), pos)

 fun parse_term_TEST ctxt (m_field, (str, pos)) =

   let

     val (m_field, term, pos) = parse_term ctxt (m_field, (str, pos))

     val (m_field, (descr, arg), pos) = split_descriptor ctxt (m_field, term, pos)

   in

     if is_undefined arg

     then Empty (m_field, (descr, descr |> type_of |> empty_for), pos)

     else Proper (m_field, (descr, arg), pos)

   end 

 fun parse_pattern ctxt (m_field, (str, pos)) =

   (m_field, ParseC.pattern_position ctxt (str, pos), pos)

 fun parse_pos ctxt model_input =

   let

     val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;

     val model = items 

       |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where") 

       |> map (parse_term ctxt)

       |> map (split_descriptor ctxt)

     val where_ = items 

       |> filter ((fn f => (fn (f', _) => f = f')) "#Where") 

       |> map (parse_pattern ctxt)

       |> map (fn (_, a, b) => (a, b))

   in (model, where_) end

 fun parse_pos_TEST ctxt model_input =

   let

     val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;

     val model = items 

       |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")

       |> map (parse_term_TEST ctxt)

     val where_ = items 

       |> filter ((fn f => (fn (f', _) => f = f')) "#Where") 

       |> map (parse_pattern ctxt)

       |> map (fn (_, a, b) => (a, b))

   in (model, where_) end

 fun pat2str ctxt (field, (dsc, id)) =

   pair2str (field, pair2str (UnparseC.term ctxt dsc, UnparseC.term ctxt id));

 fun to_string ctxt pats = (strs2str o (map (pat2str ctxt))) pats;

 \<^isac_test>\<open>

 (**)

 \<close>

 (* get the variables out of a pbl_; FIXME.WN.0311: is_copy_named ...obscure!!! *)

 fun variables pbl_ = 

   let

     fun var_of_pbl_ (_, (_, t)) = t: term

   in ((map var_of_pbl_)(* o (filter_out is_copy_named)*)) pbl_ end

 fun get_field descriptor m_patt = 

   (filter ((curry (fn (desc, (_, (desc', _))) => desc = desc')) descriptor) m_patt

     |> the_single

     |> (fn (a, _) => SOME a))

   handle List.Empty => NONE

   datatype for = Problem | Method | Undef

 (* adapt type of terms with most general type to a more specific one *)

 fun adapt_to_type ctxt (field, (descr, term_as_string)) =

   (field, (ParseC.adapt_term_to_type ctxt descr, ParseC.adapt_term_to_type ctxt term_as_string))

 (**)end(*struct*)