# HG changeset patch # User wneuper # Date 1124565616 -7200 # Node ID cac1f942e1a1c852b2340e798b5c466b5d1d5f0e # Parent 2488337fd0ddf582b88b10b51a7fa47e84fee275 find out why IntegrateScript doesnt work diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/IsacKnowledge/Integrate.ML --- a/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 21:20:16 2005 +0200 @@ -153,9 +153,9 @@ srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script IntegrationScript (f_::real) (v_::real) = \ -\ ((Rewrite_Set_Inst [(bdv,v_)] integration_rules False)\ -\ (Integral f_ D v_))" +"Script IntegrationScript (f_::real) (v_::real) = \ +\ (let t_ = Integral f_ D v_ \ +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))" )); store_met @@ -168,7 +168,8 @@ srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, - "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ -\ (F_ = Integral f_ D v_)" +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ +\ (let t_ = (F_ = Integral f_ D v_) \ +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)" )); diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/IsacKnowledge/Integrate.thy --- a/src/sml/IsacKnowledge/Integrate.thy Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/IsacKnowledge/Integrate.thy Sat Aug 20 21:20:16 2005 +0200 @@ -27,7 +27,7 @@ (*Script-names*) IntegrationScript :: "[real,real, real] => real" - ("((Script IntegrationScript (_ _=))// (_))" 9) + ("((Script IntegrationScript (_ _ =))// (_))" 9) NamedIntegrationScript :: "[real,real,real, bool] => bool" ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9) diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/ME/mathengine.sml --- a/src/sml/ME/mathengine.sml Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/ME/mathengine.sml Sat Aug 20 21:20:16 2005 +0200 @@ -1,15 +1,10 @@ -(* ME/mathengine.sml *) -(* ~~~~~~~~~~~~~~~~~~~~~~~~~~ *) -(* The _functional_ mathematics engine, ie. without a state. Input and *) -(* output are Isabelle's formulae as strings. *) +(* The _functional_ mathematics engine, ie. without a state. + Input and output are Isabelle's formulae as strings. + (c) Walther Neuper 2000 + (c) Stefan Rath 2005 - -(* sml-code for FE-interface - - use"../FE-interface/sml.sml"; - use"FE-interface/sml.sml"; - use"sml.sml"; - *) +use"~/proto2/isac/src/sml/ME/mathengine.sml"; +*) signature MATHENGINE = sig @@ -49,11 +44,6 @@ pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree - val meNEW : - tac'_ -> - pos' -> - NEW -> - ptree -> pos' * NEW * mout * tac'_ * safe * ptree val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate' val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate' @@ -63,9 +53,10 @@ - +(* structure mathengine : MATHENGINE = struct +*) fun get_pblID (pt, (p,_):pos') = let val p' = par_pblobj pt p val (_,pI,_) = get_obj g_spec pt p' @@ -97,13 +88,9 @@ (* val (m, pos) = ((mI,m), ip); val (m,(pt,pos) ) = ((mI,m), ptp); *) - (*val (p',_,f,tac,s,pt') = solve m pos pt; - - (writeln o istate2str) (get_istate pt' p'); - (term2str o fst) (get_obj g_result pt' (fst p')); - *) let val (*p,_,f,_,s,pt*) (msg, cs') = solve m (pt, pos) -(* val (_,(pt',p')) = cs'; +(* val (msg, cs') = solve m (pt, pos); + val (tacis,dels,(pt',p')) = cs'; (writeln o istate2str) (get_istate pt' p'); (term2str o fst) (get_obj g_result pt' (fst p')); *) @@ -119,8 +106,8 @@ (*report applicability of tac in tacis; pt is dropped in setNextTactic*) fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp)) | locatetac tac (ptp as (pt, p)) = -(* val ptp as (pt, p) = (pt, p); - val ptp as (pt, p) = (pt, ip); +(* val ptp as (pt, p) = (pt, ip); + val ptp as (pt, p) = (pt, p); *) let val (mI,m) = mk_tac'_ tac; in case applicable_in p pt m of @@ -236,8 +223,8 @@ (*.does a step forward; returns tactic used, ctree updated.*) fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) = (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1); + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[])); - val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs); *) let val pIopt = get_pblID (pt,ip); in if p = ([],Res) orelse ip = ([],Res) @@ -258,13 +245,13 @@ None => ("no-fmz-spec", ([], [], ptp)) | Some pI => (* val Some pI = pIopt; - val cs = (if p_ mem [Pbl,Met] + val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p)) then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) handle _ => ([], ptp); *) (case (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p)) - (*........: no Apply_Method without init_form*) + (*........: Apply_Method without init_form*) then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip)) handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*) of cs as ([],_,_) => ("helpless", cs) @@ -423,10 +410,10 @@ meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) -fun meNEW ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = +fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) = (* val (_,tac) = nxt; *) let val (pt, p) = -(* val (eee, (tacis, (pt',p'))) = locatetac tac (pt,p); +(* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p); (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p')); writeln( istate2str (get_istate pt' ([3],Res))); term2str (fst (get_obj g_result pt' [3])); @@ -454,11 +441,8 @@ else Empty_Tac; in (p:pos',[]:NEW, TESTg_form (pt, p), (tac2IDstr tac, tac):tac'_, Sundef, pt) end; - -(********************************************************************) -(****************) val me = meNEW; (*********************************) -(********************************************************************) - +(* end open mathengine; +*) \ No newline at end of file diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/ME/script.sml --- a/src/sml/ME/script.sml Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/ME/script.sml Sat Aug 20 21:20:16 2005 +0200 @@ -209,6 +209,8 @@ (*.get argument of first stactic in a script for init_form.*) fun get_stac thy (h $ body) = +(* + *) let fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = (case get_t y e1 a of None => get_t y e2 a | la => la) diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/ME/solve.sml --- a/src/sml/ME/solve.sml Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/ME/solve.sml Sat Aug 20 21:20:16 2005 +0200 @@ -136,7 +136,7 @@ (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m); - val (("Apply_Method",Apply_Method' (mI,_)), pos as (p,_))=(m, pos); + val (("Apply_Method",Apply_Method' (mI,_,_)), pos as (p,_))=(m, pos); *) fun solve ("Apply_Method",Apply_Method' (mI,_,_)) (pt:ptree,(pos as (p,_))) = let val {srls,...} = get_met mI; diff -r 2488337fd0dd -r cac1f942e1a1 src/sml/Scripts/Script.thy --- a/src/sml/Scripts/Script.thy Sat Aug 20 19:10:30 2005 +0200 +++ b/src/sml/Scripts/Script.thy Sat Aug 20 21:20:16 2005 +0200 @@ -29,16 +29,16 @@ Rewrite :: "[ID, bool, 'a] => 'a" Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a" ("(Rewrite'_Inst (_ _ _))" 11) - (*without last argument ^^ FIXXXXME*) + (*without last argument ^^ for @@*) Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11) Rewrite'_Set'_Inst :: "[(real * real) list, ID, bool, 'a] => 'a" ("(Rewrite'_Set'_Inst (_ _ _))" 11) - (*without last argument ^^ FIXXXXME*) + (*without last argument ^^ for @@*) Calculate :: "[ID, 'a] => 'a" Substitute :: "[(real * real) list, 'a] => 'a" Map :: "['a => 'b, 'a list] => 'b list" - Tac :: "ID => 'a" + Tac :: "ID => 'a" (*deprecated; only use in Test.ML*) Check'_elementwise :: "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11) diff -r 2488337fd0dd -r cac1f942e1a1 src/smltest/IsacKnowledge/integrate.sml --- a/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 19:10:30 2005 +0200 +++ b/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 21:20:16 2005 +0200 @@ -15,9 +15,8 @@ "----------- test new_c ------------------------------------------"; "----------- integrate by ruleset --------------------------------"; "----------- check probem type -----------------------------------"; -"----------- check method [Diff,integration] ---------------------"; -"----------- me method [Diff,integration] ---------------------"; -"----------- check method [Diff,integration,named] ---------------"; +"----------- check Scripts ---------------------------------------"; +"----------- me method [Diff,integration] ------------------------"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; @@ -155,30 +154,26 @@ case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => () | _ => raise error "integrate.sml: Integrate.Integrate ???"; -"----------- check method [Diff,integration] ---------------------"; -"----------- check method [Diff,integration] ---------------------"; -"----------- check method [Diff,integration] ---------------------"; -show_mets(); -(* + +"----------- check Scripts ---------------------------------------"; +"----------- check Scripts ---------------------------------------"; +"----------- check Scripts ---------------------------------------"; val str = "Script IntegrationScript (f_::real) (v_::real) = \ -\ (let t_ = (Integral f_ D v_)::real \ -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False t_::real))"; +\ (let t_ = Integral f_ D v_ \ +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +atomty thy sc; val str = -"Script IntegrationScript (f_::real) (v_::real) = \ -\ (let t_ = (Integral f_ D v_)::real \ -\ in t_)"; +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ +\ (let t_ = (F_ = Integral f_ D v_) \ +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; -val str = -"Rewrite_Set_Inst [(bdv,v_)] integration False (t_::real)"; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; +atomty thy sc; +show_mets(); -atomty thy sc; -###############################################################*) - "----------- me method [Diff,integration] ---------------------"; "----------- me method [Diff,integration] ---------------------"; "----------- me method [Diff,integration] ---------------------"; @@ -195,18 +190,8 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*) - - -"----------- check method [Diff,integration,named] ---------------"; -"----------- check method [Diff,integration,named] ---------------"; -"----------- check method [Diff,integration,named] ---------------"; -val str = -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \ -\ (F_ = Integral f_ D v_)"; -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; -atomty thy sc; -