250 (let val t = d $ t'; |
250 (let val t = d $ t'; |
251 val s = Sign.string_of_term (sign_of dI) t; |
251 val s = Sign.string_of_term (sign_of 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 dI itm^ |
255 raise error ("parsitm ("^itm2str_ 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 = |
356 *) |
356 *) |
357 (* val (dI, oris, ppc, pbt, (selct::ss))= |
357 (* val (dI, oris, ppc, pbt, (selct::ss))= |
358 (#1 (some_spec ospec spec), oris, []:itm list, |
358 (#1 (some_spec ospec spec), oris, []:itm list, |
359 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); |
359 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); |
360 val iii = appl_adds dI oris ppc pbt (selct::ss); |
360 val iii = appl_adds dI oris ppc pbt (selct::ss); |
361 writeln(itms2str thy iii); |
361 writeln(itms2str_ thy iii); |
362 |
362 |
363 val itm = appl_add' dI oris ppc pbt selct; |
363 val itm = appl_add' dI oris ppc pbt selct; |
364 val ppc = insert_ppc' itm ppc; |
364 val ppc = insert_ppc' itm ppc; |
365 |
365 |
366 val _::selct::ss = (selct::ss); |
366 val _::selct::ss = (selct::ss); |
368 val ppc = insert_ppc' itm ppc; |
368 val ppc = insert_ppc' itm ppc; |
369 |
369 |
370 val _::selct::ss = (selct::ss); |
370 val _::selct::ss = (selct::ss); |
371 val itm = appl_add' dI oris ppc pbt selct; |
371 val itm = appl_add' dI oris ppc pbt selct; |
372 val ppc = insert_ppc' itm ppc; |
372 val ppc = insert_ppc' itm ppc; |
373 writeln(itms2str thy ppc); |
373 writeln(itms2str_ thy ppc); |
374 |
374 |
375 val _::selct::ss = (selct::ss); |
375 val _::selct::ss = (selct::ss); |
376 val itm = appl_add' dI oris ppc pbt selct; |
376 val itm = appl_add' dI oris ppc pbt selct; |
377 val ppc = insert_ppc' itm ppc; |
377 val ppc = insert_ppc' itm ppc; |
378 *) |
378 *) |
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 = raise error ("par2fstr: called with "^ |
396 itm2str (assoc_thy "Isac.thy") itm); |
396 itm2str_ (assoc_thy "Isac.thy") 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 (assoc_thy "Isac.thy") itm^ |
404 raise error ("parsitm ("^itm2str_ (assoc_thy "Isac.thy") 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) = |