1.1 --- a/src/Tools/isac/Interpret/calchead.sml Wed May 04 09:01:10 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 04 14:04:53 2011 +0200
1.3 @@ -773,54 +773,49 @@
1.4 fun appl_add ctxt sel [] ppc pbt ct =
1.5 let
1.6 val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
1.7 - in case parseNEW ctxt ct of
1.8 - NONE => Add (i, [], false, sel, Syn ct)
1.9 - | SOME t =>
1.10 - let val (d, ts) = split_dts t;
1.11 - in if d = e_term then
1.12 - Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
1.13 - (case find_first (eq1 d) pbt of
1.14 - NONE => Add (i, [], true, sel, Sup (d,ts))
1.15 - | SOME (f, (_, id)) =>
1.16 - let fun eq2 d (i, _, _, _, itm_) =
1.17 - d = (d_in itm_) andalso i <> 0;
1.18 - in case find_first (eq2 d) ppc of
1.19 - NONE => Add (i, [], true, f,
1.20 - Cor ((d, ts), (id, pbl_ids' d ts))
1.21 - )
1.22 - | SOME (i', _, _, _, itm_) => if is_list_dsc d then
1.23 - let
1.24 - val in_itm = ts_in itm_;
1.25 - val ts' = union op = ts in_itm;
1.26 - val i'' = if in_itm = [] then i else i';
1.27 - in Add (i'', [], true, f,
1.28 - Cor ((d, ts'), (id, pbl_ids' d ts'))
1.29 - )
1.30 - end else
1.31 - Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.32 - end)
1.33 - end
1.34 + in
1.35 + case parseNEW ctxt ct of
1.36 + NONE => Add (i, [], false, sel, Syn ct)
1.37 + | SOME t =>
1.38 + let val (d, ts) = split_dts t;
1.39 + in
1.40 + if d = e_term
1.41 + then Add (i, [], false, sel, Mis (dsc_unknown, hd ts))
1.42 + else
1.43 + (case find_first (eq1 d) pbt of
1.44 + NONE => Add (i, [], true, sel, Sup (d,ts))
1.45 + | SOME (f, (_, id)) =>
1.46 + let fun eq2 d (i, _, _, _, itm_) =
1.47 + d = (d_in itm_) andalso i <> 0;
1.48 + in case find_first (eq2 d) ppc of
1.49 + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts)))
1.50 + | SOME (i', _, _, _, itm_) =>
1.51 + if is_list_dsc d
1.52 + then
1.53 + let
1.54 + val in_itm = ts_in itm_;
1.55 + val ts' = union op = ts in_itm;
1.56 + val i'' = if in_itm = [] then i else i';
1.57 + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end
1.58 + else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts)))
1.59 + end)
1.60 + end
1.61 end
1.62 | appl_add ctxt sel oris ppc pbt str =
1.63 case parseNEW ctxt str of
1.64 - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.65 - | SOME t => case is_known ctxt sel oris t of
1.66 - ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
1.67 - ("", itm) => Add itm
1.68 - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.69 + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
1.70 + | SOME t =>
1.71 + case is_known ctxt sel oris t of
1.72 + ("", ori', all) =>
1.73 + (case is_notyet_input ctxt ppc all ori' pbt of
1.74 + ("", itm) => Add itm
1.75 + | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg))
1.76 | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg);
1.77 -(*
1.78 -> val (msg,itm) = is_notyet_input thy ppc all ori';
1.79 -val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm
1.80 -> val itm_ = #5 itm;
1.81 -> val ts = ts_in itm_;
1.82 -> map (atomty) ts;
1.83 -*)
1.84 +
1.85
1.86 (** make oris from args of the stac SubProblem and from pbt **)
1.87 -
1.88 -(*.can this formal argument (of a model-pattern) be omitted in the arg-list
1.89 - of a SubProblem ? see ME/ptyps.sml 'type met '.*)
1.90 +(* can this formal argument (of a model-pattern) be omitted in the arg-list
1.91 + of a SubProblem ? see ME/ptyps.sml 'type met ' *)
1.92 fun is_copy_named_idstr str =
1.93 case (rev o Symbol.explode) str of
1.94 "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode))
2.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed May 04 09:01:10 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed May 04 14:04:53 2011 +0200
2.3 @@ -163,33 +163,30 @@
2.4
2.5 (*iterated by nxt_me; there (the resulting) ptp dropped
2.6 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
2.7 -(* val (ptp as (pt, pos as (p,p_))) = ptp;
2.8 - val (ptp as (pt, pos as (p,p_))) = (pt,ip);
2.9 - *)
2.10 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
2.11 - let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
2.12 - probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
2.13 - in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
2.14 - then case mI' of
2.15 - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
2.16 - | _ => nxt_specif Model_Problem (pt, (p,Pbl))
2.17 - else let val cpI = if pI = e_pblID then pI' else pI;
2.18 - val cmI = if mI = e_metID then mI' else mI;
2.19 - val {ppc,prls,where_,...} = get_pbt cpI;
2.20 - val pre = check_preconds "thy 100820" prls where_ probl;
2.21 - val pb = foldl and_ (true, map fst pre);
2.22 - (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
2.23 - val (_,tac) =
2.24 - nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
2.25 - (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
2.26 + let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
2.27 + probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
2.28 + in
2.29 + if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
2.30 + then
2.31 + case mI' of
2.32 + ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
2.33 + | _ => nxt_specif Model_Problem (pt, (p,Pbl))
2.34 + else
2.35 + let
2.36 + val cpI = if pI = e_pblID then pI' else pI;
2.37 + val cmI = if mI = e_metID then mI' else mI;
2.38 + val {ppc, prls, where_, ...} = get_pbt cpI;
2.39 + val pre = check_preconds "thy 100820" prls where_ probl;
2.40 + val pb = foldl and_ (true, map fst pre);
2.41 + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
2.42 + val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
2.43 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
2.44 in case tac of
2.45 - Apply_Method mI =>
2.46 -(* val Apply_Method mI = tac;
2.47 - *)
2.48 - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.49 - | _ => nxt_specif tac ptp end
2.50 - end;
2.51 -
2.52 + Apply_Method mI =>
2.53 + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
2.54 + | _ => nxt_specif tac ptp end
2.55 + end;
2.56
2.57 (*.specify a new method;
2.58 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
3.1 --- a/test/Tools/isac/Interpret/mstools.sml Wed May 04 09:01:10 2011 +0200
3.2 +++ b/test/Tools/isac/Interpret/mstools.sml Wed May 04 14:04:53 2011 +0200
3.3 @@ -20,7 +20,7 @@
3.4 "----------- fun declare_constraints --------------------";
3.5 "----------- fun declare_constraints --------------------";
3.6 "----------- fun declare_constraints --------------------";
3.7 -val ctxt = ProofContext.init_global @{theory}
3.8 +val ctxt = ProofContext.init_global @{theory "Isac"}
3.9 |> declare_constraints "xxx + yyy = (111::int)";
3.10 val t = case parseNEW ctxt "xxx = 123" of
3.11 NONE => error "mstools: syntax error"
4.1 --- a/test/Tools/isac/Interpret/script.sml Wed May 04 09:01:10 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/script.sml Wed May 04 14:04:53 2011 +0200
4.3 @@ -303,10 +303,8 @@
4.4 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
4.5 show_pt pt;
4.6 "~~~~~ fun me, args:"; val (_,tac) = nxt;
4.7 - val (pt, p) =
4.8 - (*locatetac is here for testing by me; step would suffice in me*)
4.9 - case locatetac tac (pt,p) of
4.10 - ("ok", (_, _, ptp)) => ptp | _ => error "test";
4.11 +val (pt, p) = case locatetac tac (pt,p) of
4.12 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
4.13 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
4.14 val pIopt = get_pblID (pt,ip);
4.15 tacis; (*= []*)
5.1 --- a/test/Tools/isac/Test_Isac.thy Wed May 04 09:01:10 2011 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Wed May 04 14:04:53 2011 +0200
5.3 @@ -81,10 +81,67 @@
5.4 (*use "ProgLang/tools.sml" 2002*)
5.5 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
5.6 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
5.7 - use "Interpret/mstools.sml" (*empty*)
5.8 +ML {*
5.9 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
5.10 +val (dI',pI',mI') =
5.11 + ("Test", ["sqroot-test","univariate","equation","test"],
5.12 + ["Test","squ-equ-test-subpbl1"]);
5.13 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
5.14 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.20 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.21 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.22 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.23 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.24 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.25 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS:
5.26 + Tac "[error] appl_add: is_known: identifiers [equality] not in example"*)
5.27 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*)
5.28 +show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*)
5.29 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
5.30 +val (pt, p) = case locatetac tac (pt,p) of
5.31 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
5.32 +
5.33 +
5.34 +
5.35 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
5.36 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
5.37 +val pIopt = get_pblID (pt,ip);
5.38 +tacis; (*= []*)
5.39 +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
5.40 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*)
5.41 +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
5.42 +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
5.43 + probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
5.44 +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*)
5.45 +val cpI = if pI = e_pblID then pI' else pI;
5.46 + val cmI = if mI = e_metID then mI' else mI;
5.47 + val {ppc, prls, where_, ...} = get_pbt cpI;
5.48 + val pre = check_preconds "thy 100820" prls where_ probl;
5.49 + val pb = foldl and_ (true, map fst pre);
5.50 +val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
5.51 + (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
5.52 +"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp);
5.53 +"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp);
5.54 +val (PblObj{meth=met,origin=(oris,(dI',pI',_),_),
5.55 + probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p;
5.56 +val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
5.57 +val cpI = if pI = e_pblID then pI' else pI;
5.58 +val ctxt = get_ctxt pt (p, Pbl);
5.59 +oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*)
5.60 +"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) =
5.61 + (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct);
5.62 +val SOME t = parseNEW ctxt str;
5.63 +if t = parseNEW "-1 + x = (0::real)" then ()
5.64 +else error "TODO"
5.65 +is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*)
5.66 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) use "Interpret/mstools.sml" (*empty*)
5.67 +*}
5.68 use "Interpret/ctree.sml" (*! *)
5.69 -ML {*
5.70 -*}
5.71 use "Interpret/ptyps.sml" (* *)
5.72 (*use "Interpret/generate.sml" new 2011*)
5.73 use "Interpret/calchead.sml" (*! *)