13 ["Test","squ-equ-test-subpbl1"]); |
13 ["Test","squ-equ-test-subpbl1"]); |
14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
15 *} |
15 *} |
16 |
16 |
17 section {* start of specify phase *} |
17 section {* start of specify phase *} |
18 |
|
19 text {* variables known from formalisation provide type-inference |
18 text {* variables known from formalisation provide type-inference |
20 for further input *} |
19 for further input *} |
21 |
20 |
22 ML {* |
21 ML {* |
23 val ctxt = get_ctxt pt p; |
22 val ctxt = get_ctxt pt p; |
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
37 *} |
36 *} |
38 |
37 |
39 section {* start interpretation of method *} |
38 section {* start interpretation of method *} |
40 |
|
41 text {* preconditions are known at start of interpretation of (root-)method *} |
39 text {* preconditions are known at start of interpretation of (root-)method *} |
42 |
40 |
43 ML {* |
41 ML {* |
44 get_assumptions_ pt p |> terms2strs; |
42 get_assumptions_ pt p |> terms2strs; |
45 *} |
43 *} |
46 |
44 |
47 ML {* |
45 ML {* |
48 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
46 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
49 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
47 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
50 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
48 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
51 *} |
49 *} |
52 |
50 |
53 section {* start a subproblem: specification *} |
51 section {* start a subproblem: specification *} |
|
52 text {* |
|
53 ctxt is initialised from the thy in "SubProblem (thy, pbl, met) args" |
|
54 and extended with the types of the variables in args. *} |
54 |
55 |
55 text {* variables known from arguments of (sub-)method provide type-inference for further input *} |
56 ML {* (*not significant in this example*) |
56 |
|
57 ML {* |
|
58 val ctxt = get_ctxt pt p; |
57 val ctxt = get_ctxt pt p; |
59 val SOME known_x = parseNEW ctxt "x+y+z"; |
58 val SOME known_x = parseNEW ctxt "x+y+z"; |
60 val SOME unknown = parseNEW ctxt "a+b+c"; |
59 val SOME unknown = parseNEW ctxt "a+b+c"; |
61 *} |
60 *} |
62 |
61 |