(* Title:  "Specify/o-model.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

"----------- initialise O_Model.T --------------------------------------------------------------";

"----------- fun partition_variants ------------------------------------------------------------";

"----------- fun O_Model.collect_variants ------------------------------------------------------";

"----------- fun partition_variants ------------------------------------------------------------";

"----------- fun add_enumerate -----------------------------------------------------------------";

"----------- fun filter_vat --------------------------------------------------------------------";

"----------- regression test fun O_Model.is_copy_named -----------------------------------------";

"----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";

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

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

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

"----------- fun init for O_Model.T ------------------------------------------------------------";

"----------- fun init for O_Model.T ------------------------------------------------------------";

"----------- fun init for O_Model.T ------------------------------------------------------------";

open O_Model;

val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  "AbleitungBiegelinie dy"];

val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)

"~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp)] = [(f_model, f_spec)];

(*  val ((pt, p), tacis) =*)

Step_Specify.nxt_specify_init_calc ctxt (fmz, sp);

"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);

	    (*val (_, hdl, (dI, pI, mI), pors, pctxt) = *)

           Step_Specify.initialise (fmz, (dI, pI, mI));

"~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);

	    val thy = ThyC.get_theory dI

	    val ctxt = Proof_Context.init_global thy;

	      (*if*) mI = ["no_met"] (*else*);

	          val pors = Problem.from_store ctxt pI |> #ppc |> O_Model.init thy fmz; (*..TermC.parseNEW'*)

(*+*)Problem.from_store ctxt pI: Problem.T;

(*+*)(Problem.from_store ctxt pI |> #ppc): Model_Pattern.T;

(*+*)val o_model = (Problem.from_store ctxt pI |> #ppc |>

   O_Model.init thy fmz);

"~~~~~ fun init , args:"; val (fmz, thy, pbt) = (fmz, thy, Problem.from_store ctxt pI |> #ppc);

      val ori = (map (fn str => str

                     |> TermC.parseNEW'' thy

                     |> Input_Descript.split

                     |> add_field thy pbt) fmz)

                 |> add_variants;

(*+  decompose..*)

(*+*)val aaa as Const (\<^const_name>\<open>Traegerlaenge\<close>, _) $ Free ("L", _) = (nth 1 fmz) |> TermC.parseNEW'' thy;

(*+*)val bbb as (Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) = aaa |> Input_Descript.split;

(*+*)val ccc as ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]) =  bbb |> add_field thy pbt;

(*+  WHY IS THE LIST IN "#Relate" NOT DECOMPOSED?...*)

(*+*)val ddd as [("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)]),

                 ("#Given", Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),

                 ("#Find", Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]),

                 ("#Relate", Const (\<^const_name>\<open>Randbedingungen\<close>, _),

                   [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(*"0"*)) $ _(*"0"*)) $

                      Const (\<^const_name>\<open>Nil\<close>, _),

                    Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Free ("y", _) $ _(**)) $ _(*"0"*)) $

                      Const (\<^const_name>\<open>Nil\<close>, _),

                    Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ _(*"0"*)) $ _(*"0"*)) $

                      Const (\<^const_name>\<open>Nil\<close>, _),

                    Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>Biegelinie.M_b\<close>, _) $ Free ("L", _)) $ _(*"0"*)) $

                      Const (\<^const_name>\<open>Nil\<close>, _)]),

                 ("#undef", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]),

                  _, _] =

               (map (fn str => str

                     |> TermC.parseNEW'' thy

                     |> Input_Descript.split

                     |> add_field thy pbt) fmz);

(*+*)val eee as [(0, ("#Given", Const (\<^const_name>\<open>Traegerlaenge\<close>, _), [Free ("L", _)])),

                 _, _, _, _, _, _] = add_variants ddd;

      val maxv = map fst ori |> max_variant;

      val maxv = if maxv = 0 then 1 else maxv;

      val oris = ori

        |> O_Model.collect_variants

        |> map (replace_0 maxv |> apfst)

        |> add_enumerate

        |> map flattup;

(*+  decompose..*)

(*+*)val fff as [([0], ("#Given", _, _)), _, _, _, _, _, _]  = ori |> O_Model.collect_variants;

(*+*)val ggg as [([1], ("#Given", _, _)), _, _, _, _, _, _] = fff |> map (replace_0 maxv |> apfst);

