1.1 --- a/test/Tools/isac/Interpret/script.sml Wed Dec 05 15:29:36 2012 +0100
1.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Dec 05 15:56:38 2012 +0100
1.3 @@ -77,7 +77,7 @@
1.4 val sc' = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.5 atomty sc';
1.6
1.7 -val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.8 +val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.9 (*---------------------------------------------------------------------
1.10 if sc = sc' then () else error"script.sml, doesnt find Substitute #1";
1.11 ---------------------------------------------------------------------*)
1.12 @@ -114,7 +114,7 @@
1.13 " in True)"
1.14 ;
1.15
1.16 -val {scr = Script sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.17 +val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
1.18 (*---------------------------------------------------------------------
1.19 if sc = sc' then () else error "script.sml, doesnt find Substitute #1";
1.20 ---------------------------------------------------------------------*)
1.21 @@ -297,7 +297,7 @@
1.22 val thy = assoc_thy thy';
1.23 val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.24 val ini = init_form thy sc env;
1.25 -"----- fun init_form, args:"; val (Script sc) = sc;
1.26 +"----- fun init_form, args:"; val (Prog sc) = sc;
1.27 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
1.28 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
1.29 | _ => error "script: Const (?, ?) in script (as term) changed";;
1.30 @@ -333,7 +333,7 @@
1.31 (*WAS stac2tac_ TODO: no match for SubProblem*)
1.32 val thy' = get_obj g_domID pt (par_pblobj pt p);
1.33 val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
1.34 -"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
1.35 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Prog (h $ body)),
1.36 (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
1.37 l; (*= [R, L, R, L, R, R]*)
1.38 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
1.39 @@ -385,7 +385,7 @@
1.40 val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.41 val d = e_rls (*FIXME: get simplifier from domID*);
1.42 "~~~~~ fun locate_gen, args:"; val ((ts as (thy',srls)), (m:tac_), ((pt,p):ptree * pos'),
1.43 - (scr as Script (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
1.44 + (scr as Prog (h $ body),d), (ScrState (E,l,a,v,S,b), ctxt)) =
1.45 ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
1.46 val thy = assoc_thy thy';
1.47 l = [] orelse ((*init.in solve..Apply_Method...*)
1.48 @@ -423,19 +423,19 @@
1.49 val (p'''', pt'''') = (p, pt);
1.50 f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation";
1.51 val (p, p_) = p(* = ([1], Frm)*);
1.52 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.53 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.54 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.55 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.56 loc_ = [];
1.57 curry_arg = NONE;
1.58 term2str res = "??.empty"; (* scrstate before starting interpretation *)
1.59 -(*term2str (go loc_ sc) = "Script Solve_root_equation e_e v_v = ...*)
1.60 +(*term2str (go loc_ sc) = "Prog Solve_root_equation e_e v_v = ...*)
1.61
1.62 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.63 val (p'''', pt'''') = (p, pt);
1.64 f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
1.65 val (p, p_) = p(* = ([1], Res)*);
1.66 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.67 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.68 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.69 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.70 loc_ = [R, L, R, L, L, R, R];
1.71 @@ -447,7 +447,7 @@
1.72 val (p'''', pt'''') = (p, pt);
1.73 f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
1.74 val (p, p_) = p(* = ([2], Res)*);
1.75 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.76 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.77 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
1.78 env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.79 loc_ = [R, L, R, L, R, R];
1.80 @@ -476,19 +476,19 @@
1.81 val (p'''', pt'''') = (p, pt);
1.82 f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
1.83 val (p, p_) = p(* = ([3, 1], Frm)*);
1.84 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.85 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.86 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.87 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
1.88 loc_ = [];
1.89 curry_arg = NONE;
1.90 term2str res = "??.empty"; (* scrstate before starting interpretation *)
1.91 -(*term2str (go loc_ sc) = "Script Solve_linear e_e v_v = ...*)
1.92 +(*term2str (go loc_ sc) = "Prog Solve_linear e_e v_v = ...*)
1.93
1.94 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.95 val (p'''', pt'''') = (p, pt);
1.96 f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
1.97 val (p, p_) = p(* = ([3, 1], Res)*);
1.98 -val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.99 +val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.100 val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.101 env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
1.102 loc_ = [R, L, R, L, R, L, R];
1.103 @@ -582,7 +582,7 @@
1.104 if metID = e_metID
1.105 then (thd3 o snd3) (get_obj g_origin pt pp)
1.106 else metID
1.107 - val {scr=Script sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.108 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
1.109 val ScrState (env,_,a,v,_,_) = get_istate pt (p,p_)
1.110 val alltacs = (*we expect at least 1 stac in a script*)
1.111 map ((stac2tac pt thy) o rep_stacexpr o #2 o