(* Title:  "Specify/pre-conditions.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- build Pre_Conds.check_pos ---------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- build Pre_Conds.check_pos ---------------------------------------------------------";

"----------- build Pre_Conds.check_pos ---------------------------------------------------------";

"----------- build Pre_Conds.check_pos ---------------------------------------------------------";

(*see Outer_Syntax:    val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)

open Model_Def;

open Pre_Conds;

open I_Model

(*//------------------ test data setup -----------------------------------------------------\\*)

val thy = @{theory Calculation}

            val state =

              case the_data thy of

                  CTbasic_TEST.EmptyPtree => Preliminary.init_ctree thy example_id

                | _(*state (*FOR TEST*)*) => (**)the_data thy(**)

                  (*let*)

                    val {origin = (o_model, o_ref, _), spec = spec_ref, probl, meth, ctxt, ...} =

                      CTbasic_TEST.get_obj I state [(*Pos will become variable*)] |> CTbasic_TEST.rep_specify_data

;

if (probl |> I_Model.to_string_TEST @{context}) = "[\n" ^

  "(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n" ^

  "(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n" ^

  "(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n" ^

  "(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n" ^

  "(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"

then () else error "probl FROM state CHANGED";

(*  probl_POS from above, #1 and #2 replaced by complete items, in order to evaluate to true*)

val probl_POS =

  (1, [1,2,3], true, "#Given",

    (Cor_TEST ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}]),

      (@{term "fixes::real"}, [@{term "r::real"}])), Position.none )) ::

  nth 2 probl :: nth 3 probl :: nth 4 probl ::

  (5, [1,2], true, "#Relate",

    (Cor_TEST ((@{term "SideConditions"}, [@{term "[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]"}]),

      (@{term "sideconds::bool list"}, [TermC.empty])), Position.none ))

  :: [] : I_Model.T_TEST;

val probl_OLD = I_Model.TEST_to_OLD probl : I_Model.T;

val {model = model_patt, where_rls, where_ = where_OLD, ...} = (*from_store without Position.T-vv*)

  Problem.from_store ctxt (References.explode_id "univariate_calculus/Optimisation")

;

if (model_patt |> Model_Pattern.to_string ctxt) =

 "[\"(#Given, (Constants, fixes))\", " ^

  "\"(#Find, (Maximum, maxx))\", " ^

  "\"(#Find, (AdditionalValues, vals))\", " ^

  "\"(#Relate, (Extremum, extr))\", " ^

  "\"(#Relate, (SideConditions, sideconds))\"]"

then () else error "i_model FROM state CHANGED";

val "[0 < fixes]" = (where_OLD |> UnparseC.terms @{context})

(*prepare check input with Position.T----------------------------------------------------------^^-*)

val where_POS = [(@{term "0 < (r::real)"}, Position.none)];

(*\\------------------ test data setup -----------------------------------------------------//*)

(*//------------------ build new code (with Position.T) ------------------------------------\\*)

 Pre_Conds.check_pos ctxt where_rls where_POS (model_patt, probl);

"~~~~~ fun check_pos , args:"; val (ctxt, where_rls, where_POS, (model_patt, i_model)) =

  (ctxt, where_rls, where_POS, (model_patt, probl));

(*+*)val [(prec, _)] = where_POS;

(*+*)val "0 < r" = prec |> UnparseC.term @{context} (* 1st substitution already done*)

(*+*)val ((1, [1, 2, 3], false, "#Given", (Inc_TEST _, _)) :: _) = probl

(*+*)val 5 = length probl;

(*!!!*)val ((1, [1, 2, 3], true, "#Given", (Cor_TEST _, _)) :: _) = probl_POS

(*!!!*)val 5 = length probl_POS; (*thus subst_atomic_all \<longrightarrow> false, replaces for test -------vvvv*)

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

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

(*+*)val "[\"\n(fixes, [[r = 7]])\"]" = env_model |> Subst.to_string @{context}

(*+*)val "[\"\n(fixes, r)\"]" = env_subst |> Subst.to_string @{context}

(*+*)val "[\"\n(r, 7)\"]" = env_eval |> Subst.to_string @{context}

      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 [((true, precond), pos)] = full_subst;

(*+*)val "0 < 7" = precond |> UnparseC.term @{context}

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

(*+*)val (true, precond) =                    eval ctxt where_rls (true, precond)

(*+*)val "0 < 7" = precond |> UnparseC.term @{context}

(*+*)val [((true, precond), pos)] = evals

(*+*)val "0 < 7" = precond |> UnparseC.term @{context}

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

(*

  NOTE ON IMPROVEMENT: one could do all subst + eval without Position.T and by ------ ^^^

  finally pair with bool (! the sequence of list items is NOT changed)

*)

(*+*)val [(true, (precond, pos))] = display

(*+*)val "0 < r" = precond |> UnparseC.term @{context}

val return_check_pos =

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

:

checked_TEST

(* final test ... ----------------------------------------------------------------------------*)

val (true, [(true, (Const ("Orderings.ord_class.less", _) $ 

    Const ("Groups.zero_class.zero", _) $ Free ("r", _), _))]) = return_check_pos

(*\\------------------ build new code (with Position.T) ------------------------------------//*)