1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Dec 05 15:29:36 2012 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Dec 05 15:56:38 2012 +0100
1.3 @@ -1266,7 +1266,7 @@
1.4 ],_
1.5 ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
1.6
1.7 - val Script sc
1.8 + val Prog sc
1.9 = (#scr o get_met) ["SignalProcessing",
1.10 "Z_Transform",
1.11 "Inverse"];
1.12 @@ -1341,7 +1341,7 @@
1.13 \item Do we have the right Script \ldots difference in the
1.14 arguments in the arguments\ldots
1.15 \begin{verbatim}
1.16 - val Script s =
1.17 + val Prog s =
1.18 (#scr o get_met) ["SignalProcessing",
1.19 "Z_Transform",
1.20 "Inverse"];
1.21 @@ -1625,7 +1625,7 @@
1.22 \item Type-checking can be very tedious. One might even inspect the
1.23 parse-tree of the program with {\sisac}'s specific debug tools:
1.24 \begin{verbatim}
1.25 - val {scr = Script t,...} =
1.26 + val {scr = Prog t,...} =
1.27 get_met ["simplification",
1.28 "of_rationals",
1.29 "to_partial_fraction"];
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Dec 05 15:29:36 2012 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Wed Dec 05 15:56:38 2012 +0100
2.3 @@ -2390,7 +2390,7 @@
2.4 \item Do we have the right Script \ldots difference in the
2.5 arguments in the arguments\ldots
2.6 \begin{verbatim}
2.7 - val Script s =
2.8 + val Prog s =
2.9 (#scr o get_met) ["SignalProcessing",
2.10 "Z_Transform",
2.11 "Inverse"];
2.12 @@ -2697,7 +2697,7 @@
2.13 \item Type-checking can be very tedious. One might even inspect the
2.14 parse-tree of the program with {\sisac}'s specific debug tools:
2.15 \begin{verbatim}
2.16 - val {scr = Script t,...} =
2.17 + val {scr = Prog t,...} =
2.18 get_met ["simplification",
2.19 "of_rationals",
2.20 "to_partial_fraction"];
3.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Dec 05 15:29:36 2012 +0100
3.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Dec 05 15:56:38 2012 +0100
3.3 @@ -45,9 +45,9 @@
3.4 "--------- appendFormula: on Res + equ_nrls ----------------------";
3.5 "--------- appendFormula: on Res + equ_nrls ----------------------";
3.6
3.7 - val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
3.8 + val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
3.9 (writeln o term2str) sc;
3.10 - val Script sc = (#scr o get_met) ["Test","solve_linear"];
3.11 + val Prog sc = (#scr o get_met) ["Test","solve_linear"];
3.12 (writeln o term2str) sc;
3.13
3.14 states:=[];
3.15 @@ -874,7 +874,7 @@
3.16 val (res, inf) =
3.17 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
3.18 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
3.19 -val {errpats, nrls = rls, scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"]
3.20 +val {errpats, nrls = rls, scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"]
3.21
3.22 val env = [(str2term "v_v", str2term "x")];
3.23 val errpats =
3.24 @@ -937,7 +937,7 @@
3.25 val msg_calcstate' = compare_step ([], [], (pt, pos_pred)) f_in
3.26 val ("no derivation found", calcstate') = msg_calcstate';
3.27 val pp = par_pblobj pt p
3.28 - val {errpats, nrls, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
3.29 + val {errpats, nrls, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
3.30 val ScrState (env, _, _, _, _, _) = get_istate pt pos;
3.31 case check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
3.32 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
3.33 @@ -976,7 +976,7 @@
3.34 "~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
3.35 val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
3.36 val pp = par_pblobj pt p
3.37 - val {errpats, scr = Script prog, ...} = get_met (get_obj g_metID pt pp)
3.38 + val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
3.39 val ScrState (env, _, _, _, _, _) = get_istate pt pos
3.40 val subst = get_bdv_subst prog env
3.41 val errpatthms = errpats
4.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Dec 05 15:29:36 2012 +0100
4.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Dec 05 15:56:38 2012 +0100
4.3 @@ -569,7 +569,7 @@
4.4 "-------- build fun get_bdv_subst --------------------------------";
4.5 "-------- build fun get_bdv_subst --------------------------------";
4.6 "-------- build fun get_bdv_subst --------------------------------";
4.7 -val {scr = Script prog, ...} = get_met ["diff", "differentiate_on_R"];
4.8 +val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
4.9 val env = [(str2term "v_v", str2term "x")];
4.10 subst2str env = "[\"\n(v_v, x)\"]";
4.11
5.1 --- a/test/Tools/isac/Interpret/script.sml Wed Dec 05 15:29:36 2012 +0100
5.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Dec 05 15:56:38 2012 +0100
5.3 @@ -77,7 +77,7 @@
5.4 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
5.5 atomty sc';
5.6
5.7 -val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
5.8 +val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
5.9 (*---------------------------------------------------------------------
5.10 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
5.11 ---------------------------------------------------------------------*)
5.12 @@ -114,7 +114,7 @@
5.13 " in True)"
5.14 ;
5.15
5.16 -val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
5.17 +val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
5.18 (*---------------------------------------------------------------------
5.19 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
5.20 ---------------------------------------------------------------------*)
5.21 @@ -297,7 +297,7 @@
5.22 val thy = assoc_thy thy';
5.23 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
5.24 val ini = init_form thy sc env;
5.25 -"----- fun init_form, args:"; val (Script sc) = sc;
5.26 +"----- fun init_form, args:"; val (Prog sc) = sc;
5.27 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
5.28 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
5.29 | _ => error "script: Const (?, ?) in script (as term) changed";;
5.30 @@ -333,7 +333,7 @@
5.31 (*WAS stac2tac_ TODO: no match for SubProblem*)
5.32 val thy' = get_obj g_domID pt (par_pblobj pt p);
5.33 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
5.34 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
5.35 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
5.36 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
5.37 l; (*= [R, L, R, L, R, R]*)
5.38 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
5.39 @@ -385,7 +385,7 @@
5.40 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
5.41 val d = e_rls (*FIXME: get simplifier from domID*);
5.42 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
5.43 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
5.44 + (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
5.45 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
5.46 val thy = assoc_thy thy';
5.47 l = [] orelse ((*init.in solve..Apply_Method...*)
5.48 @@ -423,19 +423,19 @@
5.49 val (p'''', pt'''') = (p, pt);
5.50 f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation";
5.51 val (p, p_) = p(* = ([1], Frm)*);
5.52 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.53 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.54 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
5.55 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
5.56 loc_ = [];
5.57 curry_arg = NONE;
5.58 term2str res = "??.empty"; (* scrstate before starting interpretation *)
5.59 -(*term2str (go loc_ sc) = "Script Solve_root_equation e_e v_v = ...*)
5.60 +(*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)
5.61
5.62 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
5.63 val (p'''', pt'''') = (p, pt);
5.64 f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
5.65 val (p, p_) = p(* = ([1], Res)*);
5.66 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.67 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.68 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
5.69 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
5.70 loc_ = [R, L, R, L, L, R, R];
5.71 @@ -447,7 +447,7 @@
5.72 val (p'''', pt'''') = (p, pt);
5.73 f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
5.74 val (p, p_) = p(* = ([2], Res)*);
5.75 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.76 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.77 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
5.78 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
5.79 loc_ = [R, L, R, L, R, R];
5.80 @@ -476,19 +476,19 @@
5.81 val (p'''', pt'''') = (p, pt);
5.82 f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
5.83 val (p, p_) = p(* = ([3, 1], Frm)*);
5.84 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.85 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.86 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
5.87 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
5.88 loc_ = [];
5.89 curry_arg = NONE;
5.90 term2str res = "??.empty"; (* scrstate before starting interpretation *)
5.91 -(*term2str (go loc_ sc) = "Script Solve_linear e_e v_v = ...*)
5.92 +(*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)
5.93
5.94 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
5.95 val (p'''', pt'''') = (p, pt);
5.96 f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
5.97 val (p, p_) = p(* = ([3, 1], Res)*);
5.98 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.99 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
5.100 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
5.101 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
5.102 loc_ = [R, L, R, L, R, L, R];
5.103 @@ -582,7 +582,7 @@
5.104 if metID = e_metID
5.105 then (thd3 o snd3) (get_obj g_origin pt pp)
5.106 else metID
5.107 - val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
5.108 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
5.109 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
5.110 val alltacs = (*we expect at least 1 stac in a script*)
5.111 map ((stac2tac pt thy) o rep_stacexpr o #2 o
6.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Dec 05 15:29:36 2012 +0100
6.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Dec 05 15:56:38 2012 +0100
6.3 @@ -76,7 +76,7 @@
6.4 Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
6.5
6.6 Calc ("Atools.ident",eval_ident "#ident_")],
6.7 - scr = Script ((term_of o the o (parse thy))
6.8 + scr = Prog ((term_of o the o (parse thy))
6.9 "empty_script")
6.10 }:rls
6.11 )]);
7.1 --- a/test/Tools/isac/Knowledge/inssort.sml Wed Dec 05 15:29:36 2012 +0100
7.2 +++ b/test/Tools/isac/Knowledge/inssort.sml Wed Dec 05 15:56:38 2012 +0100
7.3 @@ -117,11 +117,11 @@
7.4
7.5
7.6 (* ------- 17.6.00: mit kleinen problemen aufgegeben
7.7 -val scr=Script ((term_of o the o (parse thy))
7.8 +val scr=Prog ((term_of o the o (parse thy))
7.9 "Script Sort (u_::'a list) = \
7.10 \ Rewrite_Set ins_sort False u_");
7.11
7.12 -val scr=Script ((term_of o the o (parse thy))
7.13 +val scr=Prog ((term_of o the o (parse thy))
7.14 "Script Ins_sort (u_::real list) = \
7.15 \ (let u_ = Rewrite sort_def False u_; \
7.16 \ u_ = Rewrite foldr_rec False u_; \
8.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Dec 05 15:29:36 2012 +0100
8.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Dec 05 15:56:38 2012 +0100
8.3 @@ -348,7 +348,7 @@
8.4 val {ppc,...} = get_pbt ["named","integrate","function"];
8.5 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
8.6 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
8.7 -val {scr = Script sc,... } = get_met ["diff","integration","named"];
8.8 +val {scr = Prog sc,... } = get_met ["diff","integration","named"];
8.9 val [_,_, F2_] = formal_args sc;
8.10 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
8.11
9.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Dec 05 15:29:36 2012 +0100
9.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Dec 05 15:56:38 2012 +0100
9.3 @@ -195,13 +195,13 @@
9.4 (*locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;
9.5 WAS: not-found-in-script: NotLocatable from NasNap (Const ("List...*)
9.6 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
9.7 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
9.8 + (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
9.9 ((thy',srls), m ,(pt,(p,p_)) ,(sc,d) ,is); (* locate_gen 2nd pattern *)
9.10 val thy = assoc_thy thy';
9.11 l = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*false*);
9.12 (*WAS val NasApp _ =(astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) )
9.13 ... Assoc ... is correct*)
9.14 -"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
9.15 +"~~~~~ and astep_up, args:"; val ((ys as (_,_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
9.16 ((thy',ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]));
9.17 1 < length l (*true*);
9.18 val up = drop_last l;
9.19 @@ -209,7 +209,7 @@
9.20 (go up sc);
9.21 (*WAS val NasNap _ = ass_up ys ((E,up,a,v,S,b),ss) (go up sc)
9.22 ... ???? ... is correct*)
9.23 -"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Script sc,d)), (is as (E,l,a,v,S,b),ss),
9.24 +"~~~~~ fun ass_up, args:"; val ((ys as (y,ctxt,s,Prog sc,d)), (is as (E,l,a,v,S,b),ss),
9.25 (Const ("HOL.Let",_) $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
9.26 val l = drop_last l; (*comes from e, goes to Abs*)
9.27 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go l sc;
10.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Dec 05 15:29:36 2012 +0100
10.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Wed Dec 05 15:56:38 2012 +0100
10.3 @@ -104,15 +104,15 @@
10.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.5 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
10.6 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
10.7 - (sc as Script (h $ body)),
10.8 + (sc as Prog (h $ body)),
10.9 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
10.10 -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
10.11 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
10.12 (thy, ptp, sc, E, l, Skip_, a, v);
10.13 1 < length l; (*true*)
10.14 val up = drop_last l;
10.15 go up sc; (* = Const ("HOL.Let", *)
10.16 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
10.17 - (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
10.18 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
10.19 + (t as Const ("HOL.Let",_) $ _), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
10.20 ay = Napp_; (*false*)
10.21 val up = drop_last l;
10.22 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc; (*Const ("Script.SubProblem",..*)
10.23 @@ -291,30 +291,30 @@
10.24 val thy' = get_obj g_domID pt (par_pblobj pt p);
10.25 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
10.26 "~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'),
10.27 - (sc as Script (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
10.28 + (sc as Prog (h $ body)), (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
10.29 l = []; (* = false*)
10.30 -"~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
10.31 +"~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
10.32 (thy, ptp, sc, E, l, Skip_, a, v);
10.33 1 < length l; (* = true*)
10.34 val up = drop_last l;
10.35 (*val (t as Abs (_,_,_)) = *)(go up sc);
10.36 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay, (t as Abs (_,_,_)), a, v) =
10.37 - (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
10.38 + (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
10.39 term2str t = "%L_La. Check_elementwise L_L {v_v. Assumptions}";
10.40 -"~~~~~ and nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
10.41 +"~~~~~ and nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
10.42 (thy, ptp, scr, E, l, ay, a, v);
10.43 1 < length l; (* = true*)
10.44 val up = drop_last l;
10.45 (*val (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))) = *)(go up sc);
10.46 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay,
10.47 - (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
10.48 + (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
10.49
10.50 term2str t = "let L_La =\n SubProblem (RatEq', [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
10.51
10.52 (* comment from BEFORE Isabelle2002 --> 2011:
10.53 -nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
10.54 +nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
10.55 nstep_up thy ptp scr E l ay a v;
10.56 -nxt_up thy ptp (Script sc) E up ay (go up sc) a v;
10.57 +nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
10.58 nstep_up thy ptp sc E l Skip_ a v;
10.59 next_tac (thy',srls) (pt,pos) sc is;
10.60 nxt_solve_ (pt,ip);
11.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Dec 05 15:29:36 2012 +0100
11.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Dec 05 15:56:38 2012 +0100
11.3 @@ -35,7 +35,7 @@
11.4 val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
11.5 "~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
11.6 val actuals = itms2args thy metID itms
11.7 - val scr as Script sc = (#scr o get_met) metID
11.8 + val scr as Prog sc = (#scr o get_met) metID
11.9 val formals = formal_args sc
11.10 (*expects same sequence of (actual) args in itms and (formal) args in met*)
11.11 fun relate_args env [] [] = env
12.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Dec 05 15:29:36 2012 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Wed Dec 05 15:56:38 2012 +0100
12.3 @@ -36,14 +36,14 @@
12.4 val d = e_rls; (*FIXME.WN0108: canon.simplifier for domain is missing: generate from domID?*)
12.5 (*val Steps (is', ss as (m',f',pt',p',c')::_) = locate_gen (thy',srls) m (pt,(p,p_)) (sc,d) is;*)
12.6 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
12.7 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
12.8 + (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
12.9 ((thy',srls), m, (pt,(p,p_)), (sc,d), is);
12.10 val thy = assoc_thy thy';
12.11 l = [] orelse ((*init.in solve..Apply_Method...*)
12.12 (last_elem o fst) p = 0 andalso snd p = Res) (*false*);
12.13 (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
12.14 (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
12.15 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Script sc,_)), ((E,l,a,v,S,b),ss)) =
12.16 +"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
12.17 ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
12.18 1 < length l (*true*);
12.19 val up = drop_last l;
13.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Dec 05 15:29:36 2012 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Wed Dec 05 15:56:38 2012 +0100
13.3 @@ -64,7 +64,7 @@
13.4 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
13.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
13.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
13.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
13.8 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
13.9 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
13.10 val ctxt = get_ctxt pt pos;
13.11 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
14.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Dec 05 15:29:36 2012 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Wed Dec 05 15:56:38 2012 +0100
14.3 @@ -55,19 +55,19 @@
14.4 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
14.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
14.6 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
14.7 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Script (h $ body)),
14.8 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt, pos as (p, _)):ptree * pos'), (sc as Prog (h $ body)),
14.9 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
14.10 val ctxt = get_ctxt pt pos
14.11 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
14.12 l; (*= [R, R, D, L, R]*)
14.13 -"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Script sc), E, l, ay, a, v) =
14.14 +"~~~~~ fun nstep_up, args:"; val (thy, ptp, (Prog sc), E, l, ay, a, v) =
14.15 (thy, ptp, sc, E, l, Skip_, a, v);
14.16 1 < length l; (*true*)
14.17 val up = drop_last l;
14.18 go up sc; (* = Const ("HOL.Let", *)
14.19 -"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Script sc)), E, l, ay,
14.20 +"~~~~~ fun nxt_up, args:"; val (thy, ptp, (scr as (Prog sc)), E, l, ay,
14.21 (t as Const ("HOL.Let",_) $ _), a, v) =
14.22 -(thy, ptp, (Script sc), E, up, ay, (go up sc), a, v);
14.23 +(thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
14.24 ay = Napp_; (*false*)
14.25 val up = drop_last l;
14.26 val (Const ("HOL.Let",_) $ e $ (Abs (i,T,body))) = go up sc;
15.1 --- a/test/Tools/isac/OLDTESTS/script.sml Wed Dec 05 15:29:36 2012 +0100
15.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Wed Dec 05 15:56:38 2012 +0100
15.3 @@ -247,7 +247,7 @@
15.4 " --- test100: nxt_tac order------------------------------------ ";
15.5 " --- test100: nxt_tac order------------------------------------ ";
15.6
15.7 -val scr as (Script sc) = Script (((inst_abs Test.thy)
15.8 +val scr as (Prog sc) = Prog (((inst_abs Test.thy)
15.9 o term_of o the o (parse thy))
15.10 "Script Testeq (e_e::bool) = \
15.11 \(While (contains_root e_e) Do \
15.12 @@ -281,15 +281,15 @@
15.13 *)
15.14
15.15
15.16 -val scr as (Script sc) =
15.17 - Script (((inst_abs Test.thy) o term_of o the o (parse thy))
15.18 +val scr as (Prog sc) =
15.19 + Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
15.20 "Script Testterm (g_::real) = (Calculate cancel g_)");
15.21 (*
15.22 -val scr as (Script sc) =
15.23 - Script (((inst_abs Test.thy) o term_of o the o (parse thy))
15.24 +val scr as (Prog sc) =
15.25 + Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
15.26 "Script Testterm (g_::real) = (Calculate power g_)");
15.27 -val scr as (Script sc) =
15.28 - Script (((inst_abs Test.thy) o term_of o the o (parse thy))
15.29 +val scr as (Prog sc) =
15.30 + Prog (((inst_abs Test.thy) o term_of o the o (parse thy))
15.31 "Script Testterm (g_::real) = (Calculate pow g_)");
15.32 ..............................................................*)
15.33 writeln
16.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Dec 05 15:29:36 2012 +0100
16.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Wed Dec 05 15:56:38 2012 +0100
16.3 @@ -123,7 +123,7 @@
16.4 "boolTestFind v_i_"];
16.5 val (dI',pI',mI') = ("Test",["met_testeq","tests"],
16.6 ["Test","testeq1"]);
16.7 -val Script sc = (#scr o get_met) ["Test","testeq1"];
16.8 +val Prog sc = (#scr o get_met) ["Test","testeq1"];
16.9 atomt sc;
16.10 (*val p = e_pos'; val c = [];
16.11 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
16.12 @@ -176,7 +176,7 @@
16.13 \ e_e)\
16.14 \in [e_::bool])"
16.15 ));
16.16 -val Script sc = (#scr o get_met) ["Test","testlet"];
16.17 +val Prog sc = (#scr o get_met) ["Test","testlet"];
16.18 writeln(term2str sc);
16.19 val fmz = ["boolTestGiven (sqrt a = 0)",
16.20 "boolTestFind v_i_"];
16.21 @@ -211,7 +211,7 @@
16.22 val (dI',pI',mI') =
16.23 ("Test",["sqroot-test","univariate","equation","test"],
16.24 ["Test","sqrt-equ-test"]);
16.25 -val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
16.26 +val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];
16.27 writeln(term2str sc);
16.28
16.29 "--- s1 ---";
16.30 @@ -315,7 +315,7 @@
16.31 val (dI',pI',mI') =
16.32 ("Test",["sqroot-test","univariate","equation","test"],
16.33 ["Test","sqrt-equ-test"]);
16.34 - val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
16.35 + val Prog sc = (#scr o get_met) ["Test","sqrt-equ-test"];
16.36 (writeln o term2str) sc;
16.37 "--- s1 ---";
16.38 (*val p = e_pos'; val c = [];
16.39 @@ -485,7 +485,7 @@
16.40
16.41
16.42 (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
16.43 -val scr = Script (((inst_abs thy) o term_of o the o (parse thy))
16.44 +val scr = Prog (((inst_abs thy) o term_of o the o (parse thy))
16.45 "Script Biquadrat_poly (e_e::bool) (v_::real) = \
16.46 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
16.47 \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \
17.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Wed Dec 05 15:29:36 2012 +0100
17.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Wed Dec 05 15:56:38 2012 +0100
17.3 @@ -27,7 +27,7 @@
17.4 ("Test",["sqroot-test","univariate","equation","test"],
17.5 ["Test","squ-equ-test-subpbl1"]);
17.6
17.7 -val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
17.8 +val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
17.9 (writeln o term2str) sc;
17.10
17.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
17.12 @@ -112,7 +112,7 @@
17.13 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
17.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.15 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
17.16 - val Script sc = (#scr o get_met) ["Test","solve_linear"];
17.17 + val Prog sc = (#scr o get_met) ["Test","solve_linear"];
17.18 (writeln o term2str) sc;
17.19 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
17.20 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
17.21 @@ -294,7 +294,7 @@
17.22 val (dI',pI',mI') =
17.23 ("Test",["sqroot-test","univariate","equation","test"],
17.24 ["Test","square_equation2"]);
17.25 -val Script sc = (#scr o get_met) ["Test","square_equation2"];
17.26 +val Prog sc = (#scr o get_met) ["Test","square_equation2"];
17.27 (writeln o term2str) sc;
17.28
17.29 (*val p = e_pos'; val c = [];
17.30 @@ -363,7 +363,7 @@
17.31
17.32
17.33
17.34 -val Script s = (#scr o get_met) ["Test","square_equation"];
17.35 +val Prog s = (#scr o get_met) ["Test","square_equation"];
17.36 atomt s;
17.37
17.38
17.39 @@ -437,7 +437,7 @@
17.40 val (dI',pI',mI') =
17.41 ("Test",["squareroot","univariate","equation","test"],
17.42 ["Test","square_equation"]);
17.43 - val Script sc = (#scr o get_met) ["Test","square_equation"];
17.44 + val Prog sc = (#scr o get_met) ["Test","square_equation"];
17.45 (writeln o term2str) sc;
17.46
17.47 (*val p = e_pos'; val c = [];
18.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Wed Dec 05 15:29:36 2012 +0100
18.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Wed Dec 05 15:56:38 2012 +0100
18.3 @@ -17,7 +17,7 @@
18.4 "-------- test auto-generated script '(Repeat (Calculate times))'-";
18.5 "-------- test auto-generated script '(Repeat (Calculate times))'-";
18.6 "-------- test auto-generated script '(Repeat (Calculate times))'-";
18.7 -val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
18.8 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
18.9 writeln(term2str auto_script);
18.10 atomty auto_script;
18.11
18.12 @@ -47,7 +47,7 @@
18.13 while the auto_script must be 'z and type-instantiated before usage*)
18.14 ));
18.15 show_mets();
18.16 -val {scr = Script parsed_script,...} = get_met ["Test","test_interSteps_1"];
18.17 +val {scr = Prog parsed_script,...} = get_met ["Test","test_interSteps_1"];
18.18 writeln(term2str parsed_script);
18.19 atomty parsed_script;
18.20
18.21 @@ -85,7 +85,7 @@
18.22 "-------- test the same called by interSteps norm_Poly -----------";
18.23 "-------- test the same called by interSteps norm_Poly -----------";
18.24 "-------- test the same called by interSteps norm_Poly -----------";
18.25 -val Seq {scr = Script auto_script,...} = assoc_rls "norm_Poly";
18.26 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
18.27 writeln(term2str auto_script);
18.28 atomty auto_script;
18.29
18.30 @@ -112,7 +112,7 @@
18.31 "-------- test the same called by interSteps norm_Rational -------";
18.32 "-------- test the same called by interSteps norm_Rational -------";
18.33
18.34 -val Seq {scr = Script auto_script,...} = assoc_rls "norm_Rational";
18.35 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";
18.36 writeln(term2str auto_script);
18.37 atomty auto_script;
18.38 (***
18.39 @@ -177,7 +177,7 @@
18.40 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
18.41 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
18.42 val rls = assoc_rls "integration";
18.43 -val Seq {scr = Script auto_script,...} = rls;
18.44 +val Seq {scr = Prog auto_script,...} = rls;
18.45 writeln(term2str auto_script);
18.46
18.47 if contain_bdv (get_rules rls) then ()
19.1 --- a/test/Tools/isac/Test_Some.thy Wed Dec 05 15:29:36 2012 +0100
19.2 +++ b/test/Tools/isac/Test_Some.thy Wed Dec 05 15:56:38 2012 +0100
19.3 @@ -1,8 +1,8 @@
19.4
19.5 theory Test_Some imports Isac
19.6 -uses ("ProgLang/scrtools.sml")
19.7 +uses ("Interpret/mstools.sml")
19.8 begin
19.9 -use "ProgLang/scrtools.sml"
19.10 +use "Interpret/mstools.sml"
19.11
19.12 declare [[show_types]]
19.13 declare [[show_sorts]]