wneuper@59308
|
1 |
(* Title: Specify-phase: specifying and modeling a problem or a subproblem. The
|
wneuper@59308
|
2 |
most important types are declared in mstools.sml.
|
wneuper@59308
|
3 |
TODO: allocate elements of Selem and of Stool appropriately
|
wneuper@59308
|
4 |
Author: Walther Neuper 991122, Mathias Lehnfeld
|
wneuper@59308
|
5 |
(c) due to copyright terms
|
wneuper@59308
|
6 |
*)
|
wneuper@59298
|
7 |
signature SPECIFY_ELEMENT =
|
wneuper@59298
|
8 |
sig
|
wneuper@59298
|
9 |
type fmz
|
wneuper@59298
|
10 |
type fmz_
|
wneuper@59299
|
11 |
type result
|
wneuper@59299
|
12 |
val res2str : term * term list -> string
|
wneuper@59299
|
13 |
datatype safe = Sundef | Safe | Unsafe | Helpless;
|
wneuper@59299
|
14 |
val safe2str : safe -> string
|
wneuper@59299
|
15 |
type scrstate
|
wneuper@59300
|
16 |
datatype istate = RrlsState of rrlsstate | ScrState of scrstate | Uistate
|
wneuper@59300
|
17 |
val istate2str : istate -> string
|
wneuper@59300
|
18 |
val e_istate : istate
|
wneuper@59301
|
19 |
type subs
|
wneuper@59301
|
20 |
type sube
|
wneuper@59301
|
21 |
type subte
|
wneuper@59301
|
22 |
val sube2str : cterm' list -> string
|
wneuper@59301
|
23 |
val sube2subst : theory -> cterm' list -> (term * term) list
|
wneuper@59301
|
24 |
val sube2subte : cterm' list -> term list
|
wneuper@59301
|
25 |
val subs2subst : theory -> cterm' list -> (term * term) list
|
wneuper@59301
|
26 |
val subst2sube : (term * term) list -> cterm' list (* for datatypes.sml *)
|
wneuper@59301
|
27 |
val subst2subs : (term * term) list -> cterm' list
|
wneuper@59301
|
28 |
val subst2subs' : (term * term) list -> (string * string) list
|
wneuper@59301
|
29 |
val subte2sube : term list -> cterm' list
|
wneuper@59301
|
30 |
val e_ctxt : Proof.context
|
wneuper@59298
|
31 |
(*----- needed for tac, tac_ immediately (probably pre-requisites missing)
|
wneuper@59298
|
32 |
type istate
|
wneuper@59298
|
33 |
type subte
|
wneuper@59298
|
34 |
type subs
|
wneuper@59298
|
35 |
type sube
|
wneuper@59298
|
36 |
*)
|
wneuper@59310
|
37 |
(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
|
wneuper@59301
|
38 |
val e_fmz : fmz_ * spec (* for datatypes.sml *)
|
wneuper@59301
|
39 |
val e_sube : cterm' list
|
wneuper@59301
|
40 |
val e_subs : string list
|
wneuper@59301
|
41 |
val scrstate2str : subst * loc_ * term option * term * safe * bool -> string
|
wneuper@59301
|
42 |
val istates2str : istate option * istate option -> string
|
wneuper@59301
|
43 |
val subte2subst : term list -> (term * term) list
|
wneuper@59310
|
44 |
(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
|
wneuper@59310
|
45 |
(* NONE *)
|
wneuper@59310
|
46 |
( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
|
wneuper@59298
|
47 |
|
wneuper@59310
|
48 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59310
|
49 |
(*----- unused code, kept as hints to design ideas ---------------------------------------------*)
|
wneuper@59310
|
50 |
(* NONE *)
|
wneuper@59298
|
51 |
end
|
wneuper@59298
|
52 |
|
wneuper@59298
|
53 |
structure Selem(**): SPECIFY_ELEMENT(**) =
|
wneuper@59298
|
54 |
struct
|
wneuper@59298
|
55 |
|
wneuper@59298
|
56 |
type fmz_ = cterm' list;
|
wneuper@59298
|
57 |
(* a formalization of an example containing data
|
wneuper@59298
|
58 |
sufficient for mechanically finding the solution for the example
|
wneuper@59298
|
59 |
FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
|
wneuper@59298
|
60 |
type fmz = fmz_ * spec;
|
wneuper@59298
|
61 |
val e_fmz = ([], e_spec);
|
wneuper@59298
|
62 |
|
wneuper@59299
|
63 |
type result = term * term list
|
wneuper@59299
|
64 |
fun res2str (t, ts) = pair2str (term2str t, terms2str ts); (* for tests only *)
|
wneuper@59299
|
65 |
|
wneuper@59299
|
66 |
datatype safe = Sundef | Safe | Unsafe | Helpless;
|
wneuper@59299
|
67 |
fun safe2str Sundef = "Sundef"
|
wneuper@59299
|
68 |
| safe2str Safe = "Safe"
|
wneuper@59299
|
69 |
| safe2str Unsafe = "Unsafe"
|
wneuper@59299
|
70 |
| safe2str Helpless = "Helpless";
|
wneuper@59299
|
71 |
|
wneuper@59299
|
72 |
type scrstate = (* state for script interpreter *)
|
wneuper@59374
|
73 |
LTool.env(*stack*) (* used to instantiate tac for checking assod
|
wneuper@59299
|
74 |
12.03.noticed: e_ not updated during execution ?!? *)
|
wneuper@59299
|
75 |
* loc_ (* location of tac in script *)
|
wneuper@59299
|
76 |
* term option (* argument of curried functions *)
|
wneuper@59299
|
77 |
* term (* value obtained by tac executed
|
wneuper@59299
|
78 |
updated also after a derivation by 'new_val' *)
|
wneuper@59299
|
79 |
* safe (* estimation of how result will be obtained *)
|
wneuper@59299
|
80 |
* bool; (* true = strongly .., false = weakly associated:
|
wneuper@59299
|
81 |
only used during ass_dn/up *)
|
wneuper@59299
|
82 |
fun topt2str NONE = "NONE"
|
wneuper@59299
|
83 |
| topt2str (SOME t) = "SOME" ^ term2str t;
|
wneuper@59299
|
84 |
fun scrstate2str (env, loc_, topt, t, safe, bool) = (* for tests only *)
|
wneuper@59299
|
85 |
"(" ^ env2str env ^ ", " ^ loc_2str loc_ ^ ", " ^ topt2str topt ^ ", \n" ^
|
wneuper@59299
|
86 |
term2str t ^ ", " ^ safe2str safe ^ ", " ^ bool2str bool ^ ")";
|
wneuper@59299
|
87 |
|
wneuper@59300
|
88 |
(* for handling type istate see fun from_pblobj_or_detail', +? *)
|
wneuper@59300
|
89 |
datatype istate = (*interpreter state*)
|
wneuper@59300
|
90 |
Uistate (*undefined in modspec, in '_deriv'ation*)
|
wneuper@59300
|
91 |
| ScrState of scrstate (*for script interpreter*)
|
wneuper@59300
|
92 |
| RrlsState of rrlsstate; (*for reverse rewriting*)
|
wneuper@59300
|
93 |
val e_istate = (ScrState ([], [], NONE, e_term, Sundef, false));
|
wneuper@59300
|
94 |
|
wneuper@59300
|
95 |
fun rta2str (r, (t, a)) = "\n(" ^ rule2str r ^ ",(" ^ term2str t ^", " ^ terms2str a ^ "))";
|
wneuper@59300
|
96 |
fun istate2str Uistate = "Uistate"
|
wneuper@59300
|
97 |
| istate2str (ScrState (e, l, to, t, s, b)) =
|
wneuper@59300
|
98 |
"ScrState ("^ subst2str e ^ ",\n " ^
|
wneuper@59300
|
99 |
loc_2str l ^ ", " ^ termopt2str to ^ ",\n " ^
|
wneuper@59300
|
100 |
term2str t ^ ", " ^ safe2str s ^ ", " ^ bool2str b ^ ")"
|
wneuper@59300
|
101 |
| istate2str (RrlsState (t, t1, rss, rtas)) =
|
wneuper@59300
|
102 |
"RrlsState (" ^ term2str t ^ ", " ^ term2str t1 ^ ", " ^
|
wneuper@59300
|
103 |
(strs2str o (map (strs2str o (map rule2str)))) rss ^ ", " ^
|
wneuper@59300
|
104 |
(strs2str o (map rta2str)) rtas ^ ")";
|
wneuper@59300
|
105 |
fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
|
wneuper@59300
|
106 |
| istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
|
wneuper@59300
|
107 |
| istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
|
wneuper@59300
|
108 |
| istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
|
wneuper@59300
|
109 |
|
wneuper@59301
|
110 |
type subs = cterm' list; (*16.11.00 for FE-KE*)
|
wneuper@59301
|
111 |
val e_subs = ["(bdv, x)"]; (* for tests only *)
|
wneuper@59301
|
112 |
|
wneuper@59301
|
113 |
(* argument type of tac Rewrite_Inst *)
|
wneuper@59301
|
114 |
type sube = cterm' list;
|
wneuper@59301
|
115 |
val e_sube = []: cterm' list; (* for tests only *)
|
wneuper@59301
|
116 |
fun sube2str s = strs2str s;
|
wneuper@59301
|
117 |
|
wneuper@59301
|
118 |
(* _sub_stitution as _t_erms of _e_qualities *)
|
wneuper@59301
|
119 |
type subte = term list;
|
wneuper@59301
|
120 |
|
wneuper@59301
|
121 |
val subte2sube = map term2str;
|
wneuper@59301
|
122 |
val subst2subs = map (pair2str o (apfst term2str) o (apsnd term2str));
|
wneuper@59301
|
123 |
fun subst2sube subst = map term2str (map HOLogic.mk_eq subst)
|
wneuper@59301
|
124 |
val subst2subs' = map ((apfst term2str) o (apsnd term2str));
|
wneuper@59389
|
125 |
fun subs2subst thy s = map (TermC.isapair2pair o (TermC.parse_patt thy)) s;
|
wneuper@59390
|
126 |
fun sube2subst thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
|
wneuper@59389
|
127 |
val sube2subte = map TermC.str2term;
|
wneuper@59301
|
128 |
val subte2subst = map HOLogic.dest_eq;
|
wneuper@59396
|
129 |
val e_ctxt = Proof_Context.init_global @{theory "Isac"};
|
wneuper@59301
|
130 |
|
wneuper@59298
|
131 |
end
|