# HG changeset patch # User Walther Neuper # Date 1304510693 -7200 # Node ID bf17547ce9608a396c9e8f3ab69c64868b583053 # Parent 22c5483e9bfbce08c62161ab66159fc6a5883996 tuned diff -r 22c5483e9bfb -r bf17547ce960 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Wed May 04 09:01:10 2011 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Wed May 04 14:04:53 2011 +0200 @@ -773,54 +773,49 @@ fun appl_add ctxt sel [] ppc pbt ct = let val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl); - in case parseNEW ctxt ct of - NONE => Add (i, [], false, sel, Syn ct) - | SOME t => - let val (d, ts) = split_dts t; - in if d = e_term then - Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else - (case find_first (eq1 d) pbt of - NONE => Add (i, [], true, sel, Sup (d,ts)) - | SOME (f, (_, id)) => - let fun eq2 d (i, _, _, _, itm_) = - d = (d_in itm_) andalso i <> 0; - in case find_first (eq2 d) ppc of - NONE => Add (i, [], true, f, - Cor ((d, ts), (id, pbl_ids' d ts)) - ) - | SOME (i', _, _, _, itm_) => if is_list_dsc d then - let - val in_itm = ts_in itm_; - val ts' = union op = ts in_itm; - val i'' = if in_itm = [] then i else i'; - in Add (i'', [], true, f, - Cor ((d, ts'), (id, pbl_ids' d ts')) - ) - end else - Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts))) - end) - end + in + case parseNEW ctxt ct of + NONE => Add (i, [], false, sel, Syn ct) + | SOME t => + let val (d, ts) = split_dts t; + in + if d = e_term + then Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) + else + (case find_first (eq1 d) pbt of + NONE => Add (i, [], true, sel, Sup (d,ts)) + | SOME (f, (_, id)) => + let fun eq2 d (i, _, _, _, itm_) = + d = (d_in itm_) andalso i <> 0; + in case find_first (eq2 d) ppc of + NONE => Add (i, [], true, f,Cor ((d, ts), (id, pbl_ids' d ts))) + | SOME (i', _, _, _, itm_) => + if is_list_dsc d + then + let + val in_itm = ts_in itm_; + val ts' = union op = ts in_itm; + val i'' = if in_itm = [] then i else i'; + in Add (i'', [], true, f, Cor ((d, ts'), (id, pbl_ids' d ts'))) end + else Add (i', [], true, f, Cor ((d, ts),(id, pbl_ids' d ts))) + end) + end end | appl_add ctxt sel oris ppc pbt str = case parseNEW ctxt str of - NONE => Err ("appl_add: syntax error in '" ^ str ^ "'") - | SOME t => case is_known ctxt sel oris t of - ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of - ("", itm) => Add itm - | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg)) + NONE => Err ("appl_add: syntax error in '" ^ str ^ "'") + | SOME t => + case is_known ctxt sel oris t of + ("", ori', all) => + (case is_notyet_input ctxt ppc all ori' pbt of + ("", itm) => Add itm + | (msg, _) => Err ("[error] appl_add: is_notyet_input: " ^ msg)) | (msg, _, _) => Err ("[error] appl_add: is_known: " ^ msg); -(* -> val (msg,itm) = is_notyet_input thy ppc all ori'; -val itm = (12,[3],false,"#Relate",Cor (Const #,[#,#])) : itm -> val itm_ = #5 itm; -> val ts = ts_in itm_; -> map (atomty) ts; -*) + (** make oris from args of the stac SubProblem and from pbt **) - -(*.can this formal argument (of a model-pattern) be omitted in the arg-list - of a SubProblem ? see ME/ptyps.sml 'type met '.*) +(* can this formal argument (of a model-pattern) be omitted in the arg-list + of a SubProblem ? see ME/ptyps.sml 'type met ' *) fun is_copy_named_idstr str = case (rev o Symbol.explode) str of "'":: _ ::"'"::_ => (tracing ((strs2str o (rev o Symbol.explode)) diff -r 22c5483e9bfb -r bf17547ce960 src/Tools/isac/Interpret/mathengine.sml --- a/src/Tools/isac/Interpret/mathengine.sml Wed May 04 09:01:10 2011 +0200 +++ b/src/Tools/isac/Interpret/mathengine.sml Wed May 04 14:04:53 2011 +0200 @@ -163,33 +163,30 @@ (*iterated by nxt_me; there (the resulting) ptp dropped may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*) -(* val (ptp as (pt, pos as (p,p_))) = ptp; - val (ptp as (pt, pos as (p,p_))) = (pt,ip); - *) fun nxt_specify_ (ptp as (pt, pos as (p,p_))) = - let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), - probl,spec=(dI,pI,mI),...}) = get_obj I pt p; - in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin - then case mI' of - ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl)) - | _ => nxt_specif Model_Problem (pt, (p,Pbl)) - else let val cpI = if pI = e_pblID then pI' else pI; - val cmI = if mI = e_metID then mI' else mI; - val {ppc,prls,where_,...} = get_pbt cpI; - val pre = check_preconds "thy 100820" prls where_ probl; - val pb = foldl and_ (true, map fst pre); - (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*) - val (_,tac) = - nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) - (ppc, (#ppc o get_met) cmI) (dI, pI, mI); + let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), + probl,spec=(dI,pI,mI),...}) = get_obj I pt p; + in + if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin + then + case mI' of + ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl)) + | _ => nxt_specif Model_Problem (pt, (p,Pbl)) + else + let + val cpI = if pI = e_pblID then pI' else pI; + val cmI = if mI = e_metID then mI' else mI; + val {ppc, prls, where_, ...} = get_pbt cpI; + val pre = check_preconds "thy 100820" prls where_ probl; + val pb = foldl and_ (true, map fst pre); + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*) + val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) + (ppc, (#ppc o get_met) cmI) (dI, pI, mI); in case tac of - Apply_Method mI => -(* val Apply_Method mI = tac; - *) - nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp - | _ => nxt_specif tac ptp end - end; - + Apply_Method mI => + nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp + | _ => nxt_specif tac ptp end + end; (*.specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*) diff -r 22c5483e9bfb -r bf17547ce960 test/Tools/isac/Interpret/mstools.sml --- a/test/Tools/isac/Interpret/mstools.sml Wed May 04 09:01:10 2011 +0200 +++ b/test/Tools/isac/Interpret/mstools.sml Wed May 04 14:04:53 2011 +0200 @@ -20,7 +20,7 @@ "----------- fun declare_constraints --------------------"; "----------- fun declare_constraints --------------------"; "----------- fun declare_constraints --------------------"; -val ctxt = ProofContext.init_global @{theory} +val ctxt = ProofContext.init_global @{theory "Isac"} |> declare_constraints "xxx + yyy = (111::int)"; val t = case parseNEW ctxt "xxx = 123" of NONE => error "mstools: syntax error" diff -r 22c5483e9bfb -r bf17547ce960 test/Tools/isac/Interpret/script.sml --- a/test/Tools/isac/Interpret/script.sml Wed May 04 09:01:10 2011 +0200 +++ b/test/Tools/isac/Interpret/script.sml Wed May 04 14:04:53 2011 +0200 @@ -303,10 +303,8 @@ (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*) show_pt pt; "~~~~~ fun me, args:"; val (_,tac) = nxt; - val (pt, p) = - (*locatetac is here for testing by me; step would suffice in me*) - case locatetac tac (pt,p) of - ("ok", (_, _, ptp)) => ptp | _ => error "test"; +val (pt, p) = case locatetac tac (pt,p) of + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) val pIopt = get_pblID (pt,ip); tacis; (*= []*) diff -r 22c5483e9bfb -r bf17547ce960 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Wed May 04 09:01:10 2011 +0200 +++ b/test/Tools/isac/Test_Isac.thy Wed May 04 14:04:53 2011 +0200 @@ -81,10 +81,67 @@ (*use "ProgLang/tools.sml" 2002*) ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*} ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*} - use "Interpret/mstools.sml" (*empty*) +ML {* +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; +val (dI',pI',mI') = + ("Test", ["sqroot-test","univariate","equation","test"], + ["Test","squ-equ-test-subpbl1"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: + Tac "[error] appl_add: is_known: identifiers [equality] not in example"*) +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: applicable_in (p,Pbl) pt (Tac id): not at Pbl*) +show_pt pt; (*WAS ...(([3], Pbl), solve (-1 + x = 0, x))] OK*) +"~~~~~ fun me, args:"; val (_,tac) = nxt; +val (pt, p) = case locatetac tac (pt,p) of + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac"; + + + +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) +val pIopt = get_pblID (pt,ip); +tacis; (*= []*) +pIopt; (*= SOME ["sqroot-test", "univariate", ...]*) +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= true*) +"~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip); +val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_), + probl,spec=(dI,pI,mI),...}) = get_obj I pt p; +just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin; (*false*) +val cpI = if pI = e_pblID then pI' else pI; + val cmI = if mI = e_metID then mI' else mI; + val {ppc, prls, where_, ...} = get_pbt cpI; + val pre = check_preconds "thy 100820" prls where_ probl; + val pb = foldl and_ (true, map fst pre); +val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) + (ppc, (#ppc o get_met) cmI) (dI, pI, mI); +"~~~~~ fun nxt_specif, args:"; val (Add_Given ct, ptp) = (tac, ptp); +"~~~~~ fun nxt_specif_additem, args:"; val (sel, ct, ptp as (pt, (p, Pbl))) = ("#Given", ct, ptp); +val (PblObj{meth=met,origin=(oris,(dI',pI',_),_), + probl=pbl,spec=(dI,pI,_),...}) = get_obj I pt p; +val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI; +val cpI = if pI = e_pblID then pI' else pI; +val ctxt = get_ctxt pt (p, Pbl); +oris; (*= [(1, [1], "#Given", Const ("Descript.equality", "HOL.bool...*) +"~~~~~ fun appl_add, args:"; val (ctxt, sel, oris, ppc, pbt, str) = + (ctxt, sel, oris, pbl, (#ppc o get_pbt) cpI, ct); +val SOME t = parseNEW ctxt str; +if t = parseNEW "-1 + x = (0::real)" then () +else error "TODO" +is_known ctxt sel oris t; (*= ("identifiers [equality] not in example", ...WN110504???*) +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) use "Interpret/mstools.sml" (*empty*) +*} use "Interpret/ctree.sml" (*! *) -ML {* -*} use "Interpret/ptyps.sml" (* *) (*use "Interpret/generate.sml" new 2011*) use "Interpret/calchead.sml" (*! *)