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 "--------------------------------------------------------";
15 "--------------------------------------------------------";
16 "--------------------------------------------------------";
17 "--------------------------------------------------------";
20 "----------- fun declare_constraints --------------------";
21 "----------- fun declare_constraints --------------------";
22 "----------- fun declare_constraints --------------------";
23 val ctxt = ProofContext.init_global @{theory "Isac"}
24 |> declare_constraints "xxx + yyy = (111::int)";
25 val t = case parseNEW ctxt "xxx = 123" of
26 NONE => error "mstools: syntax error"
28 if ((lhs t) |> type_of) = @{typ int} then ()
29 else error "mstools: incorrect type inference from parseNEW ctxt";
32 "----------- fun get_assumptions, fun get_environments --";
33 "----------- fun get_assumptions, fun get_environments --";
34 "----------- fun get_assumptions, fun get_environments --";
35 val ctxt = insert_assumptions
36 [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
37 val ctxt = insert_assumptions
38 [@{term "x * v"}, @{term "2 * u"}] ctxt;
39 val asms = get_assumptions ctxt;
40 if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
41 else error "mstools.sml insert_/get_assumptions changed 1.";
43 val ctxt = insert_environments
44 [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
45 val envs = get_environments ctxt;
46 if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
47 else error "mstools.sml insert_/get_environments changed 2.";
50 "----------- fun transfer_from_subproblem ---------------";
51 "----------- fun transfer_from_subproblem ---------------";
52 "----------- fun transfer_from_subproblem ---------------";
53 terms2str (get_assumptions ctxt);
54 val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
55 val ctxt_sub = insert_assumptions [@{term "x ~= 0"}] ctxt;
56 val ctxt' = transfer_from_subproblem ctxt_sub ctxt;
57 terms2str (get_assumptions ctxt');
58 if get_assumptions ctxt' = [@{term "x ~= 0"}, @{term "x * v"}, @{term "2 * u"}]
59 then () else error "mstools.sml transfer_from_subproblem changed."