(* 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_POS.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_POS.get_obj I state [(*Pos will become variable*)] |> CTbasic_POS.rep_specify_data

;

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

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

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

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

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

  "(5, [1, 2], false ,#Relate, (Inc_POS 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_POS ((@{term "Constants"}, [@{term "[r = (7::real)]"(*should be "r = (7::real)"*)}])), Position.none )) ::

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

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

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

  :: [] : I_Model.T_POS;

val probl_OLD = probl

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_POS));

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

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

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

(*+*)val 5 = length probl;

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

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

      val (env_model, (env_subst, env_eval)) = make_environments model_patt 

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

;

(*+*)(probl_POS |> I_Model.to_string_POS @{context}) = "[\n" ^

  "(1, [1, 2, 3], true ,#Given, (Cor_POS Constants [r = 7] , pen2str, Position.T)), \n" ^

(*--------------------------------------------------^^^^^^^--- FROM test data setup -----------*)

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

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

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

(*------------------------------------------------------vvvvvvv--- FROM test data setup -------*)

  "(5, [1, 2], true ,#Relate, (Cor_POS SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"

;

(*+*)val "[\"\n(fixes, [r = 7])\", \"\n(sideconds, [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2])\"]"

 = env_model |> Subst.to_string ctxt

(*+*)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_pos

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