intermed. ctxt over all minisubpbl x+1=2
overview in test:
--- all handling ctxt in minimsubpbl x+1=2 ---
ctxt initialised in prep_ori; the latter is
* not handled correctly in input_icalhd, match_pbl, refin'
* still unclear for subproblems in script
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') =
2.1 --- a/src/Tools/isac/Interpret/inform.sml Thu May 05 09:23:32 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/inform.sml Thu May 05 14:21:54 2011 +0200
2.3 @@ -395,79 +395,57 @@
2.4 "): Par should be internal");
2.5
2.6 fun imodel2fstr iitems =
2.7 - let fun xxx is [] = is
2.8 - | xxx is ((Given strs)::iis) =
2.9 - xxx (is @ (map (pair "#Given") strs)) iis
2.10 - | xxx is ((Find strs)::iis) =
2.11 - xxx (is @ (map (pair "#Find") strs)) iis
2.12 - | xxx is ((Relate strs)::iis) =
2.13 - xxx (is @ (map (pair "#Relate") strs)) iis
2.14 - in xxx [] iitems end;
2.15 + let
2.16 + fun xxx is [] = is
2.17 + | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
2.18 + | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
2.19 + | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
2.20 + in xxx [] iitems end;
2.21
2.22 -(*.input a CAS-command via a whole calchead;
2.23 - dWN0602 ropped due to change of design in the front-end.*)
2.24 -(*since previous calc-head _only_ has changed:
2.25 - EITHER _1_ part of the specification OR some items in the model;
2.26 - the hdform is left as is except in cas_input .*)
2.27 -(*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*)
2.28 -(* val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
2.29 - (p, "xxx", empty_model, Pbl, e_spec);
2.30 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
2.31 - (p,"", [Given ["fixedValues [r=Arbfix]"],
2.32 - Find ["maximum A", "valuesFor [a,b]"],
2.33 - Relate ["relations [A=a*b, a/2=r*sin alpha, \
2.34 - \b/2=r*cos alpha]"]], Pbl, e_spec);
2.35 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) =
2.36 - (([],Pbl), "not used here",
2.37 - [Given ["fixedValues [r=Arbfix]"],
2.38 - Find ["maximum A", "valuesFor [a,b]"(*new input*)],
2.39 - Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl,
2.40 - ("DiffApp", ["e_pblID"], ["e_metID"]));
2.41 - val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd;
2.42 - *)
2.43 +(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
2.44 fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) =
2.45 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
2.46 - spec = sspec as (sdI,spI,smI), probl, meth,...} =
2.47 - get_obj I pt p;
2.48 + spec = sspec as (sdI,spI,smI), probl, meth,...} = get_obj I pt p;
2.49 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
2.50 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
2.51 - let val (pos_, pits, mits) =
2.52 - if dI <> sdI
2.53 - then let val its = map (parsitm (assoc_thy dI)) probl;
2.54 - val (its, trms) = filter_sep is_Par its;
2.55 - val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
2.56 - in (Pbl, appl_adds dI oris its pbt
2.57 - (map par2fstr trms), meth) end else
2.58 - if pI <> spI
2.59 - then if pI = snd3 ospec then (Pbl, probl, meth) else
2.60 - let val pbt = (#ppc o get_pbt) pI
2.61 - val dI' = #1 (some_spec ospec spec)
2.62 - val oris = if pI = #2 ospec then oris
2.63 - else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
2.64 - in (Pbl, appl_adds dI' oris probl pbt
2.65 - (map itms2fstr probl), meth) end else
2.66 - if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
2.67 - then let val met = (#ppc o get_met) mI
2.68 - val mits = complete_metitms oris probl meth met
2.69 - in if foldl and_ (true, map #3 mits)
2.70 - then (Pbl, probl, mits) else (Met, probl, mits)
2.71 - end else
2.72 - (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
2.73 - ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
2.74 - (imodel2fstr imodel), meth);
2.75 - val pt = update_spec pt p spec;
2.76 - in if pos_ = Pbl
2.77 - then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2.78 - val pre =check_preconds(assoc_thy"Isac")prls where_ pits
2.79 - in (update_pbl pt p pits,
2.80 - (ocalhd_complete pits pre spec,
2.81 - Pbl, hdf', pits, pre, spec):ocalhd) end
2.82 - else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2.83 - val pre = check_preconds (assoc_thy"Isac") prls pre mits
2.84 - in (update_met pt p mits,
2.85 - (ocalhd_complete mits pre spec,
2.86 - Met, hdf', mits, pre, spec):ocalhd) end
2.87 - end end
2.88 + let val (pos_, pits, mits) =
2.89 + if dI <> sdI
2.90 + then let val its = map (parsitm (assoc_thy dI)) probl;
2.91 + val (its, trms) = filter_sep is_Par its;
2.92 + val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec));
2.93 + in (Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
2.94 + else if pI <> spI
2.95 + then if pI = snd3 ospec then (Pbl, probl, meth)
2.96 + else
2.97 + let val pbt = (#ppc o get_pbt) pI
2.98 + val dI' = #1 (some_spec ospec spec)
2.99 + val oris = if pI = #2 ospec then oris
2.100 + else prep_ori fmz_(assoc_thy"Isac") pbt |> #1;
2.101 + in (Pbl, appl_adds dI' oris probl pbt
2.102 + (map itms2fstr probl), meth) end
2.103 + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
2.104 + then let val met = (#ppc o get_met) mI
2.105 + val mits = complete_metitms oris probl meth met
2.106 + in if foldl and_ (true, map #3 mits)
2.107 + then (Pbl, probl, mits) else (Met, probl, mits)
2.108 + end
2.109 + else (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)]
2.110 + ((#ppc o get_pbt) (#2 (some_spec ospec spec)))
2.111 + (imodel2fstr imodel), meth);
2.112 + val pt = update_spec pt p spec;
2.113 + in if pos_ = Pbl
2.114 + then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec))
2.115 + val pre =check_preconds(assoc_thy"Isac")prls where_ pits
2.116 + in (update_pbl pt p pits,
2.117 + (ocalhd_complete pits pre spec, Pbl, hdf', pits, pre, spec):ocalhd)
2.118 + end
2.119 + else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec))
2.120 + val pre = check_preconds (assoc_thy"Isac") prls pre mits
2.121 + in (update_met pt p mits,
2.122 + (ocalhd_complete mits pre spec, Met, hdf', mits, pre, spec):ocalhd)
2.123 + end
2.124 + end
2.125 + end
2.126 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
2.127 error "input_icalhd Met not impl.";
2.128
3.1 --- a/src/Tools/isac/Interpret/ptyps.sml Thu May 05 09:23:32 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu May 05 14:21:54 2011 +0200
3.3 @@ -82,21 +82,14 @@
3.4 fun add_where ({Given=gi,Find=fi,With=wi,Relate=re,...}:'a ppc) wh =
3.5 ({Given=gi,Where=wh,Find=fi,With=wi,Relate=re}:'a ppc);
3.6
3.7 -(*-----------------------------------------^^^-(2) aus modspec.sml 23.3.02*)
3.8 -
3.9 -
3.10 -(*-----------------------------------------vvv-(3) aus modspec.sml 23.3.02*)
3.11 -
3.12 -
3.13 -
3.14 (*decompose a problem-type into description and identifier
3.15 FIXME split_dsc: no term list !!! (just for quick redoing prep_ori) *)
3.16 fun split_dsc thy t =
3.17 (let val (hd,args) = strip_comb t
3.18 - in if is_dsc hd
3.19 - then (hd, args)
3.20 - else (e_term, [t]) (*??? 9.01 just copied*)
3.21 - end)
3.22 + in if is_dsc hd
3.23 + then (hd, args)
3.24 + else (e_term, [t]) (*??? 9.01 just copied*)
3.25 + end)
3.26 handle _ => error ("split_dsc: called with " ^ term2str t);
3.27 (*
3.28 > val t1 = (term_of o the o (parse thy)) "errorBound err_";
4.1 --- a/test/Tools/isac/Interpret/mstools.sml Thu May 05 09:23:32 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/mstools.sml Thu May 05 14:21:54 2011 +0200
4.3 @@ -11,6 +11,7 @@
4.4 "----------- fun declare_constraints --------------------";
4.5 "----------- fun get_assumptions, fun get_environments --";
4.6 "----------- fun transfer_from_subproblem ---------------";
4.7 +"----------- all handling ctxt in minimsubpbl x+1=2 ----";
4.8 "--------------------------------------------------------";
4.9 "--------------------------------------------------------";
4.10 "--------------------------------------------------------";
4.11 @@ -58,3 +59,9 @@
4.12 if get_assumptions ctxt' = [@{term "x ~= 0"}, @{term "x * v"}, @{term "2 * u"}]
4.13 then () else error "mstools.sml transfer_from_subproblem changed."
4.14
4.15 +
4.16 +"----------- all handling ctxt in minimsubpbl x+1=2 ----";
4.17 +"----------- all handling ctxt in minimsubpbl x+1=2 ----";
4.18 +"----------- all handling ctxt in minimsubpbl x+1=2 ----";
4.19 +
4.20 +
5.1 --- a/test/Tools/isac/Test_Isac.thy Thu May 05 09:23:32 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Thu May 05 14:21:54 2011 +0200
5.3 @@ -148,6 +148,44 @@
5.4 Model_Problem';
5.5 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
5.6 *}
5.7 +ML {*
5.8 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
5.9 +val (dI',pI',mI') =
5.10 + ("Test", ["sqroot-test","univariate","equation","test"],
5.11 + ["Test","squ-equ-test-subpbl1"]);
5.12 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.13 +(*nxt = Model_Problem*)
5.14 +print_depth 999; pt;
5.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.16 +(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
5.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.21 +(*nxt = Specify_Problem*)
5.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.23 +(* check precond_root_1, precond_root_2 in root-ctxt *)
5.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.25 +(*nxt = Apply_Method*)
5.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.27 +(*check precond_root_1, precond_root_2 in sub-ctxt *)
5.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.30 +*}
5.31 +ML {*
5.32 +(*nxt = Subproblem*)
5.33 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.34 +*}
5.35 +ML {*
5.36 +(*nxt = Model_Problem*)
5.37 +print_depth 999; pt;
5.38 +*}
5.39 +ML {*
5.40 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.41 +(*check parseNEW ctxt "x+y+z" --real, "a+b+c" --'a *)
5.42 +(*nxt = ERROR*)
5.43 +*}
5.44 +
5.45 use "Interpret/mstools.sml" (*new 2010*)
5.46 use "Interpret/ctree.sml" (*!...see(25)*)
5.47 use "Interpret/ptyps.sml" (* *)