1.1 --- a/src/Tools/isac/Interpret/script.sml Mon Dec 31 14:49:16 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Jan 10 18:17:48 2019 +0100
1.3 @@ -217,7 +217,8 @@
1.4 val _ = if pats = [] then raise ERROR errmsg else ()
1.5 in (flat o (map (itm2arg itms))) pats end;
1.6
1.7 -(* convert a script-tac 'stac' to a tactic 'tac';
1.8 +(* convert a script-tac 'stac' to 'tac' for users;
1.9 + for "Script.SubProblem" also create a 'tac_' for internal use. FIXME separate?
1.10 if stac is an initac, then convert to a 'tac_' (as required in appy).
1.11 arg ctree for pushing the thy specified in rootpbl into subpbls *)
1.12 fun stac2tac_ _ thy (Const ("Script.Rewrite", _) $ thmID $ _ $ _) =
1.13 @@ -226,10 +227,8 @@
1.14 in (Tac.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tac.Empty_Tac_) end
1.15 | stac2tac_ _ thy (Const ("Script.Rewrite'_Inst", _) $ sub $ thmID $ _ $ _) =
1.16 let
1.17 - val subML = ((map TermC.isapair2pair) o TermC.isalist2list) sub
1.18 - val subStr = Selem.subst2subs subML
1.19 - val tid = HOLogic.dest_string thmID (*4.10.02 unnoetig*)
1.20 - in (Tac.Rewrite_Inst (subStr, (tid, Rewrite.assoc_thm'' thy tid)), Tac.Empty_Tac_) end
1.21 + val tid = HOLogic.dest_string thmID
1.22 + in (Tac.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tac.Empty_Tac_) end
1.23 | stac2tac_ _ _ (Const ("Script.Rewrite'_Set",_) $ rls $ _ $ _) =
1.24 (Tac.Rewrite_Set (HOLogic.dest_string rls), Tac.Empty_Tac_)
1.25 | stac2tac_ _ _ (Const ("Script.Rewrite'_Set'_Inst", _) $ sub $ rls $ _ $ _) =
1.26 @@ -486,14 +485,14 @@
1.27 let val ct = Thm.global_cterm_of thy (HOLogic.Trueprop $ t)
1.28 in Rule.Thm (Rule.term_to_string''' thy (Thm.term_of ct), Thm.make_thm ct) end;
1.29
1.30 -fun rep_tac_ (Tac.Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _))) =
1.31 - let val fT = type_of f;
1.32 - val b = if put then @{term True} else @{term False};
1.33 - val sT = (type_of o fst o hd) subs;
1.34 - val subs' = TermC.list2isalist (HOLogic.mk_prodT (sT, sT)) (map HOLogic.mk_prod subs);
1.35 +fun rep_tac_ (Tac.Rewrite_Inst' (thy', _, _, _, subs, (thmID, _), f, (f', _))) =
1.36 + let
1.37 + val b = @{term False};
1.38 + val subs' = Selem.subst_to_subst' subs;
1.39 val sT' = type_of subs';
1.40 + val fT = type_of f;
1.41 val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.42 - $ subs' $ Free (thmID, HOLogic.stringT) $ b $ f;
1.43 + $ subs' $ HOLogic.mk_string thmID $ b $ f;
1.44 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.45 | rep_tac_ (Tac.Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.46 let
1.47 @@ -502,7 +501,15 @@
1.48 val lhs = Const ("Script.Rewrite", [HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.49 $ HOLogic.mk_string thmID $ b $ f;
1.50 in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.51 - | rep_tac_ (Tac.Rewrite_Set_Inst' (_, _, _, _, _, (f', _))) = (Rule.e_rule, (Rule.e_term, f'))
1.52 + | rep_tac_ (Tac.Rewrite_Set_Inst' (thy', _, subs, rls, f, (f', _))) =
1.53 + let
1.54 + val b = @{term False};
1.55 + val subs' = Selem.subst_to_subst' subs;
1.56 + val sT' = type_of subs';
1.57 + val fT = type_of f;
1.58 + val lhs = Const ("Script.Rewrite'_Set'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
1.59 + $ subs' $ HOLogic.mk_string (Rule.id_rls rls) $ b $ f;
1.60 + in (((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f')) end
1.61 | rep_tac_ (Tac.Rewrite_Set' (thy', put, rls, f, (f', _))) =
1.62 let
1.63 val fT = type_of f;
1.64 @@ -924,14 +931,14 @@
1.65 (_, LTool.Expr s) => Skip (s, E)
1.66 | (a', LTool.STac stac) =>
1.67 let val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac
1.68 - in case m of
1.69 + in case m of
1.70 Tac.Subproblem _ => Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false))
1.71 | _ =>
1.72 (case Applicable.applicable_in p pt m of
1.73 Chead.Appl m' => (Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))
1.74 | _ => Napp E)
1.75 end
1.76 -(*GOON*)
1.77 +
1.78 fun nxt_up thy ptp (scr as (Rule.Prog sc)) E l ay (Const ("HOL.Let", _) $ _) a v = (*comes from let=...*)
1.79 if ay = Napp_
1.80 then nstep_up thy ptp scr E (drop_last l) Napp_ a v
2.1 --- a/src/Tools/isac/Interpret/specification-elems.sml Mon Dec 31 14:49:16 2018 +0100
2.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml Thu Jan 10 18:17:48 2019 +0100
2.3 @@ -16,10 +16,14 @@
2.4 datatype istate = RrlsState of Rule.rrlsstate | ScrState of scrstate | Uistate
2.5 val istate2str : istate -> string
2.6 val e_istate : istate
2.7 - type subs
2.8 - type sube
2.9 - type subte
2.10 - val subst'_to_sube : term -> Rule.cterm' list
2.11 + type subs (* substitution as seen by learner. rename stubst_user ["(''bdv'', x)"]*)
2.12 + type sube (* = subs. delete ! *)
2.13 + type subte (* _sub_stitution as _t_erms of _e_qualities: revise ! [bdv = x] *)
2.14 + type subst' (* substitution in isac-programs; converted immediately [(bdv, x)] *)
2.15 +(*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
2.16 + (* use above types in functions below and elsewhere; rename below according to types *)
2.17 + val subst'_to_sube : subst' -> Rule.cterm' list (* e.g. rename to subst_user_of_prog *)
2.18 + val subst_to_subst' : Rule.subst -> subst'
2.19 val sube2str : Rule.cterm' list -> string
2.20 val sube2subst : theory -> Rule.cterm' list -> (term * term) list
2.21 val sube2subte : Rule.cterm' list -> term list
2.22 @@ -29,12 +33,7 @@
2.23 val subst2subs' : (term * term) list -> (string * string) list
2.24 val subte2sube : term list -> Rule.cterm' list
2.25 val e_ctxt : Proof.context
2.26 -(*----- needed for tac, tac_ immediately (probably pre-requisites missing)
2.27 - type istate
2.28 - type subte
2.29 - type subs
2.30 - type sube
2.31 -*)
2.32 +
2.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.34 val e_fmz : fmz_ * Celem.spec (* for datatypes.sml *)
2.35 val e_sube : Rule.cterm' list
2.36 @@ -108,31 +107,46 @@
2.37 | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
2.38 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
2.39
2.40 -type subs = Rule.cterm' list; (*16.11.00 for FE-KE*)
2.41 -val e_subs = ["(bdv, x)"]; (* for tests only *)
2.42 +type subs = Rule.cterm' list; (* substitution as seen by learner in tactics, in programs, etc.
2.43 + questionable design. rename to stubst_user *)
2.44 +val e_subs = ["(''bdv'', x)"]; (* for tests only *)
2.45
2.46 (* argument type of tac Rewrite_Inst *)
2.47 -type sube = Rule.cterm' list;
2.48 +type sube = Rule.cterm' list; (* = subs. delete *)
2.49 val e_sube = []: Rule.cterm' list; (* for tests only *)
2.50 fun sube2str s = strs2str s;
2.51
2.52 -(* _sub_stitution as _t_erms of _e_qualities *)
2.53 -type subte = term list;
2.54 +type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)
2.55
2.56 -type subst' = term (* decomposes to "(char list * term) list", where term is Free ("xxx", _)
2.57 +type subst' = term; (* substitution in isac-programs. rename to subst_prog
2.58 + is "(char list * term) list", where term is Free ("xxx", _)
2.59 e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)
2.60 fun subst'_to_sube sub = (sub
2.61 |> HOLogic.dest_list
2.62 |> map HOLogic.dest_prod
2.63 |> map (fn (e1, e2) => (HOLogic.dest_string e1, Rule.term2str e2))
2.64 - |> map (fn (e1, e2) => "(" ^ e1 ^ ", " ^ e2 ^ ")"): Rule.cterm' list)
2.65 + |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): Rule.cterm' list)
2.66 handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
2.67 -
2.68 +fun subst_to_subst' subst = subst
2.69 + |> map (apfst TermC.free2str)
2.70 + |> map (apfst HOLogic.mk_string)
2.71 + |> map HOLogic.mk_prod
2.72 + |> HOLogic.mk_list (HOLogic.mk_prodT (HOLogic.stringT, HOLogic.realT (*FIXME: 'a*)))
2.73 val subte2sube = map Rule.term2str;
2.74 -val subst2subs = map (pair2str o (apfst Rule.term2str) o (apsnd Rule.term2str));
2.75 +fun subst2subs subst_rew = (subst_rew
2.76 + |> map (apsnd Rule.term2str)
2.77 + |> map (apfst Rule.term2str)
2.78 + |> map (apfst (enclose "''" "''")))
2.79 + |> map pair2str
2.80 + handle TERM _ => raise TERM ("subst2subs: wrong argument " ^ Celem.env2str subst_rew, [])
2.81 fun subst2sube subst = map Rule.term2str (map HOLogic.mk_eq subst)
2.82 val subst2subs' = map ((apfst Rule.term2str) o (apsnd Rule.term2str));
2.83 -fun subs2subst thy s = map (TermC.isapair2pair o (TermC.parse_patt thy)) s;
2.84 +fun subs2subst thy subs = (subs
2.85 + |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
2.86 + |> map TermC.isapair2pair
2.87 + |> map (apfst HOLogic.dest_string)
2.88 + |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
2.89 + handle TERM _ => raise TERM ("subs2subst: wrong argument " ^ strs2str' subs, [])
2.90 fun sube2subst thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
2.91 val sube2subte = map TermC.str2term;
2.92 val subte2subst = map HOLogic.dest_eq;
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Dec 31 14:49:16 2018 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Jan 10 18:17:48 2019 +0100
3.3 @@ -296,7 +296,7 @@
3.4 crls = Atools_erls, errpats = [], nrls = norm_diff},
3.5 "Script DiffScr (f_f::real) (v_v::real) = " ^
3.6 " (let f_f' = Take (d_d v_v f_f) " ^
3.7 - " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
3.8 + " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
3.9 " (Repeat " ^
3.10 " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
3.11 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^
3.12 @@ -356,7 +356,7 @@
3.13 crls=Atools_erls, errpats = [], nrls = norm_diff},
3.14 "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
3.15 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
3.16 - " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
3.17 + " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^
3.18 " (Repeat " ^
3.19 " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^
3.20 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_dif'' False)) Or " ^
3.21 @@ -376,7 +376,7 @@
3.22 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^
3.23 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^
3.24 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^
3.25 - " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f') ")]
3.26 + " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') ")]
3.27 \<close>
3.28 setup \<open>KEStore_Elems.add_mets
3.29 [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Mon Dec 31 14:49:16 2018 +0100
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Jan 10 18:17:48 2019 +0100
4.3 @@ -363,7 +363,7 @@
4.4 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
4.5 "Script IntegrationScript (f_f::real) (v_v::real) = " ^
4.6 " (let t_t = Take (Integral f_f D v_v) " ^
4.7 - " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))")]
4.8 + " in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))")]
4.9 \<close>
4.10 setup \<open>KEStore_Elems.add_mets
4.11 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
4.12 @@ -374,8 +374,8 @@
4.13 crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
4.14 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
4.15 " (let t_t = Take (F_F v_v = Integral f_f D v_v) " ^
4.16 - " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^
4.17 - " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_t) ")]
4.18 + " in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@ " ^
4.19 + " (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t) ")]
4.20 \<close>
4.21
4.22 end
4.23 \ No newline at end of file
5.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Dec 31 14:49:16 2018 +0100
5.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Jan 10 18:17:48 2019 +0100
5.3 @@ -1002,8 +1002,8 @@
5.4 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [],
5.5 nrls = norm_Rational},
5.6 "Script Solve_d0_polyeq_equation (e_e::bool) (v_v::real) = " ^
5.7 - "(let e_e = ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] " ^
5.8 - " d0_polyeq_simplify False))) e_e " ^
5.9 + "(let e_e = ((Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] " ^
5.10 + " ''d0_polyeq_simplify'' False))) e_e " ^
5.11 " in ((Or_to_List e_e)::bool list))")]
5.12 \<close>
5.13 setup \<open>KEStore_Elems.add_mets
6.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Mon Dec 31 14:49:16 2018 +0100
6.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Thu Jan 10 18:17:48 2019 +0100
6.3 @@ -236,8 +236,8 @@
6.4 "Calculate ''PLUS''";
6.5 val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.6 "Calculate1 ''PLUS''";
6.7 -val Rew $ (Free (_, IDtype)) $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.8 - "Rewrite real_diff_minus False t";
6.9 +val Rew $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.10 + "Rewrite ''real_diff_minus'' False t";
6.11 (*this is specific to ScrStep_inst ...*)
6.12 val Rew_Inst $ Subs $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory}))
6.13 "Rewrite_Inst [(''bdv'',v)] ''real_diff_minus'' False";
7.1 --- a/src/Tools/isac/ProgLang/termC.sml Mon Dec 31 14:49:16 2018 +0100
7.2 +++ b/src/Tools/isac/ProgLang/termC.sml Thu Jan 10 18:17:48 2019 +0100
7.3 @@ -22,7 +22,7 @@
7.4
7.5 val isalist2list: term -> term list
7.6 val list2isalist: typ -> term list -> term
7.7 - val isapair2pair: term -> term * term
7.8 + val isapair2pair: term -> term * term (* rename to dest_pair, compare HOLogic.dest_string *)
7.9
7.10 val is_atom: term -> bool
7.11 val is_bdv: string -> bool
8.1 --- a/test/Tools/isac/Interpret/mstools.sml Mon Dec 31 14:49:16 2018 +0100
8.2 +++ b/test/Tools/isac/Interpret/mstools.sml Thu Jan 10 18:17:48 2019 +0100
8.3 @@ -49,7 +49,7 @@
8.4 val t = case parseNEW ctxt "xxx = 123" of
8.5 NONE => error "mstools: syntax error"
8.6 | SOME t' => t';
8.7 -if ((lhs t) |> type_of) = @{typ int} then ()
8.8 +if ((Tools.lhs t) |> type_of) = @{typ int} then ()
8.9 else error "mstools: incorrect type inference from parseNEW ctxt";
8.10
8.11 val t_bit = Syntax.read_term ctxt "11::int";
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/test/Tools/isac/Interpret/specification-elems.sml Thu Jan 10 18:17:48 2019 +0100
9.3 @@ -0,0 +1,51 @@
9.4 +(* ~~/test/Tools/isac/Interpret/specification-elems.sml
9.5 + Author: Walther Neuper
9.6 + Use is subject to license terms.
9.7 +*)
9.8 +
9.9 +"-----------------------------------------------------------------------------";
9.10 +"-----------------------------------------------------------------------------";
9.11 +"table of contents -----------------------------------------------------------";
9.12 +"-----------------------------------------------------------------------------";
9.13 +"-------- fun subst_to_subst' ------------------------------------------------";
9.14 +"-------- fun subst'_to_sube -------------------------------------------------";
9.15 +"-------- fun subs2subst -----------------------------------------------------";
9.16 +"-------- fun subst2subs -----------------------------------------------------";
9.17 +"-----------------------------------------------------------------------------";
9.18 +"-----------------------------------------------------------------------------";
9.19 +
9.20 +"-------- fun subst_to_subst' ------------------------------------------------";
9.21 +"-------- fun subst_to_subst' ------------------------------------------------";
9.22 +"-------- fun subst_to_subst' ------------------------------------------------";
9.23 +val subst_rew =
9.24 + [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
9.25 + (@{term "bdv_2 :: real"}, @{term "y :: real"}),
9.26 + (@{term "bdv_3 :: real"}, @{term "z :: real"})];
9.27 +if term2str (subst_to_subst' subst_rew) = "[(''bdv_1'', x), (''bdv_2'', y), (''bdv_3'', z)]"
9.28 +then () else error "subst_to_subst' changed"
9.29 +
9.30 +"-------- fun subst'_to_sube -------------------------------------------------";
9.31 +"-------- fun subst'_to_sube -------------------------------------------------";
9.32 +"-------- fun subst'_to_sube -------------------------------------------------";
9.33 +val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
9.34 +if Selem.subst'_to_sube subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
9.35 +else error "subst'_to_sube changed";
9.36 +
9.37 +"-------- fun subs2subst -----------------------------------------------------";
9.38 +"-------- fun subs2subst -----------------------------------------------------";
9.39 +"-------- fun subs2subst -----------------------------------------------------";
9.40 +case subs2subst @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
9.41 + [(Free ("bdv_1", _), Free ("x", _)),
9.42 + (Free ("bdv_2", _), Free ("y", _)),
9.43 + (Free ("bdv_3", _), Free ("z", _))] => ()
9.44 +| _ => error "subs2subst changed";
9.45 +
9.46 +"-------- fun subst2subs -----------------------------------------------------";
9.47 +"-------- fun subst2subs -----------------------------------------------------";
9.48 +"-------- fun subst2subs -----------------------------------------------------";
9.49 +val subst_rew =
9.50 + [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
9.51 + (@{term "bdv_2 :: real"}, @{term "y :: real"}),
9.52 + (@{term "bdv_3 :: real"}, @{term "z :: real"})];
9.53 +if subst2subs subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"]then ()
9.54 +else error "subst2subs changed";
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/test/Tools/isac/Minisubpbl/450-Rewrite_Set_Inst.sml Thu Jan 10 18:17:48 2019 +0100
10.3 @@ -0,0 +1,34 @@
10.4 +(* Title: 450-Rewrite_Set_Inst.sml
10.5 + Author: Walther Neuper 1803
10.6 + (c) copyright due to lincense terms.
10.7 +*)
10.8 +
10.9 +"----------- Minisubplb/450-Rewrite_Set_Inst.sml -----------------";
10.10 +"----------- Minisubplb/450-Rewrite_Set_Inst.sml -----------------";
10.11 +"----------- Minisubplb/450-Rewrite_Set_Inst.sml -----------------";
10.12 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
10.13 +val (dI',pI',mI') =
10.14 + ("Test", ["sqroot-test","univariate","equation","test"],
10.15 + ["Test","squ-equ-test-subpbl1"]);
10.16 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
10.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
10.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
10.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
10.36 +case nxt of ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv")) => ()
10.37 +| _ => error "Rewrite_Set_Inst changed";
11.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Mon Dec 31 14:49:16 2018 +0100
11.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Thu Jan 10 18:17:48 2019 +0100
11.3 @@ -381,6 +381,25 @@
11.4 if term2str t = "Try (Rewrite_Set ''rearrange_assoc'' False)" then ()
11.5 else error "rule2stac Rls_.. changed";
11.6
11.7 +val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", num_str @{thm risolate_bdv_add}));
11.8 +if term2str t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'' False))" then ()
11.9 +else error "rule2stac_inst Thm.. changed";
11.10 +case t of
11.11 + (Const ("Script.Try", _) $
11.12 + (Const ("Script.Repeat", _) $
11.13 + (Const ("Script.Rewrite'_Inst", _) $
11.14 + (Const ("List.list.Cons", _) $
11.15 + (Const ("Product_Type.Pair", _) $
11.16 + bdv $
11.17 + Free ("v", _)) $
11.18 + Const ("List.list.Nil", _)) $
11.19 + risolate_bdv_add $
11.20 + Const ("HOL.False", _)))) =>
11.21 + (if HOLogic.dest_string bdv = "bdv" andalso
11.22 + HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
11.23 + else error "rule2stac_inst changed 1")
11.24 +| _ => error "rule2stac_inst changed 2"
11.25 +
11.26 "-------- fun op @@ ----------------------------------------------------------";
11.27 "-------- fun op @@ ----------------------------------------------------------";
11.28 "-------- fun op @@ ----------------------------------------------------------";
12.1 --- a/test/Tools/isac/Test_Isac.thy Mon Dec 31 14:49:16 2018 +0100
12.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jan 10 18:17:48 2019 +0100
12.3 @@ -112,6 +112,7 @@
12.4 open TermC; atomt;
12.5 open Celem; e_pbt;
12.6 open Rule; string_of_thm;
12.7 + open Tools; eval_lhs;
12.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.9 \<close>
12.10
12.11 @@ -160,22 +161,15 @@
12.12 ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
12.13 ML_file "Minisubpbl/300-init-subpbl.sml"
12.14 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
12.15 + ML_file "Minisubpbl/450-Rewrite_Set_Inst.sml"
12.16 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"
12.17 ML_file "Minisubpbl/500-met-sub-to-root.sml"
12.18 ML_file "Minisubpbl/530-error-Check_Elementwise.sml"
12.19 ML_file "Minisubpbl/600-postcond.sml"
12.20 ML \<open>"%%%%%%%%%%%%%%%%% end Minisubpbl.thy %%%%%%%%%%%%%%%%%%%%%%%";\<close>
12.21 ML \<open>"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";\<close>
12.22 -ML \<open>
12.23 -"~~~~~ fun , args:"; val () = ();
12.24 -\<close> ML \<open>
12.25 -Tools.lhs
12.26 -\<close> ML \<open>
12.27 -\<close> ML \<open>
12.28 -\<close> ML \<open>
12.29 -"~~~~~ fun , args:"; val () = ();
12.30 -\<close>
12.31 ML_file "Interpret/mstools.sml"
12.32 + ML_file "Interpret/specification-elems.sml"
12.33 ML_file "Interpret/ctree.sml" (*!...!see(25)*)
12.34 ML_file "Interpret/ptyps.sml" (* requires setup from ptyps.thy *)
12.35 ML \<open>(*check_unsynchronized_ref (); ==== trick on error: CUT AND PASTE THIS LINE =========*)\<close>
13.1 --- a/test/Tools/isac/Test_Some.thy Mon Dec 31 14:49:16 2018 +0100
13.2 +++ b/test/Tools/isac/Test_Some.thy Thu Jan 10 18:17:48 2019 +0100
13.3 @@ -57,21 +57,255 @@
13.4 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
13.5 \<close>
13.6
13.7 -section \<open>===================================================================================\<close>
13.8 +section \<open>"----------- initContext..Thy_, fun context_thm ---------"; interSteps OK, other error\<close>
13.9 ML \<open>
13.10 "~~~~~ fun , args:"; val () = ();
13.11 \<close> ML \<open>
13.12 -lhs
13.13 \<close> ML \<open>
13.14 \<close> ML \<open>
13.15 \<close> ML \<open>
13.16 "~~~~~ fun , args:"; val () = ();
13.17 \<close>
13.18
13.19 +
13.20 +section \<open> "----------- initContext Thy_ Integration-demo ----------"; \<close>
13.21 +ML \<open>
13.22 +"~~~~~ fun , args:"; val () = ();
13.23 +\<close> ML \<open>
13.24 +"----------- initContext Thy_ Integration-demo ----------";
13.25 +"----------- initContext Thy_ Integration-demo ----------";
13.26 +"----------- initContext Thy_ Integration-demo ----------";
13.27 +reset_states ();
13.28 +CalcTree
13.29 +[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
13.30 + ("Integrate",["integrate","function"],
13.31 + ["diff","integration"]))];
13.32 +Iterator 1;
13.33 +moveActiveRoot 1;
13.34 +autoCalculate 1 CompleteCalc;
13.35 +(**)val ((pt,p),_) = get_calc 1;
13.36 +(**)\<close> ML \<open>
13.37 +(**)show_pt pt;
13.38 +(**)(*isabisac = isabisacREP
13.39 +[
13.40 +(([], Frm), Integrate (2 * x, x)),
13.41 +(([1], Frm), Integral 2 * x D x),
13.42 +(([1], Res), c + x ^^^ 2),
13.43 +(([], Res), c + x ^^^ 2)]
13.44 +val it = (): unit*)
13.45 +(**)\<close> ML \<open>
13.46 +interSteps 1 ([1],Res);
13.47 +(**)\<close> ML \<open>
13.48 +(**)val ((pt,p),_) = get_calc 1;
13.49 +(**)\<close> ML \<open>
13.50 +(**)show_pt pt;
13.51 +(**)(*isabisac = isabisacREP
13.52 +[
13.53 +(([], Frm), Integrate (2 * x, x)),
13.54 +(([1], Frm), Integral 2 * x D x),
13.55 +(([1,1], Frm), Integral 2 * x D x),
13.56 +(([1,1], Res), 2 * (x ^^^ 2 / 2)),
13.57 +(([1,2], Res), 2 * (x ^^^ 2 / 2) + c),
13.58 +(([1,3], Res), c + x ^^^ 2),
13.59 +(([1], Res), c + x ^^^ 2),
13.60 +(([], Res), c + x ^^^ 2)]
13.61 +val it = (): unit*)
13.62 +(**)
13.63 +\<close> ML \<open>
13.64 +interSteps 1 ([1,1],Res); (* doesn't create steps; inhibit writing calcstate *)
13.65 +(**)\<close> ML \<open>
13.66 +(**)val ((pt,p),_) = get_calc 1;
13.67 +(**)\<close> ML \<open>
13.68 +(**)show_pt pt;
13.69 +\<close> ML \<open>
13.70 +\<close> ML \<open>
13.71 +\<close> ML \<open>
13.72 +\<close> ML \<open>
13.73 +\<close> ML \<open>
13.74 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1,1],Res));
13.75 +\<close> ML \<open>
13.76 +val ((pt, p), tacis) = get_calc cI
13.77 +\<close> ML \<open>
13.78 +(*if*) (not o is_interpos) ip (*isabisac = isabisacREP = false *);
13.79 +\<close> ML \<open>
13.80 +val ip' = lev_pred' pt ip
13.81 +\<close> ML \<open>
13.82 +(*val ("detailrls", pt, lastpos) = case*) Math_Engine.detailstep pt ip (*of*)
13.83 +\<close> ML \<open>
13.84 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
13.85 +\<close> ML \<open>
13.86 +p = [1, 1] (*isabisac = isabisacREP = true *)
13.87 +\<close> ML \<open>
13.88 + val nd = Ctree.get_nd pt p
13.89 +\<close> ML \<open>
13.90 +(**)show_pt nd(*isabisac = isabisacREP
13.91 +[
13.92 +(([], Frm), Integral 2 * x D x)]
13.93 +val it = (): unit*)
13.94 +\<close> ML \<open>
13.95 + val cn = Ctree.children nd
13.96 +\<close> ML \<open>
13.97 +\<close> ML \<open>
13.98 +\<close> ML \<open>
13.99 +(*if*) null cn (*isabisac = isabisacREP = true *);
13.100 +\<close> ML \<open>
13.101 +(*if*) (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
13.102 + (*isabisac = isabisacREP = true*);
13.103 +\<close> ML \<open>
13.104 +Solve.detailrls pt pos
13.105 +\<close> ML \<open>
13.106 +"~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);
13.107 +\<close> ML \<open>
13.108 + val t = get_obj g_form pt p
13.109 + val tac = get_obj g_tac pt p
13.110 + val rls = (assoc_rls o Tac.rls_of) tac
13.111 + val ctxt = get_ctxt pt pos
13.112 +\<close> ML \<open>
13.113 +case rls of Rls _ => ()
13.114 +\<close> ML \<open>
13.115 + val is = Generate.init_istate tac t
13.116 + (*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
13.117 + is wrong for simpl, but working ?!? *)
13.118 + val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
13.119 + val pos' = ((lev_on o lev_dn) p, Frm)
13.120 + val thy = Celem.assoc_thy "Isac"
13.121 + val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
13.122 +\<close> ML \<open>
13.123 +(* val (_,_, (pt'', _)) =*) complete_solve CompleteSubpbl [] (pt', pos')
13.124 +\<close> ML \<open>
13.125 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_, p_)))) =
13.126 + (CompleteSubpbl, [], (pt', pos'));
13.127 +\<close> ML \<open>
13.128 +(*if*) p = ([], Res) (*isabisac = isabisacREP = false*);
13.129 +\<close> ML \<open>
13.130 +(*if*) member op = [Pbl,Met] p_ (*isabisac = isabisacREP = false*);
13.131 +\<close> ML \<open>
13.132 +(*case*) nxt_solve_ ptp (*of*) (*
13.133 +isabisac
13.134 +exception TYPE raised..: Illegal type for constant "Script.Rewrite'_Inst" ::
13.135 +isabisacREP
13.136 + = ([(Rewrite_Inst (["(bdv, x)"], ("integral_mult", ...
13.137 +*)
13.138 +\<close> ML \<open>
13.139 +"~~~~~ and nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (ptp);
13.140 +\<close> ML \<open>
13.141 +(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*isabisac = isabisac? = false*);
13.142 +\<close> ML \<open>
13.143 + val thy' = get_obj g_domID pt (par_pblobj pt p);
13.144 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
13.145 +\<close> ML \<open>
13.146 +(* val (tac_, is, (t, _)) =*) Lucin.next_tac (thy', srls) (pt, pos) sc is;
13.147 +\<close> ML \<open>
13.148 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog (_ $ body)),
13.149 + (Selem.ScrState (E,l,a,v,s,_), ctxt)) =
13.150 + ((thy', srls), (pt, pos), sc, is);
13.151 +\<close> ML \<open>
13.152 +(*if*) l = [] (*isabisac = isabisac? = true*);
13.153 +\<close> ML \<open>
13.154 +appy thy ptp E [Celem.R] body NONE v
13.155 +\<close> ML \<open>
13.156 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
13.157 + (thy, ptp, E, [Celem.R], body, NONE, v);
13.158 +\<close> ML \<open>
13.159 +appy thy ptp E (l @ [Celem.R]) e a v
13.160 +\<close> ML \<open>
13.161 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*2*),_) $ e1 $ e2 $ a), _, v) =
13.162 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
13.163 +\<close> ML \<open>
13.164 +val Skip (v,E) = (*case*) appy thy ptp E (l @ [Celem.L, Celem.L, Celem.R]) e1 (SOME a) v (*of*)
13.165 +\<close> ML \<open>
13.166 +appy thy ptp E (l @ [Celem.L, Celem.R]) e2 (SOME a) v
13.167 +\<close> ML \<open>
13.168 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2), a, v) =
13.169 + (thy, ptp, E, (l @ [Celem.L, Celem.R]), e2, (SOME a), v);
13.170 +\<close> ML \<open>
13.171 +val Skip (v,E) = (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v (*of*)
13.172 +\<close> ML \<open>
13.173 +appy thy ptp E (l @ [Celem.R]) e2 a v
13.174 +\<close> ML \<open>
13.175 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2), a, v) =
13.176 + (thy, ptp, E, (l @ [Celem.R]), e2, a, v);
13.177 +\<close> ML \<open>
13.178 +val Skip (v,E) = (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v (*of*)
13.179 +\<close> ML \<open>
13.180 +appy thy ptp E (l @ [Celem.R]) e2 a v
13.181 +\<close> ML \<open>
13.182 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Seq"(*1*),_) $ e1 $ e2), a, v) =
13.183 + (thy, ptp, E, (l @ [Celem.R]), e2, a, v);
13.184 +\<close> ML \<open>
13.185 +(*isabisac exn*) (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e1 a v (*of*)
13.186 +\<close> ML \<open>
13.187 +"~~~~~ fun appy, args:"; val (thy, ptp, E, l, (Const ("Script.Try"(*1*),_) $ e), a, v) =
13.188 + (thy, ptp, E, (l @ [Celem.L, Celem.R]), e1, a, v);
13.189 +\<close> ML \<open>
13.190 +(*case*) appy thy ptp E (l @ [Celem.R]) e a v (*of*)
13.191 +\<close> ML \<open>
13.192 +"~~~~~ fun , args:"; val (thy, ptp, E, l, (Const ("Script.Repeat"(*2*),_) $ e), a, v) =
13.193 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
13.194 +\<close> ML \<open>
13.195 +appy thy ptp E (l @ [Celem.R]) e a v
13.196 +\<close> ML \<open>
13.197 +"~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) =
13.198 + (thy, ptp, E, (l @ [Celem.R]), e, a, v);
13.199 +\<close> ML \<open>
13.200 +val (a', LTool.STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*)
13.201 +\<close> ML \<open>
13.202 +val (m,m') = stac2tac_ pt (Celem.assoc_thy th) stac
13.203 +\<close> ML \<open>
13.204 +case m of Rewrite_Inst _ => ()
13.205 +\<close> ML \<open>
13.206 +val Chead.Appl m' = (*case*) Applicable.applicable_in p pt m (*of*)
13.207 +\<close> ML \<open>
13.208 +(Appy (m', (E,l,a',tac_2res m',Selem.Sundef,false)))
13.209 +\<close> ML \<open>
13.210 +tac_2res m'
13.211 +\<close> ML \<open>
13.212 +m'
13.213 +\<close> ML \<open>
13.214 +"~~~~~ fun tac_2res, args:"; val (m') = (m');
13.215 +\<close> ML \<open>
13.216 +rep_tac_: tac_ -> rule * (term * term);
13.217 +\<close> ML \<open>
13.218 +rep_tac_ m'
13.219 +\<close> ML \<open>
13.220 +"~~~~~ fun rep_tac_, args:"; val (Tac.Rewrite_Inst' (thy', _, _, put, subs, (thmID, _), f, (f', _)))
13.221 + = (m');
13.222 +\<close> ML \<open>
13.223 + val b = @{term False};
13.224 + val subs' = Selem.subst_to_subst' subs;
13.225 + val sT' = type_of subs';
13.226 + val fT = type_of f;
13.227 + val lhs = Const ("Script.Rewrite'_Inst", [sT', HOLogic.stringT, HOLogic.boolT, fT] ---> fT)
13.228 + $ subs' $ HOLogic.mk_string thmID $ b $ f;
13.229 +(((make_rule (Celem.assoc_thy thy')) o HOLogic.mk_eq) (lhs, f'), (lhs, f'))
13.230 +\<close> ML \<open>
13.231 +\<close> ML \<open>
13.232 +\<close> ML \<open>
13.233 +\<close> ML \<open>
13.234 +\<close> ML \<open>
13.235 +\<close> ML \<open>
13.236 +\<close> ML \<open>
13.237 +\<close> ML \<open>
13.238 +\<close> ML \<open>
13.239 +\<close> ML \<open>
13.240 +\<close> ML \<open>
13.241 +"~~~~~ fun , args:"; val () = ();
13.242 +\<close> ML \<open>
13.243 +\<close> ML \<open> (*----------------- end insertion ---------------------------------------------*)
13.244 +val ((pt,p),_) = get_calc 1;
13.245 +if existpt' ([1,1,1], Frm) pt then ()
13.246 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
13.247 +initContext 1 Thy_ ([1,1,1], Frm);
13.248 +\<close> ML \<open>
13.249 +"~~~~~ fun , args:"; val () = ();
13.250 +\<close>
13.251 +
13.252 section \<open>===================================================================================\<close>
13.253 ML \<open>
13.254 "~~~~~ fun , args:"; val () = ();
13.255 \<close> ML \<open>
13.256 +
13.257 +\<close> ML \<open>
13.258 \<close> ML \<open>
13.259 \<close> ML \<open>
13.260 "~~~~~ fun , args:"; val () = ();
13.261 @@ -81,11 +315,14 @@
13.262 ML \<open>
13.263 "~~~~~ fun , args:"; val () = ();
13.264 \<close> ML \<open>
13.265 +
13.266 +\<close> ML \<open>
13.267 \<close> ML \<open>
13.268 \<close> ML \<open>
13.269 "~~~~~ fun , args:"; val () = ();
13.270 \<close>
13.271
13.272 +
13.273 section \<open>code for copy & paste ===============================================================\<close>
13.274 ML \<open>
13.275 "~~~~~ fun , args:"; val () = ();
14.1 --- a/zcoding-to-test.sh Mon Dec 31 14:49:16 2018 +0100
14.2 +++ b/zcoding-to-test.sh Thu Jan 10 18:17:48 2019 +0100
14.3 @@ -7,4 +7,5 @@
14.4 cd ../../../ # go back to ~~/.
14.5
14.6 # immediately go to testing
14.7 -./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
14.8 +./bin/isabelle jedit -l Isac test/Tools/isac/Test_Some.thy &
14.9 +#./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &