(* Title: tests for Interpret/mstools.sml

   Author: Walther Neuper 100930, Mathias Lehnfeld

   (c) copyright due to lincense terms.

12345678901234567890123456789012345678901234567890123456789012345678901234567890

        10        20        30        40        50        60        70        80

*)

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

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

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

"----------- fun declare_constraints' -------------------";

"----------- fun declare_constraints --------------------";

"----------- fun get_assumptions, fun get_environments --";

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

"----------- fun from_subpbl_to_caller ------------------";

"----------- all ctxt changes in minimsubpbl x+1=2 ------";

"----------- go through Model_Problem until nxt_tac -----";

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

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

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

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

"----------- fun declare_constraints' -------------------";

"----------- fun declare_constraints' -------------------";

"----------- fun declare_constraints' -------------------";

val ctxt = ProofContext.init_global @{theory "Isac"};

val SOME ta = parseNEW ctxt "x";

if type_of ta = TFree ("'a",[]) then () else error "TODO";

(*----- add a type constraint to ctxt *)

val SOME ti = parseNEW ctxt "x::int";

val ctxt = declare_constraints' [ti] ctxt;

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

val SOME t = parseNEW ctxt "x";

if type_of t = Type ("Int.int",[]) then () else error "TODO";

"----------- fun declare_constraints --------------------";

"----------- fun declare_constraints --------------------";

"----------- fun declare_constraints --------------------";

val ctxt = ProofContext.init_global @{theory "Isac"}

      |> declare_constraints "xxx + yyy = (111::int)";

val t = case parseNEW ctxt "xxx = 123" of

      NONE => error "mstools: syntax error"

    | SOME t' => t';

if ((lhs t) |> type_of) = @{typ int} then ()

  else error "mstools: incorrect type inference from parseNEW ctxt";

val t_bit = Syntax.read_term ctxt "11::int";

val t_free = numbers_to_string t_bit;

val ctxt = ProofContext.init_global @{theory "Isac"};

val SOME t = parseNEW ctxt "11";

if (t |> type_of) = TFree ("'a", ["Int.number"]) then ()

else error "parsed numeral correct";

val ctxt' = Variable.declare_constraints t_free ctxt;

val SOME t' = parseNEW ctxt' "11";

if (t' |> type_of) = TFree ("'a", ["Int.number"]) then ()

else error "Variable.declare_constraints did not recognize numeral";

"----------- fun get_assumptions, fun get_environments --";

"----------- fun get_assumptions, fun get_environments --";

"----------- fun get_assumptions, fun get_environments --";

val ctxt = insert_assumptions

      [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;

val ctxt = insert_assumptions

      [@{term "x * v"}, @{term "2 * u"}] ctxt;

val asms = get_assumptions ctxt;

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

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

val ctxt = insert_environments

      [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;

val envs = get_environments ctxt;

if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()

else error "mstools.sml insert_/get_environments changed 2.";

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

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

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

val ctxt = ProofContext.init_global @{theory "Isac"}

val from_ctxt = insert_assumptions

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

val to_ctxt = 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 from_subpbl_to_caller ------------------";

"----------- fun from_subpbl_to_caller ------------------";

"----------- fun from_subpbl_to_caller ------------------";

val ctxt = ProofContext.init_global @{theory "Isac"}

val sub_ctxt = insert_assumptions

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

val caller_ctxt = insert_assumptions

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

val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";

val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;

if terms2strs (get_assumptions new_ctxt) =

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

then () else error "fun from_subpbl_to_caller changed"

"----------- all ctxt changes in minimsubpbl x+1=2 ------";

"----------- all ctxt changes in minimsubpbl x+1=2 ------";

"----------- all ctxt changes in minimsubpbl x+1=2 ------";

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"]);

(*========== inhibit exn AK110725 ================================================

(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)

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

========== inhibit exn AK110725 ================================================*)

(*========== inhibit exn AK110725 ================================================

(* ERROR: pt and  p are not declared due to above error *)

"=(1)= variables known from formalisation provide type-inference for further input";

val ctxt = get_ctxt pt p;

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

val SOME unknown = parseNEW ctxt "xa+b+c";

if type_of known_x = Type ("RealDef.real",[]) then ()

else error "x+1=2 after start root-pbl wrong type-inference from known x";

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

else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";

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;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)

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

"=(2)= preconditions are known at start of interpretation of (root-)method";

if get_assumptions_ pt p = [str2term "precond_rootmet x"] then ()

else error "x+1=2 after start root-met no precondition";

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

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)

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

"=(3)= variables known from arguments of (sub-)method provide type-inference for further input";

val ctxt = get_ctxt pt p;

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

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

if type_of known_x = Type ("RealDef.real",[]) then ()

else error "x+1=2 after start root-pbl wrong type-inference for known x";

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

else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";

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;

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)

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

"=(4)= preconds are known at start of interpretation of (sub-)method";

if get_assumptions_ pt p =

  [parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"] then ()

else error "x+1=2 after start sub-met no precondition";

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

"prep =(5)=: inject assumptions into sub-met: sub_asm_out, sub_asm_local";

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

val ctxt = insert_assumptions [str2term "x < sub_asm_out", str2term "a < sub_asm_local"] cres;

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

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);

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

"=(5)= transfer non-local assumptions and result from sub-method to root-method." ^

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

if terms2strs (get_assumptions_ pt p) =

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

  then () else error "x+1=2 transfer from sub-met to root-met changed";

val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)

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

