|
wneuper@59298
|
1 |
signature SPECIFY_ELEMENT =
|
|
wneuper@59298
|
2 |
sig
|
|
wneuper@59298
|
3 |
type fmz
|
|
wneuper@59298
|
4 |
type fmz_
|
|
wneuper@59299
|
5 |
type result
|
|
wneuper@59299
|
6 |
val res2str : term * term list -> string
|
|
wneuper@59299
|
7 |
datatype safe = Sundef | Safe | Unsafe | Helpless;
|
|
wneuper@59299
|
8 |
val safe2str : safe -> string
|
|
wneuper@59299
|
9 |
type scrstate
|
|
wneuper@59298
|
10 |
(*----- needed for tac, tac_ immediately (probably pre-requisites missing)
|
|
wneuper@59298
|
11 |
type istate
|
|
wneuper@59298
|
12 |
type subte
|
|
wneuper@59298
|
13 |
type subs
|
|
wneuper@59298
|
14 |
type sube
|
|
wneuper@59298
|
15 |
*)
|
|
wneuper@59298
|
16 |
(* ---- for tests only: made visible in order to remove the warning --------------------------- *)
|
|
wneuper@59298
|
17 |
val e_fmz : fmz_ * spec (* for datatypes.sml *)
|
|
wneuper@59298
|
18 |
|
|
wneuper@59299
|
19 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
|
wneuper@59298
|
20 |
|
|
wneuper@59299
|
21 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
|
wneuper@59298
|
22 |
end
|
|
wneuper@59298
|
23 |
|
|
wneuper@59298
|
24 |
structure Selem(**): SPECIFY_ELEMENT(**) =
|
|
wneuper@59298
|
25 |
struct
|
|
wneuper@59298
|
26 |
|
|
wneuper@59298
|
27 |
type fmz_ = cterm' list;
|
|
wneuper@59298
|
28 |
(* a formalization of an example containing data
|
|
wneuper@59298
|
29 |
sufficient for mechanically finding the solution for the example
|
|
wneuper@59298
|
30 |
FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
|
|
wneuper@59298
|
31 |
type fmz = fmz_ * spec;
|
|
wneuper@59298
|
32 |
val e_fmz = ([], e_spec);
|
|
wneuper@59298
|
33 |
|
|
wneuper@59299
|
34 |
type result = term * term list
|
|
wneuper@59299
|
35 |
fun res2str (t, ts) = pair2str (term2str t, terms2str ts); (* for tests only *)
|
|
wneuper@59299
|
36 |
|
|
wneuper@59299
|
37 |
datatype safe = Sundef | Safe | Unsafe | Helpless;
|
|
wneuper@59299
|
38 |
fun safe2str Sundef = "Sundef"
|
|
wneuper@59299
|
39 |
| safe2str Safe = "Safe"
|
|
wneuper@59299
|
40 |
| safe2str Unsafe = "Unsafe"
|
|
wneuper@59299
|
41 |
| safe2str Helpless = "Helpless";
|
|
wneuper@59299
|
42 |
|
|
wneuper@59299
|
43 |
type scrstate = (* state for script interpreter *)
|
|
wneuper@59299
|
44 |
env(*stack*) (* used to instantiate tac for checking assod
|
|
wneuper@59299
|
45 |
12.03.noticed: e_ not updated during execution ?!? *)
|
|
wneuper@59299
|
46 |
* loc_ (* location of tac in script *)
|
|
wneuper@59299
|
47 |
* term option (* argument of curried functions *)
|
|
wneuper@59299
|
48 |
* term (* value obtained by tac executed
|
|
wneuper@59299
|
49 |
updated also after a derivation by 'new_val' *)
|
|
wneuper@59299
|
50 |
* safe (* estimation of how result will be obtained *)
|
|
wneuper@59299
|
51 |
* bool; (* true = strongly .., false = weakly associated:
|
|
wneuper@59299
|
52 |
only used during ass_dn/up *)
|
|
wneuper@59299
|
53 |
fun topt2str NONE = "NONE"
|
|
wneuper@59299
|
54 |
| topt2str (SOME t) = "SOME" ^ term2str t;
|
|
wneuper@59299
|
55 |
fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)
|
|
wneuper@59299
|
56 |
"(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
|
|
wneuper@59299
|
57 |
term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
|
|
wneuper@59299
|
58 |
|
|
wneuper@59298
|
59 |
end
|