15 "----------- fun step -----------------------------------"; |
12 "----------- fun step -----------------------------------"; |
16 "----------- fun autocalc -------------------------------"; |
13 "----------- fun autocalc -------------------------------"; |
17 "----------- fun autoCalculate --------------------------"; |
14 "----------- fun autoCalculate --------------------------"; |
18 "----------- fun autoCalculate..CompleteCalc ------------"; |
15 "----------- fun autoCalculate..CompleteCalc ------------"; |
19 "----------- search for Or_to_List ----------------------"; |
16 "----------- search for Or_to_List ----------------------"; |
|
17 "----------- check thy in CalcTreeTEST ------------------"; |
20 "--------------------------------------------------------"; |
18 "--------------------------------------------------------"; |
21 "--------------------------------------------------------"; |
19 "--------------------------------------------------------"; |
22 "--------------------------------------------------------"; |
20 "--------------------------------------------------------"; |
23 |
21 |
24 "----------- change to parse ctxt -----------------------"; |
22 "----------- change to parse ctxt -----------------------"; |
467 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
465 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; |
468 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) |
466 val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is; (*WAS Empty_Tac_: tac_*) |
469 case tac_ of Or_to_List' _ => () |
467 case tac_ of Or_to_List' _ => () |
470 | _ => error "Or_to_List broken ?" |
468 | _ => error "Or_to_List broken ?" |
471 |
469 |
472 |
470 "----------- check thy in CalcTreeTEST ------------------"; |
|
471 "----------- check thy in CalcTreeTEST ------------------"; |
|
472 "----------- check thy in CalcTreeTEST ------------------"; |
|
473 "WN1109 with Inverse_Z_Transform.thy when starting tests with CalcTreeTEST \n" ^ |
|
474 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^ |
|
475 "Below there are the steps which found out the reason: \n" ^ |
|
476 "store_pbt mistakenly stored that theory."; |
|
477 val ctxt = ProofContext.init_global @{theory Isac}; |
|
478 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))"; |
|
479 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)"; |
|
480 |
|
481 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", |
|
482 "stepResponse (x[n::real]::bool)"]; |
|
483 val (dI,pI,mI) = ("Isac", ["inverse", "Z_Transform", "SignalProcessing"], |
|
484 ["SignalProcessing","Z_Transform","inverse"]); |
|
485 |
|
486 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; |
|
487 (*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
|
488 |
|
489 "~~~~~ T fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI,pI,mI))]; |
|
490 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz, (dI, pI, mI)) = (fmz, sp); |
|
491 val thy = assoc_thy dI; |
|
492 mI = ["no_met"]; (*false*) |
|
493 val (pI, (pors, pctxt), mI) = (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI) |
|
494 val {cas, ppc, thy=thy',...} = get_pbt pI; (*take dI from _refined_ pbl*) |
|
495 "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*) |
|
496 val dI = theory2theory' (maxthy thy thy'); |
|
497 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
|
498 cas = NONE; (*true*) |
|
499 val hdl = pblterm dI pI; |
|
500 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI)) |
|
501 (pors, (dI, pI, mI), hdl) |
|
502 val pt = update_ctxt pt [] pctxt; |
|
503 |
|
504 "~~~~~ fun nxt_specif, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl))); |
|
505 val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p; |
|
506 "tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*) |
|
507 |
|
508 "~~~~~ fun some_spec, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec); |
|
509 dI = e_domID; (*true*) |
|
510 odI = "Build_Inverse_Z_Transform"; (*true*) |
|
511 dI = "e_domID"; (*true*) |
|
512 "~~~~~ after fun some_spec:"; |
|
513 val (dI, pI, mI) = some_spec ospec spec; |
|
514 "tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*) |
|
515 val thy = assoc_thy dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*) |
|
516 |