341 | _ => #3 (get_obj g_origin pt p); |
341 | _ => #3 (get_obj g_origin pt p); |
342 |
342 |
343 (* in CalcTree/Subproblem an 'just_created_' model is created; |
343 (* in CalcTree/Subproblem an 'just_created_' model is created; |
344 this is filled to 'untouched' by Model/Refine_Problem *) |
344 this is filled to 'untouched' by Model/Refine_Problem *) |
345 fun just_created_ (PblObj {meth, probl, spec, ...}) = |
345 fun just_created_ (PblObj {meth, probl, spec, ...}) = |
346 null meth andalso null probl andalso spec = Spec.empty_spec |
346 null meth andalso null probl andalso spec = Spec.empty |
347 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def."; |
347 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def."; |
348 val e_origin = ([], Spec.empty_spec, TermC.empty); |
348 val e_origin = ([], Spec.empty, TermC.empty); |
349 |
349 |
350 fun just_created (pt, (p, _)) = |
350 fun just_created (pt, (p, _)) = |
351 let val ppobj = get_obj I pt p |
351 let val ppobj = get_obj I pt p |
352 in is_pblobj ppobj andalso just_created_ ppobj end; |
352 in is_pblobj ppobj andalso just_created_ ppobj end; |
353 |
353 |
439 pos_ * (* model belongs to Problem | Method *) |
439 pos_ * (* model belongs to Problem | Method *) |
440 term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*) |
440 term * (* header: Problem ... or Cas FIXME.0312: item for marking syntaxerrors*) |
441 Model.itm list * (* model: given, find, relate *) |
441 Model.itm list * (* model: given, find, relate *) |
442 ((bool * term) list) *(* model: preconds *) |
442 ((bool * term) list) *(* model: preconds *) |
443 Spec.spec; (* specification *) |
443 Spec.spec; (* specification *) |
444 val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty_spec); |
444 val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty); |
445 |
445 |
446 datatype ptform = Form of term | ModSpec of ocalhd; |
446 datatype ptform = Form of term | ModSpec of ocalhd; |
447 |
447 |
448 (* for cut_level; (deprecated) *) |
448 (* for cut_level; (deprecated) *) |
449 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB |
449 fun test_trans (PrfObj {branch, ...}) = true andalso branch = TransitiveB |
544 (apsnd UnparseC.term) o |
544 (apsnd UnparseC.term) o |
545 (apfst bool2str)))) bts; |
545 (apfst bool2str)))) bts; |
546 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *) |
546 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *) |
547 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^ |
547 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^ |
548 ", " ^ Model.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms ^ |
548 ", " ^ Model.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms ^ |
549 ", " ^ preconds2str prec ^ ", \n" ^ Spec.spec2str spec ^ " )"; |
549 ", " ^ preconds2str prec ^ ", \n" ^ Spec.to_string spec ^ " )"; |
550 |
550 |
551 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj |
551 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj |
552 | is_pblnd _ = error "is_pblnd: uncovered fun def."; |
552 | is_pblnd _ = error "is_pblnd: uncovered fun def."; |
553 |
553 |
554 |
554 |