intermed. ctxt ..: generate1..Check_Postcond..(*map str2term asm*)
asm now contain predicates like "match ?a = ?b .." which requires parse_patt
in str2term etc.
1.1 --- a/src/Tools/isac/Interpret/generate.sml Fri May 20 09:12:40 2011 +0200
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Fri May 20 13:43:25 2011 +0200
1.3 @@ -442,10 +442,8 @@
1.4 in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
1.5
1.6 | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
1.7 - let (*val _=tracing("###generate1 Check_Postcond': pos= "^pos'2str(p,p_))*)
1.8 - (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
1.9 - val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
1.10 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.11 + let val (pt,c) = append_result pt p l (scval, (*map str2term asm*)[]) Complete
1.12 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.13 Nundef, term2str scval)), pt) end
1.14
1.15 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
2.1 --- a/src/Tools/isac/Interpret/script.sml Fri May 20 09:12:40 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/script.sml Fri May 20 13:43:25 2011 +0200
2.3 @@ -1541,7 +1541,7 @@
2.4 (case par_pbl_det pt p of
2.5 (true, p', _) =>
2.6 let val (_,pblID,_) = get_obj g_spec pt p';
2.7 - in (Check_Postcond' (pblID, (v, [(*8.6.03 NO asms???*)])),
2.8 + in (Check_Postcond' (pblID, (v, [(*WN030608 NO asms???*)])),
2.9 (e_istate, ctxt), (v,s))
2.10 end
2.11 | (_, p', rls') =>
2.12 @@ -1590,7 +1590,7 @@
2.13 val ctxt = ProofContext.init_global thy |> declare_constraints' actuals
2.14 val {pre, prls, ...} = get_met metID;
2.15 val pres = check_preconds thy prls pre itms |> map snd;
2.16 - (*val ctxt = ctxt |> insert_assumptions pres;*)
2.17 + val ctxt = ctxt |> insert_assumptions pres;
2.18 in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end;
2.19
2.20 (* decide, where to get script/istate from:
3.1 --- a/test/Tools/isac/CLEANUP Fri May 20 09:12:40 2011 +0200
3.2 +++ b/test/Tools/isac/CLEANUP Fri May 20 13:43:25 2011 +0200
3.3 @@ -24,6 +24,13 @@
3.4 rm *.tar*
3.5 rm *.orig
3.6 cd ..
3.7 +cd Minisubpbl
3.8 + rm *~
3.9 + rm #*
3.10 + rm .#*
3.11 + rm *.tar*
3.12 + rm *.orig
3.13 + cd ..
3.14 cd Interpret
3.15 rm *~
3.16 rm #*
4.1 --- a/test/Tools/isac/Interpret/mstools.sml Fri May 20 09:12:40 2011 +0200
4.2 +++ b/test/Tools/isac/Interpret/mstools.sml Fri May 20 13:43:25 2011 +0200
4.3 @@ -105,8 +105,9 @@
4.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.5
4.6 "=(2)= preconds of (root-)met are known at start of lucas-interpreter";
4.7 -if get_assumptions_ pt p = [(*str2term "precond_rootmet x"*)] then ((*!!!!!!!!!!!!!!!!*))
4.8 +if get_assumptions_ pt p = [str2term "precond_rootmet x"] then ((*!!!!!!!!!!!!!!!!*))
4.9 else error "x+1=2 after start root-met no precondition";
4.10 +
4.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
4.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.14 @@ -133,7 +134,7 @@
4.15 (*del GOON*)terms2strs (get_assumptions_ pt p);
4.16
4.17 if get_assumptions_ pt p =
4.18 - [(*parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"*)
4.19 + [parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"
4.20 (*, precond-rootmet, precond_submet*)] then ()
4.21 else error "x+1=2 after start sub-met no precondition";
4.22
4.23 @@ -159,6 +160,9 @@
4.24 "=(6)= assumptions collected during lucas-interpretation for proving postcondition";
4.25 get_assumptions_ pt p = [(*precond_rootmet, precond_submet, sub_asm_out, sub_res, root_res*)];
4.26 terms2strs (get_assumptions_ pt p);
4.27 +
4.28 +
4.29 +
4.30 "----------- go through Model_Problem until nxt_tac -----";
4.31 "----------- go through Model_Problem until nxt_tac -----";
4.32 "----------- go through Model_Problem until nxt_tac -----";
5.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Fri May 20 09:12:40 2011 +0200
5.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Fri May 20 13:43:25 2011 +0200
5.3 @@ -40,9 +40,8 @@
5.4 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
5.5 get_loc pt p |> snd |> is_e_ctxt; (*false*)
5.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
5.7 +
5.8 val (pt'''', p'''') = (pt, p);
5.9 -
5.10 -locatetac tac (pt,p); (*GOON it = ("not-applicable",*)
5.11 "~~~~~ fun me, args:"; val (_,tac) = nxt;
5.12 val (pt, p) = case locatetac tac (pt,p) of
5.13 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
6.1 --- a/test/Tools/isac/Test_Isac.thy Fri May 20 09:12:40 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Fri May 20 13:43:25 2011 +0200
6.3 @@ -167,6 +167,103 @@
6.4 ML {*
6.5 *}
6.6 ML {*
6.7 +"----------- Minisubplb/500-met-sub-to-root.sml ------------------";
6.8 +
6.9 +"----------- Minisubplb/450-nxt-Check_Postcond -------------------";
6.10 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
6.11 +val (dI',pI',mI') =
6.12 + ("Test", ["sqroot-test","univariate","equation","test"],
6.13 + ["Test","squ-equ-test-subpbl1"]);
6.14 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.15 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.16 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.18 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.19 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.20 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.21 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
6.22 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
6.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
6.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
6.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
6.35 +val (pt''''', p''''') = (pt, p);
6.36 +
6.37 +"~~~~~ fun me, args:"; val (_,tac) = nxt;
6.38 +val (pt, p) = case locatetac tac (pt,p) of
6.39 + ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
6.40 +val (pt'''', p'''') = (pt, p);
6.41 +"~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
6.42 +val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
6.43 +tacis; (*= []*)
6.44 +val SOME pI = pIopt;
6.45 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
6.46 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
6.47 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
6.48 +val thy' = get_obj g_domID pt (par_pblobj pt p);
6.49 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
6.50 +val (tac_,is,(t,_)) = next_tac (thy',srls) (pt,pos) sc is;
6.51 +;tac_; (* = Check_Postcond' *)
6.52 +"~~~~~ fun nxt_solv, args:"; val ((Check_Postcond' (pI,_)), _, (pt, pos as (p,p_))) =
6.53 + (tac_, is, ptp);
6.54 + val pp = par_pblobj pt p
6.55 + val asm =
6.56 + (case get_obj g_tac pt p of
6.57 + Check_elementwise _ => (*collects and instantiates asms*)
6.58 + (snd o (get_obj g_result pt)) p
6.59 + | _ => get_assumptions_ pt (p,p_))
6.60 + handle _ => [] (*FIXME.WN030527 asms in subpbls not completely clear*)
6.61 + val metID = get_obj g_metID pt pp;
6.62 + val {srls=srls,scr=sc,...} = get_met metID;
6.63 + val loc as (ScrState (E,l,a,_,_,b), ctxt) = get_loc pt (p,p_);
6.64 + val thy' = get_obj g_domID pt pp;
6.65 + val thy = assoc_thy thy';
6.66 + val (_,_,(scval,scsaf)) = next_tac (thy',srls) (pt,(p,p_)) sc loc;
6.67 +*}
6.68 +ML {*
6.69 +;pp = []; (*false*)
6.70 + val ppp = par_pblobj pt (lev_up p);
6.71 + val thy' = get_obj g_domID pt ppp;
6.72 + val thy = assoc_thy thy';
6.73 + val metID = get_obj g_metID pt ppp;
6.74 + val {scr,...} = get_met metID;
6.75 + val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
6.76 + val ctxt'' = transfer_from_subproblem ctxt ctxt'
6.77 + val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
6.78 + val is = ScrState (E,l,a,scval,scsaf,b)
6.79 +*}
6.80 +ML {*
6.81 +"~~~~~ fun generate1, args:"; val (thy, (Check_Postcond' (pI,(scval,asm))), l, (p,p_), pt) = (thy, tac_, (is, ctxt''), (pp, Res), pt);
6.82 +*}
6.83 +ML {*
6.84 +append_result pt p l
6.85 +*}
6.86 +ML {*
6.87 +asm
6.88 +*}
6.89 +ML {*
6.90 +*}
6.91 +ML {*
6.92 +scval
6.93 +*}
6.94 +ML {*
6.95 +(*
6.96 +val (pt,c) = append_result pt p l (scval, map str2term asm) Complete
6.97 +*)
6.98 +*}
6.99 +ML {*
6.100 +*}
6.101 +ML {*
6.102 +*}
6.103 +ML {*
6.104 *}
6.105 ML {*
6.106 *}
6.107 @@ -175,11 +272,25 @@
6.108 ML {*
6.109 *}
6.110
6.111 +
6.112 +
6.113 +
6.114 +
6.115 +
6.116 +
6.117 ML {*
6.118 -(*############################################################################*)
6.119 +generate1 thy tac_ (is, ctxt'') (pp, Res) pt; (*WAS
6.120 + exception Option raised (line 81 of "General/basics.ML")*)
6.121 *}
6.122 ML {*
6.123 -
6.124 +(*
6.125 +;nxt_solv tac_ is ptp; (*WAS exception Option raised (line 81 of "General/basics.ML")*)
6.126 +*)
6.127 +*}
6.128 +ML {*
6.129 +;step p'''' ((pt'''', e_pos'),[]); (* WAS = ("helpless", *)
6.130 +val (p,_,f,nxt,_,pt) = me nxt p''''' [] pt'''''; (*nxt = Check_Postcond ["linear","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
6.131 +show_pt pt
6.132 *}
6.133 end
6.134