1 (* Title: tests for Interpret/mstools.sml |
1 (* Title: tests for Interpret/mstools.sml |
2 Author: Walther Neuper 100930 |
2 Author: Walther Neuper 100930, Mathias Lehnfeld |
3 (c) copyright due to lincense terms. |
3 (c) copyright due to lincense terms. |
4 |
4 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
6 10 20 30 40 50 60 70 80 |
6 10 20 30 40 50 60 70 80 |
7 *) |
7 *) |
8 "--------------------------------------------------------"; |
8 "--------------------------------------------------------"; |
9 "table of contents --------------------------------------"; |
9 "table of contents --------------------------------------"; |
10 "--------------------------------------------------------"; |
10 "--------------------------------------------------------"; |
11 "----------- fun declare_constraints --------------------"; |
11 "----------- fun declare_constraints --------------------"; |
|
12 "----------- fun get_assumptions, fun get_environments --"; |
12 "--------------------------------------------------------"; |
13 "--------------------------------------------------------"; |
13 "--------------------------------------------------------"; |
14 "--------------------------------------------------------"; |
14 "--------------------------------------------------------"; |
15 "--------------------------------------------------------"; |
15 "--------------------------------------------------------"; |
16 "--------------------------------------------------------"; |
16 |
17 |
24 NONE => error "mstools: syntax error" |
25 NONE => error "mstools: syntax error" |
25 | SOME t' => t'; |
26 | SOME t' => t'; |
26 if ((lhs t) |> type_of) = @{typ int} then () |
27 if ((lhs t) |> type_of) = @{typ int} then () |
27 else error "mstools: incorrect type inference from parseNEW ctxt"; |
28 else error "mstools: incorrect type inference from parseNEW ctxt"; |
28 |
29 |
29 (*========== inhibit exn ======================================================= |
|
30 ============ inhibit exn =====================================================*) |
|
31 |
30 |
32 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
31 "----------- fun get_assumptions, fun get_environments --"; |
33 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
32 "----------- fun get_assumptions, fun get_environments --"; |
|
33 "----------- fun get_assumptions, fun get_environments --"; |
|
34 val ctxt = insert_assumptions |
|
35 [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt; |
|
36 val ctxt = insert_environments |
|
37 [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt; |
|
38 |
|
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."; |
|
42 |
|
43 val envs = get_environments ctxt; |
|
44 if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then () |
|
45 else error "mstools.sml insert_/get_environments changed."; |
|
46 |