intermed. usecase Diophant
located error with int in '= me' at first step specifying
fun is_known
1.1 --- a/src/Tools/isac/Interpret/appl.sml Thu Mar 17 10:46:02 2011 +0100
1.2 +++ b/src/Tools/isac/Interpret/appl.sml Fri Mar 18 09:26:03 2011 +0100
1.3 @@ -740,14 +740,14 @@
1.4 | applicable_in p pt (Empty_Tac) =
1.5 Notappl "Empty_Tac is not applicable"
1.6
1.7 - | applicable_in (p,p_) pt (Tac id) =
1.8 + | applicable_in (p,p_) pt (Tac id) =
1.9 let
1.10 val pp = par_pblobj pt p;
1.11 val thy' = (get_obj g_domID pt pp):theory';
1.12 val thy = assoc_thy thy';
1.13 - val _ = tracing ("fun applicable_in Tac: p_ = " ^ pos_2str p_);
1.14 val f = case p_ of
1.15 Frm => get_obj g_form pt p
1.16 + | Pbl => error "applicable_in (p,Pbl) pt (Tac id): not at Pbl"
1.17 | Res => (fst o (get_obj g_result pt)) p;
1.18 in case id of
1.19 "subproblem_equation_dummy" =>
2.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Mar 17 10:46:02 2011 +0100
2.2 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Mar 18 09:26:03 2011 +0100
2.3 @@ -278,9 +278,9 @@
2.4 (*.to an input (d,ts) find the according ori and insert the ts.*)
2.5 (*WN.11.03: + dont take first inter<>[]*)
2.6 fun seek_oridts thy sel (d,ts) [] =
2.7 - ("'" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
2.8 + ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy))
2.9 (comp_dts thy (d,ts))) ^
2.10 - "' not found (typed)", (0, [], sel, d, ts) : ori,
2.11 + "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
2.12 [])
2.13 | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
2.14 if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
2.15 @@ -296,9 +296,9 @@
2.16
2.17 (*.to an input (_,ts) find the according ori and insert the ts.*)
2.18 fun seek_orits thy sel ts [] =
2.19 - ("'" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
2.20 + ("seek_orits: input (_, '" ^ strs2str (map (Print_Mode.setmp [](Syntax.string_of_term
2.21 (thy2ctxt thy))) ts) ^
2.22 - "' not found (typed)", e_ori_, [])
2.23 + "') not found in oris (typed)", e_ori_, [])
2.24 | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
2.25 if sel = sel' andalso (inter op = ts ts') <> []
2.26 then if sel = sel'
2.27 @@ -740,6 +740,7 @@
2.28 (* val (ori,t)=(oris,term_of ct);
2.29 *)
2.30 let
2.31 + val _ = tracing ("RM is_known: t=" ^ term2str t);
2.32 val ots = (distinct o flat o (map #5)) (ori:ori list);
2.33 val oids = ((map (fst o dest_Free)) o distinct o
2.34 flat o (map vars)) ots;
3.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Mar 17 10:46:02 2011 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Mar 18 09:26:03 2011 +0100
3.3 @@ -2676,10 +2676,11 @@
3.4 ---------------------------------------------- *)
3.5
3.6
3.7 -(*. converts a term, which contains severel terms seperated by +, into a list of these terms .*)
3.8 +(* converts a term, which contains several terms seperated by +, into a list of these terms .*)
3.9 fun term2list (t as (Const("Rings.inverse_class.divide",_) $ _ $ _)) = [t]
3.10 | term2list (t as (Const("Atools.pow",_) $ _ $ _)) =
3.11 - [Const("Rings.inverse_class.divide",[HOLogic.realT,HOLogic.realT]--->HOLogic.realT) $
3.12 + [Const ("Rings.inverse_class.divide",
3.13 + [HOLogic.realT,HOLogic.realT] ---> HOLogic.realT) $
3.14 t $ Free("1",HOLogic.realT)
3.15 ]
3.16 | term2list (t as (Free(_,_))) =
3.17 @@ -2742,7 +2743,7 @@
3.18 (*.same as add_fraction_p_ but with normalform [3].*)
3.19 (*SOME (step_add_list_of_fractions2(term2list(t))); *)
3.20 fun add_fraction_ (thy:theory) t =
3.21 - if length(term2list(t))>1
3.22 + if length (term2list t) > 1
3.23 then SOME (add_list_of_fractions_exp(term2list(t))) handle _ => NONE
3.24 else (*error ("RATIONALS_ADD_FRACTION_EXCEPTION: nothing to add")*)
3.25 NONE;
4.1 --- a/src/Tools/isac/Test_Isac.thy Thu Mar 17 10:46:02 2011 +0100
4.2 +++ b/src/Tools/isac/Test_Isac.thy Fri Mar 18 09:26:03 2011 +0100
4.3 @@ -129,8 +129,11 @@
4.4 use"biegelinie.sml";
4.5 use"algein.sml";
4.6 *)
4.7 +use "../../../test/Tools/isac/Knowledge/diophanteq.sml" (**)
4.8 ML {*
4.9 -Thy_Info.get_theory "Isac"
4.10 +is_known;
4.11 +print_depth 999;
4.12 +nxt;
4.13 *}
4.14 use "../../../test/Tools/isac/Knowledge/isac.sml" (**)
4.15
5.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Thu Mar 17 10:46:02 2011 +0100
5.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Fri Mar 18 09:26:03 2011 +0100
5.3 @@ -47,11 +47,11 @@
5.4 ["diophantine","equation"], ["Test","solve_diophant"]))];
5.5 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
5.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.8 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
5.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.14 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.15 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
6.1 --- a/test/Tools/isac/Knowledge/rational.sml Thu Mar 17 10:46:02 2011 +0100
6.2 +++ b/test/Tools/isac/Knowledge/rational.sml Fri Mar 18 09:26:03 2011 +0100
6.3 @@ -1345,7 +1345,7 @@
6.4 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
6.5 term2str t';
6.6 if term2str t' =
6.7 - "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"
6.8 + "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"
6.9 (*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
6.10 then () else error "rational.sml: S.K.8..corrected 060904-6";
6.11
6.12 @@ -2078,5 +2078,3 @@
6.13 " Try (Rewrite_Set discard_parentheses False)) " ^
6.14 " t_t)"
6.15 );
6.16 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
6.17 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)