1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu May 05 09:23:32 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu May 05 14:21:54 2011 +0200
1.3 @@ -1087,47 +1087,30 @@
1.4 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
1.5 in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
1.6 end;
1.7 -(* val sel = "#Find"; val (p,_) = p; val Add_Find' ct = nxt;
1.8 - val (_,_,f,nxt',_,pt')= specify_additem sel ct (p,Met) c pt;
1.9 - *)
1.10
1.11 -(* ori
1.12 -val (msg,itm) = appl_add thy sel oris ppc ct;
1.13 -val (Cor(d,ts)) = #5 itm;
1.14 -map (atomty) ts;
1.15 -
1.16 -pre
1.17 -*)
1.18 -
1.19 -
1.20 -(* val Init_Proof' (fmz,(dI',pI',mI')) = m;
1.21 - specify (Init_Proof' (fmz,(dI',pI',mI'))) e_pos' [] EmptyPtree;
1.22 - *)
1.23 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)=
1.24 let (* either """"""""""""""" all empty or complete *)
1.25 val thy = assoc_thy dI';
1.26 - val (oris, ctxt) = if dI' = e_domID orelse pI' = e_pblID then ([], e_ctxt)
1.27 - else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
1.28 + val (oris, ctxt) =
1.29 + if dI' = e_domID orelse pI' = e_pblID
1.30 + then ([], e_ctxt)
1.31 + else pI' |> #ppc o get_pbt |> prep_ori fmz thy;
1.32 val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
1.33 - (oris,(dI',pI',mI'),e_term);
1.34 - val {ppc,prls,where_,...} = get_pbt pI'
1.35 - (*val pbl = init_pbl ppc; WN.9.03: done in Model/Refine_Problem
1.36 - val pt = update_pbl pt [] pbl;
1.37 - val pre = check_preconds thy prls where_ pbl
1.38 - val pb = foldl and_ (true, map fst pre)*)
1.39 + (oris, (dI',pI',mI'),e_term);
1.40 + val {ppc, prls, where_, ...} = get_pbt pI'
1.41 val (pbl, pre, pb) = ([], [], false)
1.42 - in case mI' of
1.43 - ["no_met"] =>
1.44 - (([],Pbl), (([],Pbl),Uistate),
1.45 - Form' (PpcKF (0,EdUndef,(length []),Nundef,
1.46 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.47 - Refine_Tacitly pI', Safe,pt)
1.48 - | _ =>
1.49 - (([],Pbl), (([],Pbl),Uistate),
1.50 - Form' (PpcKF (0,EdUndef,(length []),Nundef,
1.51 - (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.52 - Model_Problem,
1.53 - Safe,pt)
1.54 + in
1.55 + case mI' of
1.56 + ["no_met"] =>
1.57 + (([], Pbl), (([], Pbl), Uistate),
1.58 + Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.59 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.60 + Refine_Tacitly pI', Safe, pt)
1.61 + | _ =>
1.62 + (([], Pbl), (([], Pbl), Uistate),
1.63 + Form' (PpcKF (0, EdUndef, (length []), Nundef,
1.64 + (Problem [], itms2itemppc (assoc_thy dI') pbl pre))),
1.65 + Model_Problem, Safe, pt)
1.66 end
1.67
1.68 (*ONLY for STARTING modeling phase*)
1.69 @@ -1541,53 +1524,61 @@
1.70
1.71 (* create a calc-tree with oris via an cas.refined pbl *)
1.72 fun nxt_specify_init_calc (([], (dI, pI, mI)) : fmz) =
1.73 - if pI <> [] then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.74 - let val {cas, met, ppc, thy, ...} = get_pbt pI
1.75 - val dI = if dI = "" then theory2theory' thy else dI
1.76 - val thy = assoc_thy dI
1.77 - val mI = if mI = [] then hd met else mI
1.78 - val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.79 - val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.80 - ([], (dI,pI,mI), hdl)
1.81 - val pt = update_spec pt [] (dI,pI,mI)
1.82 - val pits = init_pbl' ppc
1.83 - val pt = update_pbl pt [] pits
1.84 - in ((pt, ([] ,Pbl)), []) : calcstate end
1.85 - else if mI <> [] then (* from met-browser *)
1.86 - let val {ppc,...} = get_met mI
1.87 - val dI = if dI = "" then "Isac" else dI
1.88 - val thy = assoc_thy dI;
1.89 - val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.90 - ([], (dI,pI,mI), e_term(*FIXME met*));
1.91 - val pt = update_spec pt [] (dI,pI,mI);
1.92 - val mits = init_pbl' ppc;
1.93 - val pt = update_met pt [] mits;
1.94 - in ((pt, ([], Met)), []) : calcstate end
1.95 - else (* new example, pepare for interactive modeling *)
1.96 - let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.97 - ([], e_spec, e_term)
1.98 - in ((pt,([],Pbl)), []) : calcstate end
1.99 + if pI <> []
1.100 + then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
1.101 + let
1.102 + val {cas, met, ppc, thy, ...} = get_pbt pI
1.103 + val dI = if dI = "" then theory2theory' thy else dI
1.104 + val thy = assoc_thy dI
1.105 + val mI = if mI = [] then hd met else mI
1.106 + val hdl = case cas of NONE => pblterm dI pI | SOME t => t
1.107 + val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
1.108 + ([], (dI,pI,mI), hdl)
1.109 + val pt = update_spec pt [] (dI,pI,mI)
1.110 + val pits = init_pbl' ppc
1.111 + val pt = update_pbl pt [] pits
1.112 + in ((pt, ([] ,Pbl)), []) : calcstate end
1.113 + else
1.114 + if mI <> []
1.115 + then (* from met-browser *)
1.116 + let
1.117 + val {ppc,...} = get_met mI
1.118 + val dI = if dI = "" then "Isac" else dI
1.119 + val thy = assoc_thy dI;
1.120 + val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
1.121 + ([], (dI,pI,mI), e_term(*FIXME met*));
1.122 + val pt = update_spec pt [] (dI,pI,mI);
1.123 + val mits = init_pbl' ppc;
1.124 + val pt = update_met pt [] mits;
1.125 + in ((pt, ([], Met)), []) : calcstate end
1.126 + else (* new example, pepare for interactive modeling *)
1.127 + let val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], e_spec)
1.128 + ([], e_spec, e_term)
1.129 + in ((pt, ([], Pbl)), []) : calcstate end
1.130 +
1.131 | nxt_specify_init_calc (fmz : fmz_, (dI, pI, mI) : spec) =
1.132 - let (* both """"""""""""""""""""""""" either empty or complete *)
1.133 - val thy = assoc_thy dI
1.134 - val (pI, (pors, pctxt), mI) =
1.135 - if mI = ["no_met"]
1.136 - then let val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1.137 - val pI' = refine_ori' pors pI;
1.138 - in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1.139 - (hd o #met o get_pbt) pI') end
1.140 - else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.141 - val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.142 - val dI = theory2theory' (maxthy thy thy');
1.143 - val hdl = case cas of
1.144 - NONE => pblterm dI pI
1.145 - | SOME t => subst_atomic ((vars_of_pbl_' ppc)
1.146 - ~~~ vals_of_oris pors) t;
1.147 + let (* both """"""""""""""""""""""""" either empty or complete *)
1.148 + val thy = assoc_thy dI
1.149 + val (pI, (pors, pctxt), mI) =
1.150 + if mI = ["no_met"]
1.151 + then
1.152 + let
1.153 + val (pors, pctxt) = get_pbt pI |> #ppc |> prep_ori fmz thy;
1.154 + val pI' = refine_ori' pors pI;
1.155 + in (pI', (pors(*refinement over models with diff.precond only*), pctxt),
1.156 + (hd o #met o get_pbt) pI') end
1.157 + else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy, mI)
1.158 + val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
1.159 + val dI = theory2theory' (maxthy thy thy');
1.160 + val hdl =
1.161 + case cas of
1.162 + NONE => pblterm dI pI
1.163 + | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t;
1.164 val (pt, _) = cappend_problem e_ptree [] (e_istate, pctxt) (fmz, (dI, pI, mI))
1.165 - (pors, (dI, pI, mI), hdl)
1.166 - in ((pt, ([], Pbl)),
1.167 + (pors, (dI, pI, mI), hdl)
1.168 + in ((pt, ([], Pbl)),
1.169 fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
1.170 - end;
1.171 + end;
1.172
1.173
1.174
1.175 @@ -1776,33 +1767,33 @@
1.176 (*.complete _EMPTY_ calc-head for autocalc (sub-)pbl from oris(+met from fmz);
1.177 oris and spec (incl. pbl-refinement) given from init_calc or SubProblem .*)
1.178 fun all_modspec (pt, (p,_):pos') =
1.179 -(* val (pt, (p,_)) = ptp;
1.180 - *)
1.181 - let val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1.182 - ...}) = get_obj I pt p;
1.183 - val thy = assoc_thy dI;
1.184 - val {ppc,...} = get_met mI;
1.185 - val mors = prep_ori fmz_ thy ppc |> #1;
1.186 - val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.187 - val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.188 - val pt = update_spec pt p (dI,pI,mI);
1.189 - in (pt, (p,Met): pos') end;
1.190 + let
1.191 + val (PblObj{fmz=(fmz_,_), origin=(pors, spec as (dI,pI,mI), hdl),
1.192 + ...}) = get_obj I pt p;
1.193 + val thy = assoc_thy dI;
1.194 + val {ppc,...} = get_met mI;
1.195 + val mors = prep_ori fmz_ thy ppc |> #1;
1.196 + val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
1.197 + val pt = update_metppc pt p (map (ori2Coritm ppc) mors);
1.198 + val pt = update_spec pt p (dI,pI,mI);
1.199 + in (pt, (p,Met): pos') end;
1.200
1.201 (*WN.12.03: use in nxt_spec, too ? what about variants ???*)
1.202 fun is_complete_mod_ ([]: itm list) = false
1.203 | is_complete_mod_ itms =
1.204 foldl and_ (true, (map #3 itms));
1.205 +
1.206 fun is_complete_mod (pt, pos as (p, Pbl): pos') =
1.207 - if (is_pblobj o (get_obj I pt)) p
1.208 - then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.209 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.210 + if (is_pblobj o (get_obj I pt)) p
1.211 + then (is_complete_mod_ o (get_obj g_pbl pt)) p
1.212 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.213 | is_complete_mod (pt, pos as (p, Met)) =
1.214 - if (is_pblobj o (get_obj I pt)) p
1.215 - then (is_complete_mod_ o (get_obj g_met pt)) p
1.216 - else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.217 + if (is_pblobj o (get_obj I pt)) p
1.218 + then (is_complete_mod_ o (get_obj g_met pt)) p
1.219 + else error ("is_complete_mod: called by PrfObj at "^pos'2str pos)
1.220 | is_complete_mod (_, pos) =
1.221 - error ("is_complete_mod called by "^pos'2str pos^
1.222 - " (should be Pbl or Met)");
1.223 + error ("is_complete_mod called by " ^ pos'2str pos ^
1.224 + " (should be Pbl or Met)");
1.225
1.226 (*.have (thy, pbl, met) _all_ been specified explicitly ?.*)
1.227 fun is_complete_spec (pt, pos as (p,_): pos') =