(*+*)val hhh as [(1, ([1], ("#Given", _, _))), (2, ([1], ("#Given", _, _))), _, _, _, _, _] = ggg |> add_enumerate;

(*+*)val iii = hhh |> map flattup;

(*+*)val iii as [(1, [1], "#Given", _, _), (2, [1], "#Given", _, _), _, _, _, _, _] = hhh |> map flattup;

      (oris, ctxt)  (*return from O_Model.init*);

"~~~~~ from fun O_Model.init \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);

(* final test ...*)

(*+*)if O_Model.to_string pors = "[\n" ^ 

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^ 

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^ 

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^ 

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^ 

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^ 

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^ 

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

then () else error "O_Model.init CHANGED";

"----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";

"----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";

"----------- ..CONTIUNED: initialise ctxt ------------------------------------------------------";

    val ctxt = ContextC.initialise' thy f_model;

case parseNEW ctxt "L" of

  SOME (Free ("L", Type (\<^type_name>\<open>real\<close>, []))) => ()

| _ => error "ContextC.initialise' CHANGED";

"----------- fun partition_variants ------------------------------------------------------------";

"----------- fun partition_variants ------------------------------------------------------------";

"----------- fun partition_variants ------------------------------------------------------------";

val xs = [1,1,1,2,4,4,5];

val xxx = partition_variants (op=) xs;

if xxx = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)]

then () else error "fun partition_variants CHANGED";

"----------- fun O_Model.collect_variants -----------------------------------------------------------------";

"----------- fun O_Model.collect_variants -----------------------------------------------------------------";

"----------- fun O_Model.collect_variants -----------------------------------------------------------------";

val xs = [(1,1),(2,1),(3,1),(0,2),(1,4),(2,4),(0,5)];

if O_Model.collect_variants xs = [([1, 2, 3], 1), ([0], 2), ([1, 2], 4), ([0], 5)]

then () else error "fun O_Model.collect_variants CHANGED";

(**** fun O_Model.partition_variants  #################################################### ****)

"----------- fun partition_variants ------------------------------------------------------------";

"----------- fun partition_variants ------------------------------------------------------------";

if partition_variants op= ["a", "b", "c"] = [(0, "a"), (0, "b"), (0, "c")]

then () else error "O_Model.partition_variants CHANGED 1";

if partition_variants op= ["a", "b", "b", "b", "c"] = [

  (0, "a"), 

  (1, "b"), (2, "b"), (3, "b"), 

  (0, "c")] then () else error "O_Model.partition_variants CHANGED 2";

if partition_variants op= ["a", "b", "b", "b", "c", "c"] = [

  (0, "a"), 

  (1, "b"), (2, "b"), (3, "b"), 

  (1, "c"), (2, "c")] then () else error "O_Model.partition_variants CHANGED 3";

"----------- fun add_enumerate -----------------------------------------------------------------";

"----------- fun add_enumerate -----------------------------------------------------------------";

"----------- fun add_enumerate -----------------------------------------------------------------";

val xs = [([1,2,3],1),([0],2),([1,2],4),([0],5)];

val xxx = add_enumerate xs;

if add_enumerate xs = [(1, ([1, 2, 3], 1)), (2, ([0], 2)), (3, ([1, 2], 4)), (4, ([0], 5))]

then () else error "fun add_enumerate CHANGED";

"----------- fun filter_vat --------------------------------------------------------------------";

"----------- fun filter_vat --------------------------------------------------------------------";

"----------- fun filter_vat --------------------------------------------------------------------";

val formalise = [

  "fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",

	"relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

	"relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",

  "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",

	(* \<up>  these are the elements for the root-problem (in variants)*)

        (*vvv these are elements required for subproblems*)

	"boundVariable a", "boundVariable b", "boundVariable alpha",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= 2*r}",

	"interval {x::real. 0 <= x & x <= pi}",

	"errorBound (eps=(0::real))"]

val pbt as {ppc = ppc,...} =

    Problem.from_store @{context} ["maximum_of", "function"];

val o_model = O_Model.init @{theory} formalise ppc;

case o_model of

[

  (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),

  (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), 

  (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),

  (4, [1, 2], "#Relate",  Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),

  (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),

  (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),

  (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),

  (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),

  (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),

  (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),

  (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])

] => ()

| _ =>  error "fun O_Model.init CHANGED";

(*/------- unused code -----------------------------------------------------------------------\*)