"=(6)= assumptions collected during lucas-interpretation for proof of postcondition";

if terms2strs (get_assumptions_ pt p) = (*weak check: sub-result = root-result = [x = 1]*)

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

  then () else error "x+1=2 transfer from sub-met to root-met changed";

========== inhibit exn AK110725 ================================================*)

"----------- go through Model_Problem until nxt_tac -----";

"----------- go through Model_Problem until nxt_tac -----";

"----------- go through Model_Problem until nxt_tac -----";

(*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*)

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"]);

(*========== inhibit exn AK110725 ================================================

(* ERROR: same as above, see lines 120- 123 *)

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

========== inhibit exn AK110725 ================================================*)

(*========== inhibit exn AK110725 ================================================

(* ERROR: p, nxt, pt not declared due to above error *)

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

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

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

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

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

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

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

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

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

val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Subproblem",*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Model_Problem",*)

"~~~~~ fun me, args:"; val (_,tac) = nxt;

val (pt, p) = case locatetac tac (pt,p) of

	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";

"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))

val pIopt = get_pblID (pt,ip);

tacis; (*= []*)

pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)

"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);

val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),

			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;

just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false=oldNB*)

val cpI = if pI = e_pblID then pI' else pI;

		val cmI = if mI = e_metID then mI' else mI;

		val {ppc, prls, where_, ...} = get_pbt cpI;

		val pre = check_preconds "thy 100820" prls where_ probl;

		val pb = foldl and_ (true, map fst pre);

val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 

			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI); (*tac = Add_Given "equality (-1 + x = 0)"*)

"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);

"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);

val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),

		  probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;

val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;

val cpI = if pI = e_pblID then pI' else pI;

val ctxt = get_ctxt pt (p, Pbl);

"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = (ctxt, sel, oris, pbl, ((#ppc o get_pbt) cpI), ct);

val SOME t = parseNEW ctxt str;

is_known ctxt sel oris t;

"~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);

val _ = tracing ("RM is_known: t=" ^ term2str t);

val ots = (distinct o flat o (map #5)) (ori:ori list);

val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;

val (d, ts) = split_dts t;

"~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;

(*if is_dsc d then () else error "TODO";*)

if is_dsc d then () else error "TODO";

"----- these were the errors (call hierarchy from bottom up)";

appl_add ctxt sel oris pbl ((#ppc o get_pbt) cpI) ct;(*WAS

Err "[error] appl_add: is_known: identifiers [equality] not in example"*)

nxt_specif_additem "#Given" ct ptp;(*WAS

Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)

nxt_specif tac ptp;(*WAS

Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)

nxt_specify_ (pt,ip); (*WAS

Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)

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

Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)

========== inhibit exn AK110725 ================================================*)