1.1 --- a/src/Tools/isac/Interpret/generate.sml Wed Mar 14 17:12:43 2012 +0100
1.2 +++ b/src/Tools/isac/Interpret/generate.sml Sat Mar 17 11:06:46 2012 +0100
1.3 @@ -372,97 +372,79 @@
1.4 generate1 thy (Begin_Trans' t) l (lev_on p,Frm) pt
1.5
1.6 | generate1 thy (End_Trans' tasm) l (p,p_) pt =
1.7 - let val p' = lev_up p
1.8 - val (pt,c) = append_result pt p' l tasm Complete;
1.9 - in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)),
1.10 - pt) end
1.11 + let
1.12 + val p' = lev_up p
1.13 + val (pt,c) = append_result pt p' l tasm Complete;
1.14 + in ((p',Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str t)), pt) end
1.15
1.16 - | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) (is, ctxt)
1.17 - (p,p_) pt =
1.18 - let (*val _= tracing("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));*)
1.19 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.20 - (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
1.21 - val pt = update_branch pt p TransitiveB (*040312*)
1.22 - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.23 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.24 - pt) end
1.25 + | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f', asm))) (is, ctxt) (p,p_) pt =
1.26 + let
1.27 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.28 + (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
1.29 + val pt = update_branch pt p TransitiveB
1.30 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.31
1.32 - | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt)
1.33 - (p,p_) pt =
1.34 - let (*val _= tracing("###generate1 Rewrite': pos= "^pos'2str (p,p_))*)
1.35 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.36 - (Rewrite thm') (f',asm) Complete
1.37 - val pt = update_branch pt p TransitiveB (*040312*)
1.38 - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
1.39 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.40 - pt)end
1.41 + | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.42 + let
1.43 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.44 + (Rewrite thm') (f',asm) Complete
1.45 + val pt = update_branch pt p TransitiveB
1.46 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt)end
1.47
1.48 - | generate1 thy (Rewrite_Asm' all) l p pt =
1.49 - generate1 thy (Rewrite' all) l p pt
1.50 + | generate1 thy (Rewrite_Asm' all) l p pt = generate1 thy (Rewrite' all) l p pt
1.51
1.52 - | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt)
1.53 - (p,p_) pt =
1.54 -(* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) =
1.55 - (assoc_thy "Isac", tac_, is, pos, pt);
1.56 - *)
1.57 - let (*val _=tracing("###generate1 Rewrite_Set_Inst': pos= "^pos'2str(p,p_))*)
1.58 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.59 - (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.60 - val pt = update_branch pt p TransitiveB (*040312*)
1.61 - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.62 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.63 - pt) end
1.64 + | generate1 thy (Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.65 + let
1.66 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.67 + (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
1.68 + val pt = update_branch pt p TransitiveB
1.69 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.70
1.71 - | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_)
1.72 - pt =
1.73 - let val ctxt' = insert_assumptions asm ctxt
1.74 - val (pt,c) = cappend_form pt p (is, ctxt') f
1.75 - val pt = update_branch pt p TransitiveB (*040312*)
1.76 - val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.77 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.78 - val pos' = ((lev_on o lev_dn) p, Frm)
1.79 - in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.80 + | generate1 thy (Detail_Set_Inst' (_,_,subs,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
1.81 + let
1.82 + val ctxt' = insert_assumptions asm ctxt
1.83 + val (pt,c) = cappend_form pt p (is, ctxt') f
1.84 + val pt = update_branch pt p TransitiveB
1.85 +
1.86 + val is = init_istate (Rewrite_Set_Inst (subst2subs subs, id_rls rls)) f
1.87 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.88 + val pos' = ((lev_on o lev_dn) p, Frm)
1.89 + in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.90
1.91 | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) (is, ctxt) (p,p_) pt =
1.92 - let (*val _= tracing("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))*)
1.93 - val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.94 - (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.95 - val pt = update_branch pt p TransitiveB (*040312*)
1.96 - (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
1.97 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.98 - pt) end
1.99 + let
1.100 + val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
1.101 + (Rewrite_Set (id_rls rls')) (f',asm) Complete
1.102 + val pt = update_branch pt p TransitiveB
1.103 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.104
1.105 | generate1 thy (Detail_Set' (_,_,rls,f,(f',asm))) (is, ctxt) (p,p_) pt =
1.106 - let val (pt,c) = cappend_form pt p (is, ctxt) f
1.107 - val pt = update_branch pt p TransitiveB (*040312*)
1.108 + let
1.109 + val ctxt' = insert_assumptions asm ctxt
1.110 + val (pt,c) = cappend_form pt p (is, ctxt') f
1.111 + val pt = update_branch pt p TransitiveB
1.112
1.113 - val is = init_istate (Rewrite_Set (id_rls rls)) f
1.114 - val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt)
1.115 - val pos' = ((lev_on o lev_dn) p, Frm)
1.116 - in (*implicit Take*) generate1 thy tac_ (is, ctxt) pos' pt end
1.117 + val is = init_istate (Rewrite_Set (id_rls rls)) f
1.118 + val tac_ = Apply_Method' (e_metID, SOME t, is, ctxt')
1.119 + val pos' = ((lev_on o lev_dn) p, Frm)
1.120 + in (*implicit Take*) generate1 thy tac_ (is, ctxt') pos' pt end
1.121
1.122 | generate1 thy (Check_Postcond' (pI, (scval, asm))) l (p,p_) pt =
1.123 let val (pt,c) = append_result pt p l (scval, asm) Complete
1.124 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p),
1.125 - Nundef, term2str scval)), pt) end
1.126 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str scval)), pt) end
1.127
1.128 | generate1 thy (Calculate' (thy',op_,f,(f',thm'))) l (p,p_) pt =
1.129 - let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
1.130 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.131 - pt) end
1.132 + let val (pt,c) = cappend_atomic pt p l f (Calculate op_) (f',[]) Complete;
1.133 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.134
1.135 | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
1.136 - let(*val _=tracing("###generate1 Check_elementwise': p= "^pos'2str(p,p_))*)
1.137 - val (pt,c) = cappend_atomic pt p l consts
1.138 - (Check_elementwise pred) (f',asm) Complete;
1.139 - in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
1.140 - pt) end
1.141 + let
1.142 + val (pt,c) = cappend_atomic pt p l consts (Check_elementwise pred) (f',asm) Complete;
1.143 + in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')), pt) end
1.144
1.145 | generate1 thy (Or_to_List' (ors,list)) l (p,p_) pt =
1.146 - let val (pt,c) = cappend_atomic pt p l ors
1.147 - Or_to_List (list,[]) Complete;
1.148 - in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)),
1.149 - pt) end
1.150 + let val (pt,c) = cappend_atomic pt p l ors Or_to_List (list,[]) Complete;
1.151 + in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str list)), pt) end
1.152
1.153 | generate1 thy (Substitute' (_, _, subte, t, t')) l (p,p_) pt =
1.154 let
1.155 @@ -477,9 +459,8 @@
1.156 cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
1.157 in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
1.158
1.159 - | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f))
1.160 - l (p,p_) pt =
1.161 - let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
1.162 + | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) l (p,p_) pt =
1.163 + let
1.164 val (pt,c) =
1.165 cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
1.166 val pt = update_ctxt pt p ctxt