intermed. ctxt ..: cleanup before start with Add_Given
uncommenting in src/../calchead.sm 2x "update_env" after "prep_ori"
marked with GOON.WN110506
causes errors in most test/../*, all with CalcTreeTEST; me; ..
1 (* Title: tests for Interpret/mstools.sml
2 Author: Walther Neuper 100930, Mathias Lehnfeld
3 (c) copyright due to lincense terms.
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
8 "--------------------------------------------------------";
9 "table of contents --------------------------------------";
10 "--------------------------------------------------------";
11 "----------- fun declare_constraints --------------------";
12 "----------- fun get_assumptions, fun get_environments --";
13 "----------- fun transfer_from_subproblem ---------------";
14 "----------- all handling ctxt in minimsubpbl x+1=2 -----";
15 "--------------------------------------------------------";
16 "--------------------------------------------------------";
17 "--------------------------------------------------------";
18 "--------------------------------------------------------";
21 "----------- fun declare_constraints --------------------";
22 "----------- fun declare_constraints --------------------";
23 "----------- fun declare_constraints --------------------";
24 val ctxt = ProofContext.init_global @{theory "Isac"}
25 |> declare_constraints "xxx + yyy = (111::int)";
26 val t = case parseNEW ctxt "xxx = 123" of
27 NONE => error "mstools: syntax error"
29 if ((lhs t) |> type_of) = @{typ int} then ()
30 else error "mstools: incorrect type inference from parseNEW ctxt";
33 "----------- fun get_assumptions, fun get_environments --";
34 "----------- fun get_assumptions, fun get_environments --";
35 "----------- fun get_assumptions, fun get_environments --";
36 val ctxt = insert_assumptions
37 [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
38 val ctxt = insert_assumptions
39 [@{term "x * v"}, @{term "2 * u"}] ctxt;
40 val asms = get_assumptions ctxt;
41 if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
42 else error "mstools.sml insert_/get_assumptions changed 1.";
44 val ctxt = insert_environments
45 [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
46 val envs = get_environments ctxt;
47 if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
48 else error "mstools.sml insert_/get_environments changed 2.";
51 "----------- fun transfer_from_subproblem ---------------";
52 "----------- fun transfer_from_subproblem ---------------";
53 "----------- fun transfer_from_subproblem ---------------";
54 terms2str (get_assumptions ctxt);
55 val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
56 val ctxt_sub = insert_assumptions [@{term "x ~= 0"}] ctxt;
57 val ctxt' = transfer_from_subproblem ctxt_sub ctxt;
58 terms2str (get_assumptions ctxt');
59 if get_assumptions ctxt' = [@{term "x ~= 0"}, @{term "x * v"}, @{term "2 * u"}]
60 then () else error "mstools.sml transfer_from_subproblem changed."
63 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
64 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
65 "----------- all handling ctxt in minimsubpbl x+1=2 ----";
66 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
68 ("Test", ["sqroot-test","univariate","equation","test"],
69 ["Test","squ-equ-test-subpbl1"]);
70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
71 print_depth 999; pt; (*see tmp/del.sml*)
72 (*GOON ---------------------------
73 val SOME (_, ctxt) = get_obj g_env pt (fst p);
74 if parseNEW ctxt "x+y+z" = parseNEW ctxt "x+y+(z::real)" andalso
75 parseNEW ctxt "a+b+c" <> parseNEW ctxt "a+b+(c::real)" then ()
76 else error "mstools.sml: ctxt initialisation broken in rootproblem";
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 (*nxt = Specify_Problem*)
83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
84 (* check precond_root_1, precond_root_2 in root-ctxt TODO *)
85 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
86 (*nxt = Apply_Method*)
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 (* check precond_root_1, precond_root_2 in sub-ctxt TODO *)
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 (* check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a in subproblem*)
94 print_depth 999; pt; (*see tmp/del.sml*)
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 ---------------------------GOON *)