1.1 --- a/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 19:10:30 2005 +0200
1.2 +++ b/src/sml/IsacKnowledge/Integrate.ML Sat Aug 20 21:20:16 2005 +0200
1.3 @@ -153,9 +153,9 @@
1.4 srls = e_rls,
1.5 prls=e_rls,
1.6 crls = Atools_erls, nrls = e_rls},
1.7 -"Script IntegrationScript (f_::real) (v_::real) = \
1.8 -\ ((Rewrite_Set_Inst [(bdv,v_)] integration_rules False)\
1.9 -\ (Integral f_ D v_))"
1.10 +"Script IntegrationScript (f_::real) (v_::real) = \
1.11 +\ (let t_ = Integral f_ D v_ \
1.12 +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
1.13 ));
1.14
1.15 store_met
1.16 @@ -168,7 +168,8 @@
1.17 srls = e_rls,
1.18 prls=e_rls,
1.19 crls = Atools_erls, nrls = e_rls},
1.20 - "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
1.21 -\ (F_ = Integral f_ D v_)"
1.22 +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
1.23 +\ (let t_ = (F_ = Integral f_ D v_) \
1.24 +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)"
1.25 ));
1.26
2.1 --- a/src/sml/IsacKnowledge/Integrate.thy Sat Aug 20 19:10:30 2005 +0200
2.2 +++ b/src/sml/IsacKnowledge/Integrate.thy Sat Aug 20 21:20:16 2005 +0200
2.3 @@ -27,7 +27,7 @@
2.4
2.5 (*Script-names*)
2.6 IntegrationScript :: "[real,real, real] => real"
2.7 - ("((Script IntegrationScript (_ _=))// (_))" 9)
2.8 + ("((Script IntegrationScript (_ _ =))// (_))" 9)
2.9 NamedIntegrationScript :: "[real,real,real, bool] => bool"
2.10 ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
2.11
3.1 --- a/src/sml/ME/mathengine.sml Sat Aug 20 19:10:30 2005 +0200
3.2 +++ b/src/sml/ME/mathengine.sml Sat Aug 20 21:20:16 2005 +0200
3.3 @@ -1,15 +1,10 @@
3.4 -(* ME/mathengine.sml *)
3.5 -(* ~~~~~~~~~~~~~~~~~~~~~~~~~~ *)
3.6 -(* The _functional_ mathematics engine, ie. without a state. Input and *)
3.7 -(* output are Isabelle's formulae as strings. *)
3.8 +(* The _functional_ mathematics engine, ie. without a state.
3.9 + Input and output are Isabelle's formulae as strings.
3.10 + (c) Walther Neuper 2000
3.11 + (c) Stefan Rath 2005
3.12
3.13 -
3.14 -(* sml-code for FE-interface
3.15 -
3.16 - use"../FE-interface/sml.sml";
3.17 - use"FE-interface/sml.sml";
3.18 - use"sml.sml";
3.19 - *)
3.20 +use"~/proto2/isac/src/sml/ME/mathengine.sml";
3.21 +*)
3.22
3.23 signature MATHENGINE =
3.24 sig
3.25 @@ -49,11 +44,6 @@
3.26 pos' ->
3.27 NEW ->
3.28 ptree -> pos' * NEW * mout * tac'_ * safe * ptree
3.29 - val meNEW :
3.30 - tac'_ ->
3.31 - pos' ->
3.32 - NEW ->
3.33 - ptree -> pos' * NEW * mout * tac'_ * safe * ptree
3.34
3.35 val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate'
3.36 val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate'
3.37 @@ -63,9 +53,10 @@
3.38
3.39
3.40
3.41 -
3.42 +(*
3.43 structure mathengine : MATHENGINE =
3.44 struct
3.45 +*)
3.46 fun get_pblID (pt, (p,_):pos') =
3.47 let val p' = par_pblobj pt p
3.48 val (_,pI,_) = get_obj g_spec pt p'
3.49 @@ -97,13 +88,9 @@
3.50 (* val (m, pos) = ((mI,m), ip);
3.51 val (m,(pt,pos) ) = ((mI,m), ptp);
3.52 *)
3.53 - (*val (p',_,f,tac,s,pt') = solve m pos pt;
3.54 -
3.55 - (writeln o istate2str) (get_istate pt' p');
3.56 - (term2str o fst) (get_obj g_result pt' (fst p'));
3.57 - *)
3.58 let val (*p,_,f,_,s,pt*) (msg, cs') = solve m (pt, pos)
3.59 -(* val (_,(pt',p')) = cs';
3.60 +(* val (msg, cs') = solve m (pt, pos);
3.61 + val (tacis,dels,(pt',p')) = cs';
3.62 (writeln o istate2str) (get_istate pt' p');
3.63 (term2str o fst) (get_obj g_result pt' (fst p'));
3.64 *)
3.65 @@ -119,8 +106,8 @@
3.66 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
3.67 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
3.68 | locatetac tac (ptp as (pt, p)) =
3.69 -(* val ptp as (pt, p) = (pt, p);
3.70 - val ptp as (pt, p) = (pt, ip);
3.71 +(* val ptp as (pt, p) = (pt, ip);
3.72 + val ptp as (pt, p) = (pt, p);
3.73 *)
3.74 let val (mI,m) = mk_tac'_ tac;
3.75 in case applicable_in p pt m of
3.76 @@ -236,8 +223,8 @@
3.77 (*.does a step forward; returns tactic used, ctree updated.*)
3.78 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
3.79 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
3.80 + val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
3.81 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
3.82 - val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
3.83 *)
3.84 let val pIopt = get_pblID (pt,ip);
3.85 in if p = ([],Res) orelse ip = ([],Res)
3.86 @@ -258,13 +245,13 @@
3.87 None => ("no-fmz-spec", ([], [], ptp))
3.88 | Some pI =>
3.89 (* val Some pI = pIopt;
3.90 - val cs = (if p_ mem [Pbl,Met]
3.91 + val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p))
3.92 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
3.93 handle _ => ([], ptp);
3.94 *)
3.95 (case (if p_ mem [Pbl,Met]
3.96 andalso is_none (get_obj g_env pt (fst p))
3.97 - (*........: no Apply_Method without init_form*)
3.98 + (*........: Apply_Method without init_form*)
3.99 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
3.100 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
3.101 of cs as ([],_,_) => ("helpless", cs)
3.102 @@ -423,10 +410,10 @@
3.103 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
3.104
3.105
3.106 -fun meNEW ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
3.107 +fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
3.108 (* val (_,tac) = nxt;
3.109 *) let val (pt, p) =
3.110 -(* val (eee, (tacis, (pt',p'))) = locatetac tac (pt,p);
3.111 +(* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
3.112 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));
3.113 writeln( istate2str (get_istate pt' ([3],Res)));
3.114 term2str (fst (get_obj g_result pt' [3]));
3.115 @@ -454,11 +441,8 @@
3.116 else Empty_Tac;
3.117 in (p:pos',[]:NEW, TESTg_form (pt, p),
3.118 (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
3.119 -
3.120 -(********************************************************************)
3.121 -(****************) val me = meNEW; (*********************************)
3.122 -(********************************************************************)
3.123 -
3.124 +(*
3.125 end
3.126
3.127 open mathengine;
3.128 +*)
3.129 \ No newline at end of file
4.1 --- a/src/sml/ME/script.sml Sat Aug 20 19:10:30 2005 +0200
4.2 +++ b/src/sml/ME/script.sml Sat Aug 20 21:20:16 2005 +0200
4.3 @@ -209,6 +209,8 @@
4.4
4.5 (*.get argument of first stactic in a script for init_form.*)
4.6 fun get_stac thy (h $ body) =
4.7 +(*
4.8 + *)
4.9 let
4.10 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
4.11 (case get_t y e1 a of None => get_t y e2 a | la => la)
5.1 --- a/src/sml/ME/solve.sml Sat Aug 20 19:10:30 2005 +0200
5.2 +++ b/src/sml/ME/solve.sml Sat Aug 20 21:20:16 2005 +0200
5.3 @@ -136,7 +136,7 @@
5.4
5.5
5.6 (* val ("Apply_Method",Apply_Method' (mI,_))=(mI,m);
5.7 - val (("Apply_Method",Apply_Method' (mI,_)), pos as (p,_))=(m, pos);
5.8 + val (("Apply_Method",Apply_Method' (mI,_,_)), pos as (p,_))=(m, pos);
5.9 *)
5.10 fun solve ("Apply_Method",Apply_Method' (mI,_,_)) (pt:ptree,(pos as (p,_))) =
5.11 let val {srls,...} = get_met mI;
6.1 --- a/src/sml/Scripts/Script.thy Sat Aug 20 19:10:30 2005 +0200
6.2 +++ b/src/sml/Scripts/Script.thy Sat Aug 20 21:20:16 2005 +0200
6.3 @@ -29,16 +29,16 @@
6.4 Rewrite :: "[ID, bool, 'a] => 'a"
6.5 Rewrite'_Inst:: "[(real * real) list, ID, bool, 'a] => 'a"
6.6 ("(Rewrite'_Inst (_ _ _))" 11)
6.7 - (*without last argument ^^ FIXXXXME*)
6.8 + (*without last argument ^^ for @@*)
6.9 Rewrite'_Set :: "[ID, bool, 'a] => 'a" ("(Rewrite'_Set (_ _))" 11)
6.10 Rewrite'_Set'_Inst
6.11 :: "[(real * real) list, ID, bool, 'a] => 'a"
6.12 ("(Rewrite'_Set'_Inst (_ _ _))" 11)
6.13 - (*without last argument ^^ FIXXXXME*)
6.14 + (*without last argument ^^ for @@*)
6.15 Calculate :: "[ID, 'a] => 'a"
6.16 Substitute :: "[(real * real) list, 'a] => 'a"
6.17 Map :: "['a => 'b, 'a list] => 'b list"
6.18 - Tac :: "ID => 'a"
6.19 + Tac :: "ID => 'a" (*deprecated; only use in Test.ML*)
6.20 Check'_elementwise ::
6.21 "['a list, 'b set] => 'a list"
6.22 ("Check'_elementwise (_ _)" 11)
7.1 --- a/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 19:10:30 2005 +0200
7.2 +++ b/src/smltest/IsacKnowledge/integrate.sml Sat Aug 20 21:20:16 2005 +0200
7.3 @@ -15,9 +15,8 @@
7.4 "----------- test new_c ------------------------------------------";
7.5 "----------- integrate by ruleset --------------------------------";
7.6 "----------- check probem type -----------------------------------";
7.7 -"----------- check method [Diff,integration] ---------------------";
7.8 -"----------- me method [Diff,integration] ---------------------";
7.9 -"----------- check method [Diff,integration,named] ---------------";
7.10 +"----------- check Scripts ---------------------------------------";
7.11 +"----------- me method [Diff,integration] ------------------------";
7.12 "-----------------------------------------------------------------";
7.13 "-----------------------------------------------------------------";
7.14 "-----------------------------------------------------------------";
7.15 @@ -155,30 +154,26 @@
7.16 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()
7.17 | _ => raise error "integrate.sml: Integrate.Integrate ???";
7.18
7.19 -"----------- check method [Diff,integration] ---------------------";
7.20 -"----------- check method [Diff,integration] ---------------------";
7.21 -"----------- check method [Diff,integration] ---------------------";
7.22 -show_mets();
7.23 -(*
7.24 +
7.25 +"----------- check Scripts ---------------------------------------";
7.26 +"----------- check Scripts ---------------------------------------";
7.27 +"----------- check Scripts ---------------------------------------";
7.28 val str =
7.29 "Script IntegrationScript (f_::real) (v_::real) = \
7.30 -\ (let t_ = (Integral f_ D v_)::real \
7.31 -\ in (Rewrite_Set_Inst [(bdv,v_)] integration False t_::real))";
7.32 +\ (let t_ = Integral f_ D v_ \
7.33 +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
7.34 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.35 +atomty thy sc;
7.36
7.37 val str =
7.38 -"Script IntegrationScript (f_::real) (v_::real) = \
7.39 -\ (let t_ = (Integral f_ D v_)::real \
7.40 -\ in t_)";
7.41 +"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
7.42 +\ (let t_ = (F_ = Integral f_ D v_) \
7.43 +\ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
7.44 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.45 -val str =
7.46 -"Rewrite_Set_Inst [(bdv,v_)] integration False (t_::real)";
7.47 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.48 +atomty thy sc;
7.49 +show_mets();
7.50
7.51
7.52 -atomty thy sc;
7.53 -###############################################################*)
7.54 -
7.55 "----------- me method [Diff,integration] ---------------------";
7.56 "----------- me method [Diff,integration] ---------------------";
7.57 "----------- me method [Diff,integration] ---------------------";
7.58 @@ -195,18 +190,8 @@
7.59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.63 val (p,_,f,nxt,_,pt) = me nxt p c pt;(*---> Empty_Tac*)
7.64
7.65
7.66
7.67 -
7.68 -
7.69 -"----------- check method [Diff,integration,named] ---------------";
7.70 -"----------- check method [Diff,integration,named] ---------------";
7.71 -"----------- check method [Diff,integration,named] ---------------";
7.72 -val str =
7.73 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real) = \
7.74 -\ (F_ = Integral f_ D v_)";
7.75 -val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
7.76 -atomty thy sc;
7.77 -