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