(* Title:  Specify/pre-conds.sml

   Author: Walther Neuper 110226

   (c) due to copyrigh,t terms

*)

signature PRE_CONDITIONS =

sig

  type T

  type unchecked

  type unchecked_pos

  type checked

  type checked_pos

  type env_subst

  type env_eval

  type input

  val to_string : Proof.context -> T -> string

  val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term

  val max_variant: Model_Def.i_model -> Model_Def.variant

  val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T

  val make_environments: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T * (env_subst * env_eval)

(*TODO: replace vvv with ^^^*)

  val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->

       (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)

  val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->

    ((term * term) * (term * term)) list

  val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos -> 

    Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos

  val check_internal: Proof.context -> Model_Def.i_model_TEST -> (Pos.pos_ * References_Def.id)

    -> checked

  val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)

    -> checked

  val check: Proof.context -> Rule_Set.T -> unchecked ->

    Model_Pattern.T * Model_Def.i_model_TEST -> checked

(*/----- from isac_test for Minisubpbl*)

  val get_equal_descr: Model_Def.i_model_TEST -> Model_Pattern.single ->

    (Model_Pattern.single * Model_Def.i_model_single_TEST) list

  val unchecked_OLD_to_TEST: term list -> (term * Position.T) list

  val all_lhs_atoms: term list -> bool

  val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;

  val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST

  val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;

  val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->

    ((term * term) * (term * term)) list

  val discern_typ: term -> Model_Pattern.descriptor * term list ->

    ((term * term) * (term * term)) list

  val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T

  val make_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> Env.T

  val get_descr: Model_Def.i_model_single_TEST -> Model_Def.descriptor option;

  val get_dscr': Model_Def.i_model_feedback_TEST -> Model_Def.descriptor option

  val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model_TEST ->

    Model_Def.i_model_single_TEST

  val get_descr_vnt': Model_Def.i_model_feedback_TEST -> Model_Def.variants -> O_Model.T ->

    O_Model.T

(*\----- from isac_test for Minisubpbl*)

\<^isac_test>\<open>

(**)

\<close>

end

(**)

structure Pre_Conds(**) : PRE_CONDITIONS(**) =

struct

(**)

open Model_Def

type T = Pre_Conds_Def.T;  (*= (bool * term) list;*)

type unchecked = term list

type unchecked_pos = (term * Position.T) list

type checked = bool * (bool * term) list

type checked_pos = bool * ((bool * (term * Position.T)) list)

(* 

  we have three kinds of Env.T in the specification-phase:

(*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from

    Model_Pattern.T.

                       Env.T                  / (Constants, fixes)  in Model_Pattern.T

                       e.g.[(fixes, [r = 7])] |

                                              > (Constants, [<r = 7>]) in O/I_Model.T       *)

(*2*) type env_subst = Env.T (*               / 0 < fixes           in Problem.{where_, ...}

                       eg. [(fixes, r)]       |

                                              > 0 < r *)

(*3*) type env_eval =  Env.T (*               |

                       eg. [(r, 7)]           |

                                              > 0 < 7 \<longrightarrow> true

  (*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.

  (*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".

  There is a typing problem, probably to be solved by a language for Specification in the future:

  term <fixes> in (*1*) has type "bool list"

  term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)

    fun switch_type is required.

  The transition requires better modelling by a novel language for Specification.

*)

type input = TermC.as_string list;

(** tools **)

fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);

fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);

fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)

  | eval ctxt where_rls (true, where_) =

    if Rewrite.eval_true ctxt [where_] where_rls

    then (true, where_)

    else (false, where_);

(** find the maximal variant within an I_Model.T **)

(* old code before I_Model.T_TEST *)

(*ATTENTION: misses variants with equal number of items, etc*)

