1 signature SPECIFY_NEW =
3 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
4 val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate
5 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
9 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13 structure SpecifyNEW(**): SPECIFY_NEW(**) =
20 (* was Chead.nxt_spec *)
21 fun find_next_step (pt, (p, p_)) =
23 val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
24 case Ctree.get_obj I pt p of
25 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
26 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
27 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
29 if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
32 ["no_met"] => ("ok", (Pbl, Tactic.Refine_Tacitly pI'))
33 | _ => ("ok", (Pbl, Tactic.Model_Problem))
36 val cpI = if pI = Celem.e_pblID then pI' else pI;
37 val cmI = if mI = Celem.e_metID then mI' else mI;
38 val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;
39 val pre = Stool.check_preconds "thy 100820" prls where_ pbl;
40 val preok = foldl and_ (true, map fst pre);
41 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
42 val mpc = (#ppc o Specify.get_met) cmI
46 (if dI' = Rule.e_domID andalso dI = Rule.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
47 else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
49 case find_first (is_error o #5) pbl of
50 SOME (_, _, _, fd, itm_) =>
51 ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_))
53 (case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris pbt pbl of
54 SOME (fd, ct') => ("dummy", (Pbl, mk_additem fd ct'))
55 | NONE => (*pbl-items complete*)
56 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
57 else if dI = Rule.e_domID then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
58 else if pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
59 else if mI = Celem.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))
61 case find_first (is_error o #5) met of
62 SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy dI) fd itm_))
64 (case nxt_add (Celem.assoc_thy dI) oris mpc met of
65 SOME (fd, ct') => ("dummy", (Met, mk_additem fd ct')) (*30.8.01: pre?!?*)
66 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
68 (case find_first (is_error o #5) met of
69 SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) fd itm_))
71 case nxt_add (Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)) oris mpc met of
72 SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
74 (if dI = Rule.e_domID then ("dummy", (Met, Tactic.Specify_Theory dI'))
75 else if pI = Celem.e_pblID then ("dummy", (Met, Tactic.Specify_Problem pI'))
76 else if not preok then ("dummy", (Met, Tactic.Specify_Method mI))
77 else ("dummy", (Met, Tactic.Apply_Method mI))))
78 | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)
82 (* create a calc-tree with oris via an cas.refined pbl *)
83 fun nxt_specify_init_calc ([], (dI, pI, mI)) =
85 then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
87 val {cas, met, ppc, thy, ...} = Specify.get_pbt pI
88 val dI = if dI = "" then Rule.theory2theory' thy else dI
89 val mI = if mI = [] then hd met else mI
90 val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
91 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
92 ([], (dI,pI,mI), hdl, ContextC.empty)
93 val pt = update_spec pt [] (dI, pI, mI)
94 val pits = Generate.init_pbl' ppc
95 val pt = update_pbl pt [] pits
96 in ((pt, ([] , Pbl)), []) end
99 then (* from met-browser *)
101 val {ppc, ...} = Specify.get_met mI
102 val dI = if dI = "" then "Isac_Knowledge" else dI
103 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) ([], (dI, pI, mI))
104 ([], (dI, pI, mI), Rule.e_term, ContextC.empty)
105 val pt = update_spec pt [] (dI, pI, mI)
106 val mits = Generate.init_pbl' ppc
107 val pt = update_met pt [] mits
108 in ((pt, ([], Met)), []) end
109 else (* new example, pepare for interactive modeling *)
111 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
112 ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)
113 in ((pt, ([], Pbl)), []) end
114 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
115 let (* both """"""""""""""""""""""""" either empty or complete *)
116 val thy = Celem.assoc_thy dI
117 val (pI, (pors, pctxt), mI) =
121 val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
122 val pI' = Specify.refine_ori' pors pI;
123 in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
124 (hd o #met o Specify.get_pbt) pI')
126 else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)
127 val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)
128 val dI = Rule.theory2theory' (Stool.common_subthy (thy, thy'))
129 val hdl = case cas of
130 NONE => Auto_Prog.pblterm dI pI
131 | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t
132 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) (fmz, (dI, pI, mI))
133 (pors, (dI, pI, mI), hdl, pctxt)
135 ((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))