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

 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 f_model = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

   val f_refs =

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

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

 \<close> ML \<open>

   val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_refs)];

 \<close> ML \<open>

   val PblObj {ctxt, ...} = Ctree.get_obj I pt (#1 p)

   val Free ("x", Type ("Real.real", [])) = Syntax.read_term ctxt "x"

   val Free ("a", TFree ("'a", ["HOL.type"])) = Syntax.read_term ctxt "a"

 \<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 known_x = Syntax.read_term ctxt "x + y + z";

   val unknown = Syntax.read_term 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;

 (*[1], Frm*)val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt; val Rewrite_Set "norm_equation" = nxt;

 \<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 @{context} (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;

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

 \<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>

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

 \<close> ML \<open>

   val PblObj {ctxt, ...} = Ctree.get_obj I pt (#1 p)

   val Free ("x", Type ("Real.real", [])) = Syntax.read_term ctxt "x"

   val Free ("a", TFree ("'a", ["HOL.type"])) = Syntax.read_term ctxt "a"

 \<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; 

 \<close>

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

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

 ML \<open>

 if eq_set op = ( UnparseC.asms_test @{context} (Ctree.get_assumptions pt p),

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

 then () else error "preconds at start of method CHANGED";

 \<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 [ParseC.parse_test @{context} "x < sub_asm_out",

                                  ParseC.parse_test @{context} "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>

   if eq_set op = (UnparseC.asms_test @{context} (Ctree.get_assumptions pt p),

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

   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.asms_test  @{context} (Ctree.get_assumptions pt p),

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

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

 \<close>

 ML \<open>

   Test_Tool.show_pt pt;

 \<close>

 ML \<open>

 \<close> ML \<open>

 \<close>

 end