fun cnt itms v = (v, (length o (filter (curry op = v)) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms);

fun count_variants vts itms = map (cnt itms) vts;

fun max_list [] = raise ERROR "max_list of []"

  | max_list (y :: ys) =

    let

      fun mx (a, x) [] = (a, x)             

  	    | mx (a, x) ((b, y) :: ys) = if x < y then mx (b, y) ys else mx (a, x) ys;

    in mx y ys end;

(*find most frequent variant v in itms*)

fun variants itms = ((distinct op =) o flat o (map (fn (_, vrs, _, _, _) => vrs))) itms;

(*find the variant with most items already input, without Pre_Conds (of_max_variant)*)

(*T_TESTold \<rightarrow> fun max_variants*)

fun max_variant itms = 

    let val vts = (count_variants (variants itms)) itms;

    in if vts = [] then 0 else (fst o max_list) vts end;

(* new code with I_Model.T_TEST proper handling variants *)

(*get descriptor of those items which can contribute to Subst.T and Env.T*)

(*  get_dscr': feedback_TEST -> descriptor option*)

fun get_dscr' (Cor_TEST (descr, _)) = SOME descr

  | get_dscr' (Inc_TEST (descr, _)) = SOME descr

  | get_dscr' (Sup_TEST (descr, _)) = SOME descr

  | get_dscr' _ = NONE

    (*other feedback cannot contribute to I_Model.mk_env_TEST and Pre_Conds.mk_env_TEST*)

(*  get_descr: I_Model.single_TEST -> descriptor option*)

fun get_descr (_, _, _, _, (feedb, _)) =

  case get_dscr' feedb of NONE => NONE | some_descr => some_descr

(*  get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*)

fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =

  let

    val equal_variants = 

      filter (fn i_single => case get_descr i_single of

          NONE => false (*--------vvvvv*)

        | SOME descr' => descr' = descr) (*probl_POS*) i_model

    in

      (map (pair m_patt_single) equal_variants)

    end

(*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)

fun get_descr_vnt descr vnts i_model =

  let

    val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false

      | SOME descr' => if descr = descr' then true else false) i_model 

  in

    case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of

      [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))

    | items => Library.the_single items (*only applied to model_patt, which has each descr once*)

  end

(*

  get an appropriate (description, variant) item from o_model;

  called in case of item in met_imod is_empty_single_TEST

  (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).

*)

fun get_descr_vnt' feedb vnts o_model =

  filter (fn (_, vnts', _, descr', _) =>

    case get_dscr' feedb of

      SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false

    | NONE => false) o_model

(*  all_lhs_atoms: term list -> bool*)

fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>

  if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))

  then TermC.is_atom (TermC.lhs t)

  else false) ts) true

fun handle_lists id (descr, ts) =

  if Model_Pattern.is_list_descr descr

  then if length ts > 1         (*list with more than 1 element needs to collect by [.., .., ..]*)

    then if TermC.is_list (hd ts) (*---broken elementwise input to lists---*)

      then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]

      else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)

    else if TermC.is_atom (Library.the_single ts)

      then [(id, Library.the_single ts)]                                     (* solutions L, ...*)

      else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)

  else [(id, Library.the_single ts)]                           (* solveFor x, Extremum (A = ...)*)

fun mk_env_model _ (Model_Def.Cor_TEST (_, [])) = []

  | mk_env_model id (Model_Def.Cor_TEST (descr, ts)) = 

    handle_lists id (descr, ts)

  | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)

  | mk_env_model _ (Model_Def.Inc_TEST (_, [])) = []

  | mk_env_model id (Model_Def.Inc_TEST (descr, ts)) = 

    handle_lists id (descr, ts)

  | mk_env_model _ (Model_Def.Sup_TEST _) = []

fun make_env_model equal_descr_pairs =

  map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))

        => (mk_env_model id feedb)) equal_descr_pairs

  |> flat

fun switch_type descr [] = descr

  | switch_type (Free (id_string, _)) ts =

    Free (id_string, ts |> hd |> TermC.lhs |> type_of)

  | switch_type descr _ = raise ERROR ("switch_type undefined argument " ^

      quote (UnparseC.term (ContextC.for_ERROR ()) descr))

