(* Title:  "ADDTESTS/All_Ctxt.thy"

   Author: Walther Neuper

   (c) due to copyright terms

  this theory is evaluated BEFORE Test_Isac.thy opens structures.

  So, if you encounter errors here, first fix them in $ISABELLE_ISAC_TEST/Tools/isac/Minimsubpbl/* *)

theory All_Ctxt imports Isac.Build_Isac

begin

text \<open>all changes of context are demonstrated in a mini example.

  see test/../mstools.sml --- all ctxt changes in minimsubpbl x+1=2 ---\<close>

section \<open>start of the mini example\<close>

ML \<open>

  val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

  val (dI',pI',mI') =

    ("Test", ["sqroot-test", "univariate", "equation", "test"],

     ["Test", "squ-equ-test-subpbl1"]);

\<close> ML \<open>

  val (p,_,f,nxt,_,pt) = Test_Code.CalcTreeTEST [(fmz, (dI',pI',mI'))];

\<close>

section \<open>start of specify phase\<close>

text \<open>

  variables known from formalisation provide type-inference for further input

\<close>

ML \<open>

(*+*)if ((fst p) |> get_obj g_origin pt |> LibraryC.fst3) <> []

(*+*)then () else error "check correct of get_ctxt at start of (sub-)problem";

  val ctxt = Ctree.get_ctxt pt p; 

  (*must NOT check ThyC.id_empty in specify_data.spec,      .. is still empty in this case  

    but for References_Def.T in specify_data.origin.        .. is already assigned in this case

                                                               and in case of CAS-cmd          *)

  val SOME known_x = TermC.parseNEW ctxt "x + y + z";

  val SOME unknown = TermC.parseNEW ctxt "a + b + c";

  if type_of known_x = HOLogic.realT andalso 

     type_of unknown = TFree ("'a",["Groups.plus"])

  then () else error "All_Ctx: type constraints beginning specification of root-problem ";

\<close>

ML \<open>

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

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

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

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

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

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

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

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

\<close>

section \<open>start interpretation of method\<close>

text \<open>preconditions are known at start of interpretation of (root-)method\<close>

ML \<open>

  if UnparseC.terms_to_strings (Ctree.get_assumptions pt p) = ["precond_rootmet x"]

  then () else error "All_Ctx: asms after start interpretation of root-method";

\<close>

ML \<open>

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

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

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

\<close>

section \<open>start a subproblem: specification\<close>

text \<open>

  ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args"

  and extended with the types of the variables in args.\<close>

ML \<open>(*not significant in this example*)

  val ctxt = Ctree.get_ctxt pt p;

  val SOME known_x = TermC.parseNEW ctxt "x+y+z";

  val SOME unknown = TermC.parseNEW ctxt "a+b+c";

  if type_of known_x = HOLogic.realT andalso 

     type_of unknown = TFree ("'a",["Groups.plus"])

  then () else error "All_Ctx: type constraints beginning specification of SubProblem ";

\<close>

ML \<open>

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

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

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

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

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

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

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

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

\<close>

section \<open>interpretation of subproblem's method\<close>

text \<open>preconds are known at start of interpretation of (sub-)method\<close>

ML \<open>

\<close> ML \<open>

\<close>

ML \<open>

  if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

    ["matches (?a = ?b) (- 1 + x = 0)", "precond_rootmet x"])

  then () else error "All_Ctx: asms after start interpretation of SubProblem";

\<close>

ML \<open>

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

\<close>

ML \<open>

  "artifically inject assumptions";

  val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p);

  val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out",

                                 TermC.str2term "a < sub_asm_local"] cres;

  val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));

\<close>

ML \<open>

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

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

\<close>

section \<open>finish subproblem, return to calling method\<close>

text \<open>transfer non-local assumptions and result from sub-method to root-method.

  non-local assumptions are those contaning a variable known in root-method.

\<close>

ML \<open>

eq_set

\<close>

ML \<open>

  if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

    ["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])

  then () else error "All_Ctx: asms after finishing SubProblem";

\<close>

ML \<open>

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

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

\<close>

section \<open>finish Lucas interpretation\<close>

text \<open>assumptions collected during lucas-interpretation for proof of postcondition\<close>

ML \<open>

\<close> ML \<open>

\<close>

ML \<open>

  if eq_set op = (UnparseC.terms_to_strings (Ctree.get_assumptions pt p),

    ["matches (?a = ?b) (- 1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])

  then () else error "All_Ctx at final result";

\<close>

ML \<open>

  Test_Tool.show_pt pt;

\<close>

ML \<open>

\<close> ML \<open>

\<close>

end