(* 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 / Where in Pre_Conds *)

	  (descriptor * (* for term                                       *)

	     term))     (* internal identifier for substitution           *)

(* does NOT contain Pre_Conds, 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*)