fun filter_vat oris i = filter ((member_swap op = i) o (#2 : O_Model.single -> int list)) oris;

filter_vat : O_Model.T -> int -> O_Model.T;

(*\------- unused code -----------------------------------------------------------------------/*)

val filtered = map (filter_vat o_model) [1,2,3];

(*DIFFERENT ARGUMENT HERE         \<up> \<up> ^  DOES not CHANGE ANYTHING .. ?error?*)

case filtered of

  [[

    (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),

    (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), 

    (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),

    (4, [1, 2], "#Relate",  Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),

    (6, [1], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("a", _)]),

    (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),

    (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])

  ], [

    (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),

    (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), 

    (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),

    (4, [1, 2], "#Relate",  Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),

    (7, [2], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("b", _)]),

    (9, [1, 2], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), [Const (\<^const_name>\<open>Collect\<close>, _) $ Abs ("x", _, Const (\<^const_name>\<open>conj\<close>, _) $ _ $ _)]),

    (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])

  ], [

    (1, [1, 2, 3], "#Given", Const (\<^const_name>\<open>Input_Descript.fixedValues\<close>, _), [Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("r", _) $ Const (\<^const_name>\<open>Program.Arbfix\<close>, _)) $ _]),

    (2, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.maximum\<close>, _), [Free ("A", _)]), 

    (3, [1, 2, 3], "#Find", Const (\<^const_name>\<open>Input_Descript.valuesFor\<close>, _), [_ $ Free ("a", _) $ _, Const (\<^const_name>\<open>Cons\<close>, _) $ Free ("b", _) $ _]),

    (5, [3], "#Relate", Const (\<^const_name>\<open>Input_Descript.relations\<close>, _), _),

    (8, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.boundVariable\<close>, _), [Free ("alpha", _)]),

    (10, [3], "#undef", Const (\<^const_name>\<open>Input_Descript.interval\<close>, _), _),

    (11, [1, 2, 3], "#undef", Const (\<^const_name>\<open>Input_Descript.errorBound\<close>, _), [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ Free ("eps", _) $ _(*"0"*)])

  ]] => ()

| _ => error "fun O_Model.filter_vat CHANGED";

"----------- regression test fun O_Model.is_copy_named -----------------------------------------";

"----------- regression test fun O_Model.is_copy_named -----------------------------------------";

"----------- regression test fun O_Model.is_copy_named -----------------------------------------";

val trm = ("1", (TermC.empty, @{term "v'i'"}));

if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 1";

val trm = ("1", (TermC.empty, @{term "e_e"}));

if O_Model.is_copy_named trm then error "regr. O_Model.is_copy_named 2" else ();

val trm = ("1", (TermC.empty, @{term "L'''"}));

if O_Model.is_copy_named trm then () else error "regr. O_Model.is_copy_named 3";

(* out-comment 'structure CalcHead'...

val trm = (1, (2, @{term "v'i'"}));

if is_copy_named_generating trm then () else error "regr. O_Model.is_copy_named";

val trm = (1, (2, @{term "L'''"}));

if is_copy_named_generating trm then error "regr. O_Model.is_copy_named" else ();

*)

"----------- .. CONTINUED regr.test fun O_Model.copy_name -------------------=------------------";

"----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";

"----------- .. CONTINUED regr.test fun O_Model.copy_name --------------------------------------";

(*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*)

(*the model-pattern, O_Model.is_copy_named are filter_out*)

val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})),

       ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))];

(*the model specific for an example*)

val oris = [([1], "#Given", @{term "equality"} , [TermC.parse_test @{context} "x+1= 2"]),

	([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])];

val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))];

(*...all must be true*)

case O_Model.copy_name pbt oris (hd cy) of 

    ([1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)]) => ()

  | _ => error "calchead.sml regr.test O_Model.copy_name-1-";

(*new data: O_Model.copy_name without changing the name*)

@{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};

@{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};

@{term "solution"}; type_of @{term "ss''' :: bool list"};

(*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*)

val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),

       ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];

(*the model specific for an example*)

val oris = [([1], "#Given", @{term "equalities"} ,[TermC.parse_test @{context} "[x_1+1=2,x_2=0]"]),

    ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])];

val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"}))

        (*could be more than 1*)];

case O_Model.copy_name pbt oris (hd cy) of

    ([1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)]) => ()

  | _ => error "calchead.sml regr.test O_Model.copy_name-2-";