1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Tue May 03 16:23:07 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed May 04 09:01:10 2011 +0200
1.3 @@ -235,39 +235,34 @@
1.4 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
1.5 *)
1.6 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
1.7 - let val pIopt = get_pblID (pt,ip);
1.8 - in if (*p = ([],Res) orelse*) ip = ([],Res)
1.9 - then ("end-of-calculation",(tacis, [], ptp):calcstate') else
1.10 - case tacis of
1.11 - (_::_) =>
1.12 -(* val((tac,_,_)::_) = tacis;
1.13 - *)
1.14 - if ip = p (*the request is done where ptp waits for*)
1.15 - then let val (pt',c',p') = generate tacis (pt,[],p)
1.16 - in ("ok", (tacis, c', (pt', p'))) end
1.17 - else (case (if member op = [Pbl,Met] p_
1.18 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.19 - handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
1.20 - of cs as ([],_,_) => ("helpless", cs)
1.21 - | cs => ("ok", cs))
1.22 -(* val [] = tacis;
1.23 - *)
1.24 - | _ => (case pIopt of
1.25 - NONE => ("no-fmz-spec", ([], [], ptp))
1.26 - | SOME pI =>
1.27 -(* val SOME pI = pIopt;
1.28 - val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p))
1.29 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.30 - handle _ => ([], ptp);
1.31 - *)
1.32 - (case (if member op = [Pbl,Met] p_
1.33 - andalso is_none (get_obj g_env pt (fst p))
1.34 - (*^^^^^^^^: Apply_Method without init_form*)
1.35 - then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
1.36 - handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
1.37 - of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.38 - | cs => ("ok", cs)))
1.39 - end;
1.40 + let val pIopt = get_pblID (pt,ip);
1.41 + in
1.42 + if (*p = ([],Res) orelse*) ip = ([],Res)
1.43 + then ("end-of-calculation",(tacis, [], ptp):calcstate')
1.44 + else
1.45 + case tacis of
1.46 + (_::_) =>
1.47 + if ip = p (*the request is done where ptp waits for*)
1.48 + then
1.49 + let val (pt',c',p') = generate tacis (pt,[],p)
1.50 + in ("ok", (tacis, c', (pt', p'))) end
1.51 + else (case (if member op = [Pbl,Met] p_
1.52 + then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
1.53 + handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
1.54 + cs as ([],_,_) => ("helpless", cs)
1.55 + | cs => ("ok", cs))
1.56 + | _ => (case pIopt of
1.57 + NONE => ("no-fmz-spec", ([], [], ptp))
1.58 + | SOME pI =>
1.59 + (case (if member op = [Pbl,Met] p_
1.60 + andalso is_none (get_obj g_env pt (fst p))
1.61 + (*^^^^^^^^: Apply_Method without init_form*)
1.62 + then nxt_specify_ (pt,ip)
1.63 + else nxt_solve_ (pt,ip) )
1.64 + handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
1.65 + cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
1.66 + | cs => ("ok", cs)))
1.67 + end;
1.68
1.69 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
1.70
1.71 @@ -462,29 +457,29 @@
1.72 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
1.73 *)
1.74 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
1.75 - let val (pt, p) =
1.76 - (*locatetac is here for testing by me; step would suffice in me*)
1.77 + let
1.78 + val (pt, p) =
1.79 + (*locatetac is here for testing by me; step would suffice in me*)
1.80 case locatetac tac (pt,p) of
1.81 - ("ok", (_, _, ptp)) => ptp
1.82 - | ("unsafe-ok", (_, _, ptp)) => ptp
1.83 - | ("not-applicable",_) => (pt, p)
1.84 - | ("end-of-calculation", (_, _, ptp)) => ptp
1.85 - | ("failure",_) => error "sys-error";
1.86 - val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
1.87 + ("ok", (_, _, ptp)) => ptp
1.88 + | ("unsafe-ok", (_, _, ptp)) => ptp
1.89 + | ("not-applicable",_) => (pt, p)
1.90 + | ("end-of-calculation", (_, _, ptp)) => ptp
1.91 + | ("failure",_) => error "sys-error";
1.92 + val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
1.93 (case step p ((pt, e_pos'),[]) of
1.94 - ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.95 - | ("helpless",_) => ("helpless: cannot propose tac", [])
1.96 - | ("no-fmz-spec",_) => error "no-fmz-spec"
1.97 - | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.98 + ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
1.99 + | ("helpless",_) => ("helpless: cannot propose tac", [])
1.100 + | ("no-fmz-spec",_) => error "no-fmz-spec"
1.101 + | ("end-of-calculation", (ts, _, _)) => ("",ts))
1.102 handle _ => error "sys-error";
1.103 - val tac = case ts of tacis as (_::_) =>
1.104 - let val (tac,_,_) = last_elem tacis
1.105 - in tac end
1.106 - | _ => if p = ([],Res) then End_Proof'
1.107 - else Empty_Tac;
1.108 + val tac =
1.109 + case ts of
1.110 + tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
1.111 + | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
1.112 (*form output comes from locatetac*)
1.113 - in (p:pos', []:NEW, TESTg_form (pt, p),
1.114 - (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.115 + in (p:pos', []:NEW, TESTg_form (pt, p),
1.116 + (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
1.117
1.118 (*for quick test-print-out, until 'type inout' is removed*)
1.119 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
2.1 --- a/src/Tools/isac/Interpret/script.sml Tue May 03 16:23:07 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/script.sml Wed May 04 09:01:10 2011 +0200
2.3 @@ -428,18 +428,18 @@
2.4
2.5 (*3.12.03 copied from assod SubProblem*)
2.6 (* val Const ("Script.SubProblem",_) $
2.7 - (Const ("Pair",_) $
2.8 + (Const ("Product_Type.Pair",_) $
2.9 Free (dI',_) $
2.10 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
2.11 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
2.12 str2term
2.13 "SubProblem (EqSystem_, [linear, system], [no_met])\
2.14 \ [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2],\
2.15 \ REAL_LIST [c, c_2]]";
2.16 *)
2.17 | stac2tac_ pt thy (stac as Const ("Script.SubProblem",_) $
2.18 - (Const ("Pair",_) $
2.19 + (Const ("Product_Type.Pair",_) $
2.20 Free (dI',_) $
2.21 - (Const ("Pair",_) $ pI' $ mI')) $ ags') =
2.22 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
2.23 (*compare "| assod _ (Subproblem'"*)
2.24 let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
2.25 val thy = maxthy (assoc_thy dI) (rootthy pt);
2.26 @@ -473,24 +473,9 @@
2.27 | stac2tac_ pt thy t = error
2.28 ("stac2tac_ TODO: no match for " ^
2.29 (Print_Mode.setmp [] (Syntax.string_of_term (thy2ctxt thy)) t));
2.30 -(*
2.31 -> val t = (term_of o the o (parse thy))
2.32 - "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";
2.33 -> stac2tac_ pt t;
2.34 -val it = Rewrite_Set_Inst ([(#,#)],"isolate_bdv") : tac
2.35 -
2.36 -> val t = (term_of o the o (parse SqRoot.thy))
2.37 -"(SubProblem (SqRoot_,[equation,univariate],(SqRoot_,solve_linear))\
2.38 - \ [BOOL e_, REAL v_])::bool list";
2.39 -> stac2tac_ pt SqRoot.thy t;
2.40 -val it = (Subproblem ("SqRoot",[#,#]),Const (#,#) $ (# $ # $ (# $ #)))
2.41 -*)
2.42
2.43 fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
2.44
2.45 -
2.46 -
2.47 -
2.48 (*test a term for being a _list_ (set ?) of constants; could be more rigorous*)
2.49 fun list_of_consts (Const ("List.list.Cons",_) $ _ $ _) = true
2.50 | list_of_consts (Const ("List.list.Nil",_)) = true
2.51 @@ -642,15 +627,15 @@
2.52
2.53 val (Subproblem' ((domID,pblID,metID),_,_,_,f)) = m;
2.54 val (Const ("Script.SubProblem",_) $
2.55 - (Const ("Pair",_) $
2.56 + (Const ("Product_Type.Pair",_) $
2.57 Free (dI',_) $
2.58 - (Const ("Pair",_) $ pI' $ mI')) $ ags') = stac;
2.59 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') = stac;
2.60 *)
2.61 | assod pt _ (Subproblem' ((domID,pblID,metID),_,_,_,f))
2.62 (stac as Const ("Script.SubProblem",_) $
2.63 - (Const ("Pair",_) $
2.64 + (Const ("Product_Type.Pair",_) $
2.65 Free (dI',_) $
2.66 - (Const ("Pair",_) $ pI' $ mI')) $ ags') =
2.67 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags') =
2.68 (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
2.69 let val dI = ((implode o drop_last(*.."'"*) o Symbol.explode) dI')(*^""*);
2.70 val thy = maxthy (assoc_thy dI) (rootthy pt);
2.71 @@ -1765,26 +1750,26 @@
2.72 ((thy',srls), (pt,pos), sc, is);
2.73 *)
2.74 | next_tac thy (ptp as (pt,(p,_)):ptree * pos') (sc as Script (h $ body))
2.75 - (ScrState (E,l,a,v,s,b), ctxt) =
2.76 - ((*tracing("### next_tac-----------------: E= ");
2.77 - tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
2.78 - case if l=[] then appy thy ptp E [R] body NONE v
2.79 - else nstep_up thy ptp sc E l Skip_ a v of
2.80 - Skip (v,_) => (*finished*)
2.81 - (case par_pbl_det pt p of
2.82 - (true, p', _) =>
2.83 - let val (_,pblID,_) = get_obj g_spec pt p';
2.84 - in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
2.85 - (e_istate, e_ctxt), (v,s)) end
2.86 - | (_,p',rls') => (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
2.87 - | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef)) (*helpless*)
2.88 - | Appy (m', scrst as (_,_,_,v,_,_)) => (m', (ScrState scrst, e_ctxt),
2.89 - (v, Sundef))) (*next stac*)
2.90 + (ScrState (E,l,a,v,s,b), ctxt) =
2.91 + ((*tracing("### next_tac-----------------: E= ");
2.92 + tracing( istate2str (ScrState (E,l,a,v,s,b)));*)
2.93 + case if l = []
2.94 + then appy thy ptp E [R] body NONE v
2.95 + else nstep_up thy ptp sc E l Skip_ a v of
2.96 + Skip (v, _) => (*finished*)
2.97 + (case par_pbl_det pt p of
2.98 + (true, p', _) =>
2.99 + let val (_,pblID,_) = get_obj g_spec pt p';
2.100 + in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
2.101 + (e_istate, e_ctxt), (v,s))
2.102 + end
2.103 + | (_, p', rls') =>
2.104 + (End_Detail' (e_term,[])(*8.6.03*), (e_istate, e_ctxt), (v,s)))
2.105 + | Napp _ => (Empty_Tac_, (e_istate, e_ctxt), (e_term, Sundef))(*helpless*)
2.106 + | Appy (m', scrst as (_,_,_,v,_,_)) =>
2.107 + (m', (ScrState scrst, e_ctxt), (v, Sundef))) (*next stac*)
2.108
2.109 - | next_tac _ _ _ (is, _) = error ("next_tac: not impl for "^
2.110 - (istate2str is));
2.111 -
2.112 -
2.113 + | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (istate2str is));
2.114
2.115
2.116 (*.create the initial interpreter state from the items of the guard.*)
3.1 --- a/src/Tools/isac/Interpret/solve.sml Tue May 03 16:23:07 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/solve.sml Wed May 04 09:01:10 2011 +0200
3.3 @@ -408,19 +408,18 @@
3.4 val (ptp as (pt, pos as (p,p_))) = (pt, pos);
3.5 *)
3.6 and nxt_solve_ (ptp as (pt, pos as (p,p_))) =
3.7 - if e_metID = get_obj g_metID pt (par_pblobj pt p)
3.8 - then ([], [], (pt,(p,p_))):calcstate'
3.9 - else let val thy' = get_obj g_domID pt (par_pblobj pt p);
3.10 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.11 - val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
3.12 - (*TODO here ^^^ return finished/helpless/ok !*)
3.13 - (* val (tac_',is',(t',_)) = next_tac (thy',srls) (pt,pos) sc is;
3.14 - *)
3.15 - in case tac_ of
3.16 - End_Detail' _ => ([(End_Detail,
3.17 - End_Detail' (t,[(*FIXME.040215*)]),
3.18 - (pos, is))], [], (pt, pos))
3.19 - | _ => nxt_solv tac_ is ptp end;
3.20 + if e_metID = get_obj g_metID pt (par_pblobj pt p)
3.21 + then ([], [], (pt,(p,p_))):calcstate'
3.22 + else
3.23 + let
3.24 + val thy' = get_obj g_domID pt (par_pblobj pt p);
3.25 + val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
3.26 + val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
3.27 + (*TODO here ^^^ return finished/helpless/ok !*)
3.28 + in case tac_ of
3.29 + End_Detail' _ => ([(End_Detail, End_Detail' (t,[(*FIXME.040215*)]),
3.30 + (pos, is))], [], (pt, pos))
3.31 + | _ => nxt_solv tac_ is ptp end;
3.32
3.33 (*.says how may steps of a calculation should be done by "fun autocalc".*)
3.34 (*TODO.WN0512 redesign togehter with autocalc ?*)
4.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue May 03 16:23:07 2011 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Wed May 04 09:01:10 2011 +0200
4.3 @@ -229,9 +229,9 @@
4.4 SOME i => SOME ((i, 0), (0, 0))
4.5 | NONE => NONE)
4.6 | numeral (Const ("Float.Float", _) $
4.7 - (Const ("Pair", _) $
4.8 - (Const ("Pair", T) $ Free (v1, _) $ Free (v2,_)) $
4.9 - (Const ("Pair", _) $ Free (p1, _) $ Free (p2,_))))=
4.10 + (Const ("Product_Type.Pair", _) $
4.11 + (Const ("Product_Type.Pair", T) $ Free (v1, _) $ Free (v2,_)) $
4.12 + (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
4.13 (case (int_of_str v1, int_of_str v2, int_of_str p1, int_of_str p2) of
4.14 (SOME v1', SOME v2', SOME p1', SOME p2') =>
4.15 SOME ((v1', v2'), (p1', p2'))
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue May 03 16:23:07 2011 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Wed May 04 09:01:10 2011 +0200
5.3 @@ -400,9 +400,9 @@
5.4
5.5 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
5.6 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
5.7 - val [Const ("Pair", _) $ t $ bdv] = pairl;
5.8 + val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
5.9 *)
5.10 -fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
5.11 +fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
5.12 [((term_of o the o (parse thy)) "functionTerm", [t]),
5.13 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
5.14 ((term_of o the o (parse thy)) "derivative",
5.15 @@ -418,9 +418,9 @@
5.16
5.17 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
5.18 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
5.19 - val [Const ("Pair", _) $ t $ bdv] = pairl;
5.20 + val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
5.21 *)
5.22 -fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
5.23 +fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
5.24 [((term_of o the o (parse thy)) "functionEq", [t]),
5.25 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
5.26 ((term_of o the o (parse thy)) "derivativeEq",
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Tue May 03 16:23:07 2011 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed May 04 09:01:10 2011 +0200
6.3 @@ -68,7 +68,7 @@
6.4 val (h,argl) = strip_comb ((term_of o the o (parse thy))
6.5 "solveTest (x+1=2, x)");
6.6 *)
6.7 -fun argl2dtss [Const ("Pair", _) $ eq $ bdv] =
6.8 +fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] =
6.9 [((the o (parseNEW ctxt)) "equality", [eq]),
6.10 ((the o (parseNEW ctxt)) "solveFor", [bdv]),
6.11 ((the o (parseNEW ctxt)) "solutions",
7.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue May 03 16:23:07 2011 +0200
7.2 +++ b/src/Tools/isac/ProgLang/termC.sml Wed May 04 09:01:10 2011 +0200
7.3 @@ -264,7 +264,7 @@
7.4 > (cterm_of thy) ss;
7.5 val it = "[R = R, R = R, R = R]" : cterm *)
7.6
7.7 -fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
7.8 +fun isapair2pair (Const ("Product_Type.Pair",_) $ a $ b) = (a,b)
7.9 | isapair2pair t =
7.10 error ("isapair2pair called with "^term2str t);
7.11
7.12 @@ -548,12 +548,12 @@
7.13 *)
7.14 fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
7.15 (*> val t = str2term "(1,2)";
7.16 -> val Const ("Pair",pT) $ _ $ _ = t;
7.17 +> val Const ("Product_Type.Pair",pT) $ _ $ _ = t;
7.18 > pT = PairT HOLogic.realT HOLogic.realT;
7.19 val it = true : bool
7.20 *)
7.21 fun pairt t1 t2 =
7.22 - Const ("Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
7.23 + Const ("Product_Type.Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
7.24 (*> val t = str2term "(1,2)";
7.25 > val (t1, t2) = (str2term "1", str2term "2");
7.26 > t = pairt t1 t2;
8.1 --- a/src/Tools/isac/library.sml Tue May 03 16:23:07 2011 +0200
8.2 +++ b/src/Tools/isac/library.sml Wed May 04 09:01:10 2011 +0200
8.3 @@ -248,7 +248,7 @@
8.4 > val t = (term_of o the o (parse thy))
8.5 "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
8.6 > ids_of t;
8.7 -["solve'_univar","Pair","R","Cons","univar","equation","Nil",...]*)
8.8 +["solve'_univar","Product_Type.Pair","R","Cons","univar","equation","Nil",...]*)
8.9
8.10
8.11 (*FIXME.WN090819 fun overwrite missing in ..2009/../library.ML*)
9.1 --- a/test/Tools/isac/Interpret/calchead.sml Tue May 03 16:23:07 2011 +0200
9.2 +++ b/test/Tools/isac/Interpret/calchead.sml Wed May 04 09:01:10 2011 +0200
9.3 @@ -331,9 +331,9 @@
9.4 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
9.5 "--------- match_ags, is_cp, cpy_nam +with EqSystem (!)--";
9.6 val Const ("Script.SubProblem",_) $
9.7 - (Const ("Pair",_) $
9.8 + (Const ("Product_Type.Pair",_) $
9.9 Free (dI',_) $
9.10 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
9.11 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
9.12 (*...copied from stac2tac_*)
9.13 str2term (
9.14 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
9.15 @@ -357,9 +357,9 @@
9.16
9.17 "-b------------------------------------------------------";
9.18 val Const ("Script.SubProblem",_) $
9.19 - (Const ("Pair",_) $
9.20 + (Const ("Product_Type.Pair",_) $
9.21 Free (dI',_) $
9.22 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
9.23 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
9.24 (*...copied from stac2tac_*)
9.25 str2term (
9.26 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
9.27 @@ -384,9 +384,9 @@
9.28
9.29 "-c---ERROR case: stac is missing #Given equalities e_s--";
9.30 val stac as Const ("Script.SubProblem",_) $
9.31 - (Const ("Pair",_) $
9.32 + (Const ("Product_Type.Pair",_) $
9.33 Free (dI',_) $
9.34 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
9.35 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
9.36 (*...copied from stac2tac_*)
9.37 str2term (
9.38 "SubProblem (EqSystem', [linear, system], [no_met]) " ^
9.39 @@ -430,9 +430,9 @@
9.40
9.41 "-d------------------------------------------------------";
9.42 val stac as Const ("Script.SubProblem",_) $
9.43 - (Const ("Pair",_) $
9.44 + (Const ("Product_Type.Pair",_) $
9.45 Free (dI',_) $
9.46 - (Const ("Pair",_) $ pI' $ mI')) $ ags' =
9.47 + (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
9.48 (*...copied from stac2tac_*)
9.49 str2term (
9.50 "SubProblem (Test',[univariate,equation,test]," ^
9.51 @@ -625,7 +625,7 @@
9.52 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
9.53 Const ("Integrate.Integrate",
9.54 "(RealDef.real, RealDef.real) * => RealDef.real") $
9.55 - (Const ("Pair",
9.56 + (Const ("Product_Type.Pair",
9.57 "[RealDef.real, RealDef.real]
9.58 => (RealDef.real, RealDef.real) *") $
9.59 (Const ("op +",
9.60 @@ -698,7 +698,7 @@
9.61 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
9.62 Const ("Integrate.Integrate",
9.63 "(RealDef.real, RealDef.real) * => RealDef.real") $
9.64 - (Const ("Pair",
9.65 + (Const ("Product_Type.Pair",
9.66 "[RealDef.real, RealDef.real]
9.67 => (RealDef.real, RealDef.real) *") $
9.68 (Const ("op +",
10.1 --- a/test/Tools/isac/Interpret/ctree.sml Tue May 03 16:23:07 2011 +0200
10.2 +++ b/test/Tools/isac/Interpret/ctree.sml Wed May 04 09:01:10 2011 +0200
10.3 @@ -10,7 +10,6 @@
10.4 "table of contents -----------------------------------------------";
10.5 "-----------------------------------------------------------------";
10.6 "-----------------------------------------------------------------";
10.7 -"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
10.8 "-------------- check positions in miniscript --------------------";
10.9 "-------------- get_allpos' (from ptree above)--------------------";
10.10 (**#####################################################################(**)
10.11 @@ -59,27 +58,10 @@
10.12 "-----------------------------------------------------------------";
10.13
10.14
10.15 -"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
10.16 -"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
10.17 -"-------------- build miniscript stepwise BEFORE ALL TESTS -------";
10.18 -"this build should be detailed each time a test fails later ";
10.19 -"i.e. all the tests should be caught here first ";
10.20 -"and linked with a reference to the respective test environment ";
10.21 -val fmz = ["equality (x+1=(2::int))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
10.22 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
10.23 - ["Test","squ-equ-test-subpbl1"]);
10.24 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
10.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
10.28 -
10.29 -
10.30 -
10.31 -
10.32 "-------------- check positions in miniscript --------------------";
10.33 "-------------- check positions in miniscript --------------------";
10.34 "-------------- check positions in miniscript --------------------";
10.35 -val fmz = ["equality (x+1=(2::int))",
10.36 +val fmz = ["equality (x+1=(2::real))",
10.37 "solveFor x","solutions L"];
10.38 val (dI',pI',mI') =
10.39 ("Test",["sqroot-test","univariate","equation","test"],
11.1 --- a/test/Tools/isac/Interpret/script.sml Tue May 03 16:23:07 2011 +0200
11.2 +++ b/test/Tools/isac/Interpret/script.sml Wed May 04 09:01:10 2011 +0200
11.3 @@ -13,6 +13,7 @@
11.4 "----------- WN0509 Substitute 2nd part --------------------------";
11.5 "----------- fun sel_appl_atomic_tacs ----------------------------";
11.6 "----------- fun init_form, fun get_stac -------------------------";
11.7 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
11.8 "-----------------------------------------------------------------";
11.9 "-----------------------------------------------------------------";
11.10 "-----------------------------------------------------------------";
11.11 @@ -281,3 +282,51 @@
11.12 case get_stac thy sc of SOME (Free ("e_e", _)) => ()
11.13 | _ => error "script: Const (?, ?) in script (as term) changed";;
11.14
11.15 +
11.16 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
11.17 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
11.18 +"----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
11.19 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11.20 +val (dI',pI',mI') =
11.21 + ("Test", ["sqroot-test","univariate","equation","test"],
11.22 + ["Test","squ-equ-test-subpbl1"]);
11.23 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
11.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.25 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.26 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.27 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.28 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.29 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.30 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.31 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.32 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
11.33 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
11.34 +show_pt pt;
11.35 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
11.36 + val (pt, p) =
11.37 + (*locatetac is here for testing by me; step would suffice in me*)
11.38 + case locatetac tac (pt,p) of
11.39 + ("ok", (_, _, ptp)) => ptp | _ => error "test";
11.40 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
11.41 +val pIopt = get_pblID (pt,ip);
11.42 +tacis; (*= []*)
11.43 +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
11.44 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
11.45 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
11.46 + (*WAS stac2tac_ TODO: no match for SubProblem*)
11.47 +val thy' = get_obj g_domID pt (par_pblobj pt p);
11.48 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
11.49 +"~~~~~ fun next_tac, args:"; val (thy, (ptp as (pt,(p,_)):ptree * pos'), (sc as Script (h $ body)),
11.50 + (ScrState (E,l,a,v,s,b), ctxt)) = ((thy',srls), (pt,pos), sc, is);
11.51 +l; (*= [R, L, R, L, R, R]*)
11.52 +val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
11.53 +"~~~~~ dont like to go into nstep_up...";
11.54 +val t = str2term ("SubProblem" ^
11.55 + "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
11.56 + "[BOOL (-1 + x = 0), REAL x]");
11.57 +val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
11.58 +case tac_ of
11.59 + Subproblem' _ => ()
11.60 +| _ => error "script.sml x+1=2 start SubProblem from script";
11.61 +
11.62 +
12.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 03 16:23:07 2011 +0200
12.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 04 09:01:10 2011 +0200
12.3 @@ -82,16 +82,18 @@
12.4 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
12.5 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
12.6 use "Interpret/mstools.sml" (*empty*)
12.7 - use "Interpret/ctree.sml"
12.8 + use "Interpret/ctree.sml" (*! *)
12.9 +ML {*
12.10 +*}
12.11 use "Interpret/ptyps.sml" (* *)
12.12 (*use "Interpret/generate.sml" new 2011*)
12.13 - use "Interpret/calchead.sml" (* *)
12.14 -(*use "Interpret/appl.sml" new 2011*)
12.15 - use "Interpret/rewtools.sml" (* *)
12.16 - use "Interpret/script.sml" (*TODO*)
12.17 -(*use "Interpret/solve.sml" TODO*)
12.18 -(*use "Interpret/inform.sml" TODO*)
12.19 - use "Interpret/mathengine.sml"(*part.*)
12.20 + use "Interpret/calchead.sml" (*! *)
12.21 + use "Interpret/appl.sml" (*!complete*)
12.22 + use "Interpret/rewtools.sml" (*! *)
12.23 + use "Interpret/script.sml" (*!TODO*)
12.24 +(*use "Interpret/solve.sml" !TODO*)
12.25 +(*use "Interpret/inform.sml" !TODO*)
12.26 + use "Interpret/mathengine.sml" (*!part.*)
12.27 ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
12.28 ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
12.29 (*use "xmlsrc/mathml.sml" TODO*)