1.1 --- a/src/Tools/isac/Specify/Specify.thy Tue Feb 11 11:58:45 2020 +0100
1.2 +++ b/src/Tools/isac/Specify/Specify.thy Tue Feb 11 17:25:45 2020 +0100
1.3 @@ -16,6 +16,286 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 +open Ctree
1.8 +open Pos
1.9 +open Chead
1.10 +\<close> ML \<open>
1.11 +\<close> ML \<open>
1.12 +\<close> ML \<open>
1.13 +\<close> ML \<open>
1.14 +fun header p_ pI mI =
1.15 + case p_ of Pbl => Generate.Problem (if pI = Celem.e_pblID then [] else pI)
1.16 + | Met => Generate.Method mI
1.17 + | pos => error ("header called with "^ pos_2str pos)
1.18 +\<close> ML \<open>
1.19 +fun overwrite_ppc thy itm ppc =
1.20 + let
1.21 + fun repl _ (_, _, _, _, itm_) [] =
1.22 + error ("overwrite_ppc: " ^ (Model.itm_2str_ (Rule.thy2ctxt thy) itm_) ^ " not found")
1.23 + | repl ppc' itm (p :: ppc) =
1.24 + if (#1 itm) = (#1 p)
1.25 + then ppc' @ [itm] @ ppc
1.26 + else repl (ppc' @ [p]) itm ppc
1.27 + in repl [] itm ppc end
1.28 +\<close> ML \<open>
1.29 +fun seek_ppc _ [] = NONE
1.30 + | seek_ppc id (p :: ppc) = if id = #1 (p: Model.itm) then SOME p else seek_ppc id ppc
1.31 +\<close> ML \<open>
1.32 +fun insert_ppc thy itm ppc =
1.33 + let
1.34 + fun eq_untouched d (0, _, _, _, itm_) = (d = Model.d_in itm_)
1.35 + | eq_untouched _ _ = false
1.36 + val ppc' = case seek_ppc (#1 itm) ppc of
1.37 + SOME _ => overwrite_ppc thy itm ppc (*itm updated in is_notyet_input WN.11.03*)
1.38 + | NONE => (ppc @ [itm])
1.39 + in filter_out (eq_untouched ((Model.d_in o #5) itm)) ppc' end
1.40 +\<close> ML \<open>
1.41 +fun specify_additem sel ct (pt, (p, Met)) =
1.42 + let
1.43 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
1.44 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.45 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.46 + | _ => error "specify_additem: uncovered case of get_obj I pt p"
1.47 + val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
1.48 + val cpI = if pI = Celem.e_pblID then pI' else pI
1.49 + val cmI = if mI = Celem.e_metID then mI' else mI
1.50 + val {ppc, pre, prls, ...} = Specify.get_met cmI
1.51 + in
1.52 + case Chead.appl_add ctxt sel oris met ppc ct of
1.53 + Chead.Add itm => (*..union old input *)
1.54 + let
1.55 + val met' = insert_ppc thy itm met
1.56 + val arg = case sel of
1.57 + "#Given" => Tactic.Add_Given' (ct, met')
1.58 + | "#Find" => Tactic.Add_Find' (ct, met')
1.59 + | "#Relate"=> Tactic.Add_Relation'(ct, met')
1.60 + | str => error ("specify_additem: uncovered case with " ^ str)
1.61 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p, Met) pt of
1.62 + ((p, Met), _, _, pt') => (p, pt')
1.63 + | _ => error "specify_additem: uncovered case of generate1"
1.64 + val pre' = Stool.check_preconds thy prls pre met'
1.65 + val pb = foldl and_ (true, map fst pre')
1.66 + val (p_, nxt) =
1.67 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met')
1.68 + ((#ppc o Specify.get_pbt) cpI,ppc) (dI,pI,mI);
1.69 + in
1.70 + ("ok", ([], [], (pt', (p, p_))))
1.71 + end
1.72 + | Err msg =>
1.73 + let
1.74 + val pre' = Stool.check_preconds thy prls pre met
1.75 + val pb = foldl and_ (true, map fst pre')
1.76 + val (p_, nxt) =
1.77 + nxt_spec Met pb oris (dI',pI',mI') (pbl,met)
1.78 + ((#ppc o Specify.get_pbt) cpI,(#ppc o Specify.get_met) cmI) (dI,pI,mI);
1.79 + in
1.80 + (msg, ([], [], (pt, (p, p_))))
1.81 + end
1.82 + end
1.83 + | specify_additem sel ct (pt, (p,_(*Frm, Pbl*))) =
1.84 + let
1.85 + val (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt) = case get_obj I pt p of
1.86 + (PblObj {meth = met, origin = (oris, (dI', pI', mI'),_), probl = pbl, spec = (dI, pI, mI), ctxt, ...})
1.87 + => (met, oris, dI', pI', mI', pbl, dI ,pI, mI, ctxt)
1.88 + | _ => error "specify_additem Frm, Pbl: uncovered case of get_obj I pt p"
1.89 + val thy = if dI = Rule.e_domID then Celem.assoc_thy dI' else Celem.assoc_thy dI
1.90 + val cpI = if pI = Celem.e_pblID then pI' else pI
1.91 + val cmI = if mI = Celem.e_metID then mI' else mI
1.92 + val {ppc, where_, prls, ...} = Specify.get_pbt cpI
1.93 + in
1.94 + case appl_add ctxt sel oris pbl ppc ct of
1.95 + Add itm => (*..union old input *)
1.96 + let
1.97 + val pbl' = insert_ppc thy itm pbl
1.98 + val arg = case sel of
1.99 + "#Given" => Tactic.Add_Given' (ct, pbl')
1.100 + | "#Find" => Tactic.Add_Find' (ct, pbl')
1.101 + | "#Relate"=> Tactic.Add_Relation'(ct, pbl')
1.102 + | str => error ("specify_additem Frm, Pbl: uncovered case with " ^ str)
1.103 + val (p, pt') = case Generate.generate1 thy arg (Istate_Def.Uistate, ctxt) (p,Pbl) pt of
1.104 + ((p, Pbl), _, _, pt') => (p, pt')
1.105 + | _ => error "specify_additem: uncovered case of Generate.generate1"
1.106 + val pre = Stool.check_preconds thy prls where_ pbl'
1.107 + val pb = foldl and_ (true, map fst pre)
1.108 + val (p_, nxt) =
1.109 + nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.110 + val ppc = if p_= Pbl then pbl' else met
1.111 + in
1.112 + ("ok", ([], [], (pt', (p, p_))))
1.113 + end
1.114 + | Err msg =>
1.115 + let
1.116 + val pre = Stool.check_preconds thy prls where_ pbl
1.117 + val pb = foldl and_ (true, map fst pre)
1.118 + val (p_, nxt) =
1.119 + nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.120 + (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
1.121 + in
1.122 + (msg, ([], [], (pt, (p, p_))))
1.123 + end
1.124 + end
1.125 +\<close> ML \<open>
1.126 +specify_additem: string -> Rule.cterm' -> Calc.T -> string * Chead.calcstate'
1.127 +\<close> ML \<open>
1.128 +\<close> ML \<open>
1.129 +\<close> ML \<open>
1.130 +fun by_tactic (Tactic.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =
1.131 + let (* either """"""""""""""" all empty or complete *)
1.132 + val thy = Celem.assoc_thy dI'
1.133 + val (oris, ctxt) =
1.134 + if dI' = Rule.e_domID orelse pI' = Celem.e_pblID (*andalso? WN110511*)
1.135 + then ([], ContextC.e_ctxt)
1.136 + else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy
1.137 + (* these are deprecated vvvvvvvvvvvvvvvvvvvvvvvvvv*)
1.138 + val (pt, _) = cappend_problem e_ctree [] (Istate_Def.e_istate, ctxt) (fmz, spec')
1.139 + (oris, (dI',pI',mI'), Rule.e_term)
1.140 + val pt = update_loc' pt [] (SOME (Istate_Def.e_istate, ctxt), NONE)
1.141 + in
1.142 + case mI' of
1.143 + ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))
1.144 + | _ => ("ok", ([], [], (pt, ([], Pbl))))
1.145 + end
1.146 + (* ONLY for STARTING modeling phase *)
1.147 + | by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _)) =
1.148 + let
1.149 + val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of
1.150 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>
1.151 + (oris, dI',pI',mI', dI, ctxt)
1.152 + | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"
1.153 + val thy' = if dI = Rule.e_domID then dI' else dI
1.154 + val thy = Celem.assoc_thy thy'
1.155 + val {ppc, prls, where_, ...} = Specify.get_pbt pI'
1.156 + val pre = Stool.check_preconds thy prls where_ pbl
1.157 + val pb = foldl and_ (true, map fst pre)
1.158 + val ((p, _), _, _, pt) =
1.159 + Generate.generate1 thy (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) pos pt
1.160 + val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)
1.161 + (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');
1.162 + in
1.163 + ("ok", ([], [], (pt, (p, Pbl))))
1.164 + end
1.165 + (* called only if no_met is specified *)
1.166 + | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
1.167 + let
1.168 +(* val (dI', ctxt) = case get_obj I pt p of
1.169 + PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)
1.170 + | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)
1.171 + val {met, thy,...} = Specify.get_pbt pIre
1.172 + val (domID, metID) = (Rule.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)
1.173 + val ((p,_), _, _, pt) =
1.174 + Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
1.175 + (Istate_Def.Uistate, ContextC.e_ctxt) pos pt
1.176 +(* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
1.177 +(* val (pbl, pre, _) = ([], [], false)*)
1.178 + in
1.179 + ("ok", ([], [], (pt,(p, Pbl))))
1.180 + end
1.181 + | by_tactic (Tactic.Refine_Problem' rfd) (pt, pos) =
1.182 + let
1.183 + val ctxt = get_ctxt pt pos
1.184 + val (pos, _, _, pt) =
1.185 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
1.186 + (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt
1.187 + in
1.188 + ("ok", ([], [], (pt,pos)))
1.189 + end
1.190 + (*WN110515 initialise ctxt again from itms and add preconds*)
1.191 + | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p,_)) =
1.192 + let
1.193 + val (oris, dI', pI', mI', dI, mI, ctxt, met) = case get_obj I pt p of
1.194 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
1.195 + (oris, dI', pI', mI', dI, mI, ctxt, met)
1.196 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
1.197 + val thy = Celem.assoc_thy dI
1.198 + val (p, pt) =
1.199 + case Generate.generate1 thy (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) pos pt of
1.200 + ((p, Pbl), _, _, pt) => (p, pt)
1.201 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
1.202 + val dI'' = Celem.assoc_thy (if dI = Rule.e_domID then dI' else dI)
1.203 + val mI'' = if mI = Celem.e_metID then mI' else mI
1.204 + val (_, nxt) = Chead.nxt_spec Pbl ok oris (dI', pI', mI') (itms, met) ((#ppc o Specify.get_pbt) pI,
1.205 + (#ppc o Specify.get_met) mI'') (dI, pI, mI);
1.206 + in
1.207 + ("ok", ([], [], (pt, (p, Pbl))))
1.208 + end
1.209 + (*WN110515 initialise ctxt again from itms and add preconds*)
1.210 + | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =
1.211 + let
1.212 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
1.213 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
1.214 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
1.215 + | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
1.216 + val {ppc, pre, prls,...} = Specify.get_met mID
1.217 + val thy = Celem.assoc_thy dI
1.218 + val dI'' = if dI = Rule.e_domID then dI' else dI
1.219 + val pI'' = if pI = Celem.e_pblID then pI' else pI
1.220 + val oris = Specify.add_field' thy ppc oris
1.221 + val met = if met = [] then pbl else met
1.222 + val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls) oris
1.223 + val itms = Specify.hack_until_review_Specify_1 mI' itms
1.224 + val (pos, _, _, pt) =
1.225 + Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt
1.226 + val (_, nxt) = Chead.nxt_spec Met true oris (dI', pI',mI') (pbl, itms)
1.227 + ((#ppc o Specify.get_pbt) pI'', ppc) (dI'', pI'', mID)
1.228 + in
1.229 + ("ok", ([], [], (pt, pos)))
1.230 + end
1.231 + | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p) = specify_additem "#Given" ct (pt, p)
1.232 + | by_tactic (Tactic.Add_Find' (ct, _)) (pt, p) = specify_additem "#Find" ct (pt, p)
1.233 + | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = specify_additem"#Relate" ct (pt, p)
1.234 + | by_tactic (Tactic.Specify_Theory' domID) (pt, pos as (p,p_)) =
1.235 + let
1.236 + val p_ = case p_ of Met => Met | _ => Pbl
1.237 + val thy = Celem.assoc_thy domID
1.238 + val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of
1.239 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>
1.240 + (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)
1.241 + | _ => error "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"
1.242 + val mppc = case p_ of Met => met | _ => pbl
1.243 + val cpI = if pI = Celem.e_pblID then pI' else pI
1.244 + val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI
1.245 + val cmI = if mI = Celem.e_metID then mI' else mI
1.246 + val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI
1.247 + val pre = case p_ of
1.248 + Met => (Stool.check_preconds thy mer mwh met)
1.249 + | _ => (Stool.check_preconds thy per pwh pbl)
1.250 + val pb = foldl and_ (true, map fst pre)
1.251 + in
1.252 + if domID = dI
1.253 + then
1.254 + let val (p_, nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)
1.255 + in
1.256 + ("ok", ([], [], (pt, (p, p_))))
1.257 + end
1.258 + else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
1.259 + let
1.260 + val ((p, p_), _, _, pt) = Generate.generate1 thy (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (p,p_) pt
1.261 + val (p_,nxt) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)
1.262 + in
1.263 + ("ok", ([], [], (pt, (p, p_))))
1.264 + end
1.265 + end
1.266 + | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
1.267 +\<close> ML \<open>
1.268 +\<close> ML \<open>
1.269 +\<close> ML \<open>
1.270 +by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
1.271 +\<close> ML \<open>
1.272 +\<close> ML \<open>
1.273 +\<close> ML \<open>
1.274 +(*-------------------------------------------------------------------------------------------* )
1.275 + | by_tactic m' _ _ _ = error ("specify: not impl. for " ^ Tactic.string_of m')
1.276 +( *-------------------------------------------------------------------------------------------*)
1.277 +\<close> ML \<open>
1.278 +\<close> ML \<open>
1.279 +specify : Tactic.T -> Ctree.pos' -> Ctree.cid -> Ctree.ctree ->
1.280 + Ctree.pos' * (Ctree.pos' * Istate_Def.T) * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
1.281 +\<close> ML \<open>
1.282 +\<close> ML \<open>
1.283 +\<close> ML \<open>
1.284 +\<close> ML \<open>
1.285 +\<close> ML \<open>
1.286 +\<close> ML \<open>
1.287 \<close> ML \<open>
1.288 \<close>
1.289 end