fun discern_typ _ (_, []) = []

  | discern_typ id (descr, ts) =

(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

    let

      val ts = if Model_Pattern.is_list_descr descr

        then if TermC.is_list (hd ts)

          then ts |> map TermC.isalist2list |> flat

          else ts

        else ts

    in

(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

  if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts

  then

    if length ts > 1

    then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";

      [])

    else [((switch_type id ts, TermC.lhs (hd ts)), 

           (TermC.lhs (hd ts), TermC.rhs (hd ts)))]

  else []

(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)

    end

(*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)

(*T_TESTnew*)

fun discern_feedback id (Model_Def.Cor_TEST (descr, ts)) = discern_typ id (descr, ts)

  | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)

  | discern_feedback id (Model_Def.Inc_TEST (descr, ts)) = discern_typ id (descr, ts)

  | discern_feedback _ (Model_Def.Sup_TEST _) = []

fun make_envs_preconds equal_givens =

  map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens

  |> flat

fun make_environments model_patt i_model =

  let

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt

      |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list = make_envs_preconds equal_givens

    val (env_subst, env_eval) = split_list subst_eval_list

  in

    (env_model, (env_subst, env_eval))

  end 

fun check_internal ctxt i_model (pbl_met, id) =

  let

    val (model, where_rls, where_) = case pbl_met of

        Pos.Pbl => let val {model, where_rls, where_, ...} = Problem.from_store ctxt id

          in (model, where_rls, where_) end

      | Pos.Met => let val {model, where_rls, where_, ...} = MethodC.from_store ctxt id

          in (model, where_rls, where_) end

      | _ => raise ERROR ("Pre_Conds.check_internal calles with " ^ Pos.pos_2str pbl_met)

    val (env_model, (env_subst, env_eval)) = (*Pre_Conds.*)make_environments model

      ((*filter (fn (_, _, _, m_field ,_) => m_field = "#Given")*) i_model)

    val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

    val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

    val full_subst = if env_eval = [] then pres_subst_other

      else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

    val evals = map (eval ctxt where_rls) full_subst

  in

      (foldl and_ (true, map fst evals), pres_subst_other)

  end;

(*T_TESTold*)

fun of_max_variant _ [] = ((false, 0, []), [], ([], []))

  | of_max_variant model_patt i_model =

 let

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (cnt_corrects) variants_separated

    val sum_variant_s = arrange_args sums_corr (1, all_variants)

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

    val env_model = make_env_model equal_descr_pairs

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list = make_envs_preconds equal_givens

    val (env_subst, env_eval) = split_list subst_eval_list

  in

    ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)

        = length model_patt, max_variant, i_model_max),

      env_model, (env_subst, env_eval))

  end

(*extract the environment from an I_Model.of_max_variant*)

fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2

(** check pre-conditions **)

fun check_pos ctxt where_rls where_POS (model_patt, i_model) =

    let

      val (_, _, (_, env_eval)) = of_max_variant model_patt 

        (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)

      val full_subst = if env_eval = []

        then map (fn (t, pos) => ((true, t), pos)) where_POS

        else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;

      val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;

      val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)

    in

      (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)

    end;

(*takes the envs resulting from of_max_variant*)

fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =

  let

      val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

      val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

      val full_subst = if env_eval = [] then pres_subst_other

        else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

      val evals = map (eval ctxt where_rls) full_subst

  in

      (foldl and_ (true, map fst evals), pres_subst_other)

  end

(*expects the precondition from Problem, ie. needs substitution by env_model*)

(*TODO: check shall call check_envs*)

fun check _ _ [] _  = (true, [])

  | check ctxt where_rls where_ (model_patt, i_model) =

    let

      val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model

      val pres_subst = map (TermC.subst_atomic_all env_subst) where_;

      val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);

      val full_subst = if env_eval = [] then pres_subst_other

        else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)

      val evals = map (eval ctxt where_rls) full_subst

    in

      (foldl and_ (true, map fst evals), pres_subst_other)

    end;

fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres

(**)end(**)