| changeset 59898 | 68883c046963 |
| parent 59886 | 106e7d8723ca |
| child 59903 | 5037ca1b112b |
| 59897:8cba439d0454 | 59898:68883c046963 |
|---|---|
10 val autocalc : Pos.pos' list -> Pos.pos' -> (Calc.T) * Generate.taci list -> |
10 val autocalc : Pos.pos' list -> Pos.pos' -> (Calc.T) * Generate.taci list -> |
11 Solve.auto -> string * Pos.pos' list * (Calc.T) |
11 Solve.auto -> string * Pos.pos' list * (Calc.T) |
12 |
12 |
13 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list |
13 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list |
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
15 val context_met : Celem.metID -> Ctree.ctree -> Pos.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list |
15 val context_met : Spec.metID -> Ctree.ctree -> Pos.pos -> bool * Spec.metID * Program.T * Model.itm list * (bool * term) list |
16 val context_pbl : Celem.pblID -> Ctree.ctree -> Pos.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
16 val context_pbl : Spec.pblID -> Ctree.ctree -> Pos.pos -> bool * Spec.pblID * term * Model.itm list * (bool * term) list |
17 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
17 val set_method : Spec.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
18 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
18 val set_problem : Spec.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
19 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
19 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd |
20 val tryrefine : Celem.pblID -> Ctree.ctree -> Pos.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
20 val tryrefine : Spec.pblID -> Ctree.ctree -> Pos.pos' -> bool * Spec.pblID * term * Model.itm list * (bool * term) list |
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
22 (*NONE*) |
22 (*NONE*) |
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
24 (*NONE*) |
24 (*NONE*) |
25 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
25 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
142 case Ctree.get_obj I pt p of |
142 case Ctree.get_obj I pt p of |
143 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...} |
143 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...} |
144 => (probl, os, pI, hdl, pI') |
144 => (probl, os, pI, hdl, pI') |
145 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case" |
145 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case" |
146 val pblID = |
146 val pblID = |
147 if pI' = Celem.e_pblID |
147 if pI' = Spec.e_pblID |
148 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) |
148 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) |
149 else pI' |
149 else pI' |
150 val {ppc, where_, prls, ...} = Specify.get_pbt pblID |
150 val {ppc, where_, prls, ...} = Specify.get_pbt pblID |
151 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os |
151 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os |
152 in |
152 in |
157 let |
157 let |
158 val (meth, os, mI, mI') = |
158 val (meth, os, mI, mI') = |
159 case Ctree.get_obj I pt p of |
159 case Ctree.get_obj I pt p of |
160 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI') |
160 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI') |
161 | Ctree.PrfObj _ => error "initcontext_met: uncovered case" |
161 | Ctree.PrfObj _ => error "initcontext_met: uncovered case" |
162 val metID = if mI' = Celem.e_metID |
162 val metID = if mI' = Spec.e_metID |
163 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) |
163 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) |
164 else mI' |
164 else mI' |
165 val {ppc, pre, prls, scr, ...} = Specify.get_met metID |
165 val {ppc, pre, prls, scr, ...} = Specify.get_met metID |
166 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os |
166 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os |
167 in |
167 in |