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

   val pat2str: Proof.context -> single -> string

   type model_input_pos

   type empty_input

   type pre_model

   type pre_model'

   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_empty: Proof.context -> (m_field * (string * Position.T) list) list ->

     pre_model' * (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)

   datatype pre_model_single' =

       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 typ_of_element: descriptor -> typ

   val is_list_descr: descriptor -> bool

   val empty_for: descriptor -> empty_input

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

     m_field * term * Position.T

   val parse_empty_input: Proof.context -> m_field * (string * Position.T) -> pre_model_single'

   val is_undefined: term -> bool

 \<^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

 datatype descr_type = List of typ | Single of typ

 fun descr_type (Type ("fun", [Type ("List.list", [typ]), _])) = List typ

   | descr_type (Type ("fun", [typ, _])) = Single typ

   | descr_type typ = raise TYPE ("Model_Pattern.descr_type", [typ], [])

 fun typ_of_element descr =

   case descr_type (type_of descr) of

     List typ => typ

   | Single typ => typ

 fun is_list_descr descr =

   case descr_type (type_of descr) of List _ => true | _ => false

 fun empty_for descr =

   case descr_type (type_of descr) of

     List typ => if typ = HOLogic.boolT then "[__=__, __=__]" else "[__, __]"

   | Single typ => if typ = HOLogic.boolT then "(__=__)" else "__"

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

 datatype pre_model_single' =

     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' = pre_model_single' 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

 (*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 is_undefined tm =

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

 fun parse_empty_input 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 |> 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_empty 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_empty_input 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*)