1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Interpret/inform.sml Wed Aug 25 16:20:07 2010 +0200
1.3 @@ -0,0 +1,734 @@
1.4 +(* Handle user-input during the specify- and the solve-phase.
1.5 + author: Walther Neuper
1.6 + 0603
1.7 + (c) due to copyright terms
1.8 +
1.9 +use"ME/inform.sml";
1.10 +use"inform.sml";
1.11 +*)
1.12 +
1.13 +signature INFORM =
1.14 + sig
1.15 +
1.16 + type castab
1.17 + type icalhd
1.18 +
1.19 + (* type iitem *)
1.20 + datatype
1.21 + iitem =
1.22 + Find of cterm' list
1.23 + | Given of cterm' list
1.24 + | Relate of cterm' list
1.25 + type imodel
1.26 + val imodel2fstr : iitem list -> (string * cterm') list
1.27 +
1.28 +
1.29 + val Isac : 'a -> theory
1.30 + val appl_add' :
1.31 + theory' ->
1.32 + SpecifyTools.ori list ->
1.33 + SpecifyTools.itm list ->
1.34 + ('a * (Term.term * Term.term)) list ->
1.35 + string * cterm' -> SpecifyTools.itm
1.36 + (* val appl_adds :
1.37 + theory' ->
1.38 + SpecifyTools.ori list ->
1.39 + SpecifyTools.itm list ->
1.40 + (string * (Term.term * Term.term)) list ->
1.41 + (string * string) list -> SpecifyTools.itm list *)
1.42 + (* val cas_input : string -> ptree * ocalhd *)
1.43 + (* val cas_input_ :
1.44 + spec ->
1.45 + (Term.term * Term.term list) list ->
1.46 + pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list *
1.47 + (bool * Term.term) list *)
1.48 + val castab : castab ref
1.49 + val compare_step :
1.50 + calcstate' -> Term.term -> string * calcstate'
1.51 + (* val concat_deriv :
1.52 + 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)
1.53 + ->
1.54 + rls ->
1.55 + rule list ->
1.56 + Term.term ->
1.57 + Term.term ->
1.58 + bool * (Term.term * rule * (Term.term * Term.term list)) list *)
1.59 + val dropwhile' : (* systest/auto-inform.sml *)
1.60 + ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
1.61 + (* val dtss2itm_ :
1.62 + pbt_ list ->
1.63 + Term.term * Term.term list ->
1.64 + int list * bool * string * SpecifyTools.itm_ *)
1.65 + (* val e_icalhd : icalhd *)
1.66 + val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool
1.67 + val equal : ''a -> ''a -> bool
1.68 + (* val filter_dsc :
1.69 + SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *)
1.70 + (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *)
1.71 + (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *)
1.72 + (* val fstr2itm_ :
1.73 + theory ->
1.74 + (''a * (Term.term * Term.term)) list ->
1.75 + ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
1.76 + val inform :
1.77 + calcstate' -> cterm' -> string * calcstate'
1.78 + val input_icalhd : ptree -> icalhd -> ptree * ocalhd
1.79 + (* val is_Par : SpecifyTools.itm -> bool *)
1.80 + (* val is_casinput : cterm' -> fmz -> bool *)
1.81 + (* val is_e_ts : Term.term list -> bool *)
1.82 + (* val itms2fstr : SpecifyTools.itm -> string * string *)
1.83 + (* val mk_tacis :
1.84 + rew_ord' * 'a ->
1.85 + rls ->
1.86 + Term.term * rule * (Term.term * Term.term list) ->
1.87 + tac * tac_ * (pos' * istate) *)
1.88 + val oris2itms :
1.89 + 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list
1.90 + (* val par2fstr : SpecifyTools.itm -> string * cterm' *)
1.91 + (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *)
1.92 + val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
1.93 + (* val unknown_expl :
1.94 + theory' ->
1.95 + (string * (Term.term * Term.term)) list ->
1.96 + (string * string) list -> SpecifyTools.itm list *)
1.97 + end
1.98 +
1.99 +
1.100 +
1.101 +
1.102 +
1.103 +
1.104 +(***. handle an input calc-head .***)
1.105 +
1.106 +(*------------------------------------------------------------------(**)
1.107 +structure inform :INFORM =
1.108 +struct
1.109 +(**)------------------------------------------------------------------*)
1.110 +
1.111 +datatype iitem =
1.112 + Given of cterm' list
1.113 +(*Where is never input*)
1.114 +| Find of cterm' list
1.115 +| Relate of cterm' list;
1.116 +
1.117 +type imodel = iitem list;
1.118 +
1.119 +(*calc-head as input*)
1.120 +type icalhd =
1.121 + pos' * (*the position of the calc-head in the calc-tree
1.122 + pos' as (p,p_) where p_ is neglected due to pos_ below*)
1.123 + cterm' * (*the headline*)
1.124 + imodel * (*the model (without Find) of the calc-head*)
1.125 + pos_ * (*model belongs to Pbl or Met*)
1.126 + spec; (*specification: domID, pblID, metID*)
1.127 +val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd;
1.128 +
1.129 +fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) =
1.130 + hdf <> "" andalso fmz_ = [] andalso spec = e_spec;
1.131 +
1.132 +(*.handle an input as into an algebra system.*)
1.133 +fun dtss2itm_ ppc (d, ts) =
1.134 + let val (f, (d, id)) = the (find_first ((curry op= d) o
1.135 + (#1: (term * term) -> term) o
1.136 + (#2: pbt_ -> (term * term))) ppc)
1.137 + in ([1], true, f, Cor ((d, ts), (id, ts))) end;
1.138 +
1.139 +fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
1.140 +
1.141 +
1.142 +
1.143 +(*.association list with cas-commands, for generating a complete calc-head.*)
1.144 +type castab =
1.145 + (term * (*cas-command, eg. 'solve'*)
1.146 + (spec * (*theory, problem, method*)
1.147 +
1.148 + (*the function generating a kind of formalization*)
1.149 + (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*)
1.150 + (term * (*description of an element*)
1.151 + term list) (*value of the element (always put into a list)*)
1.152 + list))) (*of elements in the formalization*)
1.153 + list; (*of cas-entries in the association list*)
1.154 +
1.155 +val castab = ref ([]: castab);
1.156 +
1.157 +
1.158 +(*..*)
1.159 +(* val (dI,pI,mI) = spec;
1.160 + *)
1.161 +(*fun cas_input_ ((dI,pI,mI): spec) dtss =
1.162 + let val thy = assoc_thy dI
1.163 + val {ppc,...} = get_pbt pI
1.164 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.165 + val its = add_id its_
1.166 + val pits = map flattup2 its
1.167 + val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
1.168 + else let val SOME (pI,_) = refine_pbl thy pI pits
1.169 + in (pI, (hd o #met o get_pbt) pI) end
1.170 + val {ppc,pre,prls,...} = get_met mI
1.171 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.172 + val its = add_id its_
1.173 + val mits = map flattup2 its
1.174 + val pre = check_preconds thy prls pre mits
1.175 +in (pI, pits: itm list, mI, mits: itm list, pre) end;*)
1.176 +
1.177 +(* val (dI,pI,mI) = spec;
1.178 + *)
1.179 +fun cas_input_ ((dI,pI,mI): spec) dtss =
1.180 + let val thy = assoc_thy dI
1.181 + val {ppc,...} = get_pbt pI
1.182 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.183 + val its = add_id its_
1.184 + val pits = map flattup2 its
1.185 + val (pI, mI) = if mI <> ["no_met"] then (pI, mI)
1.186 + else case refine_pbl thy pI pits of
1.187 + SOME (pI,_) => (pI, (hd o #met o get_pbt) pI)
1.188 + | NONE => (pI, (hd o #met o get_pbt) pI)
1.189 + val {ppc,pre,prls,...} = get_met mI
1.190 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
1.191 + val its = add_id its_
1.192 + val mits = map flattup2 its
1.193 + val pre = check_preconds thy prls pre mits
1.194 +in (pI, pits: itm list, mI, mits: itm list, pre) end;
1.195 +
1.196 +
1.197 +(*.check if the input term is a CAScmd and return a ptree with
1.198 + a _complete_ calchead.*)
1.199 +(* val hdt = ifo;
1.200 + *)
1.201 +fun cas_input hdt =
1.202 + let val (h,argl) = strip_comb hdt
1.203 + in case assoc (!castab, h) of
1.204 + NONE => NONE
1.205 + (*let val (pt,_) =
1.206 + cappend_problem e_ptree [] e_istate
1.207 + ([], e_spec) ([], e_spec, e_term)
1.208 + in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*),
1.209 + [], [], e_spec)) end*)
1.210 + | SOME (spec as (dI,_,_), argl2dtss) =>
1.211 + (* val SOME (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h);
1.212 + *)
1.213 + let val dtss = argl2dtss argl
1.214 + val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
1.215 + val spec = (dI, pI, mI)
1.216 + val (pt,_) =
1.217 + cappend_problem e_ptree [] e_istate ([], e_spec)
1.218 + ([], e_spec, hdt)
1.219 + val pt = update_spec pt [] spec
1.220 + val pt = update_pbl pt [] pits
1.221 + val pt = update_met pt [] mits
1.222 + in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end
1.223 + end;
1.224 +
1.225 +(*lazy evaluation for Isac.thy*)
1.226 +fun Isac _ = assoc_thy "Isac.thy";
1.227 +
1.228 +(*re-parse itms with a new thy and prepare for checking with ori list*)
1.229 +fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) =
1.230 +(* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
1.231 + *)
1.232 + (let val t = (comp_dts (Isac "delay")) (d,ts);
1.233 + val s = Syntax.string_of_term (thy2ctxt dI) t;
1.234 + (*this ^ should raise the exn on unability of re-parsing dts*)
1.235 + in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.236 + | parsitm dI (itm as (i,v,b,f, Syn str)) =
1.237 + (let val t = (term_of o the o (parse dI)) str
1.238 + in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
1.239 + | parsitm dI (itm as (i,v,b,f, Typ str)) =
1.240 + (let val t = (term_of o the o (parse dI)) str
1.241 + in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
1.242 + | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
1.243 + (let val t = (comp_dts (Isac "delay")) (d,ts);
1.244 + val s = Syntax.string_of_term (thy2ctxt dI) t;
1.245 + (*this ^ should raise the exn on unability of re-parsing dts*)
1.246 + in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.247 + | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
1.248 + (let val t = (comp_dts (Isac"delay" )) (d,ts);
1.249 + val s = Syntax.string_of_term (thy2ctxt dI) t;
1.250 + (*this ^ should raise the exn on unability of re-parsing dts*)
1.251 + in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.252 + | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
1.253 + (let val t = d $ t';
1.254 + val s = Syntax.string_of_term (thy2ctxt dI) t;
1.255 + (*this ^ should raise the exn on unability of re-parsing dts*)
1.256 + in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
1.257 + | parsitm dI (itm as (i,v,_,f, Par _)) =
1.258 + raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
1.259 + "): Par should be internal");
1.260 +
1.261 +(*separate a list to a pair of elements that do NOT satisfy the predicate,
1.262 + and of elements that satisfy the predicate, i.e. (false, true)*)
1.263 +fun filter_sep pred xs =
1.264 + let fun filt ab [] = ab
1.265 + | filt (a,b) (x :: xs) = if pred x
1.266 + then filt (a,b@[x]) xs
1.267 + else filt (a@[x],b) xs
1.268 + in filt ([],[]) xs end;
1.269 +fun is_Par ((_,_,_,_,Par _):itm) = true
1.270 + | is_Par _ = false;
1.271 +
1.272 +fun is_e_ts [] = true
1.273 + | is_e_ts [Const ("List.list.Nil", _)] = true
1.274 + | is_e_ts _ = false;
1.275 +
1.276 +(*WN.9.11.03 copied from fun appl_add (in modspec.sml)*)
1.277 +(* val (sel,ct) = selct;
1.278 + val (dI, oris, ppc, pbt, (sel, ct))=
1.279 + (#1 (some_spec ospec spec), oris, []:itm list,
1.280 + ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
1.281 + hd (imodel2fstr imodel));
1.282 + *)
1.283 +fun appl_add' dI oris ppc pbt (sel, ct) =
1.284 + let
1.285 + val thy = assoc_thy dI;
1.286 + in case parse thy ct of
1.287 + NONE => (0,[],false,sel, Syn ct):itm
1.288 + | SOME ct => (* val SOME ct = parse thy ct;
1.289 + *)
1.290 + (case is_known thy sel oris (term_of ct) of
1.291 + (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct);
1.292 + *)
1.293 + ("",ori'(*ts='ct'*), all) =>
1.294 + (case is_notyet_input thy ppc all ori' pbt of
1.295 + (* val ("",itm) = is_notyet_input thy ppc all ori' pbt;
1.296 + *)
1.297 + ("",itm) => itm
1.298 + (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
1.299 + *)
1.300 + | (msg,_) => raise error ("appl_add': "^msg))
1.301 + (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
1.302 + *)
1.303 + | (msg,(i,v,_,d,ts),_) =>
1.304 + if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[])))
1.305 + else (i,v,false,sel, Sup (d,ts)))
1.306 + end;
1.307 +
1.308 +(*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
1.309 +(* val (f, str) = hd selcts;
1.310 + *)
1.311 +fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d';
1.312 +fun fstr2itm_ thy pbt (f, str) =
1.313 + let val topt = parse thy str
1.314 + in case topt of
1.315 + NONE => ([], false, f, Syn str)
1.316 + | SOME ct =>
1.317 +(* val SOME ct = parse thy str;
1.318 + *)
1.319 + let val (d,ts) = ((split_dts thy) o term_of) ct
1.320 + val popt = find_first (eq7 (f,d)) pbt
1.321 + in case popt of
1.322 + NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
1.323 + | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts)))
1.324 + end
1.325 + end;
1.326 +
1.327 +
1.328 +(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
1.329 +fun unknown_expl dI pbt selcts =
1.330 + let
1.331 + val thy = assoc_thy dI
1.332 + val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
1.333 + val its = add_id its_
1.334 +in (map flattup2 its): itm list end;
1.335 +
1.336 +
1.337 +
1.338 +
1.339 +(*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
1.340 + appl_add': generate 1 item
1.341 + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
1.342 + appl_add' . is_notyet_input: compare with items in model already input
1.343 + insert_ppc': insert this 1 item*)
1.344 +(* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)],
1.345 + ((#ppc o get_pbt) (#2 (some_spec ospec spec))),
1.346 + (imodel2fstr imodel));
1.347 + *)
1.348 +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
1.349 + (*already present itms in model are being overwritten*)
1.350 + | appl_adds dI oris ppc pbt [] = ppc
1.351 + | appl_adds dI oris ppc pbt (selct::ss) =
1.352 + (* val selct = (sel, string_of_cterm ct);
1.353 + *)
1.354 + let val itm = appl_add' dI oris ppc pbt selct;
1.355 + in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end;
1.356 +(* val (dI, oris, ppc, pbt, selct::ss) =
1.357 + (dI, pors, probl, ppc, map itms2fstr probl);
1.358 + ...vvv
1.359 + *)
1.360 +(* val (dI, oris, ppc, pbt, (selct::ss))=
1.361 + (#1 (some_spec ospec spec), oris, []:itm list,
1.362 + ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel));
1.363 + val iii = appl_adds dI oris ppc pbt (selct::ss);
1.364 + writeln(itms2str_ thy iii);
1.365 +
1.366 + val itm = appl_add' dI oris ppc pbt selct;
1.367 + val ppc = insert_ppc' itm ppc;
1.368 +
1.369 + val _::selct::ss = (selct::ss);
1.370 + val itm = appl_add' dI oris ppc pbt selct;
1.371 + val ppc = insert_ppc' itm ppc;
1.372 +
1.373 + val _::selct::ss = (selct::ss);
1.374 + val itm = appl_add' dI oris ppc pbt selct;
1.375 + val ppc = insert_ppc' itm ppc;
1.376 + writeln(itms2str_ thy ppc);
1.377 +
1.378 + val _::selct::ss = (selct::ss);
1.379 + val itm = appl_add' dI oris ppc pbt selct;
1.380 + val ppc = insert_ppc' itm ppc;
1.381 + *)
1.382 +
1.383 +
1.384 +fun oris2itms _ _ ([]:ori list) = ([]:itm list)
1.385 + | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) =
1.386 + if member op = vat v
1.387 + then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os)
1.388 + else oris2itms pbt vat os;
1.389 +
1.390 +fun filter_dsc oris itm =
1.391 + filter_out ((curry op= ((d_in o #5) (itm:itm))) o
1.392 + (#4:ori -> term)) oris;
1.393 +
1.394 +
1.395 +
1.396 +
1.397 +fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
1.398 + | par2fstr itm = raise error ("par2fstr: called with " ^
1.399 + itm2str_ (thy2ctxt' "Isac") itm);
1.400 +fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts))
1.401 + | itms2fstr (_,_,_,f, Syn str) = (f, str)
1.402 + | itms2fstr (_,_,_,f, Typ str) = (f, str)
1.403 + | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts))
1.404 + | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts))
1.405 + | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t))
1.406 + | itms2fstr (itm as (_,_,_,f, Par _)) =
1.407 + raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
1.408 + "): Par should be internal");
1.409 +
1.410 +fun imodel2fstr iitems =
1.411 + let fun xxx is [] = is
1.412 + | xxx is ((Given strs)::iis) =
1.413 + xxx (is @ (map (pair "#Given") strs)) iis
1.414 + | xxx is ((Find strs)::iis) =
1.415 + xxx (is @ (map (pair "#Find") strs)) iis
1.416 + | xxx is ((Relate strs)::iis) =
1.417 + xxx (is @ (map (pair "#Relate") strs)) iis
1.418 + in xxx [] iitems end;
1.419 +
1.420 +(*.input a CAS-command via a whole calchead;
1.421 + dWN0602 ropped due to change of design in the front-end.*)
1.422 +(*since previous calc-head _only_ has changed:
1.423 + EITHER _1_ part of the specification OR some items in the model;
1.424 + the hdform is left as is except in cas_input .*)
1.425 +(*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*)
1.426 +(* val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.427 + (p, "xxx", empty_model, Pbl, e_spec);
1.428 + val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.429 + (p,"", [Given ["fixedValues [r=Arbfix]"],
1.430 + Find ["maximum A", "valuesFor [a,b]"],
1.431 + Relate ["relations [A=a*b, a/2=r*sin alpha, \
1.432 + \b/2=r*cos alpha]"]], Pbl, e_spec);
1.433 + val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
1.434 + (([],Pbl), "not used here",
1.435 + [Given ["fixedValues [r=Arbfix]"],
1.436 + Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1.437 + Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
1.438 + ("DiffApp.thy", ["e_pblID"], ["e_metID"]));
1.439 + val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;
1.440 + *)
1.441 +fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
1.442 + let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
1.443 + spec = sspec as (sdI,spI,smI), probl, meth,...} =
1.444 + get_obj I pt p;
1.445 + in if is_casinput hdf fmz then the (cas_input (str2term hdf))
1.446 + else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
1.447 + let val (pos_, pits, mits) =
1.448 + if dI <> sdI
1.449 + then let val its = map (parsitm (assoc_thy dI)) probl;
1.450 + val (its, trms) = filter_sep is_Par its;
1.451 + val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
1.452 + in (Pbl, appl_adds dI oris its pbt
1.453 + (map par2fstr trms), meth) end else
1.454 + if pI <> spI
1.455 + then if pI = snd3 ospec then (Pbl, probl, meth) else
1.456 + let val pbt = (#ppc o get_pbt) pI
1.457 + val dI' = #1 (some_spec ospec spec)
1.458 + val oris = if pI = #2 ospec then oris
1.459 + else prep_ori fmz_(assoc_thy"Isac.thy") pbt;
1.460 + in (Pbl, appl_adds dI' oris probl pbt
1.461 + (map itms2fstr probl), meth) end else
1.462 + if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
1.463 + then let val met = (#ppc o get_met) mI
1.464 + val mits = complete_metitms oris probl meth met
1.465 + in if foldl and_ (true, map #3 mits)
1.466 + then (Pbl, probl, mits) else (Met, probl, mits)
1.467 + end else
1.468 + (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
1.469 + ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
1.470 + (imodel2fstr imodel), meth);
1.471 + val pt = update_spec pt p spec;
1.472 + in if pos_ = Pbl
1.473 + then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
1.474 + val pre =check_preconds(assoc_thy"Isac.thy")prls where_ pits
1.475 + in (update_pbl pt p pits,
1.476 + (ocalhd_complete pits pre spec,
1.477 + Pbl, hdf', pits, pre, spec):ocalhd) end
1.478 + else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
1.479 + val pre = check_preconds (assoc_thy"Isac.thy") prls pre mits
1.480 + in (update_met pt p mits,
1.481 + (ocalhd_complete mits pre spec,
1.482 + Met, hdf', mits, pre, spec):ocalhd) end
1.483 + end end
1.484 + | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
1.485 + raise error "input_icalhd Met not impl.";
1.486 +
1.487 +
1.488 +(***. handle an input formula .***)
1.489 +(*
1.490 +Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
1.491 +Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
1.492 +wenn Abteilungen nur auf gleichem Level gesucht werden ?
1.493 +WN.040216
1.494 +
1.495 +Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
1.496 +
1.497 +------------------------------------------------------------------------------
1.498 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
1.499 +------------------------------------------------------------------------------
1.500 +1. "5 * x / (x - 2) - x / (x + 2) = 4"
1.501 +...
1.502 +4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
1.503 +...
1.504 +4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
1.505 +...
1.506 +4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
1.507 +...
1.508 +"[x = -4 / 3]"
1.509 +------------------------------------------------------------------------------
1.510 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.511 +
1.512 +(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
1.513 +------------------------------------------------------------------------------
1.514 +
1.515 +
1.516 +------------------------------------------------------------------------------
1.517 +"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
1.518 +------------------------------------------------------------------------------
1.519 +1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x"
1.520 +...
1.521 +4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
1.522 + Subproblem["normalize", "polynomial", "univariate"..
1.523 +...
1.524 +4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
1.525 +...
1.526 +4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.527 +4.4.5. "[x = 0, x = 6 / 5]"
1.528 +...
1.529 +5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
1.530 + "[x = 6 / 5]"
1.531 +------------------------------------------------------------------------------
1.532 +(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
1.533 +
1.534 +(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
1.535 +------------------------------------------------------------------------------
1.536 +
1.537 +
1.538 +------------------------------------------------------------------------------
1.539 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1.540 +------------------------------------------------------------------------------
1.541 +1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
1.542 +...
1.543 +6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
1.544 + Subproblem["sq", "root", "univariate", "equation"]
1.545 +...
1.546 +6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
1.547 + Subproblem["normalize", "polynomial", "univariate", "equation"]
1.548 +...
1.549 +6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
1.550 +... Or_to_List
1.551 +6.6.3.2 "UniversalList"
1.552 +------------------------------------------------------------------------------
1.553 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
1.554 +
1.555 +(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
1.556 +------------------------------------------------------------------------------
1.557 +*)
1.558 +(*sh. comments auf 498*)
1.559 +
1.560 +fun equal a b = a=b;
1.561 +
1.562 +(*the lists contain eq-al elem-pairs at the beginning;
1.563 + return first list reverted (again) - ie. in order as required subsequently*)
1.564 +fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
1.565 + if equal f1 i1 then
1.566 + if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
1.567 + else (rev (f1::f2::fs), i1::i2::is)
1.568 + else raise error "dropwhile': did not start with equal elements"
1.569 + | dropwhile' equal (f::fs) [i] =
1.570 + if equal f i then (rev (f::fs), [i])
1.571 + else raise error "dropwhile': did not start with equal elements"
1.572 + | dropwhile' equal [f] (i::is) =
1.573 + if equal f i then ([f], i::is)
1.574 + else raise error "dropwhile': did not start with equal elements";
1.575 +(*
1.576 + fun equal a b = a=b;
1.577 + val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
1.578 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.579 + dropwhile' equal r_foder r_ifoder;
1.580 +> vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
1.581 +
1.582 + val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
1.583 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.584 + dropwhile' equal r_foder r_ifoder;
1.585 +> val it = ([3], [3, 12, 11]) : int list * int list
1.586 +
1.587 + val foder = [5]; val ifoder = [11,12,3,4,5];
1.588 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.589 + dropwhile' equal r_foder r_ifoder;
1.590 +> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
1.591 +
1.592 + val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
1.593 + val r_foder = rev foder; val r_ifoder = rev ifoder;
1.594 + dropwhile' equal r_foder r_ifoder;
1.595 +> *** dropwhile': did not start with equal elements*)
1.596 +
1.597 +(*040214: version for concat_deriv*)
1.598 +fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
1.599 +
1.600 +fun mk_tacis ro erls (t, r as Thm _, (t', a)) =
1.601 + (Rewrite (rule2thm' r),
1.602 + Rewrite' ("Isac.thy", fst ro, erls, false,
1.603 + rule2thm' r, t, (t', a)),
1.604 + (e_pos'(*to be updated before generate tacis!!!*), Uistate))
1.605 + | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) =
1.606 + (Rewrite_Set (rule2rls' r),
1.607 + Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)),
1.608 + (e_pos'(*to be updated before generate tacis!!!*), Uistate));
1.609 +
1.610 +(*fo = ifo excluded already in inform*)
1.611 +fun concat_deriv rew_ord erls rules fo ifo =
1.612 + let fun derivat ([]:(term * rule * (term * term list)) list) = e_term
1.613 + | derivat dt = (#1 o #3 o last_elem) dt
1.614 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2
1.615 + val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo
1.616 + val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo
1.617 + in case (fod, ifod) of
1.618 + ([], []) => if fo = ifo then (true, [])
1.619 + else (false, [])
1.620 + | (fod, []) => if derivat fod = ifo
1.621 + then (true, fod) (*ifo is normal form*)
1.622 + else (false, [])
1.623 + | ([], ifod) => if fo = derivat ifod
1.624 + then (true, ((map rev_deriv') o rev) ifod)
1.625 + else (false, [])
1.626 + | (fod, ifod) =>
1.627 + if derivat fod = derivat ifod (*common normal form found*)
1.628 + then let val (fod', rifod') =
1.629 + dropwhile' equal (rev fod) (rev ifod)
1.630 + in (true, fod' @ (map rev_deriv' rifod')) end
1.631 + else (false, [])
1.632 + end;
1.633 +(*
1.634 + val ({rew_ord, erls, rules,...}, fo, ifo) =
1.635 + (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0");
1.636 + (writeln o trtas2str) fod';
1.637 +> ["
1.638 +(x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))","
1.639 +(-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))","
1.640 +(-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))","
1.641 +(1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
1.642 +val it = () : unit
1.643 + (writeln o trtas2str) (map rev_deriv' rifod');
1.644 +> ["
1.645 +(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))","
1.646 +(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))","
1.647 +(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
1.648 +val it = () : unit
1.649 +*)
1.650 +
1.651 +
1.652 +(*.compare inform with ctree.form at current pos by nrls;
1.653 + if found, embed the derivation generated during comparison
1.654 + if not, let the mat-engine compute the next ctree.form.*)
1.655 +(*structure copied from complete_solve
1.656 + CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
1.657 + all_modspec etc. has to be inserted at Subproblem'*)
1.658 +(* val (tacis, c, ptp as (pt, pos as (p,p_))) = (tacis, ptp);
1.659 + val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
1.660 +
1.661 + val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos));
1.662 + -----rec.call:
1.663 + val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
1.664 + *)
1.665 +fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo =
1.666 + let val fo = case p_ of Frm => get_obj g_form pt p
1.667 + | Res => (fst o (get_obj g_result pt)) p
1.668 + | _ => e_term (*on PblObj is fo <> ifo*);
1.669 + val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p))
1.670 + val {rew_ord, erls, rules,...} = rep_rls nrls
1.671 + val (found, der) = concat_deriv rew_ord erls rules fo ifo;
1.672 + in if found
1.673 + then let val tacis' = map (mk_tacis rew_ord erls) der;
1.674 + val (c', ptp) = embed_deriv tacis' ptp;
1.675 + in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end
1.676 + else
1.677 + if pos = ([], Res)
1.678 + then ("no derivation found", (tacis, c, ptp): calcstate')
1.679 + else let val cs' as (tacis, c', ptp) = nxt_solve_ ptp;
1.680 + val cs' as (tacis, c'', ptp) =
1.681 + case tacis of
1.682 + ((Subproblem _, _, _)::_) =>
1.683 + let val ptp as (pt, (p,_)) = all_modspec ptp
1.684 + val mI = get_obj g_metID pt p
1.685 + in nxt_solv (Apply_Method' (mI, NONE, e_istate))
1.686 + e_istate ptp end
1.687 + | _ => cs';
1.688 + in compare_step (tacis, c @ c' @ c'', ptp) ifo end
1.689 + end;
1.690 +(* writeln (trtas2str der);
1.691 + *)
1.692 +
1.693 +(*.handle a user-input formula, which may be a CAS-command, too.
1.694 +CAS-command:
1.695 + create a calchead, and do 1 step
1.696 + TOOODO.WN0602 works only for the root-problem !!!
1.697 +formula, which is no CAS-command:
1.698 + compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
1.699 + collect all the tacs applied by the way.*)
1.700 +(*structure copied from autocalc*)
1.701 +(* val (cs as (_, _, (pt, pos as (p, p_))): calcstate') = cs';
1.702 + val ifo = str2term ifo;
1.703 +
1.704 + val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
1.705 + (cs', encode ifo);
1.706 + val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo));
1.707 + val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
1.708 + (([],[],(pt,p)), (encode ifo));
1.709 + *)
1.710 +fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr =
1.711 + case parse (assoc_thy "Isac.thy") istr of
1.712 +(* val SOME ifo = parse (assoc_thy "Isac.thy") istr;
1.713 + *)
1.714 + SOME ifo =>
1.715 + let val ifo = term_of ifo
1.716 + val fo = case p_ of Frm => get_obj g_form pt p
1.717 + | Res => (fst o (get_obj g_result pt)) p
1.718 + | _ => #3 (get_obj g_origin pt p)
1.719 + in if fo = ifo
1.720 + then ("same-formula", cs)
1.721 + (*thus ctree not cut with replaceFormula!*)
1.722 + else case cas_input ifo of
1.723 +(* val SOME (pt, _) = cas_input ifo;
1.724 + *)
1.725 + SOME (pt, _) => ("ok",([],[],(pt, (p, Met))))
1.726 + | NONE =>
1.727 + compare_step ([],[],(pt,
1.728 + (*last step re-calc in compare_step TODO*)
1.729 + lev_back pos)) ifo
1.730 + end
1.731 + | NONE => ("syntax error in '"^istr^"'", e_calcstate');
1.732 +
1.733 +
1.734 +(*------------------------------------------------------------------(**)
1.735 +end
1.736 +open inform;
1.737 +(**)------------------------------------------------------------------*)