neuper@37906
|
1 |
(* Handle user-input during the specify- and the solve-phase.
|
neuper@37906
|
2 |
author: Walther Neuper
|
neuper@37906
|
3 |
0603
|
neuper@37906
|
4 |
(c) due to copyright terms
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
use"ME/inform.sml";
|
neuper@37906
|
7 |
use"inform.sml";
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37906
|
10 |
signature INFORM =
|
neuper@37906
|
11 |
sig
|
neuper@37906
|
12 |
|
neuper@37906
|
13 |
type castab
|
neuper@37906
|
14 |
type icalhd
|
neuper@37906
|
15 |
|
neuper@37906
|
16 |
(* type iitem *)
|
neuper@37906
|
17 |
datatype
|
neuper@37906
|
18 |
iitem =
|
neuper@37906
|
19 |
Find of cterm' list
|
neuper@37906
|
20 |
| Given of cterm' list
|
neuper@37906
|
21 |
| Relate of cterm' list
|
neuper@37906
|
22 |
type imodel
|
neuper@37906
|
23 |
val imodel2fstr : iitem list -> (string * cterm') list
|
neuper@37906
|
24 |
|
neuper@37906
|
25 |
|
neuper@37931
|
26 |
val Isac : 'a -> theory
|
neuper@37906
|
27 |
val appl_add' :
|
neuper@37906
|
28 |
theory' ->
|
neuper@37906
|
29 |
SpecifyTools.ori list ->
|
neuper@37906
|
30 |
SpecifyTools.itm list ->
|
neuper@37906
|
31 |
('a * (Term.term * Term.term)) list ->
|
neuper@37906
|
32 |
string * cterm' -> SpecifyTools.itm
|
neuper@37906
|
33 |
(* val appl_adds :
|
neuper@37906
|
34 |
theory' ->
|
neuper@37906
|
35 |
SpecifyTools.ori list ->
|
neuper@37906
|
36 |
SpecifyTools.itm list ->
|
neuper@37906
|
37 |
(string * (Term.term * Term.term)) list ->
|
neuper@37906
|
38 |
(string * string) list -> SpecifyTools.itm list *)
|
neuper@37906
|
39 |
(* val cas_input : string -> ptree * ocalhd *)
|
neuper@37906
|
40 |
(* val cas_input_ :
|
neuper@37906
|
41 |
spec ->
|
neuper@37906
|
42 |
(Term.term * Term.term list) list ->
|
neuper@37906
|
43 |
pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
|
neuper@37906
|
44 |
(bool * Term.term) list *)
|
neuper@37906
|
45 |
val castab : castab ref
|
neuper@37906
|
46 |
val compare_step :
|
neuper@37906
|
47 |
calcstate' -> Term.term -> string * calcstate'
|
neuper@37906
|
48 |
(* val concat_deriv :
|
neuper@37906
|
49 |
'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)
|
neuper@37906
|
50 |
->
|
neuper@37906
|
51 |
rls ->
|
neuper@37906
|
52 |
rule list ->
|
neuper@37906
|
53 |
Term.term ->
|
neuper@37906
|
54 |
Term.term ->
|
neuper@37906
|
55 |
bool * (Term.term * rule * (Term.term * Term.term list)) list *)
|
neuper@37906
|
56 |
val dropwhile' : (* systest/auto-inform.sml *)
|
neuper@37906
|
57 |
('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
|
neuper@37906
|
58 |
(* val dtss2itm_ :
|
neuper@37906
|
59 |
pbt_ list ->
|
neuper@37906
|
60 |
Term.term * Term.term list ->
|
neuper@37906
|
61 |
int list * bool * string * SpecifyTools.itm_ *)
|
neuper@37906
|
62 |
(* val e_icalhd : icalhd *)
|
neuper@37906
|
63 |
val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool
|
neuper@37906
|
64 |
val equal : ''a -> ''a -> bool
|
neuper@37906
|
65 |
(* val filter_dsc :
|
neuper@37906
|
66 |
SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *)
|
neuper@37906
|
67 |
(* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
|
neuper@37906
|
68 |
(* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
|
neuper@37906
|
69 |
(* val fstr2itm_ :
|
neuper@37931
|
70 |
theory ->
|
neuper@37906
|
71 |
(''a * (Term.term * Term.term)) list ->
|
neuper@37906
|
72 |
''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
|
neuper@37906
|
73 |
val inform :
|
neuper@37906
|
74 |
calcstate' -> cterm' -> string * calcstate'
|
neuper@37906
|
75 |
val input_icalhd : ptree -> icalhd -> ptree * ocalhd
|
neuper@37906
|
76 |
(* val is_Par : SpecifyTools.itm -> bool *)
|
neuper@37906
|
77 |
(* val is_casinput : cterm' -> fmz -> bool *)
|
neuper@37906
|
78 |
(* val is_e_ts : Term.term list -> bool *)
|
neuper@37906
|
79 |
(* val itms2fstr : SpecifyTools.itm -> string * string *)
|
neuper@37906
|
80 |
(* val mk_tacis :
|
neuper@37906
|
81 |
rew_ord' * 'a ->
|
neuper@37906
|
82 |
rls ->
|
neuper@37906
|
83 |
Term.term * rule * (Term.term * Term.term list) ->
|
neuper@37906
|
84 |
tac * tac_ * (pos' * istate) *)
|
neuper@37906
|
85 |
val oris2itms :
|
neuper@37906
|
86 |
'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
|
neuper@37906
|
87 |
(* val par2fstr : SpecifyTools.itm -> string * cterm' *)
|
neuper@37931
|
88 |
(* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
|
neuper@37906
|
89 |
val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
|
neuper@37906
|
90 |
(* val unknown_expl :
|
neuper@37906
|
91 |
theory' ->
|
neuper@37906
|
92 |
(string * (Term.term * Term.term)) list ->
|
neuper@37906
|
93 |
(string * string) list -> SpecifyTools.itm list *)
|
neuper@37906
|
94 |
end
|
neuper@37906
|
95 |
|
neuper@37906
|
96 |
|
neuper@37906
|
97 |
|
neuper@37906
|
98 |
|
neuper@37906
|
99 |
|
neuper@37906
|
100 |
|
neuper@37906
|
101 |
(***. handle an input calc-head .***)
|
neuper@37906
|
102 |
|
neuper@37906
|
103 |
(*------------------------------------------------------------------(**)
|
neuper@37906
|
104 |
structure inform :INFORM =
|
neuper@37906
|
105 |
struct
|
neuper@37906
|
106 |
(**)------------------------------------------------------------------*)
|
neuper@37906
|
107 |
|
neuper@37906
|
108 |
datatype iitem =
|
neuper@37906
|
109 |
Given of cterm' list
|
neuper@37906
|
110 |
(*Where is never input*)
|
neuper@37906
|
111 |
| Find of cterm' list
|
neuper@37906
|
112 |
| Relate of cterm' list;
|
neuper@37906
|
113 |
|
neuper@37906
|
114 |
type imodel = iitem list;
|
neuper@37906
|
115 |
|
neuper@37906
|
116 |
(*calc-head as input*)
|
neuper@37906
|
117 |
type icalhd =
|
neuper@37906
|
118 |
pos' * (*the position of the calc-head in the calc-tree
|
neuper@37906
|
119 |
pos' as (p,p_) where p_ is neglected due to pos_ below*)
|
neuper@37906
|
120 |
cterm' * (*the headline*)
|
neuper@37906
|
121 |
imodel * (*the model (without Find) of the calc-head*)
|
neuper@37906
|
122 |
pos_ * (*model belongs to Pbl or Met*)
|
neuper@37906
|
123 |
spec; (*specification: domID, pblID, metID*)
|
neuper@37906
|
124 |
val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd;
|
neuper@37906
|
125 |
|
neuper@37906
|
126 |
fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) =
|
neuper@37906
|
127 |
hdf <> "" andalso fmz_ = [] andalso spec = e_spec;
|
neuper@37906
|
128 |
|
neuper@37906
|
129 |
(*.handle an input as into an algebra system.*)
|
neuper@37906
|
130 |
fun dtss2itm_ ppc (d, ts) =
|
neuper@37906
|
131 |
let val (f, (d, id)) = the (find_first ((curry op= d) o
|
neuper@37906
|
132 |
(#1: (term * term) -> term) o
|
neuper@37906
|
133 |
(#2: pbt_ -> (term * term))) ppc)
|
neuper@37906
|
134 |
in ([1], true, f, Cor ((d, ts), (id, ts))) end;
|
neuper@37906
|
135 |
|
neuper@37906
|
136 |
fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
|
neuper@37906
|
137 |
|
neuper@37906
|
138 |
|
neuper@37906
|
139 |
|
neuper@37906
|
140 |
(*.association list with cas-commands, for generating a complete calc-head.*)
|
neuper@37906
|
141 |
type castab =
|
neuper@37906
|
142 |
(term * (*cas-command, eg. 'solve'*)
|
neuper@37906
|
143 |
(spec * (*theory, problem, method*)
|
neuper@37906
|
144 |
|
neuper@37906
|
145 |
(*the function generating a kind of formalization*)
|
neuper@37906
|
146 |
(term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)
|
neuper@37906
|
147 |
(term * (*description of an element*)
|
neuper@37906
|
148 |
term list) (*value of the element (always put into a list)*)
|
neuper@37906
|
149 |
list))) (*of elements in the formalization*)
|
neuper@37906
|
150 |
list; (*of cas-entries in the association list*)
|
neuper@37906
|
151 |
|
neuper@37906
|
152 |
val castab = ref ([]: castab);
|
neuper@37906
|
153 |
|
neuper@37906
|
154 |
|
neuper@37906
|
155 |
(*..*)
|
neuper@37906
|
156 |
(* val (dI,pI,mI) = spec;
|
neuper@37906
|
157 |
*)
|
neuper@37906
|
158 |
(*fun cas_input_ ((dI,pI,mI): spec) dtss =
|
neuper@37906
|
159 |
let val thy = assoc_thy dI
|
neuper@37906
|
160 |
val {ppc,...} = get_pbt pI
|
neuper@37906
|
161 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
neuper@37906
|
162 |
val its = add_id its_
|
neuper@37906
|
163 |
val pits = map flattup2 its
|
neuper@37906
|
164 |
val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
|
neuper@37926
|
165 |
else let val SOME (pI,_) = refine_pbl thy pI pits
|
neuper@37906
|
166 |
in (pI, (hd o #met o get_pbt) pI) end
|
neuper@37906
|
167 |
val {ppc,pre,prls,...} = get_met mI
|
neuper@37906
|
168 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
neuper@37906
|
169 |
val its = add_id its_
|
neuper@37906
|
170 |
val mits = map flattup2 its
|
neuper@37906
|
171 |
val pre = check_preconds thy prls pre mits
|
neuper@37906
|
172 |
in (pI, pits: itm list, mI, mits: itm list, pre) end;*)
|
neuper@37906
|
173 |
|
neuper@37906
|
174 |
(* val (dI,pI,mI) = spec;
|
neuper@37906
|
175 |
*)
|
neuper@37906
|
176 |
fun cas_input_ ((dI,pI,mI): spec) dtss =
|
neuper@37906
|
177 |
let val thy = assoc_thy dI
|
neuper@37906
|
178 |
val {ppc,...} = get_pbt pI
|
neuper@37906
|
179 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
neuper@37906
|
180 |
val its = add_id its_
|
neuper@37906
|
181 |
val pits = map flattup2 its
|
neuper@37906
|
182 |
val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
|
neuper@37906
|
183 |
else case refine_pbl thy pI pits of
|
neuper@37926
|
184 |
SOME (pI,_) => (pI, (hd o #met o get_pbt) pI)
|
neuper@37926
|
185 |
| NONE => (pI, (hd o #met o get_pbt) pI)
|
neuper@37906
|
186 |
val {ppc,pre,prls,...} = get_met mI
|
neuper@37906
|
187 |
val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
|
neuper@37906
|
188 |
val its = add_id its_
|
neuper@37906
|
189 |
val mits = map flattup2 its
|
neuper@37906
|
190 |
val pre = check_preconds thy prls pre mits
|
neuper@37906
|
191 |
in (pI, pits: itm list, mI, mits: itm list, pre) end;
|
neuper@37906
|
192 |
|
neuper@37906
|
193 |
|
neuper@37906
|
194 |
(*.check if the input term is a CAScmd and return a ptree with
|
neuper@37906
|
195 |
a _complete_ calchead.*)
|
neuper@37906
|
196 |
(* val hdt = ifo;
|
neuper@37906
|
197 |
*)
|
neuper@37906
|
198 |
fun cas_input hdt =
|
neuper@37906
|
199 |
let val (h,argl) = strip_comb hdt
|
neuper@37906
|
200 |
in case assoc (!castab, h) of
|
neuper@37926
|
201 |
NONE => NONE
|
neuper@37906
|
202 |
(*let val (pt,_) =
|
neuper@37906
|
203 |
cappend_problem e_ptree [] e_istate
|
neuper@37906
|
204 |
([], e_spec) ([], e_spec, e_term)
|
neuper@37906
|
205 |
in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),
|
neuper@37906
|
206 |
[], [], e_spec)) end*)
|
neuper@37926
|
207 |
| SOME (spec as (dI,_,_), argl2dtss) =>
|
neuper@37926
|
208 |
(* val SOME (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h);
|
neuper@37906
|
209 |
*)
|
neuper@37906
|
210 |
let val dtss = argl2dtss argl
|
neuper@37906
|
211 |
val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
|
neuper@37906
|
212 |
val spec = (dI, pI, mI)
|
neuper@37906
|
213 |
val (pt,_) =
|
neuper@37906
|
214 |
cappend_problem e_ptree [] e_istate ([], e_spec)
|
neuper@37906
|
215 |
([], e_spec, hdt)
|
neuper@37906
|
216 |
val pt = update_spec pt [] spec
|
neuper@37906
|
217 |
val pt = update_pbl pt [] pits
|
neuper@37906
|
218 |
val pt = update_met pt [] mits
|
neuper@37926
|
219 |
in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
|
neuper@37906
|
220 |
end;
|
neuper@37906
|
221 |
|
neuper@37906
|
222 |
(*lazy evaluation for Isac.thy*)
|
neuper@37906
|
223 |
fun Isac _ = assoc_thy "Isac.thy";
|
neuper@37906
|
224 |
|
neuper@37906
|
225 |
(*re-parse itms with a new thy and prepare for checking with ori list*)
|
neuper@37906
|
226 |
fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
|
neuper@37906
|
227 |
(* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
|
neuper@37906
|
228 |
*)
|
neuper@37939
|
229 |
(let val t = (comp_dts (Isac "delay")) (d,ts);
|
neuper@37934
|
230 |
val s = Syntax.string_of_term (thy2ctxt dI) t;
|
neuper@37906
|
231 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@37906
|
232 |
in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
|
neuper@37906
|
233 |
| parsitm dI (itm as (i,v,b,f, Syn str)) =
|
neuper@37906
|
234 |
(let val t = (term_of o the o (parse dI)) str
|
neuper@37906
|
235 |
in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
|
neuper@37906
|
236 |
| parsitm dI (itm as (i,v,b,f, Typ str)) =
|
neuper@37906
|
237 |
(let val t = (term_of o the o (parse dI)) str
|
neuper@37906
|
238 |
in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
|
neuper@37906
|
239 |
| parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
|
neuper@37939
|
240 |
(let val t = (comp_dts (Isac "delay")) (d,ts);
|
neuper@37934
|
241 |
val s = Syntax.string_of_term (thy2ctxt dI) t;
|
neuper@37906
|
242 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@37906
|
243 |
in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
|
neuper@37906
|
244 |
| parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
|
neuper@37939
|
245 |
(let val t = (comp_dts (Isac"delay" )) (d,ts);
|
neuper@37934
|
246 |
val s = Syntax.string_of_term (thy2ctxt dI) t;
|
neuper@37906
|
247 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@37906
|
248 |
in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
|
neuper@37906
|
249 |
| parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
|
neuper@37906
|
250 |
(let val t = d $ t';
|
neuper@37934
|
251 |
val s = Syntax.string_of_term (thy2ctxt dI) t;
|
neuper@37906
|
252 |
(*this ^ should raise the exn on unability of re-parsing dts*)
|
neuper@37906
|
253 |
in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
|
neuper@37906
|
254 |
| parsitm dI (itm as (i,v,_,f, Par _)) =
|
neuper@37939
|
255 |
raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
|
neuper@37906
|
256 |
"): Par should be internal");
|
neuper@37906
|
257 |
|
neuper@37906
|
258 |
(*separate a list to a pair of elements that do NOT satisfy the predicate,
|
neuper@37906
|
259 |
and of elements that satisfy the predicate, i.e. (false, true)*)
|
neuper@37906
|
260 |
fun filter_sep pred xs =
|
neuper@37906
|
261 |
let fun filt ab [] = ab
|
neuper@37906
|
262 |
| filt (a,b) (x :: xs) = if pred x
|
neuper@37906
|
263 |
then filt (a,b@[x]) xs
|
neuper@37906
|
264 |
else filt (a@[x],b) xs
|
neuper@37906
|
265 |
in filt ([],[]) xs end;
|
neuper@37906
|
266 |
fun is_Par ((_,_,_,_,Par _):itm) = true
|
neuper@37906
|
267 |
| is_Par _ = false;
|
neuper@37906
|
268 |
|
neuper@37906
|
269 |
fun is_e_ts [] = true
|
neuper@37906
|
270 |
| is_e_ts [Const ("List.list.Nil", _)] = true
|
neuper@37906
|
271 |
| is_e_ts _ = false;
|
neuper@37906
|
272 |
|
neuper@37906
|
273 |
(*WN.9.11.03 copied from fun appl_add (in modspec.sml)*)
|
neuper@37906
|
274 |
(* val (sel,ct) = selct;
|
neuper@37906
|
275 |
val (dI, oris, ppc, pbt, (sel, ct))=
|
neuper@37906
|
276 |
(#1 (some_spec ospec spec), oris, []:itm list,
|
neuper@37906
|
277 |
((#ppc o get_pbt) (#2 (some_spec ospec spec))),
|
neuper@37906
|
278 |
hd (imodel2fstr imodel));
|
neuper@37906
|
279 |
*)
|
neuper@37906
|
280 |
fun appl_add' dI oris ppc pbt (sel, ct) =
|
neuper@37906
|
281 |
let
|
neuper@37906
|
282 |
val thy = assoc_thy dI;
|
neuper@37906
|
283 |
in case parse thy ct of
|
neuper@37926
|
284 |
NONE => (0,[],false,sel, Syn ct):itm
|
neuper@37926
|
285 |
| SOME ct => (* val SOME ct = parse thy ct;
|
neuper@37906
|
286 |
*)
|
neuper@37906
|
287 |
(case is_known thy sel oris (term_of ct) of
|
neuper@37906
|
288 |
(* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);
|
neuper@37906
|
289 |
*)
|
neuper@37906
|
290 |
("",ori'(*ts='ct'*), all) =>
|
neuper@37906
|
291 |
(case is_notyet_input thy ppc all ori' pbt of
|
neuper@37906
|
292 |
(* val ("",itm) = is_notyet_input thy ppc all ori' pbt;
|
neuper@37906
|
293 |
*)
|
neuper@37906
|
294 |
("",itm) => itm
|
neuper@37906
|
295 |
(* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
|
neuper@37906
|
296 |
*)
|
neuper@37906
|
297 |
| (msg,_) => raise error ("appl_add': "^msg))
|
neuper@37906
|
298 |
(* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
|
neuper@37906
|
299 |
*)
|
neuper@37906
|
300 |
| (msg,(i,v,_,d,ts),_) =>
|
neuper@37906
|
301 |
if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[])))
|
neuper@37906
|
302 |
else (i,v,false,sel, Sup (d,ts)))
|
neuper@37906
|
303 |
end;
|
neuper@37906
|
304 |
|
neuper@37906
|
305 |
(*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
|
neuper@37906
|
306 |
(* val (f, str) = hd selcts;
|
neuper@37906
|
307 |
*)
|
neuper@37906
|
308 |
fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';
|
neuper@37906
|
309 |
fun fstr2itm_ thy pbt (f, str) =
|
neuper@37906
|
310 |
let val topt = parse thy str
|
neuper@37906
|
311 |
in case topt of
|
neuper@37926
|
312 |
NONE => ([], false, f, Syn str)
|
neuper@37926
|
313 |
| SOME ct =>
|
neuper@37926
|
314 |
(* val SOME ct = parse thy str;
|
neuper@37906
|
315 |
*)
|
neuper@37906
|
316 |
let val (d,ts) = ((split_dts thy) o term_of) ct
|
neuper@37906
|
317 |
val popt = find_first (eq7 (f,d)) pbt
|
neuper@37906
|
318 |
in case popt of
|
neuper@37926
|
319 |
NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
|
neuper@37926
|
320 |
| SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts)))
|
neuper@37906
|
321 |
end
|
neuper@37906
|
322 |
end;
|
neuper@37906
|
323 |
|
neuper@37906
|
324 |
|
neuper@37906
|
325 |
(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
|
neuper@37906
|
326 |
fun unknown_expl dI pbt selcts =
|
neuper@37906
|
327 |
let
|
neuper@37906
|
328 |
val thy = assoc_thy dI
|
neuper@37906
|
329 |
val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
|
neuper@37906
|
330 |
val its = add_id its_
|
neuper@37906
|
331 |
in (map flattup2 its): itm list end;
|
neuper@37906
|
332 |
|
neuper@37906
|
333 |
|
neuper@37906
|
334 |
|
neuper@37906
|
335 |
|
neuper@37906
|
336 |
(*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
|
neuper@37906
|
337 |
appl_add': generate 1 item
|
neuper@37906
|
338 |
appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
|
neuper@37906
|
339 |
appl_add' . is_notyet_input: compare with items in model already input
|
neuper@37906
|
340 |
insert_ppc': insert this 1 item*)
|
neuper@37906
|
341 |
(* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)],
|
neuper@37906
|
342 |
((#ppc o get_pbt) (#2 (some_spec ospec spec))),
|
neuper@37906
|
343 |
(imodel2fstr imodel));
|
neuper@37906
|
344 |
*)
|
neuper@37906
|
345 |
fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
|
neuper@37906
|
346 |
(*already present itms in model are being overwritten*)
|
neuper@37906
|
347 |
| appl_adds dI oris ppc pbt [] = ppc
|
neuper@37906
|
348 |
| appl_adds dI oris ppc pbt (selct::ss) =
|
neuper@37906
|
349 |
(* val selct = (sel, string_of_cterm ct);
|
neuper@37906
|
350 |
*)
|
neuper@37906
|
351 |
let val itm = appl_add' dI oris ppc pbt selct;
|
neuper@37906
|
352 |
in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end;
|
neuper@37906
|
353 |
(* val (dI, oris, ppc, pbt, selct::ss) =
|
neuper@37906
|
354 |
(dI, pors, probl, ppc, map itms2fstr probl);
|
neuper@37906
|
355 |
...vvv
|
neuper@37906
|
356 |
*)
|
neuper@37906
|
357 |
(* val (dI, oris, ppc, pbt, (selct::ss))=
|
neuper@37906
|
358 |
(#1 (some_spec ospec spec), oris, []:itm list,
|
neuper@37906
|
359 |
((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
|
neuper@37906
|
360 |
val iii = appl_adds dI oris ppc pbt (selct::ss);
|
neuper@37924
|
361 |
writeln(itms2str_ thy iii);
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
val itm = appl_add' dI oris ppc pbt selct;
|
neuper@37906
|
364 |
val ppc = insert_ppc' itm ppc;
|
neuper@37906
|
365 |
|
neuper@37906
|
366 |
val _::selct::ss = (selct::ss);
|
neuper@37906
|
367 |
val itm = appl_add' dI oris ppc pbt selct;
|
neuper@37906
|
368 |
val ppc = insert_ppc' itm ppc;
|
neuper@37906
|
369 |
|
neuper@37906
|
370 |
val _::selct::ss = (selct::ss);
|
neuper@37906
|
371 |
val itm = appl_add' dI oris ppc pbt selct;
|
neuper@37906
|
372 |
val ppc = insert_ppc' itm ppc;
|
neuper@37924
|
373 |
writeln(itms2str_ thy ppc);
|
neuper@37906
|
374 |
|
neuper@37906
|
375 |
val _::selct::ss = (selct::ss);
|
neuper@37906
|
376 |
val itm = appl_add' dI oris ppc pbt selct;
|
neuper@37906
|
377 |
val ppc = insert_ppc' itm ppc;
|
neuper@37906
|
378 |
*)
|
neuper@37906
|
379 |
|
neuper@37906
|
380 |
|
neuper@37906
|
381 |
fun oris2itms _ _ ([]:ori list) = ([]:itm list)
|
neuper@37906
|
382 |
| oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) =
|
neuper@37930
|
383 |
if member op = vat v
|
neuper@37906
|
384 |
then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os)
|
neuper@37906
|
385 |
else oris2itms pbt vat os;
|
neuper@37906
|
386 |
|
neuper@37906
|
387 |
fun filter_dsc oris itm =
|
neuper@37906
|
388 |
filter_out ((curry op= ((d_in o #5) (itm:itm))) o
|
neuper@37906
|
389 |
(#4:ori -> term)) oris;
|
neuper@37906
|
390 |
|
neuper@37906
|
391 |
|
neuper@37906
|
392 |
|
neuper@37906
|
393 |
|
neuper@37906
|
394 |
fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
|
neuper@37939
|
395 |
| par2fstr itm = raise error ("par2fstr: called with " ^
|
neuper@37939
|
396 |
itm2str_ (thy2ctxt' "Isac") itm);
|
neuper@37906
|
397 |
fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
|
neuper@37906
|
398 |
| itms2fstr (_,_,_,f, Syn str) = (f, str)
|
neuper@37906
|
399 |
| itms2fstr (_,_,_,f, Typ str) = (f, str)
|
neuper@37906
|
400 |
| itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts))
|
neuper@37906
|
401 |
| itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
|
neuper@37906
|
402 |
| itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
|
neuper@37906
|
403 |
| itms2fstr (itm as (_,_,_,f, Par _)) =
|
neuper@37939
|
404 |
raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
|
neuper@37906
|
405 |
"): Par should be internal");
|
neuper@37906
|
406 |
|
neuper@37906
|
407 |
fun imodel2fstr iitems =
|
neuper@37906
|
408 |
let fun xxx is [] = is
|
neuper@37906
|
409 |
| xxx is ((Given strs)::iis) =
|
neuper@37906
|
410 |
xxx (is @ (map (pair "#Given") strs)) iis
|
neuper@37906
|
411 |
| xxx is ((Find strs)::iis) =
|
neuper@37906
|
412 |
xxx (is @ (map (pair "#Find") strs)) iis
|
neuper@37906
|
413 |
| xxx is ((Relate strs)::iis) =
|
neuper@37906
|
414 |
xxx (is @ (map (pair "#Relate") strs)) iis
|
neuper@37906
|
415 |
in xxx [] iitems end;
|
neuper@37906
|
416 |
|
neuper@37906
|
417 |
(*.input a CAS-command via a whole calchead;
|
neuper@37906
|
418 |
dWN0602 ropped due to change of design in the front-end.*)
|
neuper@37906
|
419 |
(*since previous calc-head _only_ has changed:
|
neuper@37906
|
420 |
EITHER _1_ part of the specification OR some items in the model;
|
neuper@37906
|
421 |
the hdform is left as is except in cas_input .*)
|
neuper@37906
|
422 |
(*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*)
|
neuper@37906
|
423 |
(* val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
|
neuper@37906
|
424 |
(p, "xxx", empty_model, Pbl, e_spec);
|
neuper@37906
|
425 |
val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
|
neuper@37906
|
426 |
(p,"", [Given ["fixedValues [r=Arbfix]"],
|
neuper@37906
|
427 |
Find ["maximum A", "valuesFor [a,b]"],
|
neuper@37906
|
428 |
Relate ["relations [A=a*b, a/2=r*sin alpha, \
|
neuper@37906
|
429 |
\b/2=r*cos alpha]"]], Pbl, e_spec);
|
neuper@37906
|
430 |
val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
|
neuper@37906
|
431 |
(([],Pbl), "not used here",
|
neuper@37906
|
432 |
[Given ["fixedValues [r=Arbfix]"],
|
neuper@37906
|
433 |
Find ["maximum A", "valuesFor [a,b]"(*new input*)],
|
neuper@37906
|
434 |
Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
|
neuper@37906
|
435 |
("DiffApp.thy", ["e_pblID"], ["e_metID"]));
|
neuper@37906
|
436 |
val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;
|
neuper@37906
|
437 |
*)
|
neuper@37906
|
438 |
fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
|
neuper@37906
|
439 |
let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
|
neuper@37906
|
440 |
spec = sspec as (sdI,spI,smI), probl, meth,...} =
|
neuper@37906
|
441 |
get_obj I pt p;
|
neuper@37906
|
442 |
in if is_casinput hdf fmz then the (cas_input (str2term hdf))
|
neuper@37906
|
443 |
else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
|
neuper@37906
|
444 |
let val (pos_, pits, mits) =
|
neuper@37906
|
445 |
if dI <> sdI
|
neuper@37906
|
446 |
then let val its = map (parsitm (assoc_thy dI)) probl;
|
neuper@37906
|
447 |
val (its, trms) = filter_sep is_Par its;
|
neuper@37906
|
448 |
val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
|
neuper@37906
|
449 |
in (Pbl, appl_adds dI oris its pbt
|
neuper@37906
|
450 |
(map par2fstr trms), meth) end else
|
neuper@37906
|
451 |
if pI <> spI
|
neuper@37906
|
452 |
then if pI = snd3 ospec then (Pbl, probl, meth) else
|
neuper@37906
|
453 |
let val pbt = (#ppc o get_pbt) pI
|
neuper@37906
|
454 |
val dI' = #1 (some_spec ospec spec)
|
neuper@37906
|
455 |
val oris = if pI = #2 ospec then oris
|
neuper@37906
|
456 |
else prep_ori fmz_(assoc_thy"Isac.thy") pbt;
|
neuper@37906
|
457 |
in (Pbl, appl_adds dI' oris probl pbt
|
neuper@37906
|
458 |
(map itms2fstr probl), meth) end else
|
neuper@37906
|
459 |
if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
|
neuper@37906
|
460 |
then let val met = (#ppc o get_met) mI
|
neuper@37906
|
461 |
val mits = complete_metitms oris probl meth met
|
neuper@37906
|
462 |
in if foldl and_ (true, map #3 mits)
|
neuper@37906
|
463 |
then (Pbl, probl, mits) else (Met, probl, mits)
|
neuper@37906
|
464 |
end else
|
neuper@37906
|
465 |
(Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
|
neuper@37906
|
466 |
((#ppc o get_pbt) (#2 (some_spec ospec spec)))
|
neuper@37906
|
467 |
(imodel2fstr imodel), meth);
|
neuper@37906
|
468 |
val pt = update_spec pt p spec;
|
neuper@37906
|
469 |
in if pos_ = Pbl
|
neuper@37906
|
470 |
then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
|
neuper@37906
|
471 |
val pre =check_preconds(assoc_thy"Isac.thy")prls where_ pits
|
neuper@37906
|
472 |
in (update_pbl pt p pits,
|
neuper@37906
|
473 |
(ocalhd_complete pits pre spec,
|
neuper@37906
|
474 |
Pbl, hdf', pits, pre, spec):ocalhd) end
|
neuper@37906
|
475 |
else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
|
neuper@37906
|
476 |
val pre = check_preconds (assoc_thy"Isac.thy") prls pre mits
|
neuper@37906
|
477 |
in (update_met pt p mits,
|
neuper@37906
|
478 |
(ocalhd_complete mits pre spec,
|
neuper@37906
|
479 |
Met, hdf', mits, pre, spec):ocalhd) end
|
neuper@37906
|
480 |
end end
|
neuper@37906
|
481 |
| input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
|
neuper@37906
|
482 |
raise error "input_icalhd Met not impl.";
|
neuper@37906
|
483 |
|
neuper@37906
|
484 |
|
neuper@37906
|
485 |
(***. handle an input formula .***)
|
neuper@37906
|
486 |
(*
|
neuper@37906
|
487 |
Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
|
neuper@37906
|
488 |
Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
|
neuper@37906
|
489 |
wenn Abteilungen nur auf gleichem Level gesucht werden ?
|
neuper@37906
|
490 |
WN.040216
|
neuper@37906
|
491 |
|
neuper@37906
|
492 |
Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
|
neuper@37906
|
493 |
|
neuper@37906
|
494 |
------------------------------------------------------------------------------
|
neuper@37906
|
495 |
"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
|
neuper@37906
|
496 |
------------------------------------------------------------------------------
|
neuper@37906
|
497 |
1. "5 * x / (x - 2) - x / (x + 2) = 4"
|
neuper@37906
|
498 |
...
|
neuper@37906
|
499 |
4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
|
neuper@37906
|
500 |
...
|
neuper@37906
|
501 |
4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
|
neuper@37906
|
502 |
...
|
neuper@37906
|
503 |
4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
|
neuper@37906
|
504 |
...
|
neuper@37906
|
505 |
"[x = -4 / 3]"
|
neuper@37906
|
506 |
------------------------------------------------------------------------------
|
neuper@37906
|
507 |
(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
|
neuper@37906
|
508 |
|
neuper@37906
|
509 |
(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
|
neuper@37906
|
510 |
------------------------------------------------------------------------------
|
neuper@37906
|
511 |
|
neuper@37906
|
512 |
|
neuper@37906
|
513 |
------------------------------------------------------------------------------
|
neuper@37906
|
514 |
"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
|
neuper@37906
|
515 |
------------------------------------------------------------------------------
|
neuper@37906
|
516 |
1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
|
neuper@37906
|
517 |
...
|
neuper@37906
|
518 |
4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
|
neuper@37906
|
519 |
Subproblem["normalize", "polynomial", "univariate"..
|
neuper@37906
|
520 |
...
|
neuper@37906
|
521 |
4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
|
neuper@37906
|
522 |
...
|
neuper@37906
|
523 |
4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
|
neuper@37906
|
524 |
4.4.5. "[x = 0, x = 6 / 5]"
|
neuper@37906
|
525 |
...
|
neuper@37906
|
526 |
5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
|
neuper@37906
|
527 |
"[x = 6 / 5]"
|
neuper@37906
|
528 |
------------------------------------------------------------------------------
|
neuper@37906
|
529 |
(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
|
neuper@37906
|
530 |
|
neuper@37906
|
531 |
(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
|
neuper@37906
|
532 |
------------------------------------------------------------------------------
|
neuper@37906
|
533 |
|
neuper@37906
|
534 |
|
neuper@37906
|
535 |
------------------------------------------------------------------------------
|
neuper@37906
|
536 |
"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
|
neuper@37906
|
537 |
------------------------------------------------------------------------------
|
neuper@37906
|
538 |
1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
|
neuper@37906
|
539 |
...
|
neuper@37906
|
540 |
6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
|
neuper@37906
|
541 |
Subproblem["sq", "root", "univariate", "equation"]
|
neuper@37906
|
542 |
...
|
neuper@37906
|
543 |
6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
|
neuper@37906
|
544 |
Subproblem["normalize", "polynomial", "univariate", "equation"]
|
neuper@37906
|
545 |
...
|
neuper@37906
|
546 |
6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
|
neuper@37906
|
547 |
... Or_to_List
|
neuper@37906
|
548 |
6.6.3.2 "UniversalList"
|
neuper@37906
|
549 |
------------------------------------------------------------------------------
|
neuper@37906
|
550 |
(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
|
neuper@37906
|
551 |
|
neuper@37906
|
552 |
(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
|
neuper@37906
|
553 |
------------------------------------------------------------------------------
|
neuper@37906
|
554 |
*)
|
neuper@37906
|
555 |
(*sh. comments auf 498*)
|
neuper@37906
|
556 |
|
neuper@37906
|
557 |
fun equal a b = a=b;
|
neuper@37906
|
558 |
|
neuper@37906
|
559 |
(*the lists contain eq-al elem-pairs at the beginning;
|
neuper@37906
|
560 |
return first list reverted (again) - ie. in order as required subsequently*)
|
neuper@37906
|
561 |
fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
|
neuper@37906
|
562 |
if equal f1 i1 then
|
neuper@37906
|
563 |
if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
|
neuper@37906
|
564 |
else (rev (f1::f2::fs), i1::i2::is)
|
neuper@37906
|
565 |
else raise error "dropwhile': did not start with equal elements"
|
neuper@37906
|
566 |
| dropwhile' equal (f::fs) [i] =
|
neuper@37906
|
567 |
if equal f i then (rev (f::fs), [i])
|
neuper@37906
|
568 |
else raise error "dropwhile': did not start with equal elements"
|
neuper@37906
|
569 |
| dropwhile' equal [f] (i::is) =
|
neuper@37906
|
570 |
if equal f i then ([f], i::is)
|
neuper@37906
|
571 |
else raise error "dropwhile': did not start with equal elements";
|
neuper@37906
|
572 |
(*
|
neuper@37906
|
573 |
fun equal a b = a=b;
|
neuper@37906
|
574 |
val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
|
neuper@37906
|
575 |
val r_foder = rev foder; val r_ifoder = rev ifoder;
|
neuper@37906
|
576 |
dropwhile' equal r_foder r_ifoder;
|
neuper@37906
|
577 |
> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
|
neuper@37906
|
578 |
|
neuper@37906
|
579 |
val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
|
neuper@37906
|
580 |
val r_foder = rev foder; val r_ifoder = rev ifoder;
|
neuper@37906
|
581 |
dropwhile' equal r_foder r_ifoder;
|
neuper@37906
|
582 |
> val it = ([3], [3, 12, 11]) : int list * int list
|
neuper@37906
|
583 |
|
neuper@37906
|
584 |
val foder = [5]; val ifoder = [11,12,3,4,5];
|
neuper@37906
|
585 |
val r_foder = rev foder; val r_ifoder = rev ifoder;
|
neuper@37906
|
586 |
dropwhile' equal r_foder r_ifoder;
|
neuper@37906
|
587 |
> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
|
neuper@37906
|
588 |
|
neuper@37906
|
589 |
val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
|
neuper@37906
|
590 |
val r_foder = rev foder; val r_ifoder = rev ifoder;
|
neuper@37906
|
591 |
dropwhile' equal r_foder r_ifoder;
|
neuper@37906
|
592 |
> *** dropwhile': did not start with equal elements*)
|
neuper@37906
|
593 |
|
neuper@37906
|
594 |
(*040214: version for concat_deriv*)
|
neuper@37906
|
595 |
fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
|
neuper@37906
|
596 |
|
neuper@37906
|
597 |
fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
|
neuper@37906
|
598 |
(Rewrite (rule2thm' r),
|
neuper@37906
|
599 |
Rewrite' ("Isac.thy", fst ro, erls, false,
|
neuper@37906
|
600 |
rule2thm' r, t, (t', a)),
|
neuper@37906
|
601 |
(e_pos'(*to be updated before generate tacis!!!*), Uistate))
|
neuper@37906
|
602 |
| mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
|
neuper@37906
|
603 |
(Rewrite_Set (rule2rls' r),
|
neuper@37906
|
604 |
Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)),
|
neuper@37906
|
605 |
(e_pos'(*to be updated before generate tacis!!!*), Uistate));
|
neuper@37906
|
606 |
|
neuper@37906
|
607 |
(*fo = ifo excluded already in inform*)
|
neuper@37906
|
608 |
fun concat_deriv rew_ord erls rules fo ifo =
|
neuper@37906
|
609 |
let fun derivat ([]:(term * rule * (term * term list)) list) = e_term
|
neuper@37906
|
610 |
| derivat dt = (#1 o #3 o last_elem) dt
|
neuper@37906
|
611 |
fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
|
neuper@37926
|
612 |
val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
|
neuper@37926
|
613 |
val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
|
neuper@37906
|
614 |
in case (fod, ifod) of
|
neuper@37906
|
615 |
([], []) => if fo = ifo then (true, [])
|
neuper@37906
|
616 |
else (false, [])
|
neuper@37906
|
617 |
| (fod, []) => if derivat fod = ifo
|
neuper@37906
|
618 |
then (true, fod) (*ifo is normal form*)
|
neuper@37906
|
619 |
else (false, [])
|
neuper@37906
|
620 |
| ([], ifod) => if fo = derivat ifod
|
neuper@37906
|
621 |
then (true, ((map rev_deriv') o rev) ifod)
|
neuper@37906
|
622 |
else (false, [])
|
neuper@37906
|
623 |
| (fod, ifod) =>
|
neuper@37906
|
624 |
if derivat fod = derivat ifod (*common normal form found*)
|
neuper@37906
|
625 |
then let val (fod', rifod') =
|
neuper@37906
|
626 |
dropwhile' equal (rev fod) (rev ifod)
|
neuper@37906
|
627 |
in (true, fod' @ (map rev_deriv' rifod')) end
|
neuper@37906
|
628 |
else (false, [])
|
neuper@37906
|
629 |
end;
|
neuper@37906
|
630 |
(*
|
neuper@37906
|
631 |
val ({rew_ord, erls, rules,...}, fo, ifo) =
|
neuper@37906
|
632 |
(rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
|
neuper@37906
|
633 |
(writeln o trtas2str) fod';
|
neuper@37906
|
634 |
> ["
|
neuper@37906
|
635 |
(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
|
neuper@37906
|
636 |
(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
|
neuper@37906
|
637 |
(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
|
neuper@37906
|
638 |
(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
|
neuper@37906
|
639 |
val it = () : unit
|
neuper@37906
|
640 |
(writeln o trtas2str) (map rev_deriv' rifod');
|
neuper@37906
|
641 |
> ["
|
neuper@37906
|
642 |
(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
|
neuper@37906
|
643 |
(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
|
neuper@37906
|
644 |
(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
|
neuper@37906
|
645 |
val it = () : unit
|
neuper@37906
|
646 |
*)
|
neuper@37906
|
647 |
|
neuper@37906
|
648 |
|
neuper@37906
|
649 |
(*.compare inform with ctree.form at current pos by nrls;
|
neuper@37906
|
650 |
if found, embed the derivation generated during comparison
|
neuper@37906
|
651 |
if not, let the mat-engine compute the next ctree.form.*)
|
neuper@37906
|
652 |
(*structure copied from complete_solve
|
neuper@37906
|
653 |
CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
|
neuper@37906
|
654 |
all_modspec etc. has to be inserted at Subproblem'*)
|
neuper@37906
|
655 |
(* val (tacis, c, ptp as (pt, pos as (p,p_))) = (tacis, ptp);
|
neuper@37906
|
656 |
val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
|
neuper@37906
|
657 |
|
neuper@37906
|
658 |
val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos));
|
neuper@37906
|
659 |
-----rec.call:
|
neuper@37906
|
660 |
val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
|
neuper@37906
|
661 |
*)
|
neuper@37906
|
662 |
fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
|
neuper@37906
|
663 |
let val fo = case p_ of Frm => get_obj g_form pt p
|
neuper@37906
|
664 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@37906
|
665 |
| _ => e_term (*on PblObj is fo <> ifo*);
|
neuper@37906
|
666 |
val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
|
neuper@37906
|
667 |
val {rew_ord, erls, rules,...} = rep_rls nrls
|
neuper@37906
|
668 |
val (found, der) = concat_deriv rew_ord erls rules fo ifo;
|
neuper@37906
|
669 |
in if found
|
neuper@37906
|
670 |
then let val tacis' = map (mk_tacis rew_ord erls) der;
|
neuper@37906
|
671 |
val (c', ptp) = embed_deriv tacis' ptp;
|
neuper@37906
|
672 |
in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
|
neuper@37906
|
673 |
else
|
neuper@37906
|
674 |
if pos = ([], Res)
|
neuper@37906
|
675 |
then ("no derivation found", (tacis, c, ptp): calcstate')
|
neuper@37906
|
676 |
else let val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
|
neuper@37906
|
677 |
val cs' as (tacis, c'', ptp) =
|
neuper@37906
|
678 |
case tacis of
|
neuper@37906
|
679 |
((Subproblem _, _, _)::_) =>
|
neuper@37906
|
680 |
let val ptp as (pt, (p,_)) = all_modspec ptp
|
neuper@37906
|
681 |
val mI = get_obj g_metID pt p
|
neuper@37926
|
682 |
in nxt_solv (Apply_Method' (mI, NONE, e_istate))
|
neuper@37906
|
683 |
e_istate ptp end
|
neuper@37906
|
684 |
| _ => cs';
|
neuper@37906
|
685 |
in compare_step (tacis, c @ c' @ c'', ptp) ifo end
|
neuper@37906
|
686 |
end;
|
neuper@37906
|
687 |
(* writeln (trtas2str der);
|
neuper@37906
|
688 |
*)
|
neuper@37906
|
689 |
|
neuper@37906
|
690 |
(*.handle a user-input formula, which may be a CAS-command, too.
|
neuper@37906
|
691 |
CAS-command:
|
neuper@37906
|
692 |
create a calchead, and do 1 step
|
neuper@37906
|
693 |
TOOODO.WN0602 works only for the root-problem !!!
|
neuper@37906
|
694 |
formula, which is no CAS-command:
|
neuper@37906
|
695 |
compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
|
neuper@37906
|
696 |
collect all the tacs applied by the way.*)
|
neuper@37906
|
697 |
(*structure copied from autocalc*)
|
neuper@37906
|
698 |
(* val (cs as (_, _, (pt, pos as (p, p_))): calcstate') = cs';
|
neuper@37906
|
699 |
val ifo = str2term ifo;
|
neuper@37906
|
700 |
|
neuper@37906
|
701 |
val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
|
neuper@37906
|
702 |
(cs', encode ifo);
|
neuper@37906
|
703 |
val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo));
|
neuper@37906
|
704 |
val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
|
neuper@37906
|
705 |
(([],[],(pt,p)), (encode ifo));
|
neuper@37906
|
706 |
*)
|
neuper@37906
|
707 |
fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
|
neuper@37906
|
708 |
case parse (assoc_thy "Isac.thy") istr of
|
neuper@37926
|
709 |
(* val SOME ifo = parse (assoc_thy "Isac.thy") istr;
|
neuper@37906
|
710 |
*)
|
neuper@37926
|
711 |
SOME ifo =>
|
neuper@37906
|
712 |
let val ifo = term_of ifo
|
neuper@37906
|
713 |
val fo = case p_ of Frm => get_obj g_form pt p
|
neuper@37906
|
714 |
| Res => (fst o (get_obj g_result pt)) p
|
neuper@37906
|
715 |
| _ => #3 (get_obj g_origin pt p)
|
neuper@37906
|
716 |
in if fo = ifo
|
neuper@37906
|
717 |
then ("same-formula", cs)
|
neuper@37906
|
718 |
(*thus ctree not cut with replaceFormula!*)
|
neuper@37906
|
719 |
else case cas_input ifo of
|
neuper@37926
|
720 |
(* val SOME (pt, _) = cas_input ifo;
|
neuper@37906
|
721 |
*)
|
neuper@37926
|
722 |
SOME (pt, _) => ("ok",([],[],(pt, (p, Met))))
|
neuper@37926
|
723 |
| NONE =>
|
neuper@37906
|
724 |
compare_step ([],[],(pt,
|
neuper@37906
|
725 |
(*last step re-calc in compare_step TODO*)
|
neuper@37906
|
726 |
lev_back pos)) ifo
|
neuper@37906
|
727 |
end
|
neuper@37926
|
728 |
| NONE => ("syntax error in '"^istr^"'", e_calcstate');
|
neuper@37906
|
729 |
|
neuper@37906
|
730 |
|
neuper@37906
|
731 |
(*------------------------------------------------------------------(**)
|
neuper@37906
|
732 |
end
|
neuper@37906
|
733 |
open inform;
|
neuper@37906
|
734 |
(**)------------------------------------------------------------------*)
|