walther@59747
|
1 |
(* Title: Specify/step-specify.sml
|
walther@59747
|
2 |
Author: Walther Neuper 2019
|
walther@59747
|
3 |
(c) due to copyright terms
|
walther@59747
|
4 |
*)
|
walther@59747
|
5 |
|
walther@59747
|
6 |
signature STEP_SPECIFY =
|
walther@59747
|
7 |
sig
|
walther@59763
|
8 |
val by_tactic: Tactic.input -> Ctree.state -> Chead.calcstate'
|
walther@59763
|
9 |
(*val do_next: Step.specify_do_next requires LucinNEW.by_tactic, which is not yet known in Step_Specify*)
|
walther@59747
|
10 |
|
walther@59747
|
11 |
end
|
walther@59747
|
12 |
|
walther@59747
|
13 |
(**)
|
walther@59747
|
14 |
structure Step_Specify(**): STEP_SPECIFY(**) =
|
walther@59747
|
15 |
struct
|
walther@59747
|
16 |
(**)
|
walther@59763
|
17 |
open Pos
|
walther@59763
|
18 |
open Ctree
|
walther@59763
|
19 |
open Chead
|
walther@59747
|
20 |
|
walther@59763
|
21 |
(* was fun Math_Engine.nxt_specify_ *)
|
walther@59763
|
22 |
fun by_tactic (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
|
walther@59763
|
23 |
let
|
walther@59763
|
24 |
val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
|
walther@59763
|
25 |
PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
|
walther@59763
|
26 |
| _ => error "by_tactic Model_Problem; uncovered case get_obj"
|
walther@59763
|
27 |
val (dI, pI, mI) = some_spec ospec spec
|
walther@59763
|
28 |
val thy = Celem.assoc_thy dI
|
walther@59763
|
29 |
val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)
|
walther@59763
|
30 |
val {cas, ppc, ...} = Specify.get_pbt pI
|
walther@59763
|
31 |
val pbl = Generate.init_pbl ppc (* fill in descriptions *)
|
walther@59763
|
32 |
(*----------------if you think, this should be done by the Dialog
|
walther@59763
|
33 |
in the java front-end, search there for WN060225-modelProblem----*)
|
walther@59763
|
34 |
val (pbl, met) = case cas of
|
walther@59763
|
35 |
NONE => (pbl, [])
|
walther@59763
|
36 |
| _ => complete_mod_ (oris, mpc, ppc, probl)
|
walther@59763
|
37 |
(*----------------------------------------------------------------*)
|
walther@59763
|
38 |
val tac_ = Tactic.Model_Problem' (pI, pbl, met)
|
walther@59763
|
39 |
val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
40 |
in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end
|
walther@59763
|
41 |
| by_tactic (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
|
walther@59763
|
42 |
| by_tactic (Tactic.Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
|
walther@59763
|
43 |
| by_tactic (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
|
walther@59763
|
44 |
(*. called only if no_met is specified .*)
|
walther@59763
|
45 |
| by_tactic (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
|
walther@59763
|
46 |
let
|
walther@59763
|
47 |
val (oris, dI, ctxt) = case get_obj I pt p of
|
walther@59763
|
48 |
(PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
|
walther@59763
|
49 |
| _ => error "by_tactic Refine_Tacitly: uncovered case get_obj"
|
walther@59763
|
50 |
val opt = Specify.refine_ori oris pI
|
walther@59763
|
51 |
in
|
walther@59763
|
52 |
case opt of
|
walther@59763
|
53 |
SOME pI' =>
|
walther@59763
|
54 |
let
|
walther@59763
|
55 |
val {met, ...} = Specify.get_pbt pI'
|
walther@59763
|
56 |
(*val pt = update_pbl pt p pbl ..done by Model_Problem*)
|
walther@59763
|
57 |
val mI = if length met = 0 then Celem.e_metID else hd met
|
walther@59763
|
58 |
val thy = Celem.assoc_thy dI
|
walther@59763
|
59 |
val (pos, c, _, pt) =
|
walther@59763
|
60 |
Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
61 |
in
|
walther@59763
|
62 |
([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
|
walther@59763
|
63 |
(pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
|
walther@59763
|
64 |
end
|
walther@59763
|
65 |
| NONE => ([], [], ptp)
|
walther@59763
|
66 |
end
|
walther@59763
|
67 |
| by_tactic (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
|
walther@59763
|
68 |
let
|
walther@59763
|
69 |
val (dI, dI', probl, ctxt) = case get_obj I pt p of
|
walther@59763
|
70 |
PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
|
walther@59763
|
71 |
(dI, dI', probl, ctxt)
|
walther@59763
|
72 |
| _ => error "by_tactic Refine_Problem: uncovered case get_obj"
|
walther@59763
|
73 |
val thy = if dI' = Rule.e_domID then dI else dI'
|
walther@59763
|
74 |
in
|
walther@59763
|
75 |
case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of
|
walther@59763
|
76 |
NONE => ([], [], ptp)
|
walther@59763
|
77 |
| SOME rfd =>
|
walther@59763
|
78 |
let
|
walther@59763
|
79 |
val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
80 |
in
|
walther@59763
|
81 |
([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
|
walther@59763
|
82 |
end
|
walther@59763
|
83 |
end
|
walther@59763
|
84 |
| by_tactic (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =
|
walther@59763
|
85 |
let
|
walther@59763
|
86 |
val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
|
walther@59763
|
87 |
PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
|
walther@59763
|
88 |
(oris, dI, dI', pI', probl, ctxt)
|
walther@59763
|
89 |
| _ => error ""
|
walther@59763
|
90 |
val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');
|
walther@59763
|
91 |
val {ppc,where_,prls,...} = Specify.get_pbt pI
|
walther@59763
|
92 |
val pbl =
|
walther@59763
|
93 |
if pI' = Celem.e_pblID andalso pI = Celem.e_pblID
|
walther@59763
|
94 |
then (false, (Generate.init_pbl ppc, []))
|
walther@59763
|
95 |
else Specify.match_itms_oris thy probl (ppc,where_,prls) oris
|
walther@59763
|
96 |
(*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
|
walther@59763
|
97 |
val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) pos pt of
|
walther@59763
|
98 |
((_, Pbl), c, _, pt) => (c, pt)
|
walther@59763
|
99 |
| _ => error ""
|
walther@59763
|
100 |
in
|
walther@59763
|
101 |
([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))
|
walther@59763
|
102 |
end
|
walther@59763
|
103 |
(* transfers oris (not required in pbl) to met-model for script-env
|
walther@59763
|
104 |
FIXME.WN.8.03: application of several mIDs to SAME model? *)
|
walther@59763
|
105 |
| by_tactic (Tactic.Specify_Method mID) (pt, pos as (p,_)) =
|
walther@59763
|
106 |
let
|
walther@59763
|
107 |
val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of
|
walther@59763
|
108 |
PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}
|
walther@59763
|
109 |
=> (oris, pbl, dI, met, ctxt)
|
walther@59763
|
110 |
| _ => error "by_tactic Specify_Method: uncovered case get_obj"
|
walther@59763
|
111 |
val {ppc,pre,prls,...} = Specify.get_met mID
|
walther@59763
|
112 |
val thy = Celem.assoc_thy dI
|
walther@59763
|
113 |
val oris = Specify.add_field' thy ppc oris
|
walther@59763
|
114 |
val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
|
walther@59763
|
115 |
val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris
|
walther@59763
|
116 |
val itms = Specify.hack_until_review_Specify_2 mID itms
|
walther@59763
|
117 |
val (pos, c, _, pt) =
|
walther@59763
|
118 |
Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
119 |
in
|
walther@59763
|
120 |
([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos))
|
walther@59763
|
121 |
end
|
walther@59763
|
122 |
| by_tactic (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
|
walther@59763
|
123 |
let
|
walther@59763
|
124 |
val ctxt = get_ctxt pt pos
|
walther@59763
|
125 |
val (pos, c, _, pt) =
|
walther@59763
|
126 |
Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
127 |
in (*FIXXXME: check if pbl can still be parsed*)
|
walther@59763
|
128 |
([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,
|
walther@59763
|
129 |
(pt, pos))
|
walther@59763
|
130 |
end
|
walther@59763
|
131 |
| by_tactic (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
|
walther@59763
|
132 |
let
|
walther@59763
|
133 |
val ctxt = get_ctxt pt pos
|
walther@59763
|
134 |
val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt
|
walther@59763
|
135 |
in (*FIXXXME: check if met can still be parsed*)
|
walther@59763
|
136 |
([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))
|
walther@59763
|
137 |
end
|
walther@59763
|
138 |
| by_tactic m' _ = error ("by_tactic: not impl. for " ^ Tactic.tac2str m')
|
walther@59763
|
139 |
|
walther@59763
|
140 |
(**)end(**)
|