4 *) |
4 *) |
5 |
5 |
6 "-----------------------------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------------------------------------"; |
9 "----------- check all handling of context -----------------------------------------------------"; |
9 "----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------"; |
|
10 "-----------------------------------------------------------------------------------------------"; |
|
11 "----------- fun initialise --------------------------------------------------------------------"; |
|
12 "----------- build fun initialise'--------------------------------------------------------------"; |
|
13 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------"; |
|
14 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
|
15 "----------- fun from_subpbl_to_caller ---------------------------------------------------------"; |
|
16 "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------"; |
10 "-----------------------------------------------------------------------------------------------"; |
17 "-----------------------------------------------------------------------------------------------"; |
11 "-----------------------------------------------------------------------------------------------"; |
18 "-----------------------------------------------------------------------------------------------"; |
12 "-----------------------------------------------------------------------------------------------"; |
19 "-----------------------------------------------------------------------------------------------"; |
13 |
20 |
14 |
21 |
15 "----------- check all handling of context -----------------------------------------------------"; |
22 "----------- fun initialise --------------------------------------------------------------------"; |
16 "----------- check all handling of context -----------------------------------------------------"; |
23 "----------- fun initialise --------------------------------------------------------------------"; |
17 "----------- check all handling of context -----------------------------------------------------"; |
24 "----------- fun initialise --------------------------------------------------------------------"; |
18 (* waits in Test_Some.thy for checking further updates to context handling *) |
25 val t = @{term "a * b + -123 * c :: real"}; |
|
26 val ctxt = initialise "Rational" (vars t) |
|
27 |
|
28 (*----- now parsing infers the type *) |
|
29 val SOME t = parseNEW ctxt "x"; |
|
30 if type_of t = HOLogic.realT then error "type inference failed 1" else (); |
|
31 |
|
32 val SOME t = parseNEW ctxt "a"; |
|
33 if type_of t = HOLogic.realT then () else error "type inference failed 2"; |
|
34 |
|
35 "----------- build fun initialise'--------------------------------------------------------------"; |
|
36 "----------- build fun initialise'--------------------------------------------------------------"; |
|
37 "----------- build fun initialise'--------------------------------------------------------------"; |
|
38 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y", |
|
39 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", |
|
40 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", |
|
41 "AbleitungBiegelinie dy"]; |
|
42 val (thy, fmz) = (@{theory Biegelinie}, fmz); |
|
43 |
|
44 initialise' thy fmz; |
|
45 |
|
46 val ctxt = thy |> Proof_Context.init_global |
|
47 val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct |
|
48 val _ = TermC.raise_type_conflicts ts; |
|
49 |
|
50 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------"; |
|
51 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------"; |
|
52 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------"; |
|
53 val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt; |
|
54 val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt; |
|
55 val asms = get_assumptions ctxt; |
|
56 if asms = [@{term "x * v"}, @{term "2 * u"}] |
|
57 then () else error "mstools.sml insert_/get_assumptions changed 1."; |
|
58 |
|
59 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
|
60 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
|
61 "----------- fun transfer_asms_from_to ---------------------------------------------------------"; |
|
62 val ctxt = Proof_Context.init_global @{theory "Isac"} |
|
63 val from_ctxt = insert_assumptions |
|
64 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt |
|
65 val to_ctxt = insert_assumptions |
|
66 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt |
|
67 val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt; |
|
68 if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"] |
|
69 then () else error "fun transfer_asms_from_to changed" |
|
70 |
|
71 "----------- fun from_subpbl_to_caller ---------------------------------------------------------"; |
|
72 "----------- fun from_subpbl_to_caller ---------------------------------------------------------"; |
|
73 "----------- fun from_subpbl_to_caller ---------------------------------------------------------"; |
|
74 val ctxt = Proof_Context.init_global @{theory "Isac"} |
|
75 val sub_ctxt = insert_assumptions |
|
76 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt |
|
77 val caller_ctxt = insert_assumptions |
|
78 [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt |
|
79 val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]"; |
|
80 val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt; |
|
81 if terms2strs (get_assumptions new_ctxt) = |
|
82 ["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"] |
|
83 then () else error "fun from_subpbl_to_caller changed" |
|
84 |
|
85 |
|
86 |
|
87 "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------"; |
|
88 "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------"; |
|
89 "----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------"; |
|
90 (* waits in Test_Some.thy *) |