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

  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 variables: T -> term list

  val get_field: descriptor -> T -> m_field option

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

  val adapt_term_to_type: Proof.context -> term -> term

  val adapt_to_type_real: term -> term

  val adapt_to_type_int: term -> term

\<^isac_test>\<open>

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

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

    m_field * term * Position.T

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

    m_field * term * Position.T

\<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 = (string * (string * Position.T) list) list

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

type pre_model = (m_field * (term * term) * Position.T) 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_in_ctxt 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,

    (Syntax.read_term ctxt str

      handle ERROR msg => error (msg ^ Position.here pos)),

    pos)

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

  (m_field,

    (Proof_Context.read_term_pattern ctxt str

      handle ERROR msg => error (msg ^ Position.here 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 pat2str ctxt (field, (dsc, id)) =

  pair2str (field, pair2str (UnparseC.term_in_ctxt ctxt dsc, UnparseC.term_in_ctxt 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

(* 

  adapt type of terms with most general type to a more specific one.

  TODO: clarify how to decide by use of data from the current context.

*)

fun T_a2real (Type (s, [])) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else Type (s, [])

  | T_a2real (Type (s, Ts)) = Type (s, map T_a2real Ts)

  | T_a2real (TFree (s, srt)) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TFree (s, srt)

  | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT

  | T_a2real (TVar ((s, i), srt)) = 

    if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)

(*val adapt_to_type_real: term -> term*)

fun adapt_to_type_real (Const( s, T)) = (Const( s, T_a2real T)) 

  | adapt_to_type_real (Free( s, T)) = (Free( s, T_a2real T))

  | adapt_to_type_real (Var( n, T)) = (Var( n, T_a2real T))

  | adapt_to_type_real (Bound i) = (Bound i)

  | adapt_to_type_real (Abs(s,T,t)) = Abs(s, T, adapt_to_type_real t)

  | adapt_to_type_real (t1 $ t2) = (adapt_to_type_real t1) $ (adapt_to_type_real t2);

(*val adapt_to_type_int: term -> term*)

fun adapt_to_type_int _ = raise ERROR "Model_Pattern.adapt_to_type NOT implemented for HOLogic.intT"

fun adapt_term_to_type ctxt t =

  let

    val choice = ctxt |> K HOLogic.realT (*clarify how ctxt can be used here*)

  in

    if choice = HOLogic.realT then adapt_to_type_real t

    else if choice = HOLogic.intT then adapt_to_type_int t

    else raise ERROR "TermC.adapt_to_type only implemented for HOLogic.realT"

  end

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

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

(**)end(*struct*)