426 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts)); |
426 "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts)); |
427 |
427 |
428 (*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]" |
428 (*+*)val "[[0 = - 1 * c_4 / - 1], [0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24], [0 = c_2], [0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]]" |
429 = ts |> UnparseC.terms @{context} |
429 = ts |> UnparseC.terms @{context} |
430 |
430 |
431 val ts = if Model_Pattern.is_list_descr descr |
431 val ts = if Pre_Conds.is_list_descr descr |
432 then if TermC.is_list (hd ts) |
432 then if TermC.is_list (hd ts) |
433 then ts |> map TermC.isalist2list |> flat |
433 then ts |> map TermC.isalist2list |> flat |
434 else ts |
434 else ts |
435 else ts |
435 else ts |
436 |
436 |
555 spec = refs, ...} = Calc.specify_data (pt, pos); |
555 spec = refs, ...} = Calc.specify_data (pt, pos); |
556 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
556 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); |
557 (*if*) p_ = Pos.Pbl (*then*); |
557 (*if*) p_ = Pos.Pbl (*then*); |
558 |
558 |
559 val ("dummy", (Pbl, Add_Find "solutions L")) = |
559 val ("dummy", (Pbl, Add_Find "solutions L")) = |
560 for_problem ctxt oris (o_refs, refs) (pbl, met); |
560 for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_TEST met); |
561 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
561 "~~~~~ fun for_problem , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) = |
562 (oris, (o_refs, refs), (pbl, met)); |
562 (oris, (o_refs, refs), (pbl, met)); |
563 val cpI = if pI = Problem.id_empty then pI' else pI; |
563 val cpI = if pI = Problem.id_empty then pI' else pI; |
564 val cmI = if mI = MethodC.id_empty then mI' else mI; |
564 val cmI = if mI = MethodC.id_empty then mI' else mI; |
565 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
565 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; |
567 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); |
567 val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl); |
568 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
568 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); |
569 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); |
569 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); |
570 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*); |
570 val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*); |
571 val SOME ("#Find", "solutions L") = (*case*) |
571 val SOME ("#Find", "solutions L") = (*case*) |
572 item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*); |
572 item_to_add ctxt oris (I_Model.OLD_to_TEST pbl); |
573 (*if*) not preok (*then*); |
573 (*if*) not preok (*then*); |
574 |
574 |
575 (*+*)Pre_Conds.to_string @{context} xxxxx = "[\n" ^ |
575 (*+*)Pre_Conds.to_string @{context} xxxxx = "[\n" ^ |
576 "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^ |
576 "(false, matches (x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^ |
577 "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^ |
577 "matches (?b * x = 0) ((x + 1) * (x + 2) = x \<up> 2 + 8) \<or>\n" ^ |