1.1 --- a/src/Tools/isac/Interpret/appl.sml Wed May 04 14:07:51 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Thu May 05 09:23:32 2011 +0200
1.3 @@ -221,36 +221,32 @@
1.4 tests for applicability are so expensive, that results (rewrites!)
1.5 are kept in the return-value of 'type tac_'.
1.6 .*)
1.7 -fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) =
1.8 - Appl (Init_Proof' (ct', spec))
1.9 +fun applicable_in (_:pos') _ (Init_Proof (ct', spec)) = Appl (Init_Proof' (ct', spec))
1.10
1.11 | applicable_in (p,p_) pt Model_Problem =
1.12 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.13 - then Notappl ((tac2str Model_Problem)^
1.14 - " not for pos "^(pos'2str (p,p_)))
1.15 - else let val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
1.16 - val {ppc,...} = get_pbt pI'
1.17 - val pbl = init_pbl ppc
1.18 - in Appl (Model_Problem' (pI', pbl, [])) end
1.19 -(* val Refine_Tacitly pI = m;
1.20 - *)
1.21 + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.22 + then Notappl ((tac2str Model_Problem) ^ " not for pos " ^ (pos'2str (p,p_)))
1.23 + else
1.24 + let
1.25 + val (PblObj{origin=(_,(_,pI',_),_),...}) = get_obj I pt p
1.26 + val {ppc,...} = get_pbt pI'
1.27 + val pbl = init_pbl ppc
1.28 + in Appl (Model_Problem' (pI', pbl, [])) end
1.29 +
1.30 | applicable_in (p,p_) pt (Refine_Tacitly pI) =
1.31 - if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.32 - then Notappl ((tac2str (Refine_Tacitly pI))^
1.33 - " not for pos "^(pos'2str (p,p_)))
1.34 - else (* val Refine_Tacitly pI = m;
1.35 - *)
1.36 - let val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
1.37 - val opt = refine_ori oris pI;
1.38 - in case opt of
1.39 - SOME pblID =>
1.40 - Appl (Refine_Tacitly' (pI, pblID,
1.41 - e_domID, e_metID, [](*filled in specify*)))
1.42 - | NONE => Notappl ((tac2str (Refine_Tacitly pI))^
1.43 - " not applicable") end
1.44 -(* val (p,p_) = ip;
1.45 - val Refine_Problem pI = m;
1.46 - *)
1.47 + if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.48 + then Notappl ((tac2str (Refine_Tacitly pI)) ^ " not for pos " ^ (pos'2str (p,p_)))
1.49 + else
1.50 + let
1.51 + val (PblObj {origin = (oris, (dI',_,_),_), ...}) = get_obj I pt p;
1.52 + val opt = refine_ori oris pI;
1.53 + in case opt of
1.54 + SOME pblID =>
1.55 + Appl (Refine_Tacitly' (pI, pblID,
1.56 + e_domID, e_metID, [](*filled in specify*)))
1.57 + | NONE => Notappl ((tac2str (Refine_Tacitly pI)) ^ " not applicable")
1.58 + end
1.59 +
1.60 | applicable_in (p,p_) pt (Refine_Problem pI) =
1.61 if not (is_pblobj (get_obj I pt p)) orelse p_ = Res
1.62 then Notappl ((tac2str (Refine_Problem pI))^
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 04 14:07:51 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu May 05 09:23:32 2011 +0200
2.3 @@ -1129,27 +1129,26 @@
2.4 Model_Problem,
2.5 Safe,pt)
2.6 end
2.7 - (*ONLY for STARTING modeling phase*)
2.8 +
2.9 + (*ONLY for STARTING modeling phase*)
2.10 | specify (Model_Problem' (_,pbl,met)) (pos as (p,p_)) c pt =
2.11 - let (* val (Model_Problem' (_,pbl), pos as (p,p_)) = (m, (p,p_));
2.12 - *)
2.13 - val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) =
2.14 - get_obj I pt p
2.15 - val thy' = if dI = e_domID then dI' else dI
2.16 - val thy = assoc_thy thy'
2.17 - val {ppc,prls,where_,...} = get_pbt pI'
2.18 - val pre = check_preconds thy prls where_ pbl
2.19 - val pb = foldl and_ (true, map fst pre)
2.20 - val ((p,_),_,_,pt) =
2.21 - generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
2.22 - val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
2.23 - (ppc,(#ppc o get_met) mI') (dI',pI',mI');
2.24 - in ((p,Pbl), ((p,p_),Uistate),
2.25 - Form' (PpcKF (0,EdUndef,(length p),Nundef,
2.26 - (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
2.27 - nxt, Safe, pt) end
2.28 + let
2.29 + val (PblObj{origin=(oris,(dI',pI',mI'),_), spec=(dI,_,_),...}) = get_obj I pt p
2.30 + val thy' = if dI = e_domID then dI' else dI
2.31 + val thy = assoc_thy thy'
2.32 + val {ppc,prls,where_,...} = get_pbt pI'
2.33 + val pre = check_preconds thy prls where_ pbl
2.34 + val pb = foldl and_ (true, map fst pre)
2.35 + val ((p,_),_,_,pt) = generate1 thy (Model_Problem'([],pbl,met)) (Uistate, e_ctxt) pos pt
2.36 + val (_,nxt) = nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met)
2.37 + (ppc,(#ppc o get_met) mI') (dI',pI',mI');
2.38 + in ((p, Pbl), ((p, p_), Uistate),
2.39 + Form' (PpcKF (0, EdUndef, length p, Nundef,
2.40 + (Problem pI', itms2itemppc (assoc_thy dI') pbl pre))),
2.41 + nxt, Safe, pt)
2.42 + end
2.43
2.44 -(*. called only if no_met is specified .*)
2.45 + (*. called only if no_met is specified .*)
2.46 | specify (Refine_Tacitly' (pI,pIre,_,_,_)) (pos as (p,_)) c pt =
2.47 let (* val Refine_Tacitly' (pI,pIre,_,_,_) = m;
2.48 *)
2.49 @@ -1429,20 +1428,19 @@
2.50 val pbl = init_pbl ppc (* fill in descriptions *)
2.51 (*----------------if you think, this should be done by the Dialog
2.52 in the java front-end, search there for WN060225-modelProblem----*)
2.53 - val (pbl, met) = case cas of NONE => (pbl, [])
2.54 - | _ => complete_mod_ (oris, mpc, ppc, probl)
2.55 + val (pbl, met) =
2.56 + case cas of NONE => (pbl, [])
2.57 + | _ => complete_mod_ (oris, mpc, ppc, probl)
2.58 (*----------------------------------------------------------------*)
2.59 val tac_ = Model_Problem' (pI, pbl, met)
2.60 val (pos,c,_,pt) = generate1 thy tac_ (Uistate, e_ctxt) pos pt
2.61 in ([(tac,tac_, (pos, (Uistate, e_ctxt)))], c, (pt,pos)):calcstate' end
2.62
2.63 -(* val Add_Find ct = tac;
2.64 - *)
2.65 | nxt_specif (Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp
2.66 | nxt_specif (Add_Find ct) ptp = nxt_specif_additem "#Find" ct ptp
2.67 | nxt_specif (Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp
2.68
2.69 -(*. called only if no_met is specified .*)
2.70 + (*. called only if no_met is specified .*)
2.71 | nxt_specif (Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =
2.72 let val (PblObj {origin = (oris, (dI,_,_),_), ...}) = get_obj I pt p
2.73 val opt = refine_ori oris pI
3.1 --- a/src/Tools/isac/Interpret/ctree.sml Wed May 04 14:07:51 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/ctree.sml Thu May 05 09:23:32 2011 +0200
3.3 @@ -727,36 +727,33 @@
3.4 val empty_envp = ([],[],[],[]):envp;
3.5
3.6 datatype ppobj =
3.7 - PrfObj of {cell : lrd option, (*where in form tac has been applied*)
3.8 - (*^^^FIXME.WN0607 rename this field*)
3.9 - form : term,
3.10 - tac : tac, (* also in istate*)
3.11 - loc : (istate * Proof.context) option * (istate * Proof.context) option, (*for form, result
3.12 -13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
3.13 - branch: branch,
3.14 - result: term * term list,
3.15 - ostate: ostate} (*Complete <=> result is OK*)
3.16 - | PblObj of {cell : lrd option,(*unused: meaningful only for some _Prf_Obj*)
3.17 - fmz : fmz, (*from init:FIXME never use this spec;-drop*)
3.18 - origin: (ori list) * (*representation from fmz+pbt
3.19 - for efficiently adding items in probl, meth*)
3.20 - spec * (*updated by Refine_Tacitly*)
3.21 - term, (*headline of calc-head, as calculated
3.22 - initially(!)*)
3.23 - (*# the origin of a root-pbl is created from fmz
3.24 - (thus providing help for input to the user),
3.25 - # the origin of a sub-pbl is created from the argument
3.26 - -list of a script-tac 'SubProblem (spec) [arg-list]'
3.27 - by 'match_ags'*)
3.28 - spec : spec, (*explicitly input*)
3.29 - probl : itm list, (*itms explicitly input*)
3.30 - meth : itm list, (*itms automatically added to copy of probl
3.31 - TODO: input like to 'probl'*)
3.32 - env : (istate * Proof.context) option,(*for problem with initac in script*)
3.33 - loc : (istate * Proof.context) option * (istate * Proof.context) option, (*for pbl+met * result*)
3.34 - branch: branch,
3.35 - result: term * term list,
3.36 - ostate: ostate}; (*Complete <=> result is _proven_ OK*)
3.37 + PrfObj of
3.38 + {cell : lrd option, (* where in form tac has been applied *)
3.39 + (*^^^FIXME.WN0607 rename this field*)
3.40 + form : term, (* where tac is applied to *)
3.41 + tac : tac, (* also in istate *)
3.42 + loc : (istate * Proof.context) option * (istate * Proof.context) option,
3.43 + (*for form, result 13.8.02: (NONE,NONE) <==> e_istate ! see update_loc, get_loc*)
3.44 + branch: branch, (* only rudimentary *)
3.45 + result: term * term list, (* result and assumptions *)
3.46 + ostate: ostate} (* Complete <=> result is OK *)
3.47 + | PblObj of
3.48 + {cell : lrd option, (* unused: meaningful only for some _Prf_Obj *)
3.49 + fmz : fmz, (* from init:FIXME never use this spec;-drop *)
3.50 + origin: (ori list) * (* representation from fmz+pbt
3.51 + for efficiently adding items in probl, meth *)
3.52 + spec * (* updated by Refine_Tacitly *)
3.53 + term, (* headline of calc-head, as calculated initially(!)*)
3.54 + spec : spec, (* explicitly input *)
3.55 + probl : itm list, (* itms explicitly input *)
3.56 + meth : itm list, (* itms automatically added to copy of probl *)
3.57 + env : (istate * Proof.context) option,
3.58 + (* for problem with initac in script*)
3.59 + loc : (istate * Proof.context) option * (istate * Proof.context) option,
3.60 + (* for pbl+met * result *)
3.61 + branch: branch, (* only rudimentary *)
3.62 + result: term * term list, (* result and assumptions *)
3.63 + ostate: ostate}; (* Complete <=> result is _proven_ OK *)
3.64
3.65 (*.this tree contains isac's calculations; TODO.WN03 rename to ctree;
3.66 the structure has been copied from an early version of Theorema(c);
4.1 --- a/src/Tools/isac/Interpret/generate.sml Wed May 04 14:07:51 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/generate.sml Thu May 05 09:23:32 2011 +0200
4.3 @@ -295,12 +295,11 @@
4.4 pt) end
4.5
4.6 | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
4.7 -(* val (itms,pos as (p,_)) = (pbl, pos);
4.8 - *)
4.9 - let val pt = update_pbl pt p itms
4.10 - val pt = update_met pt p met
4.11 - in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,
4.12 - (Upblmet,itms2itemppc thy [][]))), pt) end
4.13 + let
4.14 + val pt = update_pbl pt p itms
4.15 + val pt = update_met pt p met
4.16 + in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
4.17 + end
4.18
4.19 | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl))
4.20 _ (pos as (p,_)) pt =
5.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed May 04 14:07:51 2011 +0200
5.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu May 05 09:23:32 2011 +0200
5.3 @@ -111,29 +111,23 @@
5.4 (*. locate a tactic in a script and apply it if possible .*)
5.5 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
5.6 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
5.7 -(* val ptp as (pt, p) = (pt, p);
5.8 - val ptp as (pt, p) = (pt, ip);
5.9 - *)
5.10 | locatetac tac (ptp as (pt, p)) =
5.11 - let val (mI,m) = mk_tac'_ tac;
5.12 - in case applicable_in p pt m of
5.13 - Notappl e => ("not-applicable", ([],[], ptp):calcstate')
5.14 - | Appl m =>
5.15 -(* val Appl m = applicable_in p pt m;
5.16 - *)
5.17 - let val x = if member op = specsteps mI
5.18 - then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
5.19 - in case x of
5.20 - ERror e => ("failure", ([], [], ptp))
5.21 - (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
5.22 - | UNsafe cs' => ("unsafe-ok", cs')
5.23 - | Updated (cs' as (_,_,(_,p'))) =>
5.24 - (*ev.SEVER.tacs like Begin_Trans*)
5.25 - (if p' = ([],Res) then "end-of-calculation" else "ok",
5.26 - cs')(*for -"- user to ask ? *)
5.27 - end
5.28 - end;
5.29 -
5.30 + let val (mI,m) = mk_tac'_ tac;
5.31 + in case applicable_in p pt m of
5.32 + Notappl e => ("not-applicable", ([],[], ptp):calcstate')
5.33 + | Appl m =>
5.34 + let
5.35 + val x = if member op = specsteps mI
5.36 + then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
5.37 + in case x of
5.38 + ERror e => ("failure", ([], [], ptp))
5.39 + (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
5.40 + | UNsafe cs' => ("unsafe-ok", cs')
5.41 + | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
5.42 + (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
5.43 + (*for SEVER.tacs user to ask ? *)
5.44 + end
5.45 + end;
5.46
5.47 (*------------------------------------------------------------------
5.48 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
6.1 --- a/src/Tools/isac/Interpret/ptyps.sml Wed May 04 14:07:51 2011 +0200
6.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu May 05 09:23:32 2011 +0200
6.3 @@ -289,8 +289,6 @@
6.4 |> map flattup;
6.5 in (oris, ctxt) end;
6.6
6.7 -(*-----------------------------------------^^^-(4) aus modspec.sml 23.3.02*)
6.8 -
6.9 (*.the pattern for an item of a problems model or a methods guard.*)
6.10 type pat = (string * (*field*)
6.11 (term * (*description*)
7.1 --- a/src/Tools/isac/Interpret/solve.sml Wed May 04 14:07:51 2011 +0200
7.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu May 05 09:23:32 2011 +0200
7.3 @@ -184,67 +184,52 @@
7.4 end
7.5
7.6 | solve ("Free_Solve", Free_Solve') (pt,po as (p,_)) =
7.7 - let (*val _=tracing"###solve Free_Solve";*)
7.8 - val p' = lev_dn_ (p,Res);
7.9 - val pt = update_metID pt (par_pblobj pt p) e_metID;
7.10 - in ("ok", ((*(p',Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Unsafe,*)
7.11 - [(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p'))) end
7.12 + let (*val _=tracing"###solve Free_Solve";*)
7.13 + val p' = lev_dn_ (p,Res);
7.14 + val pt = update_metID pt (par_pblobj pt p) e_metID;
7.15 + in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))
7.16 + end
7.17
7.18 -(* val (("Check_Postcond",Check_Postcond' (pI,_)), (pt,(pos as (p,p_)))) =
7.19 - ( m, (pt, pos));
7.20 - *)
7.21 | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
7.22 - let (*val _=tracing"###solve Check_Postcond";*)
7.23 - val pp = par_pblobj pt p
7.24 - val asm = (case get_obj g_tac pt p of
7.25 - Check_elementwise _ => (*collects and instantiates asms*)
7.26 - (snd o (get_obj g_result pt)) p
7.27 - | _ => get_assumptions_ pt (p,p_))
7.28 - handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
7.29 - val metID = get_obj g_metID pt pp;
7.30 - val {srls=srls,scr=sc,...} = get_met metID;
7.31 - val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
7.32 - (*val _= tracing("### solve Check_postc, subpbl pos= "^(pos'2str (p,p_)));
7.33 - val _= tracing("### solve Check_postc, is= "^(istate2str is));*)
7.34 - val thy' = get_obj g_domID pt pp;
7.35 - val thy = assoc_thy thy';
7.36 - val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
7.37 - (*val _= tracing("### solve Check_postc, scval= "^(term2str scval));*)
7.38 + let (*val _=tracing"###solve Check_Postcond";*)
7.39 + val pp = par_pblobj pt p
7.40 + val asm =
7.41 + (case get_obj g_tac pt p of
7.42 + Check_elementwise _ => (*collects and instantiates asms*)
7.43 + (snd o (get_obj g_result pt)) p
7.44 + | _ => get_assumptions_ pt (p,p_))
7.45 + handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
7.46 + val metID = get_obj g_metID pt pp;
7.47 + val {srls=srls,scr=sc,...} = get_met metID;
7.48 + val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
7.49 + val thy' = get_obj g_domID pt pp;
7.50 + val thy = assoc_thy thy';
7.51 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
7.52 + in
7.53 + if pp = []
7.54 + then
7.55 + let
7.56 + val is = ScrState (E,l,a,scval,scsaf,b)
7.57 + val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
7.58 + val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
7.59 + in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
7.60 + else
7.61 + let (*resume script of parpbl, transfer value of subpbl-script*)
7.62 + val ppp = par_pblobj pt (lev_up p);
7.63 + val thy' = get_obj g_domID pt ppp;
7.64 + val thy = assoc_thy thy';
7.65 + val metID = get_obj g_metID pt ppp;
7.66 + val sc = (#scr o get_met) metID;
7.67 + val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
7.68 + val ctxt'' = transfer_from_subproblem ctxt ctxt'
7.69 + val ((p,p_),ps,f,pt) =
7.70 + generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
7.71 + (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
7.72 + in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
7.73 + ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
7.74 + end
7.75 + end
7.76
7.77 - in if pp = [] then
7.78 - let val is = ScrState (E,l,a,scval,scsaf,b)
7.79 - val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
7.80 - val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
7.81 - in ("ok", ((*(([],Res),is,End_Proof''), f, End_Proof', scsaf,*)
7.82 - [(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
7.83 - else
7.84 - let
7.85 - (*resume script of parpbl, transfer value of subpbl-script*)
7.86 - val ppp = par_pblobj pt (lev_up p);
7.87 - val thy' = get_obj g_domID pt ppp;
7.88 - val thy = assoc_thy thy';
7.89 - val metID = get_obj g_metID pt ppp;
7.90 - val sc = (#scr o get_met) metID;
7.91 - val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm);
7.92 - val ctxt'' = transfer_from_subproblem ctxt ctxt'
7.93 - val ((p,p_),ps,f,pt) =
7.94 - generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
7.95 - (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
7.96 - in ("ok",(*((pp,Res),is',nx), f, tac_2tac nx, scsaf,*)
7.97 - ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
7.98 - ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
7.99 - end
7.100 - end
7.101 -(* val (msg, cs') =
7.102 - ("ok",([(Check_Postcond pI,Check_Postcond'(pI, (scval, map term2str asm))),
7.103 - ((pp,Res),(ScrState (E,l,a,scval,scsaf,b)))], (pt,(p,p_))));
7.104 - val (_,(pt',p')) = cs';
7.105 - (tracing o istate2str) (get_istate pt' p');
7.106 - (term2str o fst) (get_obj g_result pt' (fst p'));
7.107 - *)
7.108 -
7.109 -(* tracing(istate2str(get_istate pt (p,p_)));
7.110 - *)
7.111 | solve (_,End_Proof'') (pt, (p,p_)) =
7.112 ("end-proof",
7.113 ((*(([],Res),Uistate,Empty_Tac_), EmptyMout, Empty_Tac, Safe,*)
8.1 --- a/test/Tools/isac/Interpret/appl.sml Wed May 04 14:07:51 2011 +0200
8.2 +++ b/test/Tools/isac/Interpret/appl.sml Thu May 05 09:23:32 2011 +0200
8.3 @@ -41,7 +41,45 @@
8.4 (*TODO.WN110416 read pres from ctxt and check*)
8.5
8.6 (*========== inhibit exn 110415 ================================================
8.7 -
8.8 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
8.9 show_pt pt;
8.10 ============ inhibit exn 110415 ==============================================*)
8.11 +
8.12 +
8.13 +
8.14 +
8.15 +
8.16 +
8.17 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
8.18 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
8.19 +val pIopt = get_pblID (pt,ip);
8.20 +tacis; (*= []*)
8.21 +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
8.22 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
8.23 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
8.24 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
8.25 + probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
8.26 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
8.27 +val cpI = if pI = e_pblID then pI' else pI;
8.28 + val cmI = if mI = e_metID then mI' else mI;
8.29 + val {ppc, prls, where_, ...} = get_pbt cpI;
8.30 + val pre = check_preconds "thy 100820" prls where_ probl;
8.31 + val pb = foldl and_ (true, map fst pre);
8.32 +val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
8.33 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
8.34 +"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
8.35 +"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
8.36 +val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
8.37 + probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
8.38 +val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
8.39 +val cpI = if pI = e_pblID then pI' else pI;
8.40 +val ctxt = get_ctxt pt (p, Pbl);
8.41 +oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
8.42 +"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
8.43 + (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
8.44 +val SOME t = parseNEW ctxt str;
8.45 +if t = parseNEW "-1 + x = (0::real)" then ()
8.46 +else error "TODO"
8.47 +is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
8.48 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) use "Interpret/mstools.sml" (*empty*)
8.49 +
9.1 --- a/test/Tools/isac/Interpret/mstools.sml Wed May 04 14:07:51 2011 +0200
9.2 +++ b/test/Tools/isac/Interpret/mstools.sml Thu May 05 09:23:32 2011 +0200
9.3 @@ -38,13 +38,14 @@
9.4 [@{term "x * v"}, @{term "2 * u"}] ctxt;
9.5 val asms = get_assumptions ctxt;
9.6 if asms = [@{term "x * v"}, @{term "2 * u"}] then ()
9.7 -else error "mstools.sml insert_/get_assumptions changed.";
9.8 +else error "mstools.sml insert_/get_assumptions changed 1.";
9.9
9.10 val ctxt = insert_environments
9.11 [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] ctxt;
9.12 val envs = get_environments ctxt;
9.13 if envs = [(@{term "y"}, @{term "17"}), (@{term "z"}, @{term "y"})] then ()
9.14 -else error "mstools.sml insert_/get_environments changed.";
9.15 +else error "mstools.sml insert_/get_environments changed 2.";
9.16 +
9.17
9.18 "----------- fun transfer_from_subproblem ---------------";
9.19 "----------- fun transfer_from_subproblem ---------------";
10.1 --- a/test/Tools/isac/Test_Isac.thy Wed May 04 14:07:51 2011 +0200
10.2 +++ b/test/Tools/isac/Test_Isac.thy Thu May 05 09:23:32 2011 +0200
10.3 @@ -105,10 +105,6 @@
10.4 "~~~~~ fun me, args:"; val (_,tac) = nxt;
10.5 val (pt, p) = case locatetac tac (pt,p) of
10.6 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
10.7 -
10.8 -
10.9 -
10.10 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.11 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
10.12 val pIopt = get_pblID (pt,ip);
10.13 tacis; (*= []*)
10.14 @@ -135,17 +131,29 @@
10.15 oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
10.16 "~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
10.17 (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
10.18 -val SOME t = parseNEW ctxt str;
10.19 -if t = parseNEW "-1 + x = (0::real)" then ()
10.20 +*}
10.21 +ML {*
10.22 +val t = parseNEW ctxt str;
10.23 +str;
10.24 +t;
10.25 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.26 +if t = parseNEW ctxt "-1 + x = (0::real)" then ()
10.27 else error "TODO"
10.28 -is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
10.29 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) use "Interpret/mstools.sml" (*empty*)
10.30 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.31 +
10.32 *}
10.33 - use "Interpret/ctree.sml" (*! *)
10.34 +ML {*
10.35 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.36 +print_depth 999; applicable_in p pt m;
10.37 +Model_Problem';
10.38 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.39 +*}
10.40 + use "Interpret/mstools.sml" (*new 2010*)
10.41 + use "Interpret/ctree.sml" (*!...see(25)*)
10.42 use "Interpret/ptyps.sml" (* *)
10.43 (*use "Interpret/generate.sml" new 2011*)
10.44 use "Interpret/calchead.sml" (*! *)
10.45 - use "Interpret/appl.sml" (*!complete*)
10.46 + use "Interpret/appl.sml" (*!complete WEGEN INTERMED TESTCODE*)
10.47 use "Interpret/rewtools.sml" (*! *)
10.48 use "Interpret/script.sml" (*!TODO*)
10.49 (*use "Interpret/solve.sml" !TODO*)
10.50 @@ -215,3 +223,4 @@
10.51
10.52 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
10.53 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
10.54 +