250 (let val t = d $ t'; |
250 (let val t = d $ t'; |
251 val s = Syntax.string_of_term (thy2ctxt dI) t; |
251 val s = Syntax.string_of_term (thy2ctxt dI) t; |
252 (*this ^ should raise the exn on unability of re-parsing dts*) |
252 (*this ^ should raise the exn on unability of re-parsing dts*) |
253 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
253 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
254 | parsitm dI (itm as (i,v,_,f, Par _)) = |
254 | parsitm dI (itm as (i,v,_,f, Par _)) = |
255 raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^ |
255 error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^ |
256 "): Par should be internal"); |
256 "): Par should be internal"); |
257 |
257 |
258 (*separate a list to a pair of elements that do NOT satisfy the predicate, |
258 (*separate a list to a pair of elements that do NOT satisfy the predicate, |
259 and of elements that satisfy the predicate, i.e. (false, true)*) |
259 and of elements that satisfy the predicate, i.e. (false, true)*) |
260 fun filter_sep pred xs = |
260 fun filter_sep pred xs = |
292 (* val ("",itm) = is_notyet_input thy ppc all ori' pbt; |
292 (* val ("",itm) = is_notyet_input thy ppc all ori' pbt; |
293 *) |
293 *) |
294 ("",itm) => itm |
294 ("",itm) => itm |
295 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt; |
295 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt; |
296 *) |
296 *) |
297 | (msg,_) => raise error ("appl_add': "^msg)) |
297 | (msg,_) => error ("appl_add': "^msg)) |
298 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct); |
298 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct); |
299 *) |
299 *) |
300 | (msg,(i,v,_,d,ts),_) => |
300 | (msg,(i,v,_,d,ts),_) => |
301 if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[]))) |
301 if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[]))) |
302 else (i,v,false,sel, Sup (d,ts))) |
302 else (i,v,false,sel, Sup (d,ts))) |
390 |
390 |
391 |
391 |
392 |
392 |
393 |
393 |
394 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s) |
394 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s) |
395 | par2fstr itm = raise error ("par2fstr: called with " ^ |
395 | par2fstr itm = error ("par2fstr: called with " ^ |
396 itm2str_ (thy2ctxt' "Isac") itm); |
396 itm2str_ (thy2ctxt' "Isac") itm); |
397 fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts)) |
397 fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts)) |
398 | itms2fstr (_,_,_,f, Syn str) = (f, str) |
398 | itms2fstr (_,_,_,f, Syn str) = (f, str) |
399 | itms2fstr (_,_,_,f, Typ str) = (f, str) |
399 | itms2fstr (_,_,_,f, Typ str) = (f, str) |
400 | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts)) |
400 | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts)) |
401 | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts)) |
401 | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts)) |
402 | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t)) |
402 | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t)) |
403 | itms2fstr (itm as (_,_,_,f, Par _)) = |
403 | itms2fstr (itm as (_,_,_,f, Par _)) = |
404 raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ |
404 error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ |
405 "): Par should be internal"); |
405 "): Par should be internal"); |
406 |
406 |
407 fun imodel2fstr iitems = |
407 fun imodel2fstr iitems = |
408 let fun xxx is [] = is |
408 let fun xxx is [] = is |
409 | xxx is ((Given strs)::iis) = |
409 | xxx is ((Given strs)::iis) = |
477 in (update_met pt p mits, |
477 in (update_met pt p mits, |
478 (ocalhd_complete mits pre spec, |
478 (ocalhd_complete mits pre spec, |
479 Met, hdf', mits, pre, spec):ocalhd) end |
479 Met, hdf', mits, pre, spec):ocalhd) end |
480 end end |
480 end end |
481 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) = |
481 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) = |
482 raise error "input_icalhd Met not impl."; |
482 error "input_icalhd Met not impl."; |
483 |
483 |
484 |
484 |
485 (***. handle an input formula .***) |
485 (***. handle an input formula .***) |
486 (* |
486 (* |
487 Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler: |
487 Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler: |
560 return first list reverted (again) - ie. in order as required subsequently*) |
560 return first list reverted (again) - ie. in order as required subsequently*) |
561 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = |
561 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = |
562 if equal f1 i1 then |
562 if equal f1 i1 then |
563 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is) |
563 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is) |
564 else (rev (f1::f2::fs), i1::i2::is) |
564 else (rev (f1::f2::fs), i1::i2::is) |
565 else raise error "dropwhile': did not start with equal elements" |
565 else error "dropwhile': did not start with equal elements" |
566 | dropwhile' equal (f::fs) [i] = |
566 | dropwhile' equal (f::fs) [i] = |
567 if equal f i then (rev (f::fs), [i]) |
567 if equal f i then (rev (f::fs), [i]) |
568 else raise error "dropwhile': did not start with equal elements" |
568 else error "dropwhile': did not start with equal elements" |
569 | dropwhile' equal [f] (i::is) = |
569 | dropwhile' equal [f] (i::is) = |
570 if equal f i then ([f], i::is) |
570 if equal f i then ([f], i::is) |
571 else raise error "dropwhile': did not start with equal elements"; |
571 else error "dropwhile': did not start with equal elements"; |
572 (* |
572 (* |
573 fun equal a b = a=b; |
573 fun equal a b = a=b; |
574 val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5]; |
574 val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5]; |
575 val r_foder = rev foder; val r_ifoder = rev ifoder; |
575 val r_foder = rev foder; val r_ifoder = rev ifoder; |
576 dropwhile' equal r_foder r_ifoder; |
576 dropwhile' equal r_foder r_ifoder; |