(* Title:  "ProgLang/contextC.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

"----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";

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

"----------- fun initialise --------------------------------------------------------------------";

"----------- build fun initialise'--------------------------------------------------------------";

"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";

"----------- fun transfer_asms_from_to ---------------------------------------------------------";

"----------- fun avoid_contradict --------------------------------------------------------------";

"----------- fun subpbl_to_caller --------------------------------------------------------------";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

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

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

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

"----------- fun initialise --------------------------------------------------------------------";

"----------- fun initialise --------------------------------------------------------------------";

"----------- fun initialise --------------------------------------------------------------------";

val t = @{term "a * b + -123 * c :: real"};

val ctxt = initialise "Rational" (vars t)

(*----- now parsing infers the type *)

val SOME t = parseNEW ctxt "x";

if type_of t = HOLogic.realT then error "type inference failed 1" else ();

val SOME t = parseNEW ctxt "a";

if type_of t = HOLogic.realT then () else error "type inference failed 2";

"----------- build fun initialise'--------------------------------------------------------------";

"----------- build fun initialise'--------------------------------------------------------------";

"----------- build fun initialise'--------------------------------------------------------------";

val fmz = ["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 (thy, fmz) = (@{theory Biegelinie}, fmz);

initialise' thy fmz;

    val ctxt = thy |> Proof_Context.init_global

    val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct

    val _ = TermC.raise_type_conflicts ts;

"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";

"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";

"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";

val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;

val ctxt = ContextC.insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;

val asms = ContextC.get_assumptions ctxt;

if asms = [@{term "x * v"}, @{term "2 * u"}]

then () else error "mstools.sml insert_/get_assumptions changed 1.";

"----------- fun transfer_asms_from_to ---------------------------------------------------------";

"----------- fun transfer_asms_from_to ---------------------------------------------------------";

"----------- fun transfer_asms_from_to ---------------------------------------------------------";

val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}

val from_ctxt = ContextC.insert_assumptions

  [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt

val to_ctxt = ContextC.insert_assumptions

  [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt

val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;

if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]

then () else error "fun transfer_asms_from_to changed"

"----------- fun avoid_contradict --------------------------------------------------------------";

"----------- fun avoid_contradict --------------------------------------------------------------";

"----------- fun avoid_contradict --------------------------------------------------------------";

val preds = [

(*0.pre*)str2term "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",

(*1.pre*)str2term ("\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"

(*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x"),

(*0.asm*)str2term  "x \<noteq> 0",             (* <-------------- "x \<noteq> 0" would contradict "x = 0" ---\*)

(*0.asm*)str2term  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"

];

val t = str2term "[x = 0, x = 6 / 5]";

val (t', for_asm) = avoid_contradict t preds;

if term2str t' = "[x = 6 / 5]" andalso map term2str for_asm = ["x = 6 / 5"]

then () else error "avoid_contradict [x = 0, x = 6 / 5] CHANGED";

val t = str2term "x = 0";

val (t', for_asm) = avoid_contradict t preds;

if term2str t' = "bool_undef" andalso map term2str for_asm = []

then () else error "avoid_contradict x = 0 CHANGED"; (* "x \<noteq> 0" in preds *)

val t = str2term "x = 1";

val (t', for_asm) = avoid_contradict t preds;

if term2str t' = "x = 1" andalso map term2str for_asm = ["x = 1"]

then () else error "avoid_contradict x = 1 CHANGED"; (* "x \<noteq> 1" NOT in preds *)

val t = str2term "a + b";

val (t', for_asm) = avoid_contradict t preds;

if term2str t' = "a + b" andalso map term2str for_asm = []

then () else error "avoid_contradict a + b CHANGED"; (* NOT a predicate *)

val t = str2term "[a + b]";

val (t', for_asm) = avoid_contradict t preds;

if term2str t' = "[a + b]" andalso map term2str for_asm = []

then () else error "avoid_contradict [a + b] CHANGED"; (* NOT a predicate *)

"----------- fun subpbl_to_caller --------------------------------------------------------------";

"----------- fun subpbl_to_caller --------------------------------------------------------------";

"----------- fun subpbl_to_caller --------------------------------------------------------------";

val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}

val sub_ctxt = ContextC.insert_assumptions

  [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt

val prog_res = str2term "[x_1 = 1, x_2 = (2::int), x_3 = 3]";

(* NO contradiction ..*)

val caller_ctxt = ContextC.insert_assumptions

  [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt

val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;

if term2str t = "[x_1 = 1, x_2 = 2, x_3 = 3]" andalso map term2str (get_assumptions new_ctxt) =

  ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]

then () else error "fun subpbl_to_caller changed 1";

(* a contradiction ..*)

val caller_ctxt = ContextC.insert_assumptions

  [str2term "b < (to::int)", str2term "x_2 \<noteq> (2::int)"] ctxt

val (t, new_ctxt) = subpbl_to_caller sub_ctxt prog_res caller_ctxt;

if term2str t = "[x_1 = 1, x_3 = 3]" andalso map term2str (get_assumptions new_ctxt) =

  ["b < fro", "x_1 = 1", "x_3 = 3", "b < to", "x_2 \<noteq> 2"]

then () else error "fun subpbl_to_caller changed 2";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";

(*ER-7*) (*Schalk I s.87 Bsp 55b*)

val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",

	   "solveFor x","solutions L"];

val spec = ("RatEq",["univariate","equation"],["no_met"]);

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];                          (* 0. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*+*)case nxt of  Apply_Method ["RatEq", "solve_rat_equation"] => ()

(*+*)| _ => error "55b root specification broken";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                         (* 0. solve-phase*)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";

(*+*)if (Ctree.get_assumptions pt p |> map term2str) =

(*+*)  ["x \<noteq> 0", 

(*+*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0", 

(*+*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]

(*+*)then () else error "assumptions before 1. Subproblem CHANGED";

(*+*)if p = ([3], Res) andalso f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"

(*+*)then

(*+*)  ((case nxt of Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) => ()

(*+*)  | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))

(*+*)else error "1. Subproblem -- call changed";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 1. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;

case nxt of Apply_Method ["PolyEq", "normalise_poly"] => ()

| _ => error "55b normalise_poly specification broken 1";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                       (* 1. solve-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "-6 * x + 5 * x ^^^ 2 = 0";

if p = ([4, 3], Res) andalso f2str f = "-6 * x + 5 * x ^^^ 2 = 0"

then

  ((case nxt of Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]) => ()

  | _ => error ("S.68, Bsp.: 40 nxt =" ^ tac2str nxt)))

else error "xxx";

val (p,_,f,nxt,_,pt) = me nxt p [] pt;                                     (* 2. specify-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>*)

case nxt of Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"] => ()

| _ => error "55b normalise_poly specification broken 2";

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*f = "-6 * x + 5 * x ^^^ 2 = 0"*)    (* 2. solve-phase *)

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>Or_to_List*)

(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";

(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)

(*     *)if eq_set op = ((Ctree.get_assumptions pt p |> map term2str), [

(*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",

(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"

(*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",

(*0.asm*)  "x \<noteq> 0", 

(*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"

(*     *)])

(*     *)then () else error "assumptions at end 2. Subproblem CHANGED";

(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt;(*\<rightarrow>1. Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)

(*/--------- step into 2. Check_Postcond -----------------------------------------------------\*)

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);

    val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

"~~~~~ fun by_tactic , args:"; val (m, (ptp as (pt, p))) = (tac, (pt, p));

    val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);

	    (*if*) Tactic.for_specify' m (*else*);

    val ("ok", (([(Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"], _, _)]), _, _)) =

Step_Solve.by_tactic m ptp;

"~~~~~ fun by_tactic , args:"; val ((tac as Tactic.Check_Postcond' _), (ptp as (pt, p))) = (m, ptp);

        LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp;

"~~~~~ fun by_tactic , args:"; val ((Tactic.Check_Postcond' (pI, res)), (sub_ist, sub_ctxt), (pt, pos as (p, _)))

  = (tac, (get_istate_LI pt p, get_ctxt_LI pt p), ptp);

      val parent_pos = par_pblobj pt p

      val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);

      val prog_res =

         case LI.find_next_step scr (pt, pos) sub_ist sub_ctxt of

(*OLD*)    Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res

  |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res

(*OLD*)  | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)

(*OLD* )   vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)

(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of

(*OLD*)    Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p

(*OLD*)  | _ => Ctree.get_assumptions pt pos);

(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))

( *OLD*)

      (*if*) parent_pos = [] (*else*);

(*NEW*)   val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of

(*NEW*)     (Pstate i, c) => (i, c)

(*NEW*)   | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc";

(*     *)if eq_set op = (map term2str (get_assumptions ctxt_parent), [

(*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",

(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"

(*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",

(*0.asm*)  "x \<noteq> 0", 

(*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"

(*     *)])

(*     *)then () else error "assumptions at xxx CHANGED";

	        val (prog_res', ctxt') =

  ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent;

(*     *)if eq_set op = (map term2str (get_assumptions ctxt'), [

(*0.pre*)  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",

(*1.pre*)  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"

(*1.pre*)    ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",

(*0.asm*)  "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",

(*0.asm*)  "x \<noteq> 0",             (* <----------------------- "x \<noteq> 0" contradiction resoved ---\*)

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x", 

(*2.pre*)  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",

(*2.res*)  (*"x \<noteq> 0",*) "x = 6 / 5" (* <---------------- "x \<noteq> 0" would contradict "x = 0" ---/*)

(*     *)])

(*     *)then () else error "assumptions at xxx CHANGED";

"~~~~~ fun subpbl_to_caller , args:"; val (sub_ctxt, prog_res, caller_ctxt)

  = (sub_ctxt, prog_res, ctxt_parent);

val xxxxx = caller_ctxt

  |> get_assumptions 

  |> avoid_contradict prog_res

  |> apsnd (insert_assumptions_cao caller_ctxt)

  |> apsnd (transfer_asms_from_to sub_ctxt);

     xxxxx (*return from xxx*);

"~~~~~ from fun subpbl_to_caller \<longrightarrow>fun by_tactic , return:"; val (prog_res', ctxt')

  = (xxxxx);

(*NEW*)   val tac = Tactic.Check_Postcond' (pI, prog_res')

(*NEW*)   val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)

(*NEW*)   val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res));

(*NEW*)   ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))

           (*return from xxx*);

"~~~~~ from fun LI.by_tactic \<longrightarrow>fun Step_Solve.by_tactic \<longrightarrow>fun Step.by_tactic \<longrightarrow>fun me, return:"; val (("ok", (_, _, (pt, p))))

  = ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))));

  val ("ok", (ts as (_, _, _) :: _, _, _)) =

    (*case*) Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

  	  val tac = 

        case ts of 

          tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

  		  | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;

"~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''')

  = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), 

  	    tac, Telem.Sundef, pt);

(*\--------- step into 2. Check_Postcond -----------------------------------------------------/*)

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)

(*/-------- final test -----------------------------------------------------------------------\*)

if f2str f = "[x = 6 / 5]" andalso map term2str (Ctree.get_assumptions pt p) =

 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",

  "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",

  "\<not> matches (?a = 0)\n        ((3 + -1 * x + x ^^^ 2) * x =\n         1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n            1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",

  "x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",

  "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]

then () else error "test CHANGED";